Add builtins and proofs for the Merkle example

Lampe/Lampe.lean

@@ -3,7 +3,6 @@ import Lampe.Ast.Extensions
 import Lampe.Builtin.Arith
 import Lampe.Builtin.Array
 import Lampe.Builtin.Basic
-import Lampe.Builtin.BigInt
 import Lampe.Builtin.Bit
 import Lampe.Builtin.Cast
 import Lampe.Builtin.Cmp

Lampe/Lampe/Ast/Extensions.lean

@@ -1,7 +1,6 @@
 import Lampe.Ast
 import Lampe.Builtin.Arith
 import Lampe.Builtin.Array
-import Lampe.Builtin.BigInt
 import Lampe.Builtin.Bit
 import Lampe.Builtin.Cmp
 import Lampe.Builtin.Field
@@ -30,13 +29,13 @@ def Expr.writeRef (ref : rep tp.ref) (val : rep tp) : Lampe.Expr rep .unit :=
 
 /-- A utility function for creating a slice expression. -/
 @[reducible]
-def Expr.mkSlice (n : Nat) (vals : HList rep (List.replicate n tp)) 
+def Expr.mkSlice (n : Nat) (vals : HList rep (List.replicate n tp))
   : Lampe.Expr rep (.slice tp) :=
   Lampe.Expr.callBuiltin _ (.slice tp) .mkSlice vals
 
 /-- A utility function for creating an array expression. -/
 @[reducible]
-def Expr.mkArray (n : Lampe.U 32) (vals : HList rep (List.replicate n.toNat tp)) 
+def Expr.mkArray (n : Lampe.U 32) (vals : HList rep (List.replicate n.toNat tp))
   : Lampe.Expr rep (.array tp n) :=
   Lampe.Expr.callBuiltin _ (.array tp n) .mkArray vals
 
@@ -52,7 +51,7 @@ def Expr.mkRepArray (n : Lampe.U 32) (val : rep tp) : Lampe.Expr rep (.array tp
 
 /-- A utility function for creating a tuple expression. -/
 @[reducible]
-def Expr.mkTuple (name : Option String) (args : HList rep tps) 
+def Expr.mkTuple (name : Option String) (args : HList rep tps)
   : Lampe.Expr rep (.tuple name tps) :=
   Lampe.Expr.callBuiltin tps (.tuple name tps) .mkTuple args
 
@@ -64,12 +63,12 @@ def Expr.modifyLens (r : rep $ .ref tp₁) (v : rep tp₂) (lens : Lampe.Lens re
 
 /-- A utility function for creating a lens read expression. -/
 @[reducible]
-def Expr.getLens (v : rep tp₁) (lens : Lampe.Lens rep tp₁ tp₂) 
+def Expr.getLens (v : rep tp₁) (lens : Lampe.Lens rep tp₁ tp₂)
   : Lampe.Expr rep tp₂ :=
   Lampe.Expr.callBuiltin _ tp₂ (.getLens lens) h![v]
 
 /-- A utility function for creating a member access. -/
 @[reducible]
 def Expr.getMember (v : rep (Tp.tuple name tps)) (member : Lampe.Builtin.Member tp tps)
-  : Lampe.Expr rep tp := 
+  : Lampe.Expr rep tp :=
   Expr.callBuiltin _ tp (Lampe.Builtin.getMember member) h![v]

Lampe/Lampe/Builtin/Basic.lean

@@ -70,6 +70,46 @@ end Lampe
 
 namespace Lampe.Builtin
 
+inductive genericOmni {A : Type}
+  (sgn : A → List Tp × Tp)
+  (desc : {p : Prime} → (a : A) → (args : HList (Tp.denote p) (sgn a).fst) → (Tp.denote p (sgn a).snd) → Prop)
+  : Omni where
+  | ok {p st a args Q val} :
+    (h : desc a args val)
+      → Q (some (st, val))
+      → (genericOmni sgn desc) p st (sgn a).fst (sgn a).snd args Q
+  | err {p st a args Q} :
+    (h : ∀ val, ¬ desc a args val)
+      → Q none
+      → (genericOmni sgn desc) p st (sgn a).fst (sgn a).snd args Q
+
+def newGenericBuiltin {A : Type}
+  (sgn : A → List Tp × Tp)
+  (desc : {p : Prime} → (a : A) → (args : HList (Tp.denote p) (sgn a).fst) → (Tp.denote p (sgn a).snd) → Prop) : Builtin := {
+  omni := genericOmni sgn desc
+  conseq := by
+    unfold omni_conseq
+    intros
+    cases_type genericOmni
+    · apply genericOmni.ok <;> tauto
+    · apply genericOmni.err <;> tauto
+  frame := by
+    unfold omni_frame
+    intros
+    cases_type genericOmni
+    · apply genericOmni.ok
+      · assumption
+      · simp
+        repeat apply Exists.intro
+        constructor
+        · assumption
+        · tauto
+    · apply genericOmni.err
+      · assumption
+      · simp
+        tauto
+}
+
 inductive genericPureOmni {A : Type}
   (sgn : A → List Tp × Tp)
   (desc : {p : Prime}
@@ -165,6 +205,17 @@ def assert := newPureBuiltin
   (fun h![a] => ⟨a == true,
     fun _ => ()⟩)
 
+/--
+Defines the static assertion builtin that takes a boolean and a message of type `tp : Tp`.
+We assume the following:
+- If `a == true`, it evaluates to `()`.
+- Else, an exception is thrown.
+-/
+def staticAssert := newGenericPureBuiltin
+  (fun tp => ⟨[.bool, tp], .unit⟩)
+  (fun _ h![a, _] => ⟨a == true,
+    fun _ => ()⟩)
+
 inductive freshOmni : Omni where
 | mk {P st tp Q} : (∀ v, Q (some (st, v))) → freshOmni P st [] tp h![] Q
 

Lampe/Lampe/Builtin/Field.lean

@@ -6,9 +6,10 @@ For a prime `p`, a field element `a : Fp p`, and a bit size `w : U 32`,
 this builtin evaluates to `()` if and only if `a < 2^w`, i.e., it can be represented by `w` bits.
 Otherwise, an exception is thrown.
 
-In Noir, this builtin corresponds to `fn __assert_max_bit_size(self, bit_size: u32)` implemented for `Field`.
+In Noir, this builtin corresponds to `fn __assert_max_bit_size(self, bit_size: u32)` implemented
+for `Field`.
 -/
-def fApplyRangeConstraint := newPureBuiltin
+def applyRangeConstraint := newPureBuiltin
   ⟨[.field, (.u 32)], .unit⟩
   (fun h![a, w] => ⟨a.val < 2^w.toNat,
     fun _ => ()⟩)
@@ -22,8 +23,8 @@ In Noir, this builtin corresponds to `fn modulus_num_bits() -> u64` implemented
 -/
 def fModNumBits := newPureBuiltin
   ⟨[.field], (.u 64)⟩
-  (@fun p h![_] => ⟨numBits p.val < 2^64,
-    fun _ => numBits p.val⟩)
+  (@fun p h![_] => ⟨numBits p.natVal < 2^64,
+    fun _ => numBits p.natVal⟩)
 
 /--
 For a prime `p`, a field element `a : Fp p`, this builtin evaluates to the bit representation of `p` in little-endian format.
@@ -32,7 +33,7 @@ In Noir, this builtin corresponds to `fn modulus_le_bits() -> [u1]` implemented
 -/
 def fModLeBits := newTotalPureBuiltin
   ⟨[.field], (.slice (.u 1))⟩
-  (@fun p h![_] => decomposeToRadix 2 p.val (by tauto))
+  (@fun p h![_] => RadixVec.of ⟨2, by linarith⟩ p.natVal |>.toDigitsBE.toList.reverse)
 
 /--
 For a prime `p`, a field element `a : Fp p`, this builtin evaluates to the bit representation of `p` in big-endian format.
@@ -41,7 +42,7 @@ In Noir, this builtin corresponds to `fn modulus_be_bits() -> [u1]` implemented
 -/
 def fModBeBits := newTotalPureBuiltin
   ⟨[.field], (.slice (.u 1))⟩
-  (@fun p h![_] => .reverse (decomposeToRadix 2 p.val (by tauto)))
+  (@fun p h![_] => RadixVec.toDigitsBE' 2 p.natVal |>.map fun d => BitVec.ofNatLT d.val d.prop) --.of ⟨2, by linarith⟩ p.natVal |>.toDigitsBE.toList)
 
 /--
 For a prime `p`, a field element `a : Fp p`, this builtin evaluates to the byte representation of `p` in little-endian format.
@@ -50,7 +51,7 @@ In Noir, this builtin corresponds to `fn modulus_le_bytes() -> [u8]` implemented
 -/
 def fModLeBytes := newTotalPureBuiltin
   ⟨[.field], (.slice (.u 8))⟩
-  (@fun p h![_] => decomposeToRadix 256 p.val (by linarith))
+  (@fun p h![_] => RadixVec.of ⟨256, by linarith⟩ p.natVal |>.toDigitsBE.toList.reverse)
 
 /--
 For a prime `p`, a field element `a : Fp p`, this builtin evaluates to the bit representation of `p` in big-endian format.
@@ -59,7 +60,7 @@ In Noir, this builtin corresponds to `fn modulus_be_bytes() -> [u8]` implemented
 -/
 def fModBeBytes := newTotalPureBuiltin
   ⟨[.field], (.slice (.u 8))⟩
-  (@fun p h![_] => .reverse (decomposeToRadix 256 p.val (by linarith)))
+  (@fun p h![_] => RadixVec.of ⟨256, by linarith⟩ p.natVal |>.toDigitsBE.toList)
 
 /--
 Represents the builtin that converts a field element to an unsigned integer.
@@ -90,7 +91,7 @@ Represents the builtin that converts an unsigned integer into a field element.
 
 Noir's semantics for this conversion take the unsigned integer and zero-extend it up to the size of
 the field. We do this by taking our unsigned int as an arbitrary `i ∈ ℤ` and then convert this to a
-field element by zero extending. In Noir, this builtin corresponds to `fn as_field(self) -> Field` 
+field element by zero extending. In Noir, this builtin corresponds to `fn as_field(self) -> Field`
 implemented for uints of bit size `s`.
 
 Integers are also internally represented as field elements with an additional restriction that all
@@ -111,7 +112,7 @@ Represents the builtin that converts a signed integer into a field element.
 
 Noir's semantics for this conversion take the signed integer and zero-extend it up to the size of
 the field. We do this by taking our signed int as an arbitrary `i ∈ ℤ` and then convert this to a
-field element by zero extending. In Noir, this builtin corresponds to `fn as_field(self) -> Field` 
+field element by zero extending. In Noir, this builtin corresponds to `fn as_field(self) -> Field`
 implemented for uints of bit size `s`.
 
 Integers are also internally represented as field elements with an additional restriction that all
@@ -127,4 +128,86 @@ def iAsField := newGenericTotalPureBuiltin
   -- source of which can be viewed with `set_option trace.Meta.synthInstance`.
   (fun _ h![a] => a.toNat)
 
+/--
+Represents the builtin that returns the bit representation of the modulus of a field in
+little-endian format.
+-/
+def modulusLeBits : Builtin := newTotalPureBuiltin
+  ⟨[], (.slice (.u 1))⟩
+  (fun {p} h![] => RadixVec.of ⟨2, by linarith⟩ p.natVal |>.toDigitsBE.toList.reverse)
+
+/--
+Represents the builtin that returns the bit representation of the modulus of a field in
+big-endian format.
+-/
+def modulusBeBits : Builtin := newTotalPureBuiltin
+  ⟨[], (.slice (.u 1))⟩
+  (fun {p} h![] => RadixVec.toDigitsBE' 2 p.natVal |>.map fun d => BitVec.ofNatLT d.val d.prop)
+
+/--
+Represents the builtin that returns the byte representation of the modulus of a field in
+little-endian format.
+-/
+def modulusLeBytes : Builtin := newTotalPureBuiltin
+  ⟨[], (.slice (.u 8))⟩
+  (fun {p} h![] => RadixVec.of ⟨256, by linarith⟩ p.natVal |>.toDigitsBE.toList.reverse)
+
+/--
+Represents the builtin that returns the byte representation of the modulus of a field in
+big-endian format.
+-/
+def modulusBeBytes : Builtin := newTotalPureBuiltin
+  ⟨[], (.slice (.u 8))⟩
+  (fun {p} h![] => RadixVec.of ⟨256, by linarith⟩ p.natVal |>.toDigitsBE.toList)
+
+/--
+Represents the builtin that returns the number of bits in the modulus of a field.
+-/
+def modulusNumBits : Builtin := newTotalPureBuiltin
+  ⟨[], (.u 64)⟩
+  -- Note: We could use the `log2` definition but this is easier to reason about.
+  (fun {p} h![] => numBits p.natVal)
+
+/--
+Represents the builtin that converts a field element to its bit representation in little-endian format.
+
+Fails if `f ≥ 2^s`.
+-/
+def toLeBits : Builtin := newGenericBuiltin
+  (fun s => ([.field], .array (.u 1) s))
+  fun _ h![f] output =>
+    f = RadixVec.ofDigitsBE (r := 2) (output.map BitVec.toFin).reverse
+
+/--
+Represents the builtin that converts a field element to its bit representation in big-endian format.
+
+Fails if `f ≥ 2^s`.
+-/
+def toBeBits : Builtin := newGenericBuiltin
+  (fun s => ([.field], .array (.u 1) s))
+  fun _ h![f] output =>
+    f = RadixVec.ofDigitsBE (r := 2) (output.map BitVec.toFin)
+
+/--
+Represents the builtin that converts a field element to its radix representation in little-endian
+format.
+
+Fails if `r ≤ 1` or `f ≥ 2^s`.
+-/
+def toLeRadix : Builtin := newGenericBuiltin
+  (fun s => ([.field, .u 32], .array (.u 8) s))
+  fun _ h![f, r] output =>
+    f = RadixVec.ofLimbsBE r.toNat (output.map BitVec.toNat).reverse
+
+/--
+Represents the builtin that converts a field element to its radix representation in big-endian
+format.
+
+Fails if `r ≤ 1` or `f ≥ 2^s`.
+-/
+def toBeRadix : Builtin := newGenericBuiltin
+  (fun s => ([.field, .u 32], .array (.u 8) s))
+  fun _ h![f, r] output =>
+    f = RadixVec.ofLimbsBE r.toNat (output.map BitVec.toNat)
+
 end Lampe.Builtin