Merge pull request #124 from AeneasVerif/son/lean1

Add more definitions to the Lean library

7 files changed, 420 insertions, 5 deletions

diff --git a/backends/lean/Base/Primitives.lean b/backends/lean/Base/Primitives.lean
index 7196d2ec..f80c2004 100644
--- a/backends/lean/Base/Primitives.lean
+++ b/backends/lean/Base/Primitives.lean
@@ -4,4 +4,5 @@ import Base.Primitives.Scalar
 import Base.Primitives.ArraySlice
 import Base.Primitives.Vec
 import Base.Primitives.Alloc
-import Base.Primitives.CoreOps
+import Base.Primitives.Core
+import Base.Primitives.CoreConvertNum
diff --git a/backends/lean/Base/Primitives/Alloc.lean b/backends/lean/Base/Primitives/Alloc.lean
index 15fe1ff9..1b15d36d 100644
--- a/backends/lean/Base/Primitives/Alloc.lean
+++ b/backends/lean/Base/Primitives/Alloc.lean
@@ -1,6 +1,6 @@
 import Lean
 import Base.Primitives.Base
-import Base.Primitives.CoreOps
+import Base.Primitives.Core
 
 open Primitives
 open Result
diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean
index 91ca7284..157f9df1 100644
--- a/backends/lean/Base/Primitives/ArraySlice.lean
+++ b/backends/lean/Base/Primitives/ArraySlice.lean
@@ -6,7 +6,7 @@ import Mathlib.Tactic.Linarith
 import Base.IList
 import Base.Primitives.Scalar
 import Base.Primitives.Range
-import Base.Primitives.CoreOps
+import Base.Primitives.Core
 import Base.Arith
 import Base.Progress.Base
 
diff --git a/backends/lean/Base/Primitives/CoreOps.lean b/backends/lean/Base/Primitives/Core.lean
index 1736bfa6..99f65985 100644
--- a/backends/lean/Base/Primitives/CoreOps.lean
+++ b/backends/lean/Base/Primitives/Core.lean
@@ -4,7 +4,13 @@ import Base.Primitives.Base
 open Primitives
 open Result
 
-namespace core.ops
+namespace core
+
+/- Trait declaration: [core::convert::From] -/
+structure convert.From (Self T : Type) where
+  from_ : T → Result Self
+
+namespace ops -- core.ops
 
 namespace index -- core.ops.index
 
@@ -32,4 +38,17 @@ structure DerefMut (Self : Type) where
 
 end deref -- core.ops.deref
 
-end core.ops
+end ops -- core.ops
+
+/- Trait declaration: [core::clone::Clone] -/
+structure clone.Clone (Self : Type) where
+  clone : Self → Result Self
+
+/- [core::clone::impls::{(core::clone::Clone for bool)#19}::clone] -/
+def clone.impls.CloneBool.clone (b : Bool) : Bool := b
+
+def clone.CloneBool : clone.Clone Bool := {
+  clone := fun b => ok (clone.impls.CloneBool.clone b)
+}
+
+end core
diff --git a/backends/lean/Base/Primitives/CoreConvertNum.lean b/backends/lean/Base/Primitives/CoreConvertNum.lean
new file mode 100644
index 00000000..eb456a96
--- /dev/null
+++ b/backends/lean/Base/Primitives/CoreConvertNum.lean
@@ -0,0 +1,277 @@
+import Lean
+import Lean.Meta.Tactic.Simp
+import Init.Data.List.Basic
+import Mathlib.Tactic.Linarith
+import Base.IList
+import Base.Primitives.Scalar
+import Base.Primitives.ArraySlice
+import Base.Arith
+import Base.Progress.Base
+
+namespace Primitives
+
+open Result Error
+
+namespace core.convert
+
+namespace num -- core.convert.num
+
+-- Conversions
+def FromUsizeBool.from (b : Bool) : Usize :=
+  if b then 1#usize else 0#usize
+
+def FromU8Bool.from (b : Bool) : U8 :=
+  if b then 1#u8 else 0#u8
+
+def FromU16Bool.from (b : Bool) : U16 :=
+  if b then 1#u16 else 0#u16
+
+def FromU32Bool.from (b : Bool) : U32 :=
+  if b then 1#u32 else 0#u32
+
+def FromU64Bool.from (b : Bool) : U64 :=
+  if b then 1#u64 else 0#u64
+
+def FromU128Bool.from (b : Bool) : U128 :=
+  if b then 1#u128 else 0#u128
+
+def FromIsizeBool.from (b : Bool) : Isize :=
+  if b then 1#isize else 0#isize
+
+def FromI8Bool.from (b : Bool) : I8 :=
+  if b then 1#i8 else 0#i8
+
+def FromI16Bool.from (b : Bool) : I16 :=
+  if b then 1#i16 else 0#i16
+
+def FromI32Bool.from (b : Bool) : I32 :=
+  if b then 1#i32 else 0#i32
+
+def FromI64Bool.from (b : Bool) : I64 :=
+  if b then 1#i64 else 0#i64
+
+def FromI128Bool.from (b : Bool) : I128 :=
+  if b then 1#i128 else 0#i128
+
+def FromUsizeU8.from (x : U8) : Usize := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+
+def FromUsizeU16.from (x : U16) : Usize := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromUsizeU32.from (x : U32) : Usize := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromUsizeUsize.from (x : Usize) : Usize := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+
+def FromU8U8.from (x : U8) : U8 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+
+def FromU16U8.from (x : U8) : U16 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromU16U16.from (x : U16) : U16 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+
+def FromU32U8.from (x : U8) : U32 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromU32U16.from (x : U16) : U32 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromU32U32.from (x : U32) : U32 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+
+def FromU64U8.from (x : U8) : U64 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromU64U16.from (x : U16) : U64 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromU64U32.from (x : U32) : U64 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromU64U64.from (x : U64) : U64 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+
+def FromU128U8.from (x : U8) : U128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromU128U16.from (x : U16) : U128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromU128U32.from (x : U32) : U128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromU128U64.from (x : U64) : U128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromU128U128.from (x : U128) : U128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+
+def FromIsizeI8.from (x : I8) : Isize := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromIsizeI16.from (x : I16) : Isize := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromIsizeI32.from (x : I32) : Isize := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromIsizeIsize.from (x : Isize) : Isize := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+
+def FromI8I8.from (x : I8) : I8 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+
+def FromI16I8.from (x : I8) : I16 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromI16I16.from (x : I16) : I16 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+
+def FromI32I8.from (x : I8) : I32 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromI32I16.from (x : I16) : I32 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromI32I32.from (x : I32) : I32 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+
+def FromI64I8.from (x : I8) : I64 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromI64I16.from (x : I16) : I64 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromI64I32.from (x : I32) : I64 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromI64I64.from (x : I64) : I64 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+
+def FromI128I8.from (x : I8) : I128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromI128I16.from (x : I16) : I128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromI128I32.from (x : I32) : I128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromI128I64.from (x : I64) : I128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+def FromI128I128.from (x : I128) : I128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
+
+end num -- core.convert.num
+
+def FromUsizeU8 : core.convert.From Usize U8 := {
+  from_ := fun x => ok (num.FromUsizeU8.from x)
+}
+
+def FromUsizeU16 : core.convert.From Usize U16 := {
+  from_ := fun x => ok (num.FromUsizeU16.from x)
+}
+
+def FromUsizeU32 : core.convert.From Usize U32 := {
+  from_ := fun x => ok (num.FromUsizeU32.from x)
+}
+
+def FromUsizeUsize : core.convert.From Usize Usize := {
+  from_ := fun x => ok (num.FromUsizeUsize.from x)
+}
+
+def FromU8U8 : core.convert.From U8 U8 := {
+  from_ := fun x => ok (num.FromU8U8.from x)
+}
+
+def FromU16U8 : core.convert.From U16 U8 := {
+  from_ := fun x => ok (num.FromU16U8.from x)
+}
+
+def FromU16U16 : core.convert.From U16 U16 := {
+  from_ := fun x => ok (num.FromU16U16.from x)
+}
+
+def FromU32U8 : core.convert.From U32 U8 := {
+  from_ := fun x => ok (num.FromU32U8.from x)
+}
+
+def FromU32U16 : core.convert.From U32 U16 := {
+  from_ := fun x => ok (num.FromU32U16.from x)
+}
+
+def FromU32U32 : core.convert.From U32 U32 := {
+  from_ := fun x => ok (num.FromU32U32.from x)
+}
+
+def FromU64U8 : core.convert.From U64 U8 := {
+  from_ := fun x => ok (num.FromU64U8.from x)
+}
+
+def FromU64U16 : core.convert.From U64 U16 := {
+  from_ := fun x => ok (num.FromU64U16.from x)
+}
+
+def FromU64U32 : core.convert.From U64 U32 := {
+  from_ := fun x => ok (num.FromU64U32.from x)
+}
+
+def FromU64U64 : core.convert.From U64 U64 := {
+  from_ := fun x => ok (num.FromU64U64.from x)
+}
+
+def FromU128U8 : core.convert.From U128 U8 := {
+  from_ := fun x => ok (num.FromU128U8.from x)
+}
+
+def FromU128U16 : core.convert.From U128 U16 := {
+  from_ := fun x => ok (num.FromU128U16.from x)
+}
+
+def FromU128U32 : core.convert.From U128 U32 := {
+  from_ := fun x => ok (num.FromU128U32.from x)
+}
+
+def FromU128U64 : core.convert.From U128 U64 := {
+  from_ := fun x => ok (num.FromU128U64.from x)
+}
+
+def FromU128U128 : core.convert.From U128 U128 := {
+  from_ := fun x => ok (num.FromU128U128.from x)
+}
+
+def FromIsizeI8 : core.convert.From Isize I8 := {
+  from_ := fun x => ok (num.FromIsizeI8.from x)
+}
+
+def FromIsizeI16 : core.convert.From Isize I16 := {
+  from_ := fun x => ok (num.FromIsizeI16.from x)
+}
+
+def FromIsizeI32 : core.convert.From Isize I32 := {
+  from_ := fun x => ok (num.FromIsizeI32.from x)
+}
+
+def FromIsizeIsize : core.convert.From Isize Isize := {
+  from_ := fun x => ok (num.FromIsizeIsize.from x)
+}
+
+def FromI8I8 : core.convert.From I8 I8 := {
+  from_ := fun x => ok (num.FromI8I8.from x)
+}
+
+def FromI16I8 : core.convert.From I16 I8 := {
+  from_ := fun x => ok (num.FromI16I8.from x)
+}
+
+def FromI16I16 : core.convert.From I16 I16 := {
+  from_ := fun x => ok (num.FromI16I16.from x)
+}
+
+def FromI32I8 : core.convert.From I32 I8 := {
+  from_ := fun x => ok (num.FromI32I8.from x)
+}
+
+def FromI32I16 : core.convert.From I32 I16 := {
+  from_ := fun x => ok (num.FromI32I16.from x)
+}
+
+def FromI32I32 : core.convert.From I32 I32 := {
+  from_ := fun x => ok (num.FromI32I32.from x)
+}
+
+def FromI64I8 : core.convert.From I64 I8 := {
+  from_ := fun x => ok (num.FromI64I8.from x)
+}
+
+def FromI64I16 : core.convert.From I64 I16 := {
+  from_ := fun x => ok (num.FromI64I16.from x)
+}
+
+def FromI64I32 : core.convert.From I64 I32 := {
+  from_ := fun x => ok (num.FromI64I32.from x)
+}
+
+def FromI64I64 : core.convert.From I64 I64 := {
+  from_ := fun x => ok (num.FromI64I64.from x)
+}
+
+def FromI128I8 : core.convert.From I128 I8 := {
+  from_ := fun x => ok (num.FromI128I8.from x)
+}
+
+def FromI128I16 : core.convert.From I128 I16 := {
+  from_ := fun x => ok (num.FromI128I16.from x)
+}
+
+def FromI128I32 : core.convert.From I128 I32 := {
+  from_ := fun x => ok (num.FromI128I32.from x)
+}
+
+def FromI128I64 : core.convert.From I128 I64 := {
+  from_ := fun x => ok (num.FromI128I64.from x)
+}
+
+def FromI128I128 : core.convert.From I128 I128 := {
+  from_ := fun x => ok (num.FromI128I128.from x)
+}
+
+-- to_le_bytes
+def core.num.U8.to_le_bytes (x : U8) : Array U8 1#usize := sorry
+def core.num.U16.to_le_bytes (x : U16) : Array U8 2#usize := sorry
+def core.num.U32.to_le_bytes (x : U32) : Array U8 4#usize := sorry
+def core.num.U64.to_le_bytes (x : U64) : Array U8 8#usize := sorry
+def core.num.U128.to_le_bytes (x : U128) : Array U8 128#usize := sorry
+
+-- to_be_bytes
+def core.num.U8.to_be_bytes (x : U8) : Array U8 1#usize := sorry
+def core.num.U16.to_be_bytes (x : U16) : Array U8 2#usize := sorry
+def core.num.U32.to_be_bytes (x : U32) : Array U8 4#usize := sorry
+def core.num.U64.to_be_bytes (x : U64) : Array U8 8#usize := sorry
+def core.num.U128.to_be_bytes (x : U128) : Array U8 128#usize := sorry
+
+end core.convert
+
+end Primitives
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index 8de2b3f2..b8d93d30 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -2,6 +2,7 @@ import Lean
 import Lean.Meta.Tactic.Simp
 import Mathlib.Tactic.Linarith
 import Base.Primitives.Base
+import Base.Primitives.Core
 import Base.Diverge.Base
 import Base.Progress.Base
 import Base.Arith.Int
@@ -1393,4 +1394,82 @@ instance (ty : ScalarTy) : DecidableEq (Scalar ty) :=
 @[simp] theorem Scalar.neq_to_neq_val {ty} : ∀ {i j : Scalar ty}, (¬ i = j) ↔ ¬ i.val = j.val := by
   simp [eq_equiv]
 
+-- Leading zeros
+def core.num.Usize.leading_zeros (x : Usize) : U32 := sorry
+def core.num.U8.leading_zeros (x : U8) : U32 := sorry
+def core.num.U16.leading_zeros (x : U16) : U32 := sorry
+def core.num.U32.leading_zeros (x : U32) : U32 := sorry
+def core.num.U64.leading_zeros (x : U64) : U32 := sorry
+def core.num.U128.leading_zeros (x : U128) : U32 := sorry
+
+def core.num.Isize.leading_zeros (x : Isize) : U32 := sorry
+def core.num.I8.leading_zeros (x : I8) : U32 := sorry
+def core.num.I16.leading_zeros (x : I16) : U32 := sorry
+def core.num.I32.leading_zeros (x : I32) : U32 := sorry
+def core.num.I64.leading_zeros (x : I64) : U32 := sorry
+def core.num.I128.leading_zeros (x : I128) : U32 := sorry
+
+-- Clone
+def core.clone.impls.CloneUsize.clone (x : Usize) : Usize := x
+def core.clone.impls.CloneU8.clone (x : U8) : U8 := x
+def core.clone.impls.CloneU16.clone (x : U16) : U16 := x
+def core.clone.impls.CloneU32.clone (x : U32) : U32 := x
+def core.clone.impls.CloneU64.clone (x : U64) : U64 := x
+def core.clone.impls.CloneU128.clone (x : U128) : U128 := x
+
+def core.clone.impls.CloneIsize.clone (x : Isize) : Isize := x
+def core.clone.impls.CloneI8.clone (x : I8) : I8 := x
+def core.clone.impls.CloneI16.clone (x : I16) : I16 := x
+def core.clone.impls.CloneI32.clone (x : I32) : I32 := x
+def core.clone.impls.CloneI64.clone (x : I64) : I64 := x
+def core.clone.impls.CloneI128.clone (x : I128) : I128 := x
+
+def core.clone.CloneUsize : core.clone.Clone Usize := {
+  clone := fun x => ok (core.clone.impls.CloneUsize.clone x)
+}
+
+def core.clone.CloneU8 : core.clone.Clone U8 := {
+  clone := fun x => ok (core.clone.impls.CloneU8.clone x)
+}
+
+def core.clone.CloneU16 : core.clone.Clone U16 := {
+  clone := fun x => ok (core.clone.impls.CloneU16.clone x)
+}
+
+def core.clone.CloneU32 : core.clone.Clone U32 := {
+  clone := fun x => ok (core.clone.impls.CloneU32.clone x)
+}
+
+def core.clone.CloneU64 : core.clone.Clone U64 := {
+  clone := fun x => ok (core.clone.impls.CloneU64.clone x)
+}
+
+def core.clone.CloneU128 : core.clone.Clone U128 := {
+  clone := fun x => ok (core.clone.impls.CloneU128.clone x)
+}
+
+def core.clone.CloneIsize : core.clone.Clone Isize := {
+  clone := fun x => ok (core.clone.impls.CloneIsize.clone x)
+}
+
+def core.clone.CloneI8 : core.clone.Clone I8 := {
+  clone := fun x => ok (core.clone.impls.CloneI8.clone x)
+}
+
+def core.clone.CloneI16 : core.clone.Clone I16 := {
+  clone := fun x => ok (core.clone.impls.CloneI16.clone x)
+}
+
+def core.clone.CloneI32 : core.clone.Clone I32 := {
+  clone := fun x => ok (core.clone.impls.CloneI32.clone x)
+}
+
+def core.clone.CloneI64 : core.clone.Clone I64 := {
+  clone := fun x => ok (core.clone.impls.CloneI64.clone x)
+}
+
+def core.clone.CloneI128 : core.clone.Clone I128 := {
+  clone := fun x => ok (core.clone.impls.CloneI128.clone x)
+}
+
 end Primitives
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index 8e2d65a8..5ed7b606 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -182,4 +182,43 @@ theorem Vec.index_mut_slice_index {α : Type} (v : Vec α) (i : Usize) :
 
 end alloc.vec
 
+/-- [alloc::slice::{@Slice<T>}::to_vec] -/
+def alloc.slice.Slice.to_vec
+  (T : Type) (cloneInst : core.clone.Clone T) (s : Slice T) : Result (alloc.vec.Vec T) :=
+  -- TODO: we need a monadic map
+  sorry
+
+/-- [core::slice::{@Slice<T>}::reverse] -/
+def core.slice.Slice.reverse (T : Type) (s : Slice T) : Slice T :=
+  ⟨ s.val.reverse, by sorry ⟩
+
+def alloc.vec.Vec.with_capacity (T : Type) (s : Usize) : alloc.vec.Vec T := Vec.new T
+
+/- [alloc::vec::{(core::ops::deref::Deref for alloc::vec::Vec<T, A>)#9}::deref]:
+   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/alloc/src/vec/mod.rs', lines 2624:4-2624:27
+   Name pattern: alloc::vec::{core::ops::deref::Deref<alloc::vec::Vec<@T, @A>>}::deref -/
+def alloc.vec.DerefVec.deref (T : Type) (v : Vec T) : Slice T :=
+  ⟨ v.val, v.property ⟩
+
+def core.ops.deref.DerefVec (T : Type) : core.ops.deref.Deref (alloc.vec.Vec T) := {
+  Target := Slice T
+  deref := fun v => ok (alloc.vec.DerefVec.deref T v)
+}
+
+/- [alloc::vec::{(core::ops::deref::DerefMut for alloc::vec::Vec<T, A>)#10}::deref_mut]:
+   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/alloc/src/vec/mod.rs', lines 2632:4-2632:39
+   Name pattern: alloc::vec::{core::ops::deref::DerefMut<alloc::vec::Vec<@T, @A>>}::deref_mut -/
+def alloc.vec.DerefMutVec.deref_mut (T : Type) (v :  alloc.vec.Vec T) :
+   Result ((Slice T) × (Slice T → Result (alloc.vec.Vec T))) :=
+   ok (⟨ v.val, v.property ⟩, λ s => ok ⟨ s.val, s.property ⟩)
+
+/- Trait implementation: [alloc::vec::{(core::ops::deref::DerefMut for alloc::vec::Vec<T, A>)#10}]
+   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/alloc/src/vec/mod.rs', lines 2630:0-2630:49
+   Name pattern: core::ops::deref::DerefMut<alloc::vec::Vec<@Self, @>> -/
+def core.ops.deref.DerefMutVec (T : Type) :
+  core.ops.deref.DerefMut (alloc.vec.Vec T) := {
+  derefInst := core.ops.deref.DerefVec T
+  deref_mut := alloc.vec.DerefMutVec.deref_mut T
+}
+
 end Primitives