From e43fcf17e49080ba55de1240c1959b6d6b5f1cc2 Mon Sep 17 00:00:00 2001 From: Matej Penciak Date: Wed, 15 Jan 2025 16:10:46 -0500 Subject: [PATCH 1/3] (wip) Move examples Lampe.lean -> Tests/Tests.lean --- Lampe/Lampe.lean | 458 +---------------------------------------- Lampe/Lampe/Basic.lean | 9 - Lampe/Tests/Tests.lean | 437 +++++++++++++++++++++++++++++++++++++++ 3 files changed, 446 insertions(+), 458 deletions(-) delete mode 100644 Lampe/Lampe/Basic.lean create mode 100644 Lampe/Tests/Tests.lean diff --git a/Lampe/Lampe.lean b/Lampe/Lampe.lean index 85d8233..b74e921 100644 --- a/Lampe/Lampe.lean +++ b/Lampe/Lampe.lean @@ -1,449 +1,9 @@ -import Mathlib -import Lampe.Basic -open Lampe - -nr_def simple_muts<>(x : Field) -> Field { - let mut y = x; - let mut z = x; - z = z; - y = z; - y -} - -example : STHoare p Γ ⟦⟧ (simple_muts.fn.body _ h![] |>.body h![x]) fun v => v = x := by - simp only [simple_muts] - steps - simp_all - -nr_def weirdEq(x : I, y : I) -> Unit { - let a = #fresh() : I; - #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 - simp only [weirdEq] - steps - simp_all - -nr_def sliceAppend(x: [I], y: [I]) -> [I] { - let mut self = x; - for i in (0 : u32) .. #sliceLen(y):u32 { - self = #slicePushBack(self, #sliceIndex(y, i): I): [I] - }; - self -} - -lemma BitVec.add_toNat_of_lt_max {a b : BitVec w} (h: a.toNat + b.toNat < 2^w) : - (a + b).toNat = a.toNat + b.toNat := by - simp only [BitVec.add_def, BitVec.toNat_ofNat] - rw [Nat.mod_eq_of_lt] - assumption - -example {self that : Tp.denote p (.slice tp)} : - STHoare p Γ ⟦⟧ (sliceAppend.fn.body _ h![tp] |>.body h![self, that]) - fun v => v = self ++ that := by - simp only [sliceAppend] - steps - rename Tp.denote _ tp.slice.ref => selfRef - loop_inv (fun i _ _ => [selfRef ↦ ⟨.slice tp, self ++ that.take i.toNat⟩]) - · intros i _ _ - steps - have : (i + 1).toNat = i.toNat + 1 := by - apply BitVec.add_toNat_of_lt_max - casesm* (Tp.denote p (.u 32)), (U _), Fin _ - simp at * - linarith - simp only [this, List.take_succ] - aesop - · simp_all - · simp_all - steps - simp_all [Nat.mod_eq_of_lt] - -nr_def simple_if<>(x : Field, y : Field) -> Field { - let mut z = x; - if #fEq(x, x) : bool { - z = y - }; - z -} - -example {p Γ x y} : STHoare p Γ ⟦⟧ (simple_if.fn.body _ h![] |>.body h![x, y]) - fun v => v = y := by - simp only [simple_if] - steps <;> try tauto - . sl - . sl - simp_all - . subst_vars - rfl - - -nr_def simple_if_else<>(x : Field, y : Field) -> Field { - let z = if #fEq(x, x) : bool { x } else { y }; - z -} - -example {p Γ x y} : STHoare p Γ ⟦⟧ (simple_if_else.fn.body _ h![] |>.body h![x, y]) - fun v => v = x := by - simp only [simple_if_else] - steps - . simp only [decide_true, exists_const] - sl - contradiction - . simp_all [decide_true, exists_const] - -nr_def simple_lambda<>(x : Field, y : Field) -> Field { - let add = |a : Field, b : Field| -> Field { #fAdd(a, b) : Field }; - add(x, y); -} - -example {p Γ} {x y : Tp.denote p Tp.field} : - STHoare p Γ ⟦⟧ (simple_lambda.fn.body _ h![] |>.body h![x, y]) - fun v => v = x + y := by - simp only [simple_lambda] - steps - . apply STHoare.consequence_frame_left STHoare.callLambda_intro - . rw [SLP.star_assoc, SLP.star_comm, SLP.star_assoc] - rw [SLP.top_star_top] - apply SLP.ent_star_top - . exact fun v => v = x + y - . simp only - steps - simp_all only [exists_const, SLP.true_star] - unfold SLP.wand SLP.entails SLP.forall' - intros _ _ _ _ _ _ - simp_all [SLP.star, SLP.lift] - simp_all - steps - simp_all - intros st₁ h₁ v st₂ _ _ - apply SLP.ent_drop_left at h₁ - unfold SLP.lift SLP.star at * - simp_all - -nr_trait_impl[bulbulizeField] <> Bulbulize<> for Field where { - fn bulbulize<>(x : Field) -> Field { - #fAdd(x, x) : Field - }; -} - -nr_trait_impl[bulbulizeU32] <> Bulbulize<> for u32 where { - fn bulbulize<>(_x : u32) -> u32 { - 69 : u32 - } -} - -def simpleTraitEnv : Env := { - functions := [], - traits := [bulbulizeField, bulbulizeU32] -} - -nr_def simple_trait_call (x : I) -> I { - ((I as Bulbulize<>)::bulbulize<> as λ(I) → I)(x) -} - -example {p} {arg : Tp.denote p Tp.field} : - STHoare p simpleTraitEnv ⟦⟧ (simple_trait_call.fn.body _ h![.field] |>.body h![arg]) - fun v => v = 2 * arg := by - simp only [simple_trait_call] - steps - . apply STHoare.callTrait_intro - sl - tauto - try_impls_all [] simpleTraitEnv - all_goals try tauto - simp only - steps - simp_all only [exists_const, SLP.true_star] - on_goal 2 => exact (fun v => v = 2 * arg) - sl - intros - subst_vars - ring - steps - intros - subst_vars - rfl - -nr_trait_impl[me] Me<> for I where { - fn me<>(x : I) -> I { - x - } -} - -def genericTraitEnv : Env := { - functions := [], - traits := [me] -} - -nr_def generic_trait_call<>(x : Field) -> Field { - ((Field as Me<>)::me<> as λ(Field) → Field)(x) -} - -example {p} {x : Tp.denote p Tp.field} : - STHoare p genericTraitEnv ⟦⟧ (generic_trait_call.fn.body _ h![] |>.body h![x]) - fun v => v = x := by - simp only [generic_trait_call] - steps - . apply STHoare.callTrait_intro - sl - tauto - try_impls_all [Tp.field] genericTraitEnv - tauto - all_goals try rfl - steps - . steps - simp_all - -nr_struct_def Pair { - a : I, - b : I -} - -nr_def struct_construct<>(a : Field, b : Field) -> Pair { - Pair { a, b } -} - -example {p} {a b : Tp.denote p .field} : - 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 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 Γ ⟦⟧ (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 p .field) => v = x.toNat := by - simp only [basic_cast] - steps - aesop - -nr_def add_two_fields<>(a : Field, b : Field) -> Field { - #fAdd(a, b) : Field -} - -nr_def call_decl<>() -> Field { - (@add_two_fields<> as λ(Field, Field) → Field)(1 : Field, 2 : Field) -} - -example : STHoare p ⟨[(add_two_fields.name, add_two_fields.fn)], []⟩ ⟦⟧ - (call_decl.fn.body _ h![] |>.body h![]) - fun (v : Tp.denote p .field) => v = 3 := by - simp only [call_decl] - steps - apply STHoare.callDecl_intro - . sl - tauto - on_goal 3 => exact add_two_fields.fn - all_goals try tauto - on_goal 3 => exact fun v => v = 3 - . simp only [add_two_fields] - steps - simp_all - intros - ring - . steps - simp_all - -nr_def simple_tuple<>() -> Field { - let t = `(1 : Field, true, 3 : Field); - t.2 -} - -example : STHoare p Γ ⟦⟧ (simple_tuple.fn.body _ h![] |>.body h![]) - fun (v : Tp.denote p .field) => v = 3 := by - simp only [simple_tuple] - steps - aesop - -nr_def simple_slice<>() -> bool { - let s = &[true, false]; - s[[1 : u32]] -} - -example : STHoare p Γ ⟦⟧ (simple_slice.fn.body _ h![] |>.body h![]) - fun (v : Tp.denote p .bool) => v = false := by - simp only [simple_slice, Expr.mkSlice] - steps - rfl - 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 <;> try tauto - aesop - -nr_def simple_rep_array<>() -> [Field; 4] { - let arr = [1 : Field ; 4]; - arr -} - -example : STHoare p Γ ⟦⟧ (simple_rep_array.fn.body _ h![] |>.body h![]) - fun (v : Tp.denote p $ .array _ _) => v.toList = [1, 1, 1, 1] := by - simp only [simple_rep_array, Expr.mkArray] - steps <;> try tauto - aesop - -nr_def simple_rep_slice<>() -> [Field] { - let arr = &[1 : Field ; 4]; - arr -} - -example : STHoare p Γ ⟦⟧ (simple_rep_slice.fn.body _ h![] |>.body h![]) - fun (v : Tp.denote p $ .slice _) => v = [1, 1, 1, 1] := by - simp only [simple_rep_slice, Expr.mkArray] - steps <;> try tauto - aesop - - -nr_def tuple_lens<>() -> Field { - let mut p = `(`(1 : Field, 2 : Field), 3 : Field); - p .0 .1 = 3 : Field; - p .0 .1 -} - -example : STHoare p Γ ⟦⟧ (tuple_lens.fn.body _ h![] |>.body h![]) - fun (v : Tp.denote p .field) => v = 3 := by - simp only [tuple_lens] - steps - subst_vars - simp_all only [Access.get, exists_const, Lens.modify, Lens.get, Option.bind_eq_bind, - Option.some_bind, Option.bind_some, Option.some.injEq] - subst_vars - rfl - -nr_def struct_lens<>() -> Field { - let mut p = `(Pair{ 1 : Field, 2 : Field}, 3 : Field); - (p .0 as Pair).b = 3 : Field; - (p .0 as Pair).b -} - -example : STHoare p Γ ⟦⟧ (struct_lens.fn.body _ h![] |>.body h![]) - fun (v : Tp.denote p .field) => v = 3 := by - simp only [struct_lens] - steps - aesop - -nr_def array_lens<>() -> Field { - let mut p = `([1 : Field, 2 : Field], 3 : Field); - p.0[1 : u32] = 3 : Field; - p.0[1 : u32] -} - -example : STHoare p Γ ⟦⟧ (array_lens.fn.body _ h![] |>.body h![]) - fun (v : Tp.denote p .field) => v = 3 := by - simp only [array_lens] - steps - rfl - on_goal 3 => exact (⟨[1, 3], (by rfl)⟩, 3) - . simp_all - rfl - . simp_all - aesop - -nr_def slice_lens<>() -> Field { - let mut p = `(&[1 : Field, 2 : Field], 3 : Field); - p .0 [[1 : u32]] = 3 : Field; - p .0 [[1 : u32]] -} - -example : STHoare p Γ ⟦⟧ (slice_lens.fn.body _ h![] |>.body h![]) - fun (v : Tp.denote p .field) => v = 3 := by - simp only [slice_lens] - steps - all_goals try exact ([1, 3], 3) - all_goals try tauto - . simp_all - rfl - . simp_all [Builtin.indexTpl] - -nr_def simple_func<>() -> Field { - 10 : Field -} - -nr_def deref_lens<>() -> Field { - let r = #ref(`(5 : Field)) : &`(Field); - *(r).0 = 3 : Field; - *(r).0 -} - -example : STHoare p Γ ⟦⟧ (deref_lens.fn.body _ h![] |>.body h![]) - fun (v : Tp.denote p .field) => v = 3 := by - simp only [deref_lens] - steps - subst_vars - simp_all only [exists_const, Lens.modify, Lens.get] - subst_vars - simp_all [Builtin.indexTpl] - -nr_def call<>(f : λ() → Field) -> Field { - f() -} - -nr_def simple_hof<>() -> Field { - let func = @simple_func<> as λ() → Field; - (@call<> as λ(λ() → Field) → Field)(func) -} - -example : STHoare p ⟨[(simple_func.name, simple_func.fn), (call.name, call.fn)], []⟩ ⟦⟧ - (simple_hof.fn.body _ h![] |>.body h![]) - fun (v : Tp.denote p .field) => v = 10 := by - simp only [simple_hof] - steps - . apply STHoare.callDecl_intro - sl - all_goals try tauto - simp only [call] - steps - . apply STHoare.callDecl_intro - sl - all_goals try tauto - simp only [simple_func] - steps - on_goal 2 => exact fun v => v = 10 - sl - simp_all - . steps - on_goal 2 => exact fun v => v = 10 - sl - simp_all - steps - simp_all - -nr_def «string_test»<>() -> str<5> { - let x = "Hello"; - x -} - -example : STHoare p Γ ⟦⟧ (string_test.fn.body _ h![] |>.body h![]) - fun v => v = ⟨"Hello".data, rfl⟩ := by - simp only [string_test] - steps - simp_all - +import Lampe.Semantics +import Lampe.Syntax +import Lampe.Ast +import Lampe.Tp +import Lampe.Lens +import Lampe.Hoare.Total +import Lampe.Hoare.SepTotal +import Lampe.Tactic.SeparationLogic +import Lampe.Tactic.Traits diff --git a/Lampe/Lampe/Basic.lean b/Lampe/Lampe/Basic.lean deleted file mode 100644 index b74e921..0000000 --- a/Lampe/Lampe/Basic.lean +++ /dev/null @@ -1,9 +0,0 @@ -import Lampe.Semantics -import Lampe.Syntax -import Lampe.Ast -import Lampe.Tp -import Lampe.Lens -import Lampe.Hoare.Total -import Lampe.Hoare.SepTotal -import Lampe.Tactic.SeparationLogic -import Lampe.Tactic.Traits diff --git a/Lampe/Tests/Tests.lean b/Lampe/Tests/Tests.lean new file mode 100644 index 0000000..323a051 --- /dev/null +++ b/Lampe/Tests/Tests.lean @@ -0,0 +1,437 @@ +import Lampe + +open Lampe + +nr_def simple_muts<>(x : Field) -> Field { + let mut y = x; + let mut z = x; + z = z; + y = z; + y +} + +example : STHoare p Γ ⟦⟧ (simple_muts.fn.body _ h![] |>.body h![x]) fun v => v = x := by + simp only [simple_muts] + steps + simp_all + +nr_def weirdEq(x : I, y : I) -> Unit { + let a = #fresh() : I; + #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 + simp only [weirdEq] + steps + simp_all + +nr_def sliceAppend(x: [I], y: [I]) -> [I] { + let mut self = x; + for i in (0 : u32) .. #sliceLen(y):u32 { + self = #slicePushBack(self, #sliceIndex(y, i): I): [I] + }; + self +} + +lemma BitVec.add_toNat_of_lt_max {a b : BitVec w} (h: a.toNat + b.toNat < 2^w) : + (a + b).toNat = a.toNat + b.toNat := by + simp only [BitVec.add_def, BitVec.toNat_ofNat] + rw [Nat.mod_eq_of_lt] + assumption + +example {self that : Tp.denote p (.slice tp)} : + STHoare p Γ ⟦⟧ (sliceAppend.fn.body _ h![tp] |>.body h![self, that]) + fun v => v = self ++ that := by + simp only [sliceAppend] + steps + rename Tp.denote _ tp.slice.ref => selfRef + loop_inv (fun i _ _ => [selfRef ↦ ⟨.slice tp, self ++ that.take i.toNat⟩]) + · intros i _ _ + steps + have : (i + 1).toNat = i.toNat + 1 := by + apply BitVec.add_toNat_of_lt_max + casesm* (Tp.denote p (.u 32)), (U _), Fin _ + simp at * + linarith + simp only [this, List.take_succ] + aesop + · simp_all + · simp_all + steps + simp_all [Nat.mod_eq_of_lt] + +nr_def simple_if<>(x : Field, y : Field) -> Field { + let mut z = x; + if #fEq(x, x) : bool { + z = y + }; + z +} + +example {p Γ x y} : STHoare p Γ ⟦⟧ (simple_if.fn.body _ h![] |>.body h![x, y]) + fun v => v = y := by + simp only [simple_if] + steps <;> try tauto + . sl + . sl + simp_all + . subst_vars + rfl + + +nr_def simple_if_else<>(x : Field, y : Field) -> Field { + let z = if #fEq(x, x) : bool { x } else { y }; + z +} + +example {p Γ x y} : STHoare p Γ ⟦⟧ (simple_if_else.fn.body _ h![] |>.body h![x, y]) + fun v => v = x := by + simp only [simple_if_else] + steps + . simp only [decide_true, exists_const] + sl + contradiction + . simp_all [decide_true, exists_const] + +nr_def simple_lambda<>(x : Field, y : Field) -> Field { + let add = |a : Field, b : Field| -> Field { #fAdd(a, b) : Field }; + add(x, y); +} + +example {p Γ} {x y : Tp.denote p Tp.field} : + STHoare p Γ ⟦⟧ (simple_lambda.fn.body _ h![] |>.body h![x, y]) + fun v => v = x + y := by + simp only [simple_lambda] + steps + . apply STHoare.consequence_frame_left STHoare.callLambda_intro + . rw [SLP.star_assoc, SLP.star_comm, SLP.star_assoc] + rw [SLP.top_star_top] + apply SLP.ent_star_top + . exact fun v => v = x + y + . simp only + steps + simp_all only [exists_const, SLP.true_star] + unfold SLP.wand SLP.entails SLP.forall' + intros _ _ _ _ _ _ + simp_all [SLP.star, SLP.lift] + simp_all + steps + simp_all + intros st₁ h₁ v st₂ _ _ + apply SLP.ent_drop_left at h₁ + unfold SLP.lift SLP.star at * + simp_all + +nr_trait_impl[bulbulizeField] <> Bulbulize<> for Field where { + fn bulbulize<>(x : Field) -> Field { + #fAdd(x, x) : Field + }; +} + +nr_trait_impl[bulbulizeU32] <> Bulbulize<> for u32 where { + fn bulbulize<>(_x : u32) -> u32 { + 69 : u32 + } +} + +def simpleTraitEnv : Env := { + functions := [], + traits := [bulbulizeField, bulbulizeU32] +} + +nr_def simple_trait_call (x : I) -> I { + ((I as Bulbulize<>)::bulbulize<> as λ(I) → I)(x) +} + +example {p} {arg : Tp.denote p Tp.field} : + STHoare p simpleTraitEnv ⟦⟧ (simple_trait_call.fn.body _ h![.field] |>.body h![arg]) + fun v => v = 2 * arg := by + simp only [simple_trait_call] + steps + . apply STHoare.callTrait_intro + sl + tauto + try_impls_all [] simpleTraitEnv + all_goals try tauto + simp only + steps + simp_all only [exists_const, SLP.true_star] + on_goal 2 => exact (fun v => v = 2 * arg) + sl + intros + subst_vars + ring + steps + intros + subst_vars + rfl + +nr_trait_impl[me] Me<> for I where { + fn me<>(x : I) -> I { + x + } +} + +def genericTraitEnv : Env := { + functions := [], + traits := [me] +} + +nr_def generic_trait_call<>(x : Field) -> Field { + ((Field as Me<>)::me<> as λ(Field) → Field)(x) +} + +example {p} {x : Tp.denote p Tp.field} : + STHoare p genericTraitEnv ⟦⟧ (generic_trait_call.fn.body _ h![] |>.body h![x]) + fun v => v = x := by + simp only [generic_trait_call] + steps + . apply STHoare.callTrait_intro + sl + tauto + try_impls_all [Tp.field] genericTraitEnv + tauto + all_goals try rfl + steps + . steps + simp_all + +nr_struct_def Pair { + a : I, + b : I +} + +nr_def struct_construct<>(a : Field, b : Field) -> Pair { + Pair { a, b } +} + +example {p} {a b : Tp.denote p .field} : + 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 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 Γ ⟦⟧ (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 p .field) => v = x.toNat := by + simp only [basic_cast] + steps + aesop + +nr_def add_two_fields<>(a : Field, b : Field) -> Field { + #fAdd(a, b) : Field +} + +nr_def call_decl<>() -> Field { + (@add_two_fields<> as λ(Field, Field) → Field)(1 : Field, 2 : Field) +} + +example : STHoare p ⟨[(add_two_fields.name, add_two_fields.fn)], []⟩ ⟦⟧ + (call_decl.fn.body _ h![] |>.body h![]) + fun (v : Tp.denote p .field) => v = 3 := by + simp only [call_decl] + steps + apply STHoare.callDecl_intro + . sl + tauto + on_goal 3 => exact add_two_fields.fn + all_goals try tauto + on_goal 3 => exact fun v => v = 3 + . simp only [add_two_fields] + steps + simp_all + intros + ring + . steps + simp_all + +nr_def simple_tuple<>() -> Field { + let t = `(1 : Field, true, 3 : Field); + t.2 +} + +example : STHoare p Γ ⟦⟧ (simple_tuple.fn.body _ h![] |>.body h![]) + fun (v : Tp.denote p .field) => v = 3 := by + simp only [simple_tuple] + steps + aesop + +nr_def simple_slice<>() -> bool { + let s = &[true, false]; + s[[1 : u32]] +} + +example : STHoare p Γ ⟦⟧ (simple_slice.fn.body _ h![] |>.body h![]) + fun (v : Tp.denote p .bool) => v = false := by + simp only [simple_slice, Expr.mkSlice] + steps + rfl + 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 <;> try tauto + aesop + +nr_def simple_rep_array<>() -> [Field; 4] { + let arr = [1 : Field ; 4]; + arr +} + +example : STHoare p Γ ⟦⟧ (simple_rep_array.fn.body _ h![] |>.body h![]) + fun (v : Tp.denote p $ .array _ _) => v.toList = [1, 1, 1, 1] := by + simp only [simple_rep_array, Expr.mkArray] + steps <;> try tauto + aesop + +nr_def simple_rep_slice<>() -> [Field] { + let arr = &[1 : Field ; 4]; + arr +} + +example : STHoare p Γ ⟦⟧ (simple_rep_slice.fn.body _ h![] |>.body h![]) + fun (v : Tp.denote p $ .slice _) => v = [1, 1, 1, 1] := by + simp only [simple_rep_slice, Expr.mkArray] + steps <;> try tauto + aesop + + +nr_def tuple_lens<>() -> Field { + let mut p = `(`(1 : Field, 2 : Field), 3 : Field); + p .0 .1 = 3 : Field; + p .0 .1 +} + +example : STHoare p Γ ⟦⟧ (tuple_lens.fn.body _ h![] |>.body h![]) + fun (v : Tp.denote p .field) => v = 3 := by + simp only [tuple_lens] + steps + subst_vars + simp_all only [Access.get, exists_const, Lens.modify, Lens.get, Option.bind_eq_bind, + Option.some_bind, Option.bind_some, Option.some.injEq] + subst_vars + rfl + +nr_def struct_lens<>() -> Field { + let mut p = `(Pair{ 1 : Field, 2 : Field}, 3 : Field); + (p .0 as Pair).b = 3 : Field; + (p .0 as Pair).b +} + +example : STHoare p Γ ⟦⟧ (struct_lens.fn.body _ h![] |>.body h![]) + fun (v : Tp.denote p .field) => v = 3 := by + simp only [struct_lens] + steps + aesop + +nr_def array_lens<>() -> Field { + let mut p = `([1 : Field, 2 : Field], 3 : Field); + p.0[1 : u32] = 3 : Field; + p.0[1 : u32] +} + +example : STHoare p Γ ⟦⟧ (array_lens.fn.body _ h![] |>.body h![]) + fun (v : Tp.denote p .field) => v = 3 := by + simp only [array_lens] + steps + rfl + on_goal 3 => exact (⟨[1, 3], (by rfl)⟩, 3) + . simp_all + rfl + . simp_all + aesop + +nr_def slice_lens<>() -> Field { + let mut p = `(&[1 : Field, 2 : Field], 3 : Field); + p .0 [[1 : u32]] = 3 : Field; + p .0 [[1 : u32]] +} + +example : STHoare p Γ ⟦⟧ (slice_lens.fn.body _ h![] |>.body h![]) + fun (v : Tp.denote p .field) => v = 3 := by + simp only [slice_lens] + steps + all_goals try exact ([1, 3], 3) + all_goals try tauto + . simp_all + rfl + . simp_all [Builtin.indexTpl] + +nr_def simple_func<>() -> Field { + 10 : Field +} + +nr_def deref_lens<>() -> Field { + let r = #ref(`(5 : Field)) : &`(Field); + *(r).0 = 3 : Field; + *(r).0 +} + +example : STHoare p Γ ⟦⟧ (deref_lens.fn.body _ h![] |>.body h![]) + fun (v : Tp.denote p .field) => v = 3 := by + simp only [deref_lens] + steps + subst_vars + simp_all only [exists_const, Lens.modify, Lens.get] + subst_vars + simp_all [Builtin.indexTpl] + +nr_def call<>(f : λ() → Field) -> Field { + f() +} + +nr_def simple_hof<>() -> Field { + let func = @simple_func<> as λ() → Field; + (@call<> as λ(λ() → Field) → Field)(func) +} + +example : STHoare p ⟨[(simple_func.name, simple_func.fn), (call.name, call.fn)], []⟩ ⟦⟧ + (simple_hof.fn.body _ h![] |>.body h![]) + fun (v : Tp.denote p .field) => v = 10 := by + simp only [simple_hof] + steps + . apply STHoare.callDecl_intro + sl + all_goals try tauto + simp only [call] + steps + . apply STHoare.callDecl_intro + sl + all_goals try tauto + simp only [simple_func] + steps + on_goal 2 => exact fun v => v = 10 + sl + simp_all + . steps + on_goal 2 => exact fun v => v = 10 + sl + simp_all + steps + simp_all From 1229175d29f93f0149d93b7b9a4d7a1e8fc3722d Mon Sep 17 00:00:00 2001 From: Matej Penciak Date: Thu, 16 Jan 2025 17:38:30 -0500 Subject: [PATCH 2/3] Update lakefile * Add `Tests` lib and test driver * Remove quotes from package and library names * Clean up auto-generated comments --- Lampe/lakefile.lean | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/Lampe/lakefile.lean b/Lampe/lakefile.lean index 13eba5e..5b764a5 100644 --- a/Lampe/lakefile.lean +++ b/Lampe/lakefile.lean @@ -1,15 +1,16 @@ import Lake open Lake DSL -package «Lampe» where - -- Settings applied to both builds and interactive editing +package Lampe where leanOptions := #[ - ⟨`pp.unicode.fun, true⟩ -- pretty-prints `fun a ↦ b` + ⟨`pp.unicode.fun, true⟩ ] - -- add any additional package configuration options here + testDriver := "Tests" require "leanprover-community" / "mathlib" @ git "v4.15.0-patch1" @[default_target] -lean_lib «Lampe» where - -- add any library configuration options here +lean_lib Lampe where + +lean_lib Tests where + globs := #[.submodules `Tests] From 65874dc789101ee9711fe52f4f24f6faff88f195 Mon Sep 17 00:00:00 2001 From: Matej Penciak Date: Thu, 16 Jan 2025 17:38:39 -0500 Subject: [PATCH 3/3] Update CI --- .github/workflows/ci.yaml | 6 ++++++ Lampe/Lampe.lean | 33 ++++++++++++++++++++++++++++----- 2 files changed, 34 insertions(+), 5 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 3edbe94..2fa342c 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -18,9 +18,15 @@ jobs: lint: false use-mathlib-cache: true lake-package-directory: Lampe + - name: mk_all (lake) + working-directory: Lampe + run: lake exe mk_all --check --lib Lampe - name: Build (lake) working-directory: Lampe run: lake build + - name: Test (lake) + working-directory: Lampe + run: lake test build-cargo: runs-on: ubuntu-latest steps: diff --git a/Lampe/Lampe.lean b/Lampe/Lampe.lean index b74e921..a662bc5 100644 --- a/Lampe/Lampe.lean +++ b/Lampe/Lampe.lean @@ -1,9 +1,32 @@ -import Lampe.Semantics -import Lampe.Syntax import Lampe.Ast -import Lampe.Tp -import Lampe.Lens -import Lampe.Hoare.Total +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 +import Lampe.Builtin.Field +import Lampe.Builtin.Helpers +import Lampe.Builtin.Lens +import Lampe.Builtin.Memory +import Lampe.Builtin.Slice +import Lampe.Builtin.Str +import Lampe.Builtin.Struct +import Lampe.Data.Field +import Lampe.Data.HList +import Lampe.Data.Integers +import Lampe.Hoare.Builtins import Lampe.Hoare.SepTotal +import Lampe.Hoare.Total +import Lampe.Lens +import Lampe.Semantics +import Lampe.SeparationLogic.LawfulHeap +import Lampe.SeparationLogic.SLP +import Lampe.SeparationLogic.State +import Lampe.SeparationLogic.ValHeap +import Lampe.Syntax +import Lampe.Tactic.IntroCases import Lampe.Tactic.SeparationLogic import Lampe.Tactic.Traits +import Lampe.Tp