From c21714a65a3032cd20b6216409f58d770a25acb1 Mon Sep 17 00:00:00 2001 From: jasisz Date: Fri, 25 Sep 2026 22:36:32 +0200 Subject: [PATCH 1/2] cert: certify a match on a List The plan grammar gains the two List patterns, `[]` and `[head, ..tail]`, and the two-arm List match the emitter lowers: both arms in either order, or either one first and `_` second. The wall ports `emit_mir_list_match` (stash the subject, `ref.is_null`, the `[]` arm in `then`, the head and tail read from the cons struct into the arm's binders in `else`) and proves the case in `agreement_step`, so a function that matches on a List, recursive ones included, is certified for the bytes already emitted. No helper, no new runtime contract, no schema change; the wall id rotates. The producer prints the patterns and carries the Rust twins of the arm pick, the typing and the lowering. Four hardening tests: the clean List certificate checks, and exchanged arm results, exchanged cons structs and exchanged head and tail slots decline. The ratchet records 54 gains and no loss; btc-listener goes from 632 to 765 certified exports. Co-Authored-By: Claude Opus 5.5 (1M context) --- CHANGELOG.md | 4 + aver-cert/assets/wall/current/Grammar.lean | 56 ++++- .../assets/wall/current/GrammarLower.lean | 26 +++ .../assets/wall/current/GrammarSound.lean | 195 +++++++++++++++++- aver-cert/src/engine/plan.rs | 6 + aver-cert/src/engine/plan_check.rs | 50 +++++ aver-cert/src/format.rs | 2 +- docs/certificate-format.md | 6 +- docs/certification.md | 4 +- src/codegen/cert/plan_from_mir.rs | 16 +- tests/cert_certify_spec.rs | 43 ++-- tests/cert_hardening_spec.rs | 139 ++++++++++++- tests/cert_verify_spec.rs | 7 +- ...ify_spec__add_one_certificate_package.snap | 2 +- ..._wasip2_component_certificate_package.snap | 2 +- tools/cert-baseline.json | 54 +++++ 16 files changed, 568 insertions(+), 44 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 9f529eee7..93f796309 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,6 +4,10 @@ All notable changes to Aver are documented here. Starting with 0.10.0, minor rel ## Unreleased +### Added — certificates for a match on a List + +- **A function that matches on a List can now be certified.** `match xs` with a `[]` arm and a `[head, ..tail]` arm, in either order, or one of them followed by `_`, used to leave the function source-level only. Such a function now gets a certificate for the bytes the compiler already emits, recursive ones included (`count(rest)` on the tail). On the btc-listener corpus this certifies 133 more functions, and 160 more across the examples, projects and certificate fixtures. A List argument has no source-bridge encoder yet, so these functions are certified against their plan and carry no bridge. The wall identity rotates: packages produced by earlier versions must be produced again. + ### Added — literal, constructor and list patterns at any depth - **A constructor pattern takes patterns in its fields.** `Option.Some(0)`, `Result.Ok("x")`, `Result.Err(404)`, `Shape.Rect(0, h)`, `Option.Some(true)`, `Option.Some(Option.None)` and `Option.Some((0, _))` are patterns now; before, each field had to be a name or `_`. The literals are the ones a top-level arm accepts: `Int`, `String`, `Float` and `Bool`. diff --git a/aver-cert/assets/wall/current/Grammar.lean b/aver-cert/assets/wall/current/Grammar.lean index c9d52eee0..edc8d6971 100644 --- a/aver-cert/assets/wall/current/Grammar.lean +++ b/aver-cert/assets/wall/current/Grammar.lean @@ -57,13 +57,15 @@ the struct index and the default filler. * `match_ subject arms` — `Match`, the arms 1:1 (`MirMatchArm` pattern and body). Patterns: `wild`, `litInt`, `litBool`, `litStr`, `bind slot`, - `ctor c bindings`, `tuple bindings` (the bindings are the resolver - slots, `noSlot` for `_`). The typing admits exactly the arm shapes the - emitter lowers with first-match meaning: an Int literal cascade with a - catch-all last, a two-arm Bool match, the two-arm Option / Result tag - dispatch, a user variant `ref.test` cascade of two or more arms that - covers every constructor, a String literal cascade with `_` last, and - the single-arm flat tuple destructure. + `ctor c bindings`, `tuple bindings`, `emptyList`, `cons head tail` (the + bindings are the resolver slots, `noSlot` for `_`). The typing admits + exactly the arm shapes the emitter lowers with first-match meaning: an + Int literal cascade with a catch-all last, a two-arm Bool match, the + two-arm Option / Result tag dispatch, a user variant `ref.test` cascade + of two or more arms that covers every constructor, a String literal + cascade with `_` last, the single-arm flat tuple destructure, and the + two-arm List match (`[]` and `[head, ..tail]` in either order, or + either one first with `_` second). Values: `SVal` has nested records (`record tid fields`; a one-field record is a newtype, represented as its field's value), user variants (`variant @@ -179,6 +181,11 @@ inductive Pat where | litStr (bytes : List Nat) /-- A flat tuple destructure: one slot per component (`noSlot` for `_`). -/ | tuple (bindings : List Nat) + /-- `EmptyList`, the `[]` arm of a List match. -/ + | emptyList + /-- `Cons`, the `[head, ..tail]` arm of a List match: the head and tail + slots (`noSlot` for `_`). -/ + | cons (head tl : Nat) deriving DecidableEq, Repr mutual @@ -371,6 +378,17 @@ def resPick : Pat → Pat → Option (Bool × Nat × Nat) | .ctor .err [b], .wild => some (true, noSlot, b) | _, _ => none +/-- The emitter's List arm pick (`emit_mir_list_match`) for the admitted + shapes: `(swap, head, tail)`, where `swap` says the cons arm is the first + one. A `_` stands for the arm the other one leaves (it is never first, so + the pick is first-match). -/ +def listPick : Pat → Pat → Option (Bool × Nat × Nat) + | .emptyList, .cons h tl => some (false, h, tl) + | .emptyList, .wild => some (false, noSlot, noSlot) + | .cons h tl, .emptyList => some (true, h, tl) + | .cons h tl, .wild => some (true, h, tl) + | _, _ => none + /-- The fused `Option.withDefault(Vector.get(v, i), )` shape (`emit_mir_option_with_default`): the vector and index slots when the vector and the index are bare locals. Any other operand shape is @@ -554,6 +572,7 @@ mutual else none | some .string => tyStrArms M n Γ tail arms | some (.record tid) => tyTupArms M n Γ tail tid arms + | some (.list t) => tyListArms M n Γ tail t arms | _ => none def tysOf (M : MCtx) (n : Nat) (Γ : Nat → Option Ty) : List Expr → Option (List Ty) | [] => some [] @@ -682,6 +701,27 @@ mutual else none | none => none | _ => none + /-- Two-arm List match (`listPick` shapes): the cons arm binds its head at + the element type and its tail at the list type, both fresh. -/ + def tyListArms (M : MCtx) (n : Nat) (Γ : Nat → Option Ty) (tail : Bool) (t : Ty) : + Arms → Option Ty + | .cons p1 b1 (.cons p2 b2 .nil) => + match listPick p1 p2 with + | some (swap, h, tl) => + match bindTys n Γ [h, tl] [t, .list t] with + | some Γc => + match swap with + | false => + match tyOf M n Γ tail b1, tyOf M n Γc tail b2 with + | some a, some b => if a = b then some a else none + | _, _ => none + | true => + match tyOf M n Γc tail b1, tyOf M n Γ tail b2 with + | some a, some b => if a = b then some a else none + | _, _ => none + | none => none + | none => none + | _ => none end /-! ## Source values -/ @@ -839,6 +879,8 @@ def patMatch : Pat → SVal → Option (List Nat × List SVal) | .ctor .err bs, .err _ _ v => some (bs, [v]) | .litStr k, .s x => if x = k then some ([], []) else none | .tuple bs, .record _ fs => some (bs, fs) + | .emptyList, .nil _ => some ([], []) + | .cons h tl, .cons _ x r => some ([h, tl], [x, r]) | _, _ => none /-- Bind the binders in order, skipping `noSlot`; `none` on a length diff --git a/aver-cert/assets/wall/current/GrammarLower.lean b/aver-cert/assets/wall/current/GrammarLower.lean index 53d404538..582d9e8dd 100644 --- a/aver-cert/assets/wall/current/GrammarLower.lean +++ b/aver-cert/assets/wall/current/GrammarLower.lean @@ -47,6 +47,10 @@ with `ref.cast` + `struct.get` (`emit_mir_tuple_match`); * `[]` is `ref.null` of the list's cons struct, `List.prepend` is `struct.new` of it; + * a List `Match` stashes the subject and tests it with `ref.is_null`: the + `[]` arm in `then`, and in `else` the head (field 0) and tail (field 1) + binders, each by `ref.cast` + `struct.get`, then the cons arm + (`emit_mir_list_match`); * the fused `Vector.get`-or-default re-reads the vector and the index locals, converts the index through `__aint_to_index`, and bounds-checks it signed `>= 0` and unsigned `< array.len` before `array.get`; @@ -433,6 +437,9 @@ mutual | some (.record tid) => lowerB M X Γ false s ++ [.op (.localSet X.subj)] ++ lowerTupArms M X Γ tail tid arms + | some (.list t) => + lowerB M X Γ false s ++ [.op (.localSet X.subj)] ++ + lowerListArms M X Γ tail (tyOf M X.n Γ tail (.match_ s arms)) t arms | _ => [] | .interp parts => lowerArgsB M X Γ parts ++ concatB M parts.length | .list t _ => [.nullOf (M.listStruct t)] @@ -542,6 +549,25 @@ mutual extractB X.subj (M.structOf tid) 0 bs ++ lowerB M X (((M.recFields tid).bind (bindTys X.n Γ bs)).getD Γ) tail b | _ => [] + /-- `emit_mir_list_match`, the subject already in the subject scratch: + `ref.is_null` picks the `[]` arm; otherwise the head and tail binders + are read from the cons struct, then the cons arm runs. -/ + def lowerListArms (M : MCtx) (X : LCtx) (Γ : Nat → Option Ty) (tail : Bool) + (bt : Option Ty) (t : Ty) : Arms → List BI + | .cons p1 b1 (.cons p2 b2 _) => + match listPick p1 p2 with + | some (false, h, tl) => + [.op (.localGet X.subj), .op .refIsNull, + .ifElse bt (lowerB M X Γ tail b1) + (extractB X.subj (M.listStruct t) 0 [h, tl] ++ + lowerB M X ((bindTys X.n Γ [h, tl] [t, .list t]).getD Γ) tail b2)] + | some (true, h, tl) => + [.op (.localGet X.subj), .op .refIsNull, + .ifElse bt (lowerB M X Γ tail b2) + (extractB X.subj (M.listStruct t) 0 [h, tl] ++ + lowerB M X ((bindTys X.n Γ [h, tl] [t, .list t]).getD Γ) tail b1)] + | none => [] + | _ => [] end /-- The instructions the interpreter runs. -/ diff --git a/aver-cert/assets/wall/current/GrammarSound.lean b/aver-cert/assets/wall/current/GrammarSound.lean index b59325eeb..d602f93fd 100644 --- a/aver-cert/assets/wall/current/GrammarSound.lean +++ b/aver-cert/assets/wall/current/GrammarSound.lean @@ -1398,7 +1398,8 @@ theorem tyOf_match_inv {s : Expr} {arms : Arms} {T : Ty} (∃ tid, Ts = .sum tid ∧ sumOk M tid = true ∧ varExhaustive M tid arms = true ∧ 2 ≤ arms.length ∧ tyVarArms M n Γ tail tid arms = some T) ∨ (Ts = .string ∧ tyStrArms M n Γ tail arms = some T) ∨ - (∃ tid, Ts = .record tid ∧ tyTupArms M n Γ tail tid arms = some T)) := by + (∃ tid, Ts = .record tid ∧ tyTupArms M n Γ tail tid arms = some T) ∨ + (∃ t, Ts = .list t ∧ tyListArms M n Γ tail t arms = some T)) := by simp only [tyOf] at h split at h · rename_i hs @@ -1421,7 +1422,9 @@ theorem tyOf_match_inv {s : Expr} {arms : Arms} {T : Ty} · rename_i hs exact ⟨_, hs, Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inl ⟨rfl, h⟩)))))⟩ · rename_i tid hs - exact ⟨_, hs, Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr ⟨tid, rfl, h⟩)))))⟩ + exact ⟨_, hs, Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inl ⟨tid, rfl, h⟩))))))⟩ + · rename_i t hs + exact ⟨_, hs, Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr ⟨t, rfl, h⟩))))))⟩ · cases h end TypingInv @@ -1499,9 +1502,92 @@ theorem resPick_spec {p1 p2 : Pat} {swap : Bool} {ob eb : Nat} unfold resPick at h split at h <;> simp_all +theorem listPick_spec {p1 p2 : Pat} {swap : Bool} {hd tl : Nat} + (h : listPick p1 p2 = some (swap, hd, tl)) : + (swap = false ∧ p1 = .emptyList ∧ + (p2 = .cons hd tl ∨ (p2 = .wild ∧ hd = noSlot ∧ tl = noSlot))) ∨ + (swap = true ∧ p1 = .cons hd tl ∧ (p2 = .emptyList ∨ p2 = .wild)) := by + cases p1 <;> cases p2 <;> simp [listPick] at h <;> obtain ⟨rfl, rfl, rfl⟩ := h <;> simp + +/-- The typing of a List match fixes its shape: two arms, a `listPick` + shape, fresh head and tail binders, and one type for both bodies. -/ +theorem tyListArms_shape {M : MCtx} {n : Nat} {Γ : Nat → Option Ty} {tail : Bool} {t : Ty} + {arms : Arms} {T : Ty} (h : tyListArms M n Γ tail t arms = some T) : + ∃ p1 b1 p2 b2 swap hd tl Γc, arms = .cons p1 b1 (.cons p2 b2 .nil) ∧ + listPick p1 p2 = some (swap, hd, tl) ∧ + bindTys n Γ [hd, tl] [t, .list t] = some Γc ∧ + tyOf M n Γ tail (if swap then b2 else b1) = some T ∧ + tyOf M n Γc tail (if swap then b1 else b2) = some T := by + match arms, h with + | .nil, h => simp [tyListArms] at h + | .cons _ _ .nil, h => simp [tyListArms] at h + | .cons _ _ (.cons _ _ (.cons _ _ _)), h => simp [tyListArms] at h + | .cons p1 b1 (.cons p2 b2 .nil), h => + simp only [tyListArms] at h + cases hpk : listPick p1 p2 with + | none => simp [hpk] at h + | some pr => + obtain ⟨swap, hd, tl⟩ := pr + simp only [hpk] at h + cases hb : bindTys n Γ [hd, tl] [t, .list t] with + | none => simp [hb] at h + | some Γc => + simp only [hb] at h + cases swap with + | false => + simp only at h + cases h1 : tyOf M n Γ tail b1 with + | none => simp [h1] at h + | some a => + cases h2 : tyOf M n Γc tail b2 with + | none => simp [h1, h2] at h + | some c => + simp only [h1, h2] at h + by_cases hac : a = c + · subst hac + simp only [↓reduceIte, Option.some.injEq] at h + subst h + exact ⟨p1, b1, p2, b2, false, hd, tl, Γc, rfl, hpk, hb, + by simpa using h1, by simpa using h2⟩ + · simp [hac] at h + | true => + simp only at h + cases h1 : tyOf M n Γc tail b1 with + | none => simp [h1] at h + | some a => + cases h2 : tyOf M n Γ tail b2 with + | none => simp [h1, h2] at h + | some c => + simp only [h1, h2] at h + by_cases hac : a = c + · subst hac + simp only [↓reduceIte, Option.some.injEq] at h + subst h + exact ⟨p1, b1, p2, b2, true, hd, tl, Γc, rfl, hpk, hb, + by simpa using h2, by simpa using h1⟩ + · simp [hac] at h + section ShapeEval variable (F : Nat → List SVal → Option SVal) (env : Nat → Option SVal) +/-- The List shapes pick the `[]` arm for the empty list. -/ +theorem evalList_nil {p1 p2 : Pat} {b1 b2 : Expr} {swap : Bool} {hd tl : Nat} {t : Ty} + (h : listPick p1 p2 = some (swap, hd, tl)) : + evalArms F env (.nil t) (.cons p1 b1 (.cons p2 b2 .nil)) = + eval F env (if swap then b2 else b1) := by + rcases listPick_spec h with ⟨rfl, rfl, rfl | ⟨rfl, rfl, rfl⟩⟩ | ⟨rfl, rfl, rfl | rfl⟩ <;> + simp [evalArms, patMatch, bindVals] + +/-- The List shapes pick the cons arm for a cons cell, binding head and tail. -/ +theorem evalList_cons {p1 p2 : Pat} {b1 b2 : Expr} {swap : Bool} {hd tl : Nat} {t : Ty} + {x r : SVal} (h : listPick p1 p2 = some (swap, hd, tl)) : + evalArms F env (.cons t x r) (.cons p1 b1 (.cons p2 b2 .nil)) = + match bindVals env [hd, tl] [x, r] with + | some env' => eval F env' (if swap then b1 else b2) + | none => none := by + rcases listPick_spec h with ⟨rfl, rfl, rfl | ⟨rfl, rfl, rfl⟩⟩ | ⟨rfl, rfl, rfl | rfl⟩ <;> + simp [evalArms, patMatch, bindVals, noSlot] <;> rfl + /-- The Option shapes pick the `Some` arm for a `Some` value, binding `sb`. -/ theorem evalOpt_some {p1 p2 : Pat} {b1 b2 : Expr} {swap : Bool} {sb : Nat} {t : Ty} {x : SVal} (h : optPick p1 p2 = some (swap, sb)) : @@ -1552,6 +1638,21 @@ theorem run_localSet (host : HostTbl) (ar : Nat → Option Nat) (callee : Callee wRunF host ar callee ys (wl.set j w) st := by simp [wRunF] +/-- `ref.is_null` on a stashed List subject: `[]` is `null`, a cons cell a + struct. -/ +theorem run_nullTest_null (host : HostTbl) (ar : Nat → Option Nat) (callee : Callee) + (ss : Nat) (ys : List WInstr) (wl st : List WVal) (h : wl[ss]? = some .null) : + wRunF host ar callee (.localGet ss :: .refIsNull :: ys) wl st = + wRunF host ar callee ys wl (b32 true :: st) := by + simp [wRunF, h] + +theorem run_nullTest_struct (host : HostTbl) (ar : Nat → Option Nat) (callee : Callee) + (ss ty : Nat) (fs : List WVal) (ys : List WInstr) (wl st : List WVal) + (h : wl[ss]? = some (.structv ty fs)) : + wRunF host ar callee (.localGet ss :: .refIsNull :: ys) wl st = + wRunF host ar callee ys wl (b32 false :: st) := by + simp [wRunF, h] + /-! ## Reading back a stashed scratch local A scratch local need not exist (`LRel` does not demand it). Every template @@ -2639,7 +2740,7 @@ theorem agreement_step : | .match_ s arms, hsz, Γ, env, tail, T, wl, st, out, hty, henv, hl, hrun => by obtain ⟨Ts, hts, hcases⟩ := tyOf_match_inv hty rcases hcases with ⟨rfl, hfl, hta⟩ | ⟨rfl, hta⟩ | ⟨t, rfl, hta⟩ | ⟨t, e, rfl, hta⟩ | - ⟨tid, rfl, hok, hex, hlen2, hta⟩ | ⟨rfl, hta⟩ | ⟨tid, rfl, hta⟩ + ⟨tid, rfl, hok, hex, hlen2, hta⟩ | ⟨rfl, hta⟩ | ⟨tid, rfl, hta⟩ | ⟨t, rfl, hta⟩ · -- Int literal cascade: the subject is re-run per arm simp only [lowerW, lowerB, hts] at hrun obtain ⟨ys, hys⟩ := lowerIntArms_firstLit M X Γ tail (lowerB M X Γ false s) @@ -2767,6 +2868,86 @@ theorem agreement_step : agreementTupArms arms Γ env tail T _ st out tid fs ws fts hss hws hR hfs hta henv (lrel_set_free _ hl1 hl1.1.2.1) hseq exact ⟨sv, by simp [eval, hev1, hev], hT, hres⟩ + · -- List: stash, `ref.is_null`, then the head and tail binders + obtain ⟨p1, b1, p2, b2, swap, hd, tl, Γc, rfl, hpk, hbt, hte, htc⟩ := + tyListArms_shape hta + simp only [lowerW, lowerB, hts, eraseL_append, List.append_assoc] at hrun + obtain ⟨o1, h1, hseq⟩ := run_split hrun + obtain ⟨sv1, hev1, hT1, hres1⟩ := + agreement s Γ env false (.list t) wl st o1 hts henv hl h1 + obtain ⟨wl1, w1, rfl, hw1, hl1⟩ := res_false hres1 + simp only [seqOut, eraseL, eraseI, List.cons_append, List.nil_append] at hseq + rw [run_localSet] at hseq + have hl2 := lrel_set_free (X := X) w1 hl1 hl1.1.2.1 + cases swap with + | false => + simp only [Bool.false_eq_true, ↓reduceIte] at hte htc + simp only [lowerListArms, hpk, hbt, Option.getD_some, eraseL, eraseI] at hseq + have hss := stash_read rfl hseq + rcases hasTy_list hT1 with rfl | ⟨x, r, rfl, hx, hr⟩ + · simp only [SRepr] at hw1 + subst hw1 + rw [run_nullTest_null host ar callee _ _ _ _ hss] at hseq + simp only [b32, ↓reduceIte] at hseq + rw [wRunF_ifElse_single] at hseq + simp only [Int.reduceEq, ↓reduceIte] at hseq + obtain ⟨sv, hev, hT, hres⟩ := agreement b1 Γ env tail T _ st out hte henv hl2 hseq + refine ⟨sv, ?_, hT, hres⟩ + have hA := evalList_nil (b1 := b1) (b2 := b2) (t := t) F env hpk + simp only [Bool.false_eq_true, ↓reduceIte] at hA + simp [eval, hev1, hA, hev] + · simp only [SRepr] at hw1 + obtain ⟨xw, rw', rfl, hxw, hrw⟩ := hw1 + rw [run_nullTest_struct host ar callee _ _ _ _ _ _ hss] at hseq + simp only [b32, ↓reduceIte] at hseq + rw [wRunF_ifElse_single] at hseq + simp only [↓reduceIte, eraseL_append] at hseq + obtain ⟨env', wl', hbv, henv', hl', _, hrun', hres'⟩ := + extract_run host ar callee X.subj (M.listStruct t) [xw, rw'] [hd, tl] 0 [x, r] + [t, .list t] [xw, rw'] env Γ Γc _ st hl1.1.2.1 hss + (fun j y hy => by simpa using hy) ⟨hx, hr, trivial⟩ ⟨hxw, hrw, trivial⟩ hbt + henv hl2 + rw [run_seq_eq hrun'] at hseq + obtain ⟨sv, hev, hT, hres⟩ := + agreement b2 Γc env' tail T wl' st out htc henv' hl' hseq + refine ⟨sv, ?_, hT, hres' _ _ _ _ hres⟩ + have hA := evalList_cons (b1 := b1) (b2 := b2) (x := x) (r := r) (t := t) F env hpk + simp only [Bool.false_eq_true, ↓reduceIte, hbv] at hA + simp [eval, hev1, hA, hev] + | true => + simp only [↓reduceIte] at hte htc + simp only [lowerListArms, hpk, hbt, Option.getD_some, eraseL, eraseI] at hseq + have hss := stash_read rfl hseq + rcases hasTy_list hT1 with rfl | ⟨x, r, rfl, hx, hr⟩ + · simp only [SRepr] at hw1 + subst hw1 + rw [run_nullTest_null host ar callee _ _ _ _ hss] at hseq + simp only [b32, ↓reduceIte] at hseq + rw [wRunF_ifElse_single] at hseq + simp only [Int.reduceEq, ↓reduceIte] at hseq + obtain ⟨sv, hev, hT, hres⟩ := agreement b2 Γ env tail T _ st out hte henv hl2 hseq + refine ⟨sv, ?_, hT, hres⟩ + have hA := evalList_nil (b1 := b1) (b2 := b2) (t := t) F env hpk + simp only [↓reduceIte] at hA + simp [eval, hev1, hA, hev] + · simp only [SRepr] at hw1 + obtain ⟨xw, rw', rfl, hxw, hrw⟩ := hw1 + rw [run_nullTest_struct host ar callee _ _ _ _ _ _ hss] at hseq + simp only [b32, ↓reduceIte] at hseq + rw [wRunF_ifElse_single] at hseq + simp only [↓reduceIte, eraseL_append] at hseq + obtain ⟨env', wl', hbv, henv', hl', _, hrun', hres'⟩ := + extract_run host ar callee X.subj (M.listStruct t) [xw, rw'] [hd, tl] 0 [x, r] + [t, .list t] [xw, rw'] env Γ Γc _ st hl1.1.2.1 hss + (fun j y hy => by simpa using hy) ⟨hx, hr, trivial⟩ ⟨hxw, hrw, trivial⟩ hbt + henv hl2 + rw [run_seq_eq hrun'] at hseq + obtain ⟨sv, hev, hT, hres⟩ := + agreement b1 Γc env' tail T wl' st out htc henv' hl' hseq + refine ⟨sv, ?_, hT, hres' _ _ _ _ hres⟩ + have hA := evalList_cons (b1 := b1) (b2 := b2) (x := x) (r := r) (t := t) F env hpk + simp only [↓reduceIte, hbv] at hA + simp [eval, hev1, hA, hev] | .interp parts, hsz, Γ, env, tail, T, wl, st, out, hty, henv, hl, hrun => by obtain ⟨ts, hts, hall, rfl⟩ := tyOf_interp_inv hty simp only [lowerW, lowerB, eraseL_append] at hrun @@ -2914,6 +3095,8 @@ theorem agreementIntArms_step : | ctor _ _ => simp [tyIntArms] at hty | litStr _ => simp [tyIntArms] at hty | tuple _ => simp [tyIntArms] at hty + | emptyList => simp [tyIntArms] at hty + | cons _ _ => simp [tyIntArms] at hty theorem agreementBoolArms_step : ∀ (arms : Arms) (hsz : sizeOf arms < n + 1) (Γ : Nat → Option Ty) (env : Nat → Option SVal) (tail : Bool) (T : Ty) @@ -2976,6 +3159,8 @@ theorem agreementBoolArms_step : | ctor _ _ => simp [tyBoolArms] at hty | litStr _ => simp [tyBoolArms] at hty | tuple _ => simp [tyBoolArms] at hty + | emptyList => simp [tyBoolArms] at hty + | cons _ _ => simp [tyBoolArms] at hty theorem agreementOptArms_step : ∀ (arms : Arms) (hsz : sizeOf arms < n + 1) (Γ : Nat → Option Ty) (env : Nat → Option SVal) (tail : Bool) (T : Ty) @@ -3268,6 +3453,8 @@ theorem agreementVarArms_step : | bind _ => simp [varArmΓ] at hva | litStr _ => simp [varArmΓ] at hva | tuple _ => simp [varArmΓ] at hva + | emptyList => simp [varArmΓ] at hva + | cons _ _ => simp [varArmΓ] at hva | .cons p b (.cons p' b' r), hsz, Γ, env, tail, T, wl, st, out, bt, tid, cv, fs, ws, fts, hss, hws, hcf, hfs, hcov, hinj, hty, henv, hl, hrun => by simp only [tyVarArms] at hty @@ -3347,6 +3534,8 @@ theorem agreementVarArms_step : | bind _ => simp [varArmΓ] at hty | litStr _ => simp [varArmΓ] at hty | tuple _ => simp [varArmΓ] at hty + | emptyList => simp [varArmΓ] at hty + | cons _ _ => simp [varArmΓ] at hty theorem agreementStrArms_step : ∀ (arms : Arms) (hsz : sizeOf arms < n + 1) (Γ : Nat → Option Ty) (env : Nat → Option SVal) (tail : Bool) (T : Ty) diff --git a/aver-cert/src/engine/plan.rs b/aver-cert/src/engine/plan.rs index d94a48753..1b4bf7adb 100644 --- a/aver-cert/src/engine/plan.rs +++ b/aver-cert/src/engine/plan.rs @@ -106,6 +106,10 @@ pub enum PlanPat { Ctor(PlanCtor, Vec), LitStr(Vec), Tuple(Vec), + /// `[]`. + EmptyList, + /// `[head, ..tail]`: the head and tail slots. + Cons(u32, u32), } /// `Grammar.Expr`; `Match` arms are `Grammar.Arms` in source order. @@ -326,6 +330,8 @@ impl PlanPat { PlanPat::Ctor(c, bs) => format!("(.ctor {} {})", c.lean(), lean_nat_list(bs)), PlanPat::LitStr(bytes) => format!("(.litStr {})", lean_bytes(bytes)), PlanPat::Tuple(bs) => format!("(.tuple {})", lean_nat_list(bs)), + PlanPat::EmptyList => ".emptyList".into(), + PlanPat::Cons(h, t) => format!("(.cons {h} {t})"), } } } diff --git a/aver-cert/src/engine/plan_check.rs b/aver-cert/src/engine/plan_check.rs index d8cb0afc6..782d114e7 100644 --- a/aver-cert/src/engine/plan_check.rs +++ b/aver-cert/src/engine/plan_check.rs @@ -254,6 +254,17 @@ fn res_pick(p1: &PlanPat, p2: &PlanPat) -> Option<(bool, u32, u32)> { } } +/// `Grammar.listPick`: `(swap, head, tail)`, `swap` when the cons arm is +/// first. +fn list_pick(p1: &PlanPat, p2: &PlanPat) -> Option<(bool, u32, u32)> { + match (p1, p2) { + (PlanPat::EmptyList, PlanPat::Cons(h, t)) => Some((false, *h, *t)), + (PlanPat::EmptyList, PlanPat::Wild) => Some((false, PLAN_NO_SLOT, PLAN_NO_SLOT)), + (PlanPat::Cons(h, t), PlanPat::EmptyList | PlanPat::Wild) => Some((true, *h, *t)), + _ => None, + } +} + /// `Grammar.vecGetOr?`. fn vec_get_or(lb: PlanLazy, o: &PlanExpr, d: &PlanExpr) -> Option<(u32, u32)> { match (lb, o, d) { @@ -474,6 +485,7 @@ impl MCtx<'_> { } PlanTy::Str => self.ty_str_arms(n, g, tail, arms), PlanTy::Record(tid) => self.ty_tup_arms(n, g, tail, tid, arms), + PlanTy::List(t) => self.ty_list_arms(n, g, tail, &t, arms), _ => None, }, } @@ -635,6 +647,27 @@ impl MCtx<'_> { } } + fn ty_list_arms( + &self, + n: u32, + g: &Gamma, + tail: bool, + t: &PlanTy, + arms: &[(PlanPat, PlanExpr)], + ) -> Option { + let [(p1, b1), (p2, b2)] = arms else { + return None; + }; + let (swap, h, tl) = list_pick(p1, p2)?; + let gc = bind_tys(n, g, &[h, tl], &[t.clone(), PlanTy::List(Box::new(t.clone()))])?; + let (a, b) = if swap { + (self.ty_of(n, &gc, tail, b1)?, self.ty_of(n, g, tail, b2)?) + } else { + (self.ty_of(n, g, tail, b1)?, self.ty_of(n, &gc, tail, b2)?) + }; + (a == b).then_some(a) + } + fn ty_tup_arms( &self, n: u32, @@ -1300,6 +1333,23 @@ impl MCtx<'_> { } out } + Some(PlanTy::List(t)) => { + let mut out = sc; + out.push(BI::Op(WI::LocalSet(x.subj))); + if let [(p1, b1), (p2, b2), ..] = arms.as_slice() + && let Some((swap, h, tl)) = list_pick(p1, p2) + { + let (empty_b, cons_b) = if swap { (b2, b1) } else { (b1, b2) }; + let lt = PlanTy::List(t.clone()); + let gc = bind_tys(n, g, &[h, tl], &[(*t).clone(), lt]) + .unwrap_or_else(|| g.clone()); + let mut else_b = extract(x.subj, self.list_struct(&t), &[h, tl]); + else_b.extend(self.lower(x, &gc, tail, cons_b)); + out.extend(ops(vec![WI::LocalGet(x.subj), WI::RefIsNull])); + out.push(BI::If(bt, self.lower(x, g, tail, empty_b), else_b)); + } + out + } _ => vec![], } } diff --git a/aver-cert/src/format.rs b/aver-cert/src/format.rs index e39d66fdb..6540755c8 100644 --- a/aver-cert/src/format.rs +++ b/aver-cert/src/format.rs @@ -180,7 +180,7 @@ pub const FN_CLAIM_DISCHARGE_THEOREM: &str = "AcceptanceSoundness.fn_claim_disch /// Identity of the exact checker-owned Lean wall shipped by this release. pub const CURRENT_WALL_ID: &str = - "sha256:ed89b143414bdff0bfadb49a49bc1e7d8c537365b69549c65f7e82fbccf73cef"; + "sha256:5168df0c3f4da023c53a9c929e081803c559ed2e22fc6a103f8fb827745ae4d9"; /// Complete host-import surface admitted by the wasm-gc certificate format. /// diff --git a/docs/certificate-format.md b/docs/certificate-format.md index 80429c5b4..f846521ee 100644 --- a/docs/certificate-format.md +++ b/docs/certificate-format.md @@ -29,7 +29,7 @@ Schema history, one line per bump. Each bump is exact-match, so a verifier of ve - 8: the `sourceBridges` array and the `bridges` key of every law entry. - 9: every obligation is stated over one plan grammar. The Lean manifest carries one plan list (`fnPlans`), each entry a function's optimized MIR body printed 1:1, and a declared type layout (`types`) that the wall confirms against the type and data sections. The obligations are exactly the ones the wall derives from the plans, and their model is the plan's fuel-indexed meaning. Every certified export reports the class `source-plan-v1` with wall-derived facets. `hostRoleTable` gained the `divmod` key. Source-bridges are restated over the plan grammar, in two statement kinds (section 9). -The wall identity is computed, not assigned. It is the SHA-256 of a domain-separated, sorted, length-framed encoding of every wall source file plus the toolchain pin, written as `sha256:` and 64 lowercase hex digits. The encoding is: the ASCII bytes `aver-certificate-wall\0v1\0`; the file count as a big-endian `u64`; then, for each file in ascending filename order, the filename length as a big-endian `u64`, the filename bytes, the contents length as a big-endian `u64`, and the contents. The file set is the 24 embedded `.lean` wall sources plus one synthetic file named `lean-toolchain`, whose contents are the embedded toolchain file verbatim: the ASCII bytes `leanprover/lean4:v4.34.0` and one trailing newline. The newline is hashed; a reimplementation that hashes the trimmed pin computes a different identity. The current embedded wall identity is `sha256:ed89b143414bdff0bfadb49a49bc1e7d8c537365b69549c65f7e82fbccf73cef` (`CURRENT_WALL_ID` in `format.rs`). The reference verifier recomputes the digest over its embedded sources on first use and aborts if it differs from the compiled-in constant. A reimplementation MUST resolve `format.wall_id` only against source sets whose recomputed identity matches byte for byte, never by name, path or prefix. +The wall identity is computed, not assigned. It is the SHA-256 of a domain-separated, sorted, length-framed encoding of every wall source file plus the toolchain pin, written as `sha256:` and 64 lowercase hex digits. The encoding is: the ASCII bytes `aver-certificate-wall\0v1\0`; the file count as a big-endian `u64`; then, for each file in ascending filename order, the filename length as a big-endian `u64`, the filename bytes, the contents length as a big-endian `u64`, and the contents. The file set is the 24 embedded `.lean` wall sources plus one synthetic file named `lean-toolchain`, whose contents are the embedded toolchain file verbatim: the ASCII bytes `leanprover/lean4:v4.34.0` and one trailing newline. The newline is hashed; a reimplementation that hashes the trimmed pin computes a different identity. The current embedded wall identity is `sha256:5168df0c3f4da023c53a9c929e081803c559ed2e22fc6a103f8fb827745ae4d9` (`CURRENT_WALL_ID` in `format.rs`). The reference verifier recomputes the digest over its embedded sources on first use and aborts if it differs from the compiled-in constant. A reimplementation MUST resolve `format.wall_id` only against source sets whose recomputed identity matches byte for byte, never by name, path or prefix. > **TODO-decision: freeze criteria.** Neither `format.version = 1` nor `schema_version = 9` is frozen. What counts as a compatible extension, and whether a frozen schema admits additive optional fields, is open. Until a freeze, every schema change bumps `schema_version`, and verifiers reject non-matching versions exactly. @@ -228,7 +228,7 @@ A plan (`Grammar.FnPlan`) is `{sig, nslots, locals, body}`: the signature, the r - `neg`, which the grammar has but the producer declines, because the negation helper has no wall template; - `ifThenElse`; - `recordCreate` with fields in declared order, and `project`, both for records of two or more fields; -- `match_` with the arm shapes the emitter lowers: an Int literal cascade with a catch-all last, a two-arm Bool match, a two-arm Option or Result match, a user-variant `ref.test` cascade of two or more arms covering every constructor, a String literal cascade with `_` last, and a single-arm flat tuple destructure; +- `match_` with the arm shapes the emitter lowers: an Int literal cascade with a catch-all last, a two-arm Bool match, a two-arm Option or Result match, a user-variant `ref.test` cascade of two or more arms covering every constructor, a String literal cascade with `_` last, a single-arm flat tuple destructure, and a two-arm List match (`[]` and `[head, ..tail]` in either order, or either one first and `_` second); - `construct` for user constructors and `Some`, `None`, `Ok`, `Err`, carrying the node's type; - `interp` whose parts are all Strings; - `list t []`, the empty list. @@ -245,7 +245,7 @@ The printer also declines a function that declares effects, uses raw i64 slots, `GrammarLower` is a port of the wasm-gc MIR emitter (`src/codegen/wasm_gc/body/from_mir/`) for the admitted nodes. One lowering produces both the instruction tree the interpreter runs (`fnCode`) and the code-entry bytes the acceptance compares (`codeEntryBytes`, locals vector and size prefix included), so the proved code and the pinned bytes come from one tree. -Every lowering choice is a function of the plan and the declarations, never a plan flag: an Int comparison against a literal looks for the literal on the left first and flips the operator, re-emits a bare local operand and stashes any other operand in the const-compare scratch local; the scratch locals sit after the resolver slots in the order the emitter reserves them; an `if` takes its block type from the then-branch type; a `tailCall` is `return_call` and a `call` is `call`, as MIR marked them. A reimplementation MUST compute both images inside the kernel and MUST NOT replace them with an out-of-kernel lowering. +Every lowering choice is a function of the plan and the declarations, never a plan flag: an Int comparison against a literal looks for the literal on the left first and flips the operator, re-emits a bare local operand and stashes any other operand in the const-compare scratch local; the scratch locals sit after the resolver slots in the order the emitter reserves them; an `if` takes its block type from the then-branch type; a List match tests the stashed subject with `ref.is_null`, runs the `[]` arm in `then`, and reads the head (field 0) and tail (field 1) of the cons struct into the cons arm's binders in `else`; a `tailCall` is `return_call` and a `call` is `call`, as MIR marked them. A reimplementation MUST compute both images inside the kernel and MUST NOT replace them with an out-of-kernel lowering. An index the declarations do not provide lowers to `TypeTable.absent k`, a value outside the u32 range that no encoder accepts, so a plan citing an undeclared type or helper cannot match any code entry. diff --git a/docs/certification.md b/docs/certification.md index 9e1e3aa27..4f37839af 100644 --- a/docs/certification.md +++ b/docs/certification.md @@ -105,9 +105,9 @@ L3 is derived by the wall (`GrammarTotal.checkTermGroup`), never read from a man Every certified export reports one class, `source-plan-v1`, with facets the wall derives from the plan: `recursive`, `mutual`, `calls`, `records`, `variants`, `strings`, `floats`. -The plan grammar is the admitted subset of optimized MIR. It covers Int, Bool, Float and String literals; locals and named `let`; calls to other planned functions, including self and mutual recursion and tail calls; Int `+ - *` and the six comparisons; Bool `and`, `or`, `not`, `==` and `!=`; Float comparisons other than `!=`; String `+`, `==`, `!=` and interpolation of String parts; `if`; records with two or more fields (create in declared order, and project); user variants, `Option` and `Result` (construct and match); matches on Int, Bool and String literals and flat tuple destructuring; `Option.withDefault` and `Result.withDefault`; `Option.withDefault(Vector.get(v, i), )`; `Int.div` and `Int.mod` by a nonzero literal, or fused under `Result.withDefault` with an Int default; the empty list and `List.prepend`. +The plan grammar is the admitted subset of optimized MIR. It covers Int, Bool, Float and String literals; locals and named `let`; calls to other planned functions, including self and mutual recursion and tail calls; Int `+ - *` and the six comparisons; Bool `and`, `or`, `not`, `==` and `!=`; Float comparisons other than `!=`; String `+`, `==`, `!=` and interpolation of String parts; `if`; records with two or more fields (create in declared order, and project); user variants, `Option` and `Result` (construct and match); matches on Int, Bool and String literals, flat tuple destructuring, and a List match on `[]` and `[head, ..tail]`; `Option.withDefault` and `Result.withDefault`; `Option.withDefault(Vector.get(v, i), )`; `Int.div` and `Int.mod` by a nonzero literal, or fused under `Result.withDefault` with an Int default; the empty list and `List.prepend`. -A function is declined, with the MIR node or type named in the reason, when it has effects, uses raw i64 slots, negates an Int (the negation helper has no wall template yet), uses an Int literal outside the i64 range, does Float arithmetic, calls through a function value, matches on a list, or uses any other node outside the subset. A function is also declined when the producer's check finds that its plan does not lower to exactly its code entry. +A function is declined, with the MIR node or type named in the reason, when it has effects, uses raw i64 slots, negates an Int (the negation helper has no wall template yet), uses an Int literal outside the i64 range, does Float arithmetic, calls through a function value, builds a non-empty list literal, calls a `List` helper other than `List.prepend`, or uses any other node outside the subset. A function is also declined when the producer's check finds that its plan does not lower to exactly its code entry. ## Package format diff --git a/src/codegen/cert/plan_from_mir.rs b/src/codegen/cert/plan_from_mir.rs index 3bc31c4a0..013c2ef4a 100644 --- a/src/codegen/cert/plan_from_mir.rs +++ b/src/codegen/cert/plan_from_mir.rs @@ -585,8 +585,8 @@ impl Printer<'_> { }) .collect::>()?, ), - MirPattern::EmptyList => return Err("Match pattern EmptyList".into()), - MirPattern::Cons { .. } => return Err("Match pattern Cons".into()), + MirPattern::EmptyList => PlanPat::EmptyList, + MirPattern::Cons { head, tail, .. } => PlanPat::Cons(head.0, tail.0), }) } @@ -1246,6 +1246,16 @@ fn notLiteral(a: Int, d: Int) -> Int assert_eq!(reason(&map, "neg"), "Neg (no Int negation helper template)"); assert_eq!(reason(&map, "divide"), "BinOp Div"); assert_eq!(reason(&map, "effectful"), "fn declares effects"); - assert_eq!(reason(&map, "lst"), "Match pattern EmptyList"); + } + + #[test] + fn a_list_match_prints_its_two_arms() { + let (map, _) = plans(SRC); + let lst = plan(&map, "lst"); + let PlanExpr::Match(_, arms) = &lst.body else { + panic!("lst body: {:?}", lst.body) + }; + assert_eq!(arms[0].0, PlanPat::EmptyList); + assert!(matches!(arms[1].0, PlanPat::Cons(h, t) if h != PLAN_NO_SLOT && h != t)); } } diff --git a/tests/cert_certify_spec.rs b/tests/cert_certify_spec.rs index 5b56fe928..f48129d4e 100644 --- a/tests/cert_certify_spec.rs +++ b/tests/cert_certify_spec.rs @@ -552,6 +552,14 @@ fn certify_goal_matrix_manifest_tracks_current_surface() { "wrapItems", "a `list` argument has no decoder in this version" ), + ( + "listHeadGoal", + "a `list` argument has no decoder in this version" + ), + ( + "sumListGoal", + "a `list` argument has no decoder in this version" + ), ( "floatLeGoal", "a `float` argument has no decoder in this version" @@ -660,7 +668,7 @@ fn certify_goal_matrix_manifest_tracks_current_surface() { let declared_uncertified = manifest["declaredUncertified"].as_array().unwrap(); assert_eq!( declared_uncertified.len(), - 15, + 13, "all 43 module exports must be certified or explicitly declared" ); assert!(declared_uncertified.iter().all(|entry| { @@ -918,6 +926,10 @@ fn certify_goal_matrix_manifest_tracks_current_surface() { // replaced the families: a bare parameter read is a plan like any // other (numerator moved deliberately). ("idGoal", facets(&[])), + // A List match is a plan: the head read and the recursive sum over the + // tail (numerator moved deliberately). + ("listHeadGoal", facets(&[])), + ("sumListGoal", facets(&["recursive", "calls"])), ] .into_iter() .map(|(name, facets)| (name.to_string(), facets)) @@ -1025,17 +1037,12 @@ fn certify_goal_matrix_manifest_tracks_current_surface() { .into_iter() .map(str::to_string) .collect(); - let expected_backlog: BTreeSet = [ - "floatAddGoal", - "floatMulAddGoal", - "listHeadGoal", - "sumListGoal", - ] - .into_iter() - .map(str::to_string) - .collect(); + let expected_backlog: BTreeSet = ["floatAddGoal", "floatMulAddGoal"] + .into_iter() + .map(str::to_string) + .collect(); assert_eq!(planned_goal_names.len(), 32, "goal denominator changed"); - assert_eq!(actual.len(), 28, "goal numerator changed"); + assert_eq!(actual.len(), 30, "goal numerator changed"); let contracts: Vec<&str> = manifest["runtime_contracts"] .as_array() @@ -1093,8 +1100,6 @@ fn certify_goal_matrix_manifest_tracks_current_surface() { for (name, expected) in [ ("floatAddGoal", "plan does not type in the one grammar"), ("floatMulAddGoal", "plan does not type in the one grammar"), - ("listHeadGoal", "Match pattern EmptyList"), - ("sumListGoal", "Match pattern EmptyList"), ] { let reason = manifest["source_level_only"] .as_array() @@ -1458,7 +1463,7 @@ fn assert_hostile_source_model_loses_bridges(prefix: &str, edits: &[(&str, &str) let (ok, report) = check_certificate(&tampered.join("cert_goals.wasm"), &tampered.join("cert")); assert!( - ok && report.contains("28 checked exports"), + ok && report.contains("30 checked exports"), "a wrong source definition must not touch the export verdict:\n{report}" ); assert!( @@ -2443,7 +2448,6 @@ fn certify_declines_name_the_blocker_that_actually_applies() { for (export, reason) in [ // The printer names the MIR node it has no grammar for. ("finalizeFibStats", "Call Builtin(List.reverse)"), - ("nthOrZero", "Match pattern EmptyList"), ("goldenApprox", "BinOp Div"), ("showGolden", "InterpolatedStr (a part is not a String)"), // A printed plan the one grammar does not type. @@ -2464,8 +2468,9 @@ fn certify_declines_name_the_blocker_that_actually_applies() { ); } // The pure recursions that used to decline on the retired families' - // arity limits are certified plans now. - for name in ["fibTR", "fib", "fibSpec", "bigger"] { + // arity limits are certified plans now, and so is the recursion over a + // List match. + for name in ["fibTR", "fib", "fibSpec", "bigger", "nthOrZero"] { assert!( !declared.contains_key(name), "`{name}` must be certified, not declined: {declared:?}" @@ -2956,8 +2961,8 @@ fn cert_projects_payment_ops_package_checks() { "payment_ops check verdict does not say CHECKED:\n{report}" ); assert!( - report.contains("59 checked exports"), - "payment_ops must keep the fifty-nine exports it certifies:\n{report}" + report.contains("101 checked exports"), + "payment_ops must keep the 101 exports it certifies:\n{report}" ); // The project's single `verify … law` is universal by design but its // emitted proof ladder has no `String.replace` theory and lands on its diff --git a/tests/cert_hardening_spec.rs b/tests/cert_hardening_spec.rs index ac9005269..7039e14a0 100644 --- a/tests/cert_hardening_spec.rs +++ b/tests/cert_hardening_spec.rs @@ -34,7 +34,10 @@ //! function's type index or type, or an export's position; //! * a closure claim hiding a helper, `__aint_divmod` at a supertype //! signature, a renamed `aver:work` import, and a certified closure that -//! reaches a work import. +//! reaches a work import; +//! * a List match whose arm results are exchanged, List cons structs declared +//! for each other's instantiation, and a cons pattern whose head and tail +//! slots are exchanged. //! //! Gated behind `wasm` and skipped when `lake` is unavailable, like the other //! certificate suites. @@ -1399,3 +1402,137 @@ fn cert_hardening_declines_a_bridged_law_that_does_not_use_its_model() { Tiny.addTwo", ); } + +/// A program whose three exports are List matches: `[]` then a cons arm with +/// the head ignored, a cons arm first with the tail ignored, and `[]` then +/// `_`. Each shape lowers to one `ref.is_null` on the stashed subject, the +/// `[]` arm in `then`, and the head and tail binders read from the cons +/// struct in `else`. +const LISTY: &str = "module Listy + intent = \"List match shapes.\" + exposes [count, firstOr, isEmpty] + +fn count(xs: List) -> Int + ? \"Number of elements.\" + match xs + [] -> 0 + [_, ..rest] -> 1 + count(rest) + +fn firstOr(xs: List, d: Int) -> Int + ? \"The head, or the default.\" + match xs + [h, .._] -> h + [] -> d + +fn isEmpty(xs: List) -> Bool + ? \"No elements.\" + match xs + [] -> true + _ -> false + +verify count + count([]) => 0 +"; + +/// Emit the List certificate into a fresh scratch directory. +fn list_baseline(prefix: &str) -> Option<(ScratchDir, PathBuf, PathBuf)> { + if !lake_available() { + return None; + } + let dir = temp_dir(prefix); + std::fs::write(dir.join("listy.av"), LISTY).unwrap(); + let out = dir.join("out"); + let compile = aver_command() + .current_dir(&*dir) + .args([ + "compile", + "listy.av", + "--target", + "wasm-gc", + "--certify", + "-o", + ]) + .arg(&out) + .output() + .expect("aver compile --certify runs"); + assert!( + compile.status.success(), + "compile --certify failed:\n{}", + String::from_utf8_lossy(&compile.stderr) + ); + Some((dir, out.join("listy.wasm"), out.join("cert"))) +} + +/// The honest List certificate checks, with all three exports certified. +#[test] +fn cert_hardening_accepts_list_matches() { + let Some((_dir, wasm, cert)) = list_baseline("certharden-list-clean") else { + return; + }; + let (ok, report) = aver_cert("check", &wasm, &cert); + assert!(ok, "the List certificate must check:\n{report}"); + assert!(report.contains("3 checked exports"), "{report}"); +} + +/// The arm pick is the wall's, not the plan's: a plan that gives the `[]` +/// arm the cons arm's result (`isEmpty` answering `false` for `[]`) lowers +/// to other bytes than the emitted `then` branch, so the plan is refused. +#[test] +fn cert_hardening_declines_a_list_match_with_its_arms_exchanged() { + let Some((_dir, wasm, cert)) = list_baseline("certharden-list-arms") else { + return; + }; + replace_once( + &cert.join("Plans.lean"), + "(.cons .emptyList (.literal (.bool true)) (.cons .wild (.literal (.bool false)) .nil))", + "(.cons .emptyList (.literal (.bool false)) (.cons .wild (.literal (.bool true)) .nil))", + ); + let (ok, report) = aver_cert("check", &wasm, &cert); + assert_declined(ok, &report, "did not build"); +} + +/// The cons struct a List match casts to and reads the head and tail from +/// is the type table's, confirmed against the type section: declaring the +/// `List` struct for `List` (and back) is refused. +#[test] +fn cert_hardening_declines_exchanged_list_cons_structs() { + let Some((_dir, wasm, cert)) = list_baseline("certharden-list-structs") else { + return; + }; + let plans = cert.join("Plans.lean"); + let text = std::fs::read_to_string(&plans).unwrap(); + let index_after = |needle: &str| -> String { + let at = text + .find(needle) + .expect("the List instantiation is declared") + + needle.len(); + text[at..] + .chars() + .take_while(char::is_ascii_digit) + .collect() + }; + let (int_idx, str_idx) = (index_after("lists := [(.int, "), index_after("(.string, ")); + replace_once( + &plans, + &format!("lists := [(.int, {int_idx}), (.string, {str_idx})]"), + &format!("lists := [(.int, {str_idx}), (.string, {int_idx})]"), + ); + let (ok, report) = aver_cert("check", &wasm, &cert); + assert_declined(ok, &report, "did not build"); +} + +/// A cons pattern whose head and tail slots are exchanged: the head slot +/// would hold the tail, which the typing refuses before any byte is read. +#[test] +fn cert_hardening_declines_a_cons_pattern_with_head_and_tail_exchanged() { + let Some((_dir, wasm, cert)) = list_baseline("certharden-list-binders") else { + return; + }; + replace_once( + &cert.join("Plans.lean"), + "(.cons 65535 1)", + "(.cons 1 65535)", + ); + let (ok, report) = aver_cert("check", &wasm, &cert); + assert_declined(ok, &report, "did not build"); +} diff --git a/tests/cert_verify_spec.rs b/tests/cert_verify_spec.rs index 2ed17ba20..cc1bd4315 100644 --- a/tests/cert_verify_spec.rs +++ b/tests/cert_verify_spec.rs @@ -2665,9 +2665,10 @@ fn cert_verify_declines_tampered_array_new_data_operands() { // plan grammar certifies five more: 18 of 154. Since `--certify` compiles // the same module as a plain build, the String cursor, builder and // codepoint variants the plain build synthesizes are in it too, eight more - // functions that carry no claim: 18 of 162. + // functions that carry no claim: 18 of 162. A List match certifies five + // more: 23 of 162. assert!( - compile_report.contains("(18 certified, 144 source-level-only)"), + compile_report.contains("(23 certified, 139 source-level-only)"), "json certificate KPI denominator changed: {compile_report}" ); @@ -2686,7 +2687,7 @@ fn cert_verify_declines_tampered_array_new_data_operands() { let (ok, report) = aver_check(&wasm, &cert); assert!(ok, "expected clean json certificate to verify:\n{report}"); assert!( - report.contains("18 checked exports"), + report.contains("23 checked exports"), "json should certify the widened data-segment functions:\n{report}" ); assert!( diff --git a/tests/snapshots/cert_certify_spec__add_one_certificate_package.snap b/tests/snapshots/cert_certify_spec__add_one_certificate_package.snap index 38fa3e642..5fdb67f84 100644 --- a/tests/snapshots/cert_certify_spec__add_one_certificate_package.snap +++ b/tests/snapshots/cert_certify_spec__add_one_certificate_package.snap @@ -5,7 +5,7 @@ expression: golden == cert-manifest.json == { "schema_version": 9, - "format": {"version": 1, "wall_id": "sha256:ed89b143414bdff0bfadb49a49bc1e7d8c537365b69549c65f7e82fbccf73cef"}, + "format": {"version": 1, "wall_id": "sha256:5168df0c3f4da023c53a9c929e081803c559ed2e22fc6a103f8fb827745ae4d9"}, "wasm": "add_one.wasm", "wasm_sha256": "4b86ac5e745a7f0aeef0d24178a3f47ed09b4f98ffc36216aedf252c9cb20583", "target": "wasm-gc", diff --git a/tests/snapshots/cert_certify_spec__wasip2_component_certificate_package.snap b/tests/snapshots/cert_certify_spec__wasip2_component_certificate_package.snap index 40080bd74..8e7df5cb7 100644 --- a/tests/snapshots/cert_certify_spec__wasip2_component_certificate_package.snap +++ b/tests/snapshots/cert_certify_spec__wasip2_component_certificate_package.snap @@ -5,7 +5,7 @@ expression: golden == cert-manifest.json == { "schema_version": 9, - "format": {"version": 1, "wall_id": "sha256:ed89b143414bdff0bfadb49a49bc1e7d8c537365b69549c65f7e82fbccf73cef"}, + "format": {"version": 1, "wall_id": "sha256:5168df0c3f4da023c53a9c929e081803c559ed2e22fc6a103f8fb827745ae4d9"}, "wasm": "wasip2_carrierless.component.wasm", "wasm_sha256": "0e7064150f82e180dff6f774a8f48711acd2ea21d183ee06576d4f7c9f135aed", "target": "wasip2", diff --git a/tools/cert-baseline.json b/tools/cert-baseline.json index 3fcc1b71a..366f2dd2e 100644 --- a/tools/cert-baseline.json +++ b/tools/cert-baseline.json @@ -13,7 +13,10 @@ "unescapedChar" ], "certified": { + "Bytes_allInRange": "L1", "Bytes_byteToHex": "L1", + "Bytes_firstOutOfRange": "L1", + "Bytes_firstOutOfRangeIndex": "L1", "Bytes_hexDigit": "L1", "Bytes_highNibble": "L1", "Bytes_lowNibble": "L1", @@ -23,12 +26,14 @@ "isHighSurrogate": "L1", "isLowSurrogate": "L1", "jsonEntryKey": "L1", + "jsonEntryKeys": "L1", "jsonEntryValue": "L1", "jsonFloat": "L1", "jsonInt": "L1", "jsonList": "L1", "jsonStr": "L1", "prependJsonEntry": "L1", + "renderJsonStringList": "L1", "singletonJsonEntries": "L1", "unescapedChar": "L1" }, @@ -154,34 +159,58 @@ "certified": { "App_Commands_duplicateSettlementAudit": "L1", "App_Commands_duplicateWebhookAudit": "L1", + "App_Commands_hasSettlementRow": "L1", + "App_Commands_openedCaseAuditsInto": "L1", + "App_Commands_providerStatesInto": "L1", "App_Commands_sampleAudit": "L1", "App_Commands_sampleCase": "L1", "App_Commands_sampleEvent": "L1", "App_Commands_sampleSettlement": "L1", "App_Commands_sampleState": "L1", + "App_Queries_providerEventsInto": "L1", + "App_Queries_providerStatesInto": "L1", "App_Queries_sampleCase": "L1", "App_Queries_sampleEvent": "L1", + "App_Queries_sampleOrFirst": "L1", "App_Queries_sampleSettlement": "L1", + "App_Render_renderAuditItemsInto": "L1", "App_Render_renderCaseItem": "L1", + "App_Render_renderCaseItemsInto": "L1", "App_Render_sampleAudit": "L1", "App_Render_sampleCase": "L1", "App_Render_sampleEvent": "L1", "App_Render_sampleSettlement": "L1", "App_Render_sampleSummary": "L1", "App_Render_settlementKindText": "L1", + "Bytes_allInRange": "L1", "Bytes_byteToHex": "L1", + "Bytes_firstOutOfRange": "L1", + "Bytes_firstOutOfRangeIndex": "L1", "Bytes_hexDigit": "L1", "Bytes_highNibble": "L1", "Bytes_lowNibble": "L1", "Domain_Cases_auditForOpenedCase": "L1", "Domain_Cases_auditForResolvedCase": "L1", + "Domain_Cases_caseKeyExists": "L1", + "Domain_Cases_filterOpenInto": "L1", + "Domain_Cases_filterResolvedInto": "L1", + "Domain_Cases_findCaseById": "L1", + "Domain_Cases_hasCaseId": "L1", "Domain_Cases_makeCaseDraft": "L1", + "Domain_Cases_openCasesForPaymentInto": "L1", + "Domain_Cases_prependAll": "L1", "Domain_Cases_statusText": "L1", + "Domain_Cases_tail": "L1", "Domain_Ledger_emptyState": "L1", "Domain_Ledger_eventAmount": "L1", "Domain_Ledger_eventAt": "L1", "Domain_Ledger_eventCurrency": "L1", "Domain_Ledger_eventName": "L1", + "Domain_Ledger_eventsForPaymentInto": "L1", + "Domain_Ledger_findState": "L1", + "Domain_Ledger_hasSourceId": "L1", + "Domain_Ledger_nextSeq": "L1", + "Domain_Ledger_nextSeqFrom": "L1", "Domain_Ledger_samePayment": "L1", "Domain_Ledger_sampleAuthorized": "L1", "Domain_Ledger_sampleCaptured": "L1", @@ -195,14 +224,32 @@ "Domain_Normalize_normalizeWebhookEvent": "L1", "Domain_Reconcile_amountMissing": "L1", "Domain_Reconcile_compareAmounts": "L1", + "Domain_Reconcile_findState": "L1", + "Domain_Reconcile_firstCurrency": "L1", + "Domain_Reconcile_prependAll": "L1", "Domain_Reconcile_sampleCaptureRow": "L1", "Domain_Reconcile_sampleRefundRow": "L1", "Domain_Reconcile_sampleState": "L1", + "Domain_Reconcile_settlementsForPaymentInto": "L1", + "Domain_Reconcile_settlementsForProviderInto": "L1", + "Domain_Views_capturedTotal": "L1", + "Domain_Views_capturedTotalFrom": "L1", + "Domain_Views_countOpenCases": "L1", + "Domain_Views_countOpenCasesFrom": "L1", + "Domain_Views_countProviderEvents": "L1", + "Domain_Views_countProviderEventsFrom": "L1", + "Domain_Views_countProviderRows": "L1", + "Domain_Views_countProviderRowsFrom": "L1", + "Domain_Views_refundedTotal": "L1", + "Domain_Views_refundedTotalFrom": "L1", "Domain_Views_sampleCaptureRow": "L1", "Domain_Views_sampleCase": "L1", "Domain_Views_sampleEvent": "L1", "Domain_Views_sampleState": "L1", "Infra_Audit_auditPath": "L1", + "Infra_Audit_filterSubjectInto": "L1", + "Infra_Audit_hasAuditKey": "L1", + "Infra_Audit_newEntriesInto": "L1", "Infra_Audit_sampleAudit": "L1", "Infra_Store_casesPath": "L1", "Infra_Store_dataDir": "L1", @@ -225,7 +272,10 @@ "Node_validate" ], "certified": { + "Bytes_allInRange": "L1", "Bytes_byteToHex": "L1", + "Bytes_firstOutOfRange": "L1", + "Bytes_firstOutOfRangeIndex": "L1", "Bytes_hexDigit": "L1", "Bytes_highNibble": "L1", "Bytes_lowNibble": "L1", @@ -304,11 +354,13 @@ "intLessZero": "L1", "isEven": "L3", "isOdd": "L3", + "listHeadGoal": "L1", "mkOp": "L1", "quad": "L1", "quoteOrSelf": "L1", "shout": "L1", "sumFrom": "L3", + "sumListGoal": "L1", "tagName": "L1", "userName": "L1", "wrapItems": "L1" @@ -354,6 +406,8 @@ "classify": "L1", "describe": "L1", "fcmp": "L1", + "listHead": "L1", + "sumList": "L1", "tick": "L3" }, "laws": [] From 0c4c29e199f9630119399e0c624c1a9242746e28 Mon Sep 17 00:00:00 2001 From: jasisz Date: Sat, 26 Sep 2026 00:24:33 +0200 Subject: [PATCH 2/2] cert: unfold the type table's pieces in a bridge's typing step A type table long enough to be written in pieces (`types_records_0`, `types_records_1`, ...) left those pieces folded in the `simp` that proves a bridge's arguments well typed, so the step stopped on an unreduced record lookup and the bridge fell to `sorry`. btc-listener's records crossed that length once List matches were certified: 65 of its 494 bridges and one bridged law lost their credit. The typing step now unfolds every piece of the table but the string segments, which typing never reads, and btc-listener is back at 494 of 494 bridges and 16 of 17 bridged laws with 765 certified exports. Co-Authored-By: Claude Opus 5.5 (1M context) --- aver-cert/src/engine/plan.rs | 33 ++++++++++++++++++++++++-- aver-cert/src/engine/source_bridges.rs | 18 +++++++++++++- 2 files changed, 48 insertions(+), 3 deletions(-) diff --git a/aver-cert/src/engine/plan.rs b/aver-cert/src/engine/plan.rs index 1b4bf7adb..b376f75a0 100644 --- a/aver-cert/src/engine/plan.rs +++ b/aver-cert/src/engine/plan.rs @@ -550,6 +550,17 @@ impl PlanTypeTable { /// inline (see [`LEAN_TABLE_PIECE_CHARS`]); every byte list longer than /// [`LEAN_LIST_CHUNK`] is written in `++`-joined literals. pub fn lean_decls(&self, name: &str) -> String { + self.lean_decls_and_pieces(name).0 + } + + /// The names of the piece declarations [`Self::lean_decls`] writes before + /// `def {name}`, in order. A proof that unfolds the table by `simp` must + /// unfold these too, or a field written in pieces stays opaque. + pub fn lean_piece_names(&self, name: &str) -> Vec { + self.lean_decls_and_pieces(name).1 + } + + fn lean_decls_and_pieces(&self, name: &str) -> (String, Vec) { let records = self .records .iter() @@ -607,13 +618,19 @@ impl PlanTypeTable { let lists = field("lists", "Ty × Nat", &pairs(&self.lists)); let opaques = field("opaques", "Nat × Nat", &opaques); let segs = field("strSegs", "List Nat × Nat", &segs); - format!( + let pieces = decls + .lines() + .filter_map(|line| line.strip_prefix("def ")) + .filter_map(|rest| rest.split_once(" :").map(|(n, _)| n.to_string())) + .collect(); + let text = format!( "{decls}def {name} : TypeTable :=\n {{ carrier := {}, mag := {}, str := {}, strVec := {},\n records := {records},\n sums := {sums},\n options := {options}, results := {results},\n vecs := {vecs}, lists := {lists}, opaques := {opaques},\n strSegs := {segs} }}\n\n", lean_opt_nat(self.carrier), lean_opt_nat(self.mag), lean_opt_nat(self.str_), lean_opt_nat(self.str_vec), - ) + ); + (text, pieces) } } @@ -748,6 +765,18 @@ mod tests { .flat_map(|r| [r.tid as u64, r.struct_idx as u64]) .collect(); assert_eq!(numerals(&piece_bodies(&text, "records").concat()), expected); + + // The piece names are exactly the declarations written before the + // table, so a proof unfolding the table can name every one of them. + let names = tt.lean_piece_names("types"); + let defs: Vec = text + .lines() + .filter_map(|l| l.strip_prefix("def ")) + .filter_map(|l| l.split_once(" :").map(|(n, _)| n.to_string())) + .filter(|n| n != "types") + .collect(); + assert_eq!(names, defs); + assert!(names.iter().any(|n| n.starts_with("types_records_"))); } /// A table that fits one piece is written as one declaration with one diff --git a/aver-cert/src/engine/source_bridges.rs b/aver-cert/src/engine/source_bridges.rs index cb56fba12..8e45a3c95 100644 --- a/aver-cert/src/engine/source_bridges.rs +++ b/aver-cert/src/engine/source_bridges.rs @@ -919,6 +919,10 @@ struct BridgePlan { entries: BTreeMap, /// The export names of the obligations, in `Plans.fnPlans` order. obligation_names: Vec, + /// The piece declarations `Plans.types` is written in, which the typing + /// `simp` of an export theorem must unfold with it (the string segments + /// excepted: typing never reads them). + type_pieces: Vec, } /// The largest plan a bridge is attempted for. A step proof unfolds the @@ -1036,6 +1040,13 @@ fn plan_bridges(analysis: &Analysis, model: &SourceModel) -> BridgePlan { depth: BTreeMap::new(), literals: BTreeSet::new(), with_default: false, + type_pieces: analysis + .types + .lean_piece_names("types") + .into_iter() + .filter(|piece| !piece.starts_with("types_strSegs_")) + .map(|piece| format!("AverCert.Plans.{piece}")) + .collect(), entries: analysis .entries .iter() @@ -1713,7 +1724,12 @@ fn render_export( ), }; let typing = format!( - "{intro}{split_cases}all_goals simp [{TYPING_SIMPS}, AverCert.Plans.fn{func_idx}]" + "{intro}{split_cases}all_goals simp [{TYPING_SIMPS}{pieces}, AverCert.Plans.fn{func_idx}]", + pieces = plan + .type_pieces + .iter() + .map(|piece| format!(", {piece}")) + .collect::() ); let statement = bridge.expanded_statement(); s.push_str(&format!(