cert: certify non-empty List literals

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.

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

aver-cert/assets/wall/current/AcceptanceSoundnessCore.lean

@@ -158,18 +158,30 @@ 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 :=
   (List.nodup_append.mp hf.distinct).2.1
 
 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

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. -/

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)

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<t>` 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>` (`(T, List<T>) -> List<T>`) 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<t>` 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<t>`. -/
+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 []

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

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