From c21714a65a3032cd20b6216409f58d770a25acb1 Mon Sep 17 00:00:00 2001 From: jasisz Date: Fri, 25 Sep 2026 22:36:32 +0200 Subject: [PATCH 1/5] 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/5] 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!( From c9b8e8151f67a50859a3f0c017d0bc3c2f2aa0f5 Mon Sep 17 00:00:00 2001 From: jasisz Date: Sat, 26 Sep 2026 06:09:56 +0200 Subject: [PATCH 3/5] cert: read the type section only through its cut in the acceptance proofs The package's roles_ok and plans_ok unfolded carrierState, carrierConfirmed and typeSectionMatches with simp. Each is a match on the decoded type section, and simp reduced that match before the cut could rewrite the decode, evaluating the whole type-section decode in the elaborator. After the Vector version structs changed the type section, btc-listener's Artifact.lean ran past the 9000-second phase limit. Unfold these definitions by their unconditional equations with matcher reduction off, so the decode is replaced by the cut and read only in the kernel: roles_ok 13 s and plans_ok 68 s on that package, where each ran for over 10 minutes. Co-Authored-By: Claude Opus 5.5 (1M context) --- CHANGELOG.md | 4 ++++ aver-cert/src/engine/render_package.rs | 26 +++++++++++++++++++------- 2 files changed, 23 insertions(+), 7 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index a92494f38..785a6c5af 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -16,6 +16,10 @@ All notable changes to Aver are documented here. Starting with 0.10.0, minor rel - **Every backend runs the same match.** The compiler turns such a match into nested ordinary matches right after checking it, so the VM, generated Rust, wasm-gc, `wasip2` and the Lean export all read the same program. A `match` that uses these patterns inside a `yield` function is refused for now; move it into a helper function. - **`aver format` prints match patterns in one spelling:** `[a, b, ..rest]`, `Option.Some(0)`, `(x, _)`. +### Fixed — a large certificate package checks again after Vector versions + +- **`aver-cert check` of a large package no longer runs out of time on two acceptance proofs.** The package's proofs of the host-helper table and of the plans' layout unfolded definitions that read the decoded type section, and Lean evaluated the whole decode before it could use the package's declared type-section cut. After Vector values became versions (more types in the type section), btc-listener's package passed the 9000-second limit where it had taken minutes. The two proofs now read the type section only through the cut: 13 s and 68 s on that package. Packages must be produced again to get the new proofs. + ### Fixed — `aver proof --gate` passes a law that became universal - **A law promoted from bounded to universal no longer fails the gate.** A bounded law records no axioms, and its universal proof usually depends on Lean's standard axioms, so the gate reported `REGRESSION : axioms grew {} -> {Classical.choice,Quot.sound,propext}`. It now prints `promoted : bounded -> universal, now uses …` and lists the law under `Promoted:` in the summary. The gate still fails when a law newly depends on any other axiom (`sorryAx`, `Lean.ofReduceBool`, a user `axiom`) at any tier, when it newly depends on one of the standard three at the same tier, and on a missing law, a lower tier or a changed backend. diff --git a/aver-cert/src/engine/render_package.rs b/aver-cert/src/engine/render_package.rs index 1e78ea560..dedaa6347 100644 --- a/aver-cert/src/engine/render_package.rs +++ b/aver-cert/src/engine/render_package.rs @@ -557,10 +557,16 @@ fn render_artifact( AverCert.DeclaredLayout.Chars.carrierHelperAbsent_eq,\n \ AverCert.DeclaredLayout.Chars.boxIdx_eq, AverCert.DeclaredLayout.Chars.toIndexIdx_eq,\n \ AverCert.DeclaredLayout.Chars.cmpIdx_eq{cuts}]\n \ - decide +kernel", + {carrier}decide +kernel", r.roles_lean_value(), - cuts = if layout { - ", CertDecode.carrierState, types_cut, exports_cut" + cuts = if layout { ", exports_cut" } else { "" }, + // The carrier is read through the type-section cut. Its + // definition is a `match` on the decoded type section, so it + // is unfolded by its unconditional equation with matcher + // reduction off: otherwise `simp` evaluates the whole type + // decode in the elaborator before the cut can rewrite it. + carrier = if layout { + "simp -iota only [CertDecode.carrierState.eq_def, types_cut]\n " } else { "" }, @@ -651,13 +657,19 @@ fn render_artifact( "\n " ), ); - // With a declared layout the helper types are read from it. + // With a declared layout the helper types are read from it. The + // definitions that `match` on the decoded type section are unfolded by + // their unconditional equations with matcher reduction off, so the type + // section is read only through its cut, in the kernel: `simp` with the + // definitions themselves evaluates the whole type decode in the + // elaborator first (btc-listener: over 10 minutes per theorem). let rest_proof = if layout { "(AverCert.DeclaredLayout.plansAcceptedRest_of_layout layout_ok (by\n \ dsimp only [AverCert.DeclaredLayout.plansAcceptedRestL, data]\n \ - simp only [AverCert.TypeTable.typeTableConfirmed, AverCert.TypeTable.carrierConfirmed,\n \ - CertDecode.carrierState, AverCert.DeclaredLayout.roleTypesPinnedL,\n \ - AverCert.DeclaredLayout.roleTypePinnedL, AverCert.WasmSlice.typeSectionMatches, types_cut]\n \ + simp -iota only [AverCert.TypeTable.typeTableConfirmed.eq_def,\n \ + AverCert.TypeTable.carrierConfirmed.eq_def, CertDecode.carrierState.eq_def,\n \ + AverCert.DeclaredLayout.roleTypesPinnedL, AverCert.DeclaredLayout.roleTypePinnedL,\n \ + AverCert.WasmSlice.typeSectionMatches.eq_def, types_cut]\n \ decide +kernel))" } else { "(by decide +kernel)" From 19aefded1c2de77409bab76a160152021be1ac03 Mon Sep 17 00:00:00 2001 From: jasisz Date: Sat, 26 Sep 2026 06:37:06 +0200 Subject: [PATCH 4/5] cert: certify non-empty List literals A non-empty literal pushes its items, then the empty list, and calls the per-type cons helper once per item. The plan grammar now admits that node: its typing needs the cons helper the type table declares for the element type, with the planned signature (T, List) -> List; its lowering is the items, ref.null and one call per item; its meaning is the cons cells of the items in order. The cons helper is offered as a planned internal function, and a new acceptance conjunct (consPinned) requires its plan to be the wall's own cons plan: one List.prepend of its two parameters. So the literal's calls reach a function whose meaning is proved, not assumed, and the agreement proof folds the calls over the reversed items. No schema change; the wall id rotates. The producer prints the items, declares the helper per element type, offers the helper with the literal's function, and carries the Rust twins of the typing and lowering. Bridges of functions that return a literal unfold it with the new simp lemmas. Hostile tests: the helper declared as a user function of the same signature, the helper's plan changed to return the tail, and the helpers of two instantiations exchanged, each refused. Ratchet: gains only. Co-Authored-By: Claude Opus 5.5 (1M context) --- CHANGELOG.md | 4 + .../wall/current/AcceptanceSoundness.lean | 20 +- .../wall/current/AcceptanceSoundnessCore.lean | 24 +- .../wall/current/AcceptedArtifactCore.lean | 21 +- .../assets/wall/current/DeclaredLayout.lean | 3 +- aver-cert/assets/wall/current/Grammar.lean | 58 ++++- .../assets/wall/current/GrammarBridge.lean | 10 +- .../assets/wall/current/GrammarLower.lean | 13 +- .../assets/wall/current/GrammarSound.lean | 216 +++++++++++++++--- .../assets/wall/current/GrammarTotal.lean | 29 ++- aver-cert/assets/wall/current/SchemaCore.lean | 4 + aver-cert/assets/wall/current/TypeTable.lean | 3 +- aver-cert/src/engine/plan.rs | 31 ++- aver-cert/src/engine/plan_check.rs | 83 ++++++- aver-cert/src/engine/produce.rs | 33 ++- aver-cert/src/engine/source_bridges.rs | 3 +- aver-cert/src/format.rs | 2 +- docs/certificate-format.md | 12 +- docs/certification.md | 4 +- src/codegen/cert/plan_from_mir.rs | 54 ++++- src/codegen/wasm_gc/cert_layout.rs | 5 + src/codegen/wasm_gc/module.rs | 1 + tests/cert_certify_spec.rs | 4 +- tests/cert_hardening_spec.rs | 148 +++++++++++- ...ify_spec__add_one_certificate_package.snap | 2 +- ..._wasip2_component_certificate_package.snap | 2 +- tools/cert-baseline.json | 9 + 27 files changed, 704 insertions(+), 94 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 785a6c5af..cecbdf00c 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 list literals + +- **A function that builds a non-empty list literal can now be certified.** `[a, b, c]` used to leave the function source-level only. The compiler builds such a literal by calling its cons helper for the element type once per item, and the certificate now carries that helper as a planned function: the wall checks that its plan is exactly one `List.prepend` of its two parameters, so the literal's meaning is proved, not assumed. On the btc-listener corpus this certifies 58 more functions and gives 41 more of them a source bridge (a function that returns a literal is now bridged to its source); across the examples, projects and certificate fixtures, 27 more functions are certified. The wall identity rotates: packages produced by earlier versions must be produced again. + ### 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. diff --git a/aver-cert/assets/wall/current/AcceptanceSoundness.lean b/aver-cert/assets/wall/current/AcceptanceSoundness.lean index cab000b01..163b8e057 100644 --- a/aver-cert/assets/wall/current/AcceptanceSoundness.lean +++ b/aver-cert/assets/wall/current/AcceptanceSoundness.lean @@ -46,6 +46,15 @@ theorem contracts_of {C : Nat} (S : CarrierSpec C) (h : HostFns) (hc : HostContr hCmp := hc.cmp hEq := hc.eq +/-- A declared cons helper means `List.prepend` in the one model of all plans. -/ +theorem modelOf_cons (hf : PlanFacts s tt fns) : + ∀ t f, (mctxOf s tt fns).listCons t = some f → ∀ k h tl sv, + HasTy (mctxOf s tt fns) tl (.list t) → modelOf fns k f [h, tl] = some sv → + sv = .cons t h tl := by + intro t f hf' k h tl sv htl hm + obtain ⟨p, hp, hcp⟩ := hf.cons t f hf' + exact groupModel_consPlan _ (planOf fns) hp (isConsPlan_body hcp) k h tl sv htl hm + /-- Every planned function is certified at the one model of all plans. -/ theorem fns_certified (hf : PlanFacts s tt fns) (S : CarrierSpec (mctxOf s tt fns).carrier) (h : HostFns) (hc : HostContracts S h) : @@ -64,6 +73,7 @@ theorem fns_certified (hf : PlanFacts s tt fns) refine fn_certified_group S (boxRef _) h.add h.sub h.mul h.cmp h.eq (fun _ => none) (contracts_of S h hc) (fun _ _ _ _ hr => by cases hr) _ _ (mctxOf s tt fns) rfl hBox hAdd hSub hMul hNeg hCmp hEq R (planOf fns) (fun _ _ _ => none) ?_ ?_ + (modelOf_cons hf) · intro f sig hs hG simp [mctxOf, hG] at hs · intro f p hp @@ -148,6 +158,12 @@ theorem obligation_total (hf : PlanFacts s tt fns) {e : FnEntry} (he : e ∈ fns have hp := hGP f p hg obtain ⟨e', he', rfl, rfl⟩ := planOf_some hp exact ⟨by simp [mctxOf, hp], hf.typed e' he', hClaims e' he', by simp [codeOf, hp]⟩) + (by + intro t f hf' k h tl sv htl hm + have hm' : groupModel (groupModel (fun _ _ _ => none) (planOf fns)) (groupOf ms) k f + [h, tl] = some sv := hm + rw [groupModel_restrict (planOf fns) (groupOf ms) hGP] at hm' + exact modelOf_cons hf t f hf' k h tl sv htl hm') (fun k _ _ => boxRef_total _ k) ht.add ht.sub ht.mul e.funcIdx e.plan (hGall (e.funcIdx, e.plan) (by simp only [ms, groupMembers] @@ -234,7 +250,7 @@ theorem accepted_nonvacuous (artifact : ArtifactData) have hwf : declsWellFormed artifact.manifest.subject artifact.manifest.types artifact.manifest.fnPlans = true := by simp only [plansAccepted, Bool.and_eq_true] at hPlans - exact hPlans.2 + exact hPlans.1.2 have hti : typesInhabited (mctxOf artifact.manifest.subject artifact.manifest.types artifact.manifest.fnPlans) artifact.manifest.types artifact.manifest.fnPlans = true := by simp only [declsWellFormed, Bool.and_eq_true] at hwf @@ -262,7 +278,7 @@ theorem refTest_exact_of_accepted (artifact : ArtifactData) intro M have hpin : S3Pin M d.tid d.ctors.length (grp.map (·.1)) = true := by simp only [plansAccepted, Bool.and_eq_true] at hPlans - have htt := hPlans.1.1.1.2 + have htt := hPlans.1.1.1.1.2 unfold typeTableConfirmed at htt simp only [hg, Bool.and_eq_true, List.all_eq_true] at htt have hs := htt.2.1.1.1.1.1.1.1.2 d hd diff --git a/aver-cert/assets/wall/current/AcceptanceSoundnessCore.lean b/aver-cert/assets/wall/current/AcceptanceSoundnessCore.lean index 5331ba79b..c18cdc29e 100644 --- a/aver-cert/assets/wall/current/AcceptanceSoundnessCore.lean +++ b/aver-cert/assets/wall/current/AcceptanceSoundnessCore.lean @@ -158,6 +158,8 @@ theorem groupModel_restrict (P G : Nat → Option FnPlan) structure PlanFacts (s : Subject) (tt : TypeTable) (fns : List FnEntry) : Prop where distinct : (roleIndices (mctxOf s tt fns) ++ fns.map (·.funcIdx)).Nodup typed : ∀ e ∈ fns, planTyped (mctxOf s tt fns) e.plan = true + cons : ∀ t f, (mctxOf s tt fns).listCons t = some f → + ∃ p, planOf fns f = some p ∧ isConsPlan p = true theorem PlanFacts.nodup {s : Subject} {tt : TypeTable} {fns : List FnEntry} (hf : PlanFacts s tt fns) : (fns.map (·.funcIdx)).Nodup := @@ -165,11 +167,21 @@ theorem PlanFacts.nodup {s : Subject} {tt : TypeTable} {fns : List FnEntry} theorem planFacts_of_accepted (artifact : ArtifactData) (h : plansAccepted artifact = true) : PlanFacts artifact.manifest.subject artifact.manifest.types artifact.manifest.fnPlans := by - simp only [plansAccepted, Bool.and_eq_true, List.all_eq_true] at h - obtain ⟨⟨⟨⟨⟨hd, he⟩, _⟩, _⟩, _⟩, _⟩ := h - refine ⟨of_decide_eq_true hd, fun e hm => ?_⟩ - have := he e hm - simp only [entryAccepted, Bool.and_eq_true] at this - exact this.1.1 + simp only [plansAccepted, consPinned, Bool.and_eq_true, List.all_eq_true] at h + obtain ⟨⟨⟨⟨⟨⟨hd, he⟩, _⟩, _⟩, _⟩, _⟩, hc⟩ := h + refine ⟨of_decide_eq_true hd, fun e hm => ?_, fun t f hf => ?_⟩ + · have := he e hm + simp only [entryAccepted, Bool.and_eq_true] at this + exact this.1.1 + · simp only [mctxOf, Option.map_eq_some_iff] at hf + obtain ⟨x, hx, rfl⟩ := hf + have hmem := hc x (List.mem_of_find?_eq_some hx) + revert hmem + split + · rename_i p hp + intro hmem + exact ⟨p, hp, hmem⟩ + · intro hmem + cases hmem end AcceptanceSoundness diff --git a/aver-cert/assets/wall/current/AcceptedArtifactCore.lean b/aver-cert/assets/wall/current/AcceptedArtifactCore.lean index 4eafb0ad4..f0a68cd21 100644 --- a/aver-cert/assets/wall/current/AcceptedArtifactCore.lean +++ b/aver-cert/assets/wall/current/AcceptedArtifactCore.lean @@ -103,7 +103,16 @@ def obligationsOf (s : Subject) (tt : TypeTable) (fns : List FnEntry) : List Obl /-! ### Calls -/ mutual - /-- The function indices a plan calls (`call` and `tailCall`). -/ + /-- Every declared cons helper is a planned function whose plan is the + wall's cons plan (`Grammar.isConsPlan`: its body is `consBody`), so a + non-empty list literal calls a function whose meaning is `List.prepend`. -/ +def consPinned (tt : TypeTable) (fns : List FnEntry) : Bool := + tt.listCons.all fun x => + match planOf fns x.2 with + | some p => isConsPlan p + | none => false + +/-- The function indices a plan calls (`call` and `tailCall`). -/ def callTargets : Expr → List Nat | .literal _ => [] | .local _ => [] @@ -567,7 +576,8 @@ def plansAccepted (artifact : ArtifactData) : Bool := typeTableConfirmed artifact.modBytes artifact.modLen m.subject m.types m.fnPlans && dataConfirmed artifact.modBytes artifact.modLen m.subject m.types m.fnPlans && roleTypesPinned artifact.modBytes artifact.modLen M && - declsWellFormed m.subject m.types m.fnPlans + declsWellFormed m.subject m.types m.fnPlans && + consPinned m.types m.fnPlans /-- The conjuncts of `plansAccepted` other than the per-entry checks. A package proves the per-entry checks in chunks, one declaration each, so @@ -579,7 +589,8 @@ def plansAcceptedRest (artifact : ArtifactData) : Bool := typeTableConfirmed artifact.modBytes artifact.modLen m.subject m.types m.fnPlans && dataConfirmed artifact.modBytes artifact.modLen m.subject m.types m.fnPlans && roleTypesPinned artifact.modBytes artifact.modLen M && - declsWellFormed m.subject m.types m.fnPlans + declsWellFormed m.subject m.types m.fnPlans && + consPinned m.types m.fnPlans theorem plansAccepted_of_parts (artifact : ArtifactData) (hall : artifact.manifest.fnPlans.all @@ -588,9 +599,9 @@ theorem plansAccepted_of_parts (artifact : ArtifactData) artifact.manifest.fnPlans) = true) (hrest : plansAcceptedRest artifact = true) : plansAccepted artifact = true := by simp only [plansAcceptedRest, Bool.and_eq_true] at hrest - obtain ⟨⟨⟨⟨ha, hc⟩, hd⟩, he⟩, hf⟩ := hrest + obtain ⟨⟨⟨⟨⟨ha, hc⟩, hd⟩, he⟩, hf⟩, hg⟩ := hrest simp only [plansAccepted, Bool.and_eq_true] - exact ⟨⟨⟨⟨⟨ha, hall⟩, hc⟩, hd⟩, he⟩, hf⟩ + exact ⟨⟨⟨⟨⟨⟨ha, hall⟩, hc⟩, hd⟩, he⟩, hf⟩, hg⟩ /-- The manifest's obligations are exactly the ones the wall derives from its plans: no obligation field is producer data. -/ diff --git a/aver-cert/assets/wall/current/DeclaredLayout.lean b/aver-cert/assets/wall/current/DeclaredLayout.lean index 8b3a6b811..27fef935c 100644 --- a/aver-cert/assets/wall/current/DeclaredLayout.lean +++ b/aver-cert/assets/wall/current/DeclaredLayout.lean @@ -205,7 +205,8 @@ def plansAcceptedRestL (artifact : ArtifactData) (L : Layout) : Bool := typeTableConfirmed artifact.modBytes artifact.modLen m.subject m.types m.fnPlans && dataConfirmed artifact.modBytes artifact.modLen m.subject m.types m.fnPlans && roleTypesPinnedL L artifact.modBytes artifact.modLen M && - declsWellFormed m.subject m.types m.fnPlans + declsWellFormed m.subject m.types m.fnPlans && + consPinned m.types m.fnPlans theorem plansAcceptedRest_of_layout {artifact : ArtifactData} {L : Layout} (hL : layoutConfirmed artifact.modBytes artifact.modLen L = true) diff --git a/aver-cert/assets/wall/current/Grammar.lean b/aver-cert/assets/wall/current/Grammar.lean index edc8d6971..e583845a3 100644 --- a/aver-cert/assets/wall/current/Grammar.lean +++ b/aver-cert/assets/wall/current/Grammar.lean @@ -49,7 +49,11 @@ Euclidean `__aint_divmod` call. * `interp parts` — `InterpolatedStr` whose parts are all `String` (a literal part printed as a string literal). - * `list t []` — the empty `List(..)` literal, with its element type. + * `list t items` — a `List(..)` literal with its element type: `[]` is + `ref.null` of the cons struct, and a non-empty literal pushes its items, + `ref.null`, and calls the `List` cons helper once per item. The + helper's index comes from the type table (`MCtx.listCons`), and the + acceptance pins its plan to exactly `consPlan t`. * `construct c ty args` — `Construct`; `c` is the constructor (`MirCtor::User(CtorId)` as type id + constructor index, or a built-in `Some`/`None`/`Ok`/`Err`) and `ty` is the node's stamped type @@ -206,8 +210,7 @@ mutual /-- `InterpolatedStr` whose parts are all `String`: a literal part is printed as a string literal, an embed as its expression. -/ | interp (parts : List Expr) - /-- `List(items)` with its element type (the stamped instantiation); - only the empty literal `[]` is admitted. -/ + /-- `List(items)` with its element type (the stamped instantiation). -/ | list (elem : Ty) (items : List Expr) /-- The arms of a `Match`, in source order. -/ inductive Arms where @@ -276,6 +279,9 @@ structure MCtx where vecStruct : Ty → Nat := fun _ => 0 listStruct : Ty → Nat := fun _ => 0 opaqueStruct : Nat → Nat := fun _ => 0 + /-- The cons helper of `List` (`(T, List) -> List`) a non-empty + literal calls, when the type table declares one. -/ + listCons : Ty → Option Nat := fun _ => none /-- One function's plan: signature, the resolver slot count (parameters and every binder; the const-compare scratch local sits at this index), the @@ -437,6 +443,28 @@ def varArmΓ (M : MCtx) (n : Nat) (Γ : Nat → Option Ty) (tid : Nat) : Pat → | .wild => some Γ | _ => none +/-! ## The cons helper + +A non-empty list literal calls the per-instantiation cons helper, whose body +is one `struct.new` of the cons struct: exactly the lowering of the one-node +plan `List.prepend(local 0, local 1)`. -/ + +/-- The cons helper's signature. -/ +def consSig (t : Ty) : Sig := ⟨[t, .list t], .list t⟩ + +/-- The cons helper's body: `List.prepend(head, tail)` over its parameters. -/ +def consBody : Expr := .call (.builtin .listPrepend) [.local 0, .local 1] + +/-- A plan is the wall's own cons plan: its body is `consBody`, so its + meaning is `List.prepend` of its two arguments. (Its signature is the + typing's business: a literal of `List` requires the helper's planned + signature to be `consSig t`; its slots and locals are pinned with its + code entry like every plan's.) -/ +def isConsPlan (p : FnPlan) : Bool := + match p.body with + | .call (.builtin .listPrepend) [.local 0, .local 1] => true + | _ => false + /-! ## Typing One checker for every node. `n` is the resolver slot count: a `let` binder @@ -557,9 +585,14 @@ mutual | some ts => if allStr ts then some .string else none | none => none | .list t items => - match items with - | [] => some (.list t) - | _ => none + if items.isEmpty then some (.list t) + else + match M.listCons t, tysOf M n Γ items with + | some f, some ts => + if M.sigs f = some (consSig t) ∧ ts.all (fun x => decide (x = t)) = true then + some (.list t) + else none + | _, _ => none | .match_ s arms => match tyOf M n Γ false s with | some .int => if arms.firstLit then tyIntArms M n Γ tail arms else none @@ -833,6 +866,11 @@ def strCat : List SVal → Option (List Nat) def divByZeroBytes : List Nat := [100, 105, 118, 105, 115, 105, 111, 110, 32, 98, 121, 32, 122, 101, 114, 111] +/-- The list of `vs`, in order, as cons cells of `List`. -/ +def consAll (t : Ty) : List SVal → SVal + | [] => .nil t + | v :: vs => .cons t v (consAll t vs) + def builtinEval : Builtin → List SVal → Option SVal | .boolAnd, [.b x, .b y] => some (.b (x && y)) | .boolOr, [.b x, .b y] => some (.b (x || y)) @@ -965,9 +1003,11 @@ mutual | some vs => (strCat vs).map .s | none => none | .list t items => - match items with - | [] => some (.nil t) - | _ => none + if items.isEmpty then some (.nil t) + else + match evalArgs F env items with + | some vs => some (consAll t vs) + | none => none def evalArgs (F : Nat → List SVal → Option SVal) (env : Nat → Option SVal) : List Expr → Option (List SVal) | [] => some [] diff --git a/aver-cert/assets/wall/current/GrammarBridge.lean b/aver-cert/assets/wall/current/GrammarBridge.lean index 95571940c..1aa2df632 100644 --- a/aver-cert/assets/wall/current/GrammarBridge.lean +++ b/aver-cert/assets/wall/current/GrammarBridge.lean @@ -337,7 +337,15 @@ theorem eval_mono {F G : Nat → List SVal → Option SVal} (hle : Le F G) : split at h · rename_i vs hvs; rw [evalArgs_mono hle env parts vs hvs]; exact h · cases h - | env, .list t items, v, h => by simpa [eval] using h + | env, .list t items, v, h => by + simp only [eval] at h ⊢ + by_cases he : items.isEmpty = true + · simp only [he, ↓reduceIte] at h ⊢ + exact h + · simp only [he, Bool.false_eq_true, ↓reduceIte] at h ⊢ + split at h + · rename_i vs hvs; rw [evalArgs_mono hle env items vs hvs]; exact h + · cases h theorem evalArgs_mono {F G : Nat → List SVal → Option SVal} (hle : Le F G) : ∀ (env : Nat → Option SVal) (es : List Expr) (vs : List SVal), evalArgs F env es = some vs → evalArgs G env es = some vs diff --git a/aver-cert/assets/wall/current/GrammarLower.lean b/aver-cert/assets/wall/current/GrammarLower.lean index 582d9e8dd..2ad2dccb9 100644 --- a/aver-cert/assets/wall/current/GrammarLower.lean +++ b/aver-cert/assets/wall/current/GrammarLower.lean @@ -46,7 +46,9 @@ * a tuple destructure stashes the subject and reads each bound component 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; + `struct.new` of it; a non-empty literal pushes its items in order, then + `ref.null`, then calls the cons helper once per item, so the last item + is consed first (`emit_mir_list_literal`); * 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 @@ -442,7 +444,14 @@ mutual 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)] + | .list t items => + if items.isEmpty then [.nullOf (M.listStruct t)] + else + match M.listCons t with + | some f => + lowerArgsB M X Γ items ++ [.nullOf (M.listStruct t)] ++ + List.replicate items.length (.op (.call f)) + | none => [] def lowerArgsB (M : MCtx) (X : LCtx) (Γ : Nat → Option Ty) : List Expr → List BI | [] => [] | e :: es => lowerB M X Γ false e ++ lowerArgsB M X Γ es diff --git a/aver-cert/assets/wall/current/GrammarSound.lean b/aver-cert/assets/wall/current/GrammarSound.lean index d602f93fd..c18dd032e 100644 --- a/aver-cert/assets/wall/current/GrammarSound.lean +++ b/aver-cert/assets/wall/current/GrammarSound.lean @@ -1372,12 +1372,26 @@ theorem tyOf_interp_inv {parts : List Expr} {T : Ty} · simp at h theorem tyOf_list_inv {t : Ty} {items : List Expr} {T : Ty} - (h : tyOf M n Γ tail (.list t items) = some T) : items = [] ∧ T = .list t := by + (h : tyOf M n Γ tail (.list t items) = some T) : + T = .list t ∧ (items = [] ∨ ∃ f ts, items.isEmpty = false ∧ M.listCons t = some f ∧ + M.sigs f = some (consSig t) ∧ tysOf M n Γ items = some ts ∧ ∀ x ∈ ts, x = t) := by simp only [tyOf] at h split at h - · simp only [Option.some.injEq] at h - exact ⟨rfl, h.symm⟩ - · simp at h + · rename_i he + simp only [Option.some.injEq] at h + exact ⟨h.symm, Or.inl (List.isEmpty_iff.mp he)⟩ + · rename_i he + split at h + · rename_i f ts hf hts + split at h + · rename_i hc + simp only [Option.some.injEq] at h + refine ⟨h.symm, Or.inr ⟨f, ts, by simpa using he, hf, hc.1, hts, ?_⟩⟩ + have h2 := hc.2 + simp only [List.all_eq_true, decide_eq_true_eq] at h2 + exact h2 + · simp at h + · simp at h theorem tyOf_construct_inv {c : CtorTag} {ty : Ty} {args : List Expr} {T : Ty} (h : tyOf M n Γ tail (.construct c ty args) = some T) : @@ -1879,6 +1893,98 @@ the nested argument lists and the arm shapes). The context fixes: the carrier sp host contracts at their indices, an arbitrary opaque `callee`, and a `Contract` for every callee the typing admits. -/ +/-! ## List literals + +A non-empty literal pushes its items, `ref.null`, and calls the cons helper +once per item; the stack then holds the items in reverse, so the calls fold +them into cons cells from the last one in. The helper is known only through +its `Contract` and the model fact that its meaning is `List.prepend`. -/ + +section ListLit +variable {C : Nat} {S : CarrierSpec C} {M : MCtx} + +theorem eraseL_replicate (k : Nat) (i : WInstr) : + eraseL (List.replicate k (BI.op i)) = List.replicate k i := by + induction k with + | zero => simp [eraseL] + | succ k ih => simp [List.replicate_succ, eraseL, eraseI, ih] + +theorem consAll_foldl (t : Ty) (vs : List SVal) : + consAll t vs = vs.reverse.foldl (fun a v => SVal.cons t v a) (.nil t) := by + rw [List.foldl_reverse] + induction vs with + | nil => simp [consAll] + | cons v vs ih => simp [consAll, ih] + +theorem sreprL_append : ∀ {vs1 : List SVal} {ws1 : List WVal} {vs2 : List SVal} + {ws2 : List WVal}, SReprL S M vs1 ws1 → SReprL S M vs2 ws2 → + SReprL S M (vs1 ++ vs2) (ws1 ++ ws2) + | [], [], _, _, _, h2 => by simpa using h2 + | _ :: _, _ :: _, _, _, h1, h2 => ⟨h1.1, sreprL_append h1.2 h2⟩ + | [], _ :: _, _, _, h1, _ => by simp [SReprL] at h1 + | _ :: _, [], _, _, h1, _ => by simp [SReprL] at h1 + +theorem sreprL_reverse : ∀ {vs : List SVal} {ws : List WVal}, + SReprL S M vs ws → SReprL S M vs.reverse ws.reverse + | [], [], _ => by simp [SReprL] + | _ :: _, _ :: _, h => by + simp only [List.reverse_cons] + exact sreprL_append (sreprL_reverse h.2) ⟨h.1, trivial⟩ + | [], _ :: _, h => by simp [SReprL] at h + | _ :: _, [], h => by simp [SReprL] at h + +theorem hasTyL_mem {t : Ty} : ∀ {svs : List SVal} {ts : List Ty}, + HasTyL M svs ts → (∀ x ∈ ts, x = t) → ∀ v ∈ svs, HasTy M v t + | [], _, _, _, v, hv => by simp at hv + | _ :: _, [], h, _, _, _ => by simp [HasTyL] at h + | a :: svs, x :: ts, h, hall, v, hv => by + rcases List.mem_cons.mp hv with rfl | hv + · have hx := hall x (by simp) + subst hx + exact h.1 + · exact hasTyL_mem h.2 (fun y hy => hall y (by simp [hy])) v hv + +/-- `rs.length` calls of the cons helper over `acc :: wrs ++ st`, where `acc` + represents `tl` and `wrs` the items `rs` (last item first), fold them + into `tl` and leave one represented list on `st`. -/ +theorem consCalls_run {host : HostTbl} {ar : Nat → Option Nat} {callee : Callee} + {f : Nat} {t : Ty} {model : List SVal → Option SVal} + (hC : Contract S M host ar callee f (consSig t) model) + (hm : ∀ h tl sv, HasTy M tl (.list t) → model [h, tl] = some sv → sv = .cons t h tl) : + ∀ (rs : List SVal) (wrs : List WVal) (tl : SVal) (acc : WVal) (wl st : List WVal) + (out : Out), + SReprL S M rs wrs → (∀ v ∈ rs, HasTy M v t) → SRepr S M tl acc → + HasTy M tl (.list t) → + wRunF host ar callee (List.replicate rs.length (.call f)) wl (acc :: (wrs ++ st)) = + some out → + ∃ w, out = .ok wl (w :: st) ∧ + SRepr S M (rs.foldl (fun a v => SVal.cons t v a) tl) w ∧ + HasTy M (rs.foldl (fun a v => SVal.cons t v a) tl) (.list t) + | [], [], tl, acc, wl, st, out, _, _, hacc, htl, hrun => by + simp only [List.length_nil, List.replicate_zero, List.nil_append, wRunF, + Option.some.injEq] at hrun + subst hrun + exact ⟨acc, rfl, hacc, htl⟩ + | [], _ :: _, _, _, _, _, _, hr, _, _, _, _ => by simp [SReprL] at hr + | _ :: _, [], _, _, _, _, _, hr, _, _, _, _ => by simp [SReprL] at hr + | r :: rs, w :: wrs, tl, acc, wl, st, out, hr, hall, hacc, htl, hrun => by + have har2 : ar f = some 2 := by simpa [consSig] using hC.2.1 + have hpop : popArgs 2 (acc :: w :: (wrs ++ st)) = some ([w, acc], wrs ++ st) := + popArgs_two w acc _ + simp only [List.length_cons, List.replicate_succ, List.cons_append] at hrun + cases hc : callee f [w, acc] with + | none => simp [wRunF, hC.1, har2, hpop, hc] at hrun + | some r1 => + simp only [wRunF, hC.1, har2, hpop, hc] at hrun + obtain ⟨sv, hmv, hsv, hT⟩ := hC.2.2 [r, tl] [w, acc] r1 + ⟨hall r (by simp), htl, trivial⟩ ⟨hr.1, hacc, trivial⟩ hc + have hsv' := hm r tl sv htl hmv + subst hsv' + exact consCalls_run hC hm rs wrs (.cons t r tl) r1 wl st out hr.2 + (fun v hv => hall v (by simp [hv])) hsv hT hrun + +end ListLit + section Agreement variable {C : Nat} (S : CarrierSpec C) (box add sub mul cmp eq neg : List WVal → Option WVal) @@ -1895,8 +2001,10 @@ variable {C : Nat} (S : CarrierSpec C) (F : Nat → List SVal → Option SVal) (hCallees : ∀ f sig, M.sigs f = some sig → Contract S M host ar callee f sig (F f)) + (hConsF : ∀ t f, M.listCons t = some f → ∀ h tl sv, HasTy M tl (.list t) → + F f [h, tl] = some sv → sv = .cons t h tl) (X : LCtx) -include Ctr hNegC hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R hCallees +include Ctr hNegC hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R hCallees hConsF set_option hygiene false in /-- The size side condition of a recursive call in the agreement proofs: the @@ -2962,10 +3070,28 @@ theorem agreement_step : subst hout exact ⟨.s bs, by simp [eval, hevs, hbs], by simp [HasTy], res_ok (by simp [SRepr]) hl1⟩ | .list t items, hsz, Γ, env, tail, T, wl, st, out, hty, henv, hl, hrun => by - obtain ⟨rfl, rfl⟩ := tyOf_list_inv hty - simp [lowerW, lowerB, eraseL, eraseI, wRunF] at hrun - subst hrun - exact ⟨.nil t, by simp [eval], by simp [HasTy], res_ok (by simp [SRepr]) hl⟩ + obtain ⟨rfl, hcase⟩ := tyOf_list_inv hty + rcases hcase with rfl | ⟨f, ts, hne, hf, hsig, hts, hall⟩ + · simp [lowerW, lowerB, eraseL, eraseI, wRunF] at hrun + subst hrun + exact ⟨.nil t, by simp [eval], by simp [HasTy], res_ok (by simp [SRepr]) hl⟩ + · simp only [lowerW, lowerB, hne, hf, Bool.false_eq_true, ↓reduceIte, eraseL_append, + List.append_assoc] at hrun + obtain ⟨o1, h1, hseq⟩ := run_split hrun + obtain ⟨svs, ws, wl1, rfl, hevs, hTs, hrep, hl1⟩ := + agreementArgs items Γ env ts wl st o1 hts henv hl h1 + have hlen : items.length = svs.reverse.length := by + rw [List.length_reverse, hasTyL_length hTs, tysOf_length hts] + simp only [seqOut, eraseL, eraseI, eraseL_replicate, List.cons_append, + List.nil_append, wRunF, hlen] at hseq + obtain ⟨w, rfl, hw, hT⟩ := consCalls_run (hCallees f (consSig t) hsig) + (hConsF t f hf) svs.reverse ws.reverse (.nil t) .null wl1 st out + (sreprL_reverse hrep) (fun v hv => hasTyL_mem hTs hall v (List.mem_reverse.mp hv)) + (by simp [SRepr]) (by simp [HasTy]) hseq + refine ⟨consAll t svs, ?_, ?_, res_ok ?_ hl1⟩ + · simp [eval, hne, hevs] + · rw [consAll_foldl]; exact hT + · rw [consAll_foldl]; exact hw theorem agreementArgs_step : ∀ (es : List Expr) (hsz : sizeOf es < n + 1) (Γ : Nat → Option Ty) (env : Nat → Option SVal) (Ts : List Ty) @@ -3756,23 +3882,23 @@ theorem agreement_upto : ∀ n : Nat, obtain ⟨ih0, ih1, ih2, ih3, ih4, ih5, ih6, ih7, ih8⟩ := ih refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ · intros - apply agreement_step S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X n ih0 ih1 ih2 ih3 ih4 ih5 ih6 ih7 ih8 _ ‹_› <;> assumption + apply agreement_step S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X n ih0 ih1 ih2 ih3 ih4 ih5 ih6 ih7 ih8 _ ‹_› <;> assumption · intros - apply agreementArgs_step S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X n ih0 ih1 ih2 ih3 ih4 ih5 ih6 ih7 ih8 _ ‹_› <;> assumption + apply agreementArgs_step S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X n ih0 ih1 ih2 ih3 ih4 ih5 ih6 ih7 ih8 _ ‹_› <;> assumption · intros - apply agreementIntArms_step S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X n ih0 ih1 ih2 ih3 ih4 ih5 ih6 ih7 ih8 _ ‹_› <;> assumption + apply agreementIntArms_step S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X n ih0 ih1 ih2 ih3 ih4 ih5 ih6 ih7 ih8 _ ‹_› <;> assumption · intros - apply agreementBoolArms_step S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X n ih0 ih1 ih2 ih3 ih4 ih5 ih6 ih7 ih8 _ ‹_› <;> assumption + apply agreementBoolArms_step S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X n ih0 ih1 ih2 ih3 ih4 ih5 ih6 ih7 ih8 _ ‹_› <;> assumption · intros - apply agreementOptArms_step S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X n ih0 ih1 ih2 ih3 ih4 ih5 ih6 ih7 ih8 _ ‹_› <;> assumption + apply agreementOptArms_step S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X n ih0 ih1 ih2 ih3 ih4 ih5 ih6 ih7 ih8 _ ‹_› <;> assumption · intros - apply agreementResArms_step S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X n ih0 ih1 ih2 ih3 ih4 ih5 ih6 ih7 ih8 _ ‹_› <;> assumption + apply agreementResArms_step S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X n ih0 ih1 ih2 ih3 ih4 ih5 ih6 ih7 ih8 _ ‹_› <;> assumption · intros - apply agreementVarArms_step S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X n ih0 ih1 ih2 ih3 ih4 ih5 ih6 ih7 ih8 _ ‹_› <;> assumption + apply agreementVarArms_step S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X n ih0 ih1 ih2 ih3 ih4 ih5 ih6 ih7 ih8 _ ‹_› <;> assumption · intros - apply agreementStrArms_step S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X n ih0 ih1 ih2 ih3 ih4 ih5 ih6 ih7 ih8 _ ‹_› <;> assumption + apply agreementStrArms_step S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X n ih0 ih1 ih2 ih3 ih4 ih5 ih6 ih7 ih8 _ ‹_› <;> assumption · intros - apply agreementTupArms_step S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X n ih0 ih1 ih2 ih3 ih4 ih5 ih6 ih7 ih8 _ ‹_› <;> assumption + apply agreementTupArms_step S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X n ih0 ih1 ih2 ih3 ih4 ih5 ih6 ih7 ih8 _ ‹_› <;> assumption theorem agreement : ∀ (e : Expr) (Γ : Nat → Option Ty) (env : Nat → Option SVal) (tail : Bool) (T : Ty) @@ -3786,7 +3912,7 @@ theorem agreement : := by intro e intros - apply (agreement_upto S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X (sizeOf e + 1)).1 e <;> first | assumption | exact Nat.lt_succ_self _ + apply (agreement_upto S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X (sizeOf e + 1)).1 e <;> first | assumption | exact Nat.lt_succ_self _ theorem agreementArgs : ∀ (es : List Expr) (Γ : Nat → Option Ty) (env : Nat → Option SVal) (Ts : List Ty) @@ -3801,7 +3927,7 @@ theorem agreementArgs : := by intro es intros - apply (agreement_upto S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X (sizeOf es + 1)).2.1 es <;> first | assumption | exact Nat.lt_succ_self _ + apply (agreement_upto S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X (sizeOf es + 1)).2.1 es <;> first | assumption | exact Nat.lt_succ_self _ /-- The Int literal cascade: `sc` is the subject's code, re-run per literal arm; every run yields the same Int `x` (evaluation is pure). -/ @@ -3820,7 +3946,7 @@ theorem agreementIntArms : := by intro arms intros - apply (agreement_upto S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X (sizeOf arms + 1)).2.2.1 arms <;> first | assumption | exact Nat.lt_succ_self _ + apply (agreement_upto S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X (sizeOf arms + 1)).2.2.1 arms <;> first | assumption | exact Nat.lt_succ_self _ /-- The two-arm Bool match: one `if` on the subject's `i32`. -/ theorem agreementBoolArms : @@ -3835,7 +3961,7 @@ theorem agreementBoolArms : := by intro arms intros - apply (agreement_upto S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X (sizeOf arms + 1)).2.2.2.1 arms <;> first | assumption | exact Nat.lt_succ_self _ + apply (agreement_upto S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X (sizeOf arms + 1)).2.2.2.1 arms <;> first | assumption | exact Nat.lt_succ_self _ /-- The two-arm Option match over the subject held in the scratch. -/ theorem agreementOptArms : @@ -3850,7 +3976,7 @@ theorem agreementOptArms : := by intro arms intros - apply (agreement_upto S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X (sizeOf arms + 1)).2.2.2.2.1 arms <;> first | assumption | exact Nat.lt_succ_self _ + apply (agreement_upto S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X (sizeOf arms + 1)).2.2.2.2.1 arms <;> first | assumption | exact Nat.lt_succ_self _ /-- The two-arm Result match: `Ok` in the `then` (payload field 1), `Err` in the `else` (payload field 2). -/ @@ -3866,7 +3992,7 @@ theorem agreementResArms : := by intro arms intros - apply (agreement_upto S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X (sizeOf arms + 1)).2.2.2.2.2.1 arms <;> first | assumption | exact Nat.lt_succ_self _ + apply (agreement_upto S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X (sizeOf arms + 1)).2.2.2.2.2.1 arms <;> first | assumption | exact Nat.lt_succ_self _ /-- The user-variant `ref.test` cascade over the subject held in the scratch. `coversB` says some remaining arm reaches the subject's @@ -3888,7 +4014,7 @@ theorem agreementVarArms : := by intro arms intros - apply (agreement_upto S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X (sizeOf arms + 1)).2.2.2.2.2.2.1 arms <;> first | assumption | exact Nat.lt_succ_self _ + apply (agreement_upto S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X (sizeOf arms + 1)).2.2.2.2.2.2.1 arms <;> first | assumption | exact Nat.lt_succ_self _ /-- The String literal cascade over the subject held in the scratch: each literal arm compares through `__wasmgc_string_eq`; `_` ends it. -/ @@ -3904,7 +4030,7 @@ theorem agreementStrArms : := by intro arms intros - apply (agreement_upto S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X (sizeOf arms + 1)).2.2.2.2.2.2.2.1 arms <;> first | assumption | exact Nat.lt_succ_self _ + apply (agreement_upto S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X (sizeOf arms + 1)).2.2.2.2.2.2.2.1 arms <;> first | assumption | exact Nat.lt_succ_self _ /-- The flat tuple destructure over the subject held in the scratch. -/ theorem agreementTupArms : @@ -3921,7 +4047,7 @@ theorem agreementTupArms : := by intro arms intros - apply (agreement_upto S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X (sizeOf arms + 1)).2.2.2.2.2.2.2.2 arms <;> first | assumption | exact Nat.lt_succ_self _ + apply (agreement_upto S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X (sizeOf arms + 1)).2.2.2.2.2.2.2.2 arms <;> first | assumption | exact Nat.lt_succ_self _ end Agreement @@ -3940,6 +4066,37 @@ theorem groupModel_member (outer : Nat → Nat → List SVal → Option SVal) eval (groupModel outer G fuel) (argsEnv args) p.body := by simp [groupModel, hG] +/-- The wall's own cons plan means `List.prepend` at every fuel. -/ +theorem groupModel_consPlan (outer : Nat → Nat → List SVal → Option SVal) + (G : Nat → Option FnPlan) {M : MCtx} {f : Nat} {p : FnPlan} {t : Ty} + (hG : G f = some p) (hb : p.body = consBody) : + ∀ k h tl sv, HasTy M tl (.list t) → groupModel outer G k f [h, tl] = some sv → + sv = .cons t h tl := by + intro k h tl sv htl hm + cases k with + | zero => simp [groupModel, hG] at hm + | succ k => + rw [groupModel_member outer G hG, hb] at hm + cases tl <;> simp only [HasTy] at htl + · subst htl + simp [consBody, eval, evalArgs, argsEnv, builtinEval] at hm + subst hm; rfl + · obtain ⟨rfl, -, -⟩ := htl + simp [consBody, eval, evalArgs, argsEnv, builtinEval] at hm + subst hm; rfl + +theorem isConsPlan_body {p : FnPlan} (h : isConsPlan p = true) : + p.body = consBody := by + unfold isConsPlan at h + revert h + split + · rename_i heq + intro _ + rw [heq] + rfl + · intro hb + cases hb + theorem envTy_args {M : MCtx} {svs : List SVal} {ts : List Ty} (h : HasTyL M svs ts) : EnvTy M (argsEnv svs) (paramsΓ ts) := by intro i @@ -3985,7 +4142,9 @@ theorem fn_certified_group {C : Nat} (S : CarrierSpec C) FnCertified S M code host f sig (fun fuel => outer fuel f)) (hMem : ∀ f p, G f = some p → M.sigs f = some p.sig ∧ planTyped M p = true ∧ host f = none ∧ - code f = some (fnCode M p)) : + code f = some (fnCode M p)) + (hCons : ∀ t f, M.listCons t = some f → ∀ k h tl sv, HasTy M tl (.list t) → + groupModel outer G k f [h, tl] = some sv → sv = .cons t h tl) : ∀ f p, G f = some p → FnCertified S M code host f p.sig (fun fuel => groupModel outer G fuel f) := by @@ -4047,6 +4206,7 @@ theorem fn_certified_group {C : Nat} (S : CarrierSpec C) obtain ⟨sv, hev, hT, hres⟩ := agreement S box add sub mul cmp eq neg Ctr hNegC host (fun g => (code g).map (·.arity)) (fun g as => wFuncN code host k g as) M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R (groupModel outer G k) hCallees + (fun t g hg h tl sv htl hm => hCons t g hg k h tl sv htl hm) p.lctx p.body (paramsΓ p.sig.params) (argsEnv svs) true p.sig.ret (initLocals (fnCode M p) ws) [] o hty (envTy_args hTs) hLR hw have hm : groupModel outer G (k + 1) f svs = some sv := by diff --git a/aver-cert/assets/wall/current/GrammarTotal.lean b/aver-cert/assets/wall/current/GrammarTotal.lean index 593f3e967..988fc8285 100644 --- a/aver-cert/assets/wall/current/GrammarTotal.lean +++ b/aver-cert/assets/wall/current/GrammarTotal.lean @@ -334,6 +334,8 @@ variable {C : Nat} (S : CarrierSpec C) (F : Nat → List SVal → Option SVal) (hCallees : ∀ f sig, M.sigs f = some sig → Contract S M host ar callee f sig (F f)) + (hConsF : ∀ t f, M.listCons t = some f → ∀ h tl sv, HasTy M tl (.list t) → + F f [h, tl] = some sv → sv = .cons t h tl) (X : LCtx) (hBoxT : ∀ k : Int, -(2 ^ 63 : Int) ≤ k → k < 2 ^ 63 → ∃ w, box [.i64v k] = some w) (hAddT : ∀ a b va vb, S.Repr a va → S.Repr b vb → ∃ w, add [va, vb] = some w) @@ -345,7 +347,7 @@ variable {C : Nat} (S : CarrierSpec C) (hCallP : calls = true → ∀ g sig, mem g = true → M.sigs g = some sig → ∀ svs ws, HasTyL M (.i (n - 1) :: svs) sig.params → SReprL S M (.i (n - 1) :: svs) ws → ∃ r, callee g ws = some r) -include Ctr hNegC hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R hCallees hBoxT hAddT hSubT hMulT +include Ctr hNegC hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R hCallees hConsF hBoxT hAddT hSubT hMulT hSig hCallP mutual @@ -381,13 +383,13 @@ theorem progress : · simp only [lowerW, lowerB, htl, hA, ↓reduceIte, eraseL_append, eraseL, eraseI] obtain ⟨o1, h1⟩ := progress l Γ env false .int wl st htl0 hΓ htl henv hl h0 obtain ⟨sv1, _, hT1, hres1⟩ := agreement S box add sub mul cmp eq neg Ctr hNegC host ar - callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X l Γ env false .int + callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X l Γ env false .int wl st o1 htl henv hl h1 obtain ⟨wl1, w1, rfl, hw1, hl1⟩ := res_false hres1 obtain ⟨a, rfl⟩ := hasTy_int hT1 obtain ⟨o2, h2⟩ := progress r Γ env false .int wl1 (w1 :: st) htr0 hΓ htr henv hl1 h0 obtain ⟨sv2, _, hT2, hres2⟩ := agreement S box add sub mul cmp eq neg Ctr hNegC host ar - callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X r Γ env false .int + callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X r Γ env false .int wl1 (w1 :: st) o2 htr henv hl1 h2 obtain ⟨wl2, w2, rfl, hw2, _⟩ := res_false hres2 obtain ⟨b, rfl⟩ := hasTy_int hT2 @@ -417,7 +419,7 @@ theorem progress : obtain ⟨o1, h1⟩ := progressArgs args Γ env sig.params wl st hargs hΓ hts henv hl h0 obtain ⟨svs, ws, wl1, rfl, hevs, hTs, hrep, _⟩ := agreementArgs S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd - hSub hMul hNeg hCmp hEq R F hCallees X args Γ env sig.params wl st o1 hts henv hl h1 + hSub hMul hNeg hCmp hEq R F hCallees hConsF X args Γ env sig.params wl st o1 hts henv hl h1 obtain ⟨rest, rfl⟩ := descentHead_eq hdh have hd : eval F env (.binOp .sub (.local 0) (.literal (.int 1))) = some (.i (n - 1)) := by simp [eval, h0, intBin] @@ -444,7 +446,7 @@ theorem progress : obtain ⟨o1, h1⟩ := progressArgs args Γ env sig.params wl st hargs hΓ hts henv hl h0 obtain ⟨svs, ws, wl1, rfl, hevs, hTs, hrep, _⟩ := agreementArgs S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd - hSub hMul hNeg hCmp hEq R F hCallees X args Γ env sig.params wl st o1 hts henv hl h1 + hSub hMul hNeg hCmp hEq R F hCallees hConsF X args Γ env sig.params wl st o1 hts henv hl h1 obtain ⟨rest, rfl⟩ := descentHead_eq hdh have hd : eval F env (.binOp .sub (.local 0) (.literal (.int 1))) = some (.i (n - 1)) := by simp [eval, h0, intBin] @@ -494,7 +496,7 @@ theorem progressArgs : simp only [lowerArgsW, lowerArgsB, eraseL_append] obtain ⟨o1, h1⟩ := progress e Γ env false t wl st htot.1 hΓ hte henv hl h0 obtain ⟨sv, _, _, hres⟩ := agreement S box add sub mul cmp eq neg Ctr hNegC host ar - callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X e Γ env false t + callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X e Γ env false t wl st o1 hte henv hl h1 obtain ⟨wl1, w, rfl, _, hl1⟩ := res_false hres obtain ⟨o2, h2⟩ := progressArgs es Γ env ts wl1 (w :: st) htot.2 hΓ htes henv hl1 h0 @@ -574,6 +576,8 @@ theorem fn_certified_total {C : Nat} (S : CarrierSpec C) (hMem : ∀ f p, G f = some p → M.sigs f = some p.sig ∧ planTyped M p = true ∧ host f = none ∧ code f = some (fnCode M p)) + (hCons : ∀ t f, M.listCons t = some f → ∀ k h tl sv, HasTy M tl (.list t) → + groupModel outer G k f [h, tl] = some sv → sv = .cons t h tl) (hBoxT : ∀ k : Int, -(2 ^ 63 : Int) ≤ k → k < 2 ^ 63 → ∃ w, box [.i64v k] = some w) (hAddT : ∀ a b va vb, S.Repr a va → S.Repr b vb → ∃ w, add [va, vb] = some w) (hSubT : ∀ a b va vb, S.Repr a va → S.Repr b vb → ∃ w, sub [va, vb] = some w) @@ -585,7 +589,7 @@ theorem fn_certified_total {C : Nat} (S : CarrierSpec C) FnCertified S M code host f p.sig (fun fuel => groupModel outer G fuel f) ∧ FnTotal S M code host f p.sig (fun fuel => groupModel outer G fuel f) := by have hCert := fn_certified_group S box add sub mul cmp eq neg Ctr hNegC code host M hCarrier - hBox hAdd hSub hMul hNeg hCmp hEq R G outer hOuter hMem + hBox hAdd hSub hMul hNeg hCmp hEq R G outer hOuter hMem hCons have hSigOf : ∀ f p, G f = some p → M.sigs f = some p.sig := fun f p h => (hMem f p h).1 have hSig : ∀ g sig, mem g = true → M.sigs g = some sig → sig.ret = .int ∨ sig.ret = .bool := by intro g sig hg hs @@ -650,7 +654,8 @@ theorem fn_certified_total {C : Nat} (S : CarrierSpec C) (ar := fun g => (code g).map (·.arity)) (callee := fun g as => wFuncN code host m g as) (M := M) (hCarrier := hCarrier) (hBox := hBox) (hAdd := hAdd) (hSub := hSub) (hMul := hMul) (hNeg := hNeg) (hCmp := hCmp) (hEq := hEq) (R := R) - (F := groupModel outer G m) (hCallees := hCallees) (X := p.lctx) (hBoxT := hBoxT) + (F := groupModel outer G m) (hCallees := hCallees) + (hConsF := fun t g hg h tl sv htl hm => hCons t g hg m h tl sv htl hm) (X := p.lctx) (hBoxT := hBoxT) (hAddT := hAddT) (hSubT := hSubT) (mulOk := mulOk) (hMulT := hMulT) (mem := mem) (calls := false) (n := n) (hSig := hSig) (hCallP := fun h => by cases h) base _ _ true p.sig.ret _ [] hbase hΓ hbty henv hLR h0 @@ -671,7 +676,8 @@ theorem fn_certified_total {C : Nat} (S : CarrierSpec C) (ar := fun g => (code g).map (·.arity)) (callee := fun g as => wFuncN code host m g as) (M := M) (hCarrier := hCarrier) (hBox := hBox) (hAdd := hAdd) (hSub := hSub) (hMul := hMul) (hNeg := hNeg) (hCmp := hCmp) (hEq := hEq) (R := R) - (F := groupModel outer G m) (hCallees := hCallees) (X := p.lctx) (hBoxT := hBoxT) + (F := groupModel outer G m) (hCallees := hCallees) + (hConsF := fun t g hg h tl sv htl hm => hCons t g hg m h tl sv htl hm) (X := p.lctx) (hBoxT := hBoxT) (hAddT := hAddT) (hSubT := hSubT) (mulOk := mulOk) (hMulT := hMulT) (mem := mem) (calls := true) (n := n) (hSig := hSig) (hCallP := hCallP) step _ _ true p.sig.ret _ [] hstep hΓ hsty henv hLR h0 @@ -679,6 +685,7 @@ theorem fn_certified_total {C : Nat} (S : CarrierSpec C) obtain ⟨sv, _, _, hres⟩ := agreement S box add sub mul cmp eq neg Ctr hNegC host (fun g => (code g).map (·.arity)) (fun g as => wFuncN code host m g as) M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R (groupModel outer G m) hCallees + (fun t g hg h tl sv htl hm => hCons t g hg m h tl sv htl hm) p.lctx p.body (paramsΓ p.sig.params) (argsEnv (.i n :: tl)) true p.sig.ret (initLocals (fnCode M p) (w0 :: ws')) [] out hty henv hLR hout unfold wFuncN @@ -734,6 +741,8 @@ theorem fn_certified_total_of_check {C : Nat} (S : CarrierSpec C) (hMem : ∀ f p, G f = some p → M.sigs f = some p.sig ∧ planTyped M p = true ∧ host f = none ∧ code f = some (fnCode M p)) + (hCons : ∀ t f, M.listCons t = some f → ∀ k h tl sv, HasTy M tl (.list t) → + groupModel outer G k f [h, tl] = some sv → sv = .cons t h tl) (hBoxT : ∀ k : Int, -(2 ^ 63 : Int) ≤ k → k < 2 ^ 63 → ∃ w, box [.i64v k] = some w) (hAddT : ∀ a b va vb, S.Repr a va → S.Repr b vb → ∃ w, add [va, vb] = some w) (hSubT : ∀ a b va vb, S.Repr a va → S.Repr b vb → ∃ w, sub [va, vb] = some w) @@ -743,7 +752,7 @@ theorem fn_certified_total_of_check {C : Nat} (S : CarrierSpec C) FnTotal S M code host f p.sig (fun fuel => groupModel outer G fuel f) := by obtain ⟨_, hall⟩ := checkTermGroup_spec hck refine fn_certified_total S box add sub mul cmp eq neg Ctr hNegC code host M hCarrier hBox hAdd - hSub hMul hNeg hCmp hEq R G outer hOuter hMem hBoxT hAddT hSubT (role == .mul) + hSub hMul hNeg hCmp hEq R G outer hOuter hMem hCons hBoxT hAddT hSubT (role == .mul) (fun h => hMulT (by simpa using h)) (memOf ms) ?_ ?_ · intro g hg obtain ⟨m, hm, hmg⟩ := List.any_eq_true.mp hg diff --git a/aver-cert/assets/wall/current/SchemaCore.lean b/aver-cert/assets/wall/current/SchemaCore.lean index cef070fa4..fcfac131d 100644 --- a/aver-cert/assets/wall/current/SchemaCore.lean +++ b/aver-cert/assets/wall/current/SchemaCore.lean @@ -67,6 +67,10 @@ structure TypeTable where opaques : List (Nat × Nat) /-- The passive data segment holding each string literal's bytes. -/ strSegs : List (List Nat × Nat) + /-- The cons helper of each `List` a non-empty literal builds: the + function the literal calls once per item. The acceptance pins its plan + to the wall's cons plan (`Grammar.isConsPlan`). -/ + listCons : List (Ty × Nat) := [] deriving Repr /-- One planned function: the plan is the function's MIR body printed 1:1 diff --git a/aver-cert/assets/wall/current/TypeTable.lean b/aver-cert/assets/wall/current/TypeTable.lean index 56cbf0bbb..9c785a5ac 100644 --- a/aver-cert/assets/wall/current/TypeTable.lean +++ b/aver-cert/assets/wall/current/TypeTable.lean @@ -103,7 +103,8 @@ def mctxOf (s : Subject) (tt : TypeTable) (fns : List FnEntry) : MCtx := divmod := idxOr 23 (roleOf s.hostRoleTable (·.divmod)) vecStruct := lookupTy 20 tt.vecs listStruct := lookupTy 21 tt.lists - opaqueStruct := lookupNat 22 tt.opaques } + opaqueStruct := lookupNat 22 tt.opaques + listCons := fun t => (tt.listCons.find? fun x => decide (x.1 = t)).map (·.2) } /-! ## The opening rec group, raw and decoded diff --git a/aver-cert/src/engine/plan.rs b/aver-cert/src/engine/plan.rs index b376f75a0..b4a0309c2 100644 --- a/aver-cert/src/engine/plan.rs +++ b/aver-cert/src/engine/plan.rs @@ -175,6 +175,10 @@ pub struct PlanTypeTable { pub lists: Vec<(PlanTy, u32)>, pub opaques: Vec<(u32, u32)>, pub str_segs: Vec<(Vec, u32)>, + /// The cons helper of each `List` a non-empty literal builds + /// (`Schema.TypeTable.listCons`): the function the literal calls once per + /// item, whose plan must be exactly [`FnPlan::cons`]. + pub list_cons: Vec<(PlanTy, u32)>, } /// One user function as the compiler printed it: its wasm function index, its @@ -445,6 +449,21 @@ impl PlanExpr { } impl FnPlan { + /// `Grammar.isConsPlan`'s plan: the cons helper of `List`, one + /// `List.prepend` over its two parameters and no declared local. + pub fn cons(t: &PlanTy) -> FnPlan { + FnPlan { + params: vec![t.clone(), PlanTy::List(Box::new(t.clone()))], + ret: PlanTy::List(Box::new(t.clone())), + nslots: 2, + locals: Vec::new(), + body: PlanExpr::Call( + PlanCallee::Builtin(PlanBuiltin::ListPrepend), + vec![PlanExpr::Local(0), PlanExpr::Local(1)], + ), + } + } + /// The Lean `Grammar.FnPlan` term. pub fn lean(&self) -> String { format!( @@ -618,13 +637,23 @@ 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); + // Written only when present: the wall's default is the empty list, + // so a module without list literals renders as before. + let cons = if self.list_cons.is_empty() { + String::new() + } else { + format!( + ",\n listCons := {}", + field("listCons", "Ty × Nat", &pairs(&self.list_cons)) + ) + }; 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", + "{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}{cons} }}\n\n", lean_opt_nat(self.carrier), lean_opt_nat(self.mag), lean_opt_nat(self.str_), diff --git a/aver-cert/src/engine/plan_check.rs b/aver-cert/src/engine/plan_check.rs index 782d114e7..57b97623d 100644 --- a/aver-cert/src/engine/plan_check.rs +++ b/aver-cert/src/engine/plan_check.rs @@ -137,6 +137,11 @@ impl<'a> MCtx<'a> { idx_or(21, self.tt.lists.iter().find(|l| &l.0 == t).map(|l| l.1)) } + /// `MCtx.listCons`: the declared cons helper of `List`. + fn list_cons(&self, t: &PlanTy) -> Option { + self.tt.list_cons.iter().find(|l| &l.0 == t).map(|l| l.1) + } + fn opaque_struct(&self, tid: u32) -> u64 { idx_or(22, self.tt.opaques.iter().find(|o| o.0 == tid).map(|o| o.1)) } @@ -469,7 +474,16 @@ impl MCtx<'_> { } PlanExpr::Construct(c, ty, args) => self.ctor_ty(*c, ty, &self.tys_of(n, g, args)?), PlanExpr::Interp(parts) => all_str(&self.tys_of(n, g, parts)?).then_some(PlanTy::Str), - PlanExpr::List(t, items) => items.is_empty().then(|| PlanTy::List(Box::new(t.clone()))), + PlanExpr::List(t, items) => { + let lt = PlanTy::List(Box::new(t.clone())); + if items.is_empty() { + return Some(lt); + } + let f = self.list_cons(t)?; + let ts = self.tys_of(n, g, items)?; + let sig_ok = self.sigs.get(&f) == Some(&(vec![t.clone(), lt.clone()], lt.clone())); + (sig_ok && ts.iter().all(|x| x == t)).then_some(lt) + } PlanExpr::Match(s, arms) => match self.ty_of(n, g, false, s)? { PlanTy::Int => { matches!(arms.first(), Some((PlanPat::LitInt(_), _))).then_some(())?; @@ -1358,7 +1372,18 @@ impl MCtx<'_> { out.extend(self.concat(parts.len())); out } - PlanExpr::List(t, _) => vec![BI::NullOf(self.list_struct(t))], + PlanExpr::List(t, items) => { + if items.is_empty() { + return vec![BI::NullOf(self.list_struct(t))]; + } + let Some(f) = self.list_cons(t) else { + return vec![]; + }; + let mut out = self.lower_args(x, g, items); + out.push(BI::NullOf(self.list_struct(t))); + out.extend(items.iter().map(|_| BI::Op(WI::Call(u64::from(f))))); + out + } } } @@ -1750,7 +1775,7 @@ fn lowered_calls(bs: &[BI], out: &mut Vec) { /// `AcceptedArtifact.callTargets`. fn call_targets(e: &PlanExpr, out: &mut Vec) { match e { - PlanExpr::Literal(_) | PlanExpr::Local(_) | PlanExpr::List(_, _) => {} + PlanExpr::Literal(_) | PlanExpr::Local(_) => {} PlanExpr::Let(_, v, b) => { call_targets(v, out); call_targets(b, out); @@ -1762,7 +1787,8 @@ fn call_targets(e: &PlanExpr, out: &mut Vec) { PlanExpr::Call(_, args) | PlanExpr::RecordCreate(_, args) | PlanExpr::Construct(_, _, args) - | PlanExpr::Interp(args) => args.iter().for_each(|a| call_targets(a, out)), + | PlanExpr::Interp(args) + | PlanExpr::List(_, args) => args.iter().for_each(|a| call_targets(a, out)), PlanExpr::BinOp(_, l, r) => { call_targets(l, out); call_targets(r, out); @@ -1780,6 +1806,55 @@ fn call_targets(e: &PlanExpr, out: &mut Vec) { } } +/// The element types of the non-empty list literals of a plan: each one +/// calls its type's cons helper (`MCtx.listCons`), which must therefore be +/// offered with the plan. +fn literal_list_types(e: &PlanExpr, out: &mut Vec) { + match e { + PlanExpr::Literal(_) | PlanExpr::Local(_) => {} + PlanExpr::Let(_, v, b) | PlanExpr::BinOp(_, v, b) => { + literal_list_types(v, out); + literal_list_types(b, out); + } + PlanExpr::List(t, items) => { + if !items.is_empty() { + out.push(t.clone()); + } + items.iter().for_each(|a| literal_list_types(a, out)); + } + PlanExpr::Call(_, args) + | PlanExpr::TailCall(_, args) + | PlanExpr::RecordCreate(_, args) + | PlanExpr::Construct(_, _, args) + | PlanExpr::Interp(args) => args.iter().for_each(|a| literal_list_types(a, out)), + PlanExpr::Neg(x) | PlanExpr::Project(_, _, x) => literal_list_types(x, out), + PlanExpr::If(c, t, el) => { + literal_list_types(c, out); + literal_list_types(t, out); + literal_list_types(el, out); + } + PlanExpr::Match(s, arms) => { + literal_list_types(s, out); + arms.iter().for_each(|(_, b)| literal_list_types(b, out)); + } + } +} + +/// The functions a plan runs: its calls (`call_targets`) and the cons +/// helpers of its non-empty list literals. +fn plan_targets(tt: &PlanTypeTable, p: &FnPlan) -> Vec { + let mut out = Vec::new(); + call_targets(&p.body, &mut out); + let mut tys = Vec::new(); + literal_list_types(&p.body, &mut tys); + for t in tys { + if let Some((_, f)) = tt.list_cons.iter().find(|l| l.0 == t) { + out.push(*f); + } + } + out +} + /// `GrammarLower.exprLits`: every string literal a plan lowers to /// `array.new_data`. fn string_lits<'e>(e: &'e PlanExpr, out: &mut Vec<&'e [u8]>) { diff --git a/aver-cert/src/engine/produce.rs b/aver-cert/src/engine/produce.rs index 5c569c3c4..fbeaa94e2 100644 --- a/aver-cert/src/engine/produce.rs +++ b/aver-cert/src/engine/produce.rs @@ -430,6 +430,12 @@ impl Cited { .filter(|s| self.segs.contains(&s.0)) .cloned() .collect(), + list_cons: tt + .list_cons + .iter() + .filter(|l| has(PlanTy::List(Box::new(l.0.clone())))) + .cloned() + .collect(), } } } @@ -505,8 +511,7 @@ fn check_candidate( plan: &FnPlan, candidates: &BTreeSet, ) -> Option { - let mut targets = Vec::new(); - call_targets(&plan.body, &mut targets); + let targets = plan_targets(m.tt, plan); if let Some(t) = targets.iter().find(|t| !candidates.contains(t)) { return Some(format!("calls function {t}, which has no certified plan")); } @@ -602,6 +607,18 @@ pub fn analyze( let mut types = plans.types.clone(); confirm_type_table(&facts, &mut types); + // A cons helper is never a user function: an index the compiler also + // printed a user plan for is dropped (its literals then decline). + types + .list_cons + .retain(|(_, f)| !plans.fns.iter().any(|p| p.func_idx == *f)); + // The cons helper of each literal's list type is offered with the wall's + // own cons plan; the byte check below confirms the helper is exactly it. + let cons_plans: Vec<(u32, FnPlan)> = types + .list_cons + .iter() + .map(|(t, f)| (*f, FnPlan::cons(t))) + .collect(); let mut reasons: BTreeMap = BTreeMap::new(); let mut plan_of: BTreeMap = BTreeMap::new(); @@ -615,6 +632,9 @@ pub fn analyze( } } } + for (f, p) in &cons_plans { + plan_of.entry(*f).or_insert(p); + } let mut candidates: BTreeSet = plan_of.keys().copied().collect(); loop { let fns: Vec<(u32, &FnPlan)> = candidates.iter().map(|f| (*f, plan_of[f])).collect(); @@ -638,8 +658,7 @@ pub fn analyze( // reaches. let mut edges: BTreeMap> = BTreeMap::new(); for f in &candidates { - let mut t = Vec::new(); - call_targets(&plan_of[f].body, &mut t); + let mut t = plan_targets(&types, plan_of[f]); t.sort_unstable(); t.dedup(); edges.insert(*f, t); @@ -758,7 +777,11 @@ pub fn analyze( let mut cited = Cited::default(); entries.iter().for_each(|e| cited.plan(&e.plan)); cited.close(&types); - let types = cited.restrict(&types); + let mut types = cited.restrict(&types); + // `AcceptedArtifact.consPinned`: every declared cons helper is planned. + types + .list_cons + .retain(|(_, f)| entries.iter().any(|e| e.func_idx == *f)); let declined: Vec<(String, String)> = export_name .iter() diff --git a/aver-cert/src/engine/source_bridges.rs b/aver-cert/src/engine/source_bridges.rs index 8e45a3c95..a1c1f8fd6 100644 --- a/aver-cert/src/engine/source_bridges.rs +++ b/aver-cert/src/engine/source_bridges.rs @@ -1493,7 +1493,8 @@ const STEP_EVAL: &str = "AverCert.Grammar.eval, AverCert.Grammar.evalArgs, arms_ _root_.false_and, _root_.and_false, AverCert.GrammarBridge.decodeStr_strBytes, \ _root_.Option.bind_some, _root_.Function.comp_apply, strBytes_eq_iff, strBytes_beq, \ Nat.reduceEqDiff, Int.reduceEq, ← AverCert.GrammarBridge.strBytes_append, \ - _root_.List.append_nil, str_toString, str_hadd"; + _root_.List.append_nil, str_toString, str_hadd, _root_.List.isEmpty_nil, \ + _root_.List.isEmpty_cons, _root_.Bool.false_eq_true, AverCert.Grammar.consAll"; /// Normal forms a leaf closes with, on top of the source definition. const STEP_NORM: &str = "_root_.bne, dec_eq_beq, dec_ne_bne, strBytes_eq_iff, str_toString, \ diff --git a/aver-cert/src/format.rs b/aver-cert/src/format.rs index 6540755c8..9071d838a 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:5168df0c3f4da023c53a9c929e081803c559ed2e22fc6a103f8fb827745ae4d9"; + "sha256:318de1883be91114ed8a396835aea6d183ac9acc4903c7c99e72b023a20ce2c6"; /// Complete host-import surface admitted by the wasm-gc certificate format. /// diff --git a/docs/certificate-format.md b/docs/certificate-format.md index f846521ee..1dd56a2a1 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: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. +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:318de1883be91114ed8a396835aea6d183ac9acc4903c7c99e72b023a20ce2c6` (`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. @@ -231,7 +231,7 @@ A plan (`Grammar.FnPlan`) is `{sig, nslots, locals, body}`: the signature, the r - `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. +- `list t items`, a list literal: `[]`, or a non-empty literal whose items all have the element type `t`, when the type table declares the `List` cons helper (`listCons`) and the helper's planned signature is `(t, List) -> List`. The printer also declines a function that declares effects, uses raw i64 slots, has no MIR body, or whose parameters are not slots `0..n`. @@ -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 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. +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 non-empty list literal pushes its items in order, then `ref.null` of the cons struct, then calls the declared cons helper once per item, so the last item is consed first; 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. @@ -275,7 +275,7 @@ For each `FnEntry` (`entryAccepted`): ### 7.3 Type table and data segments -The type table (`Schema.TypeTable`) declares the carrier and its magnitude array, `$string`, `Vector`, records and tuples (`RecordDecl {tid, struct, fields}`), sums (`SumDecl {tid, root, ctors}`), `Option`, `Result`, `Vector` and `List` instantiations, opaque pass-through types, and the data segment of each string literal. `TypeTable.typeTableConfirmed` requires: +The type table (`Schema.TypeTable`) declares the carrier and its magnitude array, `$string`, `Vector`, records and tuples (`RecordDecl {tid, struct, fields}`), sums (`SumDecl {tid, root, ctors}`), `Option`, `Result`, `Vector` and `List` instantiations, opaque pass-through types, the data segment of each string literal, and the cons helper of each `List` instantiation a literal builds (`listCons`, absent when empty). `TypeTable.typeTableConfirmed` requires: - the type section decodes, and its first rectype is an explicit rec group (`0x4e`); every struct and array the table names is an entry of that group; - `keysUnique`: record and sum type ids are unique; @@ -288,6 +288,8 @@ The type table (`Schema.TypeTable`) declares the carrier and its magnitude array `TypeTable.declsWellFormed` requires the declarations to be inhabited: `eqref` appears only as the subject-scratch local; no chain of one-field records loops; and every declared record and sum, and every parameter and result type of every plan, has a finite value (`inhabited`, proved sound by `inhabTy_sound`). Without it an obligation over an uninhabitable type would hold of any code. +`AcceptedArtifact.consPinned` requires every declared cons helper to be a planned function whose plan is the wall's cons plan (`Grammar.isConsPlan`: its body is `List.prepend(local 0, local 1)`). The typing of a literal of `List` requires that helper's planned signature to be `(t, List) -> List`, and its code entry is pinned like every other plan's, so a literal's calls reach a function whose meaning is `List.prepend`, proved rather than assumed. + A record's `tid` is the plans' own name for a type and is declared, not bound: a wrong id renames a confirmed layout and cannot change it. ### 7.4 Runtime contracts @@ -488,7 +490,7 @@ A certificate does not expire. It verifies against a verifier that embeds the wa | 4.4 Wasip2 envelope | `aver-cert/assets/wall/current/Wasip2Envelope.lean`, `aver-cert/assets/wall/current/AcceptedArtifactCore.lean` (`artifactEnvelopeAccepted`), `aver-cert/src/verifier.rs` (`prepare_wasip2_artifact_with_declared_envelope`) | | 5 Statement | `aver-cert/assets/wall/current/SchemaCore.lean` (`TypeTable`, `FnEntry`, `HostFns`, `HostContracts`, `HostTotal`, `Obligation`, `Manifest`, `HoldsCore`), `aver-cert/assets/wall/current/SchemaBase.lean` (`Subject`, `Policy`, `TotalityRole`, `CarrierSpec`, `CanonRepr`), `aver-cert/assets/wall/current/Schema.lean` (`Holds`), `aver-cert/assets/wall/current/AcceptedArtifact.lean` (`accepted`), `aver-cert/assets/wall/current/AcceptanceSoundness.lean` (`fn_claim_discharges`, `accept_sound`, `accepted_nonvacuous`) | | 6 Plan | `src/codegen/cert/plan_from_mir.rs`, `aver-cert/src/engine/plan.rs`, `aver-cert/assets/wall/current/Grammar.lean` (`Expr`, `FnPlan`, `tyOf`, `planTyped`, `eval`, `groupModel`, `SRepr`), `aver-cert/assets/wall/current/GrammarLower.lean` (`fnCode`, `codeEntryBytes`), `aver-cert/assets/wall/current/GrammarSound.lean` (`agreement`, `fn_certified_group`) | -| 7 Pins | `aver-cert/assets/wall/current/AcceptedArtifactCore.lean` (`entryAccepted`, `callsOrdered`, `sigPinned`, `roleTypesPinned`, `indicesDistinct`, `plansAccepted`, `obligationsOf`, `exportsAccounted`, `importsWithinCapabilities`, `startAccounted`, `closureIsolation`), `aver-cert/assets/wall/current/TypeTable.lean` (`mctxOf`, `typeTableConfirmed`, `dataConfirmed`, `declsWellFormed`), `aver-cert/assets/wall/current/GrammarLower.lean` (`S3Pin`, `DataPin`), `aver-cert/assets/wall/current/ClaimAxes.lean` (`contractsMatch`, `reportEntries`, `reportFacets`), `aver-cert/assets/wall/current/DeclaredLayout.lean` (`layoutConfirmed`, `fnTypesConfirmed`, `exportNamesDistinct`, `StringFast`, `Chars`), `aver-cert/assets/wall/current/ByteWindow.lean` (`typesLazy`, `exportsLazy`, `codeLazy`), `aver-cert/assets/wall/current/SortedKeys.lean` (`exportsAccountedOf_of_fast`, `closureIsolationL_of_S`), `aver-cert/src/wall.rs` (`render_artifact_bytes`) | +| 7 Pins | `aver-cert/assets/wall/current/AcceptedArtifactCore.lean` (`entryAccepted`, `callsOrdered`, `sigPinned`, `roleTypesPinned`, `indicesDistinct`, `consPinned`, `plansAccepted`, `obligationsOf`, `exportsAccounted`, `importsWithinCapabilities`, `startAccounted`, `closureIsolation`), `aver-cert/assets/wall/current/TypeTable.lean` (`mctxOf`, `typeTableConfirmed`, `dataConfirmed`, `declsWellFormed`), `aver-cert/assets/wall/current/GrammarLower.lean` (`S3Pin`, `DataPin`), `aver-cert/assets/wall/current/ClaimAxes.lean` (`contractsMatch`, `reportEntries`, `reportFacets`), `aver-cert/assets/wall/current/DeclaredLayout.lean` (`layoutConfirmed`, `fnTypesConfirmed`, `exportNamesDistinct`, `StringFast`, `Chars`), `aver-cert/assets/wall/current/ByteWindow.lean` (`typesLazy`, `exportsLazy`, `codeLazy`), `aver-cert/assets/wall/current/SortedKeys.lean` (`exportsAccountedOf_of_fast`, `closureIsolationL_of_S`), `aver-cert/src/wall.rs` (`render_artifact_bytes`) | | 8 Totality | `aver-cert/assets/wall/current/GrammarTotal.lean` (`checkTermGroup`, `groupPolicy`, `fn_certified_total_of_check`) | | 9 Bridges and laws | `aver-cert/assets/wall/current/GrammarBridge.lean` (`Exact`, `Adequate`, `ArgsTyped`, `adequate_transfer`, `exact_of_step`, `bridge_of_step`), `aver-cert/src/bridge_statement.rs` (`render_bridge_statement`, `pinned_from_expanded`, `law_mentioned_bridges`), `aver-cert/src/engine/source_bridges.rs`, `aver-cert/src/engine/law_claims.rs`, `aver-cert/src/verifier.rs` (`validate_law_candidate`, `validate_source_bridge_candidate`, `read_source_encoder`) | | 10 Witness and audit | `aver-cert/src/verifier.rs` (`checker_witness`, `REPORT_PIN_PREFIX`, `checker_audit`, `AXIOM_WHITELIST`, `CHECKED_ROOT`, `parse_law_audits`, `parse_bridged_law_audits`, `parse_bridge_audits`), `aver-cert/src/checker_audit.lean` | diff --git a/docs/certification.md b/docs/certification.md index 01402d97c..87ff15a8e 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, flat tuple destructuring, and a List match on `[]` and `[head, ..tail]`; `Option.withDefault` and `Result.withDefault`; `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 that touches a `Vector` is declined: on wasm-gc a `Vector` value is a version struct over a shared array, and the wall models it as the plain array of its elements. +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`; `Int.div` and `Int.mod` by a nonzero literal, or fused under `Result.withDefault` with an Int default; list literals, empty or not, and `List.prepend`. A non-empty literal calls the per-type cons helper once per item; the certificate carries that helper as a planned function and the wall checks that its plan is exactly one `List.prepend` of its two parameters. A function that touches a `Vector` is declined: on wasm-gc a `Vector` value is a version struct over a shared array, and the wall models it as the plain array of its elements. -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. +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, 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 3b6e96d41..27c1b2b72 100644 --- a/src/codegen/cert/plan_from_mir.rs +++ b/src/codegen/cert/plan_from_mir.rs @@ -61,6 +61,9 @@ pub trait PlanLayout { fn result(&self, canonical: &str) -> Option; fn vector(&self, canonical: &str) -> Option; fn list(&self, canonical: &str) -> Option; + /// The function index of the `List` cons helper a non-empty literal + /// calls once per item (`emit_mir_list_literal`). + fn list_cons(&self, canonical: &str) -> Option; fn tuple(&self, canonical: &str) -> Option; fn map(&self, canonical: &str) -> Option; /// A type name the emitter represents specially (packed sequence, @@ -430,6 +433,23 @@ impl TypeTableBuilder { Err(format!("type `{name}`")) } + /// Declare the cons helper of `List` (the literal's canonical type + /// `canonical`), which a non-empty literal calls once per item. + fn list_cons( + &mut self, + layout: &dyn PlanLayout, + canonical: &str, + elem: &PlanTy, + ) -> Result<(), String> { + let f = layout + .list_cons(canonical) + .ok_or_else(|| format!("List (non-empty literal): `{canonical}` has no cons helper"))?; + if !self.table.list_cons.iter().any(|l| &l.0 == elem) { + self.table.list_cons.push((elem.clone(), f)); + } + Ok(()) + } + /// Declare the passive data segment holding a string literal's bytes. fn str_seg(&mut self, layout: &dyn PlanLayout, bytes: &[u8]) -> Result<(), String> { if self.table.str_segs.iter().any(|(b, _)| b == bytes) { @@ -784,14 +804,18 @@ impl Printer<'_> { .collect::>()?, ), MirExpr::List(items) => { - if !items.is_empty() { - return Err("List (non-empty literal)".into()); - } - let ty = self.ty(&stamped(expr)?)?; + let text = stamped(expr)?; + let ty = self.ty(&text)?; let PlanTy::List(elem) = ty else { return Err("List (stamp is not a List)".into()); }; - PlanExpr::List(*elem, Vec::new()) + if !items.is_empty() { + let canonical = parse_ty(&text) + .map(|t| t.canonical()) + .ok_or("List (stamp does not parse)")?; + self.types.list_cons(self.layout, &canonical, &elem)?; + } + PlanExpr::List(*elem, self.exprs(items)?) } other => return Err(node_name(other).to_string()), }) @@ -1258,4 +1282,24 @@ fn notLiteral(a: Int, d: Int) -> Int assert_eq!(arms[0].0, PlanPat::EmptyList); assert!(matches!(arms[1].0, PlanPat::Cons(h, t) if h != PLAN_NO_SLOT && h != t)); } + + #[test] + fn a_list_literal_prints_its_items_and_declares_its_cons_helper() { + let (map, types) = plans( + r#" +module L + intent = "literal probes" + exposes [three] + +fn three(x: Int) -> List + [x, 2, x] +"#, + ); + let three = plan(&map, "three"); + let PlanExpr::List(PlanTy::Int, items) = &three.body else { + panic!("three body: {:?}", three.body) + }; + assert_eq!(items.len(), 3); + assert!(types.list_cons.iter().any(|(t, _)| *t == PlanTy::Int)); + } } diff --git a/src/codegen/wasm_gc/cert_layout.rs b/src/codegen/wasm_gc/cert_layout.rs index e384c8f2b..225d70b63 100644 --- a/src/codegen/wasm_gc/cert_layout.rs +++ b/src/codegen/wasm_gc/cert_layout.rs @@ -12,6 +12,7 @@ use super::types::TypeRegistry; pub(super) struct CertLayout<'a> { pub(super) registry: &'a TypeRegistry, + pub(super) fn_map: &'a super::body::FnMap, pub(super) symbol_table: &'a SymbolTable, pub(super) fn_idx: HashMap, pub(super) builtins: &'a [String], @@ -71,6 +72,10 @@ impl PlanLayout for CertLayout<'_> { self.registry.list_type_idx(canonical) } + fn list_cons(&self, canonical: &str) -> Option { + self.fn_map.list_ops_lookup(canonical).map(|ops| ops.cons) + } + fn tuple(&self, canonical: &str) -> Option { self.registry.tuple_type_idx(canonical) } diff --git a/src/codegen/wasm_gc/module.rs b/src/codegen/wasm_gc/module.rs index b8eadd50c..127754afc 100644 --- a/src/codegen/wasm_gc/module.rs +++ b/src/codegen/wasm_gc/module.rs @@ -6150,6 +6150,7 @@ pub(super) fn emit_module_with( // never changes a byte. let cert_layout = super::cert_layout::CertLayout { registry: ®istry, + fn_map: &fn_map, symbol_table: &symbol_table, fn_idx: resolved_fn_defs .iter() diff --git a/tests/cert_certify_spec.rs b/tests/cert_certify_spec.rs index f48129d4e..6231e5b40 100644 --- a/tests/cert_certify_spec.rs +++ b/tests/cert_certify_spec.rs @@ -2961,8 +2961,8 @@ fn cert_projects_payment_ops_package_checks() { "payment_ops check verdict does not say CHECKED:\n{report}" ); assert!( - report.contains("101 checked exports"), - "payment_ops must keep the 101 exports it certifies:\n{report}" + report.contains("106 checked exports"), + "payment_ops must keep the 106 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 7039e14a0..0ff1b32e8 100644 --- a/tests/cert_hardening_spec.rs +++ b/tests/cert_hardening_spec.rs @@ -37,7 +37,10 @@ //! 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. +//! slots are exchanged; +//! * a List literal's cons helper declared as a user function of the same +//! signature, a cons helper whose plan is not the cons plan, and the cons +//! helpers of two instantiations exchanged. //! //! Gated behind `wasm` and skipped when `lake` is unavailable, like the other //! certificate suites. @@ -1536,3 +1539,146 @@ fn cert_hardening_declines_a_cons_pattern_with_head_and_tail_exchanged() { let (ok, report) = aver_cert("check", &wasm, &cert); assert_declined(ok, &report, "did not build"); } + +/// A program building non-empty List literals: Int literals, String +/// parameters, and a user function `keep` with the cons helper's signature +/// whose plan is not the cons plan (it returns the tail). +const LITS: &str = "module Lits + intent = \"List literals.\" + exposes [three, pair, keep] + +fn three() -> List + ? \"Three Ints.\" + [1, 2, 3] + +fn pair(a: String, b: String) -> List + ? \"Two Strings.\" + [a, b] + +fn keep(h: Int, t: List) -> List + ? \"The tail, unchanged.\" + t +"; + +/// Emit the List-literal certificate into a fresh scratch directory. +fn literal_baseline(prefix: &str) -> Option<(ScratchDir, PathBuf, PathBuf)> { + if !lake_available() { + return None; + } + let dir = temp_dir(prefix); + std::fs::write(dir.join("lits.av"), LITS).unwrap(); + let out = dir.join("out"); + let compile = aver_command() + .current_dir(&*dir) + .args([ + "compile", + "lits.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("lits.wasm"), out.join("cert"))) +} + +/// The digits right after the first occurrence of `needle` in `text`. +fn number_after(text: &str, needle: &str) -> String { + let at = text + .find(needle) + .unwrap_or_else(|| panic!("`{needle}` is in Plans.lean")) + + needle.len(); + text[at..] + .chars() + .take_while(char::is_ascii_digit) + .collect() +} + +/// The honest certificate checks, with every export certified; the cons +/// helpers ride along as planned internal functions. +#[test] +fn cert_hardening_accepts_list_literals() { + let Some((_dir, wasm, cert)) = literal_baseline("certharden-lits-clean") else { + return; + }; + let plans = std::fs::read_to_string(cert.join("Plans.lean")).unwrap(); + assert!(plans.contains("listCons := [(.int, "), "{plans}"); + assert!(plans.contains("(.string, "), "{plans}"); + let (ok, report) = aver_cert("check", &wasm, &cert); + assert!(ok, "the List-literal certificate must check:\n{report}"); + assert!(report.contains("3 checked exports"), "{report}"); +} + +/// The cons helper a literal calls is the one the type table declares, and +/// the wall requires its plan to be exactly the cons plan: pointing +/// `List`'s entry at `keep`, a user function of the same signature +/// whose plan returns the tail, is refused. +#[test] +fn cert_hardening_declines_a_cons_helper_that_is_a_user_function() { + let Some((_dir, wasm, cert)) = literal_baseline("certharden-lits-user") else { + return; + }; + let plans = cert.join("Plans.lean"); + let text = std::fs::read_to_string(&plans).unwrap(); + let cons = number_after(&text, "listCons := [(.int, "); + let keep = number_after(&text, "⟨\"keep\", true, "); + replace_once( + &plans, + &format!("listCons := [(.int, {cons})"), + &format!("listCons := [(.int, {keep})"), + ); + let (ok, report) = aver_cert("check", &wasm, &cert); + assert_declined(ok, &report, "did not build"); +} + +/// The cons helper's own plan is pinned to the cons plan: a plan that +/// returns the tail instead of consing lowers to other bytes and is not the +/// wall's cons plan, so the package is refused. +#[test] +fn cert_hardening_declines_a_cons_helper_whose_plan_is_not_the_cons_plan() { + let Some((_dir, wasm, cert)) = literal_baseline("certharden-lits-plan") else { + return; + }; + let plans = cert.join("Plans.lean"); + let text = std::fs::read_to_string(&plans).unwrap(); + let cons = number_after(&text, "listCons := [(.int, "); + let def = format!("def fn{cons} : FnPlan :="); + let at = text.find(&def).expect("the cons helper is planned"); + let body = "body := (.call (.builtin .listPrepend) [(.local 0), (.local 1)])"; + let rel = text[at..] + .find(body) + .expect("the cons helper's body is the cons plan"); + let mut tampered = text.clone(); + tampered.replace_range(at + rel..at + rel + body.len(), "body := (.local 1)"); + std::fs::write(&plans, tampered).unwrap(); + let (ok, report) = aver_cert("check", &wasm, &cert); + assert_declined(ok, &report, "did not build"); +} + +/// The cons helpers of two instantiations exchanged: each literal would call +/// the other type's helper, whose planned signature is not its cons +/// signature, so the typing refuses the literals. +#[test] +fn cert_hardening_declines_exchanged_cons_helpers() { + let Some((_dir, wasm, cert)) = literal_baseline("certharden-lits-swap") else { + return; + }; + let plans = cert.join("Plans.lean"); + let text = std::fs::read_to_string(&plans).unwrap(); + let int_f = number_after(&text, "listCons := [(.int, "); + let str_f = number_after(&text, &format!("listCons := [(.int, {int_f}), (.string, ")); + replace_once( + &plans, + &format!("listCons := [(.int, {int_f}), (.string, {str_f})]"), + &format!("listCons := [(.int, {str_f}), (.string, {int_f})]"), + ); + let (ok, report) = aver_cert("check", &wasm, &cert); + assert_declined(ok, &report, "did not build"); +} 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 5fdb67f84..902ec8d24 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:5168df0c3f4da023c53a9c929e081803c559ed2e22fc6a103f8fb827745ae4d9"}, + "format": {"version": 1, "wall_id": "sha256:318de1883be91114ed8a396835aea6d183ac9acc4903c7c99e72b023a20ce2c6"}, "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 8e7df5cb7..5dab863f1 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:5168df0c3f4da023c53a9c929e081803c559ed2e22fc6a103f8fb827745ae4d9"}, + "format": {"version": 1, "wall_id": "sha256:318de1883be91114ed8a396835aea6d183ac9acc4903c7c99e72b023a20ce2c6"}, "wasm": "wasip2_carrierless.component.wasm", "wasm_sha256": "0e7064150f82e180dff6f774a8f48711acd2ea21d183ee06576d4f7c9f135aed", "target": "wasip2", diff --git a/tools/cert-baseline.json b/tools/cert-baseline.json index ef871ac0d..59bbac950 100644 --- a/tools/cert-baseline.json +++ b/tools/cert-baseline.json @@ -96,6 +96,7 @@ }, "projects/payment_ops/main.av": { "bridges": [ + "App_Cli_helpLines", "App_Commands_duplicateSettlementAudit", "App_Commands_duplicateWebhookAudit", "App_Commands_sampleAudit", @@ -106,10 +107,13 @@ "App_Queries_sampleCase", "App_Queries_sampleEvent", "App_Queries_sampleSettlement", + "App_Queries_sampleState", "App_Render_renderCaseItem", "App_Render_sampleAudit", "App_Render_sampleCase", + "App_Render_sampleDetail", "App_Render_sampleEvent", + "App_Render_sampleReport", "App_Render_sampleSettlement", "App_Render_sampleSummary", "App_Render_settlementKindText", @@ -157,6 +161,7 @@ "Infra_Store_settlementsPath" ], "certified": { + "App_Cli_helpLines": "L1", "App_Commands_duplicateSettlementAudit": "L1", "App_Commands_duplicateWebhookAudit": "L1", "App_Commands_hasSettlementRow": "L1", @@ -173,12 +178,15 @@ "App_Queries_sampleEvent": "L1", "App_Queries_sampleOrFirst": "L1", "App_Queries_sampleSettlement": "L1", + "App_Queries_sampleState": "L1", "App_Render_renderAuditItemsInto": "L1", "App_Render_renderCaseItem": "L1", "App_Render_renderCaseItemsInto": "L1", "App_Render_sampleAudit": "L1", "App_Render_sampleCase": "L1", + "App_Render_sampleDetail": "L1", "App_Render_sampleEvent": "L1", + "App_Render_sampleReport": "L1", "App_Render_sampleSettlement": "L1", "App_Render_sampleSummary": "L1", "App_Render_settlementKindText": "L1", @@ -224,6 +232,7 @@ "Domain_Normalize_normalizeWebhookEvent": "L1", "Domain_Reconcile_amountMissing": "L1", "Domain_Reconcile_compareAmounts": "L1", + "Domain_Reconcile_compareCurrency": "L1", "Domain_Reconcile_findState": "L1", "Domain_Reconcile_firstCurrency": "L1", "Domain_Reconcile_prependAll": "L1", From 7faeb63da5ff1849c50167164cbb85ae95b69fe7 Mon Sep 17 00:00:00 2001 From: jasisz Date: Sat, 26 Sep 2026 10:18:51 +0200 Subject: [PATCH 5/5] cert: bridge functions that take a List A source bridge's proof decodes each argument shape of its function, and a List argument had no decoder, so a function taking a List was certified against its plan only and a law about it was not on the bytes. The step lemmas now decode a List of Ints, Bools or Strings as a whole value, one cons cell at a time (decListInt, decListBool, decListString). A step splits a decoded List into its empty and cons shapes, with the tail an encoding again, so a recursive call on the tail meets its callee through the encoding, and a function that returns its List argument meets its image. An export's image reads an encoded List back, and its typing uses the encoded List's type. The List match evaluates arm by arm. Two leaf changes: a callee with a List parameter has its image unfolded in the leaves, and a self-recursive leaf also closes when unfolding the source already closes it. Hostile test: a bridge whose List argument names another element type is refused. Ratchet: gains only. Co-Authored-By: Claude Opus 5.5 (1M context) --- CHANGELOG.md | 4 + aver-cert/src/engine/source_bridges.rs | 343 +++++++++++++++++++++++-- tests/cert_certify_spec.rs | 18 +- tests/cert_hardening_spec.rs | 39 ++- tools/cert-baseline.json | 25 +- 5 files changed, 388 insertions(+), 41 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index cecbdf00c..f42db1b91 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 — source bridges for List arguments + +- **A certified function that takes a List of Ints, Bools or Strings now has a source bridge.** The proof that its plan computes your source function used to stop at a List argument, so such a function was certified against its plan only, and a law about it was not on the bytes. The bridge proofs now decode a List argument one cell at a time. On the btc-listener corpus, 98 more functions get a credited source bridge (633 of 636), and 15 more laws are proved about the certified bytes (31 of 32). A List of records, sums or Lists still has no bridge. + ### Added — certificates for list literals - **A function that builds a non-empty list literal can now be certified.** `[a, b, c]` used to leave the function source-level only. The compiler builds such a literal by calling its cons helper for the element type once per item, and the certificate now carries that helper as a planned function: the wall checks that its plan is exactly one `List.prepend` of its two parameters, so the literal's meaning is proved, not assumed. On the btc-listener corpus this certifies 58 more functions and gives 41 more of them a source bridge (a function that returns a literal is now bridged to its source); across the examples, projects and certificate fixtures, 27 more functions are certified. The wall identity rotates: packages produced by earlier versions must be produced again. diff --git a/aver-cert/src/engine/source_bridges.rs b/aver-cert/src/engine/source_bridges.rs index a1c1f8fd6..d6ea1e7c0 100644 --- a/aver-cert/src/engine/source_bridges.rs +++ b/aver-cert/src/engine/source_bridges.rs @@ -662,13 +662,19 @@ impl ModelInfo { /// pattern over them, and the source value it denotes. #[derive(Debug, Clone)] struct Alt { - /// Atomic values the shape binds as a whole `SVal` and decodes by the - /// wall's decoder: `(SVal variable, source variable)`. - binds: Vec<(String, String)>, + /// Atomic values the shape binds as a whole `SVal` and decodes: + /// `(SVal variable, source variable, decoder)`, the decoder being the + /// wall's `decodeStr` for a String or a `decList…` of the step lemmas for + /// a List. + binds: Vec, pattern: String, source: String, } +/// A value a shape decodes whole: `(SVal variable, source variable, +/// decoder)`. +type Bind = (String, String, String); + /// Most argument shapes one function's decoder may expand into. const MAX_ALTS: usize = 64; @@ -691,7 +697,7 @@ fn product(parts: Vec>) -> Result>, String> { Ok(out) } -fn join_row(row: &[Alt]) -> (Vec<(String, String)>, Vec, Vec) { +fn join_row(row: &[Alt]) -> (Vec, Vec, Vec) { let mut binders = Vec::new(); let mut patterns = Vec::new(); let mut sources = Vec::new(); @@ -703,6 +709,16 @@ fn join_row(row: &[Alt]) -> (Vec<(String, String)>, Vec, Vec) { (binders, patterns, sources) } +/// The step lemmas' decoder of a List argument with these elements. +fn list_decoder(elem: &SourceEncoder) -> Option<&'static str> { + match elem { + SourceEncoder::Int => Some("decListInt"), + SourceEncoder::Bool => Some("decListBool"), + SourceEncoder::Str => Some("decListString"), + _ => None, + } +} + fn alts(enc: &SourceEncoder, fresh: &mut usize) -> Result, String> { const SVAL: &str = "_root_.AverCert.Grammar.SVal"; let leaf = |ctor: &str, fresh: &mut usize| { @@ -724,12 +740,31 @@ fn alts(enc: &SourceEncoder, fresh: &mut usize) -> Result, String> { let t = format!("t{fresh}"); *fresh += 1; Ok(vec![Alt { - binds: vec![(v.clone(), t.clone())], + binds: vec![(v.clone(), t.clone(), "AverCert.GrammarBridge.decodeStr".into())], + pattern: v, + source: t, + }]) + } + // A List of Ints, Bools or Strings is matched as a whole value and + // decoded one cons cell at a time by the step lemmas' `decList…`; + // a step splits it into its empty and cons shapes (`decList…_cases`). + SourceEncoder::List(elem) => { + let decoder = list_decoder(elem).ok_or_else(|| { + format!( + "a `list` argument of `{}` elements has no decoder in this version", + elem.kind() + ) + })?; + let v = format!("v{fresh}"); + let t = format!("t{fresh}"); + *fresh += 1; + Ok(vec![Alt { + binds: vec![(v.clone(), t.clone(), format!("AverCert.Bridge.{decoder}"))], pattern: v, source: t, }]) } - SourceEncoder::Float | SourceEncoder::List(_) | SourceEncoder::Vector(_) => { + SourceEncoder::Float | SourceEncoder::Vector(_) => { Err(format!("a `{}` argument has no decoder in this version", enc.kind())) } SourceEncoder::Record { @@ -898,7 +933,7 @@ struct BridgedFn { /// One decoder argument shape: the atomic values it decodes, its argument /// patterns, and the source arguments it denotes. -type DecoderShape = (Vec<(String, String)>, Vec, Vec); +type DecoderShape = (Vec, Vec, Vec); /// The outcome of bridge planning. struct BridgePlan { @@ -1247,7 +1282,8 @@ fn plan_bridges(analysis: &Analysis, model: &SourceModel) -> BridgePlan { const TYPING_SIMPS: &str = "AverCert.GrammarBridge.ArgsTyped, AverCert.Grammar.HasTyL, \ AverCert.Grammar.HasTy, AverCert.Grammar.HasTyAll, AverCert.AcceptedArtifact.obligationOf, \ AverCert.TypeTable.mctxOf, AverCert.TypeTable.recordOf, AverCert.TypeTable.sumOf, \ - AverCert.Grammar.ctorFields, AverCert.Plans.types"; + AverCert.Grammar.ctorFields, AverCert.Plans.types, AverCert.Bridge.hasTy_listInt, \ + AverCert.Bridge.hasTy_listBool, AverCert.Bridge.hasTy_listString"; fn arg_type(params: &[SourceEncoder]) -> String { match params.len() { @@ -1288,8 +1324,8 @@ fn render_fn_defs(b: &BridgedFn, s: &mut String) { _ => format!("({})", sources.join(", ")), }; let mut rhs = format!("_root_.Option.some {value}"); - for (v, t) in binds.iter().rev() { - rhs = format!("(AverCert.GrammarBridge.decodeStr {v}).bind (fun {t} => {rhs})"); + for (v, t, decode) in binds.iter().rev() { + rhs = format!("({decode} {v}).bind (fun {t} => {rhs})"); } s.push_str(&format!(" | [{}] => {rhs}\n", patterns.join(", "))); } @@ -1469,16 +1505,243 @@ theorem optDefault_none (t : Ty) (d : Option SVal) : optDefault (some (.none t)) theorem resDefault_ok (t e : Ty) (v : SVal) (d : Option SVal) : resDefault (some (.ok t e v)) d = some v := rfl theorem resDefault_err (t e : Ty) (v : SVal) (d : Option SVal) : resDefault (some (.err t e v)) d = d := rfl +/-! A List argument of Ints, Bools or Strings is decoded as a whole value, + one cons cell at a time. A step splits a decoded List into its empty and + cons shapes (`…_cases`); an export's image reads an encoded List back + (`…_enc`); an encoded List inhabits its List type (`hasTy_list…`). -/ + +theorem decListInt_enc : ∀ l : List Int, + decListInt (List.foldr (fun y acc => SVal.cons .int (SVal.i y) acc) (SVal.nil .int) l) = some l + | [] => by simp [decListInt] + | y :: ys => by simp [decListInt, decListInt_enc ys] + +theorem decListBool_enc : ∀ l : List Bool, + decListBool (List.foldr (fun y acc => SVal.cons .bool (SVal.b y) acc) (SVal.nil .bool) l) = some l + | [] => by simp [decListBool] + | y :: ys => by simp [decListBool, decListBool_enc ys] + +theorem decListString_enc : ∀ l : List String, + decListString (List.foldr (fun y acc => + SVal.cons .string (SVal.s (AverCert.GrammarBridge.strBytes y)) acc) (SVal.nil .string) l) = some l + | [] => by simp [decListString] + | y :: ys => by + simp [decListString, decListString_enc ys, AverCert.GrammarBridge.decodeStr_strBytes] + +theorem decListInt_cases {v : SVal} {a : List Int} (h : decListInt v = some a) : + (v = .nil .int ∧ a = []) ∨ + ∃ x r t, v = .cons .int (.i x) r ∧ decListInt r = some t ∧ a = x :: t := by + unfold decListInt at h + split at h + · simp only [Option.some.injEq] at h + exact Or.inl ⟨rfl, h.symm⟩ + · rename_i x r + cases hr : decListInt r with + | none => simp [hr] at h + | some t => + simp only [hr, Option.map_some, Option.some.injEq] at h + exact Or.inr ⟨x, r, t, rfl, hr, h.symm⟩ + · simp at h + +theorem decListBool_cases {v : SVal} {a : List Bool} (h : decListBool v = some a) : + (v = .nil .bool ∧ a = []) ∨ + ∃ x r t, v = .cons .bool (.b x) r ∧ decListBool r = some t ∧ a = x :: t := by + unfold decListBool at h + split at h + · simp only [Option.some.injEq] at h + exact Or.inl ⟨rfl, h.symm⟩ + · rename_i x r + cases hr : decListBool r with + | none => simp [hr] at h + | some t => + simp only [hr, Option.map_some, Option.some.injEq] at h + exact Or.inr ⟨x, r, t, rfl, hr, h.symm⟩ + · simp at h + +theorem decListString_cases {v : SVal} {a : List String} (h : decListString v = some a) : + (v = .nil .string ∧ a = []) ∨ + ∃ x r t, v = .cons .string (.s (AverCert.GrammarBridge.strBytes x)) r ∧ + decListString r = some t ∧ a = x :: t := by + unfold decListString at h + split at h + · simp only [Option.some.injEq] at h + exact Or.inl ⟨rfl, h.symm⟩ + · rename_i hv r + cases hx : AverCert.GrammarBridge.decodeStr hv with + | none => simp [hx] at h + | some x => + cases hr : decListString r with + | none => simp [hx, hr] at h + | some t => + simp only [hx, hr, Option.bind_some, Option.map_some, Option.some.injEq] at h + exact Or.inr ⟨x, r, t, by rw [AverCert.GrammarBridge.decodeStr_eq_some.mp hx], hr, + h.symm⟩ + · simp at h + +/-- A decoded List of Ints is the encoding of what it decodes to. -/ +theorem decListInt_sound : ∀ (a : List Int) {v : SVal}, decListInt v = some a → + v = List.foldr (fun y acc => SVal.cons .int (SVal.i y) acc) (SVal.nil .int) a := by + intro a + induction a with + | nil => + intro v h + rcases decListInt_cases h with ⟨rfl, _⟩ | ⟨_, _, _, _, _, h2⟩ + · rfl + · cases h2 + | cons x t ih => + intro v h + rcases decListInt_cases h with ⟨_, h2⟩ | ⟨x', r, t', rfl, hr, h2⟩ + · cases h2 + · simp only [List.cons.injEq] at h2 + obtain ⟨rfl, rfl⟩ := h2 + simp only [List.foldr, ih hr] + +/-- A decoded List of Ints, split into its empty and cons shapes, the tail + an encoding. -/ +theorem decListInt_split {v : SVal} {a : List Int} (h : decListInt v = some a) : + (v = .nil .int ∧ a = []) ∨ ∃ x t, v = .cons .int (SVal.i x) (List.foldr (fun y acc => SVal.cons .int (SVal.i y) acc) (SVal.nil .int) t) ∧ a = x :: t := by + have hv := decListInt_sound _ h + cases a with + | nil => exact Or.inl ⟨hv, rfl⟩ + | cons x t => exact Or.inr ⟨x, t, by simpa [List.foldr] using hv, rfl⟩ + +/-- A decoded List of Bools is the encoding of what it decodes to. -/ +theorem decListBool_sound : ∀ (a : List Bool) {v : SVal}, decListBool v = some a → + v = List.foldr (fun y acc => SVal.cons .bool (SVal.b y) acc) (SVal.nil .bool) a := by + intro a + induction a with + | nil => + intro v h + rcases decListBool_cases h with ⟨rfl, _⟩ | ⟨_, _, _, _, _, h2⟩ + · rfl + · cases h2 + | cons x t ih => + intro v h + rcases decListBool_cases h with ⟨_, h2⟩ | ⟨x', r, t', rfl, hr, h2⟩ + · cases h2 + · simp only [List.cons.injEq] at h2 + obtain ⟨rfl, rfl⟩ := h2 + simp only [List.foldr, ih hr] + +/-- A decoded List of Bools, split into its empty and cons shapes, the tail + an encoding. -/ +theorem decListBool_split {v : SVal} {a : List Bool} (h : decListBool v = some a) : + (v = .nil .bool ∧ a = []) ∨ ∃ x t, v = .cons .bool (SVal.b x) (List.foldr (fun y acc => SVal.cons .bool (SVal.b y) acc) (SVal.nil .bool) t) ∧ a = x :: t := by + have hv := decListBool_sound _ h + cases a with + | nil => exact Or.inl ⟨hv, rfl⟩ + | cons x t => exact Or.inr ⟨x, t, by simpa [List.foldr] using hv, rfl⟩ + +/-- A decoded List of Strings is the encoding of what it decodes to. -/ +theorem decListString_sound : ∀ (a : List String) {v : SVal}, decListString v = some a → + v = List.foldr (fun y acc => SVal.cons .string (SVal.s (AverCert.GrammarBridge.strBytes y)) acc) (SVal.nil .string) a := by + intro a + induction a with + | nil => + intro v h + rcases decListString_cases h with ⟨rfl, _⟩ | ⟨_, _, _, _, _, h2⟩ + · rfl + · cases h2 + | cons x t ih => + intro v h + rcases decListString_cases h with ⟨_, h2⟩ | ⟨x', r, t', rfl, hr, h2⟩ + · cases h2 + · simp only [List.cons.injEq] at h2 + obtain ⟨rfl, rfl⟩ := h2 + simp only [List.foldr, ih hr] + +/-- A decoded List of Strings, split into its empty and cons shapes, the tail + an encoding. -/ +theorem decListString_split {v : SVal} {a : List String} (h : decListString v = some a) : + (v = .nil .string ∧ a = []) ∨ ∃ x t, v = .cons .string (SVal.s (AverCert.GrammarBridge.strBytes x)) (List.foldr (fun y acc => SVal.cons .string (SVal.s (AverCert.GrammarBridge.strBytes y)) acc) (SVal.nil .string) t) ∧ a = x :: t := by + have hv := decListString_sound _ h + cases a with + | nil => exact Or.inl ⟨hv, rfl⟩ + | cons x t => exact Or.inr ⟨x, t, by simpa [List.foldr] using hv, rfl⟩ + +theorem hasTy_listEnc {α : Type} (M : MCtx) (t : Ty) (e : α → SVal) (he : ∀ y, HasTy M (e y) t) : + ∀ l : List α, HasTy M (List.foldr (fun y acc => SVal.cons t (e y) acc) (SVal.nil t) l) (.list t) + | [] => by simp [HasTy] + | y :: ys => by + simp only [List.foldr] + exact ⟨rfl, he y, hasTy_listEnc M t e he ys⟩ + +theorem hasTy_listInt (M : MCtx) (l : List Int) : + HasTy M (List.foldr (fun y acc => SVal.cons .int (SVal.i y) acc) (SVal.nil .int) l) (.list .int) := + hasTy_listEnc M .int _ (fun y => by simp [HasTy]) l + +theorem hasTy_listBool (M : MCtx) (l : List Bool) : + HasTy M (List.foldr (fun y acc => SVal.cons .bool (SVal.b y) acc) (SVal.nil .bool) l) + (.list .bool) := + hasTy_listEnc M .bool _ (fun y => by simp [HasTy]) l + +theorem hasTy_listString (M : MCtx) (l : List String) : + HasTy M (List.foldr (fun y acc => + SVal.cons .string (SVal.s (AverCert.GrammarBridge.strBytes y)) acc) (SVal.nil .string) l) + (.list .string) := + hasTy_listEnc M .string _ (fun y => by simp [HasTy]) l + +/-! Arm-by-arm evaluation of a List match. -/ + +theorem arms_emptyList_nil (F : Nat → List SVal → Option SVal) (env : Nat → Option SVal) (t : Ty) + (b : Expr) (rest : Arms) : + evalArms F env (.nil t) (.cons .emptyList b rest) = eval F env b := by + simp [evalArms, patMatch, bindVals] + +theorem arms_emptyList_cons (F : Nat → List SVal → Option SVal) (env : Nat → Option SVal) (t : Ty) + (x r : SVal) (b : Expr) (rest : Arms) : + evalArms F env (.cons t x r) (.cons .emptyList b rest) = evalArms F env (.cons t x r) rest := by + simp [evalArms, patMatch] + +theorem arms_cons_nil (F : Nat → List SVal → Option SVal) (env : Nat → Option SVal) (t : Ty) + (hd tl : Nat) (b : Expr) (rest : Arms) : + evalArms F env (.nil t) (.cons (.cons hd tl) b rest) = evalArms F env (.nil t) rest := by + simp [evalArms, patMatch] + +theorem arms_cons_cons (F : Nat → List SVal → Option SVal) (env : Nat → Option SVal) (t : Ty) + (x r : SVal) (hd tl : Nat) (b : Expr) (rest : Arms) : + evalArms F env (.cons t x r) (.cons (.cons hd tl) b rest) = + eval F (if tl = noSlot then (if hd = noSlot then env else upd env hd x) + else upd (if hd = noSlot then env else upd env hd x) tl r) b := by + by_cases h1 : hd = noSlot <;> by_cases h2 : tl = noSlot <;> + simp [evalArms, patMatch, bindVals, h1, h2] + end StepLemmas "#; +/// The decoders of a List argument of Ints, Bools or Strings, rendered into +/// `BridgeDefs.lean` ahead of the functions' decoders that call them: the +/// whole value, one cons cell at a time. Their lemmas are in [`STEP_LEMMAS`]. +const LIST_DECODERS: &str = r#"section ListDecoders +open AverCert.Grammar + +noncomputable def decListInt : SVal → Option (List Int) + | .nil .int => some [] + | .cons .int (.i x) r => (decListInt r).map (fun t => x :: t) + | _ => none + +noncomputable def decListBool : SVal → Option (List Bool) + | .nil .bool => some [] + | .cons .bool (.b x) r => (decListBool r).map (fun t => x :: t) + | _ => none + +noncomputable def decListString : SVal → Option (List String) + | .nil .string => some [] + | .cons .string hv r => + (AverCert.GrammarBridge.decodeStr hv).bind (fun x => (decListString r).map (fun t => x :: t)) + | _ => none + +end ListDecoders + +"#; + /// Evaluation lemmas of a step proof: the plan's equations with a match /// taken arm by arm, and `if` / `withDefault` as Lean functions of their /// subject (pre-rewrites, so they win over `eval`'s own equations), the /// callee table, and the normal forms the source spells (`==`, `!=`, decided /// comparisons, literal indices, String parts folded into one `strBytes`). const STEP_EVAL: &str = "AverCert.Grammar.eval, AverCert.Grammar.evalArgs, arms_nil, arms_wild, \ - arms_bind, arms_litInt, arms_litStr, arms_litBool, arms_ctor, arms_tuple, ↓eval_ite, \ + arms_bind, arms_litInt, arms_litStr, arms_litBool, arms_ctor, arms_tuple, arms_emptyList_nil, \ + arms_emptyList_cons, arms_cons_nil, arms_cons_cons, ↓eval_ite, \ ↓eval_optDefault, ↓eval_resDefault, optDefault_ite, resDefault_ite, optDefault_some, \ optDefault_none, resDefault_ok, resDefault_err, AverCert.Grammar.argsEnv, \ AverCert.Grammar.upd, AverCert.Grammar.intBin, AverCert.Grammar.boolBin, \ @@ -1494,11 +1757,12 @@ const STEP_EVAL: &str = "AverCert.Grammar.eval, AverCert.Grammar.evalArgs, arms_ _root_.Option.bind_some, _root_.Function.comp_apply, strBytes_eq_iff, strBytes_beq, \ Nat.reduceEqDiff, Int.reduceEq, ← AverCert.GrammarBridge.strBytes_append, \ _root_.List.append_nil, str_toString, str_hadd, _root_.List.isEmpty_nil, \ - _root_.List.isEmpty_cons, _root_.Bool.false_eq_true, AverCert.Grammar.consAll"; + _root_.List.isEmpty_cons, _root_.Bool.false_eq_true, AverCert.Grammar.consAll, \ + decListInt, decListBool, decListString, decListInt_enc, decListBool_enc, decListString_enc"; /// Normal forms a leaf closes with, on top of the source definition. const STEP_NORM: &str = "_root_.bne, dec_eq_beq, dec_ne_bne, strBytes_eq_iff, str_toString, \ - str_hadd, _root_.String.append_assoc"; + str_hadd, _root_.String.append_assoc, decListInt, decListBool, decListString"; /// One step lemma, proved by construction rather than by search. The /// decoder's argument shapes are expanded; the plan body is evaluated by @@ -1567,7 +1831,19 @@ fn render_step( } else { "" }; - let norm = format!("{STEP_NORM}{empty}{constants}{with_default}"); + // A callee with a List parameter answers a call on a decoded List only + // once its decoder meets the step's `decList…` hypothesis, which the + // leaves rewrite with: the leaves unfold its image too. + let list_images: String = b + .callees + .iter() + .filter(|c| { + fns.get(c) + .is_some_and(|callee| callee.params.iter().any(|p| matches!(p, SourceEncoder::List(_)))) + }) + .map(|c| format!(", img_{c}")) + .collect(); + let norm = format!("{STEP_NORM}{empty}{constants}{with_default}{list_images}"); // A self-recursive source function is unfolded once, on the right: `simp` // with its equation would unfold the recursive call on the left as well. // The last rung of the other leaves meets a constant the source writes by @@ -1583,8 +1859,8 @@ fn render_step( let leaf = if b.recursive && !b.fuel { format!( "(with_reducible rfl)\n \ - | (symm; rw [{model}]; simp [{norm}, *]; done)\n \ - | (symm; rw [{model}]; simp_all [{norm}]; done)\n \ + | (symm; rw [{model}]; (try simp [{norm}, *]); done)\n \ + | (symm; rw [{model}]; (try simp_all [{norm}]); done)\n \ | (symm; rw [{model}]; simp_all [{norm}] <;> omega)" ) } else { @@ -1611,7 +1887,13 @@ fn render_step( unfold dec_{f} at hy\n \ split at hy <;> simp only [_root_.Option.bind_eq_some_iff, _root_.Option.some.injEq, \ reduceCtorEq, AverCert.GrammarBridge.decodeStr_eq_some] at hy\n \ - all_goals (repeat (obtain ⟨_, rfl, hy⟩ := hy))\n \ + all_goals (repeat' (first\n \ + | (obtain ⟨_, rfl, hy⟩ := hy)\n \ + | (obtain ⟨_, hl, hy⟩ := hy\n \ + first\n \ + | (rcases decListInt_split hl with (⟨rfl, rfl⟩ | ⟨_, _, rfl, rfl⟩))\n \ + | (rcases decListBool_split hl with (⟨rfl, rfl⟩ | ⟨_, _, rfl, rfl⟩))\n \ + | (rcases decListString_split hl with (⟨rfl, rfl⟩ | ⟨_, _, rfl, rfl⟩)))))\n \ all_goals (try subst hy)\n \ all_goals simp only [AverCert.Plans.fn{f}, eval_ite, eval_optDefault, eval_resDefault]\n \ all_goals simp only [img_{f}, {STEP_EVAL}, I_{f}{callee_simps}{backward}]\n \ @@ -1688,7 +1970,8 @@ fn render_export( // match (the statement's and `img_f`'s), or a conjunction of such for a // record: equal by unfolding, so `rfl` on each conjunct. let image_simps = format!( - "I_{func_idx}, dec_{func_idx}, img_{func_idx}, AverCert.GrammarBridge.decodeStr_strBytes" + "I_{func_idx}, dec_{func_idx}, img_{func_idx}, AverCert.GrammarBridge.decodeStr_strBytes, \ + decListInt_enc, decListBool_enc, decListString_enc" ); let image = format!( "(by {split_cases}all_goals first | rfl | (simp [{image_simps}]; done) | \ @@ -1844,6 +2127,7 @@ fn render_bridge_lean( set_option maxHeartbeats {FILE_HEARTBEATS}\n\n\ namespace AverCert.Bridge\n\n" )); + s.push_str(LIST_DECODERS); for b in plan.fns.values() { render_fn_defs(b, &mut s); } @@ -2457,9 +2741,26 @@ mod source_bridge_tests { // A String is matched whole and decoded by the wall's `decodeStr`. let strs = alts(&SourceEncoder::Str, &mut fresh).expect("a String decodes"); assert_eq!(strs.len(), 1); - assert_eq!(strs[0].binds, vec![("v1".to_string(), "t1".to_string())]); + assert_eq!( + strs[0].binds, + vec![( + "v1".to_string(), + "t1".to_string(), + "AverCert.GrammarBridge.decodeStr".to_string() + )] + ); assert!(alts(&SourceEncoder::Float, &mut fresh).is_err()); - assert!(alts(&SourceEncoder::List(Box::new(SourceEncoder::Int)), &mut fresh).is_err()); + let ints = alts(&SourceEncoder::List(Box::new(SourceEncoder::Int)), &mut fresh) + .expect("a List of Ints decodes"); + assert_eq!(ints.len(), 1); + assert_eq!(ints[0].binds[0].2, "AverCert.Bridge.decListInt"); + assert!( + alts( + &SourceEncoder::List(Box::new(SourceEncoder::List(Box::new(SourceEncoder::Int)))), + &mut fresh + ) + .is_err() + ); } #[test] @@ -2678,7 +2979,7 @@ mod source_bridge_tests { assert!(s.contains(", ↓ ← strLit_1]"), "{s}"); assert!(!s.contains("↓ ← strLit_0"), "the empty literal is never read back: {s}"); assert!(s.contains("all_goals (repeat' (refine ite_eq_of (fun h => ?_) (fun h => ?_)))"), "{s}"); - assert!(s.contains("| (symm; rw [_root_.M.spaces]; simp [_root_.bne"), "{s}"); + assert!(s.contains("| (symm; rw [_root_.M.spaces]; (try simp [_root_.bne"), "{s}"); assert!(s.contains(", strLit_0, _root_.M.width"), "{s}"); assert!(!s.contains("simp [_root_.M.spaces"), "a recursive source never unfolds by simp: {s}"); assert!(!s.contains("simp [AverCert.Plans.fn9"), "{s}"); diff --git a/tests/cert_certify_spec.rs b/tests/cert_certify_spec.rs index 6231e5b40..8e4cb10f7 100644 --- a/tests/cert_certify_spec.rs +++ b/tests/cert_certify_spec.rs @@ -548,18 +548,6 @@ fn certify_goal_matrix_manifest_tracks_current_surface() { assert_eq!( bridge_declined, BTreeMap::from([ - ( - "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" @@ -1356,7 +1344,7 @@ fn hostile_models_baseline(prefix: &str) -> Option { "developer preflight must never emit the certification verdict:\n{clean_report}" ); assert!( - clean_report.contains("source-bridges: 22 of 22 credited"), + clean_report.contains("source-bridges: 25 of 25 credited"), "the honest baseline credits every goals bridge:\n{clean_report}" ); @@ -1468,8 +1456,8 @@ fn assert_hostile_source_model_loses_bridges(prefix: &str, edits: &[(&str, &str) ); assert!( report.contains(&format!( - "source-bridges: {} of 22 credited", - 22 - lost.len() + "source-bridges: {} of 25 credited", + 25 - lost.len() )), "exactly the bridges through the wrong definition must lose their credit:\n{report}" ); diff --git a/tests/cert_hardening_spec.rs b/tests/cert_hardening_spec.rs index 0ff1b32e8..c601e17af 100644 --- a/tests/cert_hardening_spec.rs +++ b/tests/cert_hardening_spec.rs @@ -40,7 +40,8 @@ //! slots are exchanged; //! * a List literal's cons helper declared as a user function of the same //! signature, a cons helper whose plan is not the cons plan, and the cons -//! helpers of two instantiations exchanged. +//! helpers of two instantiations exchanged; +//! * a bridge whose List argument encoder names another element type. //! //! Gated behind `wasm` and skipped when `lake` is unavailable, like the other //! certificate suites. @@ -1410,7 +1411,9 @@ fn cert_hardening_declines_a_bridged_law_that_does_not_use_its_model() { /// 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`. +/// struct in `else`. Every export takes a List, so each has a source bridge +/// only through the List decoder, and the law over `count` is on bytes only +/// through `count`'s bridge. const LISTY: &str = "module Listy intent = \"List match shapes.\" exposes [count, firstOr, isEmpty] @@ -1435,6 +1438,10 @@ fn isEmpty(xs: List) -> Bool verify count count([]) => 0 + +verify count law neverNegative + given xs: List = [[], [1], [1, 2]] + count(xs) >= 0 => true "; /// Emit the List certificate into a fresh scratch directory. @@ -1475,6 +1482,34 @@ fn cert_hardening_accepts_list_matches() { let (ok, report) = aver_cert("check", &wasm, &cert); assert!(ok, "the List certificate must check:\n{report}"); assert!(report.contains("3 checked exports"), "{report}"); + assert!( + report.contains("source-bridges: 3 of 3 credited"), + "every List argument decodes:\n{report}" + ); + assert!( + report.contains("bridged-laws: 1 of 1 credited"), + "the law over a List function is on bytes:\n{report}" + ); +} + +/// The encoders of a bridge are the statement: the checker renders it from +/// the manifest. Declaring `count`'s argument a List of Strings states a +/// bridge about a model function that takes a List of Ints: the statement no +/// longer elaborates, and the package is refused. +#[test] +fn cert_hardening_declines_a_list_bridge_with_another_element_encoder() { + let Some((_dir, wasm, cert)) = list_baseline("certharden-list-bridge-elem") else { + return; + }; + replace_once( + &cert.join("cert-manifest.json"), + "\"model\": \"Listy.count\", \"kind\": \"adequate\", \"params\": [{\"kind\": \"list\", \ + \"elem\": {\"kind\": \"int\"}}]", + "\"model\": \"Listy.count\", \"kind\": \"adequate\", \"params\": [{\"kind\": \"list\", \ + \"elem\": {\"kind\": \"string\"}}]", + ); + let (ok, report) = aver_cert("check", &wasm, &cert); + assert_declined(ok, &report, "the checker-owned Lean witness failed"); } /// The arm pick is the wall's, not the plan's: a plan that gives the `[]` diff --git a/tools/cert-baseline.json b/tools/cert-baseline.json index 59bbac950..1449b1eb6 100644 --- a/tools/cert-baseline.json +++ b/tools/cert-baseline.json @@ -1,7 +1,10 @@ { "examples/data/json.av": { "bridges": [ + "Bytes_allInRange", "Bytes_byteToHex", + "Bytes_firstOutOfRange", + "Bytes_firstOutOfRangeIndex", "Bytes_hexDigit", "Bytes_highNibble", "Bytes_lowNibble", @@ -117,7 +120,10 @@ "App_Render_sampleSettlement", "App_Render_sampleSummary", "App_Render_settlementKindText", + "Bytes_allInRange", "Bytes_byteToHex", + "Bytes_firstOutOfRange", + "Bytes_firstOutOfRangeIndex", "Bytes_hexDigit", "Bytes_highNibble", "Bytes_lowNibble", @@ -125,6 +131,7 @@ "Domain_Cases_auditForResolvedCase", "Domain_Cases_makeCaseDraft", "Domain_Cases_statusText", + "Domain_Cases_tail", "Domain_Ledger_emptyState", "Domain_Ledger_eventAmount", "Domain_Ledger_eventAt", @@ -143,6 +150,7 @@ "Domain_Normalize_normalizeWebhookEvent", "Domain_Reconcile_amountMissing", "Domain_Reconcile_compareAmounts", + "Domain_Reconcile_compareCurrency", "Domain_Reconcile_sampleCaptureRow", "Domain_Reconcile_sampleRefundRow", "Domain_Reconcile_sampleState", @@ -274,7 +282,10 @@ }, "tests/fixtures/cert_work_job/main.av": { "bridges": [ + "Bytes_allInRange", "Bytes_byteToHex", + "Bytes_firstOutOfRange", + "Bytes_firstOutOfRangeIndex", "Bytes_hexDigit", "Bytes_highNibble", "Bytes_lowNibble", @@ -332,13 +343,16 @@ "intLessZero", "isEven", "isOdd", + "listHeadGoal", "mkOp", "quad", "quoteOrSelf", "shout", "sumFrom", + "sumListGoal", "tagName", - "userName" + "userName", + "wrapItems" ], "certified": { "addTwo": "L1", @@ -405,6 +419,8 @@ "bridges": [ "addPair", "boolAnd", + "listHead", + "sumList", "tick" ], "certified": { @@ -706,7 +722,8 @@ }, "tools/certkit/fixtures/verbatimgen.av": { "bridges": [ - "tagName" + "tagName", + "wrapItems" ], "certified": { "tagName": "L1", @@ -715,7 +732,9 @@ "laws": [] }, "tools/certkit/fixtures/verbatimwiden.av": { - "bridges": [], + "bridges": [ + "wrapItems" + ], "certified": { "wrapItems": "L1" },