diff options
author | Son HO | 2023-08-07 10:42:15 +0200 |
---|---|---|
committer | GitHub | 2023-08-07 10:42:15 +0200 |
commit | 1cbc7ce007cf3433a6df9bdeb12c4e27511fad9c (patch) | |
tree | c15a16b591cf25df3ccff87ad4cd7c46ddecc489 /backends/lean/Base/Primitives/Array.lean | |
parent | 887d0ef1efc8912c6273b5ebcf979384e9d7fa97 (diff) | |
parent | 9e14cdeaf429e9faff2d1efdcf297c1ac7dc7f1f (diff) |
Merge pull request #32 from AeneasVerif/son_arrays
Add support for arrays/slices and const generics
Diffstat (limited to '')
-rw-r--r-- | backends/lean/Base/Primitives/Array.lean | 394 |
1 files changed, 394 insertions, 0 deletions
diff --git a/backends/lean/Base/Primitives/Array.lean b/backends/lean/Base/Primitives/Array.lean new file mode 100644 index 00000000..6c95fd78 --- /dev/null +++ b/backends/lean/Base/Primitives/Array.lean @@ -0,0 +1,394 @@ +/- Arrays/slices -/ +import Lean +import Lean.Meta.Tactic.Simp +import Init.Data.List.Basic +import Mathlib.Tactic.RunCmd +import Mathlib.Tactic.Linarith +import Base.IList +import Base.Primitives.Scalar +import Base.Primitives.Range +import Base.Arith +import Base.Progress.Base + +namespace Primitives + +open Result Error + +def Array (α : Type u) (n : Usize) := { l : List α // l.length = n.val } + +instance (a : Type u) (n : Usize) : Arith.HasIntProp (Array a n) where + prop_ty := λ v => v.val.len = n.val + prop := λ ⟨ _, l ⟩ => by simp[Scalar.max, List.len_eq_length, *] + +instance {α : Type u} {n : Usize} (p : Array α n → Prop) : Arith.HasIntProp (Subtype p) where + prop_ty := λ x => p x + prop := λ x => x.property + +@[simp] +abbrev Array.length {α : Type u} {n : Usize} (v : Array α n) : Int := v.val.len + +@[simp] +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.len = n.val := by decide) : + Array α n := ⟨ init, by simp [← List.len_eq_length]; apply hl ⟩ + +example : Array Int (Usize.ofInt 2) := Array.make Int (Usize.ofInt 2) [0, 1] + +@[simp] +abbrev Array.index {α : Type u} {n : Usize} [Inhabited α] (v : Array α n) (i : Int) : α := + v.val.index i + +@[simp] +abbrev Array.slice {α : Type u} {n : Usize} [Inhabited α] (v : Array α n) (i j : Int) : List α := + v.val.slice i j + +def Array.index_shared (α : Type u) (n : Usize) (v: Array α n) (i: Usize) : Result α := + match v.val.indexOpt i.val with + | none => fail .arrayOutOfBounds + | some x => ret x + +/- In the theorems below: we don't always need the `∃ ..`, but we use one + so that `progress` introduces an opaque variable and an equality. This + helps control the context. + -/ + +@[pspec] +theorem Array.index_shared_spec {α : Type u} {n : Usize} [Inhabited α] (v: Array α n) (i: Usize) + (hbound : i.val < v.length) : + ∃ x, v.index_shared α n i = ret x ∧ x = v.val.index i.val := by + simp only [index_shared] + -- TODO: dependent rewrite + have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*]) + simp [*] + +-- This shouldn't be used +def Array.index_shared_back (α : Type u) (n : Usize) (v: Array α n) (i: Usize) (_: α) : Result Unit := + if i.val < List.length v.val then + .ret () + else + .fail arrayOutOfBounds + +def Array.index_mut (α : Type u) (n : Usize) (v: Array α n) (i: Usize) : Result α := + match v.val.indexOpt i.val with + | none => fail .arrayOutOfBounds + | some x => ret x + +@[pspec] +theorem Array.index_mut_spec {α : Type u} {n : Usize} [Inhabited α] (v: Array α n) (i: Usize) + (hbound : i.val < v.length) : + ∃ x, v.index_mut α n i = ret x ∧ x = v.val.index i.val := by + simp only [index_mut] + -- TODO: dependent rewrite + have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*]) + simp [*] + +def Array.index_mut_back (α : Type u) (n : Usize) (v: Array α n) (i: Usize) (x: α) : Result (Array α n) := + match v.val.indexOpt i.val with + | none => fail .arrayOutOfBounds + | some _ => + .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩ + +@[pspec] +theorem Array.index_mut_back_spec {α : Type u} {n : Usize} (v: Array α n) (i: Usize) (x : α) + (hbound : i.val < v.length) : + ∃ nv, v.index_mut_back α n i x = ret nv ∧ + nv.val = v.val.update i.val x + := by + simp only [index_mut_back] + have h := List.indexOpt_bounds v.val i.val + split + . simp_all [length]; cases h <;> scalar_tac + . simp_all + +def Slice (α : Type u) := { l : List α // l.length ≤ Usize.max } + +instance (a : Type u) : Arith.HasIntProp (Slice a) where + prop_ty := λ v => 0 ≤ v.val.len ∧ v.val.len ≤ Scalar.max ScalarTy.Usize + prop := λ ⟨ _, l ⟩ => by simp[Scalar.max, List.len_eq_length, *] + +instance {α : Type u} (p : Slice α → Prop) : Arith.HasIntProp (Subtype p) where + prop_ty := λ x => p x + prop := λ x => x.property + +@[simp] +abbrev Slice.length {α : Type u} (v : Slice α) : Int := v.val.len + +@[simp] +abbrev Slice.v {α : Type u} (v : Slice α) : List α := v.val + +example {a: Type u} (v : Slice a) : v.length ≤ Scalar.max ScalarTy.Usize := by + scalar_tac + +def Slice.new (α : Type u): Slice α := ⟨ [], by apply Scalar.cMax_suffices .Usize; simp ⟩ + +-- TODO: very annoying that the α is an explicit parameter +def Slice.len (α : Type u) (v : Slice α) : Usize := + Usize.ofIntCore v.val.len (by scalar_tac) (by scalar_tac) + +@[simp] +theorem Slice.len_val {α : Type u} (v : Slice α) : (Slice.len α v).val = v.length := + by rfl + +@[simp] +abbrev Slice.index {α : Type u} [Inhabited α] (v: Slice α) (i: Int) : α := + v.val.index i + +@[simp] +abbrev Slice.slice {α : Type u} [Inhabited α] (s : Slice α) (i j : Int) : List α := + s.val.slice i j + +def Slice.index_shared (α : Type u) (v: Slice α) (i: Usize) : Result α := + match v.val.indexOpt i.val with + | none => fail .arrayOutOfBounds + | some x => ret x + +/- In the theorems below: we don't always need the `∃ ..`, but we use one + so that `progress` introduces an opaque variable and an equality. This + helps control the context. + -/ + +@[pspec] +theorem Slice.index_shared_spec {α : Type u} [Inhabited α] (v: Slice α) (i: Usize) + (hbound : i.val < v.length) : + ∃ x, v.index_shared α i = ret x ∧ x = v.val.index i.val := by + simp only [index_shared] + -- TODO: dependent rewrite + have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*]) + simp [*] + +-- This shouldn't be used +def Slice.index_shared_back (α : Type u) (v: Slice α) (i: Usize) (_: α) : Result Unit := + if i.val < List.length v.val then + .ret () + else + .fail arrayOutOfBounds + +def Slice.index_mut (α : Type u) (v: Slice α) (i: Usize) : Result α := + match v.val.indexOpt i.val with + | none => fail .arrayOutOfBounds + | some x => ret x + +@[pspec] +theorem Slice.index_mut_spec {α : Type u} [Inhabited α] (v: Slice α) (i: Usize) + (hbound : i.val < v.length) : + ∃ x, v.index_mut α i = ret x ∧ x = v.val.index i.val := by + simp only [index_mut] + -- TODO: dependent rewrite + have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*]) + simp [*] + +def Slice.index_mut_back (α : Type u) (v: Slice α) (i: Usize) (x: α) : Result (Slice α) := + match v.val.indexOpt i.val with + | none => fail .arrayOutOfBounds + | some _ => + .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩ + +@[pspec] +theorem Slice.index_mut_back_spec {α : Type u} (v: Slice α) (i: Usize) (x : α) + (hbound : i.val < v.length) : + ∃ nv, v.index_mut_back α i x = ret nv ∧ + nv.val = v.val.update i.val x + := by + simp only [index_mut_back] + have h := List.indexOpt_bounds v.val i.val + split + . simp_all [length]; cases h <;> scalar_tac + . simp_all + +/- Array to slice/subslices -/ + +/- We could make this function not use the `Result` type. By making it monadic, we + push the user to use the `Array.to_slice_shared_spec` spec theorem below (through the + `progress` tactic), meaning `Array.to_slice_shared` should be considered as opaque. + All what the spec theorem reveals is that the "representative" lists are the same. -/ +def Array.to_slice_shared (α : Type u) (n : Usize) (v : Array α n) : Result (Slice α) := + ret ⟨ v.val, by simp [← List.len_eq_length]; scalar_tac ⟩ + +@[pspec] +theorem Array.to_slice_shared_spec {α : Type u} {n : Usize} (v : Array α n) : + ∃ s, to_slice_shared α n v = ret s ∧ v.val = s.val := by simp [to_slice_shared] + +def Array.to_slice_mut (α : Type u) (n : Usize) (v : Array α n) : Result (Slice α) := + to_slice_shared α n v + +@[pspec] +theorem Array.to_slice_mut_spec {α : Type u} {n : Usize} (v : Array α n) : + ∃ s, Array.to_slice_shared α n v = ret s ∧ v.val = s.val := to_slice_shared_spec v + +def Array.to_slice_mut_back (α : Type u) (n : Usize) (_ : Array α n) (s : Slice α) : Result (Array α n) := + if h: s.val.len = n.val then + ret ⟨ s.val, by simp [← List.len_eq_length, *] ⟩ + else fail panic + +@[pspec] +theorem Array.to_slice_mut_back_spec {α : Type u} {n : Usize} (a : Array α n) (ns : Slice α) (h : ns.val.len = n.val) : + ∃ na, to_slice_mut_back α n a ns = ret na ∧ na.val = ns.val + := by simp [to_slice_mut_back, *] + +def Array.subslice_shared (α : Type u) (n : Usize) (a : Array α n) (r : Range Usize) : Result (Slice α) := + -- TODO: not completely sure here + if r.start.val < r.end_.val ∧ r.end_.val ≤ a.val.len then + ret ⟨ a.val.slice r.start.val r.end_.val, + by + simp [← List.len_eq_length] + have := a.val.slice_len_le r.start.val r.end_.val + scalar_tac ⟩ + else + fail panic + +@[pspec] +theorem Array.subslice_shared_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize) + (h0 : r.start.val < r.end_.val) (h1 : r.end_.val ≤ a.val.len) : + ∃ s, subslice_shared α n a r = ret s ∧ + s.val = a.val.slice r.start.val r.end_.val ∧ + (∀ i, 0 ≤ i → i + r.start.val < r.end_.val → s.val.index i = a.val.index (r.start.val + i)) + := by + simp [subslice_shared, *] + intro i _ _ + have := List.index_slice r.start.val r.end_.val i a.val (by scalar_tac) (by scalar_tac) (by trivial) (by scalar_tac) + simp [*] + +def Array.subslice_mut (α : Type u) (n : Usize) (a : Array α n) (r : Range Usize) : Result (Slice α) := + Array.subslice_shared α n a r + +@[pspec] +theorem Array.subslice_mut_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize) + (h0 : r.start.val < r.end_.val) (h1 : r.end_.val ≤ a.val.len) : + ∃ s, subslice_mut α n a r = ret s ∧ + s.val = a.slice r.start.val r.end_.val ∧ + (∀ i, 0 ≤ i → i + r.start.val < r.end_.val → s.val.index i = a.val.index (r.start.val + i)) + := subslice_shared_spec a r h0 h1 + +def Array.subslice_mut_back (α : Type u) (n : Usize) (a : Array α n) (r : Range Usize) (s : Slice α) : Result (Array α n) := + -- TODO: not completely sure here + if h: r.start.val < r.end_.val ∧ r.end_.val ≤ a.length ∧ s.val.len = r.end_.val - r.start.val then + let s_beg := a.val.itake r.start.val + let s_end := a.val.idrop r.end_.val + have : s_beg.len = r.start.val := by + apply List.itake_len + . simp_all; scalar_tac + . scalar_tac + have : s_end.len = a.val.len - r.end_.val := by + apply List.idrop_len + . scalar_tac + . scalar_tac + let na := s_beg.append (s.val.append s_end) + have : na.len = a.val.len := by simp [*] + ret ⟨ na, by simp_all [← List.len_eq_length]; scalar_tac ⟩ + else + fail panic + +-- TODO: it is annoying to write `.val` everywhere. We could leverage coercions, +-- but: some symbols like `+` are already overloaded to be notations for monadic +-- operations/ +-- We should introduce special symbols for the monadic arithmetic operations +-- (the use will never write those symbols directly). +@[pspec] +theorem Array.subslice_mut_back_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize) (s : Slice α) + (_ : r.start.val < r.end_.val) (_ : r.end_.val ≤ a.length) (_ : s.length = r.end_.val - r.start.val) : + ∃ na, subslice_mut_back α n a r s = ret na ∧ + (∀ i, 0 ≤ i → i < r.start.val → na.index i = a.index i) ∧ + (∀ i, r.start.val ≤ i → i < r.end_.val → na.index i = s.index (i - r.start.val)) ∧ + (∀ i, r.end_.val ≤ i → i < n.val → na.index i = a.index i) := by + simp [subslice_mut_back, *] + have h := List.replace_slice_index r.start.val r.end_.val a.val s.val + (by scalar_tac) (by scalar_tac) (by scalar_tac) (by scalar_tac) + simp [List.replace_slice] at h + have ⟨ h0, h1, h2 ⟩ := h + clear h + split_conjs + . intro i _ _ + have := h0 i (by int_tac) (by int_tac) + simp [*] + . intro i _ _ + have := h1 i (by int_tac) (by int_tac) + simp [*] + . intro i _ _ + have := h2 i (by int_tac) (by int_tac) + simp [*] + +def Slice.subslice_shared (α : Type u) (s : Slice α) (r : Range Usize) : Result (Slice α) := + -- TODO: not completely sure here + if r.start.val < r.end_.val ∧ r.end_.val ≤ s.length then + ret ⟨ s.val.slice r.start.val r.end_.val, + by + simp [← List.len_eq_length] + have := s.val.slice_len_le r.start.val r.end_.val + scalar_tac ⟩ + else + fail panic + +@[pspec] +theorem Slice.subslice_shared_spec {α : Type u} [Inhabited α] (s : Slice α) (r : Range Usize) + (h0 : r.start.val < r.end_.val) (h1 : r.end_.val ≤ s.val.len) : + ∃ ns, subslice_shared α s r = ret ns ∧ + ns.val = s.slice r.start.val r.end_.val ∧ + (∀ i, 0 ≤ i → i + r.start.val < r.end_.val → ns.index i = s.index (r.start.val + i)) + := by + simp [subslice_shared, *] + intro i _ _ + have := List.index_slice r.start.val r.end_.val i s.val (by scalar_tac) (by scalar_tac) (by trivial) (by scalar_tac) + simp [*] + +def Slice.subslice_mut (α : Type u) (s : Slice α) (r : Range Usize) : Result (Slice α) := + Slice.subslice_shared α s r + +@[pspec] +theorem Slice.subslice_mut_spec {α : Type u} [Inhabited α] (s : Slice α) (r : Range Usize) + (h0 : r.start.val < r.end_.val) (h1 : r.end_.val ≤ s.val.len) : + ∃ ns, subslice_mut α s r = ret ns ∧ + ns.val = s.slice r.start.val r.end_.val ∧ + (∀ i, 0 ≤ i → i + r.start.val < r.end_.val → ns.index i = s.index (r.start.val + i)) + := subslice_shared_spec s r h0 h1 + +attribute [pp_dot] List.len List.length List.index -- use the dot notation when printing +set_option pp.coercions false -- do not print coercions with ↑ (this doesn't parse) + +def Slice.subslice_mut_back (α : Type u) (s : Slice α) (r : Range Usize) (ss : Slice α) : Result (Slice α) := + -- TODO: not completely sure here + if h: r.start.val < r.end_.val ∧ r.end_.val ≤ s.length ∧ ss.val.len = r.end_.val - r.start.val then + let s_beg := s.val.itake r.start.val + let s_end := s.val.idrop r.end_.val + have : s_beg.len = r.start.val := by + apply List.itake_len + . simp_all; scalar_tac + . scalar_tac + have : s_end.len = s.val.len - r.end_.val := by + apply List.idrop_len + . scalar_tac + . scalar_tac + let ns := s_beg.append (ss.val.append s_end) + have : ns.len = s.val.len := by simp [*] + ret ⟨ ns, by simp_all [← List.len_eq_length]; scalar_tac ⟩ + else + fail panic + +@[pspec] +theorem Slice.subslice_mut_back_spec {α : Type u} [Inhabited α] (a : Slice α) (r : Range Usize) (ss : Slice α) + (_ : r.start.val < r.end_.val) (_ : r.end_.val ≤ a.length) (_ : ss.length = r.end_.val - r.start.val) : + ∃ na, subslice_mut_back α a r ss = ret na ∧ + (∀ i, 0 ≤ i → i < r.start.val → na.index i = a.index i) ∧ + (∀ i, r.start.val ≤ i → i < r.end_.val → na.index i = ss.index (i - r.start.val)) ∧ + (∀ i, r.end_.val ≤ i → i < a.length → na.index i = a.index i) := by + simp [subslice_mut_back, *] + have h := List.replace_slice_index r.start.val r.end_.val a.val ss.val + (by scalar_tac) (by scalar_tac) (by scalar_tac) (by scalar_tac) + simp [List.replace_slice, *] at h + have ⟨ h0, h1, h2 ⟩ := h + clear h + split_conjs + . intro i _ _ + have := h0 i (by int_tac) (by int_tac) + simp [*] + . intro i _ _ + have := h1 i (by int_tac) (by int_tac) + simp [*] + . intro i _ _ + have := h2 i (by int_tac) (by int_tac) + simp [*] + +end Primitives |