From 4d30546c809cb2c512e0c3fd8ee540fff1330eab Mon Sep 17 00:00:00 2001 From: Son HO Date: Fri, 21 Jun 2024 23:24:01 +0200 Subject: Add some proofs for the Lean backend (#255) * Make progress on the proofs of the hashmap * Make a minor modification to the hashmap * Make progress on the hashmap * Make progress on the proofs * Make progress on the proofs * Make progress on the proof of the hashmap * Progress on the proofs of the hashmap * Update a proof * Update the Charon pin * Make minor modifications to the hashmap * Regenerate the tests * Regenerate the hashmap * Add lemmas to the Lean backend * Make progress on the proofs of the hashmap * Make a minor fix * Finish the proof about the hashmap * Update scalar_tac * Make a minor modification in the hashmap * Update the proofs of the hashmap --------- Co-authored-by: Son Ho Co-authored-by: Son Ho --- backends/lean/Base/Primitives/ArraySlice.lean | 2 +- backends/lean/Base/Primitives/Scalar.lean | 11 ++++++----- backends/lean/Base/Primitives/Vec.lean | 13 +++++++++++-- 3 files changed, 18 insertions(+), 8 deletions(-) (limited to 'backends/lean/Base/Primitives') diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean index be460987..899871af 100644 --- a/backends/lean/Base/Primitives/ArraySlice.lean +++ b/backends/lean/Base/Primitives/ArraySlice.lean @@ -129,7 +129,7 @@ example {a: Type u} (v : Slice a) : v.length ≤ Scalar.max ScalarTy.Usize := by def Slice.new (α : Type u): Slice α := ⟨ [], by apply Scalar.cMax_suffices .Usize; simp ⟩ -- TODO: very annoying that the α is an explicit parameter -def Slice.len (α : Type u) (v : Slice α) : Usize := +abbrev Slice.len (α : Type u) (v : Slice α) : Usize := Usize.ofIntCore v.val.len (by constructor <;> scalar_tac) @[simp] diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean index 9f809ead..31038e0d 100644 --- a/backends/lean/Base/Primitives/Scalar.lean +++ b/backends/lean/Base/Primitives/Scalar.lean @@ -1301,22 +1301,25 @@ instance {ty} : LT (Scalar ty) where instance {ty} : LE (Scalar ty) where le a b := LE.le a.val b.val --- Not marking this one with @[simp] on purpose +-- Not marking this one with @[simp] on purpose: if we have `x = y` somewhere in the context, +-- we may want to use it to substitute `y` with `x` somewhere. +-- TODO: mark it as simp anyway? theorem Scalar.eq_equiv {ty : ScalarTy} (x y : Scalar ty) : x = y ↔ (↑x : Int) = ↑y := by cases x; cases y; simp_all -- This is sometimes useful when rewriting the goal with the local assumptions +-- TODO: this doesn't get triggered @[simp] theorem Scalar.eq_imp {ty : ScalarTy} (x y : Scalar ty) : (↑x : Int) = ↑y → x = y := (eq_equiv x y).mpr -theorem Scalar.lt_equiv {ty : ScalarTy} (x y : Scalar ty) : +@[simp] theorem Scalar.lt_equiv {ty : ScalarTy} (x y : Scalar ty) : x < y ↔ (↑x : Int) < ↑y := by simp [LT.lt] @[simp] theorem Scalar.lt_imp {ty : ScalarTy} (x y : Scalar ty) : (↑x : Int) < (↑y) → x < y := (lt_equiv x y).mpr -theorem Scalar.le_equiv {ty : ScalarTy} (x y : Scalar ty) : +@[simp] theorem Scalar.le_equiv {ty : ScalarTy} (x y : Scalar ty) : x ≤ y ↔ (↑x : Int) ≤ ↑y := by simp [LE.le] @[simp] theorem Scalar.le_imp {ty : ScalarTy} (x y : Scalar ty) : @@ -1377,8 +1380,6 @@ theorem coe_max {ty: ScalarTy} (a b: Scalar ty): ↑(Max.max a b) = (Max.max ( -- TODO: there should be a shorter way to prove this. rw [max_def, max_def] split_ifs <;> simp_all - refine' absurd _ (lt_irrefl a) - exact lt_of_le_of_lt (by assumption) ((Scalar.lt_equiv _ _).2 (by assumption)) -- Max theory -- TODO: do the min theory later on. diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean index 0b010944..e584777a 100644 --- a/backends/lean/Base/Primitives/Vec.lean +++ b/backends/lean/Base/Primitives/Vec.lean @@ -33,14 +33,15 @@ abbrev Vec.v {α : Type u} (v : Vec α) : List α := v.val example {a: Type u} (v : Vec a) : v.length ≤ Scalar.max ScalarTy.Usize := by scalar_tac -def Vec.new (α : Type u): Vec α := ⟨ [], by apply Scalar.cMax_suffices .Usize; simp ⟩ +abbrev Vec.new (α : Type u): Vec α := ⟨ [], by apply Scalar.cMax_suffices .Usize; simp ⟩ instance (α : Type u) : Inhabited (Vec α) := by constructor apply Vec.new -- TODO: very annoying that the α is an explicit parameter -def Vec.len (α : Type u) (v : Vec α) : Usize := +@[simp] +abbrev Vec.len (α : Type u) (v : Vec α) : Usize := Usize.ofIntCore v.val.len (by constructor <;> scalar_tac) @[simp] @@ -63,6 +64,14 @@ def Vec.push (α : Type u) (v : Vec α) (x : α) : Result (Vec α) else fail maximumSizeExceeded +@[pspec] +theorem Vec.push_spec {α : Type u} (v : Vec α) (x : α) (h : v.val.len < Usize.max) : + ∃ v1, v.push α x = ok v1 ∧ + v1.val = v.val ++ [x] := by + simp [push] + split <;> simp_all [List.len_eq_length] + scalar_tac + -- This shouldn't be used def Vec.insert_fwd (α : Type u) (v: Vec α) (i: Usize) (_: α) : Result Unit := if i.val < v.length then -- cgit v1.2.3