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 () ->