From c729ab4b5afdeaf974a24b8dfdf60559be08c8b4 Mon Sep 17 00:00:00 2001 From: utkn Date: Thu, 26 Dec 2024 14:03:05 +0100 Subject: [PATCH 1/6] initial commit --- Lampe/Lampe.lean | 78 +++++++++-------- Lampe/Lampe/Builtin/Cast.lean | 74 ++++++++++++++++ Lampe/Lampe/Builtin/Cmp.lean | 2 +- Lampe/Lampe/Hoare/Builtins.lean | 18 +++- Lampe/Lampe/Syntax.lean | 107 +++++++++--------------- Lampe/Lampe/Tactic/SeparationLogic.lean | 10 ++- 6 files changed, 183 insertions(+), 106 deletions(-) create mode 100644 Lampe/Lampe/Builtin/Cast.lean diff --git a/Lampe/Lampe.lean b/Lampe/Lampe.lean index be684c7..99c38ad 100644 --- a/Lampe/Lampe.lean +++ b/Lampe/Lampe.lean @@ -16,9 +16,9 @@ example : STHoare p Γ ⟦⟧ (simple_muts.fn.body _ h![] |>.body h![x]) fun v = nr_def weirdEq(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(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 (x : I) -> I { +nr_def simple_trait_call_syntax (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 { b : I } -nr_def structConstruct<>(a : Field, b : Field) -> struct Pair { - @Pair { a : Field, b : Field } +nr_def struct_construct<>(a : Field, b : Field) -> Pair { + Pair { 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 s[a] +nr_def struct_project<>(x : Field, y : Field) -> Field { + let s = Pair { x, y }; + (s as Pair).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 diff --git a/Lampe/Lampe/Builtin/Cast.lean b/Lampe/Lampe/Builtin/Cast.lean new file mode 100644 index 0000000..5f12161 --- /dev/null +++ b/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 diff --git a/Lampe/Lampe/Builtin/Cmp.lean b/Lampe/Lampe/Builtin/Cmp.lean index 7292154..a8d8883 100644 --- a/Lampe/Lampe/Builtin/Cmp.lean +++ b/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⟩) diff --git a/Lampe/Lampe/Hoare/Builtins.lean b/Lampe/Lampe/Hoare/Builtins.lean index f8e7fe5..48a9ac3 100644 --- a/Lampe/Lampe/Hoare/Builtins.lean +++ 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 diff --git a/Lampe/Lampe/Syntax.lean b/Lampe/Lampe/Syntax.lean index 5c9bbf5..2bde3b1 100644 --- a/Lampe/Lampe/Syntax.lean +++ b/Lampe/Lampe/Syntax.lean @@ -33,11 +33,16 @@ partial def mkNrIdent [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [ | i => throwError "Unexpected ident {i}" syntax ident : nr_type -syntax "struct" ident "<" nr_type,* ">" : nr_type syntax "${" term "}" : nr_type syntax nr_ident "<" nr_type,* ">" : nr_type syntax "[" nr_type "]" : nr_type +def mkFieldName (structName : String) (fieldName : String) : Lean.Ident := + mkIdent $ Name.mkSimple $ "field" ++ "#" ++ structName ++ "#" ++ fieldName + +def mkStructDefIdent (structName : String) : Lean.Ident := + mkIdent $ Name.mkSimple $ "struct" ++ "#" ++ structName + def mkListLit [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [MonadError m] : List (TSyntax `term) → m (TSyntax `term) | [] => `([]) | x :: xs => do @@ -60,42 +65,15 @@ partial def mkNrType [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [M | `(nr_type| Field) => `(Tp.field) | `(nr_type| Unit) => `(Tp.unit) | `(nr_type| $i:ident) => `($i) -| `(nr_type| struct $i:ident < $generics,*> ) => do +| `(nr_type| $structName:nr_ident < $generics,* >) => do let generics ← generics.getElems.toList.mapM mkNrType - `(Lampe.Struct.tp $i $(←mkHListLit generics)) -| `(nr_type| $i:nr_ident < $generics,* >) => do - let name := mkIdent $ Name.mkSimple $ ← mkNrIdent i - let generics ← generics.getElems.toList.mapM mkNrType - `(Struct.tp $name $(←mkHListLit generics)) + `(Struct.tp $(mkStructDefIdent (←mkNrIdent structName)) $(←mkHListLit generics)) | `(nr_type| ${ $i }) => pure i | `(nr_type| [ $tp ]) => do `(Tp.slice $(←mkNrType tp)) | _ => 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.sub) -| "mul" => ``(Builtin.mul) -| "div" => ``(Builtin.div) -| "eq" => ``(Builtin.fEq) -| "assert" => ``(Builtin.assert) -| "not" => ``(Builtin.not) -| "lt" => ``(Builtin.lt) -| "index" => ``(Builtin.index) -| "cast" => ``(Builtin.cast) -| "modulus_num_bits" => ``(Builtin.fModNumBits) -| "to_le_bytes" => ``(Builtin.toLeBytes) -| "fresh" => ``(Builtin.fresh) -| "slice_len" => ``(Builtin.sliceLen) -| "slice_push_back" => ``(Builtin.slicePushBack) -| "slice_push_front" => ``(Builtin.slicePushFront) -| "slice_pop_back" => ``(Builtin.slicePopBack) -| "slice_index" => ``(Builtin.sliceIndex) -| "slice_pop_front" => ``(Builtin.slicePopFront) -| "slice_insert" => ``(Builtin.sliceInsert) -| "ref" => ``(Builtin.ref) -| "read_ref" => ``(Builtin.readRef) -| "write_ref" => ``(Builtin.writeRef) -| _ => throwError "Unknown builtin {i}" +def mkBuiltin [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [MonadError m] (i : String) : m (TSyntax `term) := + `($(mkIdent $ (Name.mkSimple "Builtin") ++ (Name.mkSimple i))) syntax ident ":" nr_type : nr_param_decl @@ -120,8 +98,8 @@ syntax "^" nr_ident "(" nr_expr,* ")" ":" nr_type : nr_expr -- Lambda call syntax nr_typed_expr := nr_expr ":" nr_type syntax "(" nr_type "as" nr_ident "<" nr_type,* ">" ")" "::" nr_ident "<" nr_type,* ">" "(" nr_typed_expr,* ")" ":" nr_type : nr_expr -syntax "@" nr_ident "<" nr_type,* ">" ident "[" ident "]" : nr_expr -- Struct access -syntax "@" nr_ident "{" sepBy(nr_typed_expr, ",", ",", allowTrailingSep) "}" : nr_expr -- Struct constructor +syntax "(" ident "as" nr_ident "<" nr_type,* ">" ")" "." ident : nr_expr -- Struct access +syntax nr_ident "<" nr_type,* ">" "{" sepBy(nr_expr, ",", ",", allowTrailingSep) "}" : nr_expr -- Struct constructor syntax nr_fn_decl := nr_ident "<" ident,* ">" "(" nr_param_decl,* ")" "->" nr_type "{" sepBy(nr_expr, ";", ";", allowTrailingSep) "}" syntax nr_trait_constraint := nr_type ":" nr_ident "<" nr_type,* ">" @@ -172,9 +150,6 @@ def wrapSimple [MonadSyntax m] (e : TSyntax `term) (ident : Option Lean.Ident) ( let rest ← k ident `(Lampe.Expr.letIn $e fun $ident => $rest) -def mkFieldName (structName : String) (fieldName : String) : Lean.Ident := - mkIdent $ Name.mkSimple (structName |>.append "#" |>.append fieldName) - mutual partial def mkBlock [MonadSyntax m] (items: List (TSyntax `nr_expr)) (k : TSyntax `term → m (TSyntax `term)): m (TSyntax `term) := match items with @@ -201,21 +176,21 @@ partial def mkArgs [MonadSyntax m] (args : List (TSyntax `nr_expr)) (k : List (T mkArgs t fun t => k (h :: t) partial def mkExpr [MonadSyntax m] (e : TSyntax `nr_expr) (vname : Option Lean.Ident) (k : TSyntax `term → m (TSyntax `term)): m (TSyntax `term) := match e with -| `(nr_expr|$n:num : $tp) => do wrapSimple (←``(Lampe.Expr.lit $(←mkNrType tp) $n)) vname k -| `(nr_expr| true) => do wrapSimple (←``(Lampe.Expr.lit Tp.bool 1)) vname k -| `(nr_expr| false) => do wrapSimple (←``(Lampe.Expr.lit Tp.bool 0)) vname k +| `(nr_expr|$n:num : $tp) => do wrapSimple (←`(Lampe.Expr.lit $(←mkNrType tp) $n)) vname k +| `(nr_expr| true) => do wrapSimple (←`(Lampe.Expr.lit Tp.bool 1)) vname k +| `(nr_expr| false) => do wrapSimple (←`(Lampe.Expr.lit Tp.bool 0)) vname k | `(nr_expr| { $exprs;* }) => mkBlock exprs.getElems.toList k | `(nr_expr| $i:ident) => do - if ←isAutoDeref i.getId then wrapSimple (← ``(Lampe.Expr.readRef $i)) vname k else match vname with + if ←isAutoDeref i.getId then wrapSimple (← `(Lampe.Expr.readRef $i)) vname k else match vname with | none => k i - | some _ => wrapSimple (←``(Lampe.Expr.var $i)) vname k + | some _ => wrapSimple (←`(Lampe.Expr.var $i)) vname k | `(nr_expr| # $i:ident ($args,*): $tp) => do mkArgs args.getElems.toList fun argVals => do wrapSimple (←`(Lampe.Expr.call h![] _ $(←mkNrType tp) (.builtin $(←mkBuiltin i.getId.toString)) $(←mkHListLit argVals))) vname k | `(nr_expr| for $i in $lo .. $hi $body) => do mkExpr lo none fun lo => mkExpr hi none fun hi => do - let body ← mkExpr body none (fun x => ``(Lampe.Expr.var $x)) + let body ← mkExpr body none (fun x => `(Lampe.Expr.var $x)) wrapSimple (←`(Lampe.Expr.loop $lo $hi fun $i => $body)) vname k | `(nr_expr| $v:ident = $e) => do mkExpr e none fun eVal => do @@ -223,12 +198,12 @@ partial def mkExpr [MonadSyntax m] (e : TSyntax `nr_expr) (vname : Option Lean.I | `(nr_expr| ( $e )) => mkExpr e vname k | `(nr_expr| if $cond $mainBody else $elseBody) => do mkExpr cond none fun cond => do - let mainBody ← mkExpr mainBody none fun x => ``(Lampe.Expr.var $x) - let elseBody ← mkExpr elseBody none fun x => ``(Lampe.Expr.var $x) + let mainBody ← mkExpr mainBody none fun x => `(Lampe.Expr.var $x) + let elseBody ← mkExpr elseBody none fun x => `(Lampe.Expr.var $x) wrapSimple (←`(Lampe.Expr.ite $cond $mainBody $elseBody)) vname k | `(nr_expr| if $cond $mainBody) => do mkExpr cond none fun cond => do - let mainBody ← mkExpr mainBody none fun x => ``(Lampe.Expr.var $x) + let mainBody ← mkExpr mainBody none fun x => `(Lampe.Expr.var $x) wrapSimple (←`(Lampe.Expr.ite $cond $mainBody (Lampe.Expr.skip))) vname k | `(nr_expr| | $params,* | -> $outTp $lambdaBody) => do let outTp ← mkNrType outTp @@ -238,7 +213,7 @@ partial def mkExpr [MonadSyntax m] (e : TSyntax `nr_expr) (vname : Option Lean.I let args ← mkHListLit (← params.getElems.toList.mapM fun param => match param with | `(nr_param_decl|$i:ident : $_) => `($i) | _ => throwUnsupportedSyntax) - let body ← mkExpr lambdaBody none fun x => ``(Lampe.Expr.var $x) + let body ← mkExpr lambdaBody none fun x => `(Lampe.Expr.var $x) wrapSimple (←`(Lampe.Expr.lambda $argTps $outTp (fun $args => $body))) vname k | `(nr_expr| ^ $i:ident ($args,*) : $tp) => do mkArgs args.getElems.toList fun argVals => do @@ -255,13 +230,13 @@ partial def mkExpr [MonadSyntax m] (e : TSyntax `nr_expr) (vname : Option Lean.I mkArgs argExprs fun argVals => do wrapSimple (←`(@Lampe.Expr.call _ $callGenKinds $callGenVals $(←mkListLit argTps) $(←mkNrType tp) (.trait ⟨⟨⟨$(Syntax.mkStrLit traitName), $traitGenKinds, $traitGenVals⟩, $(←mkNrType selfTp)⟩, $(Syntax.mkStrLit methodName)⟩) $(←mkHListLit argVals))) vname k -| `(nr_expr| @ $structName:nr_ident { $args,* }) => do - let argTps ← args.getElems.toList.mapM fun arg => match arg with | `(nr_typed_expr| $_ : $ty) => mkNrType ty | _ => throwUnsupportedSyntax - let argExprs ← args.getElems.toList.mapM fun arg => match arg with | `(nr_typed_expr| $expr : $_) => pure expr | _ => throwUnsupportedSyntax - let structName ← mkNrIdent structName - mkArgs argExprs fun argVals => do - wrapSimple (←`(Lampe.Expr.call h![] _ (.tuple (some $(Syntax.mkStrLit structName)) $(←mkListLit argTps)) (.builtin Builtin.mkTuple) $(←mkHListLit argVals))) vname k -| `(nr_expr| @ $structName:nr_ident < $structGenVals,* > $ref:ident [ $structField:ident ]) => do +| `(nr_expr| $structName:nr_ident < $structGenVals,* > { $args,* }) => do + let structGenValsSyn ← mkHListLit (←structGenVals.getElems.toList.mapM fun gVal => mkNrType gVal) + let paramTpsSyn ← `(Struct.fieldTypes $(mkStructDefIdent (←mkNrIdent structName)) $structGenValsSyn) + let structName ← mkNrIdent structName + mkArgs args.getElems.toList fun argVals => do + wrapSimple (←`(Lampe.Expr.call h![] _ (.tuple (some $(Syntax.mkStrLit structName)) $paramTpsSyn) (.builtin Builtin.mkTuple) $(←mkHListLit argVals))) vname k +| `(nr_expr| ( $ref:ident as $structName:nr_ident < $structGenVals,* > ) . $structField:ident) => do let structGenValsSyn ← mkHListLit (←structGenVals.getElems.toList.mapM fun gVal => mkNrType gVal) let accessor := mkFieldName (←mkNrIdent structName) (structField.getId.toString) let accessorSyn ← `($accessor $structGenValsSyn) @@ -316,7 +291,7 @@ def mkTraitImpl [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [MonadE pure (traitName, syn) | _ => throwUnsupportedSyntax -def mkStructDef [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [MonadError m] (structName : TSyntax `ident) : Syntax → m (TSyntax `term) +def mkStructDef [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [MonadError m] (structName : TSyntax `nr_ident) : Syntax → m (TSyntax `term) | `(nr_struct_def| < $generics,* > { $params,* }) => do let genericKinds ← mkListLit (←generics.getElems.toList.mapM fun _ => `(Kind.type)) let generics := generics.getElems.toList.map fun tyVar => (mkIdent $ Name.mkSimple tyVar.getId.toString) @@ -324,32 +299,32 @@ def mkStructDef [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [MonadE | `(nr_param_decl| $_:ident : $ty:nr_type) => mkNrType ty | _ => throwUnsupportedSyntax let fieldTypes ← `(fun gs => match gs with | $(←mkHListLit generics) => $(←mkListLit fieldTypes)) - let structNameStrLit := Syntax.mkStrLit structName.getId.toString + let structNameStrLit := Syntax.mkStrLit (←mkNrIdent structName) let syn ← `(Struct.mk $structNameStrLit $genericKinds $fieldTypes) pure syn | _ => throwUnsupportedSyntax -def mkRecMember [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [MonadError m] (i : Nat) : m (TSyntax `term) := match i with +def mkTplMember [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [MonadError m] (i : Nat) : m (TSyntax `term) := match i with | .zero => `(Member.head) -| .succ n' => do `(Member.tail $(←mkRecMember n')) +| .succ n' => do `(Member.tail $(←mkTplMember n')) -def mkStructProjector [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [MonadError m] (structName : TSyntax `ident) : Syntax → m (List $ TSyntax `command) +def mkStructProjector [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [MonadError m] (structName : TSyntax `nr_ident) : Syntax → m (List $ TSyntax `command) | `(nr_struct_def| < $generics,* > { $params,* }) => do let genericKinds ← mkListLit (←generics.getElems.toList.mapM fun _ => `(Kind.type)) let generics := generics.getElems.toList.map fun tyVar => (mkIdent $ Name.mkSimple tyVar.getId.toString) params.getElems.toList.enum.mapM fun (idx, paramSyn) => match paramSyn with | `(nr_param_decl| $paramName:ident : $paramType:nr_type) => do let paramDefTy ← `(match generics with - | $(←mkHListLit generics) => Member $(←mkNrType paramType) (Struct.fieldTypes $structName generics)) + | $(←mkHListLit generics) => Member $(←mkNrType paramType) (Struct.fieldTypes $(mkStructDefIdent (←mkNrIdent structName)) generics)) let paramDefSyn ← `(match generics with - | $(←mkHListLit generics) => $(←mkRecMember idx)) - let defnNameSyn := mkFieldName structName.getId.toString paramName.getId.toString + | $(←mkHListLit generics) => $(←mkTplMember idx)) + let defnNameSyn := mkFieldName (←mkNrIdent structName) paramName.getId.toString `(def $defnNameSyn (generics : HList Kind.denote $genericKinds) : $paramDefTy := $paramDefSyn) | _ => throwUnsupportedSyntax | _ => throwUnsupportedSyntax elab "expr![" expr:nr_expr "]" : term => do - let term ← MonadSyntax.run $ mkExpr expr none fun x => ``(Expr.var $x) + let term ← MonadSyntax.run $ mkExpr expr none fun x => `(Expr.var $x) Elab.Term.elabTerm term.raw none elab "nrfn![" "fn" fn:nr_fn_decl "]" : term => do @@ -366,10 +341,10 @@ elab "nr_trait_impl[" defName:ident "]" impl:nr_trait_impl : command => do let decl ← `(def $defName : String × Lampe.TraitImpl := ($(Syntax.mkStrLit name), $impl)) Elab.Command.elabCommand decl -elab "nr_struct_def" defName:ident defn:nr_struct_def : command => do +elab "nr_struct_def" defName:nr_ident defn:nr_struct_def : command => do -- define the struct itself - let structDefn ← `(def $defName := $(←mkStructDef defName defn)) - Elab.Command.elabCommand structDefn + let cmd ← `(def $(mkStructDefIdent (←mkNrIdent defName)) := $(←mkStructDef defName defn)) + Elab.Command.elabCommand cmd -- define the field projections let projs ← mkStructProjector defName defn _ ← projs.mapM fun cmd => do diff --git a/Lampe/Lampe/Tactic/SeparationLogic.lean b/Lampe/Lampe/Tactic/SeparationLogic.lean index b3a9d7b..a75272b 100644 --- a/Lampe/Lampe/Tactic/SeparationLogic.lean +++ b/Lampe/Lampe/Tactic/SeparationLogic.lean @@ -537,6 +537,7 @@ macro "stephelper1" : tactic => `(tactic|( | apply nested_triple STHoare.callLambda_intro | apply lam_intro | apply callTrait_intro + | apply cast_intro -- memory builtins | apply var_intro | apply ref_intro @@ -548,7 +549,7 @@ macro "stephelper1" : tactic => `(tactic|( | apply slicePushBack_intro -- equality | apply unitEq_intro - | apply boolEq_intro + | apply bEq_intro | apply fEq_intro | apply uEq_intro | apply iEq_intro @@ -591,8 +592,8 @@ macro "stephelper2" : tactic => `(tactic|( | apply consequence_frame_left fresh_intro | apply consequence_frame_left Lampe.STHoare.litU_intro | apply consequence_frame_left assert_intro - -- | apply consequence_frame_left skip_intro | apply consequence_frame_left lam_intro + | apply consequence_frame_left cast_intro -- memory builtins | apply consequence_frame_left var_intro | apply consequence_frame_left ref_intro @@ -604,7 +605,7 @@ macro "stephelper2" : tactic => `(tactic|( | apply consequence_frame_left slicePushBack_intro -- equality | apply consequence_frame_left unitEq_intro - | apply consequence_frame_left boolEq_intro + | apply consequence_frame_left bEq_intro | apply consequence_frame_left fEq_intro | apply consequence_frame_left uEq_intro | apply consequence_frame_left iEq_intro @@ -650,6 +651,7 @@ macro "stephelper3" : tactic => `(tactic|( | apply ramified_frame_top assert_intro | apply ramified_frame_top skip_intro | apply ramified_frame_top lam_intro + | apply ramified_frame_top cast_intro -- memory builtins | apply ramified_frame_top var_intro | apply ramified_frame_top ref_intro @@ -661,7 +663,7 @@ macro "stephelper3" : tactic => `(tactic|( | apply ramified_frame_top slicePushBack_intro -- equality | apply ramified_frame_top unitEq_intro - | apply ramified_frame_top boolEq_intro + | apply ramified_frame_top bEq_intro | apply ramified_frame_top fEq_intro | apply ramified_frame_top uEq_intro | apply ramified_frame_top iEq_intro From e977b28de6f2d93aa20c75f9baf3e0b1128232dd Mon Sep 17 00:00:00 2001 From: utkn Date: Thu, 26 Dec 2024 14:36:24 +0100 Subject: [PATCH 2/6] calldecl support and example proof --- Lampe/Lampe.lean | 22 ++++++++++++++++++++++ Lampe/Lampe/Hoare/SepTotal.lean | 13 +++++++++++++ Lampe/Lampe/Syntax.lean | 17 +++++++++++------ Lampe/Lampe/Tactic/SeparationLogic.lean | 4 +++- Lampe/Lampe/Tp.lean | 1 + 5 files changed, 50 insertions(+), 7 deletions(-) diff --git a/Lampe/Lampe.lean b/Lampe/Lampe.lean index 99c38ad..260771e 100644 --- a/Lampe/Lampe.lean +++ b/Lampe/Lampe.lean @@ -259,3 +259,25 @@ example {p} {x : Tp.denote p $ .u 8} : simp only [basic_cast] steps aesop + +nr_def call_decl<>(x: Field, y : Field) -> Field { + let s = @struct_construct<>(x, y) : Pair; + (s as Pair).a + } + + example {x y : Tp.denote p .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] + 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 diff --git a/Lampe/Lampe/Hoare/SepTotal.lean b/Lampe/Lampe/Hoare/SepTotal.lean index 5ea8e0a..1f202af 100644 --- a/Lampe/Lampe/Hoare/SepTotal.lean +++ b/Lampe/Lampe/Hoare/SepTotal.lean @@ -382,4 +382,17 @@ theorem callTrait_intro {impl} {fname fn} apply_assumption assumption +theorem callDecl_intro {fname fn} + (h_fn : (fname, fn) ∈ Γ.functions) + (hkc : fn.generics = tyKinds) + (htci : (fn.body _ (hkc ▸ generics) |>.argTps) = argTps) + (htco : (fn.body _ (hkc ▸ generics) |>.outTp) = res) + (h_hoare: STHoare p Γ H (htco ▸ (fn.body _ (hkc ▸ generics) |>.body (htci ▸ args))) Q): + STHoare p Γ H + (@Expr.call _ tyKinds generics argTps res (.decl fname) args) + Q := by + unfold STHoare THoare + intros + apply Omni.callDecl <;> tauto + end Lampe.STHoare diff --git a/Lampe/Lampe/Syntax.lean b/Lampe/Lampe/Syntax.lean index 2bde3b1..f014cdf 100644 --- a/Lampe/Lampe/Syntax.lean +++ b/Lampe/Lampe/Syntax.lean @@ -79,9 +79,6 @@ syntax ident ":" nr_type : nr_param_decl syntax num ":" nr_type : nr_expr syntax ident : nr_expr -syntax "#" nr_ident "(" nr_expr,* ")" ":" nr_type : nr_expr -syntax nr_ident "<" nr_type,* ">" "(" nr_expr,* ")" ":" nr_type : nr_expr -syntax nr_ident "<" nr_type,* ">" "{" nr_expr,* "}" : nr_expr syntax "{" sepBy(nr_expr, ";", ";", allowTrailingSep) "}" : nr_expr syntax "${" term "}" : nr_expr syntax "$" ident : nr_expr @@ -94,12 +91,15 @@ syntax "for" ident "in" nr_expr ".." nr_expr nr_expr : nr_expr syntax "(" nr_expr ")" : nr_expr syntax "*(" nr_expr ")" : nr_expr syntax "|" nr_param_decl,* "|" "->" nr_type nr_expr : nr_expr -syntax "^" nr_ident "(" nr_expr,* ")" ":" nr_type : nr_expr -- Lambda call syntax nr_typed_expr := nr_expr ":" nr_type -syntax "(" nr_type "as" nr_ident "<" nr_type,* ">" ")" "::" nr_ident "<" nr_type,* ">" "(" nr_typed_expr,* ")" ":" nr_type : nr_expr syntax "(" ident "as" nr_ident "<" nr_type,* ">" ")" "." ident : nr_expr -- Struct access -syntax nr_ident "<" nr_type,* ">" "{" sepBy(nr_expr, ",", ",", allowTrailingSep) "}" : nr_expr -- Struct constructor +syntax nr_ident "<" nr_type,* ">" "{" nr_expr,* "}" : nr_expr -- Struct constructor + +syntax "#" nr_ident "(" nr_expr,* ")" ":" nr_type : nr_expr -- Builtin call +syntax "(" nr_type "as" nr_ident "<" nr_type,* ">" ")" "::" nr_ident "<" nr_type,* ">" "(" nr_typed_expr,* ")" ":" nr_type : nr_expr -- Trait call +syntax "^" nr_ident "(" nr_expr,* ")" ":" nr_type : nr_expr -- Lambda call +syntax "@" nr_ident "<" nr_type,* ">" "(" nr_expr,* ")" ":" nr_type : nr_expr -- Decl call syntax nr_fn_decl := nr_ident "<" ident,* ">" "(" nr_param_decl,* ")" "->" nr_type "{" sepBy(nr_expr, ";", ";", allowTrailingSep) "}" syntax nr_trait_constraint := nr_type ":" nr_ident "<" nr_type,* ">" @@ -218,6 +218,11 @@ partial def mkExpr [MonadSyntax m] (e : TSyntax `nr_expr) (vname : Option Lean.I | `(nr_expr| ^ $i:ident ($args,*) : $tp) => do mkArgs args.getElems.toList fun argVals => do wrapSimple (←`(Lampe.Expr.call h![] _ $(←mkNrType tp) (.lambda $i) $(←mkHListLit argVals))) vname k +| `(nr_expr| @ $declName:nr_ident < $callGenVals:nr_type,* > ( $args,* ) : $tp) => do + let callGenKinds ← mkListLit (←callGenVals.getElems.toList.mapM fun _ => `(Kind.type)) + let callGenVals ← mkHListLit (←callGenVals.getElems.toList.mapM fun gVal => mkNrType gVal) + mkArgs args.getElems.toList fun argVals => do + wrapSimple (←`(@Lampe.Expr.call _ $callGenKinds $callGenVals _ $(←mkNrType tp) (.decl $(Syntax.mkStrLit (←mkNrIdent declName))) $(←mkHListLit argVals))) vname k | `(nr_expr| ( $selfTp as $traitName < $traitGenVals,* > ) :: $methodName < $callGenVals,* > ( $args,* ) : $tp) => do let argTps ← args.getElems.toList.mapM fun arg => match arg with | `(nr_typed_expr| $_ : $ty) => mkNrType ty | _ => throwUnsupportedSyntax let argExprs ← args.getElems.toList.mapM fun arg => match arg with | `(nr_typed_expr| $expr : $_) => pure expr | _ => throwUnsupportedSyntax diff --git a/Lampe/Lampe/Tactic/SeparationLogic.lean b/Lampe/Lampe/Tactic/SeparationLogic.lean index a75272b..db7531f 100644 --- a/Lampe/Lampe/Tactic/SeparationLogic.lean +++ b/Lampe/Lampe/Tactic/SeparationLogic.lean @@ -536,8 +536,9 @@ macro "stephelper1" : tactic => `(tactic|( | apply skip_intro | apply nested_triple STHoare.callLambda_intro | apply lam_intro - | apply callTrait_intro | apply cast_intro + | apply callTrait_intro + | apply callDecl_intro -- memory builtins | apply var_intro | apply ref_intro @@ -652,6 +653,7 @@ macro "stephelper3" : tactic => `(tactic|( | apply ramified_frame_top skip_intro | apply ramified_frame_top lam_intro | apply ramified_frame_top cast_intro + | apply ramified_frame_top callDecl_intro -- memory builtins | apply ramified_frame_top var_intro | apply ramified_frame_top ref_intro diff --git a/Lampe/Lampe/Tp.lean b/Lampe/Lampe/Tp.lean index 77191f4..114f71d 100644 --- a/Lampe/Lampe/Tp.lean +++ b/Lampe/Lampe/Tp.lean @@ -61,6 +61,7 @@ inductive Member : Tp → List Tp → Type where | head : Member tp (tp :: tps) | tail : Member tp tps → Member tp (tp' :: tps) +@[reducible] def indexTpl (tpl : Tp.denoteArgs p tps) (mem : Member tp tps) : Tp.denote p tp := match tps with | tp :: _ => match tpl, mem with | (h, _), .head => h From 6e1e0272b987353bdb3d70ed4aa0569592d4a766 Mon Sep 17 00:00:00 2001 From: utkn Date: Thu, 26 Dec 2024 17:47:02 +0100 Subject: [PATCH 3/6] array slice tuple access --- Lampe/Lampe.lean | 44 +++++-- Lampe/Lampe/Builtin/Array.lean | 105 +++++++++++++++ Lampe/Lampe/Builtin/Slice.lean | 17 +++ Lampe/Lampe/Builtin/Struct.lean | 27 ++++ Lampe/Lampe/Hoare/Builtins.lean | 26 ++++ Lampe/Lampe/Syntax.lean | 164 ++++++++++++++++++------ Lampe/Lampe/Tactic/SeparationLogic.lean | 78 +++++++++-- Lampe/Lampe/Tp.lean | 34 +++++ 8 files changed, 437 insertions(+), 58 deletions(-) diff --git a/Lampe/Lampe.lean b/Lampe/Lampe.lean index 260771e..889bb91 100644 --- a/Lampe/Lampe.lean +++ b/Lampe/Lampe.lean @@ -272,12 +272,40 @@ nr_def call_decl<>(x: Field, y : Field) -> Field { steps <;> tauto . simp_all [exists_const, SLP.true_star] steps - simp_all [exists_const, SLP.true_star] + simp only [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 + . sorry + +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 _ .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 + on_goal 3 => exact fun v => v = 2 + rotate_left + steps; aesop + simp_all + simp only [Expr.readArray] + sorry diff --git a/Lampe/Lampe/Builtin/Array.lean b/Lampe/Lampe/Builtin/Array.lean index 896c910..e09f4fd 100644 --- a/Lampe/Lampe/Builtin/Array.lean +++ b/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 diff --git a/Lampe/Lampe/Builtin/Slice.lean b/Lampe/Lampe/Builtin/Slice.lean index 36a9ffa..238da87 100644 --- a/Lampe/Lampe/Builtin/Slice.lean +++ b/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 diff --git a/Lampe/Lampe/Builtin/Struct.lean b/Lampe/Lampe/Builtin/Struct.lean index 65521e4..963b7f4 100644 --- a/Lampe/Lampe/Builtin/Struct.lean +++ b/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 diff --git a/Lampe/Lampe/Hoare/Builtins.lean b/Lampe/Lampe/Hoare/Builtins.lean index 48a9ac3..0f7ecf2 100644 --- a/Lampe/Lampe/Hoare/Builtins.lean +++ b/Lampe/Lampe/Hoare/Builtins.lean @@ -126,6 +126,15 @@ lemma pureBuiltin_intro_consequence -- Arrays +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 arrayIndex_intro : STHoarePureBuiltin p Γ Builtin.arrayIndex (by tauto) h![arr, i] := by + apply pureBuiltin_intro_consequence <;> try rfl + tauto + theorem arrayLen_intro : STHoarePureBuiltin p Γ Builtin.arrayLen (by tauto) h![arr] := by apply pureBuiltin_intro_consequence <;> try rfl tauto @@ -134,6 +143,10 @@ theorem arrayAsSlice_intro : STHoarePureBuiltin p Γ Builtin.arrayAsSlice (by ta apply pureBuiltin_intro_consequence <;> try rfl tauto +theorem replaceArray_intro : STHoarePureBuiltin p Γ Builtin.replaceArray (by tauto) h![arr, idx, v] := by + apply pureBuiltin_intro_consequence <;> try rfl + tauto + -- BigInt theorem bigIntEq_intro : STHoarePureBuiltin p Γ Builtin.bigIntEq (by tauto) h![a, b] (a := ()) := by @@ -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 diff --git a/Lampe/Lampe/Syntax.lean b/Lampe/Lampe/Syntax.lean index f014cdf..18f95f1 100644 --- a/Lampe/Lampe/Syntax.lean +++ b/Lampe/Lampe/Syntax.lean @@ -34,8 +34,10 @@ partial def mkNrIdent [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [ syntax ident : nr_type syntax "${" term "}" : nr_type -syntax nr_ident "<" nr_type,* ">" : nr_type -syntax "[" nr_type "]" : nr_type +syntax nr_ident "<" nr_type,* ">" : nr_type -- Struct +syntax "[" nr_type "]" : nr_type -- Slice +syntax "[" nr_type ";" num "]" : nr_type -- Array +syntax "`(" nr_type,* ")" : nr_type -- Tuple def mkFieldName (structName : String) (fieldName : String) : Lean.Ident := mkIdent $ Name.mkSimple $ "field" ++ "#" ++ structName ++ "#" ++ fieldName @@ -70,11 +72,32 @@ partial def mkNrType [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [M `(Struct.tp $(mkStructDefIdent (←mkNrIdent structName)) $(←mkHListLit generics)) | `(nr_type| ${ $i }) => pure i | `(nr_type| [ $tp ]) => do `(Tp.slice $(←mkNrType tp)) +| `(nr_type| [ $tp ; $len:num ]) => do `(Tp.array $(←mkNrType tp) $len) +| `(nr_type| `($tps,* )) => do + let tps ← tps.getElems.toList.mapM mkNrType + `(Tp.tuple none $(←mkListLit tps)) | _ => throwUnsupportedSyntax def mkBuiltin [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [MonadError m] (i : String) : m (TSyntax `term) := `($(mkIdent $ (Name.mkSimple "Builtin") ++ (Name.mkSimple i))) +@[reducible] +def typeof {rep : Tp → Type _} (_ : rep tp) := tp + +@[reducible] +def tupleFields (tp : Tp) := match tp with +| Tp.tuple _ fields => fields +| _ => [] + +def mkTupleMember [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [MonadError m] (i : Nat) : m (TSyntax `term) := match i with +| .zero => `(Member.head) +| .succ n' => do `(Member.tail $(←mkTupleMember n')) + +def mkStructMember [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [MonadError m] (structName : TSyntax `nr_ident) (gs : List $ TSyntax `nr_type) (field : TSyntax `ident) : m (TSyntax `term) := do + let gs ← mkHListLit (←gs.mapM fun gVal => mkNrType gVal) + let accessor := mkFieldName (←mkNrIdent structName) (field.getId.toString) + `($accessor $gs) + syntax ident ":" nr_type : nr_param_decl syntax num ":" nr_type : nr_expr @@ -85,7 +108,6 @@ syntax "$" ident : nr_expr syntax "let" ident "=" nr_expr : nr_expr syntax "let" "mut" ident "=" nr_expr : nr_expr syntax ident "=" nr_expr : nr_expr -syntax nr_expr "." num : nr_expr syntax "if" nr_expr nr_expr ("else" nr_expr)? : nr_expr syntax "for" ident "in" nr_expr ".." nr_expr nr_expr : nr_expr syntax "(" nr_expr ")" : nr_expr @@ -93,8 +115,16 @@ syntax "*(" nr_expr ")" : nr_expr syntax "|" nr_param_decl,* "|" "->" nr_type nr_expr : nr_expr syntax nr_typed_expr := nr_expr ":" nr_type -syntax "(" ident "as" nr_ident "<" nr_type,* ">" ")" "." ident : nr_expr -- Struct access + syntax nr_ident "<" nr_type,* ">" "{" nr_expr,* "}" : nr_expr -- Struct constructor +syntax "`(" nr_expr,* ")" : nr_expr -- Tuple constructor +syntax "[" nr_expr,* "]" : nr_expr -- Array constructor +syntax "&" "[" nr_expr,* "]" : nr_expr -- Slice constructor + +syntax "(" nr_expr "as" nr_ident "<" nr_type,* ">" ")" "." ident : nr_expr -- Struct access +syntax nr_expr "." num ":" nr_type : nr_expr -- Tuple access +syntax nr_expr "[" nr_expr "]" : nr_expr -- Array access +syntax nr_expr "[[" nr_expr "]]" : nr_expr -- Slice access syntax "#" nr_ident "(" nr_expr,* ")" ":" nr_type : nr_expr -- Builtin call syntax "(" nr_type "as" nr_ident "<" nr_type,* ">" ")" "::" nr_ident "<" nr_type,* ">" "(" nr_typed_expr,* ")" ":" nr_type : nr_expr -- Trait call @@ -108,19 +138,50 @@ syntax nr_trait_impl := "<" ident,* ">" nr_ident "<" nr_type,* ">" "for" nr_type "{" sepBy(nr_trait_fn_def, ";", ";", allowTrailingSep) "}" syntax nr_struct_def := "<" ident,* ">" "{" sepBy(nr_param_decl, ",", ",", allowTrailingSep) "}" -def Expr.letMutIn (definition : Expr rep tp) (body : rep tp.ref → Expr rep tp'): Expr rep tp' := - let refDef := Expr.letIn definition fun v => Expr.call h![] _ (tp.ref) (.builtin .ref) h![v] - Expr.letIn refDef body - -def Expr.ref (val : rep tp): Expr rep tp.ref := +@[reducible] +def Expr.ref (val : rep tp) : Expr rep tp.ref := Expr.call h![] _ tp.ref (.builtin .ref) h![val] -def Expr.readRef (ref : rep tp.ref): Expr rep tp := +@[reducible] +def Expr.readRef (ref : rep tp.ref) : Expr rep tp := Expr.call h![] _ tp (.builtin .readRef) h![ref] -def Expr.writeRef (ref : rep tp.ref) (val : rep tp): Expr rep .unit := +@[reducible] +def Expr.writeRef (ref : rep tp.ref) (val : rep tp) : Expr rep .unit := Expr.call h![] _ .unit (.builtin .writeRef) h![ref, val] +@[reducible] +def Expr.mkSlice (n : Nat) (vals : HList rep (List.replicate n tp)) : Expr rep (.slice tp) := + Expr.call h![] _ (.slice tp) (.builtin $ .mkSlice n) vals + +@[reducible] +def Expr.mkArray (n : Nat) (vals : HList rep (List.replicate n tp)) : Expr rep (.array tp n) := + Expr.call h![] _ (.array tp n) (.builtin $ .mkArray n) vals + +@[reducible] +def Expr.readTuple (tpl : rep $ .tuple name tps) (mem : Member tp tps) : Expr rep tp := + Expr.call h![] [typeof tpl] tp (.builtin (@Builtin.projectTuple tp tps mem)) h![tpl] + +@[reducible] +def Expr.readArray (arr : rep $ .array tp n) (idx : rep $ .u s) : Expr rep tp := + Expr.call h![] _ tp (.builtin .arrayIndex) h![arr, idx] + +@[reducible] +def Expr.readSlice (sl : rep $ .slice tp) (idx : rep $ .u s) : Expr rep tp := + Expr.call h![] _ tp (.builtin .sliceIndex) h![sl, idx] + +@[reducible] +def Expr.replaceTuple (tpl : rep $ .tuple name tps) (mem : Member tp tps) (v : rep tp) : Expr rep (.tuple name tps) := + Expr.call h![] _ (.tuple name tps) (.builtin $ .replaceTuple mem) h![tpl, v] + +@[reducible] +def Expr.replaceArray (arr : rep $ .array tp n) (idx : rep $ .u s) (v : rep tp) : Expr rep (.array tp n) := + Expr.call h![] _ (.array tp n) (.builtin .replaceArray) h![arr, idx, v] + +@[reducible] +def Expr.replaceSlice (sl : rep $ .slice tp) (idx : rep $ .u s) (v : rep tp) : Expr rep (.slice tp) := + Expr.call h![] _ (.slice tp) (.builtin .replaceSlice) h![sl, idx, v] + structure DesugarState where autoDeref : Name → Bool nextFresh : Nat @@ -176,35 +237,45 @@ partial def mkArgs [MonadSyntax m] (args : List (TSyntax `nr_expr)) (k : List (T mkArgs t fun t => k (h :: t) partial def mkExpr [MonadSyntax m] (e : TSyntax `nr_expr) (vname : Option Lean.Ident) (k : TSyntax `term → m (TSyntax `term)): m (TSyntax `term) := match e with -| `(nr_expr|$n:num : $tp) => do wrapSimple (←`(Lampe.Expr.lit $(←mkNrType tp) $n)) vname k -| `(nr_expr| true) => do wrapSimple (←`(Lampe.Expr.lit Tp.bool 1)) vname k -| `(nr_expr| false) => do wrapSimple (←`(Lampe.Expr.lit Tp.bool 0)) vname k +| `(nr_expr|$n:num : $tp) => do wrapSimple (←`(Expr.lit $(←mkNrType tp) $n)) vname k +| `(nr_expr| true) => do wrapSimple (←`(Expr.lit Tp.bool 1)) vname k +| `(nr_expr| false) => do wrapSimple (←`(Expr.lit Tp.bool 0)) vname k | `(nr_expr| { $exprs;* }) => mkBlock exprs.getElems.toList k | `(nr_expr| $i:ident) => do - if ←isAutoDeref i.getId then wrapSimple (← `(Lampe.Expr.readRef $i)) vname k else match vname with + if ←isAutoDeref i.getId then wrapSimple (← `(Expr.readRef $i)) vname k else match vname with | none => k i - | some _ => wrapSimple (←`(Lampe.Expr.var $i)) vname k + | some _ => wrapSimple (←`(Expr.var $i)) vname k | `(nr_expr| # $i:ident ($args,*): $tp) => do mkArgs args.getElems.toList fun argVals => do - wrapSimple (←`(Lampe.Expr.call h![] _ $(←mkNrType tp) (.builtin $(←mkBuiltin i.getId.toString)) $(←mkHListLit argVals))) vname k + wrapSimple (←`(Expr.call h![] _ $(←mkNrType tp) (.builtin $(←mkBuiltin i.getId.toString)) $(←mkHListLit argVals))) vname k | `(nr_expr| for $i in $lo .. $hi $body) => do mkExpr lo none fun lo => mkExpr hi none fun hi => do - let body ← mkExpr body none (fun x => `(Lampe.Expr.var $x)) - wrapSimple (←`(Lampe.Expr.loop $lo $hi fun $i => $body)) vname k + let body ← mkExpr body none (fun x => `(Expr.var $x)) + wrapSimple (←`(Expr.loop $lo $hi fun $i => $body)) vname k | `(nr_expr| $v:ident = $e) => do mkExpr e none fun eVal => do - wrapSimple (←`(Lampe.Expr.writeRef $v $eVal)) vname k + wrapSimple (←`(Expr.writeRef $v $eVal)) vname k | `(nr_expr| ( $e )) => mkExpr e vname k | `(nr_expr| if $cond $mainBody else $elseBody) => do mkExpr cond none fun cond => do - let mainBody ← mkExpr mainBody none fun x => `(Lampe.Expr.var $x) - let elseBody ← mkExpr elseBody none fun x => `(Lampe.Expr.var $x) - wrapSimple (←`(Lampe.Expr.ite $cond $mainBody $elseBody)) vname k + let mainBody ← mkExpr mainBody none fun x => `(Expr.var $x) + let elseBody ← mkExpr elseBody none fun x => `(Expr.var $x) + wrapSimple (←`(Expr.ite $cond $mainBody $elseBody)) vname k | `(nr_expr| if $cond $mainBody) => do mkExpr cond none fun cond => do - let mainBody ← mkExpr mainBody none fun x => `(Lampe.Expr.var $x) - wrapSimple (←`(Lampe.Expr.ite $cond $mainBody (Lampe.Expr.skip))) vname k + let mainBody ← mkExpr mainBody none fun x => `(Expr.var $x) + wrapSimple (←`(Expr.ite $cond $mainBody (Expr.skip))) vname k +| `(nr_expr| & [ $args,* ]) => do + let args := args.getElems.toList + let len := args.length + mkArgs args fun argVals => do + wrapSimple (←`(Expr.mkSlice $(Syntax.mkNumLit $ toString len) $(←mkHListLit argVals))) vname k +| `(nr_expr| [ $args,* ]) => do + let args := args.getElems.toList + let len := args.length + mkArgs args fun argVals => do + wrapSimple (←`(Expr.mkArray $(Syntax.mkNumLit $ toString len) $(←mkHListLit argVals))) vname k | `(nr_expr| | $params,* | -> $outTp $lambdaBody) => do let outTp ← mkNrType outTp let argTps ← mkListLit (← params.getElems.toList.mapM fun param => match param with @@ -213,16 +284,16 @@ partial def mkExpr [MonadSyntax m] (e : TSyntax `nr_expr) (vname : Option Lean.I let args ← mkHListLit (← params.getElems.toList.mapM fun param => match param with | `(nr_param_decl|$i:ident : $_) => `($i) | _ => throwUnsupportedSyntax) - let body ← mkExpr lambdaBody none fun x => `(Lampe.Expr.var $x) - wrapSimple (←`(Lampe.Expr.lambda $argTps $outTp (fun $args => $body))) vname k + let body ← mkExpr lambdaBody none fun x => `(Expr.var $x) + wrapSimple (←`(Expr.lambda $argTps $outTp (fun $args => $body))) vname k | `(nr_expr| ^ $i:ident ($args,*) : $tp) => do mkArgs args.getElems.toList fun argVals => do - wrapSimple (←`(Lampe.Expr.call h![] _ $(←mkNrType tp) (.lambda $i) $(←mkHListLit argVals))) vname k + wrapSimple (←`(Expr.call h![] _ $(←mkNrType tp) (.lambda $i) $(←mkHListLit argVals))) vname k | `(nr_expr| @ $declName:nr_ident < $callGenVals:nr_type,* > ( $args,* ) : $tp) => do let callGenKinds ← mkListLit (←callGenVals.getElems.toList.mapM fun _ => `(Kind.type)) let callGenVals ← mkHListLit (←callGenVals.getElems.toList.mapM fun gVal => mkNrType gVal) mkArgs args.getElems.toList fun argVals => do - wrapSimple (←`(@Lampe.Expr.call _ $callGenKinds $callGenVals _ $(←mkNrType tp) (.decl $(Syntax.mkStrLit (←mkNrIdent declName))) $(←mkHListLit argVals))) vname k + wrapSimple (←`(@Expr.call _ $callGenKinds $callGenVals _ $(←mkNrType tp) (.decl $(Syntax.mkStrLit (←mkNrIdent declName))) $(←mkHListLit argVals))) vname k | `(nr_expr| ( $selfTp as $traitName < $traitGenVals,* > ) :: $methodName < $callGenVals,* > ( $args,* ) : $tp) => do let argTps ← args.getElems.toList.mapM fun arg => match arg with | `(nr_typed_expr| $_ : $ty) => mkNrType ty | _ => throwUnsupportedSyntax let argExprs ← args.getElems.toList.mapM fun arg => match arg with | `(nr_typed_expr| $expr : $_) => pure expr | _ => throwUnsupportedSyntax @@ -233,19 +304,34 @@ partial def mkExpr [MonadSyntax m] (e : TSyntax `nr_expr) (vname : Option Lean.I let methodName ← mkNrIdent methodName let traitName ← mkNrIdent traitName mkArgs argExprs fun argVals => do - wrapSimple (←`(@Lampe.Expr.call _ $callGenKinds $callGenVals $(←mkListLit argTps) $(←mkNrType tp) + wrapSimple (←`(@Expr.call _ $callGenKinds $callGenVals $(←mkListLit argTps) $(←mkNrType tp) (.trait ⟨⟨⟨$(Syntax.mkStrLit traitName), $traitGenKinds, $traitGenVals⟩, $(←mkNrType selfTp)⟩, $(Syntax.mkStrLit methodName)⟩) $(←mkHListLit argVals))) vname k | `(nr_expr| $structName:nr_ident < $structGenVals,* > { $args,* }) => do let structGenValsSyn ← mkHListLit (←structGenVals.getElems.toList.mapM fun gVal => mkNrType gVal) let paramTpsSyn ← `(Struct.fieldTypes $(mkStructDefIdent (←mkNrIdent structName)) $structGenValsSyn) let structName ← mkNrIdent structName mkArgs args.getElems.toList fun argVals => do - wrapSimple (←`(Lampe.Expr.call h![] _ (.tuple (some $(Syntax.mkStrLit structName)) $paramTpsSyn) (.builtin Builtin.mkTuple) $(←mkHListLit argVals))) vname k -| `(nr_expr| ( $ref:ident as $structName:nr_ident < $structGenVals,* > ) . $structField:ident) => do - let structGenValsSyn ← mkHListLit (←structGenVals.getElems.toList.mapM fun gVal => mkNrType gVal) - let accessor := mkFieldName (←mkNrIdent structName) (structField.getId.toString) - let accessorSyn ← `($accessor $structGenValsSyn) - `(.call h![] [.tuple _ _] _ (.builtin (.projectTuple $accessorSyn)) h![$ref]) + wrapSimple (←`(Expr.call h![] _ (.tuple (some $(Syntax.mkStrLit structName)) $paramTpsSyn) (.builtin Builtin.mkTuple) $(←mkHListLit argVals))) vname k +| `(nr_expr| `( $args,* )) => do + mkArgs args.getElems.toList fun argVals => do + let argTps ← argVals.mapM fun arg => `(typeof $arg) + wrapSimple (←`(Expr.call h![] _ (.tuple none $(←mkListLit argTps)) (.builtin Builtin.mkTuple) $(←mkHListLit argVals))) vname k +| `(nr_expr| ( $lhsExpr:nr_expr as $structName:nr_ident < $structGenVals,* > ) . $structField:ident) => do + let mem ← mkStructMember structName structGenVals.getElems.toList structField + mkExpr lhsExpr none fun tpl => do + wrapSimple (←`(Expr.readTuple $tpl $mem)) vname k +| `(nr_expr| $tupleExpr:nr_expr . $idx:num : $_:nr_type) => do + let mem ← mkTupleMember idx.getNat + mkExpr tupleExpr none fun tpl => do + wrapSimple (←`(Expr.readTuple $tpl $mem)) vname k +| `(nr_expr| $lhsExpr:nr_expr [ $idxExpr:nr_expr ]) => do + mkExpr idxExpr none fun idx => do + mkExpr lhsExpr none fun arr => do + wrapSimple (←`(Expr.readArray $arr $idx)) vname k +| `(nr_expr| $lhsExpr:nr_expr [[ $idxExpr:nr_expr ]]) => do + mkExpr idxExpr none fun idx => do + mkExpr lhsExpr none fun arr => do + wrapSimple (←`(Expr.readSlice $arr $idx)) vname k | _ => throwUnsupportedSyntax end @@ -309,10 +395,6 @@ def mkStructDef [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [MonadE pure syn | _ => throwUnsupportedSyntax -def mkTplMember [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [MonadError m] (i : Nat) : m (TSyntax `term) := match i with -| .zero => `(Member.head) -| .succ n' => do `(Member.tail $(←mkTplMember n')) - def mkStructProjector [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [MonadError m] (structName : TSyntax `nr_ident) : Syntax → m (List $ TSyntax `command) | `(nr_struct_def| < $generics,* > { $params,* }) => do let genericKinds ← mkListLit (←generics.getElems.toList.mapM fun _ => `(Kind.type)) @@ -322,7 +404,7 @@ def mkStructProjector [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [ let paramDefTy ← `(match generics with | $(←mkHListLit generics) => Member $(←mkNrType paramType) (Struct.fieldTypes $(mkStructDefIdent (←mkNrIdent structName)) generics)) let paramDefSyn ← `(match generics with - | $(←mkHListLit generics) => $(←mkTplMember idx)) + | $(←mkHListLit generics) => $(←mkTupleMember idx)) let defnNameSyn := mkFieldName (←mkNrIdent structName) paramName.getId.toString `(def $defnNameSyn (generics : HList Kind.denote $genericKinds) : $paramDefTy := $paramDefSyn) | _ => throwUnsupportedSyntax diff --git a/Lampe/Lampe/Tactic/SeparationLogic.lean b/Lampe/Lampe/Tactic/SeparationLogic.lean index db7531f..d755210 100644 --- a/Lampe/Lampe/Tactic/SeparationLogic.lean +++ b/Lampe/Lampe/Tactic/SeparationLogic.lean @@ -60,7 +60,6 @@ theorem exists_star [LawfulHeap α] {P : SLP α} {Q : β → SLP α} : ((∃∃x simp [SLP.star_comm] theorem Lampe.STHoare.litU_intro: STHoare p Γ ⟦⟧ (.lit (.u s) n) fun v => v = n := by - -- apply litU_intro unfold STHoare THoare intro H st hp constructor @@ -68,6 +67,31 @@ theorem Lampe.STHoare.litU_intro: STHoare p Γ ⟦⟧ (.lit (.u s) n) fun v => v apply SLP.ent_star_top assumption +theorem Lampe.STHoare.litField_intro: STHoare p Γ ⟦⟧ (.lit .field n) fun v => v = n := by + unfold STHoare THoare + intro H st hp + constructor + simp only + apply SLP.ent_star_top + assumption + +theorem Lampe.STHoare.litFalse_intro: STHoare p Γ ⟦⟧ (.lit .bool 0) fun v => v = false := by + unfold STHoare THoare + intro H st hp + constructor + simp only + apply SLP.ent_star_top + assumption + +theorem Lampe.STHoare.litTrue_intro: STHoare p Γ ⟦⟧ (.lit .bool 1) fun v => v = true := by + unfold STHoare THoare + intro H st hp + constructor + simp only + apply SLP.ent_star_top + assumption + + theorem ref_intro' {p} {x : Tp.denote p tp} {Γ P}: STHoare p Γ P (.ref x) fun v => [v ↦ ⟨tp, x⟩] ⋆ P := by apply ramified_frame_top @@ -531,6 +555,9 @@ elab "sl" : tactic => do macro "stephelper1" : tactic => `(tactic|( (first | apply Lampe.STHoare.litU_intro + | apply Lampe.STHoare.litField_intro + | apply Lampe.STHoare.litTrue_intro + | apply Lampe.STHoare.litFalse_intro | apply fresh_intro | apply assert_intro | apply skip_intro @@ -539,15 +566,23 @@ macro "stephelper1" : tactic => `(tactic|( | apply cast_intro | apply callTrait_intro | apply callDecl_intro - -- memory builtins + -- memory | apply var_intro | apply ref_intro | apply readRef_intro | apply writeRef_intro - -- slice builtins + -- array + | apply mkArray_intro + | apply arrayLen_intro + | apply arrayIndex_intro + | apply arrayAsSlice_intro + | apply replaceArray_intro + -- slice + | apply mkSlice_intro | apply sliceLen_intro | apply sliceIndex_intro | apply slicePushBack_intro + | apply replaceSlice_intro -- equality | apply unitEq_intro | apply bEq_intro @@ -585,25 +620,37 @@ macro "stephelper1" : tactic => `(tactic|( -- struct | apply mkTuple_intro | apply projectTuple_intro + | apply replaceTuple_intro ) )) macro "stephelper2" : tactic => `(tactic|( (first - | apply consequence_frame_left fresh_intro | apply consequence_frame_left Lampe.STHoare.litU_intro + | apply consequence_frame_left Lampe.STHoare.litField_intro + | apply consequence_frame_left Lampe.STHoare.litTrue_intro + | apply consequence_frame_left Lampe.STHoare.litFalse_intro + | apply consequence_frame_left fresh_intro | apply consequence_frame_left assert_intro | apply consequence_frame_left lam_intro | apply consequence_frame_left cast_intro - -- memory builtins + -- memory | apply consequence_frame_left var_intro | apply consequence_frame_left ref_intro | apply consequence_frame_left readRef_intro | apply consequence_frame_left writeRef_intro - -- slice builtins + -- array + | apply consequence_frame_left mkArray_intro + | apply consequence_frame_left arrayLen_intro + | apply consequence_frame_left arrayIndex_intro + | apply consequence_frame_left arrayAsSlice_intro + | apply consequence_frame_left replaceArray_intro + -- slice + | apply consequence_frame_left mkSlice_intro | apply consequence_frame_left sliceLen_intro | apply consequence_frame_left sliceIndex_intro | apply consequence_frame_left slicePushBack_intro + | apply consequence_frame_left replaceSlice_intro -- equality | apply consequence_frame_left unitEq_intro | apply consequence_frame_left bEq_intro @@ -641,28 +688,40 @@ macro "stephelper2" : tactic => `(tactic|( -- struct | apply consequence_frame_left mkTuple_intro | apply consequence_frame_left projectTuple_intro + | apply consequence_frame_left replaceTuple_intro ) repeat sl )) macro "stephelper3" : tactic => `(tactic|( (first - | apply ramified_frame_top fresh_intro | apply ramified_frame_top Lampe.STHoare.litU_intro + | apply ramified_frame_top Lampe.STHoare.litField_intro + | apply ramified_frame_top Lampe.STHoare.litTrue_intro + | apply ramified_frame_top Lampe.STHoare.litFalse_intro + | apply ramified_frame_top fresh_intro | apply ramified_frame_top assert_intro | apply ramified_frame_top skip_intro | apply ramified_frame_top lam_intro | apply ramified_frame_top cast_intro | apply ramified_frame_top callDecl_intro - -- memory builtins + -- memory | apply ramified_frame_top var_intro | apply ramified_frame_top ref_intro | apply ramified_frame_top readRef_intro | apply ramified_frame_top writeRef_intro - -- slice builtins + -- array + | apply ramified_frame_top mkArray_intro + | apply ramified_frame_top arrayLen_intro + | apply ramified_frame_top arrayIndex_intro + | apply ramified_frame_top arrayAsSlice_intro + | apply ramified_frame_top replaceArray_intro + -- slice + | apply ramified_frame_top mkSlice_intro | apply ramified_frame_top sliceLen_intro | apply ramified_frame_top sliceIndex_intro | apply ramified_frame_top slicePushBack_intro + | apply ramified_frame_top replaceSlice_intro -- equality | apply ramified_frame_top unitEq_intro | apply ramified_frame_top bEq_intro @@ -700,6 +759,7 @@ macro "stephelper3" : tactic => `(tactic|( -- struct | apply ramified_frame_top mkTuple_intro | apply ramified_frame_top projectTuple_intro + | apply ramified_frame_top replaceTuple_intro ) repeat sl )) diff --git a/Lampe/Lampe/Tp.lean b/Lampe/Lampe/Tp.lean index 114f71d..4ac72c8 100644 --- a/Lampe/Lampe/Tp.lean +++ b/Lampe/Lampe/Tp.lean @@ -82,4 +82,38 @@ example : newMember [.bool, .field, .field] ⟨0, (by tauto)⟩ = Member.head := example : newMember [.bool, .field, .field] ⟨1, (by tauto)⟩ = Member.head.tail := rfl example : newMember [.bool, .field, .field] ⟨2, (by tauto)⟩ = Member.head.tail.tail := rfl +lemma List.replicate_head (hl : x :: xs = List.replicate n a) : x = a := by + unfold List.replicate at hl + aesop + +lemma List.replicate_cons (hl : x :: xs = List.replicate n a) : xs = List.replicate (n-1) a := by + unfold List.replicate at hl + cases xs <;> aesop + +@[reducible] +def HList.toList (l : HList rep tps) (_ : tps = List.replicate n tp) : List (rep tp) := match l with +| .nil => [] +| .cons x xs => match tps with + | [] => [] + | _ :: _ => ((List.replicate_head (by tauto)) ▸ x) :: (HList.toList xs (List.replicate_cons (by tauto))) + +lemma HList.toList_cons : + HList.toList (n := n + 1) (HList.cons head rem) h₁ = head :: (HList.toList (n := n) rem h₂) := by + rfl + +lemma HList.toList_length_is_n (h_same : tps = List.replicate n tp) : + (HList.toList l h_same).length = n := by + subst h_same + induction n + cases l + tauto + cases l + rw [HList.toList_cons] + simp_all + rfl + +@[reducible] +def HList.toVec (l : HList rep tps) (h_same : tps = List.replicate n tp) : Mathlib.Vector (rep tp) n := + ⟨HList.toList l h_same, by apply HList.toList_length_is_n⟩ + end Lampe From 0a0717a4314a100d436c26655ad90836f80bc8ca Mon Sep 17 00:00:00 2001 From: utkn Date: Thu, 26 Dec 2024 17:52:54 +0100 Subject: [PATCH 4/6] small change --- Lampe/Lampe.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Lampe/Lampe.lean b/Lampe/Lampe.lean index 889bb91..2124714 100644 --- a/Lampe/Lampe.lean +++ b/Lampe/Lampe.lean @@ -281,7 +281,7 @@ nr_def simple_tuple<>() -> Field { t.2 : Field } -example : STHoare p Γ ⟦⟧ (simple_tuple.fn.body _ h![] |>.body h![]) (fun (v : Tp.denote _ .field) => v = 3) := by +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 From c65feaaf87d5792b629ea7fdd416dd4a83e89f3d Mon Sep 17 00:00:00 2001 From: utkn Date: Fri, 27 Dec 2024 22:46:42 +0300 Subject: [PATCH 5/6] small fixes --- Lampe/Lampe/Syntax.lean | 6 ------ 1 file changed, 6 deletions(-) diff --git a/Lampe/Lampe/Syntax.lean b/Lampe/Lampe/Syntax.lean index 44c73aa..18f95f1 100644 --- a/Lampe/Lampe/Syntax.lean +++ b/Lampe/Lampe/Syntax.lean @@ -39,12 +39,6 @@ syntax "[" nr_type "]" : nr_type -- Slice syntax "[" nr_type ";" num "]" : nr_type -- Array syntax "`(" nr_type,* ")" : nr_type -- Tuple -def mkFieldName (structName : String) (fieldName : String) : Lean.Ident := - mkIdent $ Name.mkSimple $ "field" ++ "#" ++ structName ++ "#" ++ fieldName - -def mkStructDefIdent (structName : String) : Lean.Ident := - mkIdent $ Name.mkSimple $ "struct" ++ "#" ++ structName - def mkFieldName (structName : String) (fieldName : String) : Lean.Ident := mkIdent $ Name.mkSimple $ "field" ++ "#" ++ structName ++ "#" ++ fieldName From cd05bac6c7e5d2af51a986208ab70fb32cd7074f Mon Sep 17 00:00:00 2001 From: utkn Date: Sat, 28 Dec 2024 20:35:04 +0300 Subject: [PATCH 6/6] proofs fixed --- Lampe/Lampe.lean | 23 ++++++++++++----------- Lampe/Lampe/Hoare/Builtins.lean | 16 ++++++++-------- 2 files changed, 20 insertions(+), 19 deletions(-) diff --git a/Lampe/Lampe.lean b/Lampe/Lampe.lean index 2124714..6e3fcb5 100644 --- a/Lampe/Lampe.lean +++ b/Lampe/Lampe.lean @@ -269,12 +269,18 @@ 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 only [exists_const, SLP.true_star] - simp_all [SLP.entails, SLP.wand, SLP.star, SLP.lift, SLP.forall'] - . sorry + aesop + nr_def simple_tuple<>() -> Field { let t = `(1 : Field, true, 3 : Field); @@ -303,9 +309,4 @@ nr_def simple_array<>() -> Field { 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 - on_goal 3 => exact fun v => v = 2 - rotate_left - steps; aesop - simp_all - simp only [Expr.readArray] - sorry + aesop diff --git a/Lampe/Lampe/Hoare/Builtins.lean b/Lampe/Lampe/Hoare/Builtins.lean index 0f7ecf2..cde31bf 100644 --- a/Lampe/Lampe/Hoare/Builtins.lean +++ b/Lampe/Lampe/Hoare/Builtins.lean @@ -131,20 +131,20 @@ theorem mkArray_intro {n} {argTps : List Tp} {args : HList (Tp.denote p) argTps} apply pureBuiltin_intro_consequence <;> tauto tauto -theorem arrayIndex_intro : STHoarePureBuiltin p Γ Builtin.arrayIndex (by tauto) h![arr, i] := 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] := by - apply pureBuiltin_intro_consequence <;> try rfl +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] := by - apply pureBuiltin_intro_consequence <;> try rfl +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] := by - apply pureBuiltin_intro_consequence <;> try rfl +theorem replaceArray_intro : STHoarePureBuiltin p Γ Builtin.replaceArray (by tauto) h![arr, idx, v] (a := (tp, n)) := by + apply pureBuiltin_intro_consequence <;> tauto tauto -- BigInt