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 <sonho@Sons-MacBook-Pro.local>
Co-authored-by: Son Ho <sonho@Sons-MBP.lan>---
 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

