Update the standard library for Lean

backends/lean/Aeneas/Arith/Lemmas.lean

@@ -11,6 +11,13 @@ theorem Int.emod_of_pos_disj (n m : Int) : m ≤ 0 ∨ (0 ≤ n % m ∧ n % m <
     . apply Int.emod_lt_of_pos; omega
   else left; omega
 
+@[nonlin_scalar_tac n / m]
+theorem Int.div_of_pos_disj (n m : Int) : n < 0 ∨ m < 0 ∨ (0 ≤ n / m ∧ n / m ≤ n) := by
+  dcases hn: 0 ≤ n <;> dcases hm: 0 ≤ m <;> try simp_all
+  right; right; constructor
+  . apply Int.ediv_nonneg <;> omega
+  . apply Int.ediv_le_self; omega
+
 theorem Int.pos_mul_pos_is_pos (n m : Int) (hm : 0 ≤ m) (hn : 0 ≤ n): 0 ≤ m * n := by
   have h : (0 : Int) = 0 * 0 := by simp
   rw [h]
@@ -29,6 +36,7 @@ section
   set_option scalarTac.nonLin true
 
   example (x y : Int) (h : 0 ≤ x ∧ 0 ≤ y) : 0 ≤ x * y := by scalar_tac
+  example (x y : Int) (h : 0 ≤ x ∧ 0 ≤ y) : 0 ≤ x / y := by scalar_tac
 
 end
 

backends/lean/Aeneas/ScalarTac.lean

@@ -1,2 +1,3 @@
 import Aeneas.ScalarTac.IntTac
 import Aeneas.ScalarTac.ScalarTac
+import Aeneas.Arith.Lemmas

backends/lean/Aeneas/ScalarTac/Init.lean

@@ -16,7 +16,6 @@ namespace ScalarTac
 
 declare_aesop_rule_sets [Aeneas.ScalarTac, Aeneas.ScalarTacNonLin]
 
-#check Lean.Option.register
 register_option scalarTac.nonLin : Bool := {
   defValue := false
   group := ""

backends/lean/Aeneas/Std/ArraySlice.lean

@@ -607,6 +607,57 @@ def core.slice.Slice.copy_from_slice {T : Type} (_ : core.marker.Copy T)
 /- [core::array::TryFromSliceError] -/
 def core.array.TryFromSliceError := ()
 
+/- [core::slice::index::{core::slice::index::SliceIndex<@Slice<T>> for core::ops::range::RangeFrom<usize>}::get] -/
+def core.slice.index.SliceIndexcoreopsrangeRangeFromUsizeSlice.get {T : Type} :
+  core.ops.range.RangeFrom Usize → Slice T → Result (Option (Slice T)) := sorry
+
+/- [core::slice::index::{core::slice::index::SliceIndex<@Slice<T>> for core::ops::range::RangeFrom<usize>}::get_mut] -/
+def core.slice.index.SliceIndexcoreopsrangeRangeFromUsizeSlice.get_mut
+  {T : Type} :
+  core.ops.range.RangeFrom Usize → Slice T → Result ((Option (Slice T)) ×
+    (Option (Slice T) → Slice T)) := sorry
+
+/- [core::slice::index::{core::slice::index::SliceIndex<@Slice<T>> for core::ops::range::RangeFrom<usize>}::get_unchecked] -/
+def core.slice.index.SliceIndexcoreopsrangeRangeFromUsizeSlice.get_unchecked {T : Type} :
+  core.ops.range.RangeFrom Usize → ConstRawPtr (Slice T) → Result
+    (ConstRawPtr (Slice T)) := sorry
+
+/- [core::slice::index::{core::slice::index::SliceIndex<@Slice<T>> for core::ops::range::RangeFrom<usize>}::get_unchecked_mut] -/
+def core.slice.index.SliceIndexcoreopsrangeRangeFromUsizeSlice.get_unchecked_mut {T : Type} :
+  core.ops.range.RangeFrom Usize → MutRawPtr (Slice T) → Result (MutRawPtr (Slice T)) := sorry
+
+/- [core::slice::index::{core::slice::index::SliceIndex<@Slice<T>> for core::ops::range::RangeFrom<usize>}::index] -/
+def core.slice.index.SliceIndexcoreopsrangeRangeFromUsizeSlice.index {T : Type} :
+  core.ops.range.RangeFrom Usize → Slice T → Result (Slice T) := sorry
+
+/- [core::slice::index::{core::slice::index::SliceIndex<@Slice<T>> for core::ops::range::RangeFrom<usize>}::index_mut] -/
+def core.slice.index.SliceIndexcoreopsrangeRangeFromUsizeSlice.index_mut {T : Type} :
+  core.ops.range.RangeFrom Usize → Slice T → Result ((Slice T) × (Slice T → Slice T)) := sorry
+
+/- Trait implementation: [core::slice::index::private_slice_index::{core::slice::index::private_slice_index::Sealed for core::ops::range::RangeFrom<usize>}] -/
+@[reducible]
+def core.slice.index.private_slice_index.SealedcoreopsrangeRangeFromUsize :
+  core.slice.index.private_slice_index.Sealed (core.ops.range.RangeFrom Usize)
+  := {}
+
+/- Trait implementation: [core::slice::index::{core::slice::index::SliceIndex<[T]> for core::ops::range::RangeFrom<usize>}] -/
+@[reducible]
+def core.slice.index.SliceIndexcoreopsrangeRangeFromUsizeSlice (T : Type) :
+  core.slice.index.SliceIndex (core.ops.range.RangeFrom Usize) (Slice T) := {
+  Output := Slice T
+  sealedInst :=
+    core.slice.index.private_slice_index.SealedcoreopsrangeRangeFromUsize
+  get := core.slice.index.SliceIndexcoreopsrangeRangeFromUsizeSlice.get
+  get_mut := core.slice.index.SliceIndexcoreopsrangeRangeFromUsizeSlice.get_mut
+  get_unchecked :=
+    core.slice.index.SliceIndexcoreopsrangeRangeFromUsizeSlice.get_unchecked
+  get_unchecked_mut :=
+    core.slice.index.SliceIndexcoreopsrangeRangeFromUsizeSlice.get_unchecked_mut
+  index := core.slice.index.SliceIndexcoreopsrangeRangeFromUsizeSlice.index
+  index_mut :=
+    core.slice.index.SliceIndexcoreopsrangeRangeFromUsizeSlice.index_mut
+}
+
 end Std
 
 end Aeneas

backends/lean/Aeneas/Std/Core.lean

@@ -155,6 +155,11 @@ def core.result.Result.unwrap {T E : Type}
   | .Ok x => ok x
   | .Err _ => fail .panic
 
+/- [core::ops::range::RangeFrom] -/
+structure core.ops.range.RangeFrom (Idx : Type) where
+  start : Idx
+
+
 end Std
 
 end Aeneas

backends/lean/Aeneas/Std/Scalar.lean

@@ -89,7 +89,7 @@ def Scalar.and {ty : ScalarTy} (x : Scalar ty) (y : Scalar ty) : Scalar ty :=
 def Scalar.or {ty : ScalarTy} (x : Scalar ty) (y : Scalar ty) : Scalar ty :=
   sorry
 
-/- ¬ x reverst the bits of x
+/- ¬ x reverses the bits of x
 
    It has the following effect:
    - if x is unsigned, then it evaluates to Scalar.max - x
@@ -1154,10 +1154,10 @@ def int_saturating_add_in_bounds {ty} (x y : Scalar ty) :
   simp [int_saturating_add]
   split <;> constructor <;> cases ty <;> scalar_tac
 
-def Scalar.saturating_add {ty} (x y : Scalar ty) : Result (Scalar ty) :=
+def Scalar.saturating_add {ty} (x y : Scalar ty) : Scalar ty :=
   let r := int_saturating_add ty x.val y.val
   have h := int_saturating_add_in_bounds x y
-  ok ⟨ r, h.1, h.2 ⟩
+  ⟨ r, h.1, h.2 ⟩
 
 /- [core::num::{u8}::saturating_add] -/
 def core.num.U8.saturating_add := @Scalar.saturating_add ScalarTy.U8
@@ -1195,54 +1195,48 @@ def core.num.I128.saturating_add := @Scalar.saturating_add ScalarTy.I128
 /- [core::num::{isize}::saturating_add] -/
 def core.num.Isize.saturating_add := @Scalar.saturating_add ScalarTy.Isize
 
-@[pspec]
 theorem core.num.U8.saturating_add_spec (x y : U8) :
-  ∃ z, saturating_add x y = ok z ∧
+  let z := saturating_add x y
   if x.val + y.val > U8.max then z.val = U8.max
   else z.val = x.val + y.val
   := by
   simp [saturating_add, Scalar.saturating_add, int_saturating_add]
   split <;> split <;> split <;> scalar_tac
 
-@[pspec]
 theorem core.num.U16.saturating_add_spec (x y : U16) :
-  ∃ z, saturating_add x y = ok z ∧
+  let z := saturating_add x y
   if x.val + y.val > U16.max then z.val = U16.max
   else z.val = x.val + y.val
   := by
   simp [saturating_add, Scalar.saturating_add, int_saturating_add]
   split <;> split <;> split <;> scalar_tac
 
-@[pspec]
 theorem core.num.U32.saturating_add_spec (x y : U32) :
-  ∃ z, saturating_add x y = ok z ∧
+  let z := saturating_add x y
   if x.val + y.val > U32.max then z.val = U32.max
   else z.val = x.val + y.val
   := by
   simp [saturating_add, Scalar.saturating_add, int_saturating_add]
   split <;> split <;> split <;> scalar_tac
 
-@[pspec]
 theorem core.num.U64.saturating_add_spec (x y : U64) :
-  ∃ z, saturating_add x y = ok z ∧
+  let z := saturating_add x y
   if x.val + y.val > U64.max then z.val = U64.max
   else z.val = x.val + y.val
   := by
   simp [saturating_add, Scalar.saturating_add, int_saturating_add]
   split <;> split <;> split <;> scalar_tac
 
-@[pspec]
 theorem core.num.U128.saturating_add_spec (x y : U128) :
-  ∃ z, saturating_add x y = ok z ∧
+  let z := saturating_add x y
   if x.val + y.val > U128.max then z.val = U128.max
   else z.val = x.val + y.val
   := by
   simp [saturating_add, Scalar.saturating_add, int_saturating_add]
   split <;> split <;> split <;> scalar_tac
 
-@[pspec]
 theorem core.num.Usize.saturating_add_spec (x y : Usize) :
-  ∃ z, saturating_add x y = ok z ∧
+  let z := saturating_add x y
   if x.val + y.val > Usize.max then z.val = Usize.max
   else z.val = x.val + y.val
   := by
@@ -1262,10 +1256,10 @@ def int_saturating_sub_in_bounds {ty} (x y : Scalar ty) :
   simp [int_saturating_sub]
   split <;> constructor <;> cases ty <;> scalar_tac
 
-def Scalar.saturating_sub {ty} (x y : Scalar ty) : Result (Scalar ty) :=
+def Scalar.saturating_sub {ty} (x y : Scalar ty) : Scalar ty :=
   let r := int_saturating_sub ty x.val y.val
   have h := int_saturating_sub_in_bounds x y
-  ok ⟨ r, h.1, h.2 ⟩
+  ⟨ r, h.1, h.2 ⟩
 
 /- [core::num::{u8}::saturating_sub] -/
 def core.num.U8.saturating_sub := @Scalar.saturating_sub ScalarTy.U8
@@ -1303,54 +1297,48 @@ def core.num.I128.saturating_sub := @Scalar.saturating_sub ScalarTy.I128
 /- [core::num::{isize}::saturating_sub] -/
 def core.num.Isize.saturating_sub := @Scalar.saturating_sub ScalarTy.Isize
 
-@[pspec]
 theorem core.num.U8.saturating_sub_spec (x y : U8) :
-  ∃ z, saturating_sub x y = ok z ∧
+  let z := saturating_sub x y
   if x.val - y.val < 0 then z.val = 0
   else z.val = x.val - y.val
   := by
   simp [saturating_sub, Scalar.saturating_sub, int_saturating_sub]
   split <;> split <;> split <;> scalar_tac
 
-@[pspec]
 theorem core.num.U16.saturating_sub_spec (x y : U16) :
-  ∃ z, saturating_sub x y = ok z ∧
+  let z := saturating_sub x y
   if x.val - y.val < 0 then z.val = 0
   else z.val = x.val - y.val
   := by
   simp [saturating_sub, Scalar.saturating_sub, int_saturating_sub]
   split <;> split <;> split <;> scalar_tac
 
-@[pspec]
 theorem core.num.U32.saturating_sub_spec (x y : U32) :
-  ∃ z, saturating_sub x y = ok z ∧
+  let z := saturating_sub x y
   if x.val - y.val < 0 then z.val = 0
   else z.val = x.val - y.val
   := by
   simp [saturating_sub, Scalar.saturating_sub, int_saturating_sub]
   split <;> split <;> split <;> scalar_tac
 
-@[pspec]
 theorem core.num.U64.saturating_sub_spec (x y : U64) :
-  ∃ z, saturating_sub x y = ok z ∧
+  let z := saturating_sub x y
   if x.val - y.val < 0 then z.val = 0
   else z.val = x.val - y.val
   := by
   simp [saturating_sub, Scalar.saturating_sub, int_saturating_sub]
   split <;> split <;> split <;> scalar_tac
 
-@[pspec]
 theorem core.num.U128.saturating_sub_spec (x y : U128) :
-  ∃ z, saturating_sub x y = ok z ∧
+  let z := saturating_sub x y
   if x.val - y.val < 0 then z.val = 0
   else z.val = x.val - y.val
   := by
   simp [saturating_sub, Scalar.saturating_sub, int_saturating_sub]
   split <;> split <;> split <;> scalar_tac
 
-@[pspec]
 theorem core.num.Usize.saturating_sub_spec (x y : Usize) :
-  ∃ z, saturating_sub x y = ok z ∧
+  let z := saturating_sub x y
   if x.val - y.val < 0 then z.val = 0
   else z.val = x.val - y.val
   := by
@@ -1359,6 +1347,7 @@ theorem core.num.Usize.saturating_sub_spec (x y : Usize) :
 
 -- Wrapping add
 def Scalar.wrapping_add {ty} (x y : Scalar ty) : Scalar ty := sorry
+
 /- [core::num::{u8}::wrapping_add] -/
 def core.num.U8.wrapping_add := @Scalar.wrapping_add ScalarTy.U8
 
@@ -1399,6 +1388,7 @@ def core.num.Isize.wrapping_add := @Scalar.wrapping_add ScalarTy.Isize
 
 -- Wrapping sub
 def Scalar.wrapping_sub {ty} (x y : Scalar ty) : Scalar ty := sorry
+
 /- [core::num::{u8}::wrapping_sub] -/
 def core.num.U8.wrapping_sub := @Scalar.wrapping_sub ScalarTy.U8
 

src/extract/ExtractBuiltin.ml

@@ -10,22 +10,6 @@ include ExtractName (* TODO: only open? *)
 
 let log = Logging.builtin_log
 
-let all_int_names =
-  [
-    "usize";
-    "u8";
-    "u16";
-    "u32";
-    "u64";
-    "u128";
-    "isize";
-    "i8";
-    "i16";
-    "i32";
-    "i64";
-    "i128";
-  ]
-
 (** Small utility to memoize some computations *)
 let mk_memoized (f : unit -> 'a) : unit -> 'a =
   let r = ref None in
@@ -133,7 +117,8 @@ type builtin_type_info = {
 
 type type_variant_kind =
   | KOpaque
-  | KStruct of (string * string) list
+  | KStruct of (string * string option) list
+      (** Contains the list of (field rust name, field extracted name) *)
   | KEnum of string list
 
 let mk_struct_constructor (type_name : string) : string =
@@ -174,6 +159,11 @@ let builtin_types () : builtin_type_info list =
             List.map
               (fun (rname, name) ->
                 ( rname,
+                  let name =
+                    match name with
+                    | None -> rname
+                    | Some name -> name
+                  in
                   match backend () with
                   | FStar | Lean -> name
                   | Coq | HOL4 -> extract_name ^ "_" ^ name ))
@@ -214,7 +204,7 @@ let builtin_types () : builtin_type_info list =
     mk_type "alloc::vec::Vec" ~keep_params:(Some [ true; false ]) ();
     (* Range *)
     mk_type "core::ops::range::Range"
-      ~kind:(KStruct [ ("start", "start"); ("end", "end_") ])
+      ~kind:(KStruct [ ("start", None); ("end", Some "end_") ])
       ();
     (* Option
 
@@ -259,6 +249,9 @@ let builtin_types () : builtin_type_info list =
         mk_type "core::result::Result" ~kind:(KEnum [ "Ok"; "Err" ]) ();
         mk_type "core::fmt::Error" ();
         mk_type "core::array::TryFromSliceError" ();
+        mk_type "core::ops::range::RangeFrom"
+          ~kind:(KStruct [ ("start", None) ])
+          ();
       ]
 
 let mk_builtin_types_map () =
@@ -551,6 +544,30 @@ let mk_builtin_funs () : (pattern * bool list option * builtin_fun_info) list =
          mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::extend_from_slice"
            ~filter:(Some [ true; false ])
            ();
+         mk_fun
+           "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeFrom<usize>, \
+            [@T]>}::get"
+           ();
+         mk_fun
+           "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeFrom<usize>, \
+            [@T]>}::get_mut"
+           ();
+         mk_fun
+           "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeFrom<usize>, \
+            [@T]>}::get_unchecked"
+           ();
+         mk_fun
+           "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeFrom<usize>, \
+            [@T]>}::get_unchecked_mut"
+           ();
+         mk_fun
+           "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeFrom<usize>, \
+            [@T]>}::index"
+           ();
+         mk_fun
+           "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeFrom<usize>, \
+            [@T]>}::index_mut"
+           ();
        ]
       @ List.flatten
           (List.map
@@ -825,6 +842,13 @@ let builtin_trait_impls_info () : (pattern * (bool list option * string)) list =
         (* TryInto<T, U : TryFrom<T>> *)
         fmt "core::convert::{core::convert::TryInto<@T, @U>}"
           ~extract_name:(Some "core::convert::TryIntoFrom") ();
+        fmt
+          "core::slice::index::private_slice_index::Sealed<core::ops::range::RangeFrom<usize>>"
+          ();
+        fmt
+          "core::slice::index::SliceIndex<core::ops::range::RangeFrom<usize>, \
+           [@Self]>"
+          ();
       ]
   (* From<INT, bool> *)
   @ List.map