Merge pull request #416 from AeneasVerif/son/fix2

Fix minor issues and add definitions to the standard library

backends/lean/Base/Primitives/ArraySlice.lean

@@ -44,11 +44,21 @@ abbrev Array.v {α : Type u} {n : Usize} (v : Array α n) : List α := v.val
 example {α: Type u} {n : Usize} (v : Array α n) : v.length ≤ Scalar.max ScalarTy.Usize := by
   scalar_tac
 
-def Array.make {α : Type u} (n : Usize) (init : List α) (hl : init.length = n.val := by decide) :
+def Array.make {α : Type u} (n : Usize) (init : List α) (hl : init.length = n.val := by rfl) :
   Array α n := ⟨ init, by apply hl ⟩
 
 example : Array Int (Usize.ofInt 2) := Array.make (Usize.ofInt 2) [0, 1]
 
+example : Array Int (Usize.ofInt 2) :=
+  let x := 0
+  let y := 1
+  Array.make (Usize.ofInt 2) [x, y]
+
+example : Result (Array Int (Usize.ofInt 2)) := do
+  let x ← ok 0
+  let y ← ok 1
+  ok (Array.make (Usize.ofInt 2) [x, y])
+
 @[simp]
 abbrev Array.index_s {α : Type u} {n : Usize} [Inhabited α] (v : Array α n) (i : Nat) : α :=
   v.val.index i

backends/lean/Base/Primitives/Scalar.lean

@@ -1355,4 +1355,84 @@ theorem core.num.Usize.saturating_sub_spec (x y : Usize) :
   simp [saturating_sub, Scalar.saturating_sub, int_saturating_sub]
   split <;> split <;> split <;> scalar_tac
 
+-- Wrapping add
+def Scalar.wrapping_add {ty} (x y : Scalar ty) : Result (Scalar ty) := sorry
+/- [core::num::{u8}::wrapping_add] -/
+def core.num.U8.wrapping_add := @Scalar.wrapping_add ScalarTy.U8
+
+/- [core::num::{u16}::wrapping_add] -/
+def core.num.U16.wrapping_add := @Scalar.wrapping_add ScalarTy.U16
+
+/- [core::num::{u32}::wrapping_add] -/
+def core.num.U32.wrapping_add := @Scalar.wrapping_add ScalarTy.U32
+
+/- [core::num::{u64}::wrapping_add] -/
+def core.num.U64.wrapping_add := @Scalar.wrapping_add ScalarTy.U64
+
+/- [core::num::{u128}::wrapping_add] -/
+def core.num.U128.wrapping_add := @Scalar.wrapping_add ScalarTy.U128
+
+/- [core::num::{usize}::wrapping_add] -/
+def core.num.Usize.wrapping_add := @Scalar.wrapping_add ScalarTy.Usize
+
+/- [core::num::{i8}::wrapping_add] -/
+def core.num.I8.wrapping_add := @Scalar.wrapping_add ScalarTy.I8
+
+/- [core::num::{i16}::wrapping_add] -/
+def core.num.I16.wrapping_add := @Scalar.wrapping_add ScalarTy.I16
+
+/- [core::num::{i32}::wrapping_add] -/
+def core.num.I32.wrapping_add := @Scalar.wrapping_add ScalarTy.I32
+
+/- [core::num::{i64}::wrapping_add] -/
+def core.num.I64.wrapping_add := @Scalar.wrapping_add ScalarTy.I64
+
+/- [core::num::{i128}::wrapping_add] -/
+def core.num.I128.wrapping_add := @Scalar.wrapping_add ScalarTy.I128
+
+/- [core::num::{isize}::wrapping_add] -/
+def core.num.Isize.wrapping_add := @Scalar.wrapping_add ScalarTy.Isize
+
+-- TODO: reasoning lemmas for wrapping add
+
+-- Wrapping sub
+def Scalar.wrapping_sub {ty} (x y : Scalar ty) : Result (Scalar ty) := sorry
+/- [core::num::{u8}::wrapping_sub] -/
+def core.num.U8.wrapping_sub := @Scalar.wrapping_sub ScalarTy.U8
+
+/- [core::num::{u16}::wrapping_sub] -/
+def core.num.U16.wrapping_sub := @Scalar.wrapping_sub ScalarTy.U16
+
+/- [core::num::{u32}::wrapping_sub] -/
+def core.num.U32.wrapping_sub := @Scalar.wrapping_sub ScalarTy.U32
+
+/- [core::num::{u64}::wrapping_sub] -/
+def core.num.U64.wrapping_sub := @Scalar.wrapping_sub ScalarTy.U64
+
+/- [core::num::{u128}::wrapping_sub] -/
+def core.num.U128.wrapping_sub := @Scalar.wrapping_sub ScalarTy.U128
+
+/- [core::num::{usize}::wrapping_sub] -/
+def core.num.Usize.wrapping_sub := @Scalar.wrapping_sub ScalarTy.Usize
+
+/- [core::num::{i8}::wrapping_sub] -/
+def core.num.I8.wrapping_sub := @Scalar.wrapping_sub ScalarTy.I8
+
+/- [core::num::{i16}::wrapping_sub] -/
+def core.num.I16.wrapping_sub := @Scalar.wrapping_sub ScalarTy.I16
+
+/- [core::num::{i32}::wrapping_sub] -/
+def core.num.I32.wrapping_sub := @Scalar.wrapping_sub ScalarTy.I32
+
+/- [core::num::{i64}::wrapping_sub] -/
+def core.num.I64.wrapping_sub := @Scalar.wrapping_sub ScalarTy.I64
+
+/- [core::num::{i128}::wrapping_sub] -/
+def core.num.I128.wrapping_sub := @Scalar.wrapping_sub ScalarTy.I128
+
+/- [core::num::{isize}::wrapping_sub] -/
+def core.num.Isize.wrapping_sub := @Scalar.wrapping_sub ScalarTy.Isize
+
+-- TODO: reasoning lemmas for wrapping sub
+
 end Primitives

backends/lean/Base/Primitives/Vec.lean

@@ -204,7 +204,12 @@ def alloc.slice.Slice.to_vec
 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} (_ : Usize) : alloc.vec.Vec T := Vec.new T
+def alloc.vec.Vec.with_capacity (T : Type) (_ : Usize) : alloc.vec.Vec T := Vec.new T
+
+/- [alloc::vec::{alloc::vec::Vec<T, A>}::extend_from_slice] -/
+def alloc.vec.Vec.extend_from_slice {T : Type} (cloneInst : core.clone.Clone T)
+  (v : alloc.vec.Vec T) (s : Slice T) : Result (alloc.vec.Vec T) :=
+  sorry
 
 /- [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

src/extract/ExtractBuiltin.ml

@@ -564,6 +564,10 @@ let mk_builtin_funs () : (pattern * bool list option * builtin_fun_info) list =
          (* [core::slice::{@Slice<T>}::copy_from_slice] *)
          mk_fun "core::slice::{[@T]}::copy_from_slice" ();
          mk_fun "core::result::{core::result::Result<@T, @E>}::unwrap" ();
+         (* Vec *)
+         mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::extend_from_slice"
+           ~filter:(Some [ true; false ])
+           ();
        ]
       @ List.map
           (fun ty ->

src/interp/InterpreterBorrows.ml

@@ -2237,7 +2237,7 @@ let rec simplify_dummy_values_useless_abs_aux (config : config)
       let ctx = update_aproj_loans_to_ended span abs_id sv ctx in
       rec_call ctx
 
-let rec simplify_dummy_values_useless_abs (config : config) (span : Meta.span)
+let simplify_dummy_values_useless_abs (config : config) (span : Meta.span)
     (fixed_abs_ids : AbstractionId.Set.t) : cm_fun =
  fun ctx0 ->
   (* Simplify the context as long as it leads to changes - TODO: make this more efficient *)

src/symbolic/SymbolicToPure.ml

@@ -695,9 +695,6 @@ let compute_explicit_info (generics : Pure.generic_params) (input_tys : ty list)
     explicit_const_generics = List.map make_explicit_cg generics.const_generics;
   }
 
-let compute_fun_sig_explicit_info (sg : Pure.fun_sig) : explicit_info =
-  compute_explicit_info sg.generics sg.inputs
-
 (** Translate a type definition from LLBC
 
     Remark: this is not symbolic to pure but LLBC to pure. Still,

tests/lean/Scalars.lean

@@ -0,0 +1,51 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [scalars]
+import Base
+open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+
+namespace scalars
+
+/- [scalars::u32_use_wrapping_add]:
+   Source: 'tests/src/scalars.rs', lines 3:0-5:1 -/
+def u32_use_wrapping_add (x : U32) (y : U32) : Result U32 :=
+  Result.ok (core.num.u32.wrapping_add x y)
+
+/- [scalars::i32_use_wrapping_add]:
+   Source: 'tests/src/scalars.rs', lines 7:0-9:1 -/
+def i32_use_wrapping_add (x : I32) (y : I32) : Result I32 :=
+  Result.ok (core.num.i32.wrapping_add x y)
+
+/- [scalars::u32_use_wrapping_sub]:
+   Source: 'tests/src/scalars.rs', lines 11:0-13:1 -/
+def u32_use_wrapping_sub (x : U32) (y : U32) : Result U32 :=
+  Result.ok (core.num.u32.wrapping_sub x y)
+
+/- [scalars::i32_use_wrapping_sub]:
+   Source: 'tests/src/scalars.rs', lines 15:0-17:1 -/
+def i32_use_wrapping_sub (x : I32) (y : I32) : Result I32 :=
+  Result.ok (core.num.i32.wrapping_sub x y)
+
+/- [scalars::u32_use_shift_right]:
+   Source: 'tests/src/scalars.rs', lines 19:0-21:1 -/
+def u32_use_shift_right (x : U32) : Result U32 :=
+  x >>> 2#i32
+
+/- [scalars::i32_use_shift_right]:
+   Source: 'tests/src/scalars.rs', lines 23:0-25:1 -/
+def i32_use_shift_right (x : I32) : Result I32 :=
+  x >>> 2#i32
+
+/- [scalars::u32_use_shift_left]:
+   Source: 'tests/src/scalars.rs', lines 27:0-29:1 -/
+def u32_use_shift_left (x : U32) : Result U32 :=
+  x <<< 2#i32
+
+/- [scalars::i32_use_shift_left]:
+   Source: 'tests/src/scalars.rs', lines 31:0-33:1 -/
+def i32_use_shift_left (x : I32) : Result I32 :=
+  x <<< 2#i32
+
+end scalars

tests/lean/Vec.lean

@@ -0,0 +1,26 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [vec]
+import Base
+open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+
+namespace vec
+
+/- [vec::use_extend_from_slice]:
+   Source: 'tests/src/vec.rs', lines 5:0-7:1 -/
+def use_extend_from_slice
+  {T : Type} (corecloneCloneInst : core.clone.Clone T) (v : alloc.vec.Vec T)
+  (s : Slice T) :
+  Result (alloc.vec.Vec T)
+  :=
+  alloc.vec.Vec.extend_from_slice corecloneCloneInst v s
+
+/- [vec::use_alloc_with_capacity]:
+   Source: 'tests/src/vec.rs', lines 9:0-11:1 -/
+def use_alloc_with_capacity
+  (T : Type) (n : Usize) : Result (alloc.vec.Vec T) :=
+  Result.ok (alloc.vec.Vec.with_capacity T n)
+
+end vec

tests/src/scalars.rs

@@ -0,0 +1,33 @@
+//@ [coq,fstar,borrow-check] skip
+
+fn u32_use_wrapping_add(x : u32, y : u32) -> u32 {
+    x.wrapping_add(y)
+}
+
+fn i32_use_wrapping_add(x : i32, y : i32) -> i32 {
+    x.wrapping_add(y)
+}
+
+fn u32_use_wrapping_sub(x : u32, y : u32) -> u32 {
+    x.wrapping_sub(y)
+}
+
+fn i32_use_wrapping_sub(x : i32, y : i32) -> i32 {
+    x.wrapping_sub(y)
+}
+
+fn u32_use_shift_right(x : u32) -> u32 {
+    x >> 2
+}
+
+fn i32_use_shift_right(x : i32) -> i32 {
+    x >> 2
+}
+
+fn u32_use_shift_left(x : u32) -> u32 {
+    x << 2
+}
+
+fn i32_use_shift_left(x : i32) -> i32 {
+    x << 2
+}

tests/src/vec.rs

@@ -0,0 +1,11 @@
+//@ [coq,fstar,borrow-check] skip
+
+use std::vec::Vec;
+
+fn use_extend_from_slice<T: Clone>(v: &mut Vec<T>, s: &[T]) {
+    v.extend_from_slice(s)
+}
+
+fn use_alloc_with_capacity<T>(n: usize) -> Vec<T> {
+    Vec::with_capacity(n)
+}