initial commit

Lampe/Lampe.lean

@@ -16,9 +16,9 @@ example : STHoare p Γ ⟦⟧ (simple_muts.fn.body _ h![] |>.body h![x]) fun v =
 
 nr_def weirdEq<I>(x : I, y : I) -> Unit {
   let a = #fresh() : I;
-  #add(x, y) : I;
-  #assert(#eq(a, x) : bool) : Unit;
-  #assert(#eq(a, y) : bool) : Unit;
+  #fAdd(x, y) : I;
+  #assert(#fEq(a, x) : bool) : Unit;
+  #assert(#fEq(a, y) : bool) : Unit;
 }
 
 example {x y : Tp.denote p .field} : STHoare p Γ ⟦⟧ (weirdEq.fn.body _ h![.field] |>.body h![x, y]) fun _ => x = y := by
@@ -28,8 +28,8 @@ example {x y : Tp.denote p .field} : STHoare p Γ ⟦⟧ (weirdEq.fn.body _ h![.
 
 nr_def sliceAppend<I>(x: [I], y: [I]) -> [I] {
   let mut self = x;
-  for i in (0 : u32) .. #slice_len(y):u32 {
-    self = #slice_push_back(self, #slice_index(y, i): I): [I]
+  for i in (0 : u32) .. #sliceLen(y):u32 {
+    self = #slicePushBack(self, #sliceIndex(y, i): I): [I]
   };
   self
 }
@@ -60,9 +60,9 @@ example {self that : Tp.denote p (.slice tp)} : STHoare p Γ ⟦⟧ (sliceAppend
 
 nr_def simple_if<>(x : Field, y : Field) -> Field {
   let mut z = x;
-  if #eq(x, x) : bool {
+  if #fEq(x, x) : bool {
     z = y
-   }; -- else ()
+   };
   z
 }
 
@@ -78,7 +78,7 @@ example {p Γ x y}: STHoare p Γ ⟦⟧ (simple_if.fn.body _ h![] |>.body h![x,
 
 
 nr_def simple_if_else<>(x : Field, y : Field) -> Field {
-  let z = if #eq(x, x) : bool { x } else { y };
+  let z = if #fEq(x, x) : bool { x } else { y };
   z
 }
 
@@ -92,7 +92,7 @@ example {p Γ x y}: STHoare p Γ ⟦⟧ (simple_if_else.fn.body _ h![] |>.body h
   . aesop
 
 nr_def simple_lambda<>(x : Field, y : Field) -> Field {
-  let add = |a : Field, b : Field| -> Field { #add(a, b) : Field };
+  let add = |a : Field, b : Field| -> Field { #fAdd(a, b) : Field };
   ^add(x, y) : Field;
 }
 
@@ -114,7 +114,7 @@ example {p Γ} {x y : Tp.denote p Tp.field} :
 
 nr_trait_impl[bulbulizeField] <> Bulbulize<> for Field where {
     fn bulbulize<>(x : Field) -> Field {
-      #add(x, x) : Field
+      #fAdd(x, x) : Field
     };
 }
 
@@ -129,12 +129,12 @@ def simpleTraitEnv : Env := {
   traits := [bulbulizeField, bulbulizeU32]
 }
 
-def simpleTraitCall (tp : Tp) (arg : tp.denote P): Expr (Tp.denote P) tp :=
+def simple_trait_call (tp : Tp) (arg : tp.denote P): Expr (Tp.denote P) tp :=
   @Expr.call _ [] h![] [tp] tp (.trait ⟨⟨⟨"Bulbulize", [], h![]⟩, tp⟩, "bulbulize"⟩) h![arg]
 
 
-example : STHoare p simpleTraitEnv ⟦⟧ (simpleTraitCall .field arg) (fun v => v = 2 * arg) := by
-  simp only [simpleTraitCall]
+example : STHoare p simpleTraitEnv ⟦⟧ (simple_trait_call .field arg) (fun v => v = 2 * arg) := by
+  simp only [simple_trait_call]
   steps
   apply_impl [] bulbulizeField.2
   tauto
@@ -146,8 +146,8 @@ example : STHoare p simpleTraitEnv ⟦⟧ (simpleTraitCall .field arg) (fun v =>
   subst_vars
   ring
 
-example : STHoare p simpleTraitEnv ⟦⟧ (simpleTraitCall (.u 32) arg) (fun v => v = 69) := by
-  simp only [simpleTraitCall]
+example : STHoare p simpleTraitEnv ⟦⟧ (simple_trait_call (.u 32) arg) (fun v => v = 69) := by
+  simp only [simple_trait_call]
   steps
   apply_impl [] bulbulizeU32.2
   tauto
@@ -157,8 +157,8 @@ example : STHoare p simpleTraitEnv ⟦⟧ (simpleTraitCall (.u 32) arg) (fun v =
   aesop
 
 
-example : STHoare p simpleTraitEnv ⟦⟧ (simpleTraitCall (.u 32) arg) (fun v => v = 69) := by
-  simp only [simpleTraitCall]
+example : STHoare p simpleTraitEnv ⟦⟧ (simple_trait_call (.u 32) arg) (fun v => v = 69) := by
+  simp only [simple_trait_call]
   steps
   try_impls [] [bulbulizeField.2, bulbulizeU32.2]
   tauto
@@ -167,8 +167,8 @@ example : STHoare p simpleTraitEnv ⟦⟧ (simpleTraitCall (.u 32) arg) (fun v =
   steps
   aesop
 
-example : STHoare p simpleTraitEnv ⟦⟧ (simpleTraitCall (.u 32) arg) (fun v => v = 69) := by
-  simp only [simpleTraitCall]
+example : STHoare p simpleTraitEnv ⟦⟧ (simple_trait_call (.u 32) arg) (fun v => v = 69) := by
+  simp only [simple_trait_call]
   steps
   try_impls_all [] simpleTraitEnv
   tauto
@@ -178,13 +178,13 @@ example : STHoare p simpleTraitEnv ⟦⟧ (simpleTraitCall (.u 32) arg) (fun v =
   aesop
 
 
-nr_def simpleTraitCallSyntax<I> (x : I) -> I {
+nr_def simple_trait_call_syntax<I> (x : I) -> I {
   (I as Bulbulize<>)::bulbulize<>(x : I) : I
 }
 
 example {p} {arg : Tp.denote p Tp.field} :
-  STHoare p simpleTraitEnv ⟦⟧ (simpleTraitCallSyntax.fn.body _ h![.field] |>.body h![arg]) (fun v => v = 2 * arg) := by
-  simp only [simpleTraitCallSyntax]
+  STHoare p simpleTraitEnv ⟦⟧ (simple_trait_call_syntax.fn.body _ h![.field] |>.body h![arg]) (fun v => v = 2 * arg) := by
+  simp only [simple_trait_call_syntax]
   steps
   try_impls_all [] simpleTraitEnv
   tauto
@@ -208,13 +208,13 @@ def genericTraitEnv : Env := {
   traits := [me]
 }
 
-nr_def genericTraitCall<>(x : Field) -> Field {
+nr_def generic_trait_call<>(x : Field) -> Field {
   (Field as Me<>)::me<>(x : Field) : Field
 }
 
 example {p} {x : Tp.denote p Tp.field} :
-  STHoare p genericTraitEnv ⟦⟧ (genericTraitCall.fn.body _ h![] |>.body h![x]) (fun v => v = x) := by
-  simp only [genericTraitCall]
+  STHoare p genericTraitEnv ⟦⟧ (generic_trait_call.fn.body _ h![] |>.body h![x]) (fun v => v = x) := by
+  simp only [generic_trait_call]
   steps
   try_impls_all [Tp.field] genericTraitEnv
   tauto
@@ -229,23 +229,33 @@ nr_struct_def Pair <I> {
   b : I
 }
 
-nr_def structConstruct<>(a : Field, b : Field) -> struct Pair<Field> {
-  @Pair { a : Field, b : Field }
+nr_def struct_construct<>(a : Field, b : Field) -> Pair<Field> {
+  Pair<Field> { a, b }
 }
 
 example {p} {a b : Tp.denote p .field} :
-  STHoare p Γ ⟦⟧ (structConstruct.fn.body _ h![] |>.body h![a, b]) (fun v => v.fst = a ∧ v.snd = (b, ())) := by
-  simp only [structConstruct]
+  STHoare p Γ ⟦⟧ (struct_construct.fn.body _ h![] |>.body h![a, b]) (fun v => v.fst = a ∧ v.snd = (b, ())) := by
+  simp only [struct_construct]
   steps
   aesop
 
-nr_def structProjection<>(x : Field, y : Field) -> Field {
-  let s = @Pair { x : Field, y : Field };
-  @Pair<Field> s[a]
+nr_def struct_project<>(x : Field, y : Field) -> Field {
+  let s = Pair<Field> { x, y };
+  (s as Pair<Field>).a
 }
 
 example {p} {x y : Tp.denote p .field} :
-  STHoare p Γ ⟦⟧ (structProjection.fn.body _ h![] |>.body h![x, y]) (fun v => v = x) := by
-  simp only [structProjection]
+  STHoare p Γ ⟦⟧ (struct_project.fn.body _ h![] |>.body h![x, y]) (fun v => v = x) := by
+  simp only [struct_project]
+  steps
+  aesop
+
+nr_def basic_cast<>(x : u8) -> Field {
+  #cast(x) : Field
+}
+
+example {p} {x : Tp.denote p $ .u 8} :
+  STHoare p Γ ⟦⟧ (basic_cast.fn.body _ h![] |>.body h![x]) (fun (v : Tp.denote _ .field) => v = x.toNat) := by
+  simp only [basic_cast]
   steps
   aesop

Lampe/Lampe/Builtin/Cast.lean

@@ -0,0 +1,74 @@
+import Lampe.Builtin.Basic
+namespace Lampe.Builtin
+
+/--
+   Represents the Noir types that can be casted to each other.
+ -/
+ class CastTp (tp tp' : Tp) where
+   validate : Tp.denote p tp → Prop
+   cast : (a : Tp.denote p tp) → (validate a) → Tp.denote p tp'
+
+ @[simp]
+ instance : CastTp tp tp where
+   validate := fun _ => True
+   cast := fun a _ => a
+
+ @[simp]
+ instance : CastTp (.u s) (.i s) where
+   validate := fun a => a.toNat < 2^(s-1)
+   cast := fun a _ => a
+
+ @[simp]
+ instance : CastTp (.u s) (.field) where
+   validate := fun _ => True
+   cast := fun a _ => a.toNat
+
+ @[simp]
+ instance : CastTp (.i s) (.u s) where
+   validate := fun a => a.toNat ≥ 0
+   cast := fun a _ => a
+
+ @[simp]
+ instance : CastTp (.i s) (.field) where
+   validate := fun _ => True
+   cast := fun a _ => a.toNat
+
+ @[simp]
+ instance : CastTp (.field) (.u s) where
+   validate := fun a => a.val < 2^s
+   cast := fun a h => ⟨a.val, h⟩
+
+ @[simp]
+ instance : CastTp (.field) (.i s) where
+   validate := fun a => a.val < 2^(s-1) ∧ a.val ≥ 0
+   cast := fun a h => ⟨a.val, by
+     cases s
+     . simp_all
+     . simp_all only [add_tsub_cancel_right, Nat.pow_succ]
+       linarith
+   ⟩
+
+ inductive castOmni : Omni where
+ | ok {P st tp tp' v Q} [CastTp tp tp'] :
+   (h : CastTp.validate tp' v) → Q (some (st, CastTp.cast v h)) → castOmni P st [tp] tp' h![v] Q
+ | err {P st tp tp' v Q} [CastTp tp tp'] :
+   ¬(CastTp.validate tp' v) → Q none → castOmni P st [tp] tp' h![v] Q
+
+ def cast : Builtin := {
+   omni := castOmni
+   conseq := by
+     unfold omni_conseq
+     intros
+     cases_type castOmni
+     . apply castOmni.ok <;> simp_all
+     . apply castOmni.err <;> simp_all
+   frame := by
+     unfold omni_frame
+     intros
+     cases_type castOmni
+     . apply castOmni.ok
+       . constructor <;> tauto
+     . apply castOmni.err <;> assumption
+ }
+
+ end Lampe.Builtin

Lampe/Lampe/Builtin/Cmp.lean

@@ -16,7 +16,7 @@ Defines the equality comparison between two booleans.
 
 In Noir, this builtin corresponds to `a == b` for values `a`, `b` of type `bool`.
 -/
-def boolEq := newPureBuiltin
+def bEq := newPureBuiltin
   ⟨[.bool, .bool], .bool⟩
   (fun h![a, b] => ⟨True,
     fun _ => a = b⟩)

Lampe/Lampe/Hoare/Builtins.lean

@@ -10,6 +10,7 @@ import Lampe.Builtin.Memory
 import Lampe.Builtin.Slice
 import Lampe.Builtin.Str
 import Lampe.Builtin.Struct
+import Lampe.Builtin.Cast
 
 namespace Lampe.STHoare
 
@@ -237,7 +238,7 @@ theorem iShr_intro : STHoarePureBuiltin p Γ Builtin.iShr (by tauto) h![a, b] :=
 theorem unitEq_intro : STHoarePureBuiltin p Γ Builtin.unitEq (by tauto) h![a, b] (a := ()) := by
    apply pureBuiltin_intro_consequence <;> tauto
 
-theorem boolEq_intro : STHoarePureBuiltin p Γ Builtin.boolEq (by tauto) h![a, b] (a := ()) := by
+theorem bEq_intro : STHoarePureBuiltin p Γ Builtin.bEq (by tauto) h![a, b] (a := ()) := by
    apply pureBuiltin_intro_consequence <;> tauto
    tauto
 
@@ -456,4 +457,19 @@ theorem assert_intro : STHoarePureBuiltin p Γ Builtin.assert (by tauto) h![a] (
   apply pureBuiltin_intro_consequence <;> tauto
   tauto
 
+theorem cast_intro [Builtin.CastTp tp tp'] : STHoare p Γ ⟦⟧ (.call h![] [tp] tp' (.builtin .cast) h![v])
+   (fun v' => ∃∃ h, ⟦@Builtin.CastTp.cast tp tp' _ p v h = v'⟧) := by
+   unfold STHoare THoare
+   intros
+   constructor
+   cases em (Builtin.CastTp.validate tp' v)
+   . apply Builtin.castOmni.ok
+     . simp_all only [SLP.true_star, SLP.star, SLP.exists']
+       apply SLP.ent_star_top
+       aesop
+   . apply Builtin.castOmni.err
+     . tauto
+     . unfold mapToValHeapCondition
+       simp_all
+
 end Lampe.STHoare