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 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backends/lean/Base/Primitives/ArraySlice.lean') 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] -- cgit v1.2.3