From ae34a7d2e4aafb7be8929c8c48607c3564d3823f Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Mon, 22 Jun 2026 11:38:12 +0200 Subject: [PATCH 1/2] feat: add specs for some tricky functions --- lean/CoreModels.lean | 1 + lean/CoreModels/RustPrimitives/Funs.lean | 68 ++------- lean/CoreModels/Spec.lean | 8 + lean/CoreModels/Spec/Aeneas.lean | 137 ++++++++++++++++++ lean/CoreModels/Spec/Core/Array.lean | 81 +++++++++++ lean/CoreModels/Spec/Core/Convert.lean | 47 ++++++ lean/CoreModels/Spec/Core/Iter.lean | 30 ++++ lean/CoreModels/Spec/Core/Num.lean | 25 ++++ lean/CoreModels/Spec/Core/Slice.lean | 27 ++++ .../Spec/RustPrimitives/Arithmetic.lean | 25 ++++ .../CoreModels/Spec/RustPrimitives/Slice.lean | 78 ++++++++++ 11 files changed, 473 insertions(+), 54 deletions(-) create mode 100644 lean/CoreModels/Spec.lean create mode 100644 lean/CoreModels/Spec/Aeneas.lean create mode 100644 lean/CoreModels/Spec/Core/Array.lean create mode 100644 lean/CoreModels/Spec/Core/Convert.lean create mode 100644 lean/CoreModels/Spec/Core/Iter.lean create mode 100644 lean/CoreModels/Spec/Core/Num.lean create mode 100644 lean/CoreModels/Spec/Core/Slice.lean create mode 100644 lean/CoreModels/Spec/RustPrimitives/Arithmetic.lean create mode 100644 lean/CoreModels/Spec/RustPrimitives/Slice.lean diff --git a/lean/CoreModels.lean b/lean/CoreModels.lean index 432c69d..5630275 100644 --- a/lean/CoreModels.lean +++ b/lean/CoreModels.lean @@ -3,3 +3,4 @@ import CoreModels.Core import CoreModels.Alloc import CoreModels.HaxLib import CoreModels.RustPrimitives +import CoreModels.Spec diff --git a/lean/CoreModels/RustPrimitives/Funs.lean b/lean/CoreModels/RustPrimitives/Funs.lean index 9358f69..70cc3a2 100644 --- a/lean/CoreModels/RustPrimitives/Funs.lean +++ b/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 diff --git a/lean/CoreModels/Spec.lean b/lean/CoreModels/Spec.lean new file mode 100644 index 0000000..51aa6f9 --- /dev/null +++ b/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 diff --git a/lean/CoreModels/Spec/Aeneas.lean b/lean/CoreModels/Spec/Aeneas.lean new file mode 100644 index 0000000..bcb7124 --- /dev/null +++ b/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 eqivalent to the program being `.ok v`. -/ +theorem triple_of_result_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_of_result_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 diff --git a/lean/CoreModels/Spec/Core/Array.lean b/lean/CoreModels/Spec/Core/Array.lean new file mode 100644 index 0000000..e8f1f78 --- /dev/null +++ b/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 diff --git a/lean/CoreModels/Spec/Core/Convert.lean b/lean/CoreModels/Spec/Core/Convert.lean new file mode 100644 index 0000000..f836b99 --- /dev/null +++ b/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 diff --git a/lean/CoreModels/Spec/Core/Iter.lean b/lean/CoreModels/Spec/Core/Iter.lean new file mode 100644 index 0000000..d8aea38 --- /dev/null +++ b/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 diff --git a/lean/CoreModels/Spec/Core/Num.lean b/lean/CoreModels/Spec/Core/Num.lean new file mode 100644 index 0000000..37ea942 --- /dev/null +++ b/lean/CoreModels/Spec/Core/Num.lean @@ -0,0 +1,25 @@ +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 + +attribute [spec] + CoreModels.core.num.U8.from_le_bytes + CoreModels.core.num.U16.from_le_bytes + CoreModels.core.num.U32.from_le_bytes + CoreModels.core.num.U64.from_le_bytes + CoreModels.core.num.U128.from_le_bytes + CoreModels.core.num.Usize.from_le_bytes + CoreModels.core.num.U8.to_le_bytes + CoreModels.core.num.U16.to_le_bytes + CoreModels.core.num.U32.to_le_bytes + CoreModels.core.num.U64.to_le_bytes + CoreModels.core.num.U128.to_le_bytes + CoreModels.core.num.Usize.to_le_bytes + +end CoreModels diff --git a/lean/CoreModels/Spec/Core/Slice.lean b/lean/CoreModels/Spec/Core/Slice.lean new file mode 100644 index 0000000..9535487 --- /dev/null +++ b/lean/CoreModels/Spec/Core/Slice.lean @@ -0,0 +1,27 @@ +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 + +attribute [spec] + CoreModels.core.slice.Slice.len + +@[spec] +theorem core.Shared0Slice.Insts.CoreOpsIndexIndexRangeUsizeSlice.index_spec + {T : Type} (s : Slice T) (r : core.ops.range.Range Std.Usize) + (h0 : r.start.val < r.end.val) -- TODO: we should be able to allow "≤" + (h1 : r.end.val ≤ s.val.length) : + ⦃ ⌜ True ⌝ ⦄ + core.Shared0Slice.Insts.CoreOpsIndexIndexRangeUsizeSlice.index s r + ⦃ ⇓ r' => ⌜ r'.val = s.val.slice r.start.val r.end.val ∧ + r.start.val + r'.val.length = r.end.val ⌝ ⦄ := by + mvcgen [core.Shared0Slice.Insts.CoreOpsIndexIndexRangeUsizeSlice.index, + rust_primitives.slice.slice_slice, -Slice.subslice_spec.mvcgen_spec, Slice.subslice] + <;> grind + +end CoreModels diff --git a/lean/CoreModels/Spec/RustPrimitives/Arithmetic.lean b/lean/CoreModels/Spec/RustPrimitives/Arithmetic.lean new file mode 100644 index 0000000..dff572e --- /dev/null +++ b/lean/CoreModels/Spec/RustPrimitives/Arithmetic.lean @@ -0,0 +1,25 @@ +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 + +attribute [spec] + rust_primitives.arithmetic.from_le_bytes_u8 + rust_primitives.arithmetic.from_le_bytes_u16 + rust_primitives.arithmetic.from_le_bytes_u32 + rust_primitives.arithmetic.from_le_bytes_u64 + rust_primitives.arithmetic.from_le_bytes_u128 + rust_primitives.arithmetic.from_le_bytes_usize + rust_primitives.arithmetic.to_le_bytes_u8 + rust_primitives.arithmetic.to_le_bytes_u16 + rust_primitives.arithmetic.to_le_bytes_u32 + rust_primitives.arithmetic.to_le_bytes_u64 + rust_primitives.arithmetic.to_le_bytes_u128 + rust_primitives.arithmetic.to_le_bytes_usize + +end CoreModels diff --git a/lean/CoreModels/Spec/RustPrimitives/Slice.lean b/lean/CoreModels/Spec/RustPrimitives/Slice.lean new file mode 100644 index 0000000..68cab0d --- /dev/null +++ b/lean/CoreModels/Spec/RustPrimitives/Slice.lean @@ -0,0 +1,78 @@ +import CoreModels.Core.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 rust_primitives.slice.array_from_fn_go_spec + {T F : Type} + (inst : core.ops.function.FnMut F Std.Usize T) (c : F) (n : Nat) + (hpure : ∀ k, k < n → ∀ c', c' = c → + ⦃ ⌜ True ⌝ ⦄ inst.call_mut c' ⟨BitVec.ofNat _ k⟩ ⦃ ⇓ r => ⌜ r.2 = c ⌝ ⦄) : + ⦃ ⌜ True ⌝ ⦄ + rust_primitives.slice.array_from_fn_go inst c n + ⦃ ⇓ r => ⌜ r.2 = c ∧ ∃ h : r.1.length = n, ∀ i, (hi : i < n) → + ⦃ ⌜ True ⌝ ⦄ inst.call_mut c ⟨BitVec.ofNat _ i⟩ + ⦃ ⇓ r' => ⌜ r.1[i] = r'.1 ⌝ ⦄ ⌝ ⦄ := by + induction n generalizing c with + | zero => + mvcgen [rust_primitives.slice.array_from_fn_go] + refine ⟨trivial, rfl, ?_⟩ + intro i hi; exact absurd hi (by simp) + | succ n ih => + -- Enrich `hpure` mvcgen's VC still contains the fact that the value came from `call_mut`: + have hpure' := fun k hk c' hc' => triple_with_self (hpure k hk c' hc') + mvcgen [rust_primitives.slice.array_from_fn_go, ih, hpure'] + case vc6 => + rename_i r_rec h_rec r_call h_call + obtain ⟨h_receq, h_reclen, h_recpost⟩ := h_rec + obtain ⟨h_call2, h_callself⟩ := h_call + refine ⟨h_call2, by simp [h_reclen], ?_⟩ + intro i hi + rcases Nat.lt_succ_iff_lt_or_eq.mp hi with hlt | heq + · -- `i < n`: the `i`-th element comes from the recursion. + mvcgen [h_recpost] + grind + · -- `i = n`: the last element is `r_call.1`, pinned by `h_callself`. + subst heq + rw [← h_receq] + mvcgen [h_callself] + grind + all_goals grind + +/-- This spec assumes that the closure is not mutated. If the closure was mutated, +we would need a more complex spec that would require the user to provide an invariant. -/ +@[spec] +theorem rust_primitives.slice.array_from_fn_spec + {T F : Type} [Inhabited T] (N : Std.Usize) + (inst : core.ops.function.FnMut F Std.Usize T) (c : F) + (hpure : ∀ k : Nat, k < N.val → + ⦃ ⌜ True ⌝ ⦄ inst.call_mut c ⟨BitVec.ofNat _ k⟩ ⦃ ⇓ r => ⌜ r.2 = c ⌝ ⦄) : + ⦃ ⌜ True ⌝ ⦄ + rust_primitives.slice.array_from_fn N inst c + ⦃ ⇓ a => ⌜ ∀ i : Nat, (hi : i < N.val) → + ⦃ ⌜ True ⌝ ⦄ inst.call_mut c ⟨BitVec.ofNat _ i⟩ + ⦃ ⇓ r => ⌜ r.1 = a.val[i]'(by have := a.property; omega) ⌝ ⦄ ⌝ ⦄ := by + -- We enrich `hpure` by universally quantifying over the `call_mut` argument instead of fixing + -- it to `c`: + have hpure' : ∀ k, k < N.val → ∀ c', c' = c → + ⦃ ⌜ True ⌝ ⦄ inst.call_mut c' ⟨BitVec.ofNat _ k⟩ ⦃ ⇓ r => ⌜ r.2 = c ⌝ ⦄ := + fun k hk c' hc' => hc' ▸ hpure k hk + mvcgen [rust_primitives.slice.array_from_fn, hpure'] + · -- then-branch + rename_i r hlen hconj + obtain ⟨_, _, hpost⟩ := hconj + intro i hi + have hp := hpost i hi + mvcgen [hp] + grind + · -- else-branch is impossible: the worker's length equals `N`. + grind + +end CoreModels From a3963b36b0f8fe5cfad4a0d62bd71d8499cd3b49 Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Wed, 24 Jun 2026 09:52:36 +0200 Subject: [PATCH 2/2] implement clements suggestions --- lean/CoreModels/Spec/Aeneas.lean | 8 ++++---- lean/CoreModels/Spec/RustPrimitives/Slice.lean | 4 ++-- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/lean/CoreModels/Spec/Aeneas.lean b/lean/CoreModels/Spec/Aeneas.lean index bcb7124..abdbc17 100644 --- a/lean/CoreModels/Spec/Aeneas.lean +++ b/lean/CoreModels/Spec/Aeneas.lean @@ -13,8 +13,8 @@ theorem Result.ok_spec {α : Type} {a : α} {Q} (hQ : (Q.1 a).down) : 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 eqivalent to the program being `.ok v`. -/ -theorem triple_of_result_eq {α : Type} {x : Result α} {v : α} : +/-- 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] @@ -34,7 +34,7 @@ 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_of_result_eq.2 hx⟩ + 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) @@ -49,7 +49,7 @@ attribute [spec] Function.uncurry lift massert theorem loop_spec {α β γ : Type} {P : PostCond β (PostShape.except Error (PostShape.except PUnit.{1} PostShape.pure))} - (body : α → Result (ControlFlow α β)) (init : α) + {body : α → Result (ControlFlow α β)} {init : α} (inv : α → Prop) (rel : γ → γ → Prop) (termination : α → γ) diff --git a/lean/CoreModels/Spec/RustPrimitives/Slice.lean b/lean/CoreModels/Spec/RustPrimitives/Slice.lean index 68cab0d..86e719f 100644 --- a/lean/CoreModels/Spec/RustPrimitives/Slice.lean +++ b/lean/CoreModels/Spec/RustPrimitives/Slice.lean @@ -17,9 +17,9 @@ theorem rust_primitives.slice.array_from_fn_go_spec ⦃ ⌜ True ⌝ ⦄ inst.call_mut c' ⟨BitVec.ofNat _ k⟩ ⦃ ⇓ r => ⌜ r.2 = c ⌝ ⦄) : ⦃ ⌜ True ⌝ ⦄ rust_primitives.slice.array_from_fn_go inst c n - ⦃ ⇓ r => ⌜ r.2 = c ∧ ∃ h : r.1.length = n, ∀ i, (hi : i < n) → + ⦃ ⇓ (rl, rc) => ⌜ rc = c ∧ ∃ h : rl.length = n, ∀ i, (hi : i < n) → ⦃ ⌜ True ⌝ ⦄ inst.call_mut c ⟨BitVec.ofNat _ i⟩ - ⦃ ⇓ r' => ⌜ r.1[i] = r'.1 ⌝ ⦄ ⌝ ⦄ := by + ⦃ ⇓ r' => ⌜ rl[i] = r'.1 ⌝ ⦄ ⌝ ⦄ := by induction n generalizing c with | zero => mvcgen [rust_primitives.slice.array_from_fn_go]