Skip to content

Commit 2ee2b9c

Browse files
abentkampabentkamp
committed
wip
1 parent 938a821 commit 2ee2b9c

5 files changed

Lines changed: 531 additions & 3 deletions

File tree

‎lean/CoreModels.lean‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,5 +3,4 @@ import CoreModels.Core
33
import CoreModels.Alloc
44
import CoreModels.HaxLib
55
import CoreModels.RustPrimitives
6-
import CoreModels.FunsEpilogue
76
import CoreModels.Spec

‎lean/CoreModels/Spec/Aeneas.lean‎

Lines changed: 28 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
import CoreModels.Funs
1+
import CoreModels.Core.Funs
22

33
namespace Aeneas.Std
44
open Std.Do WP Std.Do Result
@@ -79,4 +79,31 @@ theorem loop_spec
7979
| fail e => rw [hbe] at hb; exact hb
8080
| div => rw [hbe] at hb; exact hb
8181

82+
open ScalarElab
83+
84+
iscalar_no_isize @[spec] theorem «%S».hShiftRight_I8_spec (a : «%S») (b : I8) (hmin : b.val ≥ 0) (hmax : b.val < %Size) :
85+
⦃ ⌜ True ⌝ ⦄ (a >>> b) ⦃ ⇓ r => ⌜ r.val = a.val / (2 ^ b.val.toNat) ⌝ ⦄ := by
86+
mvcgen [HShiftRight.hShiftRight, IScalar.shiftRight_IScalar, IScalar.shiftRight]
87+
<;> grind [IScalar.val, Int.shiftRight_eq_div_pow]
88+
89+
iscalar_no_isize @[spec] theorem «%S».hShiftRight_I16_spec (a : «%S») (b : I16) (hmin : b.val ≥ 0) (hmax : b.val < %Size) :
90+
⦃ ⌜ True ⌝ ⦄ (a >>> b) ⦃ ⇓ r => ⌜ r.val = a.val / (2 ^ b.val.toNat) ⌝ ⦄ := by
91+
mvcgen [HShiftRight.hShiftRight, IScalar.shiftRight_IScalar, IScalar.shiftRight]
92+
<;> grind [IScalar.val, Int.shiftRight_eq_div_pow]
93+
94+
iscalar_no_isize @[spec] theorem «%S».hShiftRight_I32_spec (a : «%S») (b : I32) (hmin : b.val ≥ 0) (hmax : b.val < %Size) :
95+
⦃ ⌜ True ⌝ ⦄ (a >>> b) ⦃ ⇓ r => ⌜ r.val = a.val / (2 ^ b.val.toNat) ⌝ ⦄ := by
96+
mvcgen [HShiftRight.hShiftRight, IScalar.shiftRight_IScalar, IScalar.shiftRight]
97+
<;> grind [IScalar.val, Int.shiftRight_eq_div_pow]
98+
99+
iscalar_no_isize @[spec] theorem «%S».hShiftRight_I64_spec (a : «%S») (b : I64) (hmin : b.val ≥ 0) (hmax : b.val < %Size) :
100+
⦃ ⌜ True ⌝ ⦄ (a >>> b) ⦃ ⇓ r => ⌜ r.val = a.val / (2 ^ b.val.toNat) ⌝ ⦄ := by
101+
mvcgen [HShiftRight.hShiftRight, IScalar.shiftRight_IScalar, IScalar.shiftRight]
102+
<;> grind [IScalar.val, Int.shiftRight_eq_div_pow]
103+
104+
iscalar_no_isize @[spec] theorem «%S».hShiftRight_I128_spec (a : «%S») (b : I128) (hmin : b.val ≥ 0) (hmax : b.val < %Size) :
105+
⦃ ⌜ True ⌝ ⦄ (a >>> b) ⦃ ⇓ r => ⌜ r.val = a.val / (2 ^ b.val.toNat) ⌝ ⦄ := by
106+
mvcgen [HShiftRight.hShiftRight, IScalar.shiftRight_IScalar, IScalar.shiftRight]
107+
<;> grind [IScalar.val, Int.shiftRight_eq_div_pow]
108+
82109
end Aeneas.Std

‎lean/CoreModels/Spec/Array.lean‎

Lines changed: 76 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
import CoreModels.Funs
1+
import CoreModels.Core.Funs
22
import CoreModels.Spec.Aeneas
33

44
namespace CoreModels
@@ -34,3 +34,78 @@ uscalar @[spec] theorem «%S».Core_modelsCmpPartialEqArray.eq_spec {N : Std.Usi
3434
· convert h; grind
3535

3636
end CoreModels
37+
38+
39+
40+
/-! ### Helper Triple: Array index by `Range Usize`.
41+
42+
Array variant of `core_models_Slice_Insts_index_RangeUsize_spec`
43+
(SliceSpecs.lean). The Array index reduces to the Slice index via
44+
`Array.to_slice`. -/
45+
46+
@[spec]
47+
theorem core_models_Array_Insts_index_RangeUsize_spec
48+
{T : Type} {N : Std.Usize} (arr : Std.Array T N)
49+
(r : CoreModels.core.ops.range.Range Std.Usize)
50+
(h0 : r.start.val ≤ r.end.val) (h1 : r.end.val ≤ N.val) :
51+
⦃ ⌜ True ⌝ ⦄
52+
CoreModels.core.Array.Insts.CoreOpsIndexIndex.index
53+
(CoreModels.core.ops.range.RangeUsize.Insts.CoreSliceIndexSliceIndexSliceSlice T) arr r
54+
⦃ ⇓ r' => ⌜ r'.val = arr.val.slice r.start.val r.end.val ∧
55+
r'.val.length = r.end.val - r.start.val ⌝ ⦄ := by
56+
-- Reduce to the slice version via `Array.to_slice`.
57+
unfold CoreModels.core.Array.Insts.CoreOpsIndexIndex.index
58+
-- Body: `core.slice.index.Slice.index inst (Array.to_slice arr) i`.
59+
have h1' : r.end.val ≤ (Std.Array.to_slice arr).val.length := by
60+
rw [Std.Array.val_to_slice]
61+
have : arr.val.length = N.val := arr.property
62+
omega
63+
have h_slice_val : (Std.Array.to_slice arr).val = arr.val :=
64+
Std.Array.val_to_slice arr
65+
-- Use the existing slice spec.
66+
have h_slice :=
67+
core_models_Slice_Insts_index_RangeUsize_spec (Std.Array.to_slice arr) r h0 h1'
68+
-- The slice version uses `CoreModels.core.Slice.Insts.CoreOpsIndexIndex.index`,
69+
-- which unfolds to the same `core.slice.index.Slice.index` we need here.
70+
-- Convert the slice spec's post (in terms of `arr.to_slice.val`) into one
71+
-- in terms of `arr.val`.
72+
obtain ⟨v, hv_eq, hv_val, hv_len⟩ := triple_exists_ok_sb h_slice
73+
refine triple_of_ok_sb (v := v) ?_ ?_
74+
· -- Equality: `core.slice.index.Slice.index inst (Array.to_slice arr) r = .ok v`.
75+
have := hv_eq
76+
unfold CoreModels.core.Slice.Insts.CoreOpsIndexIndex.index at this
77+
exact this
78+
· refine ⟨?_, ?_⟩
79+
· rw [hv_val, h_slice_val]
80+
· rw [hv_len]
81+
82+
83+
/-- **Generic pure-closure `[spec]` for `core_models.array.from_fn`.**
84+
85+
For any closure whose `call_mut` is pure (doesn't mutate state),
86+
`from_fn N inst c` succeeds and its `i`-th cell is `f i`. `hpure` is a
87+
Triple over each `call_mut` so `hax_mvcgen` can recurse through it via
88+
per-closure `@[spec]` lemmas. -/
89+
@[spec]
90+
theorem from_fn_pure_spec
91+
{T F : Type} [Inhabited T] (N : Std.Usize)
92+
(inst : core_models.ops.function.FnMut F Std.Usize T) (c : F) (f : Nat → T)
93+
(hpure : ∀ k : Nat, k < N.val →
94+
⦃ ⌜ True ⌝ ⦄
95+
inst.call_mut c ⟨BitVec.ofNat _ k⟩
96+
⦃ ⇓ r => ⌜ r = (f k, c) ⌝ ⦄) :
97+
⦃ ⌜ True ⌝ ⦄
98+
core_models.array.from_fn N inst c
99+
⦃ ⇓ a => ⌜ ∀ i : Nat, i < N.val → a.val[i]! = f i ⌝ ⦄ := by
100+
have hpure_eq : ∀ k : Nat, k < N.val →
101+
inst.call_mut c ⟨BitVec.ofNat _ k⟩ = .ok (f k, c) :=
102+
fun k hk => result_eq_of_triple (hpure k hk)
103+
have heq := from_fn_pure_eq N inst c f hpure_eq
104+
rw [heq]
105+
simp only [Triple, WP.wp]
106+
apply SPred.pure_intro
107+
intro i hi
108+
show ((List.range N.val).map f)[i]! = f i
109+
rw [List.getElem!_eq_getElem?_getD, List.getElem?_map,
110+
List.getElem?_range hi]
111+
rfl

‎lean/CoreModels/Spec/Iterator.lean‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
import CoreModels.Core.Funs
2+
import CoreModels.Alloc.Funs
3+
import CoreModels.Spec.Aeneas
4+
5+
namespace CoreModels
6+
7+
open Aeneas
8+
open Aeneas.Std hiding namespace core alloc
9+
open Std.Do WP Std.Do Result
10+
11+
set_option mvcgen.warning false
12+
13+
@[spec]
14+
theorem IteratorRange_next_CoreIterRangeStep_spec (i e : Usize) {Q}
15+
(h_lt : (h : i.val < e.val) →
16+
∀ (s : Usize), s.val = i.val + 1 → (Q.1 (some i, { start := s, «end» := e })).down)
17+
(h_ge : i.val ≥ e.val → (Q.1 (none, { start := i, «end» := e })).down) :
18+
⦃ ⌜ True ⌝ ⦄
19+
core.IteratorRange.next core.Usize.Insts.CoreIterRangeStep
20+
{ start := i, «end» := e }
21+
⦃ Q ⦄ := by
22+
unfold core.IteratorRange.next core.Usize.Insts.CoreIterRangeStep
23+
simp only [core.Usize.Insts.CoreCmpPartialOrdUsize, core.mkUPartialOrd,
24+
core.Usize.Insts.CoreCloneClone.clone, core.Usize.Insts.CoreIterRangeStep.forward_checked,
25+
core.convert.TryFromUTInfallible.Blanket.try_from, core.convert.From.Blanket.from,
26+
core.num.Usize.checked_add, core.num.Usize.overflowing_add,
27+
rust_primitives.arithmetic.overflowing_add_usize]
28+
mvcgen [uncurry]
29+
<;> grind [UScalar.overflowing_add, BitVec.uaddOverflow, UScalar.overflowing_add_eq]

0 commit comments

Comments
 (0)