feat: add specs for some tricky functions

lean/CoreModels.lean

@@ -3,3 +3,4 @@ import CoreModels.Core
 import CoreModels.Alloc
 import CoreModels.HaxLib
 import CoreModels.RustPrimitives
+import CoreModels.Spec

lean/CoreModels/RustPrimitives/Funs.lean

@@ -67,31 +67,15 @@ def rust_primitives.slice.slice_clone_from_slice
   if dest.length = src.length then ok src
   else fail .panic
 
-private theorem foldlM_list_build_length {T F : Type}
-    (step : List T × F → Nat → Result (List T × F))
-    (hstep : ∀ l f i r, step (l, f) i = .ok r → r.1.length = l.length + 1) :
-    ∀ (l : List Nat) (acc : List T) (f : F) (result : List T × F),
-    l.foldlM step (acc, f) = .ok result → result.1.length = acc.length + l.length := by
-  intro l
-  induction l with
-  | nil =>
-    intro acc f result h
-    simp only [List.foldlM_nil] at h
-    have heq : result = (acc, f) := (Result.ok.inj h).symm
-    simp [heq]
-  | cons x xs ih =>
-    intro acc f result h
-    simp only [List.foldlM_cons] at h
-    cases hstep_x : step (acc, f) x with
-    | ok r =>
-      obtain ⟨r1, r2⟩ := r
-      simp only [hstep_x] at h
-      have hlen_r : r1.length = acc.length + 1 := by
-        have := hstep acc f x ⟨r1, r2⟩ hstep_x; simpa using this
-      have ih' := ih r1 r2 result h
-      simp only [List.length_cons]; omega
-    | fail e => simp [hstep_x] at h
-    | div => simp [hstep_x] at h
+/-- This helper function for `array_from_fn` takes a `FnMut` closure and produces a list. A list
+    is easier to produce than an array because we do not need to produce a length-proof. -/
+def rust_primitives.slice.array_from_fn_go {T F : Type}
+    (inst : core.ops.function.FnMut F Std.Usize T) : F → Nat → Result (List T × F)
+  | c, 0 => ok ([], c)
+  | c, n + 1 => do
+    let p ← array_from_fn_go inst c n
+    let q ← inst.call_mut p.2 ⟨BitVec.ofNat _ n⟩
+    ok (p.1 ++ [q.1], q.2)
 
 /-- [rust_primitives::slice::array_from_fn]:
     Source: 'rust_primitives/src/lib.rs', lines 28:4-28:81
@@ -101,35 +85,11 @@ private theorem foldlM_list_build_length {T F : Type}
 def rust_primitives.slice.array_from_fn
   {T : Type} {F : Type} (N : Std.Usize) (coreopsfunctionFnMutFTupleUsizeTInst :
   core.ops.function.FnMut F Std.Usize T) :
-  F → Result (Array T N) := fun f =>
-  match h : (List.range N.val).foldlM
-    (fun (s : List T × F) (i : Nat) => do
-      let (v, f') ← coreopsfunctionFnMutFTupleUsizeTInst.call_mut s.2 ⟨BitVec.ofNat _ i⟩
-      ok (s.1 ++ [v], f'))
-    ([], f) with
-  | fail e => fail e
-  | div => div
-  | ok result => ok ⟨result.1, by
-      have hlen := foldlM_list_build_length
-        (fun (s : List T × F) (i : Nat) => do
-          let (v, f') ← coreopsfunctionFnMutFTupleUsizeTInst.call_mut s.2 ⟨BitVec.ofNat _ i⟩
-          ok (s.1 ++ [v], f'))
-        (fun l f i r hr => by
-          simp only [] at hr
-          cases hcall : coreopsfunctionFnMutFTupleUsizeTInst.call_mut f ⟨BitVec.ofNat _ i⟩ with
-          | ok p =>
-            obtain ⟨v, fv⟩ := p
-            simp only [hcall, bind_tc_ok] at hr
-            have heq : r = (l ++ [v], fv) := (Result.ok.inj hr).symm
-            simp [heq, List.length_append]
-          | fail e =>
-            simp only [hcall, bind_tc_fail] at hr
-            exact nomatch hr
-          | div =>
-            simp only [hcall, bind_tc_div] at hr
-            exact nomatch hr)
-        _ [] f result h
-      simp [List.length_range] at hlen; exact hlen⟩
+  F → Result (Array T N) := fun f => do
+  let p ← array_from_fn_go coreopsfunctionFnMutFTupleUsizeTInst f N.val
+  -- The `else` is unreachable: `array_from_fn_go` always returns one element per
+  -- index, so `p.1.length = N.val`. It's easier to prove that in the spec than here.
+  (if h : p.1.length = N.val then ok ⟨p.1, h⟩ else fail .panic)
 
 /-- [rust_primitives::slice::array_map]:
     Source: 'rust_primitives/src/lib.rs', lines 31:4-31:84

lean/CoreModels/Spec.lean

@@ -0,0 +1,8 @@
+import CoreModels.Spec.Aeneas
+import CoreModels.Spec.RustPrimitives.Arithmetic
+import CoreModels.Spec.RustPrimitives.Slice
+import CoreModels.Spec.Core.Num
+import CoreModels.Spec.Core.Array
+import CoreModels.Spec.Core.Slice
+import CoreModels.Spec.Core.Convert
+import CoreModels.Spec.Core.Iter

lean/CoreModels/Spec/Aeneas.lean

@@ -0,0 +1,137 @@
+import CoreModels.Core.Funs
+
+namespace Aeneas.Std
+open Std.Do WP Result
+
+set_option mvcgen.warning false
+
+@[spec]
+theorem Result.ok_spec {α : Type} {a : α} {Q} (hQ : (Q.1 a).down) :
+  ⦃ ⌜ True ⌝ ⦄ Result.ok a ⦃ Q ⦄ := by simpa [Triple]
+
+@[spec]
+theorem Result.fail_spec {α : Type} {e : Error} {Q} (hQ : (Q.2.1 e).down) :
+  ⦃ ⌜ True ⌝ ⦄ (Result.fail e : Result α) ⦃ Q ⦄ := by simpa [Triple]
+
+/-- A triple with postcondition `r = v` is equivalent to the program being `.ok v`. -/
+theorem triple_post_eq_iff_eq {α : Type} {x : Result α} {v : α} :
+    ⦃ ⌜ True ⌝ ⦄ x ⦃ ⇓ r => ⌜ r = v ⌝ ⦄ ↔ x = .ok v := by
+  cases x <;> simp_all [Triple, WP.wp, PredTrans.apply]
+
+/-- If the program equals `.ok v`, then a triple is equivalent to its postcondition on `.ok v`.  -/
+theorem triple_iff_post_of_eq_ok {α : Type} {x : Result α} {v : α} {P : α → Prop}
+    (hx : x = .ok v) : ⦃ ⌜ True ⌝ ⦄ x ⦃ ⇓ r => ⌜ P r ⌝ ⦄ ↔ P v := by
+  simp_all [Triple, WP.wp, PredTrans.apply]
+
+/-- A triple is equivalent to the existence of a value `a` such that the program is `.ok a`
+and the postcondition holds on `a`. -/
+theorem triple_iff_exists_ok {α : Type} {x : Result α} {P : α → Prop} :
+    ⦃ ⌜ True ⌝ ⦄ x ⦃ ⇓ r => ⌜ P r ⌝ ⦄ ↔ ∃ a, x = .ok a ∧ P a := by
+  cases x <;> simp_all [Triple, WP.wp, PredTrans.apply]
+
+/-- Enrich triple's postcondition to contain a triple stating which program produced the value. -/
+theorem triple_with_self {α : Type} {x : Result α} {P : α → Prop}
+    (h : ⦃ ⌜ True ⌝ ⦄ x ⦃ ⇓ r => ⌜ P r ⌝ ⦄) :
+    ⦃ ⌜ True ⌝ ⦄ x ⦃ ⇓ r => ⌜ P r ∧ ⦃ ⌜ True ⌝ ⦄ x ⦃ ⇓ r' => ⌜ r' = r ⌝ ⦄ ⌝ ⦄ := by
+  obtain ⟨a, hx, hPa⟩ := triple_iff_exists_ok.1 h
+  exact (triple_iff_post_of_eq_ok hx).2 ⟨hPa, triple_post_eq_iff_eq.2 hx⟩
+
+/- Modus-ponens-like reasoning on a `noThrow` and a `mayThrow` triple -/
+theorem triple_in_hypothesis {f : Result α} {Q : α → Assertion _} (p : Prop)
+    (h : ⦃ ⌜ True ⌝ ⦄ f ⦃ ⇓ r => Q r ⦄)
+    (hp : ⦃ ⌜ True ⌝ ⦄ f ⦃ ⇓? r => Q r → ⌜ p ⌝ ⦄) :
+    p := by
+  cases f <;> simp_all [Triple, WP.wp, PredTrans.apply]
+
+attribute [spec] Function.uncurry lift massert
+
+@[spec]
+theorem loop_spec
+  {α β γ : Type}
+  {P : PostCond β (PostShape.except Error (PostShape.except PUnit.{1} PostShape.pure))}
+  {body : α → Result (ControlFlow α β)} {init : α}
+  (inv : α → Prop)
+  (rel : γ → γ → Prop)
+  (termination : α → γ)
+  (hwf : WellFounded rel)
+  (h_inv_init : inv init)
+  (h_body : ∀ x, inv x → ⦃ ⌜ True ⌝ ⦄ body x ⦃ post⟨
+    fun cf => match cf with
+      | .cont r => ⌜ inv r ∧ (rel (termination r) (termination x) ∨ (P.2.2.1 ()).down) ⌝
+      | .done r => P.1 r,
+    P.2.1, P.2.2.1⟩ ⦄) :
+  ⦃ ⌜ True ⌝ ⦄ loop body init ⦃ P ⦄ := by
+  suffices h : ∀ x, inv x → (wp⟦loop body x⟧ P).down by
+    unfold Triple
+    intro _
+    exact h init h_inv_init
+  by_cases hdiv : (P.2.2.1 ()).down
+  · -- Divergence permitted: use partial-fixpoint induction.
+    intro x hinv
+    delta loop
+    refine Lean.Order.fix_induct (loop._proof_1 body)
+      (motive := fun g => ∀ x, inv x → (wp⟦g x⟧ P).down) ?_ ?_ x hinv
+    · apply Lean.Order.admissible_pi
+      intro y
+      apply Lean.Order.admissible_pi
+      intro _
+      apply Lean.Order.admissible_apply (β := fun _ => Result β)
+        (P := fun y r => (wp⟦r⟧ P).down) y
+      exact Lean.Order.admissible_flatOrder _ hdiv
+    · intro g IH y hinvy
+      have hb : (wp⟦body y⟧ _).down := h_body y hinvy trivial
+      cases hbe : body y with
+      | ok cf =>
+        rw [hbe] at hb
+        cases cf with
+        | cont r => exact IH r hb.1
+        | done r => exact hb
+      | fail e => rw [hbe] at hb; exact hb
+      | div => rw [hbe] at hb; exact hb
+  · -- Termination via WF induction on `rel`.
+    intro x hinv
+    induction hg : termination x using hwf.induction generalizing x
+    rename_i g IH
+    have hb : (wp⟦body x⟧ _).down := h_body x hinv trivial
+    rw [loop.eq_1]
+    cases hbe : body x with
+    | ok cf =>
+      rw [hbe] at hb
+      cases cf with
+      | cont r =>
+        obtain ⟨hinvr, hrel | hd⟩ := hb
+        · subst hg
+          exact IH (termination r) hrel r hinvr rfl
+        · exact absurd hd hdiv
+      | done r => exact hb
+    | fail e => rw [hbe] at hb; exact hb
+    | div => rw [hbe] at hb; exact hb
+
+open ScalarElab
+
+iscalar_no_isize @[spec] theorem  «%S».hShiftRight_I8_spec (a : «%S») (b : I8) (hmin : b.val ≥ 0) (hmax : b.val < %Size) :
+    ⦃ ⌜ True ⌝ ⦄ (a >>> b) ⦃ ⇓ r => ⌜ r.val = a.val / (2 ^ b.val.toNat) ⌝ ⦄ := by
+  mvcgen [HShiftRight.hShiftRight, IScalar.shiftRight_IScalar, IScalar.shiftRight]
+    <;> grind [IScalar.val, Int.shiftRight_eq_div_pow]
+
+iscalar_no_isize @[spec] theorem  «%S».hShiftRight_I16_spec (a : «%S») (b : I16) (hmin : b.val ≥ 0) (hmax : b.val < %Size) :
+    ⦃ ⌜ True ⌝ ⦄ (a >>> b) ⦃ ⇓ r => ⌜ r.val = a.val / (2 ^ b.val.toNat) ⌝ ⦄ := by
+  mvcgen [HShiftRight.hShiftRight, IScalar.shiftRight_IScalar, IScalar.shiftRight]
+    <;> grind [IScalar.val, Int.shiftRight_eq_div_pow]
+
+iscalar_no_isize @[spec] theorem  «%S».hShiftRight_I32_spec (a : «%S») (b : I32) (hmin : b.val ≥ 0) (hmax : b.val < %Size) :
+    ⦃ ⌜ True ⌝ ⦄ (a >>> b) ⦃ ⇓ r => ⌜ r.val = a.val / (2 ^ b.val.toNat) ⌝ ⦄ := by
+  mvcgen [HShiftRight.hShiftRight, IScalar.shiftRight_IScalar, IScalar.shiftRight]
+    <;> grind [IScalar.val, Int.shiftRight_eq_div_pow]
+
+iscalar_no_isize @[spec] theorem  «%S».hShiftRight_I64_spec (a : «%S») (b : I64) (hmin : b.val ≥ 0) (hmax : b.val < %Size) :
+    ⦃ ⌜ True ⌝ ⦄ (a >>> b) ⦃ ⇓ r => ⌜ r.val = a.val / (2 ^ b.val.toNat) ⌝ ⦄ := by
+  mvcgen [HShiftRight.hShiftRight, IScalar.shiftRight_IScalar, IScalar.shiftRight]
+    <;> grind [IScalar.val, Int.shiftRight_eq_div_pow]
+
+iscalar_no_isize @[spec] theorem  «%S».hShiftRight_I128_spec (a : «%S») (b : I128) (hmin : b.val ≥ 0) (hmax : b.val < %Size) :
+    ⦃ ⌜ True ⌝ ⦄ (a >>> b) ⦃ ⇓ r => ⌜ r.val = a.val / (2 ^ b.val.toNat) ⌝ ⦄ := by
+  mvcgen [HShiftRight.hShiftRight, IScalar.shiftRight_IScalar, IScalar.shiftRight]
+    <;> grind [IScalar.val, Int.shiftRight_eq_div_pow]
+
+end Aeneas.Std

lean/CoreModels/Spec/Core/Array.lean

@@ -0,0 +1,81 @@
+import CoreModels.Core.Funs
+import CoreModels.Spec.Aeneas
+import CoreModels.Spec.Core.Slice
+import CoreModels.Spec.RustPrimitives.Slice
+
+namespace CoreModels
+
+open Aeneas
+open Aeneas.Std hiding namespace core alloc
+open Std.Do WP Result
+set_option mvcgen.warning false
+
+open ScalarElab
+
+uscalar @[spec] theorem «%S».Array.eq_spec {N : Std.Usize} {Q}
+  (a : Array «%S» N) (b : Array «%S» N) (h : (Q.1 (a.val == b.val)).down) :
+  ⦃ ⌜ True ⌝ ⦄
+  core.Array.Insts.CoreCmpPartialEqArray.eq core.«%S».Insts.CoreCmpPartialEq'S a b
+  ⦃ Q ⦄ := by
+  mvcgen -trivial [core.Array.Insts.CoreCmpPartialEqArray.eq,
+    core.Array.Insts.CoreCmpPartialEqArray.eq_loop,
+    core.Array.Insts.CoreCmpPartialEqArray.eq_loop.body, rust_primitives.slice.array_index,
+    core.«%S».Insts.CoreCmpPartialEq'S]
+  case vc1.γ => exact Nat
+  case vc4.termination => exact fun i => N.val - i.val
+  case vc3.rel => exact (· < ·)
+  case vc5.hwf => exact wellFounded_lt
+  case vc2.inv => exact fun i => a.val.take i.val = b.val.take i.val
+  case vc10 =>
+    constructor
+    · simp_all [@List.take_add, @List.take_one, -List.take_append_getElem]
+    · grind
+  · grind
+  · grind
+  · grind
+  · grind
+  · convert h; grind
+  · convert h; grind [List.take_eq_self_iff, List.Vector.length_val]
+
+@[spec]
+theorem Array.index_range_spec
+      {T : Type} {N : Std.Usize} (arr : Std.Array T N)
+      (r : core.ops.range.Range Std.Usize)
+      (h0 : r.start.val < r.end.val) -- TODO: We should be able to allow "≤" here
+      (h1 : r.end.val ≤ N.val) :
+    ⦃ ⌜ True ⌝ ⦄
+    core.Array.Insts.CoreOpsIndexIndex.index
+      (core.Shared0Slice.Insts.CoreOpsIndexIndexRangeUsizeSlice T)
+      arr r
+    ⦃ ⇓ r' => ⌜ r'.val = arr.val.slice r.start.val r.end.val ∧
+                r'.val.length + r.start.val = r.end.val ⌝ ⦄ := by
+  mvcgen [core.Array.Insts.CoreOpsIndexIndex.index, core.array.Array.as_slice,
+      rust_primitives.slice.array_as_slice]
+    <;> grind
+
+/-- This spec for from_fn only works for non-mutating functions. If the function
+mutates, we would need a different spec with a user-provided invariant. -/
+@[spec]
+theorem Array.from_fn_spec
+    {T F : Type} [Inhabited T] (N : Std.Usize)
+    (inst : core.ops.function.FnMut F Std.Usize T) (c : F) (f : Nat → T)
+    (hpure : ∀ k : Nat, k < N.val →
+      ⦃ ⌜ True ⌝ ⦄
+      inst.call_mut c ⟨BitVec.ofNat _ k⟩
+      ⦃ ⇓ r => ⌜ r = (f k, c) ⌝ ⦄) :
+    ⦃ ⌜ True ⌝ ⦄
+    core.array.from_fn N inst c
+    ⦃ ⇓ a => ⌜ ∀ i : Nat, (hi : i < N.val) →
+                a.val[i]'(by grind) = f i ⌝ ⦄ := by
+  unfold CoreModels.core.array.from_fn
+  mvcgen
+  case vc1.hpure k hk =>
+    mvcgen [hpure]
+    grind
+  case vc2.success =>
+    intro hpost i hi
+    apply triple_in_hypothesis _ (hpost i hi)
+    mvcgen [hpure]
+    grind
+
+end CoreModels

lean/CoreModels/Spec/Core/Convert.lean

@@ -0,0 +1,47 @@
+import CoreModels.Spec.Aeneas
+import CoreModels.Spec.RustPrimitives.Slice
+
+namespace CoreModels
+
+open Aeneas
+open Aeneas.Std hiding namespace core alloc
+open Std.Do WP Result
+
+set_option mvcgen.warning false
+
+@[spec]
+theorem core.convert.TryFromArrayShared0SliceTryFromSliceError.try_from.closure.Insts.CoreOpsFunctionFnMutTupleUsizeT.call_mut_spec
+    {T : Type} [Inhabited T] {N : Std.Usize} (cpy : core.marker.Copy T)
+    (s : Slice T) (i : Std.Usize) (h : i.val < s.val.length) :
+    ⦃ ⌜ True ⌝ ⦄
+    core.convert.TryFromArrayShared0SliceTryFromSliceError.try_from.closure.Insts.CoreOpsFunctionFnMutTupleUsizeT.call_mut
+      (T := T) (N := N) cpy s i
+    ⦃ ⇓ r => ⌜ r = (s.val[i.val]'h, s) ⌝ ⦄ := by
+  unfold core.convert.TryFromArrayShared0SliceTryFromSliceError.try_from.closure.Insts.CoreOpsFunctionFnMutTupleUsizeT.call_mut
+  unfold rust_primitives.slice.slice_index Std.Slice.index_usize
+  mvcgen <;> simp_all [Std.Slice.getElem?_Usize_eq]
+
+@[spec]
+theorem core.Array.Insts.CoreConvertTryFromShared0SliceTryFromSliceError.try_from_spec
+    {T : Type} [Inhabited T] {N : Std.Usize} (cpy : core.marker.Copy T)
+    (s : Slice T) (hlen : s.val.length = N.val) :
+    ⦃ ⌜ True ⌝ ⦄
+    core.Array.Insts.CoreConvertTryFromShared0SliceTryFromSliceError.try_from
+      N cpy s
+    ⦃ ⇓ r => ⌜ r = core.result.Result.Ok
+                     (Std.Array.make N s.val (by simp [hlen])) ⌝ ⦄ := by
+  mvcgen [core.Array.Insts.CoreConvertTryFromShared0SliceTryFromSliceError.try_from,
+    core.slice.Slice.len]
+  · grind [UScalar.val]
+  · grind
+  · rename_i a hapost
+    congr
+    apply Subtype.ext
+    apply List.ext_getElem
+    · rw [a.property]; exact hlen.symm
+    · intro i h1 h2
+      apply triple_in_hypothesis _ (hapost i (a.property ▸ h1))
+      mvcgen <;> grind [UScalar.val, Array.make]
+  · grind
+
+end CoreModels

lean/CoreModels/Spec/Core/Iter.lean

@@ -0,0 +1,30 @@
+import CoreModels.Core.Funs
+import CoreModels.Alloc.Funs
+import CoreModels.Spec.Aeneas
+
+namespace CoreModels
+
+open Aeneas
+open Aeneas.Std hiding namespace core alloc
+open Std.Do WP Result
+
+set_option mvcgen.warning false
+
+@[spec]
+theorem core.IteratorRange.next_CoreIterRangeStep_spec {Q} (range : core.ops.range.Range Std.Usize)
+      (h_lt : (h : range.start.val < range.end.val) →
+        ∀ (s : Usize), s.val = range.start.val + 1 →
+        (Q.1 (some range.start, { start := s, «end» := range.end })).down)
+      (h_ge : range.start.val ≥ range.end.val → (Q.1 (none, range)).down) :
+    ⦃ ⌜ True ⌝ ⦄
+    core.IteratorRange.next core.Usize.Insts.CoreIterRangeStep range
+    ⦃ Q ⦄ := by
+  mvcgen [core.IteratorRange.next, core.Usize.Insts.CoreIterRangeStep, uncurry,
+    core.Usize.Insts.CoreCmpPartialOrdUsize, core.mkUPartialOrd,
+    core.Usize.Insts.CoreCloneClone.clone, core.Usize.Insts.CoreIterRangeStep.forward_checked,
+    core.convert.TryFromUTInfallible.Blanket.try_from, core.convert.From.Blanket.from,
+    core.num.Usize.checked_add, core.num.Usize.overflowing_add,
+    rust_primitives.arithmetic.overflowing_add_usize]
+    <;> grind [UScalar.overflowing_add, BitVec.uaddOverflow, UScalar.overflowing_add_eq]
+
+end CoreModels