diff --git a/ASSUMPTIONS.md b/ASSUMPTIONS.md index b6d404c..e9bbb43 100644 --- a/ASSUMPTIONS.md +++ b/ASSUMPTIONS.md @@ -34,6 +34,7 @@ Cross-references use `[[A-TG-N.M]]` syntax, resolved here. | A-TG-7.1 | MATH | Word problem in the braid group `B_n` is solvable in polynomial time (Birman–Ko–Lee / Garside normal form) | TG-7 | Birman–Ko–Lee 1998; _A New Approach to the Word and Conjugacy Problems in the Braid Groups_ | | A-TG-7.2 | IMPL | `braidEquiv` (`proofs/Tangle.lean`) and `braid_equiv.ml` implement Dehornoy handle reduction **correctly**, and agree with each other. Since the 2026-07-29 ruling (#50) routed `==` through them, this is **load-bearing for the semantics of `==`**: the Step relation's metatheory is proven only *relative to* `braidEquiv`, never that it decides braid-group equality. Evidenced by testing (2220 + 8 assertions), not proof. Retired by the mechanised Garside/Dehornoy proof (#51, research-grade). The Lean port is additionally **fuel-bounded**, so termination is assumed rather than proven. | TG-7 | `compiler/lib/braid_equiv.ml`; `proofs/Tangle.lean` §BRAID-GROUP EQUIVALENCE; `compiler/test/tg7` | | A-TG-92.1 | MATH | Comparing braid words of different widths is decided in B_max(n,m) via the standard embedding Bn -> Bn+1 (adjoin a strand no generator touches). Used to justify widening `T-Eq-Word` (#92) and the match-arm width join. The embedding is standard mathematics but is **asserted in prose, not mechanised** — no Lean lemma states it. What IS machine-checked is that the metatheory (Progress/Preservation/Determinism/TypeSafety, infer_sound/complete) holds under the widened rule, and that OCaml `infer_expr` still agrees with Lean `infer` on the corpus (TG-3, 496 obligations). | TG-7 / #92 | `proofs/Tangle.lean` (`tEqWord`, `infer`); `compiler/lib/typecheck.ml` | +| A-TG-11.1 | DESIGN | The simply-typed shadow is FAITHFUL to `epistemic-types`: `Epi[k,rho,tau]` models `Epi K k A` (Warrant.agda) with standpoints as Nat indices rather than an arbitrary index set K, and it omits the upstream `LawfulModality` functor laws, `FactiveModality.reflect` and `ReturnModality.return` (all deliberately opt-in upstream). What IS mechanised here is non-factivity: no elimination yields the claim. Erasure and quantity are NOT modelled - the claim is carried in the value rather than erased, because erasing it would break uniqueness of typing in a system without quantities. A QTT treatment (quantity 0 for the claim) would be the faithful version. | TG-11 | `proofs/Tangle.lean` section EPISTEMIC; `epistemic-types/src/EpistemicTypes/{Base,Warrant,EchoBridge}.agda` | | A-TG-8.1 | DESIGN | Each dialect's grammar is a strict superset of core's EBNF (`tangle.ebnf`) | TG-8 | `dialects/*/grammar.ebnf` | | A-TG-8.2 | DESIGN | Each dialect's typing rules are additive (new constructors + their typing rules only; no modification of existing rules) | TG-8 | Per-dialect spec | | A-TG-9.1 | DESIGN | `tangle-lsp` emits diagnostics in four documented categories (`PARSE_ERROR`, `MISSPELLING_HINT`, `STRUCTURAL_HINT`, `NAME_HINT`); only `PARSE_ERROR` corresponds to a grammar-level rejection. The other three are LSP-only by design (Option B from TG-9 audit; Option A — full refinement via FFI to `typecheck.ml` — remains queued at #28). Each emission site is tagged in the `Diagnostic.source` field as `tangle-lsp[CATEGORY]`. | TG-9 | `compiler/tangle-lsp/src/backend.rs`; `compiler/tangle-lsp/docs/lsp-diagnostic-categories.md` | diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md index 72e8f23..eaa19f8 100644 --- a/PROOF-NEEDS.md +++ b/PROOF-NEEDS.md @@ -60,6 +60,7 @@ Cross-referenced to [PROOF-NARRATIVE.md §3](PROOF-NARRATIVE.md#3-remaining-obli | TG-5 | `compositional.ml` (418 LoC) rewriter preserves types | TP | OCaml property test | P2 | — | **LANDED** (`compiler/test/tg5/tg5_invariants.ml`, 189 assertions in `dune runtest`). compositional is below the Ty layer, so "preserves types" = preserves the PD-lowering structural invariants + echo residue-recovery: `OpenWord`/`ClosedDiagram`/`EchoClosed` each pinned (closedness, `\|crossings\|`=unit-length, source unit-expanded, **verbatim residue** for `EchoClose` with `expand(residue)=diagram word` and echo-diagram pdv1-identical to plain `close`), error paths, count pins. Lean IR model = optional later rung | | TG-6 | WASM compilation preserves semantics (source eval ≡ wasm exec) | TP / ALG | differential + Lean bisimulation | P1 | — | **RUNG LANDED (differential)**: `compiler/tangle-wasm/tests/differential.rs` EXECUTES the generated wasm with the `wasmi` interpreter (dev-dep) and checks the braid strand-permutation equals an independent reference model (trefoil, non-commuting pairs, braid-relation pairs, 5-strand weave). Validates codegen vs the permutation semantics; not a cross-binary diff against `eval.ml`, and Markov helpers untested. Full source↔wasm bisimulation (WasmCert) remains research-grade | | TG-7 | `Step.eqBraids` decides braid-group equivalence (not list equality) | ALG / DOM | OCaml + Lean 4 | P2 | — | **SEMANTICS LANDED 2026-07-29** (owner ruling #50 → (a) true braid-group equivalence). `==` on braids now decides braid-group equality in BOTH engines: OCaml `eval.ml` `Eq`/`Isotopy` route through `compiler/lib/braid_equiv.ml`; Lean `Step.eqBraids`/`eqIdBraid`/`eqBraidId` (and the three `echoEq` counterparts) use `braidEquiv`, a faithful in-Lean port of the same Dehornoy procedure. Progress/Preservation/Determinism re-verified unchanged (they need only a total function into `Bool`). Tested: `compiler/test/tg7` 2220 assertions + 8 new semantics-distinguishing cases in `test_eval.ml`. **Remaining (research-grade): the mechanised Garside/Dehornoy correctness proof — `braidEquiv` is TRUSTED, NOT PROVEN; the Step relation is proven only RELATIVE to it** | +| TG-11 | Epistemic types: `Epi[k, rho, tau]` former + `warrant`/`epiVal`/`evidence`, with Progress/Preservation/Determinism/TypeSafety extended to cover them, and NON-FACTIVITY established (no elimination delivers the claim) | TP / DOM | Lean 4 | P1 | - | **LANDED**: `proofs/Tangle.lean` §EPISTEMIC. Six capstones: `epi_evidence_recovers`, `epi_claim_is_opaque`, `epi_only_yields_evidence`, `epi_distinguishes_standpoints`, `epi_roundtrip_typed`, `epi_over_echo_typed`. Mirrors `hyperpolymath/epistemic-types` (Warrant.agda / Base.agda / EchoBridge.agda). TG-3 extended: 4 new pins, differential regenerated and kernel-checked (496 obligations, 0 errors) | | TG-8 | Each dialect (braid-calculus, quantum-circuit, skein-algebra, string-diagram, virtual-knot) is a conservative extension of core | TP | OCaml model + Lean per-dialect | P3 | — | **TEMPLATE LANDED (virtual-knot)**: `compiler/lib/dialect_vk.ml` models VBₙ ⊃ Bₙ as core + a virtual layer that DELEGATES to `Braid_equiv` on the real fragment, so conservativity holds by construction; `compiler/test/tg8` (2311 assertions) verifies faithful embedding, core-delegation, invariant agreement, proper extension, virtual involution, honest undecided-frontier. Remaining: surface-syntax parser integration, the other 4 dialects (replicate the template), and a Lean conservativity proof | | TG-9 | LSP diagnostics are a subset of `HasType` failures (no LSP-only diagnostics) | INV | Audit + refactor | P2 | — | **LANDED** (`tangle-lsp` delegates all diagnostics to `tanglec --check` ⇒ `compiler/lib/check.ml`; hand-rolled LSP-only false positives removed. Subset holds by construction. Tests: `test_check.ml` + tangle-lsp unit/delegation tests) | | TG-10 | Echo-types integrated into the type system: `Echo[ρ,τ]` former + `echoClose`/`lower`/`residue`/`echoAdd`/`echoEq` + product type (`pair`/`fst`/`snd`), with Progress/Preservation/Determinism/TypeSafety extended to cover them and the non-injectivity / residue-recovery capstones proven | TP / DOM | Lean 4 | P1 | — | **LANDED** (`proofs/Tangle.lean` §ECHO-TYPES) | diff --git a/compiler/lib/ast.ml b/compiler/lib/ast.ml index 692799e..f887dc6 100644 --- a/compiler/lib/ast.ml +++ b/compiler/lib/ast.ml @@ -93,6 +93,14 @@ and expr = | EchoAdd of expr * expr (* echo-preserving addition (residue = summand pair) *) | EchoEq of expr * expr (* echo-preserving equality (residue = operand pair) *) + (* ---- Epistemic (warranted claim) — mirrors §EPISTEMIC in + * proofs/Tangle.lean and epistemic-types' Warrant.agda. + * NON-FACTIVE: `Evidence` is the only elimination. There is no + * operation taking a warrant to the thing warranted. ---- *) + | Warrant of int * expr * expr (* warrant κ claim evidence (redex) *) + | EpiVal of int * expr * expr (* formed warrant: standpoint, claim, token *) + | Evidence of expr (* project the evidence token (ONLY elimination) *) + (* ---- Literals ---- *) | BraidLit of generator list | Identity diff --git a/compiler/lib/eval.ml b/compiler/lib/eval.ml index 8d748b5..cd909cc 100644 --- a/compiler/lib/eval.ml +++ b/compiler/lib/eval.ml @@ -42,6 +42,11 @@ type value = | VFun of string list * expr * env (** Closure: params, body, captured env *) | VUnit (** Unit / void result *) | VInvariant of string * string (** Invariant name, result string *) + | VEpi of int * value * value (** Formed warrant: standpoint, claim, token. + The claim is CARRIED but has no + projection — `Evidence` is the only + elimination. Mirrors epiVal in + proofs/Tangle.lean. *) | VEcho of value * value (** Formed echo: residue, result — mirrors [echoVal] in proofs/Tangle.lean *) | VPair of value * value (** Product value *) @@ -92,6 +97,8 @@ let rec pp_value (v : value) : string = | VFun _ -> "" | VUnit -> "()" | VInvariant (name, result) -> Printf.sprintf "%s = %s" name result + | VEpi (k, c, ev) -> + Printf.sprintf "warrant[%d](%s, %s)" k (pp_value c) (pp_value ev) | VEcho (res, result) -> "echo(" ^ pp_value res ^ ", " ^ pp_value result ^ ")" | VPair (a, b) -> @@ -396,6 +403,21 @@ let rec eval_expr (env : env) (e : expr) : value = (pp_value v) end + (* Epistemic. `warrant` forms the value; `evidence` is the sole projection + and yields the TOKEN. There is deliberately no operation returning the + claim — holding a warrant is not holding the fact. *) + | Warrant (k, claim, ev) -> + VEpi (k, eval_expr env claim, eval_expr env ev) + + | EpiVal (k, claim, ev) -> + VEpi (k, eval_expr env claim, eval_expr env ev) + + | Evidence e -> + begin match eval_expr env e with + | VEpi (_, _, ev) -> ev + | v -> eval_error "evidence requires a warrant, got %s" (pp_value v) + end + | Cap (_e1, _e2) -> (* Cap creates a tangle that absorbs two strands — a single-crossing cup/cap pair. Represented as an empty closed tangle. *) diff --git a/compiler/lib/pretty.ml b/compiler/lib/pretty.ml index 17eb0a9..51f4c50 100644 --- a/compiler/lib/pretty.ml +++ b/compiler/lib/pretty.ml @@ -276,6 +276,17 @@ let rec pp_expr ctx = function emit ctx " yield strands "; pp_strand_list ctx w.weave_outputs + | Warrant (k, c, ev) -> + emit ctx "warrant["; emit ctx (string_of_int k); emit ctx "]("; + pp_expr ctx c; emit ctx ", "; pp_expr ctx ev; emit ctx ")" + + | EpiVal (k, c, ev) -> + emit ctx "epiVal["; emit ctx (string_of_int k); emit ctx "]("; + pp_expr ctx c; emit ctx ", "; pp_expr ctx ev; emit ctx ")" + + | Evidence e -> + emit ctx "evidence("; pp_expr ctx e; emit ctx ")" + | Crossing (a, op, b) -> emit ctx "("; emit ctx a; diff --git a/compiler/lib/typecheck.ml b/compiler/lib/typecheck.ml index 32c1047..f40d8d1 100644 --- a/compiler/lib/typecheck.ml +++ b/compiler/lib/typecheck.ml @@ -44,6 +44,11 @@ type ty = | TProd of ty * ty (** ρ × σ — product / residue carrier for lossy ops *) | TEcho of ty * ty (** Echo[ρ, τ] — structured loss: residue ρ, result τ. Mirrors Ty.echo in proofs/Tangle.lean. *) + | TEpi of int * ty * ty (** Epi[κ, ρ, τ] — at standpoint κ, evidence ρ + purporting to support claim τ. Mirrors + Ty.epi in proofs/Tangle.lean. τ appears + in the type but NO rule eliminates to it: + a warrant is not knowledge. *) (** Function signature: (param_types) -> return_type. *) type fun_sig = { @@ -100,6 +105,7 @@ let rec pp_ty = function | TStr -> "Str" | TProd (a, b) -> Printf.sprintf "(%s * %s)" (pp_ty a) (pp_ty b) | TEcho (r, t) -> Printf.sprintf "Echo[%s, %s]" (pp_ty r) (pp_ty t) + | TEpi (k, r, t) -> Printf.sprintf "Epi[%d, %s, %s]" k (pp_ty r) (pp_ty t) (* ================================================================== *) (* Environment operations *) @@ -218,6 +224,26 @@ let rec infer_expr (gamma : env) (sigma : strand_ctx) (e : expr) : ty = ) wb.weave_outputs in TTangle (input_boundary, output_boundary) + (* [T-Warrant] / [T-Epi-Val] / [T-Evidence] — epistemic. + Note the absence: no case here produces τ from an Epi. `Evidence` yields + the token type ρ, and that is the only elimination. Contrast `Lower`, + which DOES deliver an echo's result. *) + | Warrant (k, claim, ev) -> + let t_claim = infer_expr gamma sigma claim in + let t_ev = infer_expr gamma sigma ev in + TEpi (k, t_ev, t_claim) + + | EpiVal (k, claim, ev) -> + let t_claim = infer_expr gamma sigma claim in + let t_ev = infer_expr gamma sigma ev in + TEpi (k, t_ev, t_claim) + + | Evidence e -> + begin match infer_expr gamma sigma e with + | TEpi (_, rho, _) -> rho + | t -> type_error "evidence requires an Epi[k, rho, tau], got %s" (pp_ty t) + end + (* ---- Variables [T-Var] ---- *) | Var name -> @@ -652,6 +678,7 @@ and strand_type_of_ty (t : ty) : strand_type = | TTangle _ -> StrandDefault | TProd _ -> StrandDefault | TEcho _ -> StrandDefault + | TEpi _ -> StrandDefault (** Convert a strand_type to a boundary element for self-crossing. *) and strand_to_type (st : strand_type) : strand_type = st @@ -725,7 +752,9 @@ let rec expr_calls (f : string) (e : expr) : bool = | Cap (e1, e2) | Cup (e1, e2) | Pair (e1, e2) | EchoAdd (e1, e2) | EchoEq (e1, e2) -> go e1 || go e2 | UnaryOp (_, e1) | Close e1 | Mirror e1 | Reverse e1 | Simplify e1 - | Twist e1 | EchoClose e1 | Lower e1 | Residue e1 | Fst e1 | Snd e1 -> go e1 + | Twist e1 | EchoClose e1 | Lower e1 | Residue e1 | Fst e1 | Snd e1 + | Evidence e1 -> go e1 + | Warrant (_, c, ev) | EpiVal (_, c, ev) -> go c || go ev | Weave wb -> go wb.weave_body | BraidLit _ | Identity | BoolLit _ | IntLit _ | FloatLit _ | StringLit _ | Var _ | Crossing _ -> false diff --git a/compiler/test/test_typecheck.ml b/compiler/test/test_typecheck.ml index a78d663..c7fc4cc 100644 --- a/compiler/test/test_typecheck.ml +++ b/compiler/test/test_typecheck.ml @@ -1089,6 +1089,40 @@ let test_echo_types () = ] in infer [] (Match (BraidLit [sigma 1], arms)) = TWord 2); + (* ---------------------------------------------------------------- *) + (* EPISTEMIC TYPES. The commitment is NON-FACTIVITY: holding a warrant *) + (* is not holding the fact. `Evidence` is the ONLY elimination, and it *) + (* yields the token type, never the claim type. *) + (* ---------------------------------------------------------------- *) + + test "epi: warrant types as Epi[k, rho, tau]" (fun () -> + infer [] (Warrant (0, IntLit 1, BraidLit [sigma 1])) + = TEpi (0, TWord 2, TNum)); + + test "epi: evidence yields the EVIDENCE type, not the claim" (fun () -> + (* The heart of it. Claim is Num, evidence is Word[2]; the projection + must give Word[2]. If it gave Num, the warrant would be factive. *) + infer [] (Evidence (Warrant (0, IntLit 1, BraidLit [sigma 1]))) + = TWord 2); + + test "epi: NO elimination delivers the claim type" (fun () -> + (* Guard: evidence must never return the claim type when the two differ. *) + infer [] (Evidence (Warrant (0, StringLit "claimed", BraidLit [sigma 1]))) + <> TStr); + + test "epi: standpoints are distinguished" (fun () -> + infer [] (Warrant (1, IntLit 1, IntLit 2)) + <> infer [] (Warrant (2, IntLit 1, IntLit 2))); + + test "epi: composes over echo without collapsing into it" (fun () -> + (* EpistemicEcho from EchoBridge.agda: standpoint k with access to an + echo. The two modalities nest; neither absorbs the other. *) + infer [] (Warrant (1, IntLit 0, EchoClose (BraidLit [sigma 1]))) + = TEpi (1, TEcho (TWord 2, TWord 0), TNum)); + + test "epi: evidence of a non-warrant is rejected" (fun () -> + raises (fun () -> infer [] (Evidence (IntLit 1)))); + test "#92 match arms of genuinely different KINDS still fail" (fun () -> let arms = [ { arm_pattern = PatIdentity; arm_body = IntLit 1 }; diff --git a/compiler/test/tg3/tg3_emit.ml b/compiler/test/tg3/tg3_emit.ml index f04cce9..1b4f84b 100644 --- a/compiler/test/tg3/tg3_emit.ml +++ b/compiler/test/tg3/tg3_emit.ml @@ -61,6 +61,7 @@ let rec lean_ty (t : ty) : string = | TWord n -> Printf.sprintf "(.word %d)" n | TEcho (r, v) -> Printf.sprintf "(.echo %s %s)" (lean_ty r) (lean_ty v) | TProd (a, b) -> Printf.sprintf "(.prod %s %s)" (lean_ty a) (lean_ty b) + | TEpi (k, r, t) -> Printf.sprintf "(.epi %d %s %s)" k (lean_ty r) (lean_ty t) | TTangle _ -> failwith "TG-3: TTangle has no Lean image — a non-core term leaked into the corpus" @@ -69,6 +70,7 @@ let rec lean_ty (t : ty) : string = let rec ty_tangle_free = function | TTangle _ -> false | TEcho (a, b) | TProd (a, b) -> ty_tangle_free a && ty_tangle_free b + | TEpi (_, r, t) -> ty_tangle_free r && ty_tangle_free t | TWord _ | TNum | TStr | TBool -> true (* ================================================================== *) @@ -130,6 +132,13 @@ let rec lean_expr (scope : string list) (e : expr) : string = | Snd e1 -> Printf.sprintf "(.snd %s)" (lean_expr scope e1) | EchoAdd (a, b) -> Printf.sprintf "(.echoAdd %s %s)" (lean_expr scope a) (lean_expr scope b) | EchoEq (a, b) -> Printf.sprintf "(.echoEq %s %s)" (lean_expr scope a) (lean_expr scope b) + (* Epistemic is IN the mechanised core (proofs/Tangle.lean §EPISTEMIC), so + these are translated, not rejected. *) + | Warrant (k, c, ev) -> + Printf.sprintf "(.warrant %d %s %s)" k (lean_expr scope c) (lean_expr scope ev) + | EpiVal (k, c, ev) -> + Printf.sprintf "(.epiVal %d %s %s)" k (lean_expr scope c) (lean_expr scope ev) + | Evidence e1 -> Printf.sprintf "(.evidence %s)" (lean_expr scope e1) (* Non-core: must never appear in the corpus (close is the boundary gateway). *) | FloatLit _ | BinOp ((Sub | Mul | Div | Isotopy), _, _) | UnaryOp _ | Close _ | Mirror _ | Reverse _ | Simplify _ | Cap _ | Cup _ | Twist _ @@ -360,6 +369,17 @@ let check () = (* #92: widths need not agree, so this is now WELL-TYPED rather than rejected. It is the `identity == braid` shape the Lean step relation has always had rules for (eqIdBraid / eqBraidId). *) + (* Epistemic pins: OCaml infer_expr must agree with Lean infer on the new + constructors. The `evidence` pin is the important one: it must yield the + EVIDENCE type, never the claim type. *) + pin "warrant num/word" (Warrant (0, IntLit 1, BraidLit [s 1])) + (TEpi (0, TWord 2, TNum)); + pin "warrant word/str" (Warrant (3, BraidLit [s 1], StringLit "ev")) + (TEpi (3, TStr, TWord 2)); + pin "evidence yields rho" (Evidence (Warrant (0, IntLit 1, BraidLit [s 1]))) + (TWord 2); + pin "epi over echo" (Warrant (1, IntLit 0, EchoClose (BraidLit [s 1]))) + (TEpi (1, TEcho (TWord 2, TWord 0), TNum)); pin "eq diff-width word" (BinOp (Eq, BraidLit [s 1], Identity)) TBool; (* 3. Reject pins — these must raise Type_error. *) diff --git a/proofs/Tangle.lean b/proofs/Tangle.lean index 2e202df..19d4905 100644 --- a/proofs/Tangle.lean +++ b/proofs/Tangle.lean @@ -86,6 +86,26 @@ inductive Ty where -- residue (domain witness x : A), τ is the result -- (codomain point y). See §ECHO-TYPES below. | prod : Ty → Ty → Ty -- product (pair) type ρ × σ; residue carrier for lossy binary ops + | epi : Nat → Ty → Ty → Ty + -- Epi[κ, ρ, τ]: at STANDPOINT κ, evidence of type ρ + -- purporting to support a claim of type τ. The + -- simply-typed shadow of epistemic-types' + -- `Epi K κ A` (EpistemicTypes/Warrant.agda), whose + -- record carries `warrant` + `evidence` and — the + -- whole point — NO field of type A. + -- + -- κ is a standpoint index: an agent, evidence + -- state, accessibility context or warrant regime. + -- Indexed by Nat, mirroring `word : Nat → Ty`. + -- + -- NON-FACTIVE BY CONSTRUCTION: τ appears in the + -- type but there is NO elimination rule producing + -- τ. Holding `Epi[κ,ρ,τ]` does not give you τ — + -- that is the difference between knowing and + -- having a warrant. Upstream models the factive + -- case as a SEPARATE record (`FactiveModality` + -- with `reflect`), never as a modality with a + -- missing proof; this mirrors that choice. deriving DecidableEq, Repr /-- Core expression AST. Mirrors the OCaml AST in compiler/lib/ast.ml. @@ -117,6 +137,13 @@ inductive Expr where | pair : Expr → Expr → Expr -- product introduction | fst : Expr → Expr -- first projection | snd : Expr → Expr -- second projection + -- Epistemic (warranted claim). `warrant κ c ev` is the redex; it reduces to + -- the formed value `epiVal κ c ev`. The claim `c` is RETAINED in the value + -- (so typing stays unique) but is unreachable: `evidence` is the only + -- elimination, and it yields the token, never the claim. + | warrant : Nat → Expr → Expr → Expr -- warrant κ claim evidence (redex) + | epiVal : Nat → Expr → Expr → Expr -- formed warrant: standpoint, claim, token + | evidence : Expr → Expr -- project the evidence token (ONLY elimination) | echoAdd : Expr → Expr → Expr -- echo-preserving addition (residue = pair of summands) | echoEq : Expr → Expr → Expr -- echo-preserving equality (residue = operand pair) deriving DecidableEq, Repr @@ -130,6 +157,7 @@ inductive IsValue : Expr → Prop where | braidLit : ∀ gs, IsValue (.braidLit gs) | echoVal : ∀ {r v}, IsValue r → IsValue v → IsValue (.echoVal r v) -- a formed echo value (residue r, result v) | pair : ∀ {a b}, IsValue a → IsValue b → IsValue (.pair a b) + | epiVal : ∀ {κ c ev}, IsValue c → IsValue ev → IsValue (.epiVal κ c ev) -- ═══════════════════════════════════════════════════════════════════════ -- WIDTH @@ -305,6 +333,9 @@ def shift (d : Nat) (c : Nat) : Expr → Expr | .residue a => .residue (shift d c a) | .echoVal a b => .echoVal (shift d c a) (shift d c b) | .pair a b => .pair (shift d c a) (shift d c b) + | .warrant κ cl ev => .warrant κ (shift d c cl) (shift d c ev) + | .epiVal κ cl ev => .epiVal κ (shift d c cl) (shift d c ev) + | .evidence e => .evidence (shift d c e) | .fst a => .fst (shift d c a) | .snd a => .snd (shift d c a) | .echoAdd a b => .echoAdd (shift d c a) (shift d c b) @@ -331,6 +362,9 @@ def subst (j : Nat) (s : Expr) : Expr → Expr | .residue a => .residue (subst j s a) | .echoVal a b => .echoVal (subst j s a) (subst j s b) | .pair a b => .pair (subst j s a) (subst j s b) + | .warrant κ cl ev => .warrant κ (subst j s cl) (subst j s ev) + | .epiVal κ cl ev => .epiVal κ (subst j s cl) (subst j s ev) + | .evidence e => .evidence (subst j s e) | .fst a => .fst (subst j s a) | .snd a => .snd (subst j s a) | .echoAdd a b => .echoAdd (subst j s a) (subst j s b) @@ -403,6 +437,22 @@ inductive HasType : Ctx → Expr → Ty → Prop where HasType Γ e₁ .str → HasType Γ e₂ .str → HasType Γ (.eq e₁ e₂) .bool + -- ── Epistemic (warranted claim) ───────────────────────────────────── + -- Note what is ABSENT: there is no rule with conclusion `HasType Γ _ τ` + -- from a premise `HasType Γ e (.epi κ ρ τ)`. A warrant does not discharge + -- its claim. Upstream states the same thing by giving `Warrant` only an + -- `Evidence` field and putting extraction in a separate `SoundWarrant`. + | tWarrant (Γ : Ctx) (κ : Nat) (c ev : Expr) (ρ τ : Ty) : -- [T-Warrant] + HasType Γ c τ → -- what is claimed + HasType Γ ev ρ → -- the evidence token + HasType Γ (.warrant κ c ev) (.epi κ ρ τ) + | tEpiVal (Γ : Ctx) (κ : Nat) (c ev : Expr) (ρ τ : Ty) : -- [T-Epi-Val] + HasType Γ c τ → + HasType Γ ev ρ → + HasType Γ (.epiVal κ c ev) (.epi κ ρ τ) + | tEvidence (Γ : Ctx) (e : Expr) (κ : Nat) (ρ τ : Ty) : -- [T-Evidence] + HasType Γ e (.epi κ ρ τ) → + HasType Γ (.evidence e) ρ -- ρ, NEVER τ | tEchoClose (Γ : Ctx) (e : Expr) (n : Nat) : -- [T-Echo-Close] HasType Γ e (.word n) → -- echo-intro for `close`: HasType Γ (.echoClose e) (.echo (.word n) (.word 0)) -- residue Word[n], result Word[0] @@ -483,6 +533,16 @@ inductive Step : Expr → Expr → Prop where | eqIdId : Step (.eq .identity .identity) (.boolLit true) | eqIdBraid : Step (.eq .identity (.braidLit gs)) (.boolLit (isTrivialBraid gs)) | eqBraidId : Step (.eq (.braidLit gs) .identity) (.boolLit (isTrivialBraid gs)) + -- Epistemic: `warrant` is a redex reducing into a formed `epiVal`; `evidence` + -- is the sole projection off it, and yields the TOKEN. There is deliberately + -- no projection yielding the claim. + | warrantClaim : Step c c' → Step (.warrant κ c ev) (.warrant κ c' ev) + | warrantEv : IsValue c → Step ev ev' → Step (.warrant κ c ev) (.warrant κ c ev') + | warrantForm : IsValue c → IsValue ev → Step (.warrant κ c ev) (.epiVal κ c ev) + | epiValClaim : Step c c' → Step (.epiVal κ c ev) (.epiVal κ c' ev) + | epiValEv : IsValue c → Step ev ev' → Step (.epiVal κ c ev) (.epiVal κ c ev') + | evidenceStep : Step e e' → Step (.evidence e) (.evidence e') + | evidenceVal : IsValue c → IsValue ev → Step (.evidence (.epiVal κ c ev)) ev -- Echo (structured loss): `echoClose` is a redex that reduces into a formed -- echo value `echoVal residue result`; `lower`/`residue` are the two generic -- projections off a formed echo value. `lower` yields the result component @@ -545,6 +605,9 @@ theorem value_no_step {e e' : Expr} (hv : IsValue e) (hs : Step e e') : False := | pair _ _ iha ihb => cases hs with | pairLeft h => exact iha h | pairRight _ h => exact ihb h + | epiVal _ _ ihc ihe => cases hs with + | epiValClaim h => exact ihc h + | epiValEv _ h => exact ihe h | _ => cases hs /-- Canonical forms for Num. -/ @@ -567,6 +630,7 @@ theorem canonical_word : IsValue e → HasType [] e (.word n) → | braidLit gs => right; cases ht with | tBraid => exact ⟨gs, rfl, rfl⟩ | echoVal _ _ => cases ht | pair _ _ => cases ht + | epiVal _ _ => cases ht /-- Canonical forms for Echo[ρ, τ]: a value of echo type is a formed echo value `echoVal r v` whose residue `r` and result `v` are themselves values. This @@ -582,6 +646,25 @@ theorem canonical_echo : IsValue e → HasType [] e (.echo ρ τ) → | braidLit => cases ht | echoVal hr hv => exact ⟨_, _, rfl, hr, hv⟩ | pair _ _ => cases ht + | epiVal _ _ => cases ht + +/-- Canonical forms for Epi[κ, ρ, τ]: a value of epistemic type is a formed + warrant `epiVal κ c ev` whose claim and token are themselves values. This is + the canonical form that lets `evidence` make progress. Note it yields the + TOKEN's value-hood, not the claim's truth — the claim rides along in the + value but no rule projects it out. -/ +theorem canonical_epi : IsValue e → HasType [] e (.epi κ ρ τ) → + ∃ c ev, e = .epiVal κ c ev ∧ IsValue c ∧ IsValue ev := by + intro hv ht + cases hv with + | num => cases ht + | str => cases ht + | boolLit => cases ht + | identity => cases ht + | braidLit => cases ht + | echoVal _ _ => cases ht + | pair _ _ => cases ht + | epiVal hc he => cases ht; exact ⟨_, _, rfl, hc, he⟩ /-- Canonical forms for products: a value of product type is a `pair a b` whose components `a` and `b` are themselves values. This is the canonical form @@ -597,6 +680,7 @@ theorem canonical_prod : IsValue e → HasType [] e (.prod α β) → | braidLit => cases ht | echoVal _ _ => cases ht | pair ha hb => exact ⟨_, _, rfl, ha, hb⟩ + | epiVal _ _ => cases ht -- Width distribution lemmas private theorem foldl_max_init (gs : List Generator) (a : Nat) : @@ -717,6 +801,14 @@ theorem weakening {Γ₁ Γ₂ : Ctx} {e : Expr} {τ σ : Ty} : cases h; rename_i ρ τ' h₁ h₂; simp only [shift]; exact .tEchoVal _ _ _ ρ τ' (iha h₁) (ihb h₂) | pair a b iha ihb => cases h; rename_i α β h₁ h₂; simp only [shift]; exact .tPair _ _ _ α β (iha h₁) (ihb h₂) + | warrant κ cl ev ihc ihe => + cases h; rename_i ρ τ' h₁ h₂; simp only [shift] + exact .tWarrant _ _ _ _ _ _ (ihc h₁) (ihe h₂) + | epiVal κ cl ev ihc ihe => + cases h; rename_i ρ τ' h₁ h₂; simp only [shift] + exact .tEpiVal _ _ _ _ _ _ (ihc h₁) (ihe h₂) + | evidence a iha => + cases h; rename_i κ τ' h₁; simp only [shift]; exact .tEvidence _ _ _ _ _ (iha h₁) | fst a iha => cases h; rename_i β h₁; simp only [shift]; exact .tFst _ _ _ β (iha h₁) | snd a iha => @@ -795,6 +887,14 @@ theorem subst_preserves {Γ₁ Γ₂ : Ctx} {e s : Expr} {τ σ : Ty} : cases h; rename_i ρ τ' h₁ h₂; simp only [subst]; exact .tEchoVal _ _ _ ρ τ' (iha h₁ hs) (ihb h₂ hs) | pair a b iha ihb => cases h; rename_i α β h₁ h₂; simp only [subst]; exact .tPair _ _ _ α β (iha h₁ hs) (ihb h₂ hs) + | warrant κ cl ev ihc ihe => + cases h; rename_i ρ τ' h₁ h₂; simp only [subst] + exact .tWarrant _ _ _ _ _ _ (ihc h₁ hs) (ihe h₂ hs) + | epiVal κ cl ev ihc ihe => + cases h; rename_i ρ τ' h₁ h₂; simp only [subst] + exact .tEpiVal _ _ _ _ _ _ (ihc h₁ hs) (ihe h₂ hs) + | evidence a iha => + cases h; rename_i κ τ' h₁; simp only [subst]; exact .tEvidence _ _ _ _ _ (iha h₁ hs) | fst a iha => cases h; rename_i β h₁; simp only [subst]; exact .tFst _ _ _ β (iha h₁ hs) | snd a iha => @@ -949,6 +1049,30 @@ theorem progress : HasType [] e τ → IsValue e ∨ ∃ e', Step e e' := by · exact .inl (.pair hva hvb) · exact .inr ⟨_, .pairRight hva hsb⟩ · exact .inr ⟨_, .pairLeft hsa⟩ + | warrant κ cl ev ihc ihe => + -- Always a redex: it forms once both components are values. + cases ht; rename_i hc he + right + rcases ihc hc with hvc | ⟨c', hsc⟩ + · rcases ihe he with hve | ⟨ev', hse⟩ + · exact ⟨_, .warrantForm hvc hve⟩ + · exact ⟨_, .warrantEv hvc hse⟩ + · exact ⟨_, .warrantClaim hsc⟩ + | epiVal κ cl ev ihc ihe => + -- A value iff both components are; otherwise the relevant one steps. + cases ht; rename_i hc he + rcases ihc hc with hvc | ⟨c', hsc⟩ + · rcases ihe he with hve | ⟨ev', hse⟩ + · exact .inl (.epiVal hvc hve) + · exact .inr ⟨_, .epiValEv hvc hse⟩ + · exact .inr ⟨_, .epiValClaim hsc⟩ + | evidence a iha => + cases ht; rename_i κ τ' h + right + rcases iha h with hv | ⟨e', hs⟩ + · obtain ⟨c, ev, rfl, hc, he⟩ := canonical_epi hv h + exact ⟨_, .evidenceVal hc he⟩ + · exact ⟨_, .evidenceStep hs⟩ | fst a iha => cases ht; rename_i h right @@ -1111,6 +1235,24 @@ theorem preservation : HasType [] e τ → Step e e' → HasType [] e' τ := by | echoCloseId => cases ht with | tEchoClose _ _ n h => cases h with | tIdentity => exact .tEchoVal _ _ _ _ _ (.tIdentity _) (.tIdentity _) + -- Epistemic. Note `evidenceVal`: it inverts tEvidence then tEpiVal and + -- returns the TOKEN's typing (he), never the claim's (hc). That asymmetry is + -- exactly non-factivity, discharged here by the type system. + | warrantClaim hs ih => + cases ht with | tWarrant _ _ _ _ _ _ hc he => exact .tWarrant _ _ _ _ _ _ (ih hc) he + | warrantEv _ hs ih => + cases ht with | tWarrant _ _ _ _ _ _ hc he => exact .tWarrant _ _ _ _ _ _ hc (ih he) + | warrantForm _ _ => + cases ht with | tWarrant _ _ _ _ _ _ hc he => exact .tEpiVal _ _ _ _ _ _ hc he + | epiValClaim hs ih => + cases ht with | tEpiVal _ _ _ _ _ _ hc he => exact .tEpiVal _ _ _ _ _ _ (ih hc) he + | epiValEv _ hs ih => + cases ht with | tEpiVal _ _ _ _ _ _ hc he => exact .tEpiVal _ _ _ _ _ _ hc (ih he) + | evidenceStep hs ih => + cases ht with | tEvidence _ _ _ _ _ h => exact .tEvidence _ _ _ _ _ (ih h) + | evidenceVal _ _ => + cases ht with | tEvidence _ _ _ _ _ h => + cases h with | tEpiVal _ _ _ _ _ _ hc he => exact he | echoValLeft hs ih => cases ht with | tEchoVal _ _ _ _ _ hr hv => exact .tEchoVal _ _ _ _ _ (ih hr) hv | echoValRight _ hs ih => @@ -1336,6 +1478,33 @@ theorem determinism : Step e e₁ → Step e e₂ → e₁ = e₂ := by | echoCloseId => cases hs₂ with | echoCloseStep h => exact absurd h (value_no_step .identity) | echoCloseId => rfl + -- Epistemic: three-way races. `warrantForm` fires only when BOTH components + -- are values, so it never races its own congruence rules; `evidenceVal` + -- likewise fires only on a formed `epiVal`. + | warrantClaim hs ih => cases hs₂ with + | warrantClaim h => exact congrArg (Expr.warrant _ · _) (ih h) + | warrantEv hc _ => exact absurd hs (value_no_step hc) + | warrantForm hc _ => exact absurd hs (value_no_step hc) + | warrantEv hc hs ih => cases hs₂ with + | warrantClaim h => exact absurd h (value_no_step hc) + | warrantEv _ h => exact congrArg (Expr.warrant _ _ ·) (ih h) + | warrantForm _ he => exact absurd hs (value_no_step he) + | warrantForm hc he => cases hs₂ with + | warrantClaim h => exact absurd h (value_no_step hc) + | warrantEv _ h => exact absurd h (value_no_step he) + | warrantForm _ _ => rfl + | epiValClaim hs ih => cases hs₂ with + | epiValClaim h => exact congrArg (Expr.epiVal _ · _) (ih h) + | epiValEv hc _ => exact absurd hs (value_no_step hc) + | epiValEv hc hs ih => cases hs₂ with + | epiValClaim h => exact absurd h (value_no_step hc) + | epiValEv _ h => exact congrArg (Expr.epiVal _ _ ·) (ih h) + | evidenceStep hs ih => cases hs₂ with + | evidenceStep h => exact congrArg Expr.evidence (ih h) + | evidenceVal hc he => exact absurd hs (value_no_step (.epiVal hc he)) + | evidenceVal hc he => cases hs₂ with + | evidenceStep h => exact absurd h (value_no_step (.epiVal hc he)) + | evidenceVal _ _ => rfl | echoValLeft hs ih => cases hs₂ with | echoValLeft h => exact congrArg (Expr.echoVal · _) (ih h) | echoValRight hr _ => exact absurd hs (value_no_step hr) @@ -1512,6 +1681,71 @@ theorem echo_roundtrip_typed (e : Expr) (n : Nat) (h : HasType [] e (.word n)) : HasType [] (.lower (.echoClose e)) (.word 0) := ⟨.tResidue _ _ _ _ (.tEchoClose _ _ n h), .tLower _ _ _ _ (.tEchoClose _ _ n h)⟩ +-- ═══════════════════════════════════════════════════════════════════════ +-- EPISTEMIC CAPSTONES +-- ═══════════════════════════════════════════════════════════════════════ +-- +-- The echo capstones show that a *lossy* operation can be made recoverable by +-- carrying its residue. The epistemic capstones show the dual discipline: a +-- warrant carries evidence WITHOUT thereby discharging what it claims. Where +-- echo says "the witness is retained", epi says "the claim is not delivered". + +/-- `evidence ∘ warrant` recovers the token. The warrant forms, then the sole + projection yields the evidence that was deposited. -/ +theorem epi_evidence_recovers (κ : Nat) (c ev : Expr) (hc : IsValue c) (he : IsValue ev) : + StepStar (.evidence (.warrant κ c ev)) ev := + .head (.evidenceStep (.warrantForm hc he)) (.head (.evidenceVal hc he) .refl) + +/-- **The claim is opaque.** Two warrants at the same standpoint carrying the + same evidence but asserting DIFFERENT claims are observationally identical: + every observation yields the token, never the claim. This is the epistemic + dual of `echo_distinguishes_collapsed` — echo *reveals* what `close` + forgot; a warrant *withholds* what it purports. Holding evidence is not + holding the fact. -/ +theorem epi_claim_is_opaque (κ : Nat) (c₁ c₂ ev : Expr) + (h₁ : IsValue c₁) (h₂ : IsValue c₂) (he : IsValue ev) : + StepStar (.evidence (.warrant κ c₁ ev)) ev ∧ + StepStar (.evidence (.warrant κ c₂ ev)) ev := + ⟨epi_evidence_recovers κ c₁ ev h₁ he, epi_evidence_recovers κ c₂ ev h₂ he⟩ + +/-- **Non-factivity, at the type level.** From `e : Epi[κ, ρ, τ]` the only + elimination yields ρ. Contrast `tLower`, which *does* deliver an echo's + result τ. A warrant is not knowledge: there is no rule taking you from a + warrant to the thing warranted. Upstream models the factive case as a + SEPARATE record (`FactiveModality`, with `reflect : E κ A → A`) rather than + as a modality with a missing proof; the absence here is the same choice. -/ +theorem epi_only_yields_evidence (Γ : Ctx) (e : Expr) (κ : Nat) (ρ τ : Ty) + (h : HasType Γ e (.epi κ ρ τ)) : + HasType Γ (.evidence e) ρ := + .tEvidence _ _ κ ρ τ h + +/-- Standpoints are distinguished: the same evidence for the same claim held at + different standpoints inhabits different types. Warrant is indexed by who + holds it, so κ₁ ≠ κ₂ gives genuinely different epistemic positions. -/ +theorem epi_distinguishes_standpoints {κ₁ κ₂ : Nat} (ρ τ : Ty) (h : κ₁ ≠ κ₂) : + Ty.epi κ₁ ρ τ ≠ Ty.epi κ₂ ρ τ := by + intro heq; exact h (Ty.epi.inj heq).1 + +/-- The epistemic round-trip is type-safe: from a claim at τ and evidence at ρ, + the warrant is `Epi[κ,ρ,τ]` and `evidence` recovers exactly ρ. -/ +theorem epi_roundtrip_typed (κ : Nat) (c ev : Expr) (ρ τ : Ty) + (hc : HasType [] c τ) (he : HasType [] ev ρ) : + HasType [] (.warrant κ c ev) (.epi κ ρ τ) ∧ + HasType [] (.evidence (.warrant κ c ev)) ρ := + ⟨.tWarrant _ κ _ _ ρ τ hc he, .tEvidence _ _ κ ρ τ (.tWarrant _ κ _ _ ρ τ hc he)⟩ + +/-- Epistemic and echo COMPOSE without collapsing into each other: + `Epi[κ, Echo[ρ,τ], σ]` is a warrant, at standpoint κ, whose evidence is an + echo. Mirrors `EpistemicEcho` in EpistemicTypes/EchoBridge.agda — "standpoint + κ has epistemic access to an echo of A". The bridge module is explicit that + these are different modalities: echo grades irrecoverability, epi indexes + standpoints. -/ +theorem epi_over_echo_typed (κ : Nat) (c e : Expr) (n : Nat) (σ : Ty) + (hc : HasType [] c σ) (he : HasType [] e (.word n)) : + HasType [] (.warrant κ c (.echoClose e)) + (.epi κ (.echo (.word n) (.word 0)) σ) := + .tWarrant _ κ _ _ _ σ hc (.tEchoClose _ _ n he) + /-- `echoAdd` recovers the summands: `add` discards which numbers were added, but the residue retains the pair. -/ theorem echoAdd_residue_recovers (n₁ n₂ : Int) : @@ -1592,6 +1826,20 @@ def infer (Γ : Ctx) : Expr → Option Ty | some .num, some .num => some .bool | some .str, some .str => some .bool | _, _ => none + -- Epistemic. `evidence` returns the EVIDENCE component ρ; there is no case + -- returning τ, which is where non-factivity lives in the algorithm. + | .warrant κ cl ev => + match infer Γ cl, infer Γ ev with + | some τ, some ρ => some (.epi κ ρ τ) + | _, _ => none + | .epiVal κ cl ev => + match infer Γ cl, infer Γ ev with + | some τ, some ρ => some (.epi κ ρ τ) + | _, _ => none + | .evidence e => + match infer Γ e with + | some (.epi _ ρ _) => some ρ + | _ => none | .echoClose e => match infer Γ e with | some (.word n) => some (.echo (.word n) (.word 0)) @@ -1685,6 +1933,18 @@ theorem infer_sound {Γ : Ctx} {e : Expr} {τ : Ty} : next he₁ he₂ => injection h with h; subst h; exact .tEqNum _ _ _ (ih₁ he₁) (ih₂ he₂) next he₁ he₂ => injection h with h; subst h; exact .tEqStr _ _ _ (ih₁ he₁) (ih₂ he₂) all_goals simp at h + | warrant κ cl ev ihc ihe => + intro h; simp only [infer] at h; split at h + next τ' ρ hc he => injection h with h; subst h; exact .tWarrant _ κ _ _ ρ τ' (ihc hc) (ihe he) + all_goals simp at h + | epiVal κ cl ev ihc ihe => + intro h; simp only [infer] at h; split at h + next τ' ρ hc he => injection h with h; subst h; exact .tEpiVal _ κ _ _ ρ τ' (ihc hc) (ihe he) + all_goals simp at h + | evidence e ih => + intro h; simp only [infer] at h; split at h + next κ ρ τ' he => injection h with h; subst h; exact .tEvidence _ _ κ _ τ' (ih he) + all_goals simp at h | echoClose e ih => intro h; simp only [infer] at h; split at h next k he => injection h with h; subst h; exact .tEchoClose _ _ k (ih he)