cert: certify a match on a List

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

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), <literal>)` 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

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