Extended tuple, array, slice support (#27)

Lampe/Lampe.lean

@@ -269,15 +269,44 @@ nr_def call_decl<>(x: Field, y : Field) -> Field {
    STHoare p ⟨[(struct_construct.name, struct_construct.fn)], []⟩
      ⟦⟧ (call_decl.fn.body _ h![] |>.body h![x, y]) (fun v => v = x) := by
   simp only [call_decl, struct_construct]
-  steps <;> tauto
-  . simp_all [exists_const, SLP.true_star]
+  apply STHoare.letIn_intro
+  on_goal 3 => exact (fun (v : Tp.denote p $ .tuple _ [.field, .field]) => v = (x, y, ()))
+  apply STHoare.callDecl_intro <;> tauto
+  . apply STHoare.letIn_intro
+    . steps
+    . intros
+      steps
+      aesop
+  . intros
     steps
-    simp_all [exists_const, SLP.true_star]
-    simp_all [SLP.entails, SLP.wand, SLP.star, SLP.lift, SLP.forall']
-    intros
-    exists ∅, ∅
-    simp_all
-    apply And.intro rfl ?_
-    exists ∅, ∅
-    simp_all
-    apply And.intro rfl rfl
+    aesop
+
+
+nr_def simple_tuple<>() -> Field {
+  let t = `(1 : Field, true, 3 : Field);
+  t.2 : Field
+}
+
+example : STHoare p Γ ⟦⟧ (simple_tuple.fn.body _ h![] |>.body h![]) (fun (v : Tp.denote p .field) => v = 3) := by
+  simp only [simple_tuple]
+  steps
+  aesop
+
+nr_def simple_slice<>() -> bool {
+  let s = &[true, false];
+  s[[1 : u32]]
+}
+
+example : STHoare p Γ ⟦⟧ (simple_slice.fn.body _ h![] |>.body h![]) (fun (v : Tp.denote p .bool) => v = false) := by
+  simp only [simple_slice, Expr.mkSlice]
+  steps <;> aesop
+
+nr_def simple_array<>() -> Field {
+  let arr = [1 : Field, 2 : Field];
+  arr[1 : u32]
+}
+
+example : STHoare p Γ ⟦⟧ (simple_array.fn.body _ h![] |>.body h![]) (fun (v : Tp.denote p .field) => v = 2) := by
+  simp only [simple_array, Expr.mkArray]
+  steps <;> tauto
+  aesop

Lampe/Lampe/Builtin/Array.lean

@@ -1,6 +1,105 @@
 import Lampe.Builtin.Basic
 namespace Lampe.Builtin
 
+lemma _root_.Finmap.insert_mem_disjoint [DecidableEq α] {m₁ m₂ : Finmap fun _ : α => β} {hd : m₁.Disjoint m₂} {he : ref ∈ m₁} :
+  (m₁.insert ref v).Disjoint m₂ := by
+  rw [Finmap.insert_eq_singleton_union]
+  have _ : ref ∉ m₂ := by aesop
+  simp only [Finmap.disjoint_union_left]
+  aesop
+
+lemma Nat.dec_add_eq_self {n : Nat} {h : n ≠ 0} : n - 1 + 1 = n := by
+  cases n
+  contradiction
+  simp
+
+lemma Fin.n_is_non_zero {h : Fin n} : n > 0 := by
+  cases_type Fin
+  cases n
+  contradiction
+  simp
+
+lemma Mathlib.Vector.get_after_erase {idx : Nat} {vec : Mathlib.Vector α n} {h₁ h₂ h₃} :
+  (Mathlib.Vector.eraseIdx ⟨idx, h₁⟩ vec).get ⟨idx, h₂⟩ = Mathlib.Vector.get vec ⟨idx + 1, h₃⟩ := by
+  unfold Mathlib.Vector.get Mathlib.Vector.eraseIdx
+  cases vec
+  simp_all only [Fin.cast_mk, List.get_eq_getElem]
+  rename List _ => l
+  rename_i P
+  subst_vars
+  revert idx
+  induction l
+  . intros
+    rename Nat => idx
+    unfold List.length at *
+    contradiction
+  . rename_i head₁ tail₁ ih
+    intros idx h₁ h₂ h₃
+    cases idx
+    . simp_all
+    . simp only [List.eraseIdx_cons_succ, List.getElem_cons_succ]
+      apply ih
+      . aesop
+      . simp_all only [List.length_cons, add_lt_add_iff_right, add_tsub_cancel_right]
+        rw [←add_lt_add_iff_right (a := 1)]
+        have _ : tail₁.length ≠ 0 := by aesop
+        have ht : tail₁.length - 1 + 1 = tail₁.length := by simp_all [Nat.dec_add_eq_self]
+        simp_all
+      . aesop
+
+lemma Mathlib.Vector.get_after_insert {idx : Nat} {vec : Mathlib.Vector α n} {h} :
+  (Mathlib.Vector.insertNth v ⟨idx, h⟩ vec).get ⟨idx, h⟩ = v := by
+  unfold Mathlib.Vector.insertNth Mathlib.Vector.get
+  cases vec
+  simp_all only [List.get_eq_getElem, Fin.coe_cast]
+  apply List.get_insertNth_self
+  subst_vars
+  linarith
+
+@[reducible]
+def replaceArray' (arr : Tp.denote p (.array tp n)) (idx : Fin n.toNat) (v : Tp.denote p tp) : Tp.denote p (.array tp n) :=
+  let arr' := (arr.insertNth v ⟨idx.val + 1, by aesop⟩)
+  arr'.eraseIdx ⟨idx.val, by cases idx; tauto⟩
+
+example {p} : (replaceArray' (p := p) (n := ⟨3, by aesop⟩) (tp := .bool) ⟨[false, false, false], (by rfl)⟩ ⟨1, by tauto⟩ true).get ⟨1, by tauto⟩ = true := by rfl
+
+@[simp]
+theorem index_replaced_arr {n : U 32} {idx : Fin n.toNat} {arr} :
+  (replaceArray' arr idx v').get idx = v' := by
+  unfold replaceArray'
+  cases em (n.toNat > 0)
+  . simp_all only [gt_iff_lt, eq_mp_eq_cast]
+    generalize h₁ : (Mathlib.Vector.insertNth _ _ _) = arr₁
+    cases idx
+    rw [Mathlib.Vector.get_after_erase, ←h₁]
+    apply Mathlib.Vector.get_after_insert
+  . simp_all only [gt_iff_lt, not_lt, nonpos_iff_eq_zero, lt_self_iff_false, dite_false]
+    rename_i h
+    rw [h] at idx
+    apply Fin.n_is_non_zero at idx
+    contradiction
+
+/--
+Defines the builtin array constructor.
+-/
+def mkArray (n : U 32) := newGenericPureBuiltin
+  (fun (argTps, tp) => ⟨argTps, (.array tp n)⟩)
+  (fun (argTps, tp) args => ⟨argTps = List.replicate n.toNat tp,
+    fun h => HList.toVec args h⟩)
+
+/--
+Defines the indexing of a array `l : Array tp n` with `i : U 32`
+We make the following assumptions:
+- If `i < n`, then the builtin returns `l[i] : Tp.denote tp`
+- Else (out of bounds access), an exception is thrown.
+
+In Noir, this builtin corresponds to `T[i]` for `T: [T; n]` and `i: uint32`.
+-/
+def arrayIndex := newGenericPureBuiltin
+  (fun (tp, n) => ⟨[.array tp n, .u 32], tp⟩)
+  (fun (_, n) h![l, i] => ⟨i.toNat < n.toNat,
+    fun h => l.get (Fin.mk i.toNat h)⟩)
+
 /--
 Defines the function that evaluates to an array's length `n`.
 This builtin evaluates to an `U 32`. Hence, we assume that `n < 2^32`.
@@ -22,4 +121,10 @@ def arrayAsSlice := newGenericPureBuiltin
   (fun (_, _) h![a] => ⟨True,
     fun _ => a.toList⟩)
 
+def replaceArray := newGenericPureBuiltin
+  (fun (tp, n) => ⟨[.array tp n, .u 32, tp], (.array tp n)⟩)
+  (fun (_, n) h![arr, idx, v] => ⟨idx.toNat < n.toNat,
+    fun h => replaceArray' arr ⟨idx.toNat, h⟩ v⟩)
+
+
 end Lampe.Builtin

Lampe/Lampe/Builtin/Slice.lean

@@ -1,6 +1,18 @@
 import Lampe.Builtin.Basic
 namespace Lampe.Builtin
 
+@[reducible]
+def replaceSlice' (s : Tp.denote p $ .slice tp) (i : Nat) (v : Tp.denote p tp) : Tp.denote p $ .slice tp :=
+  s.eraseIdx i |>.insertNth i v
+
+/--
+Defines the builtin slice constructor.
+-/
+def mkSlice (n : Nat) := newGenericPureBuiltin
+  (fun (argTps, tp) => ⟨argTps, (.slice tp)⟩)
+  (fun (argTps, tp) args => ⟨argTps = List.replicate n tp,
+    fun h => HList.toList args h⟩)
+
 /--
 Defines the indexing of a slice `l : List tp` with `i : U 32`
 We make the following assumptions:
@@ -105,4 +117,9 @@ def sliceRemove := newGenericPureBuiltin
   (fun _ h![l, i] => ⟨i.toNat < l.length,
     fun h => (l.eraseIdx i.toNat, l.get (Fin.mk i.toNat h), ())⟩)
 
+def replaceSlice := newGenericPureBuiltin
+  (fun tp => ⟨[.slice tp, .u 32, tp], (.slice tp)⟩)
+  (fun _ h![sl, idx, v] => ⟨True,
+    fun _ => replaceSlice' sl idx.toNat v⟩)
+
 end Lampe.Builtin

Lampe/Lampe/Builtin/Struct.lean

@@ -18,13 +18,40 @@ lemma listRep_tp_denote_is_tp_denote_tuple :
     tauto
   }
 
+@[reducible]
+def replaceTuple' (tpl : Tp.denoteArgs p tps) (mem : Member tp tps) (v : Tp.denote p tp) : Tp.denoteArgs p tps := match tps with
+| tp :: _ => match tpl, mem with
+  | (_, rem), .head => (v, rem)
+  | (h, rem), .tail m => (h, replaceTuple' rem m v)
+
+example : replaceTuple' (p := p) exampleTuple Member.head false = (false, 4, 5) := rfl
+example : replaceTuple' (p := p) exampleTuple Member.head.tail 3 = (true, 3, 5) := rfl
+example : replaceTuple' (p := p) exampleTuple Member.head.tail.tail 2 = (true, 4, 2) := rfl
+
+@[simp]
+theorem index_replaced_tpl :
+  indexTpl p (replaceTuple' tpl mem v') mem = v' := by
+  induction mem <;> aesop
+
+/--
+Defines the builtin tuple constructor.
+-/
 def mkTuple := newGenericPureBuiltin
   (fun (name, fieldTps) => ⟨fieldTps, (.tuple name fieldTps)⟩)
   (fun _ fieldExprs => ⟨True,
     fun _ => listRep_tp_denote_is_tp_denote_tuple ▸ HList.toProd fieldExprs⟩)
 
+/--
+Defines the indexing/projection of a tuple with a `Member`.
+-/
 def projectTuple (mem : Member outTp fieldTps) := newGenericPureBuiltin
   (fun name => ⟨[.tuple name fieldTps], outTp⟩)
   (fun _ h![tpl] => ⟨True, fun _ => indexTpl _ tpl mem⟩)
 
+
+def replaceTuple (mem : Member tp tps) := newGenericPureBuiltin
+  (fun name => ⟨[.tuple name tps, tp], (.tuple name tps)⟩)
+  (fun _ h![tpl, v] => ⟨True,
+    fun _ => replaceTuple' tpl mem v⟩)
+
 end Lampe.Builtin

Lampe/Lampe/Hoare/Builtins.lean

@@ -126,12 +126,25 @@ lemma pureBuiltin_intro_consequence
 
 -- Arrays
 
-theorem arrayLen_intro : STHoarePureBuiltin p Γ Builtin.arrayLen (by tauto) h![arr] := by
-  apply pureBuiltin_intro_consequence <;> try rfl
+theorem mkArray_intro {n} {argTps : List Tp} {args : HList (Tp.denote p) argTps} {_ : argTps.length = n} :
+  STHoarePureBuiltin p Γ (Builtin.mkArray n) (by tauto) args (a := (argTps, tp)) := by
+  apply pureBuiltin_intro_consequence <;> tauto
   tauto
 
-theorem arrayAsSlice_intro : STHoarePureBuiltin p Γ Builtin.arrayAsSlice (by tauto) h![arr] := by
-  apply pureBuiltin_intro_consequence <;> try rfl
+theorem arrayIndex_intro : STHoarePureBuiltin p Γ Builtin.arrayIndex (by tauto) h![arr, i] (a := (tp, n)) := by
+  apply pureBuiltin_intro_consequence <;> tauto
+  tauto
+
+theorem arrayLen_intro : STHoarePureBuiltin p Γ Builtin.arrayLen (by tauto) h![arr] (a := (tp, n)) := by
+  apply pureBuiltin_intro_consequence <;> tauto
+  tauto
+
+theorem arrayAsSlice_intro : STHoarePureBuiltin p Γ Builtin.arrayAsSlice (by tauto) h![arr] (a := (tp, n)) := by
+  apply pureBuiltin_intro_consequence <;> tauto
+  tauto
+
+theorem replaceArray_intro : STHoarePureBuiltin p Γ Builtin.replaceArray (by tauto) h![arr, idx, v] (a := (tp, n)) := by
+  apply pureBuiltin_intro_consequence <;> tauto
   tauto
 
 -- BigInt
@@ -311,6 +324,11 @@ theorem iFromField_intro : STHoarePureBuiltin p Γ Builtin.iFromField (by tauto)
 
 -- Slice
 
+theorem mkSlice_intro {n} {argTps : List Tp} {args : HList (Tp.denote p) argTps} {_ : argTps.length = n} :
+  STHoarePureBuiltin p Γ (Builtin.mkSlice n) (by tauto) args (a := (argTps, tp)) := by
+  apply pureBuiltin_intro_consequence <;> tauto
+  tauto
+
 theorem sliceLen_intro : STHoarePureBuiltin p Γ Builtin.sliceLen (by tauto) h![s] := by
   apply pureBuiltin_intro_consequence <;> try rfl
   tauto
@@ -343,6 +361,10 @@ theorem sliceRemove_intro : STHoarePureBuiltin p Γ Builtin.sliceRemove (by taut
   apply pureBuiltin_intro_consequence <;> try rfl
   tauto
 
+theorem replaceSlice_intro : STHoarePureBuiltin p Γ Builtin.replaceSlice (by tauto) h![sl, idx, v] := by
+  apply pureBuiltin_intro_consequence <;> try rfl
+  tauto
+
 -- String
 
 theorem strAsBytes_intro : STHoarePureBuiltin p Γ Builtin.strAsBytes (by tauto) h![s] := by
@@ -451,6 +473,10 @@ theorem projectTuple_intro : STHoarePureBuiltin p Γ (Builtin.projectTuple mem)
   apply pureBuiltin_intro_consequence <;> tauto
   tauto
 
+theorem replaceTuple_intro {mem : Member tp tps} : STHoarePureBuiltin p Γ (Builtin.replaceTuple mem) (by tauto) h![tpl, v] := by
+  apply pureBuiltin_intro_consequence <;> try rfl
+  tauto
+
 -- Misc
 
 theorem assert_intro : STHoarePureBuiltin p Γ Builtin.assert (by tauto) h![a] (a := ()) := by