From f9b95020e845e7155ed6ca0534ced281d09a21d2 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 29 Jul 2026 08:18:24 +0100 Subject: [PATCH 1/2] feat(typecheck): QTT quantity semiring; make strands linear in weave MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `weave` performed no usage checking at all. It built the strand context, checked the body, computed `Tangle[A,B]` — and discarded it, returning gamma unchanged. Three unsound programs were accepted in silence: weave strands a, b into (a > a) yield strands a, b # contraction weave strands a, b into (a > b) yield strands a, b, a # contraction weave strands a, b into (a > b) yield strands a # weakening The spec already forbade the first (`i != j` on [T-Cross-Over]) and the third ("yield declarations match B"). Both side conditions were written down and never enforced. ## Why a semiring and not "make the language linear" The requirement is genuinely mixed, so a single discipline is the wrong answer in both directions: * braid WORDS are unrestricted (omega) — `x . x` is sigma_1^2, a legitimate braid. Blanket linearity would reject valid programs. * STRANDS are linear (1) — a strand is a physical thread. A braid on n strands is a permutation of those n strands, so strand count is a conservation law. AFFINE is specifically wrong here: affine permits discarding, and a strand cannot vanish. That case is what decides it. * the CLAIM in `Epi[k, rho, tau]` is erased (0) — A-TG-11.1's recorded gap. `compiler/lib/quantity.ml` provides {0, 1, omega} with add/mul/permits. Independent uses combine with semiring addition, so two uses of one strand give 1 + 1 = omega, which is not permitted where 1 was declared. ## Applied in BOTH weave forms Wiring the check into the weave STATEMENT rule alone left `def x = weave ...` — the idiomatic spelling — entirely unchecked, because it reaches the weave EXPRESSION rule and never touches the statement rule. The new conformance tier caught this on its first run. ## Gating New `conformance/ill-typed/` tier with a DOUBLE assertion: the file must PARSE and then FAIL to typecheck. Asserting only "the compiler rejects it" is the failure this suite already had once, when three invalid/ cases scored points because the command was wrong and failed on every input. Requiring the parse first proves the rejection came from the typechecker, not from a typo in the fixture. Wired into `scripts/check-corpus.sh` (what CI runs) as well as `run_conformance.sh`, and verified with a negative control: making one ill-typed fixture well-typed turns the gate red, restoring it turns it green. `valid/` is now also required to TYPECHECK, not merely parse. All 16 already do. ## Verification * semiring laws checked EXHAUSTIVELY over all 27 triples — a "semiring" whose operations don't satisfy the laws is two arbitrary tables, and every soundness claim resting on it is worth nothing * 677 compiler tests pass (`dune runtest --force`) * conformance 23/23; 8/8 examples evaluate; stdlib typechecks * corpus + RSR gates green Spec: new section 3.10.1 with the [T-Weave-Linear] rule and the quantity table. Co-Authored-By: Claude Opus 5 --- compiler/lib/quantity.ml | 102 ++++++++++ compiler/lib/typecheck.ml | 80 ++++++++ compiler/test/dune | 4 +- compiler/test/test_quantity.ml | 189 ++++++++++++++++++ .../t01_strand_duplicated_in_body.tangle | 11 + .../t02_strand_duplicated_in_yield.tangle | 11 + .../ill-typed/t03_strand_vanishes.tangle | 10 + .../t04_undeclared_strand_yielded.tangle | 7 + conformance/run_conformance.sh | 51 ++++- docs/spec/FORMAL-SEMANTICS.md | 59 ++++++ scripts/check-corpus.sh | 31 ++- 11 files changed, 544 insertions(+), 11 deletions(-) create mode 100644 compiler/lib/quantity.ml create mode 100644 compiler/test/test_quantity.ml create mode 100644 conformance/ill-typed/t01_strand_duplicated_in_body.tangle create mode 100644 conformance/ill-typed/t02_strand_duplicated_in_yield.tangle create mode 100644 conformance/ill-typed/t03_strand_vanishes.tangle create mode 100644 conformance/ill-typed/t04_undeclared_strand_yielded.tangle diff --git a/compiler/lib/quantity.ml b/compiler/lib/quantity.ml new file mode 100644 index 0000000..a186e5e --- /dev/null +++ b/compiler/lib/quantity.ml @@ -0,0 +1,102 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* quantity.ml — the QTT quantity semiring {0, 1, omega}. + * + * Quantitative Type Theory (Atkey 2018) annotates each binding with a quantity + * drawn from a semiring. With {0, 1, omega} that single mechanism subsumes + * three disciplines rather than forcing a choice between them: + * + * 0 erased present for typing, absent at runtime + * 1 linear used exactly once + * omega unrestricted used freely + * + * ── Why TANGLE needs the semiring and not one discipline ──────────────────── + * The requirement is genuinely mixed, which is why "make the language linear" + * or "make it affine" are both wrong answers: + * + * * BRAID WORDS are unrestricted (omega). `x . x` is sigma_1^2 — composing + * a braid with itself is a legitimate braid, not resource duplication. + * Linearity would forbid a valid program. + * + * * STRANDS inside a `weave` are LINEAR (1). A strand is a physical thread: + * it is used exactly once, and it must come out the other side. Braids are + * permutations of n strands and strand count is a conservation law, so + * AFFINE is specifically wrong here — affine permits discarding, and a + * strand cannot vanish. + * + * * The CLAIM in `Epi[k, rho, tau]` (TG-11) is erased (0): it fixes the type + * and is never observable. Assumption A-TG-11.1 records that the current + * encoding carries it instead, because erasing it without quantities would + * break uniqueness of typing. This module is the missing half. + * + * ── Scope ─────────────────────────────────────────────────────────────────── + * This provides the semiring and applies it to STRAND usage, which is where + * the discipline actually bites and where a real soundness gap exists. It is + * NOT a QTT conversion of the whole core: TANGLE's judgement is still + * `Gamma |- e : tau` without quantities on ordinary bindings. Doing that means + * changing the judgement shape and re-proving the metatheory, and is tracked + * separately. + *) + +(** A quantity from the {0, 1, omega} semiring. *) +type t = + | Zero (** erased: present for typing, absent at runtime *) + | One (** linear: used exactly once *) + | Omega (** unrestricted *) + +let to_string = function + | Zero -> "0" | One -> "1" | Omega -> "omega" + +(** Semiring addition. Combines the quantities of two INDEPENDENT uses — + e.g. the two operands of a crossing. Using something once in each of two + places is using it twice, which is unrestricted usage, so 1 + 1 = omega + rather than an error: the error is raised later by [check_linear], when the + binding's declared quantity is compared against its total use. *) +let add a b = + match a, b with + | Zero, x | x, Zero -> x + | One, One -> Omega + | Omega, _ | _, Omega -> Omega + +(** Semiring multiplication. Scales a usage by the context it sits in — a + binding used once inside something used twice is used twice. Zero + annihilates: nothing inside an erased position is used at all. *) +let mul a b = + match a, b with + | Zero, _ | _, Zero -> Zero + | One, x | x, One -> x + | Omega, Omega -> Omega + +(** Additive identity. *) +let zero = Zero + +(** Multiplicative identity. *) +let one = One + +(** Is [actual] usage permitted where [declared] was promised? + + * [Zero] demands NO use at runtime. + * [One] demands EXACTLY one — neither zero (the resource vanishes) nor + more (it is duplicated). This is what makes it linear rather + than affine: [Zero] actual is a violation. + * [Omega] permits anything. *) +let permits ~declared ~actual = + match declared, actual with + | Zero, Zero -> true + | Zero, _ -> false + | One, One -> true + | One, _ -> false + | Omega, _ -> true + +(** Why a usage was rejected, in words a programmer can act on. *) +let explain ~declared ~actual = + match declared, actual with + | One, Zero -> + "declared linear (used exactly once) but never used — a strand cannot \ + vanish; braids conserve strand count" + | One, Omega -> + "declared linear (used exactly once) but used more than once — a strand \ + cannot be duplicated" + | Zero, _ -> + "declared erased (quantity 0) but used at runtime" + | _ -> + Printf.sprintf "declared %s but used %s" (to_string declared) (to_string actual) diff --git a/compiler/lib/typecheck.ml b/compiler/lib/typecheck.ml index 846b053..c976ff0 100644 --- a/compiler/lib/typecheck.ml +++ b/compiler/lib/typecheck.ml @@ -164,6 +164,77 @@ let apply_perm (b : boundary) (gens : generator list) : boundary = (* Type inference for expressions *) (* ================================================================== *) +(* ================================================================== *) +(* Strand linearity (QTT quantities applied to weave) *) +(* ================================================================== *) + +(** Count how many times each STRAND is used in a weave body, in the {0,1,omega} + semiring. Independent uses combine with semiring ADDITION, so two uses of + the same strand give 1 + 1 = omega — which then fails the linear check. + + Strands appear in two places: as the operands of a crossing (`a > b`), and + under a twist (`(~a)`, [T-Twist-Strand]). *) +let rec strand_uses (sigma : strand_ctx) (e : expr) : (string * Quantity.t) list = + let merge xs ys = + List.fold_left (fun acc (n, q) -> + match List.assoc_opt n acc with + | Some q' -> (n, Quantity.add q q') :: List.remove_assoc n acc + | None -> (n, q) :: acc) xs ys + in + let go = strand_uses sigma in + let use n = if strand_lookup sigma n <> None then [(n, Quantity.one)] else [] in + match e with + | Crossing (a, _, b) -> merge (use a) (use b) + | Twist (Var a) -> use a + | Var a -> use a + | BinOp (_, x, y) | Pipeline (x, y) | Cap (x, y) | Cup (x, y) + | Pair (x, y) | EchoAdd (x, y) | EchoEq (x, y) -> merge (go x) (go y) + | UnaryOp (_, x) | Close x | Mirror x | Reverse x | Simplify x | Twist x + | EchoClose x | Lower x | Residue x | Fst x | Snd x | Evidence x -> go x + | Warrant (_, c, ev) | EpiVal (_, c, ev) -> merge (go c) (go ev) + | Let (_, a, b) -> merge (go a) (go b) + | Match (sc, arms) -> + List.fold_left (fun acc a -> merge acc (go a.arm_body)) (go sc) arms + | Call (_, args) -> List.fold_left (fun acc a -> merge acc (go a)) [] args + | Weave wb -> go wb.weave_body + | AddBlock _ | BraidLit _ | Identity | BoolLit _ | IntLit _ | FloatLit _ + | StringLit _ -> [] + +(** Enforce that every declared input strand is used EXACTLY ONCE, and that the + yielded strands are a permutation of the inputs. + + Both halves are conservation laws of braids, not stylistic rules. A braid + on n strands is a permutation of those n strands: none may be duplicated + (contraction) and none may vanish (weakening). That is why the discipline + is LINEAR and not affine — affine would permit the second. *) +let check_strand_linearity (sigma : strand_ctx) (wb : weave_block) : unit = + let uses = strand_uses sigma wb.weave_body in + (* 1. Each input is linear: exactly one use. *) + List.iter (fun (name, _) -> + let actual = match List.assoc_opt name uses with + | Some q -> q | None -> Quantity.zero in + if not (Quantity.permits ~declared:Quantity.one ~actual) then + type_error "strand '%s': %s" name + (Quantity.explain ~declared:Quantity.one ~actual) + ) sigma; + (* 2. The yield must be a permutation of the inputs: same multiset of names, + each exactly once. This is where `yield strands a, b, a` is caught. *) + let ins = List.map fst sigma in + let outs = List.map (fun ts -> ts.strand_name) wb.weave_outputs in + List.iter (fun n -> + let k = List.length (List.filter (( = ) n) outs) in + if k = 0 then + type_error "strand '%s' is declared but never yielded — a strand cannot \ + vanish; braids conserve strand count" n + else if k > 1 then + type_error "strand '%s' is yielded %d times — a strand cannot be \ + duplicated" n k + ) ins; + List.iter (fun n -> + if not (List.mem n ins) then + type_error "strand '%s' is yielded but was never declared as an input" n + ) outs + (* ================================================================== *) (* Harvard data types and the |-_hd judgement (spec sections 7.1, 9.3) *) (* ================================================================== *) @@ -300,6 +371,11 @@ let rec infer_expr (gamma : env) (sigma : strand_ctx) (e : expr) : ty = (ts.strand_name, { strand_pos = i + 1; strand_ty = sty }) ) wb.weave_inputs in let input_boundary = List.map (fun (_, se) -> se.strand_ty) sigma' in + (* Strands are LINEAR — see [check_strand_linearity]. This must be applied + in BOTH weave forms: `def x = weave ...` reaches the expression rule and + never touches the statement rule, so checking only there would leave the + ordinary, idiomatic spelling of a weave completely unchecked. *) + check_strand_linearity sigma' wb; (* The body is checked in the strand context, exactly as the statement form does — strand names are only meaningful there. *) let body_ty = infer_expr gamma sigma' wb.weave_body in @@ -998,6 +1074,10 @@ let check_statement (gamma : env) (stmt : statement) : env = ) wb.weave_inputs in (* Build input boundary A *) let input_boundary = List.map (fun (_, se) -> se.strand_ty) sigma in + (* Strands are LINEAR (QTT quantity 1): used exactly once, and conserved + into the yield. Checked before the body's type, so the diagnostic names + the strand rather than some downstream type mismatch. *) + check_strand_linearity sigma wb; (* Type-check the body in the strand context *) let body_ty = infer_expr gamma sigma wb.weave_body in (* Validate the body produces a Tangle type *) diff --git a/compiler/test/dune b/compiler/test/dune index e2bf91a..3692c65 100644 --- a/compiler/test/dune +++ b/compiler/test/dune @@ -1,5 +1,5 @@ ; SPDX-License-Identifier: MPL-2.0 (tests - (names test_parser test_typecheck test_eval test_e2e test_property test_compositional test_roundtrip test_check test_jeg) - (libraries tangle)) + (names test_parser test_typecheck test_eval test_e2e test_property test_compositional test_roundtrip test_check test_jeg test_quantity) + (libraries tangle str)) diff --git a/compiler/test/test_quantity.ml b/compiler/test/test_quantity.ml new file mode 100644 index 0000000..32802fb --- /dev/null +++ b/compiler/test/test_quantity.ml @@ -0,0 +1,189 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* test_quantity.ml — the {0, 1, omega} quantity semiring, and the strand + * linearity rule built on it. + * + * Two halves, and the first is not decoration. A "semiring" whose operations + * do not actually satisfy the semiring laws is just two arbitrary tables, and + * every soundness claim resting on it is worth nothing. The carrier is three + * elements, so the laws are decidable by exhaustion: we check all 27 triples + * rather than asserting the laws in a comment. + * + * The second half checks the rule that consumes the semiring — that a strand + * is used exactly once, and that the yield is a permutation of the inputs. + *) + +open Tangle.Ast +open Tangle.Typecheck + +let passed = ref 0 +let failed = ref 0 + +let test name f = + (try + if f () then begin incr passed; Printf.printf " PASS %s\n" name end + else begin incr failed; Printf.printf " FAIL %s\n" name end + with e -> + incr failed; + Printf.printf " FAIL %s (%s)\n" name (Printexc.to_string e)) + +(* The whole carrier. Three elements, so "for all" is a fold, not a sample. *) +let all = Tangle.Quantity.[ Zero; One; Omega ] + +let for_all1 p = List.for_all p all +let for_all2 p = List.for_all (fun a -> List.for_all (p a) all) all +let for_all3 p = + List.for_all (fun a -> + List.for_all (fun b -> List.for_all (p a b) all) all) all + +(* ------------------------------------------------------------------ *) +(* Semiring laws — exhaustively, over every triple *) +(* ------------------------------------------------------------------ *) + +let () = print_endline "\n=== Semiring laws (exhaustive over all 3^3 triples) ===" + +let () = + let open Tangle.Quantity in + + test "(+) is associative" (fun () -> + for_all3 (fun a b c -> add (add a b) c = add a (add b c))); + + test "(+) is commutative" (fun () -> + for_all2 (fun a b -> add a b = add b a)); + + test "0 is the additive identity" (fun () -> + for_all1 (fun a -> add zero a = a && add a zero = a)); + + test "( * ) is associative" (fun () -> + for_all3 (fun a b c -> mul (mul a b) c = mul a (mul b c))); + + test "1 is the multiplicative identity" (fun () -> + for_all1 (fun a -> mul one a = a && mul a one = a)); + + test "0 annihilates under ( * )" (fun () -> + for_all1 (fun a -> mul zero a = zero && mul a zero = zero)); + + test "( * ) distributes over (+) on the left" (fun () -> + for_all3 (fun a b c -> mul a (add b c) = add (mul a b) (mul a c))); + + test "( * ) distributes over (+) on the right" (fun () -> + for_all3 (fun a b c -> mul (add a b) c = add (mul a c) (mul b c))) + +(* ------------------------------------------------------------------ *) +(* The intended readings of the two operations *) +(* ------------------------------------------------------------------ *) + +let () = print_endline "\n=== Intended readings ===" + +let () = + let open Tangle.Quantity in + + (* This single equation is the whole reason `a > a` is rejected: two + independent uses of a linear resource add to omega, and omega is not + permitted where 1 was declared. *) + test "1 + 1 = omega (two independent uses is unrestricted use)" (fun () -> + add one one = Omega); + + test "omega is absorbing under (+)" (fun () -> + for_all1 (fun a -> add Omega a = Omega)); + + (* permits is the linear, not the affine, check. The distinguishing case is + the FIRST one: an affine discipline would accept it. *) + test "declared 1, used 0 is REJECTED (linear, not affine)" (fun () -> + not (permits ~declared:one ~actual:zero)); + + test "declared 1, used 1 is accepted" (fun () -> + permits ~declared:one ~actual:one); + + test "declared 1, used omega is rejected" (fun () -> + not (permits ~declared:one ~actual:Omega)); + + test "declared omega permits every usage" (fun () -> + for_all1 (fun a -> permits ~declared:Omega ~actual:a)); + + test "declared 0 permits only 0" (fun () -> + for_all1 (fun a -> permits ~declared:zero ~actual:a = (a = Zero))); + + test "explain names the vanishing case" (fun () -> + let s = explain ~declared:one ~actual:zero in + (* substring search, so the wording can be improved without breaking this *) + let re = Str.regexp_string "never used" in + (try ignore (Str.search_forward re s 0); true with Not_found -> false)) + +(* ------------------------------------------------------------------ *) +(* Strand linearity, through the typechecker *) +(* ------------------------------------------------------------------ *) + +let () = print_endline "\n=== Strand linearity (weave) ===" + +let strand n = { strand_name = n; strand_type = Some "Q" } + +let weave ins body outs = + Weave { weave_inputs = List.map strand ins; + weave_body = body; + weave_outputs = List.map strand outs } + +let cross a b = Crossing (a, Over, b) + +let accepts e = + try ignore (infer_expr [] [] e); true with _ -> false + +let rejects e = not (accepts e) + +let () = + test "permutation weave is accepted" (fun () -> + accepts (weave ["a"; "b"] (cross "a" "b") ["b"; "a"])); + + test "identity-order yield is accepted" (fun () -> + accepts (weave ["a"; "b"] (cross "a" "b") ["a"; "b"])); + + test "single strand under a twist is accepted" (fun () -> + accepts (weave ["a"] (Twist (Var "a")) ["a"])); + + (* The three soundness gaps this work closes. *) + test "REJECTED: strand crossed with itself (a > a)" (fun () -> + rejects (weave ["a"; "b"] (cross "a" "a") ["a"; "b"])); + + test "REJECTED: strand yielded twice (contraction)" (fun () -> + rejects (weave ["a"; "b"] (cross "a" "b") ["a"; "b"; "a"])); + + test "REJECTED: strand dropped from the yield (weakening)" (fun () -> + rejects (weave ["a"; "b"] (cross "a" "b") ["a"])); + + test "REJECTED: yielding a strand that was never an input" (fun () -> + rejects (weave ["a"; "b"] (cross "a" "b") ["a"; "c"])); + + (* An input that the body never mentions is a violation too: it is declared + linear and used zero times. Distinct from the yield check — this one + fires even when the yield is a perfect permutation. *) + test "REJECTED: input strand never used in the body" (fun () -> + rejects (weave ["a"; "b"; "c"] (cross "a" "b") ["a"; "b"; "c"])) + +(* ------------------------------------------------------------------ *) +(* Braid WORDS are unrestricted — linearity must not leak into them *) +(* ------------------------------------------------------------------ *) + +let () = print_endline "\n=== Words stay unrestricted (omega) ===" + +let () = + (* `x . x` is sigma_1^2 — a legitimate braid. If the linear discipline + leaked out of `weave` and onto ordinary bindings, this would break, and + the language would reject valid programs. That is exactly why the answer + is a SEMIRING and not "make the language linear". *) + let gamma = [ ("x", EVal (TWord 2)) ] in + test "x . x typechecks (a word composed with itself)" (fun () -> + try ignore (infer_expr gamma [] (BinOp (Compose, Var "x", Var "x"))); true + with _ -> false); + + test "x . x . x typechecks (three uses)" (fun () -> + try + ignore (infer_expr gamma [] + (BinOp (Compose, Var "x", BinOp (Compose, Var "x", Var "x")))); + true + with _ -> false) + +(* ------------------------------------------------------------------ *) + +let () = + Printf.printf "\n=====================================\n"; + Printf.printf "Results: %d/%d passed\n" !passed (!passed + !failed); + if !failed > 0 then exit 1 diff --git a/conformance/ill-typed/t01_strand_duplicated_in_body.tangle b/conformance/ill-typed/t01_strand_duplicated_in_body.tangle new file mode 100644 index 0000000..dcf8ca9 --- /dev/null +++ b/conformance/ill-typed/t01_strand_duplicated_in_body.tangle @@ -0,0 +1,11 @@ +# SPDX-License-Identifier: MPL-2.0 +# Conformance (ILL-TYPED): a strand crossed with itself. +# +# `a > a` uses the strand 'a' twice. Strands carry QTT quantity 1 (linear): +# a strand is a physical thread, not a value, and it cannot be duplicated. +# This PARSES — it is rejected by the typechecker, not the grammar. + +def self_cross = + weave strands a:Q, b:Q into + (a > a) + yield strands a:Q, b:Q diff --git a/conformance/ill-typed/t02_strand_duplicated_in_yield.tangle b/conformance/ill-typed/t02_strand_duplicated_in_yield.tangle new file mode 100644 index 0000000..37cfefb --- /dev/null +++ b/conformance/ill-typed/t02_strand_duplicated_in_yield.tangle @@ -0,0 +1,11 @@ +# SPDX-License-Identifier: MPL-2.0 +# Conformance (ILL-TYPED): contraction — the yield names a strand twice. +# +# A braid on n strands is a PERMUTATION of those n strands, so the output +# boundary must be a permutation of the input boundary. Yielding 'a' twice +# manufactures a strand out of nothing. + +def duplicating = + weave strands a:Q, b:Q into + (a > b) + yield strands a:Q, b:Q, a:Q diff --git a/conformance/ill-typed/t03_strand_vanishes.tangle b/conformance/ill-typed/t03_strand_vanishes.tangle new file mode 100644 index 0000000..f63d594 --- /dev/null +++ b/conformance/ill-typed/t03_strand_vanishes.tangle @@ -0,0 +1,10 @@ +# SPDX-License-Identifier: MPL-2.0 +# Conformance (ILL-TYPED): weakening — a strand is dropped from the yield. +# +# This is the case that makes the discipline LINEAR rather than AFFINE. +# Affine would permit discarding; braids conserve strand count, so it cannot. + +def vanishing = + weave strands a:Q, b:Q into + (a > b) + yield strands a:Q diff --git a/conformance/ill-typed/t04_undeclared_strand_yielded.tangle b/conformance/ill-typed/t04_undeclared_strand_yielded.tangle new file mode 100644 index 0000000..4517f16 --- /dev/null +++ b/conformance/ill-typed/t04_undeclared_strand_yielded.tangle @@ -0,0 +1,7 @@ +# SPDX-License-Identifier: MPL-2.0 +# Conformance (ILL-TYPED): the yield names a strand that was never an input. + +def conjuring = + weave strands a:Q, b:Q into + (a > b) + yield strands a:Q, c:Q diff --git a/conformance/run_conformance.sh b/conformance/run_conformance.sh index c326014..7796cd3 100755 --- a/conformance/run_conformance.sh +++ b/conformance/run_conformance.sh @@ -2,8 +2,17 @@ # SPDX-License-Identifier: MPL-2.0 # Conformance test runner for Tangle # -# Invokes the Tangle compiler (OCaml/Menhir) on every file in valid/ -# and invalid/, asserting success for valid files and failure for invalid files. +# Three tiers, because "rejected" is not one property: +# +# valid/ MUST parse AND MUST typecheck +# invalid/ MUST FAIL TO PARSE (grammar-level rejection) +# ill-typed/ MUST PARSE but MUST FAIL to typecheck +# +# The third tier carries a DOUBLE assertion on purpose. Asserting only "the +# compiler rejects it" is the failure this suite already suffered once: an +# invalid case scores a point whenever the command fails, including when it +# fails for an unrelated reason. Requiring the file to parse FIRST proves the +# rejection came from the typechecker and not from a typo in the test. # # Usage: ./run_conformance.sh [path-to-tangle-binary] @@ -34,22 +43,30 @@ else fi fi -echo "parser: ${PARSER_CMD[*]}" +# The typechecker is the same binary with --check. Built as a separate array +# so a caller-supplied PARSER_CMD still gets the flag appended correctly. +CHECK_CMD=("${PARSER_CMD[@]}" --check) + +echo "parser: ${PARSER_CMD[*]}" +echo "typechecker: ${CHECK_CMD[*]}" PASS=0 FAIL=0 TOTAL=0 -# --- Valid programs: parser MUST succeed --- +# --- Valid programs: MUST parse AND MUST typecheck --- for f in "${SCRIPT_DIR}"/valid/*.tangle; do TOTAL=$((TOTAL + 1)) name="$(basename "$f")" - if "${PARSER_CMD[@]}" "$f" >/dev/null 2>&1; then + if ! "${PARSER_CMD[@]}" "$f" >/dev/null 2>&1; then + echo " FAIL valid/${name} (expected to parse, got a parse error)" + FAIL=$((FAIL + 1)) + elif ! "${CHECK_CMD[@]}" "$f" >/dev/null 2>&1; then + echo " FAIL valid/${name} (parses, but does not typecheck)" + FAIL=$((FAIL + 1)) + else echo " PASS valid/${name}" PASS=$((PASS + 1)) - else - echo " FAIL valid/${name} (expected success, got failure)" - FAIL=$((FAIL + 1)) fi done @@ -66,6 +83,24 @@ for f in "${SCRIPT_DIR}"/invalid/*.tangle; do fi done +# --- Ill-typed programs: MUST parse, MUST NOT typecheck --- +for f in "${SCRIPT_DIR}"/ill-typed/*.tangle; do + TOTAL=$((TOTAL + 1)) + name="$(basename "$f")" + if ! "${PARSER_CMD[@]}" "$f" >/dev/null 2>&1; then + # Not a pass. The file was supposed to reach the typechecker; if it + # cannot even parse, the test is broken and proves nothing. + echo " FAIL ill-typed/${name} (must PARSE first — got a parse error)" + FAIL=$((FAIL + 1)) + elif "${CHECK_CMD[@]}" "$f" >/dev/null 2>&1; then + echo " FAIL ill-typed/${name} (typechecker accepted an ill-typed program)" + FAIL=$((FAIL + 1)) + else + echo " PASS ill-typed/${name}" + PASS=$((PASS + 1)) + fi +done + echo "" echo "Results: ${PASS}/${TOTAL} passed, ${FAIL} failed" diff --git a/docs/spec/FORMAL-SEMANTICS.md b/docs/spec/FORMAL-SEMANTICS.md index b0061f6..5578281 100644 --- a/docs/spec/FORMAL-SEMANTICS.md +++ b/docs/spec/FORMAL-SEMANTICS.md @@ -477,6 +477,65 @@ yield declarations match B Weave blocks can reference all definitions in Γ (D2.8). +#### 3.10.1 Strand quantities — the linear discipline + +The rule above has two side conditions that were, until the quantity semiring +landed, written down and never enforced: the `i ≠ j` on `[T-Cross-Over]` / +`[T-Cross-Under]` below, and "yield declarations match B". Both are instances +of one law, so both are now discharged by one check. + +TANGLE annotates resources with a quantity from the QTT semiring +{0, 1, ω} (Atkey 2018), rather than committing the whole language to a single +substructural discipline: + +| quantity | reading | who carries it | +|---|---|---| +| `0` | erased — present for typing, absent at runtime | the claim in `Epi[κ, ρ, τ]` (see A-TG-11.1) | +| `1` | linear — used **exactly** once | **strands** inside a `weave` | +| `ω` | unrestricted — used freely | braid **words**, and every ordinary binding | + +Why a semiring and not a choice: + +- **Words are ω.** `x . x` is σ₁², a perfectly good braid. A blanket linear + discipline would reject a valid program. +- **Strands are 1, and linear rather than affine.** A strand is a physical + thread. A braid on *n* strands is a *permutation* of those *n* strands, so + strand count is a conservation law: a strand may be neither duplicated + (contraction) nor dropped (weakening). Affine permits the second, so affine + is specifically the wrong discipline here — this is the case that decides it. + +Independent uses combine with semiring addition, so two uses of one strand give +`1 + 1 = ω`, and `ω` is not permitted where `1` was declared. + +``` +Σ = {a₁ : (1, T₁), ..., aₙ : (n, Tₙ)} +uses(body, aᵢ) = 1 for every i (no contraction, no + unused strand) +⟦b₁, ..., bₘ⟧ is a permutation of ⟦a₁, ..., aₙ⟧ (m = n; conservation) +────────────────────────────────────────────────────────── [T-Weave-Linear] +Σ ⊢ weave strands a₁,...,aₙ into body yield strands b₁,...,bₘ linear +``` + +`uses` is defined by structural recursion over the body, mapping into the +semiring: a strand occurrence contributes `1`, the two operands of a crossing +and the two sides of any binary form combine with `+`, and non-strand leaves +contribute `0`. + +Four programs this rejects, each previously accepted in silence: + +| program | violated law | +|---|---| +| `weave strands a, b into (a > a) yield strands a, b` | contraction (also the spec's `i ≠ j`) | +| `weave strands a, b into (a > b) yield strands a, b, a` | contraction in the yield | +| `weave strands a, b into (a > b) yield strands a` | weakening — a strand vanished | +| `weave strands a, b into (a > b) yield strands a, c` | `c` is not in the input boundary | + +**Scope.** This is the semiring applied *to strands*, which is where the +discipline bites and where the soundness gap was. TANGLE's core judgement is +still `Γ ⊢ e : τ` without quantities on ordinary bindings; a full QTT judgement +`Γ ⊢ e :^q τ` would change the judgement shape and require re-proving the +metatheory, and is tracked separately. + **Crossing in weave context**: ``` diff --git a/scripts/check-corpus.sh b/scripts/check-corpus.sh index 00a30d3..2cc005f 100755 --- a/scripts/check-corpus.sh +++ b/scripts/check-corpus.sh @@ -187,10 +187,39 @@ for f in "${ROOT}"/conformance/invalid/*.tangle; do fi done +# ── 6. Conformance: ill-typed programs must PARSE and then be REJECTED. +# +# A third tier, separate from invalid/, because "the compiler rejects it" is +# two different properties and conflating them produces a gate that passes for +# the wrong reason. invalid/ is grammar-level: the file must not parse. +# ill-typed/ is type-level: the file MUST parse — reaching the typechecker is +# the whole point of the test — and the typechecker must then reject it. +# +# Asserting only the rejection is precisely the failure this suite already had +# once, when three invalid/ cases "passed" because the command was wrong and +# failed on every input. A typo in an ill-typed/ fixture would score the same +# false point here, so the parse step is asserted first. +echo +echo "== conformance: ill-typed programs must parse, then be rejected ==" +for f in "${ROOT}"/conformance/ill-typed/*.tangle; do + [[ -e "$f" ]] || continue + n="$(basename "$f")" + if ! "${BIN}" "$f" >/dev/null 2>&1; then + note "ill-typed/$n" "PARSE FAILED (must parse first)" + echo "::error::conformance/ill-typed/${n} does not parse — it must reach the typechecker to prove anything"; fail=1 + elif "${BIN}" --check "$f" >/dev/null 2>&1; then + note "ill-typed/$n" "TYPECHECKED (should not)" + echo "::error::conformance/ill-typed/${n} was accepted by the typechecker but is meant to be rejected"; fail=1 + else + note "ill-typed/$n" "parsed, then rejected ok" + fi +done + echo if [[ "$fail" -ne 0 ]]; then echo "::error::corpus drifted from the manifest — see the errors above." exit 1 fi echo "Corpus matches the manifest: examples parse, the must-run set evaluates," -echo "known gaps are unchanged, and invalid programs are still rejected." +echo "known gaps are unchanged, invalid programs are still rejected, and" +echo "ill-typed programs still parse but still fail to typecheck." From 159c8e7584e923142de3a690caddf00d1b7179a6 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 29 Jul 2026 08:36:37 +0100 Subject: [PATCH 2/2] feat(jeg): close all 17 deferred rules; report the one remaining hole MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Seventeen rules matched a `-> ()` arm in `check`. That is not a partial check — it is an ACCEPT. A forged node naming T-Close, T-App or T-Weave could conclude any type at all and the graph still checked green. Since the JEG's whole claim is "evidence, not a log", those arms were the part that made the claim false. ## What made them underivable, and the fix Three of them (T-App, T-Crossing, T-Weave) genuinely could not be re-derived from the recorded data, because the judgement did not carry what the rule reads. So the judgement was widened: * `j_ctx` now holds `env_entry`, not `ty` — a T-App node cannot be checked without the callee's SIGNATURE. * `j_sigma` (new) holds the strand context — T-Crossing and T-Weave read Sigma rather than premise types. They were previously bare LEAVES: nodes asserting a type with nothing licensing it at all. The rest were derivable all along and simply had not been written. ## Shared rule functions, so the JEG cannot drift `infer_binop` was already a type-in/type-out function. The remaining rules were inline in `infer_expr`, so the JEG would have had to RE-IMPLEMENT them — and a JEG that re-implements the rules can drift from the typechecker, at which point it certifies a rule the compiler does not apply and the evidence is worthless. Extracted 16 of them (`infer_close`, `infer_mirror`, `infer_echo_eq`, `join_arm_ty`, ...) into one definition each, called by BOTH. Drift is now impossible by construction rather than by discipline. The extraction is behaviour-preserving: all pre-existing tests pass unchanged. ## Two rules with real substance * T-Let checks the conclusion is the BODY's type AND that the body was checked under the binding the let actually makes. Checking only the type would accept a derivation whose body silently assumed `x` had some more convenient type — there is a test for exactly that forgery. * T-Weave re-runs the strand LINEARITY check, so a graph cannot launder a weave that duplicates or drops a strand. ## The remaining hole is reported, not hidden T-Add-Block's island has its own judgement (|-_hd). Rather than a silent accept, it is recorded: new `unchecked : derivation -> (string * judgement) list`. "check succeeded" and "check succeeded and re-derived every node" are now distinguishable, and `--derive` prints which it was: == c == (3 nodes, depth 3, every node re-derived) ## Verification * JEG suite 19 -> 51 tests; an honest/forged PAIR for each rule closed, so each test's forged half is a case that would have PASSED before * 709 compiler tests pass (`dune runtest --force`) * conformance 23/23, corpus + RSR gates green Co-Authored-By: Claude Opus 5 --- compiler/bin/main.ml | 18 ++- compiler/lib/jeg.ml | 262 ++++++++++++++++++++++++++++++++++---- compiler/lib/jeg.mli | 39 +++++- compiler/lib/typecheck.ml | 254 +++++++++++++++++++++--------------- compiler/test/test_jeg.ml | 191 ++++++++++++++++++++++++++- 5 files changed, 627 insertions(+), 137 deletions(-) diff --git a/compiler/bin/main.ml b/compiler/bin/main.ml index 3a234ae..a39ce33 100644 --- a/compiler/bin/main.ml +++ b/compiler/bin/main.ml @@ -231,8 +231,22 @@ let derive_file ?(dot = false) (filename : string) : unit = end; if dot then print_string (Tangle.Jeg.to_dot dv) else begin - Printf.printf "== %s == (%d nodes, depth %d)\n" - d.Tangle.Ast.def_name (Tangle.Jeg.size dv) (Tangle.Jeg.depth dv); + (* Report coverage, not just size. A graph that checks is worth less + if some of its nodes were accepted without being re-derived, and + the reader cannot tell the difference from the tree alone. *) + let unchecked = Tangle.Jeg.unchecked dv in + let coverage = + match unchecked with + | [] -> "every node re-derived" + | us -> + Printf.sprintf "%d node(s) NOT re-derived: %s" + (List.length us) + (String.concat ", " + (List.sort_uniq compare (List.map fst us))) + in + Printf.printf "== %s == (%d nodes, depth %d, %s)\n" + d.Tangle.Ast.def_name (Tangle.Jeg.size dv) (Tangle.Jeg.depth dv) + coverage; print_string (Tangle.Jeg.to_string dv); print_newline () end; diff --git a/compiler/lib/jeg.ml b/compiler/lib/jeg.ml index 1296b83..2f60f6a 100644 --- a/compiler/lib/jeg.ml +++ b/compiler/lib/jeg.ml @@ -5,9 +5,10 @@ open Ast open Typecheck type judgement = { - j_ctx : (string * ty) list; - j_expr : expr; - j_ty : ty; + j_ctx : (string * env_entry) list; + j_sigma : (string * strand_entry) list; + j_expr : expr; + j_ty : ty; } type derivation = { @@ -29,23 +30,47 @@ type check_error = { (* Only the bindings a node actually consults are recorded, so the graph stays readable: a 40-binding environment would otherwise be repeated at every node. *) -let ctx_of (gamma : env) (names : string list) : (string * ty) list = +(* Function signatures are recorded, not just value types: without the callee's + signature a T-App node cannot be re-derived at all, and an unre-derivable + node is a hole a forger can put anything through. *) +let ctx_of (gamma : env) (names : string list) : (string * env_entry) list = List.filter_map (fun n -> match env_lookup gamma n with - | Some (EVal t) -> Some (n, t) - | _ -> None) names + | Some entry -> Some (n, entry) + | None -> None) names -let node rule gamma names e t premises = +let node ?(sigma = []) rule gamma names e t premises = { d_rule = rule; - d_conclusion = { j_ctx = ctx_of gamma names; j_expr = e; j_ty = t }; + d_conclusion = + { j_ctx = ctx_of gamma names; j_sigma = sigma; j_expr = e; j_ty = t }; d_premises = premises } +(* Record only the strand entries a node consults, mirroring [ctx_of]. *) +let strands_of (sigma : strand_ctx) (names : string list) : + (string * strand_entry) list = + List.filter_map (fun n -> + match strand_lookup sigma n with + | Some se -> Some (n, se) + | None -> None) names + +(* The strand context a weave block introduces — the same construction + [infer_expr] performs for [T-Weave]. *) +let sigma_of_weave (wb : weave_block) : strand_ctx = + List.mapi (fun i ts -> + let sty = match ts.strand_type with + | Some name -> StrandNamed name + | None -> StrandDefault + in + (ts.strand_name, { strand_pos = i + 1; strand_ty = sty })) wb.weave_inputs + (* The derivation is produced by the SAME rules the checker uses — `derive` is not a parallel implementation that could drift. Each case mirrors one inference rule from FORMAL-SEMANTICS.md, and the type recorded on the conclusion is the one `infer_expr` computes. *) -let rec derive (gamma : env) (e : expr) : derivation = - let ty = infer_expr gamma [] e in +let rec derive_in (gamma : env) (sigma : strand_ctx) (e : expr) : derivation = + let derive gamma e = derive_in gamma sigma e in + let node ?(sigma = sigma) = node ~sigma in + let ty = infer_expr gamma sigma e in let leaf rule = node rule gamma [] e ty [] in match e with | IntLit _ | FloatLit _ -> leaf "T-Num" @@ -99,9 +124,29 @@ let rec derive (gamma : env) (e : expr) : derivation = (derive gamma scrut :: List.map (fun a -> derive gamma a.arm_body) arms) | Call (f, args) -> node "T-App" gamma [f] e ty (List.map (derive gamma) args) + + (* An add{} island has its own judgement (|-_hd), so there is no TANGLE-rule + premise structure to record. It is the one rule `check` cannot re-derive, + and [unchecked] reports it rather than passing it off as verified. *) | AddBlock _ -> leaf "T-Add-Block" - | Crossing _ -> leaf "T-Crossing" - | Weave _ -> leaf "T-Weave" + + (* Crossings and weaves read the STRAND context, not premise types. Recording + Sigma on the judgement is what lets `check` re-derive them — previously + they were bare leaves, i.e. nodes that asserted a type with nothing + licensing it. *) + | Crossing (a, _, b) -> + { d_rule = "T-Crossing"; + d_conclusion = + { j_ctx = []; j_sigma = strands_of sigma [a; b]; j_expr = e; j_ty = ty }; + d_premises = [] } + + | Weave wb -> + (* The body is derived in the weave's OWN strand context, which is where + strand names mean anything. *) + let sigma' = sigma_of_weave wb in + node ~sigma "T-Weave" gamma [] e ty [derive_in gamma sigma' wb.weave_body] + +and derive (gamma : env) (e : expr) : derivation = derive_in gamma [] e (* ================================================================== *) (* Checking — independent of `derive` *) @@ -115,10 +160,27 @@ let rec derive (gamma : env) (e : expr) : derivation = let errs = ref [] let fail rule reason at = errs := { ce_rule = rule; ce_reason = reason; ce_at = at } :: !errs +(* Nodes accepted WITHOUT re-derivation. A rule that cannot be re-derived is a + hole — a forger can put any conclusion through it — so the holes are counted + and reportable rather than hidden behind a silent `-> ()`. `check` returning + Ok while [unchecked] is non-empty is a meaningful, and different, result. *) +let unchecked_nodes = ref [] +let defer rule at = unchecked_nodes := (rule, at) :: !unchecked_nodes + (* The type a node CLAIMS for each premise, in order. *) let premise_tys (d : derivation) : ty list = List.map (fun p -> p.d_conclusion.j_ty) d.d_premises +(* Every T-Var node inside a derivation that names [x], with the type it + assumed. Used by T-Let to verify the body was checked under the binding the + let actually introduces. *) +let rec var_uses_in (x : string) (d : derivation) : (string * ty) list = + let here = + if d.d_rule = "T-Var" && d.d_conclusion.j_expr = Var x + then [ (x, d.d_conclusion.j_ty) ] else [] + in + here @ List.concat_map (var_uses_in x) d.d_premises + let rec check_node (d : derivation) : unit = List.iter check_node d.d_premises; let c = d.d_conclusion in @@ -135,6 +197,26 @@ let rec check_node (d : derivation) : unit = fail d.d_rule (Printf.sprintf "concludes %s but the rule gives %s" (pp_ty c.j_ty) (pp_ty want)) c in + (* Run a rule function and compare. A Type_error means the premises do not + license the conclusion at all, which is a failure, not an exception to + propagate: `check` reports, it does not throw. *) + let guard rule at f = + match (try Ok (f ()) with Type_error m -> Error m) with + | Ok want -> + if at.j_ty <> want then + fail rule + (Printf.sprintf "concludes %s but the rule gives %s" + (pp_ty at.j_ty) (pp_ty want)) at + | Error m -> fail rule ("premises do not license it: " ^ m) at + in + let unary_rule d c pts f = + if arity 1 then + (match pts with [t] -> guard d.d_rule c (fun () -> f t) | _ -> ()) + in + let binary_rule d c pts f = + if arity 2 then + (match pts with [a; b] -> guard d.d_rule c (fun () -> f a b) | _ -> ()) + in match d.d_rule with (* Axioms: the conclusion must match the literal, and there are no premises. *) | "T-Num" -> if arity 0 then expect TNum @@ -151,7 +233,10 @@ let rec check_node (d : derivation) : unit = (match c.j_expr with | Var n -> (match List.assoc_opt n c.j_ctx with - | Some t -> expect t + | Some (EVal t) -> expect t + | Some (EFun _) -> + fail d.d_rule + (Printf.sprintf "'%s' is a function; it has no value type" n) c | None -> fail d.d_rule (Printf.sprintf "'%s' not in the recorded context" n) c) | _ -> fail d.d_rule "conclusion is not a variable" c) @@ -220,22 +305,149 @@ let rec check_node (d : derivation) : unit = | [t] -> fail d.d_rule ("premise must be an Epi, got " ^ pp_ty t) c | _ -> ()) - (* Rules whose side conditions are not yet re-derivable here. Listed - explicitly rather than swallowed by a wildcard, so the coverage gap is - visible: an unknown rule name is itself an error. *) - | "T-Pipeline" | "T-Unary" | "T-Close" | "T-Mirror" | "T-Reverse" - | "T-Simplify" | "T-Twist" | "T-Cap" | "T-Cup" | "T-Echo-Add" | "T-Echo-Eq" - | "T-Let" | "T-Match" | "T-App" | "T-Crossing" | "T-Weave" -> () + (* ---- Unary and pipeline: re-run the rule on the premise type. ---- *) + + | "T-Pipeline" -> + if arity 2 then + (match pts with + | [t1; t2] -> guard d.d_rule c (fun () -> infer_binop Compose t1 t2) + | _ -> ()) + + | "T-Unary" -> + if arity 1 then + (match c.j_expr, pts with + | UnaryOp (op, _), [t] -> guard d.d_rule c (fun () -> infer_unop op t) + | _ -> fail d.d_rule "conclusion is not a unary operation" c) + + | "T-Close" -> unary_rule d c pts infer_close + | "T-Mirror" -> unary_rule d c pts infer_mirror + | "T-Reverse" -> unary_rule d c pts infer_reverse + | "T-Simplify" -> unary_rule d c pts infer_simplify + | "T-Twist" -> unary_rule d c pts infer_twist + + | "T-Cap" -> binary_rule d c pts infer_cap + | "T-Cup" -> binary_rule d c pts infer_cup + | "T-Echo-Add" -> binary_rule d c pts infer_echo_add + | "T-Echo-Eq" -> binary_rule d c pts infer_echo_eq + + (* ---- T-Let ---- + Two obligations. The conclusion is the BODY's type (the bound expression's + type does not escape), and — the substantive half — the body must have been + checked under the binding the let actually introduces. Checking only the + first would accept a derivation whose body silently assumed `x` had some + more convenient type. *) + | "T-Let" -> + if arity 2 then + (match c.j_expr, d.d_premises, pts with + | Let (x, _, _), [_; body], [t1; t2] -> + expect t2; + List.iter (fun (nm, t) -> + if nm = x && t <> t1 then + fail d.d_rule + (Printf.sprintf + "body assumes '%s' : %s, but the let binds it at %s" + x (pp_ty t) (pp_ty t1)) c) + (var_uses_in x body) + | _ -> fail d.d_rule "conclusion is not a let" c) + + (* ---- T-Match ---- + Premises are the scrutinee followed by one per arm. The conclusion is the + join of the arm types (words agree up to width, #92). *) + | "T-Match" -> + (match c.j_expr, pts with + | Match (_, arms), _ :: arm_tys when List.length arms = List.length arm_tys + && arm_tys <> [] -> + let joined = + List.fold_left (fun acc t -> + match acc with None -> None | Some a -> join_arm_ty a t) + (Some (List.hd arm_tys)) arm_tys + in + (match joined with + | Some t -> expect t + | None -> fail d.d_rule "arms have no common type" c) + | Match (arms_e, _), _ -> + ignore arms_e; + fail d.d_rule + "premises must be the scrutinee followed by exactly one per arm" c + | _ -> fail d.d_rule "conclusion is not a match" c) + + (* ---- T-App ---- + Re-derivable now that the callee's SIGNATURE is recorded on the judgement. + Both halves matter: the argument types must match the parameters, and the + conclusion must be the declared return type. *) + | "T-App" -> + (match c.j_expr with + | Call (f, _) -> + (match List.assoc_opt f c.j_ctx with + | Some (EFun fs) -> + let np = List.length fs.fsig_params in + if List.length pts <> np then + fail d.d_rule + (Printf.sprintf "'%s' takes %d argument(s), the graph supplies %d" + f np (List.length pts)) c + else + List.iteri (fun i (want, got) -> + if want <> got then + fail d.d_rule + (Printf.sprintf "argument %d of '%s' is %s but the signature \ + declares %s" (i + 1) f (pp_ty got) (pp_ty want)) c) + (List.combine fs.fsig_params pts); + expect fs.fsig_return + | Some (EVal _) -> + fail d.d_rule (Printf.sprintf "'%s' is a value, not a function" f) c + | None -> + fail d.d_rule + (Printf.sprintf "'%s' is not in the recorded context — the callee's \ + signature is required to re-derive the call" f) c) + | _ -> fail d.d_rule "conclusion is not a call" c) + + (* ---- T-Crossing / T-Weave ---- + These read the STRAND context rather than premise types, so they are + re-derived against the Sigma recorded on the judgement. That is still + independent of `derive`: it recomputes the rule from the graph's own data. + For T-Weave it also re-checks strand LINEARITY, so a graph asserting a + weave that duplicates or drops a strand is rejected here too. *) + | "T-Crossing" -> + if arity 0 then + (match c.j_expr with + | Crossing _ -> guard d.d_rule c (fun () -> infer_expr [] c.j_sigma c.j_expr) + | _ -> fail d.d_rule "conclusion is not a crossing" c) + + | "T-Weave" -> + (match c.j_expr with + | Weave wb -> + guard d.d_rule c (fun () -> + (* linearity + boundary, exactly as the typechecker computes them *) + check_strand_linearity (sigma_of_weave wb) wb; + let inb = List.map (fun (_, se) -> se.strand_ty) (sigma_of_weave wb) in + let outb = List.map (fun ts -> + match ts.strand_type with + | Some n -> StrandNamed n + | None -> StrandDefault) wb.weave_outputs in + TTangle (inb, outb)) + | _ -> fail d.d_rule "conclusion is not a weave" c) + (* T-Add-Block: the island has its own judgement (|-_hd), so re-deriving it - here would mean re-implementing that checker. Deferred, and listed. *) - | "T-Add-Block" -> () + here would mean re-implementing that checker. Recorded as UNCHECKED — the + one remaining hole, and reported as such rather than silently accepted. *) + | "T-Add-Block" -> defer d.d_rule c + | r -> fail r "unknown rule name" c let check (d : derivation) : (unit, check_error list) result = errs := []; + unchecked_nodes := []; check_node d; match List.rev !errs with [] -> Ok () | es -> Error es +(** Which nodes `check` accepted without re-deriving. Empty means every node + in the graph was licensed by a rule the checker recomputed. *) +let unchecked (d : derivation) : (string * judgement) list = + errs := []; + unchecked_nodes := []; + check_node d; + List.rev !unchecked_nodes + (* ================================================================== *) (* Presentation *) (* ================================================================== *) @@ -250,7 +462,13 @@ let judgement_to_string (j : judgement) : string = let ctx = if j.j_ctx = [] then "" else (String.concat ", " - (List.map (fun (n, t) -> n ^ ":" ^ pp_ty t) j.j_ctx)) ^ " " + (List.map (fun (n, entry) -> + match entry with + | EVal t -> n ^ ":" ^ pp_ty t + | EFun fs -> + Printf.sprintf "%s:(%s)->%s" n + (String.concat ", " (List.map pp_ty fs.fsig_params)) + (pp_ty fs.fsig_return)) j.j_ctx)) ^ " " in Printf.sprintf "%s|- %s : %s" ctx (Pretty.expr_to_string j.j_expr) (pp_ty j.j_ty) diff --git a/compiler/lib/jeg.mli b/compiler/lib/jeg.mli index 3fa9e87..ea00d51 100644 --- a/compiler/lib/jeg.mli +++ b/compiler/lib/jeg.mli @@ -18,6 +18,13 @@ * from the premises. A hand-edited or forged graph fails. That is the whole * point — see the forgery tests in test_jeg.ml. * + * ── Coverage ──────────────────────────────────────────────────────────────── + * Every rule the graph can name is re-derived by [check], with one exception: + * [T-Add-Block], whose island is typed by a separate judgement (⊢_hd). That + * exception is REPORTED by [unchecked] rather than hidden behind a silent + * accept, because a rule the checker waves through is a hole — any conclusion + * passes it, and "the graph checks" then means less than it appears to. + * * ── Relation to TG-11 (epistemic types) ───────────────────────────────────── * A checked derivation is exactly what `Epi[κ, ρ, τ]` is for: standpoint κ * holds evidence ρ for claim τ. The JEG is the ρ. And the non-factivity of @@ -26,12 +33,21 @@ * `SoundWarrant.sound` of this module. *) -(** A single judgement: Γ ⊢ e : τ. The context records only the bindings the - derivation actually consults, so the graph stays readable. *) +(** A single judgement: Γ; Σ ⊢ e : τ. The contexts record only the bindings the + derivation actually consults, so the graph stays readable. + + [j_ctx] carries full environment entries, not just value types, because a + T-App node cannot be re-derived without the callee's SIGNATURE — and a node + that cannot be re-derived is a hole a forger can put anything through. + + [j_sigma] is the strand context, for the same reason: [T-Crossing] and + [T-Weave] read Σ rather than premise types, so without it they were bare + leaves asserting a type with nothing licensing it. *) type judgement = { - j_ctx : (string * Typecheck.ty) list; - j_expr : Ast.expr; - j_ty : Typecheck.ty; + j_ctx : (string * Typecheck.env_entry) list; + j_sigma : (string * Typecheck.strand_entry) list; + j_expr : Ast.expr; + j_ty : Typecheck.ty; } (** A derivation node: the rule applied, what it concludes, and the sub-derivations @@ -54,11 +70,24 @@ type check_error = { produced by the same rules, not a parallel implementation. *) val derive : Typecheck.env -> Ast.expr -> derivation +(** As [derive], but starting inside a given strand context — the form needed + to derive an expression that mentions strand names. *) +val derive_in : Typecheck.env -> Typecheck.strand_ctx -> Ast.expr -> derivation + (** Independently re-validate a derivation. Does NOT call [derive]: it checks each node's rule against its premises from scratch, so a forged graph is rejected. [Ok ()] iff every node is licensed by the rule it names. *) val check : derivation -> (unit, check_error list) result +(** The nodes [check] accepted WITHOUT re-deriving them, with the rule name. + + A rule the checker cannot recompute is a hole: any conclusion passes through + it. Rather than hide those behind a silent accept, they are counted, so + "check succeeded" and "check succeeded and re-derived every node" are + distinguishable results. Currently the only such rule is [T-Add-Block], + whose island has its own judgement (⊢_hd). *) +val unchecked : derivation -> (string * judgement) list + (** Number of nodes (judgements) in the graph. *) val size : derivation -> int diff --git a/compiler/lib/typecheck.ml b/compiler/lib/typecheck.ml index c976ff0..9895256 100644 --- a/compiler/lib/typecheck.ml +++ b/compiler/lib/typecheck.ml @@ -470,79 +470,29 @@ let rec infer_expr (gamma : env) (sigma : strand_ctx) (e : expr) : ty = (* ---- Unary operators ---- *) - | UnaryOp (Neg, e1) -> - let t = infer_expr gamma sigma e1 in - begin match t with - | TNum -> TNum - | _ -> type_error "Negation requires Num, got %s" (pp_ty t) - end - - | UnaryOp (Not, e1) -> - let t = infer_expr gamma sigma e1 in - begin match t with - | TBool -> TBool - | _ -> type_error "Logical not requires Bool, got %s" (pp_ty t) - end + | UnaryOp (op, e1) -> infer_unop op (infer_expr gamma sigma e1) (* ---- Tier 1 primitives ---- *) (* [T-Close-Word], [T-Close-Tangle] *) - | Close e1 -> - let t = infer_expr gamma sigma e1 in - begin match t with - | TWord _ -> TTangle (empty_boundary, empty_boundary) - | TTangle (a, b) -> - if List.length a <> List.length b then - type_error "close requires |A| = |B|, got |%s| = %d and |%s| = %d" - (pp_boundary a) (List.length a) - (pp_boundary b) (List.length b); - TTangle (empty_boundary, empty_boundary) - | _ -> type_error "close requires Word[n] or Tangle[A,B], got %s" (pp_ty t) - end + | Close e1 -> infer_close (infer_expr gamma sigma e1) (* [T-Mirror-Word], [T-Mirror-Tangle] *) - | Mirror e1 -> - let t = infer_expr gamma sigma e1 in - begin match t with - | TWord n -> TWord n - | TTangle (a, b) -> TTangle (b, a) - | _ -> type_error "mirror requires Word[n] or Tangle[A,B], got %s" (pp_ty t) - end + | Mirror e1 -> infer_mirror (infer_expr gamma sigma e1) (* [T-Reverse] *) - | Reverse e1 -> - let t = infer_expr gamma sigma e1 in - begin match t with - | TWord n -> TWord n - | _ -> type_error "reverse requires Word[n], got %s" (pp_ty t) - end + | Reverse e1 -> infer_reverse (infer_expr gamma sigma e1) (* [T-Simplify-Word], [T-Simplify-Tangle] *) - | Simplify e1 -> - let t = infer_expr gamma sigma e1 in - begin match t with - | TWord n -> TWord n - | TTangle (a, b) -> TTangle (a, b) - | _ -> type_error "simplify requires Word[n] or Tangle[A,B], got %s" (pp_ty t) - end + | Simplify e1 -> infer_simplify (infer_expr gamma sigma e1) (* [T-Cap], [T-Cap-Typed] *) | Cap (e1, e2) -> - let t1 = infer_expr gamma sigma e1 in - let t2 = infer_expr gamma sigma e2 in - (* Cap creates a tangle that absorbs two strands from above *) - let s1 = strand_type_of_ty t1 in - let s2 = strand_type_of_ty t2 in - TTangle ([s1; s2], empty_boundary) + infer_cap (infer_expr gamma sigma e1) (infer_expr gamma sigma e2) (* [T-Cup], [T-Cup-Typed] *) | Cup (e1, e2) -> - let t1 = infer_expr gamma sigma e1 in - let t2 = infer_expr gamma sigma e2 in - (* Cup creates a tangle that emits two strands below *) - let s1 = strand_type_of_ty t1 in - let s2 = strand_type_of_ty t2 in - TTangle (empty_boundary, [s1; s2]) + infer_cup (infer_expr gamma sigma e1) (infer_expr gamma sigma e2) (* [T-Twist-Word], [T-Twist-Tangle] (D1.18) *) | Twist e1 -> @@ -566,12 +516,7 @@ let rec infer_expr (gamma : env) (sigma : strand_ctx) (e : expr) : ty = TTangle ([strand_to_type ea.strand_ty], [strand_to_type ea.strand_ty]) | _ -> (* [T-Twist-Word] / [T-Twist-Tangle]: the standalone forms. *) - let t = infer_expr gamma sigma e1 in - begin match t with - | TWord n -> TWord n - | TTangle (a, b) -> TTangle (a, b) - | _ -> type_error "twist requires Word[n] or Tangle[A,B], got %s" (pp_ty t) - end + infer_twist (infer_expr gamma sigma e1) end (* ---- Crossings in weave context [T-Cross-Over], [T-Cross-Under] ---- *) @@ -624,12 +569,7 @@ let rec infer_expr (gamma : env) (sigma : strand_ctx) (e : expr) : ty = requiring equal widths. Arms at Word[0] and Word[2] describe the same kind of thing at different strand counts; the join is the wider. Everything else must still match exactly. *) - let join_ty a b = - match a, b with - | TWord n, TWord m -> Some (TWord (max n m)) - | x, y when x = y -> Some x - | _ -> None - in + let join_ty = join_arm_ty in let result_ty = List.fold_left (fun acc ty -> match acc with @@ -661,56 +601,26 @@ let rec infer_expr (gamma : env) (sigma : strand_ctx) (e : expr) : ty = * [T-Echo-Add] echoAdd a b : Echo[Num × Num, Num] * [T-Echo-Eq] echoEq a b : Echo[ρ × ρ, Bool] for ρ ∈ {Num, Str, Word[n]} *) - | EchoClose e1 -> - begin match infer_expr gamma sigma e1 with - | TWord n -> TEcho (TWord n, TWord 0) - | t -> type_error "echoClose requires Word[n], got %s" (pp_ty t) - end + | EchoClose e1 -> infer_echo_close (infer_expr gamma sigma e1) - | Lower e1 -> - begin match infer_expr gamma sigma e1 with - | TEcho (_, t) -> t - | t -> type_error "lower requires Echo[_, _], got %s" (pp_ty t) - end + | Lower e1 -> infer_lower (infer_expr gamma sigma e1) - | Residue e1 -> - begin match infer_expr gamma sigma e1 with - | TEcho (r, _) -> r - | t -> type_error "residue requires Echo[_, _], got %s" (pp_ty t) - end + | Residue e1 -> infer_residue (infer_expr gamma sigma e1) | Pair (e1, e2) -> let t1 = infer_expr gamma sigma e1 in let t2 = infer_expr gamma sigma e2 in TProd (t1, t2) - | Fst e1 -> - begin match infer_expr gamma sigma e1 with - | TProd (a, _) -> a - | t -> type_error "fst requires a product, got %s" (pp_ty t) - end + | Fst e1 -> infer_fst (infer_expr gamma sigma e1) - | Snd e1 -> - begin match infer_expr gamma sigma e1 with - | TProd (_, b) -> b - | t -> type_error "snd requires a product, got %s" (pp_ty t) - end + | Snd e1 -> infer_snd (infer_expr gamma sigma e1) | EchoAdd (e1, e2) -> - begin match infer_expr gamma sigma e1, infer_expr gamma sigma e2 with - | TNum, TNum -> TEcho (TProd (TNum, TNum), TNum) - | t1, t2 -> type_error "echoAdd requires Num, Num, got %s, %s" (pp_ty t1) (pp_ty t2) - end + infer_echo_add (infer_expr gamma sigma e1) (infer_expr gamma sigma e2) | EchoEq (e1, e2) -> - begin match infer_expr gamma sigma e1, infer_expr gamma sigma e2 with - | TNum, TNum -> TEcho (TProd (TNum, TNum), TBool) - | TStr, TStr -> TEcho (TProd (TStr, TStr), TBool) - | TWord n, TWord m when n = m -> TEcho (TProd (TWord n, TWord n), TBool) - | t1, t2 -> - type_error "echoEq requires matching Num/Str/Word[n] operands, got %s, %s" - (pp_ty t1) (pp_ty t2) - end + infer_echo_eq (infer_expr gamma sigma e1) (infer_expr gamma sigma e2) (** Infer the type of a binary operation given operand types. * Implements rules from sections 3.4, 3.5, 3.6. @@ -860,6 +770,138 @@ and check_compatible (expected : ty) (actual : ty) (fname : string) : unit = type_error "Function '%s': expected %s but got %s" fname (pp_ty expected) (pp_ty actual) +(* ================================================================== *) +(* Type-level rule functions *) +(* ================================================================== *) +(* One function per typing rule, taking the PREMISE types and returning the + conclusion type (or raising Type_error). [infer_binop] was always written + this way; these bring the remaining rules into the same shape. + + The point is not tidiness. The Judgement Evidence Graph (jeg.ml) has to + re-derive each rule in order to reject forged derivations, and a JEG that + re-implements the rules independently can DRIFT from the typechecker — at + which point it certifies a rule the compiler does not actually apply, and + the evidence is worthless. Sharing one definition makes drift impossible + by construction: there is nothing to keep in sync. *) + +and infer_unop (op : unaryop) (t : ty) : ty = + match op, t with + | Neg, TNum -> TNum + | Neg, _ -> type_error "Negation requires Num, got %s" (pp_ty t) + | Not, TBool -> TBool + | Not, _ -> type_error "Logical not requires Bool, got %s" (pp_ty t) + +(** [T-Close-Word], [T-Close-Tangle]. Closure needs |A| = |B| — you cannot + join a boundary to one of a different size. *) +and infer_close (t : ty) : ty = + match t with + | TWord _ -> TTangle (empty_boundary, empty_boundary) + | TTangle (a, b) -> + if List.length a <> List.length b then + type_error "close requires |A| = |B|, got |%s| = %d and |%s| = %d" + (pp_boundary a) (List.length a) (pp_boundary b) (List.length b); + TTangle (empty_boundary, empty_boundary) + | _ -> type_error "close requires Word[n] or Tangle[A,B], got %s" (pp_ty t) + +(** [T-Mirror-Word], [T-Mirror-Tangle]. Mirroring a tangle swaps its + boundaries; mirroring a word keeps its width. *) +and infer_mirror (t : ty) : ty = + match t with + | TWord n -> TWord n + | TTangle (a, b) -> TTangle (b, a) + | _ -> type_error "mirror requires Word[n] or Tangle[A,B], got %s" (pp_ty t) + +(** [T-Reverse]. Words only — reverse is w^-1, and inversion is not defined + on a tangle's boundary pair. *) +and infer_reverse (t : ty) : ty = + match t with + | TWord n -> TWord n + | _ -> type_error "reverse requires Word[n], got %s" (pp_ty t) + +(** [T-Simplify-Word], [T-Simplify-Tangle]. Reidemeister reduction preserves + the type: it changes the representative, not what it is a representative + of. *) +and infer_simplify (t : ty) : ty = + match t with + | TWord n -> TWord n + | TTangle (a, b) -> TTangle (a, b) + | _ -> type_error "simplify requires Word[n] or Tangle[A,B], got %s" (pp_ty t) + +(** [T-Twist-Word], [T-Twist-Tangle] — the STANDALONE forms only. + [T-Twist-Strand] is not here because it reads the strand context rather + than a premise type, so it has no type-in/type-out shape. *) +and infer_twist (t : ty) : ty = + match t with + | TWord n -> TWord n + | TTangle (a, b) -> TTangle (a, b) + | _ -> type_error "twist requires Word[n] or Tangle[A,B], got %s" (pp_ty t) + +(** [T-Cap] — absorbs two strands from above. *) +and infer_cap (t1 : ty) (t2 : ty) : ty = + TTangle ([strand_type_of_ty t1; strand_type_of_ty t2], empty_boundary) + +(** [T-Cup] — emits two strands below. *) +and infer_cup (t1 : ty) (t2 : ty) : ty = + TTangle (empty_boundary, [strand_type_of_ty t1; strand_type_of_ty t2]) + +(** [T-Echo-Close]. Residue-retaining closure: the word that was closed is + kept as the residue rather than discarded. *) +and infer_echo_close (t : ty) : ty = + match t with + | TWord n -> TEcho (TWord n, TWord 0) + | _ -> type_error "echoClose requires Word[n], got %s" (pp_ty t) + +(** [T-Lower] — project an echo to its result, discarding the residue. *) +and infer_lower (t : ty) : ty = + match t with + | TEcho (_, r) -> r + | _ -> type_error "lower requires Echo[_, _], got %s" (pp_ty t) + +(** [T-Residue] — recover the witness. *) +and infer_residue (t : ty) : ty = + match t with + | TEcho (r, _) -> r + | _ -> type_error "residue requires Echo[_, _], got %s" (pp_ty t) + +(** [T-Fst], [T-Snd]. *) +and infer_fst (t : ty) : ty = + match t with + | TProd (a, _) -> a + | _ -> type_error "fst requires a product, got %s" (pp_ty t) + +and infer_snd (t : ty) : ty = + match t with + | TProd (_, b) -> b + | _ -> type_error "snd requires a product, got %s" (pp_ty t) + +(** [T-Echo-Add] — addition that keeps both summands as residue. *) +and infer_echo_add (t1 : ty) (t2 : ty) : ty = + match t1, t2 with + | TNum, TNum -> TEcho (TProd (TNum, TNum), TNum) + | _ -> type_error "echoAdd requires Num, Num, got %s, %s" (pp_ty t1) (pp_ty t2) + +(** [T-Echo-Eq] — equality that keeps both operands as residue. This is the + operation that makes loss structured: ordinary `==` forgets what it + compared, and the residue is exactly what it forgot. *) +and infer_echo_eq (t1 : ty) (t2 : ty) : ty = + match t1, t2 with + | TNum, TNum -> TEcho (TProd (TNum, TNum), TBool) + | TStr, TStr -> TEcho (TProd (TStr, TStr), TBool) + | TWord n, TWord m when n = m -> TEcho (TProd (TWord n, TWord n), TBool) + | _ -> + type_error "echoEq requires matching Num/Str/Word[n] operands, got %s, %s" + (pp_ty t1) (pp_ty t2) + +(** The join used by [T-Match] to reconcile arm types. Words agree UP TO + WIDTH (#92): arms at Word[0] and Word[2] describe the same kind of thing + at different strand counts, and the join is the wider. Everything else + must match exactly. *) +and join_arm_ty (a : ty) (b : ty) : ty option = + match a, b with + | TWord n, TWord m -> Some (TWord (max n m)) + | x, y when x = y -> Some x + | _ -> None + (** Extract a strand_type from a type expression for cap/cup. * Numbers/strings produce default strands; this is a simplified model. *) diff --git a/compiler/test/test_jeg.ml b/compiler/test/test_jeg.ml index 858214b..bf3b04a 100644 --- a/compiler/test/test_jeg.ml +++ b/compiler/test/test_jeg.ml @@ -29,8 +29,14 @@ let sigma i = gen i 1 let ok = function Ok () -> true | Error _ -> false let rejected = function Ok () -> false | Error _ -> true -(* Build a node directly, bypassing `derive` — this is how a forgery is made. *) -let j ctx e t = { j_ctx = ctx; j_expr = e; j_ty = t } +(* Build a node directly, bypassing `derive` — this is how a forgery is made. + [ctx] is given as plain (name, ty) pairs for brevity; [jf] takes function + signatures, which T-App needs. *) +let j ctx e t = + { j_ctx = List.map (fun (n, ty) -> (n, EVal ty)) ctx; + j_sigma = []; j_expr = e; j_ty = t } +let jf ctx e t = { j_ctx = ctx; j_sigma = []; j_expr = e; j_ty = t } +let js sigma e t = { j_ctx = []; j_sigma = sigma; j_expr = e; j_ty = t } let n rule concl prems = { d_rule = rule; d_conclusion = concl; d_premises = prems } (* ================================================================== *) @@ -124,6 +130,187 @@ let () = [n "T-Num" (j [] (IntLit 42) TNum) []; n "T-Braid" (j [] (BraidLit [sigma 1]) (TWord 2)) []]))); + (* ================================================================== *) + (* Rules that used to be DEFERRED *) + (* ================================================================== *) + (* Every rule below previously matched a `-> ()` arm: `check` accepted the + node without re-deriving it, so ANY conclusion passed. Each honest/forged + pair here is the evidence that the hole is closed — the forged half would + have passed before. *) + + Printf.printf "\n=== Unary and structural rules (were deferred) ===\n"; + + let w2 = BraidLit [sigma 1] in (* : Word[2] *) + let dw2 () = n "T-Braid" (j [] w2 (TWord 2)) [] in + + test "honest: T-Mirror on a word keeps the width" (fun () -> + ok (check (n "T-Mirror" (j [] (Mirror w2) (TWord 2)) [dw2 ()]))); + + test "forged: T-Mirror changing the width is rejected" (fun () -> + rejected (check (n "T-Mirror" (j [] (Mirror w2) (TWord 9)) [dw2 ()]))); + + test "forged: T-Reverse on a non-word is rejected" (fun () -> + rejected (check (n "T-Reverse" (j [] (Reverse (IntLit 1)) TNum) + [n "T-Num" (j [] (IntLit 1) TNum) []]))); + + test "honest: T-Close yields the closed tangle" (fun () -> + ok (check (n "T-Close" (j [] (Close w2) (TTangle ([], []))) [dw2 ()]))); + + test "forged: T-Close concluding a word is rejected" (fun () -> + rejected (check (n "T-Close" (j [] (Close w2) (TWord 2)) [dw2 ()]))); + + test "forged: T-Simplify changing the type is rejected" (fun () -> + rejected (check (n "T-Simplify" (j [] (Simplify w2) TNum) [dw2 ()]))); + + test "forged: T-Twist on a Num is rejected" (fun () -> + rejected (check (n "T-Twist" (j [] (Twist (IntLit 1)) TNum) + [n "T-Num" (j [] (IntLit 1) TNum) []]))); + + test "honest: T-Pipeline composes" (fun () -> + ok (check (n "T-Pipeline" (j [] (Pipeline (w2, w2)) (TWord 2)) + [dw2 (); dw2 ()]))); + + test "forged: T-Pipeline with a bogus result width is rejected" (fun () -> + rejected (check (n "T-Pipeline" (j [] (Pipeline (w2, w2)) (TWord 7)) + [dw2 (); dw2 ()]))); + + test "forged: T-Unary negating a Bool is rejected" (fun () -> + rejected (check (n "T-Unary" (j [] (UnaryOp (Neg, BoolLit true)) TBool) + [n "T-Bool" (j [] (BoolLit true) TBool) []]))); + + test "forged: T-Echo-Eq on mismatched operands is rejected" (fun () -> + rejected (check (n "T-Echo-Eq" + (j [] (EchoEq (IntLit 1, StringLit "a")) + (TEcho (TProd (TNum, TNum), TBool))) + [n "T-Num" (j [] (IntLit 1) TNum) []; + n "T-Str" (j [] (StringLit "a") TStr) []]))); + + Printf.printf "\n=== T-Let: the body must use the binding the let makes ===\n"; + + let letexp = Let ("x", IntLit 1, Var "x") in + + test "honest: T-Let concludes the body type" (fun () -> + ok (check (n "T-Let" (j [] letexp TNum) + [n "T-Num" (j [] (IntLit 1) TNum) []; + n "T-Var" (j [("x", TNum)] (Var "x") TNum) []]))); + + (* The forgery that the type-only check would miss: the body claims `x` is a + Word, which the let never bound it to. *) + test "forged: body assumes a different type for the bound variable" (fun () -> + rejected (check (n "T-Let" (j [] letexp (TWord 2)) + [n "T-Num" (j [] (IntLit 1) TNum) []; + n "T-Var" (j [("x", TWord 2)] (Var "x") (TWord 2)) []]))); + + test "forged: T-Let concluding the BOUND type not the body type" (fun () -> + let e = Let ("x", IntLit 1, BoolLit true) in + rejected (check (n "T-Let" (j [] e TNum) + [n "T-Num" (j [] (IntLit 1) TNum) []; + n "T-Bool" (j [] (BoolLit true) TBool) []]))); + + Printf.printf "\n=== T-Match: the conclusion is the join of the arms ===\n"; + + let marms = [ { arm_pattern = PatWildcard; arm_body = IntLit 1 } ] in + let mexp = Match (IntLit 0, marms) in + + test "honest: single-arm match concludes the arm type" (fun () -> + ok (check (n "T-Match" (j [] mexp TNum) + [n "T-Num" (j [] (IntLit 0) TNum) []; + n "T-Num" (j [] (IntLit 1) TNum) []]))); + + test "forged: match concluding a type no arm has" (fun () -> + rejected (check (n "T-Match" (j [] mexp TBool) + [n "T-Num" (j [] (IntLit 0) TNum) []; + n "T-Num" (j [] (IntLit 1) TNum) []]))); + + test "forged: match missing an arm premise" (fun () -> + let two = [ { arm_pattern = PatWildcard; arm_body = IntLit 1 }; + { arm_pattern = PatWildcard; arm_body = IntLit 2 } ] in + rejected (check (n "T-Match" (j [] (Match (IntLit 0, two)) TNum) + [n "T-Num" (j [] (IntLit 0) TNum) []; + n "T-Num" (j [] (IntLit 1) TNum) []]))); + + Printf.printf "\n=== T-App: checked against the recorded signature ===\n"; + + let fsig = EFun { fsig_params = [TNum]; fsig_return = TBool } in + let callexp = Call ("f", [IntLit 1]) in + + test "honest: call matching the signature" (fun () -> + ok (check (n "T-App" (jf [("f", fsig)] callexp TBool) + [n "T-Num" (j [] (IntLit 1) TNum) []]))); + + test "forged: call concluding a type the signature does not return" (fun () -> + rejected (check (n "T-App" (jf [("f", fsig)] callexp TNum) + [n "T-Num" (j [] (IntLit 1) TNum) []]))); + + test "forged: argument type does not match the parameter" (fun () -> + rejected (check (n "T-App" (jf [("f", fsig)] (Call ("f", [BoolLit true])) TBool) + [n "T-Bool" (j [] (BoolLit true) TBool) []]))); + + test "forged: wrong number of arguments" (fun () -> + rejected (check (n "T-App" (jf [("f", fsig)] (Call ("f", [])) TBool) []))); + + test "forged: callee absent from the recorded context" (fun () -> + rejected (check (n "T-App" (jf [] callexp TBool) + [n "T-Num" (j [] (IntLit 1) TNum) []]))); + + Printf.printf "\n=== T-Crossing / T-Weave: re-derived against Sigma ===\n"; + + let sq p = { strand_pos = p; strand_ty = StrandNamed "Q" } in + let sg = [ ("a", sq 1); ("b", sq 2) ] in + let cr = Crossing ("a", Over, "b") in + let qq = [StrandNamed "Q"; StrandNamed "Q"] in + + test "honest: crossing derived and checked in a strand context" (fun () -> + ok (check (derive_in [] sg cr))); + + test "honest: hand-built crossing node against Sigma" (fun () -> + ok (check (n "T-Crossing" (js sg cr (TTangle (qq, qq))) []))); + + test "forged: crossing concluding a word" (fun () -> + rejected (check (n "T-Crossing" (js sg cr (TWord 2)) []))); + + test "forged: crossing naming a strand not in Sigma" (fun () -> + rejected (check (n "T-Crossing" + (js [("a", sq 1)] cr (TTangle (qq, qq))) []))); + + let mkweave ins body outs = + let st nm = { strand_name = nm; strand_type = Some "Q" } in + Weave { weave_inputs = List.map st ins; + weave_body = body; + weave_outputs = List.map st outs } in + + test "honest: a permutation weave derives and checks" (fun () -> + ok (check (derive [] (mkweave ["a"; "b"] cr ["b"; "a"])))); + + (* The graph cannot launder a linearity violation: T-Weave re-runs the same + strand check the typechecker does. *) + test "forged: weave node duplicating a strand is rejected" (fun () -> + let bad = mkweave ["a"; "b"] cr ["a"; "b"; "a"] in + rejected (check (n "T-Weave" (j [] bad (TTangle (qq, qq @ [StrandNamed "Q"]))) []))); + + test "forged: weave node dropping a strand is rejected" (fun () -> + let bad = mkweave ["a"; "b"] cr ["a"] in + rejected (check (n "T-Weave" (j [] bad (TTangle (qq, [StrandNamed "Q"]))) []))); + + Printf.printf "\n=== Coverage: the remaining hole is reported, not hidden ===\n"; + + test "a fully-derived ordinary program leaves NO unchecked nodes" (fun () -> + (* Exercises T-Let, T-Var, T-Mirror, T-Braid and T-Close in one graph — + four of the five were deferred until now. *) + let prog = Let ("x", w2, Close (Mirror (Var "x"))) in + let d = derive [] prog in + ok (check d) && unchecked d = []); + + test "T-Add-Block is reported as unchecked rather than silently accepted" (fun () -> + let d = n "T-Add-Block" (j [] (IntLit 0) TNum) [] in + (* it does not FAIL the check ... *) + ok (check d) + (* ... but it is visibly not re-derived *) + && List.map fst (unchecked d) = ["T-Add-Block"]); + + test "an unknown rule name is still an error, not an unchecked node" (fun () -> + rejected (check (n "T-Nonsense" (j [] (IntLit 0) TNum) []))); + Printf.printf "\n=== Rendering ===\n"; test "to_string shows rule names and judgements" (fun () ->