Skip to content

Commit

Permalink
Builtin fixes
Browse files Browse the repository at this point in the history
  • Loading branch information
utkn committed Dec 18, 2024
1 parent 8033b35 commit 28f59f8
Show file tree
Hide file tree
Showing 4 changed files with 54 additions and 31 deletions.
32 changes: 14 additions & 18 deletions Lampe/Lampe.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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;
#f_add(x, y) : I;
#assert(#f_eq(a, x) : bool) : Unit;
#assert(#f_eq(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
Expand Down Expand Up @@ -60,7 +60,7 @@ 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 #f_eq(x, x) : bool {
z = y
};
z
Expand All @@ -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 #f_eq(x, x) : bool { x } else { y };
z
}

Expand All @@ -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 { #f_add(a, b) : Field };
^add(x, y) : Field;
}

Expand All @@ -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
#f_add(x, x) : Field
};
}

Expand Down Expand Up @@ -182,7 +182,7 @@ nr_def simpleTraitCallSyntax<I>(x : I) -> I {
(I as Bulbulize<>)::bulbulize<>(x) : I
}

example {p} {arg : Tp.denote p Tp.field} :
example {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]
steps
Expand Down Expand Up @@ -212,7 +212,7 @@ nr_def genericTraitCall<>(x : Field) -> Field {
(Field as Me<>)::me<>(x) : Field
}

example {p} {x : Tp.denote p Tp.field} :
example {x : Tp.denote p Tp.field} :
STHoare p genericTraitEnv ⟦⟧ (genericTraitCall.fn.body _ h![] |>.body h![x]) (fun v => v = x) := by
simp only [genericTraitCall]
steps
Expand All @@ -233,7 +233,7 @@ nr_def structConstruct<>(a : Field, b : Field) -> Pair<Field> {
Pair<Field> { a, b }
}

example {p} {a b : Tp.denote p .field} :
example {a b : Tp.denote p .field} :
STHoare p Γ ⟦⟧ (structConstruct.fn.body _ h![] |>.body h![a, b]) (fun v => v = (a, b, ())) := by
simp only [structConstruct]
steps
Expand All @@ -244,7 +244,7 @@ nr_def structProjection<>(x : Field, y : Field) -> Field {
s[Pair<Field>.a]
}

example {p} {x y : Tp.denote p .field} :
example {x y : Tp.denote p .field} :
STHoare p Γ ⟦⟧ (structProjection.fn.body _ h![] |>.body h![x, y]) (fun v => v = x) := by
simp only [structProjection]
steps
Expand All @@ -255,7 +255,7 @@ nr_def callDecl<>(x: Field, y : Field) -> Field {
s[Pair<Field>.a]
}

example {p} {x y : Tp.denote p .field} :
example {x y : Tp.denote p .field} :
STHoare p ⟨[(structConstruct.name, structConstruct.fn)], []⟩
⟦⟧ (callDecl.fn.body _ h![] |>.body h![x, y]) (fun v => v = x) := by
simp only [callDecl]
Expand All @@ -275,16 +275,12 @@ nr_def createSlice<>() -> [bool] {

example : STHoare p Γ ⟦⟧ (createSlice.fn.body _ h![] |>.body h![]) (fun v => v.get? 1 = some false) := by
simp only [createSlice, Expr.slice]
steps
aesop
aesop
steps <;> aesop

nr_def createArray<>() -> [Field; 2] {
[1 : Field, 2 : Field]
}

example : STHoare p Γ ⟦⟧ (createArray.fn.body _ h![] |>.body h![]) (fun v => v.toList.get? 1 = some 2) := by
simp only [createArray, Expr.array]
steps
aesop
aesop
steps <;> aesop
2 changes: 1 addition & 1 deletion Lampe/Lampe/Builtin/Cmp.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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⟩)
Expand Down
2 changes: 1 addition & 1 deletion Lampe/Lampe/Hoare/Builtins.lean
Original file line number Diff line number Diff line change
Expand Up @@ -227,7 +227,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

Expand Down
49 changes: 38 additions & 11 deletions Lampe/Lampe/Syntax.lean
Original file line number Diff line number Diff line change
Expand Up @@ -70,31 +70,58 @@ partial def mkNrType [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [M
| _ => throwUnsupportedSyntax

partial def mkBuiltin [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [MonadError m] (i : String) : m (TSyntax `term) := match i with
| "add" => `(Builtin.fAdd)
| "sub" => `(Builtin.fSub)
| "mul" => `(Builtin.fMul)
| "div" => `(Builtin.fDiv)
| "eq" => `(Builtin.fEq)
| "assert" => `(Builtin.assert)
| "not" => `(Builtin.bNot)
| "lt" => `(Builtin.lt)
| "cast" => `(Builtin.cast)
| "modulus_num_bits" => `(Builtin.fModNumBits)
| "to_le_bytes" => `(Builtin.toLeBytes)
-- arith
| "f_add" => `(Builtin.fAdd)
| "u_add" => `(Builtin.uAdd)
| "i_add" => `(Builtin.iAdd)
| "f_sub" => `(Builtin.fSub)
| "u_sub" => `(Builtin.uSub)
| "i_sub" => `(Builtin.iSub)
| "f_mul" => `(Builtin.fMul)
| "u_mul" => `(Builtin.uMul)
| "i_mul" => `(Builtin.iMul)
| "f_div" => `(Builtin.fDiv)
| "u_div" => `(Builtin.uDiv)
| "i_div" => `(Builtin.iDiv)
| "u_rem" => `(Builtin.uRem)
| "i_rem" => `(Builtin.iRem)
| "f_neg" => `(Builtin.fNeg)
| "i_neg" => `(Builtin.iNeg)
-- cmp
| "b_eq" => `(Builtin.bEq)
| "f_eq" => `(Builtin.fEq)
| "u_eq" => `(Builtin.uEq)
| "i_eq" => `(Builtin.iEq)
| "unit_eq" => `(Builtin.unitEq)
| "str_eq" => `(Builtin.strEq)
| "u_lt" => `(Builtin.uLt)
| "i_lt" => `(Builtin.iLt)
| "u_gt" => `(Builtin.uGt)
| "i_gt" => `(Builtin.iGt)
-- bit
| "b_not" => `(Builtin.bNot)
-- array
| "array_len" => `(Builtin.arrayLen)
| "array_index" => `(Builtin.arrayIndex)
| "array_as_slice" => `(Builtin.arrayAsSlice)
-- slice
| "slice_len" => `(Builtin.sliceLen)
| "slice_index" => `(Builtin.sliceIndex)
| "slice_push_back" => `(Builtin.slicePushBack)
| "slice_push_front" => `(Builtin.slicePushFront)
| "slice_pop_back" => `(Builtin.slicePopBack)
| "slice_pop_front" => `(Builtin.slicePopFront)
| "slice_insert" => `(Builtin.sliceInsert)
-- memory
| "ref" => `(Builtin.ref)
| "read_ref" => `(Builtin.readRef)
| "write_ref" => `(Builtin.writeRef)
| "fresh" => `(Builtin.fresh)
-- other
| "assert" => `(Builtin.assert)
| "cast" => `(Builtin.cast)
| "modulus_num_bits" => `(Builtin.fModNumBits)
| "to_le_bytes" => `(Builtin.toLeBytes)
| _ => throwError "Unknown builtin {i}"

syntax ident ":" nr_type : nr_param_decl
Expand Down

0 comments on commit 28f59f8

Please sign in to comment.