diff options
Diffstat (limited to 'backends')
| -rw-r--r-- | backends/coq/Primitives.v | 427 | ||||
| -rw-r--r-- | backends/fstar/Primitives.fst | 464 | ||||
| -rw-r--r-- | backends/hol4/primitivesScript.sml | 26 | ||||
| -rw-r--r-- | backends/hol4/primitivesTheory.sig | 120 | ||||
| -rw-r--r-- | backends/lean/Base/Arith/Base.lean | 12 | ||||
| -rw-r--r-- | backends/lean/Base/Arith/Int.lean | 15 | ||||
| -rw-r--r-- | backends/lean/Base/Arith/Scalar.lean | 13 | ||||
| -rw-r--r-- | backends/lean/Base/IList/IList.lean | 39 | ||||
| -rw-r--r-- | backends/lean/Base/Primitives.lean | 4 | ||||
| -rw-r--r-- | backends/lean/Base/Primitives/Alloc.lean | 37 | ||||
| -rw-r--r-- | backends/lean/Base/Primitives/Array.lean | 394 | ||||
| -rw-r--r-- | backends/lean/Base/Primitives/ArraySlice.lean | 552 | ||||
| -rw-r--r-- | backends/lean/Base/Primitives/Base.lean | 11 | ||||
| -rw-r--r-- | backends/lean/Base/Primitives/CoreOps.lean | 37 | ||||
| -rw-r--r-- | backends/lean/Base/Primitives/Range.lean | 2 | ||||
| -rw-r--r-- | backends/lean/Base/Primitives/Scalar.lean | 127 | ||||
| -rw-r--r-- | backends/lean/Base/Primitives/Vec.lean | 94 | ||||
| -rw-r--r-- | backends/lean/Base/Progress/Progress.lean | 29 | ||||
| -rw-r--r-- | backends/lean/Base/Utils.lean | 75 |
19 files changed, 1893 insertions, 585 deletions
diff --git a/backends/coq/Primitives.v b/backends/coq/Primitives.v index 71a2d9c3..83f860b6 100644 --- a/backends/coq/Primitives.v +++ b/backends/coq/Primitives.v @@ -63,13 +63,15 @@ Check (if true then Return (1 + 2) else Fail_ Failure)%global = 3. (*** Misc *) - Definition string := Coq.Strings.String.string. Definition char := Coq.Strings.Ascii.ascii. Definition char_of_byte := Coq.Strings.Ascii.ascii_of_byte. -Definition mem_replace_fwd (a : Type) (x : a) (y : a) : a := x . -Definition mem_replace_back (a : Type) (x : a) (y : a) : a := y . +Definition core_mem_replace (a : Type) (x : a) (y : a) : a := x . +Definition core_mem_replace_back (a : Type) (x : a) (y : a) : a := y . + +Record mut_raw_ptr (T : Type) := { mut_raw_ptr_v : T }. +Record const_raw_ptr (T : Type) := { const_raw_ptr_v : T }. (*** Scalars *) @@ -394,12 +396,89 @@ Notation "x s< y" := (scalar_ltb x y) (at level 80) : Primitives_scope. Notation "x s>= y" := (scalar_geb x y) (at level 80) : Primitives_scope. Notation "x s> y" := (scalar_gtb x y) (at level 80) : Primitives_scope. -(*** Range *) -Record range (T : Type) := mk_range { - start: T; - end_: T; +(** Constants *) +Definition core_u8_max := u8_max %u32. +Definition core_u16_max := u16_max %u32. +Definition core_u32_max := u32_max %u32. +Definition core_u64_max := u64_max %u64. +Definition core_u128_max := u64_max %u128. +Axiom core_usize_max : usize. (** TODO *) +Definition core_i8_max := i8_max %i32. +Definition core_i16_max := i16_max %i32. +Definition core_i32_max := i32_max %i32. +Definition core_i64_max := i64_max %i64. +Definition core_i128_max := i64_max %i128. +Axiom core_isize_max : isize. (** TODO *) + +(*** core::ops *) + +(* Trait declaration: [core::ops::index::Index] *) +Record core_ops_index_Index (Self Idx : Type) := mk_core_ops_index_Index { + core_ops_index_Index_Output : Type; + core_ops_index_Index_index : Self -> Idx -> result core_ops_index_Index_Output; +}. +Arguments mk_core_ops_index_Index {_ _}. +Arguments core_ops_index_Index_Output {_ _}. +Arguments core_ops_index_Index_index {_ _}. + +(* Trait declaration: [core::ops::index::IndexMut] *) +Record core_ops_index_IndexMut (Self Idx : Type) := mk_core_ops_index_IndexMut { + core_ops_index_IndexMut_indexInst : core_ops_index_Index Self Idx; + core_ops_index_IndexMut_index_mut : Self -> Idx -> result core_ops_index_IndexMut_indexInst.(core_ops_index_Index_Output); + core_ops_index_IndexMut_index_mut_back : Self -> Idx -> core_ops_index_IndexMut_indexInst.(core_ops_index_Index_Output) -> result Self; +}. +Arguments mk_core_ops_index_IndexMut {_ _}. +Arguments core_ops_index_IndexMut_indexInst {_ _}. +Arguments core_ops_index_IndexMut_index_mut {_ _}. +Arguments core_ops_index_IndexMut_index_mut_back {_ _}. + +(* Trait declaration [core::ops::deref::Deref] *) +Record core_ops_deref_Deref (Self : Type) := mk_core_ops_deref_Deref { + core_ops_deref_Deref_target : Type; + core_ops_deref_Deref_deref : Self -> result core_ops_deref_Deref_target; +}. +Arguments mk_core_ops_deref_Deref {_}. +Arguments core_ops_deref_Deref_target {_}. +Arguments core_ops_deref_Deref_deref {_}. + +(* Trait declaration [core::ops::deref::DerefMut] *) +Record core_ops_deref_DerefMut (Self : Type) := mk_core_ops_deref_DerefMut { + core_ops_deref_DerefMut_derefInst : core_ops_deref_Deref Self; + core_ops_deref_DerefMut_deref_mut : Self -> result core_ops_deref_DerefMut_derefInst.(core_ops_deref_Deref_target); + core_ops_deref_DerefMut_deref_mut_back : Self -> core_ops_deref_DerefMut_derefInst.(core_ops_deref_Deref_target) -> result Self; }. -Arguments mk_range {_}. +Arguments mk_core_ops_deref_DerefMut {_}. +Arguments core_ops_deref_DerefMut_derefInst {_}. +Arguments core_ops_deref_DerefMut_deref_mut {_}. +Arguments core_ops_deref_DerefMut_deref_mut_back {_}. + +Record core_ops_range_Range (T : Type) := mk_core_ops_range_Range { + core_ops_range_Range_start : T; + core_ops_range_Range_end_ : T; +}. +Arguments mk_core_ops_range_Range {_}. +Arguments core_ops_range_Range_start {_}. +Arguments core_ops_range_Range_end_ {_}. + +(*** [alloc] *) + +Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Return x. +Definition alloc_boxed_Box_deref_mut (T : Type) (x : T) : result T := Return x. +Definition alloc_boxed_Box_deref_mut_back (T : Type) (_ : T) (x : T) : result T := Return x. + +(* Trait instance *) +Definition alloc_boxed_Box_coreopsDerefInst (Self : Type) : core_ops_deref_Deref Self := {| + core_ops_deref_Deref_target := Self; + core_ops_deref_Deref_deref := alloc_boxed_Box_deref Self; +|}. + +(* Trait instance *) +Definition alloc_boxed_Box_coreopsDerefMutInst (Self : Type) : core_ops_deref_DerefMut Self := {| + core_ops_deref_DerefMut_derefInst := alloc_boxed_Box_coreopsDerefInst Self; + core_ops_deref_DerefMut_deref_mut := alloc_boxed_Box_deref_mut Self; + core_ops_deref_DerefMut_deref_mut_back := alloc_boxed_Box_deref_mut_back Self; +|}. + (*** Arrays *) Definition array T (n : usize) := { l: list T | Z.of_nat (length l) = to_Z n}. @@ -419,51 +498,50 @@ Qed. (* TODO: finish the definitions *) Axiom mk_array : forall (T : Type) (n : usize) (l : list T), array T n. -Axiom array_index_shared : forall (T : Type) (n : usize) (x : array T n) (i : usize), result T. -Axiom array_index_mut_fwd : forall (T : Type) (n : usize) (x : array T n) (i : usize), result T. -Axiom array_index_mut_back : forall (T : Type) (n : usize) (x : array T n) (i : usize) (nx : T), result (array T n). +(* For initialization *) +Axiom array_repeat : forall (T : Type) (n : usize) (x : T), array T n. + +Axiom array_index_usize : forall (T : Type) (n : usize) (x : array T n) (i : usize), result T. +Axiom array_update_usize : forall (T : Type) (n : usize) (x : array T n) (i : usize) (nx : T), result (array T n). (*** Slice *) Definition slice T := { l: list T | Z.of_nat (length l) <= usize_max}. Axiom slice_len : forall (T : Type) (s : slice T), usize. -Axiom slice_index_shared : forall (T : Type) (x : slice T) (i : usize), result T. -Axiom slice_index_mut_fwd : forall (T : Type) (x : slice T) (i : usize), result T. -Axiom slice_index_mut_back : forall (T : Type) (x : slice T) (i : usize) (nx : T), result (slice T). +Axiom slice_index_usize : forall (T : Type) (x : slice T) (i : usize), result T. +Axiom slice_update_usize : forall (T : Type) (x : slice T) (i : usize) (nx : T), result (slice T). (*** Subslices *) -Axiom array_to_slice_shared : forall (T : Type) (n : usize) (x : array T n), result (slice T). -Axiom array_to_slice_mut_fwd : forall (T : Type) (n : usize) (x : array T n), result (slice T). -Axiom array_to_slice_mut_back : forall (T : Type) (n : usize) (x : array T n) (s : slice T), result (array T n). +Axiom array_to_slice : forall (T : Type) (n : usize) (x : array T n), result (slice T). +Axiom array_from_slice : forall (T : Type) (n : usize) (x : array T n) (s : slice T), result (array T n). + +Axiom array_subslice: forall (T : Type) (n : usize) (x : array T n) (r : core_ops_range_Range usize), result (slice T). +Axiom array_update_subslice: forall (T : Type) (n : usize) (x : array T n) (r : core_ops_range_Range usize) (ns : slice T), result (array T n). -Axiom array_subslice_shared: forall (T : Type) (n : usize) (x : array T n) (r : range usize), result (slice T). -Axiom array_subslice_mut_fwd: forall (T : Type) (n : usize) (x : array T n) (r : range usize), result (slice T). -Axiom array_subslice_mut_back: forall (T : Type) (n : usize) (x : array T n) (r : range usize) (ns : slice T), result (array T n). -Axiom slice_subslice_shared: forall (T : Type) (x : slice T) (r : range usize), result (slice T). -Axiom slice_subslice_mut_fwd: forall (T : Type) (x : slice T) (r : range usize), result (slice T). -Axiom slice_subslice_mut_back: forall (T : Type) (x : slice T) (r : range usize) (ns : slice T), result (slice T). +Axiom slice_subslice: forall (T : Type) (x : slice T) (r : core_ops_range_Range usize), result (slice T). +Axiom slice_update_subslice: forall (T : Type) (x : slice T) (r : core_ops_range_Range usize) (ns : slice T), result (slice T). (*** Vectors *) -Definition vec T := { l: list T | Z.of_nat (length l) <= usize_max }. +Definition alloc_vec_Vec T := { l: list T | Z.of_nat (length l) <= usize_max }. -Definition vec_to_list {T: Type} (v: vec T) : list T := proj1_sig v. +Definition alloc_vec_Vec_to_list {T: Type} (v: alloc_vec_Vec T) : list T := proj1_sig v. -Definition vec_length {T: Type} (v: vec T) : Z := Z.of_nat (length (vec_to_list v)). +Definition alloc_vec_Vec_length {T: Type} (v: alloc_vec_Vec T) : Z := Z.of_nat (length (alloc_vec_Vec_to_list v)). -Definition vec_new (T: Type) : vec T := (exist _ [] le_0_usize_max). +Definition alloc_vec_Vec_new (T: Type) : alloc_vec_Vec T := (exist _ [] le_0_usize_max). -Lemma vec_len_in_usize {T} (v: vec T) : usize_min <= vec_length v <= usize_max. +Lemma alloc_vec_Vec_len_in_usize {T} (v: alloc_vec_Vec T) : usize_min <= alloc_vec_Vec_length v <= usize_max. Proof. - unfold vec_length, usize_min. + unfold alloc_vec_Vec_length, usize_min. split. - lia. - apply (proj2_sig v). Qed. -Definition vec_len (T: Type) (v: vec T) : usize := - exist _ (vec_length v) (vec_len_in_usize v). +Definition alloc_vec_Vec_len (T: Type) (v: alloc_vec_Vec T) : usize := + exist _ (alloc_vec_Vec_length v) (alloc_vec_Vec_len_in_usize v). Fixpoint list_update {A} (l: list A) (n: nat) (a: A) : list A := @@ -474,50 +552,279 @@ Fixpoint list_update {A} (l: list A) (n: nat) (a: A) | S m => x :: (list_update t m a) end end. -Definition vec_bind {A B} (v: vec A) (f: list A -> result (list B)) : result (vec B) := - l <- f (vec_to_list v) ; +Definition alloc_vec_Vec_bind {A B} (v: alloc_vec_Vec A) (f: list A -> result (list B)) : result (alloc_vec_Vec B) := + l <- f (alloc_vec_Vec_to_list v) ; match sumbool_of_bool (scalar_le_max Usize (Z.of_nat (length l))) with | left H => Return (exist _ l (scalar_le_max_valid _ _ H)) | right _ => Fail_ Failure end. (* The **forward** function shouldn't be used *) -Definition vec_push_fwd (T: Type) (v: vec T) (x: T) : unit := tt. +Definition alloc_vec_Vec_push_fwd (T: Type) (v: alloc_vec_Vec T) (x: T) : unit := tt. -Definition vec_push_back (T: Type) (v: vec T) (x: T) : result (vec T) := - vec_bind v (fun l => Return (l ++ [x])). +Definition alloc_vec_Vec_push (T: Type) (v: alloc_vec_Vec T) (x: T) : result (alloc_vec_Vec T) := + alloc_vec_Vec_bind v (fun l => Return (l ++ [x])). (* The **forward** function shouldn't be used *) -Definition vec_insert_fwd (T: Type) (v: vec T) (i: usize) (x: T) : result unit := - if to_Z i <? vec_length v then Return tt else Fail_ Failure. +Definition alloc_vec_Vec_insert_fwd (T: Type) (v: alloc_vec_Vec T) (i: usize) (x: T) : result unit := + if to_Z i <? alloc_vec_Vec_length v then Return tt else Fail_ Failure. -Definition vec_insert_back (T: Type) (v: vec T) (i: usize) (x: T) : result (vec T) := - vec_bind v (fun l => +Definition alloc_vec_Vec_insert (T: Type) (v: alloc_vec_Vec T) (i: usize) (x: T) : result (alloc_vec_Vec T) := + alloc_vec_Vec_bind v (fun l => if to_Z i <? Z.of_nat (length l) then Return (list_update l (usize_to_nat i) x) else Fail_ Failure). -(* The **backward** function shouldn't be used *) -Definition vec_index_fwd (T: Type) (v: vec T) (i: usize) : result T := - match nth_error (vec_to_list v) (usize_to_nat i) with - | Some n => Return n - | None => Fail_ Failure - end. - -Definition vec_index_back (T: Type) (v: vec T) (i: usize) (x: T) : result unit := - if to_Z i <? vec_length v then Return tt else Fail_ Failure. - -(* The **backward** function shouldn't be used *) -Definition vec_index_mut_fwd (T: Type) (v: vec T) (i: usize) : result T := - match nth_error (vec_to_list v) (usize_to_nat i) with - | Some n => Return n - | None => Fail_ Failure +(* Helper *) +Axiom alloc_vec_Vec_index_usize : forall {T : Type} (v : alloc_vec_Vec T) (i : usize), result T. + +(* Helper *) +Axiom alloc_vec_Vec_update_usize : forall {T : Type} (v : alloc_vec_Vec T) (i : usize) (x : T), result (alloc_vec_Vec T). + +(* Trait declaration: [core::slice::index::private_slice_index::Sealed] *) +Definition core_slice_index_private_slice_index_Sealed (self : Type) := unit. + +(* Trait declaration: [core::slice::index::SliceIndex] *) +Record core_slice_index_SliceIndex (Self T : Type) := mk_core_slice_index_SliceIndex { + core_slice_index_SliceIndex_sealedInst : core_slice_index_private_slice_index_Sealed Self; + core_slice_index_SliceIndex_Output : Type; + core_slice_index_SliceIndex_get : Self -> T -> result (option core_slice_index_SliceIndex_Output); + core_slice_index_SliceIndex_get_mut : Self -> T -> result (option core_slice_index_SliceIndex_Output); + core_slice_index_SliceIndex_get_mut_back : Self -> T -> option core_slice_index_SliceIndex_Output -> result T; + core_slice_index_SliceIndex_get_unchecked : Self -> const_raw_ptr T -> result (const_raw_ptr core_slice_index_SliceIndex_Output); + core_slice_index_SliceIndex_get_unchecked_mut : Self -> mut_raw_ptr T -> result (mut_raw_ptr core_slice_index_SliceIndex_Output); + core_slice_index_SliceIndex_index : Self -> T -> result core_slice_index_SliceIndex_Output; + core_slice_index_SliceIndex_index_mut : Self -> T -> result core_slice_index_SliceIndex_Output; + core_slice_index_SliceIndex_index_mut_back : Self -> T -> core_slice_index_SliceIndex_Output -> result T; +}. +Arguments mk_core_slice_index_SliceIndex {_ _}. +Arguments core_slice_index_SliceIndex_sealedInst {_ _}. +Arguments core_slice_index_SliceIndex_Output {_ _}. +Arguments core_slice_index_SliceIndex_get {_ _}. +Arguments core_slice_index_SliceIndex_get_mut {_ _}. +Arguments core_slice_index_SliceIndex_get_mut_back {_ _}. +Arguments core_slice_index_SliceIndex_get_unchecked {_ _}. +Arguments core_slice_index_SliceIndex_get_unchecked_mut {_ _}. +Arguments core_slice_index_SliceIndex_index {_ _}. +Arguments core_slice_index_SliceIndex_index_mut {_ _}. +Arguments core_slice_index_SliceIndex_index_mut_back {_ _}. + +(* [core::slice::index::[T]::index]: forward function *) +Definition core_slice_index_Slice_index + (T Idx : Type) (inst : core_slice_index_SliceIndex Idx (slice T)) + (s : slice T) (i : Idx) : result inst.(core_slice_index_SliceIndex_Output) := + x <- inst.(core_slice_index_SliceIndex_get) i s; + match x with + | None => Fail_ Failure + | Some x => Return x end. -Definition vec_index_mut_back (T: Type) (v: vec T) (i: usize) (x: T) : result (vec T) := - vec_bind v (fun l => - if to_Z i <? Z.of_nat (length l) - then Return (list_update l (usize_to_nat i) x) - else Fail_ Failure). +(* [core::slice::index::Range:::get]: forward function *) +Axiom core_slice_index_RangeUsize_get : forall (T : Type) (i : core_ops_range_Range usize) (s : slice T), result (option (slice T)). + +(* [core::slice::index::Range::get_mut]: forward function *) +Axiom core_slice_index_RangeUsize_get_mut : + forall (T : Type), core_ops_range_Range usize -> slice T -> result (option (slice T)). + +(* [core::slice::index::Range::get_mut]: backward function 0 *) +Axiom core_slice_index_RangeUsize_get_mut_back : + forall (T : Type), core_ops_range_Range usize -> slice T -> option (slice T) -> result (slice T). + +(* [core::slice::index::Range::get_unchecked]: forward function *) +Definition core_slice_index_RangeUsize_get_unchecked + (T : Type) : + core_ops_range_Range usize -> const_raw_ptr (slice T) -> result (const_raw_ptr (slice T)) := + (* Don't know what the model should be - for now we always fail to make + sure code which uses it fails *) + fun _ _ => Fail_ Failure. + +(* [core::slice::index::Range::get_unchecked_mut]: forward function *) +Definition core_slice_index_RangeUsize_get_unchecked_mut + (T : Type) : + core_ops_range_Range usize -> mut_raw_ptr (slice T) -> result (mut_raw_ptr (slice T)) := + (* Don't know what the model should be - for now we always fail to make + sure code which uses it fails *) + fun _ _ => Fail_ Failure. + +(* [core::slice::index::Range::index]: forward function *) +Axiom core_slice_index_RangeUsize_index : + forall (T : Type), core_ops_range_Range usize -> slice T -> result (slice T). + +(* [core::slice::index::Range::index_mut]: forward function *) +Axiom core_slice_index_RangeUsize_index_mut : + forall (T : Type), core_ops_range_Range usize -> slice T -> result (slice T). + +(* [core::slice::index::Range::index_mut]: backward function 0 *) +Axiom core_slice_index_RangeUsize_index_mut_back : + forall (T : Type), core_ops_range_Range usize -> slice T -> slice T -> result (slice T). + +(* [core::slice::index::[T]::index_mut]: forward function *) +Axiom core_slice_index_Slice_index_mut : + forall (T Idx : Type) (inst : core_slice_index_SliceIndex Idx (slice T)), + slice T -> Idx -> result inst.(core_slice_index_SliceIndex_Output). + +(* [core::slice::index::[T]::index_mut]: backward function 0 *) +Axiom core_slice_index_Slice_index_mut_back : + forall (T Idx : Type) (inst : core_slice_index_SliceIndex Idx (slice T)), + slice T -> Idx -> inst.(core_slice_index_SliceIndex_Output) -> result (slice T). + +(* [core::array::[T; N]::index]: forward function *) +Axiom core_array_Array_index : + forall (T Idx : Type) (N : usize) (inst : core_ops_index_Index (slice T) Idx) + (a : array T N) (i : Idx), result inst.(core_ops_index_Index_Output). + +(* [core::array::[T; N]::index_mut]: forward function *) +Axiom core_array_Array_index_mut : + forall (T Idx : Type) (N : usize) (inst : core_ops_index_IndexMut (slice T) Idx) + (a : array T N) (i : Idx), result inst.(core_ops_index_IndexMut_indexInst).(core_ops_index_Index_Output). + +(* [core::array::[T; N]::index_mut]: backward function 0 *) +Axiom core_array_Array_index_mut_back : + forall (T Idx : Type) (N : usize) (inst : core_ops_index_IndexMut (slice T) Idx) + (a : array T N) (i : Idx) (x : inst.(core_ops_index_IndexMut_indexInst).(core_ops_index_Index_Output)), result (array T N). + +(* Trait implementation: [core::slice::index::private_slice_index::Range] *) +Definition core_slice_index_private_slice_index_SealedRangeUsizeInst + : core_slice_index_private_slice_index_Sealed (core_ops_range_Range usize) := tt. + +(* Trait implementation: [core::slice::index::Range] *) +Definition core_slice_index_SliceIndexRangeUsizeSliceTInst (T : Type) : + core_slice_index_SliceIndex (core_ops_range_Range usize) (slice T) := {| + core_slice_index_SliceIndex_sealedInst := core_slice_index_private_slice_index_SealedRangeUsizeInst; + core_slice_index_SliceIndex_Output := slice T; + core_slice_index_SliceIndex_get := core_slice_index_RangeUsize_get T; + core_slice_index_SliceIndex_get_mut := core_slice_index_RangeUsize_get_mut T; + core_slice_index_SliceIndex_get_mut_back := core_slice_index_RangeUsize_get_mut_back T; + core_slice_index_SliceIndex_get_unchecked := core_slice_index_RangeUsize_get_unchecked T; + core_slice_index_SliceIndex_get_unchecked_mut := core_slice_index_RangeUsize_get_unchecked_mut T; + core_slice_index_SliceIndex_index := core_slice_index_RangeUsize_index T; + core_slice_index_SliceIndex_index_mut := core_slice_index_RangeUsize_index_mut T; + core_slice_index_SliceIndex_index_mut_back := core_slice_index_RangeUsize_index_mut_back T; +|}. + +(* Trait implementation: [core::slice::index::[T]] *) +Definition core_ops_index_IndexSliceTIInst (T Idx : Type) + (inst : core_slice_index_SliceIndex Idx (slice T)) : + core_ops_index_Index (slice T) Idx := {| + core_ops_index_Index_Output := inst.(core_slice_index_SliceIndex_Output); + core_ops_index_Index_index := core_slice_index_Slice_index T Idx inst; +|}. + +(* Trait implementation: [core::slice::index::[T]] *) +Definition core_ops_index_IndexMutSliceTIInst (T Idx : Type) + (inst : core_slice_index_SliceIndex Idx (slice T)) : + core_ops_index_IndexMut (slice T) Idx := {| + core_ops_index_IndexMut_indexInst := core_ops_index_IndexSliceTIInst T Idx inst; + core_ops_index_IndexMut_index_mut := core_slice_index_Slice_index_mut T Idx inst; + core_ops_index_IndexMut_index_mut_back := core_slice_index_Slice_index_mut_back T Idx inst; +|}. + +(* Trait implementation: [core::array::[T; N]] *) +Definition core_ops_index_IndexArrayInst (T Idx : Type) (N : usize) + (inst : core_ops_index_Index (slice T) Idx) : + core_ops_index_Index (array T N) Idx := {| + core_ops_index_Index_Output := inst.(core_ops_index_Index_Output); + core_ops_index_Index_index := core_array_Array_index T Idx N inst; +|}. + +(* Trait implementation: [core::array::[T; N]] *) +Definition core_ops_index_IndexMutArrayInst (T Idx : Type) (N : usize) + (inst : core_ops_index_IndexMut (slice T) Idx) : + core_ops_index_IndexMut (array T N) Idx := {| + core_ops_index_IndexMut_indexInst := core_ops_index_IndexArrayInst T Idx N inst.(core_ops_index_IndexMut_indexInst); + core_ops_index_IndexMut_index_mut := core_array_Array_index_mut T Idx N inst; + core_ops_index_IndexMut_index_mut_back := core_array_Array_index_mut_back T Idx N inst; +|}. + +(* [core::slice::index::usize::get]: forward function *) +Axiom core_slice_index_usize_get : forall (T : Type), usize -> slice T -> result (option T). + +(* [core::slice::index::usize::get_mut]: forward function *) +Axiom core_slice_index_usize_get_mut : forall (T : Type), usize -> slice T -> result (option T). + +(* [core::slice::index::usize::get_mut]: backward function 0 *) +Axiom core_slice_index_usize_get_mut_back : + forall (T : Type), usize -> slice T -> option T -> result (slice T). + +(* [core::slice::index::usize::get_unchecked]: forward function *) +Axiom core_slice_index_usize_get_unchecked : + forall (T : Type), usize -> const_raw_ptr (slice T) -> result (const_raw_ptr T). + +(* [core::slice::index::usize::get_unchecked_mut]: forward function *) +Axiom core_slice_index_usize_get_unchecked_mut : + forall (T : Type), usize -> mut_raw_ptr (slice T) -> result (mut_raw_ptr T). + +(* [core::slice::index::usize::index]: forward function *) +Axiom core_slice_index_usize_index : forall (T : Type), usize -> slice T -> result T. + +(* [core::slice::index::usize::index_mut]: forward function *) +Axiom core_slice_index_usize_index_mut : forall (T : Type), usize -> slice T -> result T. + +(* [core::slice::index::usize::index_mut]: backward function 0 *) +Axiom core_slice_index_usize_index_mut_back : + forall (T : Type), usize -> slice T -> T -> result (slice T). + +(* Trait implementation: [core::slice::index::private_slice_index::usize] *) +Definition core_slice_index_private_slice_index_SealedUsizeInst + : core_slice_index_private_slice_index_Sealed usize := tt. + +(* Trait implementation: [core::slice::index::usize] *) +Definition core_slice_index_SliceIndexUsizeSliceTInst (T : Type) : + core_slice_index_SliceIndex usize (slice T) := {| + core_slice_index_SliceIndex_sealedInst := core_slice_index_private_slice_index_SealedUsizeInst; + core_slice_index_SliceIndex_Output := T; + core_slice_index_SliceIndex_get := core_slice_index_usize_get T; + core_slice_index_SliceIndex_get_mut := core_slice_index_usize_get_mut T; + core_slice_index_SliceIndex_get_mut_back := core_slice_index_usize_get_mut_back T; + core_slice_index_SliceIndex_get_unchecked := core_slice_index_usize_get_unchecked T; + core_slice_index_SliceIndex_get_unchecked_mut := core_slice_index_usize_get_unchecked_mut T; + core_slice_index_SliceIndex_index := core_slice_index_usize_index T; + core_slice_index_SliceIndex_index_mut := core_slice_index_usize_index_mut T; + core_slice_index_SliceIndex_index_mut_back := core_slice_index_usize_index_mut_back T; +|}. + +(* [alloc::vec::Vec::index]: forward function *) +Axiom alloc_vec_Vec_index : forall (T Idx : Type) (inst : core_slice_index_SliceIndex Idx (slice T)) + (Self : alloc_vec_Vec T) (i : Idx), result inst.(core_slice_index_SliceIndex_Output). + +(* [alloc::vec::Vec::index_mut]: forward function *) +Axiom alloc_vec_Vec_index_mut : forall (T Idx : Type) (inst : core_slice_index_SliceIndex Idx (slice T)) + (Self : alloc_vec_Vec T) (i : Idx), result inst.(core_slice_index_SliceIndex_Output). + +(* [alloc::vec::Vec::index_mut]: backward function 0 *) +Axiom alloc_vec_Vec_index_mut_back : + forall (T Idx : Type) (inst : core_slice_index_SliceIndex Idx (slice T)) + (Self : alloc_vec_Vec T) (i : Idx) (x : inst.(core_slice_index_SliceIndex_Output)), result (alloc_vec_Vec T). + +(* Trait implementation: [alloc::vec::Vec] *) +Definition alloc_vec_Vec_coreopsindexIndexInst (T Idx : Type) + (inst : core_slice_index_SliceIndex Idx (slice T)) : + core_ops_index_Index (alloc_vec_Vec T) Idx := {| + core_ops_index_Index_Output := inst.(core_slice_index_SliceIndex_Output); + core_ops_index_Index_index := alloc_vec_Vec_index T Idx inst; +|}. + +(* Trait implementation: [alloc::vec::Vec] *) +Definition alloc_vec_Vec_coreopsindexIndexMutInst (T Idx : Type) + (inst : core_slice_index_SliceIndex Idx (slice T)) : + core_ops_index_IndexMut (alloc_vec_Vec T) Idx := {| + core_ops_index_IndexMut_indexInst := alloc_vec_Vec_coreopsindexIndexInst T Idx inst; + core_ops_index_IndexMut_index_mut := alloc_vec_Vec_index_mut T Idx inst; + core_ops_index_IndexMut_index_mut_back := alloc_vec_Vec_index_mut_back T Idx inst; +|}. + +(*** Theorems *) + +Axiom alloc_vec_Vec_index_eq : forall {a : Type} (v : alloc_vec_Vec a) (i : usize) (x : a), + alloc_vec_Vec_index a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i = + alloc_vec_Vec_index_usize v i. + +Axiom alloc_vec_Vec_index_mut_eq : forall {a : Type} (v : alloc_vec_Vec a) (i : usize) (x : a), + alloc_vec_Vec_index_mut a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i = + alloc_vec_Vec_index_usize v i. + +Axiom alloc_vec_Vec_index_mut_back_eq : forall {a : Type} (v : alloc_vec_Vec a) (i : usize) (x : a), + alloc_vec_Vec_index_mut_back a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i x = + alloc_vec_Vec_update_usize v i x. End Primitives. diff --git a/backends/fstar/Primitives.fst b/backends/fstar/Primitives.fst index 9db82069..94322ead 100644 --- a/backends/fstar/Primitives.fst +++ b/backends/fstar/Primitives.fst @@ -55,8 +55,12 @@ type string = string let is_zero (n: nat) : bool = n = 0 let decrease (n: nat{n > 0}) : nat = n - 1 -let mem_replace_fwd (a : Type0) (x : a) (y : a) : a = x -let mem_replace_back (a : Type0) (x : a) (y : a) : a = y +let core_mem_replace (a : Type0) (x : a) (y : a) : a = x +let core_mem_replace_back (a : Type0) (x : a) (y : a) : a = y + +// We don't really use raw pointers for now +type mut_raw_ptr (t : Type0) = { v : t } +type const_raw_ptr (t : Type0) = { v : t } (*** Scalars *) /// Rem.: most of the following code was partially generated @@ -100,6 +104,11 @@ type scalar_ty = | U64 | U128 +let is_unsigned = function + | Isize | I8 | I16 | I32 | I64 | I128 -> false + | Usize | U8 | U16 | U32 | U64 | U128 -> true + + let scalar_min (ty : scalar_ty) : int = match ty with | Isize -> isize_min @@ -162,6 +171,15 @@ let scalar_sub (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = mk_scalar ty (x * y) +let scalar_lxor (#ty : scalar_ty { is_unsigned ty && ty <> Usize }) + (x : scalar ty) (y : scalar ty) : scalar ty = + match ty with + | U8 -> FStar.UInt.logxor #8 x y + | U16 -> FStar.UInt.logxor #16 x y + | U32 -> FStar.UInt.logxor #32 x y + | U64 -> FStar.UInt.logxor #64 x y + | U128 -> FStar.UInt.logxor #128 x y + (** Cast an integer from a [src_ty] to a [tgt_ty] *) // TODO: check the semantics of casts in Rust let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) = @@ -169,17 +187,44 @@ let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : /// The scalar types type isize : eqtype = scalar Isize -type i8 : eqtype = scalar I8 -type i16 : eqtype = scalar I16 -type i32 : eqtype = scalar I32 -type i64 : eqtype = scalar I64 -type i128 : eqtype = scalar I128 +type i8 : eqtype = scalar I8 +type i16 : eqtype = scalar I16 +type i32 : eqtype = scalar I32 +type i64 : eqtype = scalar I64 +type i128 : eqtype = scalar I128 type usize : eqtype = scalar Usize -type u8 : eqtype = scalar U8 -type u16 : eqtype = scalar U16 -type u32 : eqtype = scalar U32 -type u64 : eqtype = scalar U64 -type u128 : eqtype = scalar U128 +type u8 : eqtype = scalar U8 +type u16 : eqtype = scalar U16 +type u32 : eqtype = scalar U32 +type u64 : eqtype = scalar U64 +type u128 : eqtype = scalar U128 + + +let core_isize_min : isize = isize_min +let core_isize_max : isize = isize_max +let core_i8_min : i8 = i8_min +let core_i8_max : i8 = i8_max +let core_i16_min : i16 = i16_min +let core_i16_max : i16 = i16_max +let core_i32_min : i32 = i32_min +let core_i32_max : i32 = i32_max +let core_i64_min : i64 = i64_min +let core_i64_max : i64 = i64_max +let core_i128_min : i128 = i128_min +let core_i128_max : i128 = i128_max + +let core_usize_min : usize = usize_min +let core_usize_max : usize = usize_max +let core_u8_min : u8 = u8_min +let core_u8_max : u8 = u8_max +let core_u16_min : u16 = u16_min +let core_u16_max : u16 = u16_max +let core_u32_min : u32 = u32_min +let core_u32_max : u32 = u32_max +let core_u64_min : u64 = u64_min +let core_u64_max : u64 = u64_max +let core_u128_min : u128 = u128_min +let core_u128_max : u128 = u128_max /// Negation let isize_neg = scalar_neg #Isize @@ -231,7 +276,7 @@ let u32_add = scalar_add #U32 let u64_add = scalar_add #U64 let u128_add = scalar_add #U128 -/// Substraction +/// Subtraction let isize_sub = scalar_sub #Isize let i8_sub = scalar_sub #I8 let i16_sub = scalar_sub #I16 @@ -259,12 +304,65 @@ let u32_mul = scalar_mul #U32 let u64_mul = scalar_mul #U64 let u128_mul = scalar_mul #U128 -(*** Range *) -type range (a : Type0) = { +/// Logical operators, defined for unsigned types only, so far +let u8_xor = scalar_lxor #U8 +let u16_xor = scalar_lxor #U16 +let u32_xor = scalar_lxor #U32 +let u64_xor = scalar_lxor #U64 +let u128_xor = scalar_lxor #U128 + +(*** core::ops *) + +// Trait declaration: [core::ops::index::Index] +noeq type core_ops_index_Index (self idx : Type0) = { + output : Type0; + index : self → idx → result output +} + +// Trait declaration: [core::ops::index::IndexMut] +noeq type core_ops_index_IndexMut (self idx : Type0) = { + indexInst : core_ops_index_Index self idx; + index_mut : self → idx → result indexInst.output; + index_mut_back : self → idx → indexInst.output → result self; +} + +// Trait declaration [core::ops::deref::Deref] +noeq type core_ops_deref_Deref (self : Type0) = { + target : Type0; + deref : self → result target; +} + +// Trait declaration [core::ops::deref::DerefMut] +noeq type core_ops_deref_DerefMut (self : Type0) = { + derefInst : core_ops_deref_Deref self; + deref_mut : self → result derefInst.target; + deref_mut_back : self → derefInst.target → result self; +} + +type core_ops_range_Range (a : Type0) = { start : a; end_ : a; } +(*** [alloc] *) + +let alloc_boxed_Box_deref (t : Type0) (x : t) : result t = Return x +let alloc_boxed_Box_deref_mut (t : Type0) (x : t) : result t = Return x +let alloc_boxed_Box_deref_mut_back (t : Type) (_ : t) (x : t) : result t = Return x + +// Trait instance +let alloc_boxed_Box_coreopsDerefInst (self : Type0) : core_ops_deref_Deref self = { + target = self; + deref = alloc_boxed_Box_deref self; +} + +// Trait instance +let alloc_boxed_Box_coreopsDerefMutInst (self : Type0) : core_ops_deref_DerefMut self = { + derefInst = alloc_boxed_Box_coreopsDerefInst self; + deref_mut = alloc_boxed_Box_deref_mut self; + deref_mut_back = alloc_boxed_Box_deref_mut_back self; +} + (*** Array *) type array (a : Type0) (n : usize) = s:list a{length s = n} @@ -278,15 +376,11 @@ let mk_array (a : Type0) (n : usize) normalize_term_spec (FStar.List.Tot.length l); l -let array_index_shared (a : Type0) (n : usize) (x : array a n) (i : usize) : result a = - if i < length x then Return (index x i) - else Fail Failure - -let array_index_mut_fwd (a : Type0) (n : usize) (x : array a n) (i : usize) : result a = +let array_index_usize (a : Type0) (n : usize) (x : array a n) (i : usize) : result a = if i < length x then Return (index x i) else Fail Failure -let array_index_mut_back (a : Type0) (n : usize) (x : array a n) (i : usize) (nx : a) : result (array a n) = +let array_update_usize (a : Type0) (n : usize) (x : array a n) (i : usize) (nx : a) : result (array a n) = if i < length x then Return (list_update x i nx) else Fail Failure @@ -295,55 +389,54 @@ type slice (a : Type0) = s:list a{length s <= usize_max} let slice_len (a : Type0) (s : slice a) : usize = length s -let slice_index_shared (a : Type0) (x : slice a) (i : usize) : result a = +let slice_index_usize (a : Type0) (x : slice a) (i : usize) : result a = if i < length x then Return (index x i) else Fail Failure -let slice_index_mut_fwd (a : Type0) (x : slice a) (i : usize) : result a = - if i < length x then Return (index x i) - else Fail Failure - -let slice_index_mut_back (a : Type0) (x : slice a) (i : usize) (nx : a) : result (slice a) = +let slice_update_usize (a : Type0) (x : slice a) (i : usize) (nx : a) : result (slice a) = if i < length x then Return (list_update x i nx) else Fail Failure (*** Subslices *) -let array_to_slice_shared (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x -let array_to_slice_mut_fwd (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x -let array_to_slice_mut_back (a : Type0) (n : usize) (x : array a n) (s : slice a) : result (array a n) = +let array_to_slice (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x +let array_from_slice (a : Type0) (n : usize) (x : array a n) (s : slice a) : result (array a n) = if length s = n then Return s else Fail Failure // TODO: finish the definitions below (there lacks [List.drop] and [List.take] in the standard library *) -let array_subslice_shared (a : Type0) (n : usize) (x : array a n) (r : range usize) : result (slice a) = - admit() - -let array_subslice_mut_fwd (a : Type0) (n : usize) (x : array a n) (r : range usize) : result (slice a) = +let array_subslice (a : Type0) (n : usize) (x : array a n) (r : core_ops_range_Range usize) : result (slice a) = admit() -let array_subslice_mut_back (a : Type0) (n : usize) (x : array a n) (r : range usize) (ns : slice a) : result (array a n) = +let array_update_subslice (a : Type0) (n : usize) (x : array a n) (r : core_ops_range_Range usize) (ns : slice a) : result (array a n) = admit() -let slice_subslice_shared (a : Type0) (x : slice a) (r : range usize) : result (slice a) = +let array_repeat (a : Type0) (n : usize) (x : a) : array a n = admit() -let slice_subslice_mut_fwd (a : Type0) (x : slice a) (r : range usize) : result (slice a) = +let slice_subslice (a : Type0) (x : slice a) (r : core_ops_range_Range usize) : result (slice a) = admit() -let slice_subslice_mut_back (a : Type0) (x : slice a) (r : range usize) (ns : slice a) : result (slice a) = +let slice_update_subslice (a : Type0) (x : slice a) (r : core_ops_range_Range usize) (ns : slice a) : result (slice a) = admit() (*** Vector *) -type vec (a : Type0) = v:list a{length v <= usize_max} +type alloc_vec_Vec (a : Type0) = v:list a{length v <= usize_max} -let vec_new (a : Type0) : vec a = assert_norm(length #a [] == 0); [] -let vec_len (a : Type0) (v : vec a) : usize = length v +let alloc_vec_Vec_new (a : Type0) : alloc_vec_Vec a = assert_norm(length #a [] == 0); [] +let alloc_vec_Vec_len (a : Type0) (v : alloc_vec_Vec a) : usize = length v + +// Helper +let alloc_vec_Vec_index_usize (#a : Type0) (v : alloc_vec_Vec a) (i : usize) : result a = + if i < length v then Return (index v i) else Fail Failure +// Helper +let alloc_vec_Vec_update_usize (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result (alloc_vec_Vec a) = + if i < length v then Return (list_update v i x) else Fail Failure // The **forward** function shouldn't be used -let vec_push_fwd (a : Type0) (v : vec a) (x : a) : unit = () -let vec_push_back (a : Type0) (v : vec a) (x : a) : - Pure (result (vec a)) +let alloc_vec_Vec_push_fwd (a : Type0) (v : alloc_vec_Vec a) (x : a) : unit = () +let alloc_vec_Vec_push (a : Type0) (v : alloc_vec_Vec a) (x : a) : + Pure (result (alloc_vec_Vec a)) (requires True) (ensures (fun res -> match res with @@ -358,18 +451,279 @@ let vec_push_back (a : Type0) (v : vec a) (x : a) : else Fail Failure // The **forward** function shouldn't be used -let vec_insert_fwd (a : Type0) (v : vec a) (i : usize) (x : a) : result unit = +let alloc_vec_Vec_insert_fwd (a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result unit = if i < length v then Return () else Fail Failure -let vec_insert_back (a : Type0) (v : vec a) (i : usize) (x : a) : result (vec a) = +let alloc_vec_Vec_insert (a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result (alloc_vec_Vec a) = if i < length v then Return (list_update v i x) else Fail Failure -// The **backward** function shouldn't be used -let vec_index_fwd (a : Type0) (v : vec a) (i : usize) : result a = - if i < length v then Return (index v i) else Fail Failure -let vec_index_back (a : Type0) (v : vec a) (i : usize) (x : a) : result unit = - if i < length v then Return () else Fail Failure +// Trait declaration: [core::slice::index::private_slice_index::Sealed] +type core_slice_index_private_slice_index_Sealed (self : Type0) = unit + +// Trait declaration: [core::slice::index::SliceIndex] +noeq type core_slice_index_SliceIndex (self t : Type0) = { + sealedInst : core_slice_index_private_slice_index_Sealed self; + output : Type0; + get : self → t → result (option output); + get_mut : self → t → result (option output); + get_mut_back : self → t → option output → result t; + get_unchecked : self → const_raw_ptr t → result (const_raw_ptr output); + get_unchecked_mut : self → mut_raw_ptr t → result (mut_raw_ptr output); + index : self → t → result output; + index_mut : self → t → result output; + index_mut_back : self → t → output → result t; +} -let vec_index_mut_fwd (a : Type0) (v : vec a) (i : usize) : result a = - if i < length v then Return (index v i) else Fail Failure -let vec_index_mut_back (a : Type0) (v : vec a) (i : usize) (nx : a) : result (vec a) = - if i < length v then Return (list_update v i nx) else Fail Failure +// [core::slice::index::[T]::index]: forward function +let core_slice_index_Slice_index + (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t)) + (s : slice t) (i : idx) : result inst.output = + let* x = inst.get i s in + match x with + | None -> Fail Failure + | Some x -> Return x + +// [core::slice::index::Range:::get]: forward function +let core_slice_index_RangeUsize_get (t : Type0) (i : core_ops_range_Range usize) (s : slice t) : + result (option (slice t)) = + admit () // TODO + +// [core::slice::index::Range::get_mut]: forward function +let core_slice_index_RangeUsize_get_mut + (t : Type0) : core_ops_range_Range usize → slice t → result (option (slice t)) = + admit () // TODO + +// [core::slice::index::Range::get_mut]: backward function 0 +let core_slice_index_RangeUsize_get_mut_back + (t : Type0) : + core_ops_range_Range usize → slice t → option (slice t) → result (slice t) = + admit () // TODO + +// [core::slice::index::Range::get_unchecked]: forward function +let core_slice_index_RangeUsize_get_unchecked + (t : Type0) : + core_ops_range_Range usize → const_raw_ptr (slice t) → result (const_raw_ptr (slice t)) = + // Don't know what the model should be - for now we always fail to make + // sure code which uses it fails + fun _ _ -> Fail Failure + +// [core::slice::index::Range::get_unchecked_mut]: forward function +let core_slice_index_RangeUsize_get_unchecked_mut + (t : Type0) : + core_ops_range_Range usize → mut_raw_ptr (slice t) → result (mut_raw_ptr (slice t)) = + // Don't know what the model should be - for now we always fail to make + // sure code which uses it fails + fun _ _ -> Fail Failure + +// [core::slice::index::Range::index]: forward function +let core_slice_index_RangeUsize_index + (t : Type0) : core_ops_range_Range usize → slice t → result (slice t) = + admit () // TODO + +// [core::slice::index::Range::index_mut]: forward function +let core_slice_index_RangeUsize_index_mut + (t : Type0) : core_ops_range_Range usize → slice t → result (slice t) = + admit () // TODO + +// [core::slice::index::Range::index_mut]: backward function 0 +let core_slice_index_RangeUsize_index_mut_back + (t : Type0) : core_ops_range_Range usize → slice t → slice t → result (slice t) = + admit () // TODO + +// [core::slice::index::[T]::index_mut]: forward function +let core_slice_index_Slice_index_mut + (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t)) : + slice t → idx → result inst.output = + admit () // + +// [core::slice::index::[T]::index_mut]: backward function 0 +let core_slice_index_Slice_index_mut_back + (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t)) : + slice t → idx → inst.output → result (slice t) = + admit () // TODO + +// [core::array::[T; N]::index]: forward function +let core_array_Array_index + (t idx : Type0) (n : usize) (inst : core_ops_index_Index (slice t) idx) + (a : array t n) (i : idx) : result inst.output = + admit () // TODO + +// [core::array::[T; N]::index_mut]: forward function +let core_array_Array_index_mut + (t idx : Type0) (n : usize) (inst : core_ops_index_IndexMut (slice t) idx) + (a : array t n) (i : idx) : result inst.indexInst.output = + admit () // TODO + +// [core::array::[T; N]::index_mut]: backward function 0 +let core_array_Array_index_mut_back + (t idx : Type0) (n : usize) (inst : core_ops_index_IndexMut (slice t) idx) + (a : array t n) (i : idx) (x : inst.indexInst.output) : result (array t n) = + admit () // TODO + +// Trait implementation: [core::slice::index::private_slice_index::Range] +let core_slice_index_private_slice_index_SealedRangeUsizeInst + : core_slice_index_private_slice_index_Sealed (core_ops_range_Range usize) = () + +// Trait implementation: [core::slice::index::Range] +let core_slice_index_SliceIndexRangeUsizeSliceTInst (t : Type0) : + core_slice_index_SliceIndex (core_ops_range_Range usize) (slice t) = { + sealedInst = core_slice_index_private_slice_index_SealedRangeUsizeInst; + output = slice t; + get = core_slice_index_RangeUsize_get t; + get_mut = core_slice_index_RangeUsize_get_mut t; + get_mut_back = core_slice_index_RangeUsize_get_mut_back t; + get_unchecked = core_slice_index_RangeUsize_get_unchecked t; + get_unchecked_mut = core_slice_index_RangeUsize_get_unchecked_mut t; + index = core_slice_index_RangeUsize_index t; + index_mut = core_slice_index_RangeUsize_index_mut t; + index_mut_back = core_slice_index_RangeUsize_index_mut_back t; +} + +// Trait implementation: [core::slice::index::[T]] +let core_ops_index_IndexSliceTIInst (t idx : Type0) + (inst : core_slice_index_SliceIndex idx (slice t)) : + core_ops_index_Index (slice t) idx = { + output = inst.output; + index = core_slice_index_Slice_index t idx inst; +} + +// Trait implementation: [core::slice::index::[T]] +let core_ops_index_IndexMutSliceTIInst (t idx : Type0) + (inst : core_slice_index_SliceIndex idx (slice t)) : + core_ops_index_IndexMut (slice t) idx = { + indexInst = core_ops_index_IndexSliceTIInst t idx inst; + index_mut = core_slice_index_Slice_index_mut t idx inst; + index_mut_back = core_slice_index_Slice_index_mut_back t idx inst; +} + +// Trait implementation: [core::array::[T; N]] +let core_ops_index_IndexArrayInst (t idx : Type0) (n : usize) + (inst : core_ops_index_Index (slice t) idx) : + core_ops_index_Index (array t n) idx = { + output = inst.output; + index = core_array_Array_index t idx n inst; +} + +// Trait implementation: [core::array::[T; N]] +let core_ops_index_IndexMutArrayIInst (t idx : Type0) (n : usize) + (inst : core_ops_index_IndexMut (slice t) idx) : + core_ops_index_IndexMut (array t n) idx = { + indexInst = core_ops_index_IndexArrayInst t idx n inst.indexInst; + index_mut = core_array_Array_index_mut t idx n inst; + index_mut_back = core_array_Array_index_mut_back t idx n inst; +} + +// [core::slice::index::usize::get]: forward function +let core_slice_index_usize_get + (t : Type0) : usize → slice t → result (option t) = + admit () // TODO + +// [core::slice::index::usize::get_mut]: forward function +let core_slice_index_usize_get_mut + (t : Type0) : usize → slice t → result (option t) = + admit () // TODO + +// [core::slice::index::usize::get_mut]: backward function 0 +let core_slice_index_usize_get_mut_back + (t : Type0) : usize → slice t → option t → result (slice t) = + admit () // TODO + +// [core::slice::index::usize::get_unchecked]: forward function +let core_slice_index_usize_get_unchecked + (t : Type0) : usize → const_raw_ptr (slice t) → result (const_raw_ptr t) = + admit () // TODO + +// [core::slice::index::usize::get_unchecked_mut]: forward function +let core_slice_index_usize_get_unchecked_mut + (t : Type0) : usize → mut_raw_ptr (slice t) → result (mut_raw_ptr t) = + admit () // TODO + +// [core::slice::index::usize::index]: forward function +let core_slice_index_usize_index (t : Type0) : usize → slice t → result t = + admit () // TODO + +// [core::slice::index::usize::index_mut]: forward function +let core_slice_index_usize_index_mut (t : Type0) : usize → slice t → result t = + admit () // TODO + +// [core::slice::index::usize::index_mut]: backward function 0 +let core_slice_index_usize_index_mut_back + (t : Type0) : usize → slice t → t → result (slice t) = + admit () // TODO + +// Trait implementation: [core::slice::index::private_slice_index::usize] +let core_slice_index_private_slice_index_SealedUsizeInst + : core_slice_index_private_slice_index_Sealed usize = () + +// Trait implementation: [core::slice::index::usize] +let core_slice_index_SliceIndexUsizeSliceTInst (t : Type0) : + core_slice_index_SliceIndex usize (slice t) = { + sealedInst = core_slice_index_private_slice_index_SealedUsizeInst; + output = t; + get = core_slice_index_usize_get t; + get_mut = core_slice_index_usize_get_mut t; + get_mut_back = core_slice_index_usize_get_mut_back t; + get_unchecked = core_slice_index_usize_get_unchecked t; + get_unchecked_mut = core_slice_index_usize_get_unchecked_mut t; + index = core_slice_index_usize_index t; + index_mut = core_slice_index_usize_index_mut t; + index_mut_back = core_slice_index_usize_index_mut_back t; +} + +// [alloc::vec::Vec::index]: forward function +let alloc_vec_Vec_index (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t)) + (self : alloc_vec_Vec t) (i : idx) : result inst.output = + admit () // TODO + +// [alloc::vec::Vec::index_mut]: forward function +let alloc_vec_Vec_index_mut (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t)) + (self : alloc_vec_Vec t) (i : idx) : result inst.output = + admit () // TODO + +// [alloc::vec::Vec::index_mut]: backward function 0 +let alloc_vec_Vec_index_mut_back + (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t)) + (self : alloc_vec_Vec t) (i : idx) (x : inst.output) : result (alloc_vec_Vec t) = + admit () // TODO + +// Trait implementation: [alloc::vec::Vec] +let alloc_vec_Vec_coreopsindexIndexInst (t idx : Type0) + (inst : core_slice_index_SliceIndex idx (slice t)) : + core_ops_index_Index (alloc_vec_Vec t) idx = { + output = inst.output; + index = alloc_vec_Vec_index t idx inst; +} + +// Trait implementation: [alloc::vec::Vec] +let alloc_vec_Vec_coreopsindexIndexMutInst (t idx : Type0) + (inst : core_slice_index_SliceIndex idx (slice t)) : + core_ops_index_IndexMut (alloc_vec_Vec t) idx = { + indexInst = alloc_vec_Vec_coreopsindexIndexInst t idx inst; + index_mut = alloc_vec_Vec_index_mut t idx inst; + index_mut_back = alloc_vec_Vec_index_mut_back t idx inst; +} + +(*** Theorems *) + +let alloc_vec_Vec_index_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) : + Lemma ( + alloc_vec_Vec_index a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i == + alloc_vec_Vec_index_usize v i) + [SMTPat (alloc_vec_Vec_index a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i)] + = + admit() + +let alloc_vec_Vec_index_mut_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) : + Lemma ( + alloc_vec_Vec_index_mut a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i == + alloc_vec_Vec_index_usize v i) + [SMTPat (alloc_vec_Vec_index_mut a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i)] + = + admit() + +let alloc_vec_Vec_index_mut_back_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : + Lemma ( + alloc_vec_Vec_index_mut_back a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i x == + alloc_vec_Vec_update_usize v i x) + [SMTPat (alloc_vec_Vec_index_mut_back a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i x)] + = + admit() diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml index 82da4de9..916988be 100644 --- a/backends/hol4/primitivesScript.sml +++ b/backends/hol4/primitivesScript.sml @@ -555,6 +555,32 @@ Proof QED val _ = evalLib.add_unfold_thm "mk_isize_unfold" +(** Constants *) +val core_i8_min_def = Define ‘core_i8_min = int_to_i8 i8_min’ +val core_i8_max_def = Define ‘core_i8_max = int_to_i8 i8_max’ +val core_i16_min_def = Define ‘core_i16_min = int_to_i16 i16_min’ +val core_i16_max_def = Define ‘core_i16_max = int_to_i16 i16_max’ +val core_i32_min_def = Define ‘core_i32_min = int_to_i32 i32_min’ +val core_i32_max_def = Define ‘core_i32_max = int_to_i32 i32_max’ +val core_i64_min_def = Define ‘core_i64_min = int_to_i64 i64_min’ +val core_i64_max_def = Define ‘core_i64_max = int_to_i64 i64_max’ +val core_i128_min_def = Define ‘core_i128_min = int_to_i128 i128_min’ +val core_i128_max_def = Define ‘core_i128_max = int_to_i128 i128_max’ +val core_isize_min_def = Define ‘core_isize_min = int_to_isize isize_min’ +val core_isize_max_def = Define ‘core_isize_max = int_to_isize isize_max’ +val core_u8_min_def = Define ‘core_u8_min = int_to_u8 0’ +val core_u8_max_def = Define ‘core_u8_max = int_to_u8 u8_max’ +val core_u16_min_def = Define ‘core_u16_min = int_to_u16 0’ +val core_u16_max_def = Define ‘core_u16_max = int_to_u16 u16_max’ +val core_u32_min_def = Define ‘core_u32_min = int_to_u32 0’ +val core_u32_max_def = Define ‘core_u32_max = int_to_u32 u32_max’ +val core_u64_min_def = Define ‘core_u64_min = int_to_u64 0’ +val core_u64_max_def = Define ‘core_u64_max = int_to_u64 u64_max’ +val core_u128_min_def = Define ‘core_u128_min = int_to_u128 0’ +val core_u128_max_def = Define ‘core_u128_max = int_to_u128 u128_max’ +val core_usize_min_def = Define ‘core_usize_min = int_to_usize 0’ +val core_usize_max_def = Define ‘core_usize_max = int_to_usize usize_max’ + val isize_neg_def = Define ‘isize_neg x = mk_isize (- (isize_to_int x))’ val i8_neg_def = Define ‘i8_neg x = mk_i8 (- (i8_to_int x))’ val i16_neg_def = Define ‘i16_neg x = mk_i16 (- (i16_to_int x))’ diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig index 6660b02d..4ae6bb3e 100644 --- a/backends/hol4/primitivesTheory.sig +++ b/backends/hol4/primitivesTheory.sig @@ -46,6 +46,30 @@ sig (* Definitions *) val bind_def : thm + val core_i128_max_def : thm + val core_i128_min_def : thm + val core_i16_max_def : thm + val core_i16_min_def : thm + val core_i32_max_def : thm + val core_i32_min_def : thm + val core_i64_max_def : thm + val core_i64_min_def : thm + val core_i8_max_def : thm + val core_i8_min_def : thm + val core_isize_max_def : thm + val core_isize_min_def : thm + val core_u128_max_def : thm + val core_u128_min_def : thm + val core_u16_max_def : thm + val core_u16_min_def : thm + val core_u32_max_def : thm + val core_u32_min_def : thm + val core_u64_max_def : thm + val core_u64_min_def : thm + val core_u8_max_def : thm + val core_u8_min_def : thm + val core_usize_max_def : thm + val core_usize_min_def : thm val error_BIJ : thm val error_CASE : thm val error_TY_DEF : thm @@ -566,6 +590,102 @@ sig monad_bind x f = case x of Return y => f y | Fail e => Fail e | Diverge => Diverge + [core_i128_max_def] Definition + + ⊢ core_i128_max = int_to_i128 i128_max + + [core_i128_min_def] Definition + + ⊢ core_i128_min = int_to_i128 i128_min + + [core_i16_max_def] Definition + + ⊢ core_i16_max = int_to_i16 i16_max + + [core_i16_min_def] Definition + + ⊢ core_i16_min = int_to_i16 i16_min + + [core_i32_max_def] Definition + + ⊢ core_i32_max = int_to_i32 i32_max + + [core_i32_min_def] Definition + + ⊢ core_i32_min = int_to_i32 i32_min + + [core_i64_max_def] Definition + + ⊢ core_i64_max = int_to_i64 i64_max + + [core_i64_min_def] Definition + + ⊢ core_i64_min = int_to_i64 i64_min + + [core_i8_max_def] Definition + + ⊢ core_i8_max = int_to_i8 i8_max + + [core_i8_min_def] Definition + + ⊢ core_i8_min = int_to_i8 i8_min + + [core_isize_max_def] Definition + + ⊢ core_isize_max = int_to_isize isize_max + + [core_isize_min_def] Definition + + ⊢ core_isize_min = int_to_isize isize_min + + [core_u128_max_def] Definition + + ⊢ core_u128_max = int_to_u128 u128_max + + [core_u128_min_def] Definition + + ⊢ core_u128_min = int_to_u128 0 + + [core_u16_max_def] Definition + + ⊢ core_u16_max = int_to_u16 u16_max + + [core_u16_min_def] Definition + + ⊢ core_u16_min = int_to_u16 0 + + [core_u32_max_def] Definition + + ⊢ core_u32_max = int_to_u32 u32_max + + [core_u32_min_def] Definition + + ⊢ core_u32_min = int_to_u32 0 + + [core_u64_max_def] Definition + + ⊢ core_u64_max = int_to_u64 u64_max + + [core_u64_min_def] Definition + + ⊢ core_u64_min = int_to_u64 0 + + [core_u8_max_def] Definition + + ⊢ core_u8_max = int_to_u8 u8_max + + [core_u8_min_def] Definition + + ⊢ core_u8_min = int_to_u8 0 + + [core_usize_max_def] Definition + + ⊢ core_usize_max = int_to_usize usize_max + + [core_usize_min_def] Definition + + ⊢ core_usize_min = int_to_usize 0 + [error_BIJ] Definition ⊢ (∀a. num2error (error2num a) = a) ∧ diff --git a/backends/lean/Base/Arith/Base.lean b/backends/lean/Base/Arith/Base.lean index 9c11ed45..8ada4171 100644 --- a/backends/lean/Base/Arith/Base.lean +++ b/backends/lean/Base/Arith/Base.lean @@ -57,4 +57,16 @@ theorem int_pos_ind (p : Int → Prop) : -- TODO: there is probably something more general to do theorem nat_zero_eq_int_zero : (0 : Nat) = (0 : Int) := by simp +-- This is mostly used in termination proofs +theorem to_int_to_nat_lt (x y : ℤ) (h0 : 0 ≤ x) (h1 : x < y) : + ↑(x.toNat) < y := by + simp [*] + +-- This is mostly used in termination proofs +theorem to_int_sub_to_nat_lt (x y : ℤ) (x' : ℕ) + (h0 : ↑x' ≤ x) (h1 : x - ↑x' < y) : + ↑(x.toNat - x') < y := by + have : 0 ≤ x := by linarith + simp [Int.toNat_sub_of_le, *] + end Arith diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean index 3359ecdb..a57f8bb1 100644 --- a/backends/lean/Base/Arith/Int.lean +++ b/backends/lean/Base/Arith/Int.lean @@ -162,7 +162,7 @@ def introInstances (declToUnfold : Name) (lookup : Expr → MetaM (Option Expr)) -- Add a declaration let nval ← Utils.addDeclTac name e type (asLet := false) -- Simplify to unfold the declaration to unfold (i.e., the projector) - Utils.simpAt [declToUnfold] [] [] (Tactic.Location.targets #[mkIdent name] false) + Utils.simpAt true [declToUnfold] [] [] (Location.targets #[mkIdent name] false) -- Return the new value pure nval @@ -240,7 +240,7 @@ def intTac (splitGoalConjs : Bool) (extraPreprocess : Tactic.TacticM Unit) : Ta -- the goal. I think before leads to a smaller proof term? Tactic.allGoals (intTacPreprocess extraPreprocess) -- More preprocessing - Tactic.allGoals (Utils.tryTac (Utils.simpAt [] [``nat_zero_eq_int_zero] [] .wildcard)) + Tactic.allGoals (Utils.tryTac (Utils.simpAt true [] [``nat_zero_eq_int_zero] [] .wildcard)) -- Split the conjunctions in the goal if splitGoalConjs then Tactic.allGoals (Utils.repeatTac Utils.splitConjTarget) -- Call linarith @@ -270,6 +270,17 @@ elab "int_tac" args:(" split_goal"?): tactic => let split := args.raw.getArgs.size > 0 intTac split (do pure ()) +-- For termination proofs +syntax "int_decr_tac" : tactic +macro_rules + | `(tactic| int_decr_tac) => + `(tactic| + simp_wf; + -- TODO: don't use a macro (namespace problems) + (first | apply Arith.to_int_to_nat_lt + | apply Arith.to_int_sub_to_nat_lt) <;> + simp_all <;> int_tac) + example (x : Int) (h0: 0 ≤ x) (h1: x ≠ 0) : 0 < x := by int_tac_preprocess linarith diff --git a/backends/lean/Base/Arith/Scalar.lean b/backends/lean/Base/Arith/Scalar.lean index 47751c8a..2342cce6 100644 --- a/backends/lean/Base/Arith/Scalar.lean +++ b/backends/lean/Base/Arith/Scalar.lean @@ -17,7 +17,7 @@ def scalarTacExtraPreprocess : Tactic.TacticM Unit := do add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Usize []]) add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Isize []]) -- Reveal the concrete bounds, simplify calls to [ofInt] - Utils.simpAt [``Scalar.min, ``Scalar.max, ``Scalar.cMin, ``Scalar.cMax, + Utils.simpAt true [``Scalar.min, ``Scalar.max, ``Scalar.cMin, ``Scalar.cMax, ``I8.min, ``I16.min, ``I32.min, ``I64.min, ``I128.min, ``I8.max, ``I16.max, ``I32.max, ``I64.max, ``I128.max, ``U8.min, ``U16.min, ``U32.min, ``U64.min, ``U128.min, @@ -36,6 +36,17 @@ def scalarTac (splitGoalConjs : Bool) : Tactic.TacticM Unit := do elab "scalar_tac" : tactic => scalarTac false +-- For termination proofs +syntax "scalar_decr_tac" : tactic +macro_rules + | `(tactic| scalar_decr_tac) => + `(tactic| + simp_wf; + -- TODO: don't use a macro (namespace problems) + (first | apply Arith.to_int_to_nat_lt + | apply Arith.to_int_sub_to_nat_lt) <;> + simp_all <;> scalar_tac) + instance (ty : ScalarTy) : HasIntProp (Scalar ty) where -- prop_ty is inferred prop := λ x => And.intro x.hmin x.hmax diff --git a/backends/lean/Base/IList/IList.lean b/backends/lean/Base/IList/IList.lean index a940da25..f71f2de2 100644 --- a/backends/lean/Base/IList/IList.lean +++ b/backends/lean/Base/IList/IList.lean @@ -112,7 +112,13 @@ def pairwise_rel section Lemmas -variable {α : Type u} +variable {α : Type u} + +def ireplicate {α : Type u} (i : ℤ) (x : α) : List α := + if i ≤ 0 then [] + else x :: ireplicate (i - 1) x +termination_by ireplicate i x => i.toNat +decreasing_by int_decr_tac @[simp] theorem update_nil : update ([] : List α) i y = [] := by simp [update] @[simp] theorem update_zero_cons : update ((x :: tl) : List α) 0 y = y :: tl := by simp [update] @@ -129,6 +135,10 @@ variable {α : Type u} @[simp] theorem slice_nil : slice i j ([] : List α) = [] := by simp [slice] @[simp] theorem slice_zero : slice 0 0 (ls : List α) = [] := by cases ls <;> simp [slice] +@[simp] theorem ireplicate_zero : ireplicate 0 x = [] := by rw [ireplicate]; simp +@[simp] theorem ireplicate_nzero_cons (hne : 0 < i) : ireplicate i x = x :: ireplicate (i - 1) x := by + rw [ireplicate]; simp [*]; intro; linarith + @[simp] theorem slice_nzero_cons (i j : Int) (x : α) (tl : List α) (hne : i ≠ 0) : slice i j ((x :: tl) : List α) = slice (i - 1) (j - 1) tl := match tl with @@ -144,6 +154,33 @@ theorem slice_nzero_cons (i j : Int) (x : α) (tl : List α) (hne : i ≠ 0) : s conv at this => lhs; simp [slice, *] simp [*, slice] +@[simp] +theorem ireplicate_replicate {α : Type u} (l : ℤ) (x : α) (h : 0 ≤ l) : + ireplicate l x = replicate l.toNat x := + if hz: l = 0 then by + simp [*] + else by + have : 0 < l := by int_tac + have hr := ireplicate_replicate (l - 1) x (by int_tac) + simp [*] + have hl : l.toNat = .succ (l.toNat - 1) := by + cases hl: l.toNat <;> simp_all + conv => rhs; rw[hl] +termination_by ireplicate_replicate l x h => l.toNat +decreasing_by int_decr_tac + +@[simp] +theorem ireplicate_len {α : Type u} (l : ℤ) (x : α) (h : 0 ≤ l) : + (ireplicate l x).len = l := + if hz: l = 0 then by + simp [*] + else by + have : 0 < l := by int_tac + have hr := ireplicate_len (l - 1) x (by int_tac) + simp [*] +termination_by ireplicate_len l x h => l.toNat +decreasing_by int_decr_tac + theorem len_eq_length (ls : List α) : ls.len = ls.length := by induction ls . rfl diff --git a/backends/lean/Base/Primitives.lean b/backends/lean/Base/Primitives.lean index 6b7b0792..613b6076 100644 --- a/backends/lean/Base/Primitives.lean +++ b/backends/lean/Base/Primitives.lean @@ -1,4 +1,6 @@ import Base.Primitives.Base import Base.Primitives.Scalar -import Base.Primitives.Array +import Base.Primitives.ArraySlice import Base.Primitives.Vec +import Base.Primitives.Alloc +import Base.Primitives.CoreOps diff --git a/backends/lean/Base/Primitives/Alloc.lean b/backends/lean/Base/Primitives/Alloc.lean new file mode 100644 index 00000000..6c89c6bb --- /dev/null +++ b/backends/lean/Base/Primitives/Alloc.lean @@ -0,0 +1,37 @@ +import Lean +import Base.Primitives.Base +import Base.Primitives.CoreOps + +open Primitives +open Result + +namespace alloc + +namespace boxed -- alloc.boxed + +namespace Box -- alloc.boxed.Box + +def deref (T : Type) (x : T) : Result T := ret x +def deref_mut (T : Type) (x : T) : Result T := ret x +def deref_mut_back (T : Type) (_ : T) (x : T) : Result T := ret x + +/-- Trait instance -/ +def coreopsDerefInst (Self : Type) : + core.ops.deref.Deref Self := { + Target := Self + deref := deref Self +} + +/-- Trait instance -/ +def coreopsDerefMutInst (Self : Type) : + core.ops.deref.DerefMut Self := { + derefInst := coreopsDerefInst Self + deref_mut := deref_mut Self + deref_mut_back := deref_mut_back Self +} + +end Box -- alloc.boxed.Box + +end boxed -- alloc.boxed + +end alloc diff --git a/backends/lean/Base/Primitives/Array.lean b/backends/lean/Base/Primitives/Array.lean deleted file mode 100644 index 6c95fd78..00000000 --- a/backends/lean/Base/Primitives/Array.lean +++ /dev/null @@ -1,394 +0,0 @@ -/- 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 diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean new file mode 100644 index 00000000..f68c0846 --- /dev/null +++ b/backends/lean/Base/Primitives/ArraySlice.lean @@ -0,0 +1,552 @@ +/- 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.Primitives.CoreOps +import Base.Arith +import Base.Progress.Base + +namespace Primitives + +open Result Error core.ops.range + +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_s {α : 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_usize (α : Type u) (n : Usize) (v: Array α n) (i: Usize) : Result α := + match v.val.indexOpt i.val with + | none => fail .arrayOutOfBounds + | some x => ret x + +-- For initialization +def Array.repeat (α : Type u) (n : Usize) (x : α) : Array α n := + ⟨ List.ireplicate n.val x, by have h := n.hmin; simp_all [Scalar.min] ⟩ + +@[pspec] +theorem Array.repeat_spec {α : Type u} (n : Usize) (x : α) : + ∃ a, Array.repeat α n x = a ∧ a.val = List.ireplicate n.val x := by + simp [Array.repeat] + +/- 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_usize_spec {α : Type u} {n : Usize} [Inhabited α] (v: Array α n) (i: Usize) + (hbound : i.val < v.length) : + ∃ x, v.index_usize α n i = ret x ∧ x = v.val.index i.val := by + simp only [index_usize] + -- TODO: dependent rewrite + have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*]) + simp [*] + +def Array.update_usize (α : 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.update_usize_spec {α : Type u} {n : Usize} (v: Array α n) (i: Usize) (x : α) + (hbound : i.val < v.length) : + ∃ nv, v.update_usize α n i x = ret nv ∧ + nv.val = v.val.update i.val x + := by + simp only [update_usize] + 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_s {α : 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_usize (α : 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_usize_spec {α : Type u} [Inhabited α] (v: Slice α) (i: Usize) + (hbound : i.val < v.length) : + ∃ x, v.index_usize α i = ret x ∧ x = v.val.index i.val := by + simp only [index_usize] + -- 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.update_usize (α : 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.update_usize_spec {α : Type u} (v: Slice α) (i: Usize) (x : α) + (hbound : i.val < v.length) : + ∃ nv, v.update_usize α i x = ret nv ∧ + nv.val = v.val.update i.val x + := by + simp only [update_usize] + 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_spec` spec theorem below (through the + `progress` tactic), meaning `Array.to_slice` should be considered as opaque. + All what the spec theorem reveals is that the "representative" lists are the same. -/ +def Array.to_slice (α : 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_spec {α : Type u} {n : Usize} (v : Array α n) : + ∃ s, to_slice α n v = ret s ∧ v.val = s.val := by simp [to_slice] + +def Array.from_slice (α : 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.from_slice_spec {α : Type u} {n : Usize} (a : Array α n) (ns : Slice α) (h : ns.val.len = n.val) : + ∃ na, from_slice α n a ns = ret na ∧ na.val = ns.val + := by simp [from_slice, *] + +def Array.subslice (α : 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_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 α 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, *] + 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.update_subslice (α : 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.update_subslice_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, update_subslice α n a r s = ret na ∧ + (∀ i, 0 ≤ i → i < r.start.val → na.index_s i = a.index_s i) ∧ + (∀ i, r.start.val ≤ i → i < r.end_.val → na.index_s i = s.index_s (i - r.start.val)) ∧ + (∀ i, r.end_.val ≤ i → i < n.val → na.index_s i = a.index_s i) := by + simp [update_subslice, *] + 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 (α : 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_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 α 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_s i = s.index_s (r.start.val + i)) + := by + simp [subslice, *] + 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 [*] + +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.update_subslice (α : 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.update_subslice_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, update_subslice α a r ss = ret na ∧ + (∀ i, 0 ≤ i → i < r.start.val → na.index_s i = a.index_s i) ∧ + (∀ i, r.start.val ≤ i → i < r.end_.val → na.index_s i = ss.index_s (i - r.start.val)) ∧ + (∀ i, r.end_.val ≤ i → i < a.length → na.index_s i = a.index_s i) := by + simp [update_subslice, *] + 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 [*] + +/- Trait declaration: [core::slice::index::private_slice_index::Sealed] -/ +structure core.slice.index.private_slice_index.Sealed (Self : Type) where + +/- Trait declaration: [core::slice::index::SliceIndex] -/ +structure core.slice.index.SliceIndex (Self T : Type) where + sealedInst : core.slice.index.private_slice_index.Sealed Self + Output : Type + get : Self → T → Result (Option Output) + get_mut : Self → T → Result (Option Output) + get_mut_back : Self → T → Option Output → Result T + get_unchecked : Self → ConstRawPtr T → Result (ConstRawPtr Output) + get_unchecked_mut : Self → MutRawPtr T → Result (MutRawPtr Output) + index : Self → T → Result Output + index_mut : Self → T → Result Output + index_mut_back : Self → T → Output → Result T + +/- [core::slice::index::[T]::index]: forward function -/ +def core.slice.index.Slice.index + (T I : Type) (inst : core.slice.index.SliceIndex I (Slice T)) + (slice : Slice T) (i : I) : Result inst.Output := do + let x ← inst.get i slice + match x with + | none => fail panic + | some x => ret x + +/- [core::slice::index::Range:::get]: forward function -/ +def core.slice.index.RangeUsize.get (T : Type) (i : Range Usize) (slice : Slice T) : + Result (Option (Slice T)) := + sorry -- TODO + +/- [core::slice::index::Range::get_mut]: forward function -/ +def core.slice.index.RangeUsize.get_mut + (T : Type) : Range Usize → Slice T → Result (Option (Slice T)) := + sorry -- TODO + +/- [core::slice::index::Range::get_mut]: backward function 0 -/ +def core.slice.index.RangeUsize.get_mut_back + (T : Type) : + Range Usize → Slice T → Option (Slice T) → Result (Slice T) := + sorry -- TODO + +/- [core::slice::index::Range::get_unchecked]: forward function -/ +def core.slice.index.RangeUsize.get_unchecked + (T : Type) : + Range Usize → ConstRawPtr (Slice T) → Result (ConstRawPtr (Slice T)) := + -- Don't know what the model should be - for now we always fail to make + -- sure code which uses it fails + fun _ _ => fail panic + +/- [core::slice::index::Range::get_unchecked_mut]: forward function -/ +def core.slice.index.RangeUsize.get_unchecked_mut + (T : Type) : + Range Usize → MutRawPtr (Slice T) → Result (MutRawPtr (Slice T)) := + -- Don't know what the model should be - for now we always fail to make + -- sure code which uses it fails + fun _ _ => fail panic + +/- [core::slice::index::Range::index]: forward function -/ +def core.slice.index.RangeUsize.index + (T : Type) : Range Usize → Slice T → Result (Slice T) := + sorry -- TODO + +/- [core::slice::index::Range::index_mut]: forward function -/ +def core.slice.index.RangeUsize.index_mut + (T : Type) : Range Usize → Slice T → Result (Slice T) := + sorry -- TODO + +/- [core::slice::index::Range::index_mut]: backward function 0 -/ +def core.slice.index.RangeUsize.index_mut_back + (T : Type) : Range Usize → Slice T → Slice T → Result (Slice T) := + sorry -- TODO + +/- [core::slice::index::[T]::index_mut]: forward function -/ +def core.slice.index.Slice.index_mut + (T I : Type) (inst : core.slice.index.SliceIndex I (Slice T)) : + Slice T → I → Result inst.Output := + sorry -- TODO + +/- [core::slice::index::[T]::index_mut]: backward function 0 -/ +def core.slice.index.Slice.index_mut_back + (T I : Type) (inst : core.slice.index.SliceIndex I (Slice T)) : + Slice T → I → inst.Output → Result (Slice T) := + sorry -- TODO + +/- [core::array::[T; N]::index]: forward function -/ +def core.array.Array.index + (T I : Type) (N : Usize) (inst : core.ops.index.Index (Slice T) I) + (a : Array T N) (i : I) : Result inst.Output := + sorry -- TODO + +/- [core::array::[T; N]::index_mut]: forward function -/ +def core.array.Array.index_mut + (T I : Type) (N : Usize) (inst : core.ops.index.IndexMut (Slice T) I) + (a : Array T N) (i : I) : Result inst.indexInst.Output := + sorry -- TODO + +/- [core::array::[T; N]::index_mut]: backward function 0 -/ +def core.array.Array.index_mut_back + (T I : Type) (N : Usize) (inst : core.ops.index.IndexMut (Slice T) I) + (a : Array T N) (i : I) (x : inst.indexInst.Output) : Result (Array T N) := + sorry -- TODO + +/- Trait implementation: [core::slice::index::private_slice_index::Range] -/ +def core.slice.index.private_slice_index.SealedRangeUsizeInst + : core.slice.index.private_slice_index.Sealed (Range Usize) := {} + +/- Trait implementation: [core::slice::index::Range] -/ +def core.slice.index.SliceIndexRangeUsizeSliceTInst (T : Type) : + core.slice.index.SliceIndex (Range Usize) (Slice T) := { + sealedInst := core.slice.index.private_slice_index.SealedRangeUsizeInst + Output := Slice T + get := core.slice.index.RangeUsize.get T + get_mut := core.slice.index.RangeUsize.get_mut T + get_mut_back := core.slice.index.RangeUsize.get_mut_back T + get_unchecked := core.slice.index.RangeUsize.get_unchecked T + get_unchecked_mut := core.slice.index.RangeUsize.get_unchecked_mut T + index := core.slice.index.RangeUsize.index T + index_mut := core.slice.index.RangeUsize.index_mut T + index_mut_back := core.slice.index.RangeUsize.index_mut_back T +} + +/- Trait implementation: [core::slice::index::[T]] -/ +def core.ops.index.IndexSliceTIInst (T I : Type) + (inst : core.slice.index.SliceIndex I (Slice T)) : + core.ops.index.Index (Slice T) I := { + Output := inst.Output + index := core.slice.index.Slice.index T I inst +} + +/- Trait implementation: [core::slice::index::[T]] -/ +def core.ops.index.IndexMutSliceTIInst (T I : Type) + (inst : core.slice.index.SliceIndex I (Slice T)) : + core.ops.index.IndexMut (Slice T) I := { + indexInst := core.ops.index.IndexSliceTIInst T I inst + index_mut := core.slice.index.Slice.index_mut T I inst + index_mut_back := core.slice.index.Slice.index_mut_back T I inst +} + +/- Trait implementation: [core::array::[T; N]] -/ +def core.ops.index.IndexArrayIInst (T I : Type) (N : Usize) + (inst : core.ops.index.Index (Slice T) I) : + core.ops.index.Index (Array T N) I := { + Output := inst.Output + index := core.array.Array.index T I N inst +} + +/- Trait implementation: [core::array::[T; N]] -/ +def core.ops.index.IndexMutArrayIInst (T I : Type) (N : Usize) + (inst : core.ops.index.IndexMut (Slice T) I) : + core.ops.index.IndexMut (Array T N) I := { + indexInst := core.ops.index.IndexArrayIInst T I N inst.indexInst + index_mut := core.array.Array.index_mut T I N inst + index_mut_back := core.array.Array.index_mut_back T I N inst +} + +/- [core::slice::index::usize::get]: forward function -/ +def core.slice.index.Usize.get + (T : Type) : Usize → Slice T → Result (Option T) := + sorry -- TODO + +/- [core::slice::index::usize::get_mut]: forward function -/ +def core.slice.index.Usize.get_mut + (T : Type) : Usize → Slice T → Result (Option T) := + sorry -- TODO + +/- [core::slice::index::usize::get_mut]: backward function 0 -/ +def core.slice.index.Usize.get_mut_back + (T : Type) : Usize → Slice T → Option T → Result (Slice T) := + sorry -- TODO + +/- [core::slice::index::usize::get_unchecked]: forward function -/ +def core.slice.index.Usize.get_unchecked + (T : Type) : Usize → ConstRawPtr (Slice T) → Result (ConstRawPtr T) := + sorry -- TODO + +/- [core::slice::index::usize::get_unchecked_mut]: forward function -/ +def core.slice.index.Usize.get_unchecked_mut + (T : Type) : Usize → MutRawPtr (Slice T) → Result (MutRawPtr T) := + sorry -- TODO + +/- [core::slice::index::usize::index]: forward function -/ +def core.slice.index.Usize.index (T : Type) : Usize → Slice T → Result T := + sorry -- TODO + +/- [core::slice::index::usize::index_mut]: forward function -/ +def core.slice.index.Usize.index_mut (T : Type) : Usize → Slice T → Result T := + sorry -- TODO + +/- [core::slice::index::usize::index_mut]: backward function 0 -/ +def core.slice.index.Usize.index_mut_back + (T : Type) : Usize → Slice T → T → Result (Slice T) := + sorry -- TODO + +/- Trait implementation: [core::slice::index::private_slice_index::usize] -/ +def core.slice.index.private_slice_index.SealedUsizeInst + : core.slice.index.private_slice_index.Sealed Usize := {} + +/- Trait implementation: [core::slice::index::usize] -/ +def core.slice.index.SliceIndexUsizeSliceTInst (T : Type) : + core.slice.index.SliceIndex Usize (Slice T) := { + sealedInst := core.slice.index.private_slice_index.SealedUsizeInst + Output := T + get := core.slice.index.Usize.get T + get_mut := core.slice.index.Usize.get_mut T + get_mut_back := core.slice.index.Usize.get_mut_back T + get_unchecked := core.slice.index.Usize.get_unchecked T + get_unchecked_mut := core.slice.index.Usize.get_unchecked_mut T + index := core.slice.index.Usize.index T + index_mut := core.slice.index.Usize.index_mut T + index_mut_back := core.slice.index.Usize.index_mut_back T +} + +end Primitives diff --git a/backends/lean/Base/Primitives/Base.lean b/backends/lean/Base/Primitives/Base.lean index 7c0fa3bb..7fc33251 100644 --- a/backends/lean/Base/Primitives/Base.lean +++ b/backends/lean/Base/Primitives/Base.lean @@ -120,11 +120,18 @@ def Result.attach {α: Type} (o : Result α): Result { x : α // o = ret x } := -- MISC -- ---------- -@[simp] def mem.replace (a : Type) (x : a) (_ : a) : a := x -@[simp] def mem.replace_back (a : Type) (_ : a) (y : a) : a := y +@[simp] def core.mem.replace (a : Type) (x : a) (_ : a) : a := x +@[simp] def core.mem.replace_back (a : Type) (_ : a) (y : a) : a := y /-- Aeneas-translated function -- useful to reduce non-recursive definitions. Use with `simp [ aeneas ]` -/ register_simp_attr aeneas +-- We don't really use raw pointers for now +structure MutRawPtr (T : Type) where + v : T + +structure ConstRawPtr (T : Type) where + v : T + end Primitives diff --git a/backends/lean/Base/Primitives/CoreOps.lean b/backends/lean/Base/Primitives/CoreOps.lean new file mode 100644 index 00000000..da458f66 --- /dev/null +++ b/backends/lean/Base/Primitives/CoreOps.lean @@ -0,0 +1,37 @@ +import Lean +import Base.Primitives.Base + +open Primitives +open Result + +namespace core.ops + +namespace index -- core.ops.index + +/- Trait declaration: [core::ops::index::Index] -/ +structure Index (Self Idx : Type) where + Output : Type + index : Self → Idx → Result Output + +/- Trait declaration: [core::ops::index::IndexMut] -/ +structure IndexMut (Self Idx : Type) where + indexInst : Index Self Idx + index_mut : Self → Idx → Result indexInst.Output + index_mut_back : Self → Idx → indexInst.Output → Result Self + +end index -- core.ops.index + +namespace deref -- core.ops.deref + +structure Deref (Self : Type) where + Target : Type + deref : Self → Result Target + +structure DerefMut (Self : Type) where + derefInst : Deref Self + deref_mut : Self → Result derefInst.Target + deref_mut_back : Self → derefInst.Target → Result Self + +end deref -- core.ops.deref + +end core.ops diff --git a/backends/lean/Base/Primitives/Range.lean b/backends/lean/Base/Primitives/Range.lean index 26cbee42..a268bcba 100644 --- a/backends/lean/Base/Primitives/Range.lean +++ b/backends/lean/Base/Primitives/Range.lean @@ -11,7 +11,7 @@ import Base.Progress.Base namespace Primitives -structure Range (α : Type u) where +structure core.ops.range.Range (α : Type u) where mk :: start: α end_: α diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean index 55227a9f..ec9665a5 100644 --- a/backends/lean/Base/Primitives/Scalar.lean +++ b/backends/lean/Base/Primitives/Scalar.lean @@ -230,6 +230,20 @@ def Scalar.cMax (ty : ScalarTy) : Int := | .Usize => Scalar.max .U32 | _ => Scalar.max ty +theorem Scalar.min_lt_max (ty : ScalarTy) : Scalar.min ty < Scalar.max ty := by + cases ty <;> simp [Scalar.min, Scalar.max] + . simp [Isize.min, Isize.max] + have h1 := Isize.refined_min.property + have h2 := Isize.refined_max.property + cases h1 <;> cases h2 <;> simp [*] + . simp [Usize.max] + have h := Usize.refined_max.property + cases h <;> simp [*] + +theorem Scalar.min_le_max (ty : ScalarTy) : Scalar.min ty ≤ Scalar.max ty := by + have := Scalar.min_lt_max ty + int_tac + theorem Scalar.cMin_bound ty : Scalar.min ty ≤ Scalar.cMin ty := by cases ty <;> simp [Scalar.min, Scalar.max, Scalar.cMin, Scalar.cMax] at * have h := Isize.refined_min.property @@ -395,6 +409,34 @@ def Scalar.cast {src_ty : ScalarTy} (tgt_ty : ScalarTy) (x : Scalar src_ty) : Re @[reducible] def U64 := Scalar .U64 @[reducible] def U128 := Scalar .U128 +-- TODO: reducible? +@[reducible] def core_isize_min : Isize := Scalar.ofInt Isize.min (by simp [Scalar.min, Scalar.max]; apply (Scalar.min_le_max .Isize)) +@[reducible] def core_isize_max : Isize := Scalar.ofInt Isize.max (by simp [Scalar.min, Scalar.max]; apply (Scalar.min_le_max .Isize)) +@[reducible] def core_i8_min : I8 := Scalar.ofInt I8.min +@[reducible] def core_i8_max : I8 := Scalar.ofInt I8.max +@[reducible] def core_i16_min : I16 := Scalar.ofInt I16.min +@[reducible] def core_i16_max : I16 := Scalar.ofInt I16.max +@[reducible] def core_i32_min : I32 := Scalar.ofInt I32.min +@[reducible] def core_i32_max : I32 := Scalar.ofInt I32.max +@[reducible] def core_i64_min : I64 := Scalar.ofInt I64.min +@[reducible] def core_i64_max : I64 := Scalar.ofInt I64.max +@[reducible] def core_i128_min : I128 := Scalar.ofInt I128.min +@[reducible] def core_i128_max : I128 := Scalar.ofInt I128.max + +-- TODO: reducible? +@[reducible] def core_usize_min : Usize := Scalar.ofInt Usize.min +@[reducible] def core_usize_max : Usize := Scalar.ofInt Usize.max (by simp [Scalar.min, Scalar.max]; apply (Scalar.min_le_max .Usize)) +@[reducible] def core_u8_min : U8 := Scalar.ofInt U8.min +@[reducible] def core_u8_max : U8 := Scalar.ofInt U8.max +@[reducible] def core_u16_min : U16 := Scalar.ofInt U16.min +@[reducible] def core_u16_max : U16 := Scalar.ofInt U16.max +@[reducible] def core_u32_min : U32 := Scalar.ofInt U32.min +@[reducible] def core_u32_max : U32 := Scalar.ofInt U32.max +@[reducible] def core_u64_min : U64 := Scalar.ofInt U64.min +@[reducible] def core_u64_max : U64 := Scalar.ofInt U64.max +@[reducible] def core_u128_min : U128 := Scalar.ofInt U128.min +@[reducible] def core_u128_max : U128 := Scalar.ofInt U128.max + -- TODO: below: not sure this is the best way. -- Should we rather overload operations like +, -, etc.? -- Also, it is possible to automate the generation of those definitions @@ -861,33 +903,33 @@ theorem Scalar.rem_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : S -- ofIntCore -- TODO: typeclass? -@[reducible] def Isize.ofIntCore := @Scalar.ofIntCore .Isize -@[reducible] def I8.ofIntCore := @Scalar.ofIntCore .I8 -@[reducible] def I16.ofIntCore := @Scalar.ofIntCore .I16 -@[reducible] def I32.ofIntCore := @Scalar.ofIntCore .I32 -@[reducible] def I64.ofIntCore := @Scalar.ofIntCore .I64 -@[reducible] def I128.ofIntCore := @Scalar.ofIntCore .I128 -@[reducible] def Usize.ofIntCore := @Scalar.ofIntCore .Usize -@[reducible] def U8.ofIntCore := @Scalar.ofIntCore .U8 -@[reducible] def U16.ofIntCore := @Scalar.ofIntCore .U16 -@[reducible] def U32.ofIntCore := @Scalar.ofIntCore .U32 -@[reducible] def U64.ofIntCore := @Scalar.ofIntCore .U64 -@[reducible] def U128.ofIntCore := @Scalar.ofIntCore .U128 +def Isize.ofIntCore := @Scalar.ofIntCore .Isize +def I8.ofIntCore := @Scalar.ofIntCore .I8 +def I16.ofIntCore := @Scalar.ofIntCore .I16 +def I32.ofIntCore := @Scalar.ofIntCore .I32 +def I64.ofIntCore := @Scalar.ofIntCore .I64 +def I128.ofIntCore := @Scalar.ofIntCore .I128 +def Usize.ofIntCore := @Scalar.ofIntCore .Usize +def U8.ofIntCore := @Scalar.ofIntCore .U8 +def U16.ofIntCore := @Scalar.ofIntCore .U16 +def U32.ofIntCore := @Scalar.ofIntCore .U32 +def U64.ofIntCore := @Scalar.ofIntCore .U64 +def U128.ofIntCore := @Scalar.ofIntCore .U128 -- ofInt -- TODO: typeclass? -@[reducible] def Isize.ofInt := @Scalar.ofInt .Isize -@[reducible] def I8.ofInt := @Scalar.ofInt .I8 -@[reducible] def I16.ofInt := @Scalar.ofInt .I16 -@[reducible] def I32.ofInt := @Scalar.ofInt .I32 -@[reducible] def I64.ofInt := @Scalar.ofInt .I64 -@[reducible] def I128.ofInt := @Scalar.ofInt .I128 -@[reducible] def Usize.ofInt := @Scalar.ofInt .Usize -@[reducible] def U8.ofInt := @Scalar.ofInt .U8 -@[reducible] def U16.ofInt := @Scalar.ofInt .U16 -@[reducible] def U32.ofInt := @Scalar.ofInt .U32 -@[reducible] def U64.ofInt := @Scalar.ofInt .U64 -@[reducible] def U128.ofInt := @Scalar.ofInt .U128 +abbrev Isize.ofInt := @Scalar.ofInt .Isize +abbrev I8.ofInt := @Scalar.ofInt .I8 +abbrev I16.ofInt := @Scalar.ofInt .I16 +abbrev I32.ofInt := @Scalar.ofInt .I32 +abbrev I64.ofInt := @Scalar.ofInt .I64 +abbrev I128.ofInt := @Scalar.ofInt .I128 +abbrev Usize.ofInt := @Scalar.ofInt .Usize +abbrev U8.ofInt := @Scalar.ofInt .U8 +abbrev U16.ofInt := @Scalar.ofInt .U16 +abbrev U32.ofInt := @Scalar.ofInt .U32 +abbrev U64.ofInt := @Scalar.ofInt .U64 +abbrev U128.ofInt := @Scalar.ofInt .U128 postfix:max "#isize" => Isize.ofInt postfix:max "#i8" => I8.ofInt @@ -905,9 +947,46 @@ postfix:max "#u128" => U128.ofInt -- Testing the notations example : Result Usize := 0#usize + 1#usize +-- TODO: factor those lemmas out @[simp] theorem Scalar.ofInt_val_eq {ty} (h : Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty) : (Scalar.ofInt x h).val = x := by simp [Scalar.ofInt, Scalar.ofIntCore] +@[simp] theorem Isize.ofInt_val_eq (h : Scalar.min ScalarTy.Isize ≤ x ∧ x ≤ Scalar.max ScalarTy.Isize) : (Isize.ofInt x h).val = x := by + apply Scalar.ofInt_val_eq h + +@[simp] theorem I8.ofInt_val_eq (h : Scalar.min ScalarTy.I8 ≤ x ∧ x ≤ Scalar.max ScalarTy.I8) : (I8.ofInt x h).val = x := by + apply Scalar.ofInt_val_eq h + +@[simp] theorem I16.ofInt_val_eq (h : Scalar.min ScalarTy.I16 ≤ x ∧ x ≤ Scalar.max ScalarTy.I16) : (I16.ofInt x h).val = x := by + apply Scalar.ofInt_val_eq h + +@[simp] theorem I32.ofInt_val_eq (h : Scalar.min ScalarTy.I32 ≤ x ∧ x ≤ Scalar.max ScalarTy.I32) : (I32.ofInt x h).val = x := by + apply Scalar.ofInt_val_eq h + +@[simp] theorem I64.ofInt_val_eq (h : Scalar.min ScalarTy.I64 ≤ x ∧ x ≤ Scalar.max ScalarTy.I64) : (I64.ofInt x h).val = x := by + apply Scalar.ofInt_val_eq h + +@[simp] theorem I128.ofInt_val_eq (h : Scalar.min ScalarTy.I128 ≤ x ∧ x ≤ Scalar.max ScalarTy.I128) : (I128.ofInt x h).val = x := by + apply Scalar.ofInt_val_eq h + +@[simp] theorem Usize.ofInt_val_eq (h : Scalar.min ScalarTy.Usize ≤ x ∧ x ≤ Scalar.max ScalarTy.Usize) : (Usize.ofInt x h).val = x := by + apply Scalar.ofInt_val_eq h + +@[simp] theorem U8.ofInt_val_eq (h : Scalar.min ScalarTy.U8 ≤ x ∧ x ≤ Scalar.max ScalarTy.U8) : (U8.ofInt x h).val = x := by + apply Scalar.ofInt_val_eq h + +@[simp] theorem U16.ofInt_val_eq (h : Scalar.min ScalarTy.U16 ≤ x ∧ x ≤ Scalar.max ScalarTy.U16) : (U16.ofInt x h).val = x := by + apply Scalar.ofInt_val_eq h + +@[simp] theorem U32.ofInt_val_eq (h : Scalar.min ScalarTy.U32 ≤ x ∧ x ≤ Scalar.max ScalarTy.U32) : (U32.ofInt x h).val = x := by + apply Scalar.ofInt_val_eq h + +@[simp] theorem U64.ofInt_val_eq (h : Scalar.min ScalarTy.U64 ≤ x ∧ x ≤ Scalar.max ScalarTy.U64) : (U64.ofInt x h).val = x := by + apply Scalar.ofInt_val_eq h + +@[simp] theorem U128.ofInt_val_eq (h : Scalar.min ScalarTy.U128 ≤ x ∧ x ≤ Scalar.max ScalarTy.U128) : (U128.ofInt x h).val = x := by + apply Scalar.ofInt_val_eq h + -- Comparisons instance {ty} : LT (Scalar ty) where lt a b := LT.lt a.val b.val diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean index c4c4d9f2..e600a151 100644 --- a/backends/lean/Base/Primitives/Vec.lean +++ b/backends/lean/Base/Primitives/Vec.lean @@ -6,7 +6,7 @@ import Mathlib.Tactic.RunCmd import Mathlib.Tactic.Linarith import Base.IList import Base.Primitives.Scalar -import Base.Primitives.Array +import Base.Primitives.ArraySlice import Base.Arith import Base.Progress.Base @@ -14,6 +14,8 @@ namespace Primitives open Result Error +namespace alloc.vec + def Vec (α : Type u) := { l : List α // l.length ≤ Usize.max } instance (a : Type u) : Arith.HasIntProp (Vec a) where @@ -79,7 +81,7 @@ theorem Vec.insert_spec {α : Type u} (v: Vec α) (i: Usize) (x: α) ∃ nv, v.insert α i x = ret nv ∧ nv.val = v.val.update i.val x := by simp [insert, *] -def Vec.index_shared (α : Type u) (v: Vec α) (i: Usize) : Result α := +def Vec.index_usize {α : Type u} (v: Vec α) (i: Usize) : Result α := match v.val.indexOpt i.val with | none => fail .arrayOutOfBounds | some x => ret x @@ -90,51 +92,83 @@ def Vec.index_shared (α : Type u) (v: Vec α) (i: Usize) : Result α := -/ @[pspec] -theorem Vec.index_shared_spec {α : Type u} [Inhabited α] (v: Vec α) (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 Vec.index_back (α : Type u) (v: Vec α) (i: Usize) (_: α) : Result Unit := - if i.val < List.length v.val then - .ret () - else - .fail arrayOutOfBounds - -def Vec.index_mut (α : Type u) (v: Vec α) (i: Usize) : Result α := - match v.val.indexOpt i.val with - | none => fail .arrayOutOfBounds - | some x => ret x - -@[pspec] -theorem Vec.index_mut_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize) +theorem Vec.index_usize_spec {α : Type u} [Inhabited α] (v: Vec α) (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] + ∃ x, v.index_usize i = ret x ∧ x = v.val.index i.val := by + simp only [index_usize] -- TODO: dependent rewrite have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*]) simp [*] -def Vec.index_mut_back (α : Type u) (v: Vec α) (i: Usize) (x: α) : Result (Vec α) := +def Vec.update_usize {α : Type u} (v: Vec α) (i: Usize) (x: α) : Result (Vec α) := 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 Vec.index_mut_back_spec {α : Type u} (v: Vec α) (i: Usize) (x : α) +theorem Vec.update_usize_spec {α : Type u} (v: Vec α) (i: Usize) (x : α) (hbound : i.val < v.length) : - ∃ nv, v.index_mut_back α i x = ret nv ∧ + ∃ nv, v.update_usize i x = ret nv ∧ nv.val = v.val.update i.val x := by - simp only [index_mut_back] + simp only [update_usize] have h := List.indexOpt_bounds v.val i.val split . simp_all [length]; cases h <;> scalar_tac . simp_all +/- [alloc::vec::Vec::index]: forward function -/ +def Vec.index (T I : Type) (inst : core.slice.index.SliceIndex I (Slice T)) + (self : Vec T) (i : I) : Result inst.Output := + sorry -- TODO + +/- [alloc::vec::Vec::index_mut]: forward function -/ +def Vec.index_mut (T I : Type) (inst : core.slice.index.SliceIndex I (Slice T)) + (self : Vec T) (i : I) : Result inst.Output := + sorry -- TODO + +/- [alloc::vec::Vec::index_mut]: backward function 0 -/ +def Vec.index_mut_back + (T I : Type) (inst : core.slice.index.SliceIndex I (Slice T)) + (self : Vec T) (i : I) (x : inst.Output) : Result (alloc.vec.Vec T) := + sorry -- TODO + +/- Trait implementation: [alloc::vec::Vec] -/ +def Vec.coreopsindexIndexInst (T I : Type) + (inst : core.slice.index.SliceIndex I (Slice T)) : + core.ops.index.Index (alloc.vec.Vec T) I := { + Output := inst.Output + index := Vec.index T I inst +} + +/- Trait implementation: [alloc::vec::Vec] -/ +def Vec.coreopsindexIndexMutInst (T I : Type) + (inst : core.slice.index.SliceIndex I (Slice T)) : + core.ops.index.IndexMut (alloc.vec.Vec T) I := { + indexInst := Vec.coreopsindexIndexInst T I inst + index_mut := Vec.index_mut T I inst + index_mut_back := Vec.index_mut_back T I inst +} + +@[simp] +theorem Vec.index_slice_index {α : Type} (v : Vec α) (i : Usize) : + Vec.index α Usize (core.slice.index.SliceIndexUsizeSliceTInst α) v i = + Vec.index_usize v i := + sorry + +@[simp] +theorem Vec.index_mut_slice_index {α : Type} (v : Vec α) (i : Usize) : + Vec.index_mut α Usize (core.slice.index.SliceIndexUsizeSliceTInst α) v i = + Vec.index_usize v i := + sorry + +@[simp] +theorem Vec.index_mut_back_slice_index {α : Type} (v : Vec α) (i : Usize) (x : α) : + Vec.index_mut_back α Usize (core.slice.index.SliceIndexUsizeSliceTInst α) v i x = + Vec.update_usize v i x := + sorry + +end alloc.vec + end Primitives diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean index 8b0759c5..ba63f09d 100644 --- a/backends/lean/Base/Progress/Progress.lean +++ b/backends/lean/Base/Progress/Progress.lean @@ -8,6 +8,27 @@ namespace Progress open Lean Elab Term Meta Tactic open Utils +-- TODO: the scalar types annoyingly often get reduced when we use the progress +-- tactic. We should find a way of controling reduction. For now we use rewriting +-- lemmas to make sure the goal remains clean, but this complexifies proof terms. +-- It seems there used to be a `fold` tactic. +theorem scalar_isize_eq : Primitives.Scalar .Isize = Primitives.Isize := by rfl +theorem scalar_i8_eq : Primitives.Scalar .I8 = Primitives.I8 := by rfl +theorem scalar_i16_eq : Primitives.Scalar .I16 = Primitives.I16 := by rfl +theorem scalar_i32_eq : Primitives.Scalar .I32 = Primitives.I32 := by rfl +theorem scalar_i64_eq : Primitives.Scalar .I64 = Primitives.I64 := by rfl +theorem scalar_i128_eq : Primitives.Scalar .I128 = Primitives.I128 := by rfl +theorem scalar_usize_eq : Primitives.Scalar .Usize = Primitives.Usize := by rfl +theorem scalar_u8_eq : Primitives.Scalar .U8 = Primitives.U8 := by rfl +theorem scalar_u16_eq : Primitives.Scalar .U16 = Primitives.U16 := by rfl +theorem scalar_u32_eq : Primitives.Scalar .U32 = Primitives.U32 := by rfl +theorem scalar_u64_eq : Primitives.Scalar .U64 = Primitives.U64 := by rfl +theorem scalar_u128_eq : Primitives.Scalar .U128 = Primitives.U128 := by rfl +def scalar_eqs := [ + ``scalar_isize_eq, ``scalar_i8_eq, ``scalar_i16_eq, ``scalar_i32_eq, ``scalar_i64_eq, ``scalar_i128_eq, + ``scalar_usize_eq, ``scalar_u8_eq, ``scalar_u16_eq, ``scalar_u32_eq, ``scalar_u64_eq, ``scalar_u128_eq +] + inductive TheoremOrLocal where | Theorem (thName : Name) | Local (asm : LocalDecl) @@ -111,8 +132,11 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal) splitEqAndPost fun hEq hPost ids => do trace[Progress] "eq and post:\n{hEq} : {← inferType hEq}\n{hPost}" tryTac ( - simpAt [] [``Primitives.bind_tc_ret, ``Primitives.bind_tc_fail, ``Primitives.bind_tc_div] + simpAt true [] + [``Primitives.bind_tc_ret, ``Primitives.bind_tc_fail, ``Primitives.bind_tc_div] [hEq.fvarId!] (.targets #[] true)) + -- TODO: remove this (some types get unfolded too much: we "fold" them back) + tryTac (simpAt true [] scalar_eqs [] .wildcard_dep) -- Clear the equality, unless the user requests not to do so let mgoal ← do if keep.isSome then getMainGoal @@ -359,6 +383,7 @@ namespace Test -- #eval showStoredPSpec -- #eval showStoredPSpecClass -- #eval showStoredPSpecExprClass + open alloc.vec example {ty} {x y : Scalar ty} (hmin : Scalar.min ty ≤ x.val + y.val) @@ -384,7 +409,7 @@ namespace Test `α : Type u` where u is quantified, while here we use `α : Type 0` -/ example {α : Type} (v: Vec α) (i: Usize) (x : α) (hbounds : i.val < v.length) : - ∃ nv, v.index_mut_back α i x = ret nv ∧ + ∃ nv, v.update_usize i x = ret nv ∧ nv.val = v.val.update i.val x := by progress simp [*] diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean index 5224e1c3..b917a789 100644 --- a/backends/lean/Base/Utils.lean +++ b/backends/lean/Base/Utils.lean @@ -604,16 +604,12 @@ example (h : ∃ x y z, x + y + z ≥ 0) : ∃ x, x ≥ 0 := by rename_i x y z exists x + y + z -/- Call the simp tactic. - The initialization of the context is adapted from Tactic.elabSimpArgs. - Something very annoying is that there is no function which allows to - initialize a simp context without doing an elaboration - as a consequence - we write our own here. -/ -def simpAt (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId) - (loc : Tactic.Location) : - Tactic.TacticM Unit := do - -- Initialize with the builtin simp theorems - let simpThms ← Tactic.simpOnlyBuiltins.foldlM (·.addConst ·) ({} : SimpTheorems) +def mkSimpCtx (simpOnly : Bool) (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId) : + Tactic.TacticM Simp.Context := do + -- Initialize either with the builtin simp theorems or with all the simp theorems + let simpThms ← + if simpOnly then Tactic.simpOnlyBuiltins.foldlM (·.addConst ·) ({} : SimpTheorems) + else getSimpTheorems -- Add the equational theorem for the declarations to unfold let simpThms ← declsToUnfold.foldlM (fun thms decl => thms.addDeclToUnfold decl) simpThms @@ -637,8 +633,63 @@ def simpAt (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVar throwError "Not a proposition: {thmName}" ) simpThms let congrTheorems ← getSimpCongrTheorems - let ctx : Simp.Context := { simpTheorems := #[simpThms], congrTheorems } + pure { simpTheorems := #[simpThms], congrTheorems } + + +inductive Location where + /-- Apply the tactic everywhere. Same as `Tactic.Location.wildcard` -/ + | wildcard + /-- Apply the tactic everywhere, including in the variable types (i.e., in + assumptions which are not propositions). --/ + | wildcard_dep + /-- Same as Tactic.Location -/ + | targets (hypotheses : Array Syntax) (type : Bool) + +-- Comes from Tactic.simpLocation +def customSimpLocation (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) + (loc : Location) : TacticM Simp.UsedSimps := do + match loc with + | Location.targets hyps simplifyTarget => + withMainContext do + let fvarIds ← Lean.Elab.Tactic.getFVarIds hyps + go fvarIds simplifyTarget + | Location.wildcard => + withMainContext do + go (← (← getMainGoal).getNondepPropHyps) (simplifyTarget := true) + | Location.wildcard_dep => + withMainContext do + let ctx ← Lean.MonadLCtx.getLCtx + let decls ← ctx.getDecls + let tgts := (decls.map (fun d => d.fvarId)).toArray + go tgts (simplifyTarget := true) +where + go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Simp.UsedSimps := do + let mvarId ← getMainGoal + let (result?, usedSimps) ← simpGoal mvarId ctx (simplifyTarget := simplifyTarget) (discharge? := discharge?) (fvarIdsToSimp := fvarIdsToSimp) + match result? with + | none => replaceMainGoal [] + | some (_, mvarId) => replaceMainGoal [mvarId] + return usedSimps + +/- Call the simp tactic. + The initialization of the context is adapted from Tactic.elabSimpArgs. + Something very annoying is that there is no function which allows to + initialize a simp context without doing an elaboration - as a consequence + we write our own here. -/ +def simpAt (simpOnly : Bool) (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId) + (loc : Location) : + Tactic.TacticM Unit := do + -- Initialize the simp context + let ctx ← mkSimpCtx simpOnly declsToUnfold thms hypsToUse + -- Apply the simplifier + let _ ← customSimpLocation ctx (discharge? := .none) loc + +-- Call the simpAll tactic +def simpAll (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId) : + Tactic.TacticM Unit := do + -- Initialize the simp context + let ctx ← mkSimpCtx false declsToUnfold thms hypsToUse -- Apply the simplifier - let _ ← Tactic.simpLocation ctx (discharge? := .none) loc + let _ ← Lean.Meta.simpAll (← getMainGoal) ctx end Utils |