diff options
| -rw-r--r-- | backends/coq/Primitives.v | 56 | ||||
| -rw-r--r-- | backends/fstar/Primitives.fst | 75 | ||||
| -rw-r--r-- | backends/lean/Base/Primitives/Array.lean | 28 | ||||
| -rw-r--r-- | compiler/Extract.ml | 22 | ||||
| -rw-r--r-- | compiler/Translate.ml | 2 |
5 files changed, 151 insertions, 32 deletions
diff --git a/backends/coq/Primitives.v b/backends/coq/Primitives.v index ae961ac2..d462715f 100644 --- a/backends/coq/Primitives.v +++ b/backends/coq/Primitives.v @@ -213,6 +213,7 @@ Proof. pose (scalar_max_cons_valid ty). lia. Qed. +Print scalar_le_max_valid. Definition scalar_in_bounds (ty: scalar_ty) (x: Z) : bool := scalar_ge_min ty x && scalar_le_max ty x . @@ -394,13 +395,15 @@ 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. -(*** Vectors *) - -Definition vec T := { l: list T | Z.of_nat (length l) <= usize_max }. +(*** Range *) +Record range (T : Type) := mk_range { + start: T; + end_: T; +}. +Arguments mk_range {_}. -Definition vec_to_list {T: Type} (v: vec T) : list T := proj1_sig v. - -Definition vec_length {T: Type} (v: vec T) : Z := Z.of_nat (length (vec_to_list v)). +(*** Arrays *) +Definition array T (n : usize) := { l: list T | Z.of_nat (length l) = to_Z n}. Lemma le_0_usize_max : 0 <= usize_max. Proof. @@ -409,6 +412,47 @@ Proof. lia. Qed. +Lemma eqb_imp_eq (x y : Z) : Z.eqb x y = true -> x = y. +Proof. + lia. +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). + +(*** 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). + +(*** 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_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). + +(*** Vectors *) + +Definition 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 vec_length {T: Type} (v: vec T) : Z := Z.of_nat (length (vec_to_list v)). + Definition vec_new (T: Type) : vec T := (exist _ [] le_0_usize_max). Lemma vec_len_in_usize {T} (v: vec T) : usize_min <= vec_length v <= usize_max. diff --git a/backends/fstar/Primitives.fst b/backends/fstar/Primitives.fst index 98a696b6..9db82069 100644 --- a/backends/fstar/Primitives.fst +++ b/backends/fstar/Primitives.fst @@ -259,6 +259,81 @@ let u32_mul = scalar_mul #U32 let u64_mul = scalar_mul #U64 let u128_mul = scalar_mul #U128 +(*** Range *) +type range (a : Type0) = { + start : a; + end_ : a; +} + +(*** Array *) +type array (a : Type0) (n : usize) = s:list a{length s = n} + +// We tried putting the normalize_term condition as a refinement on the list +// but it didn't work. It works with the requires clause. +let mk_array (a : Type0) (n : usize) + (l : list a) : + Pure (array a n) + (requires (normalize_term(FStar.List.Tot.length l) = n)) + (ensures (fun _ -> True)) = + 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 = + 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) = + if i < length x then Return (list_update x i nx) + else Fail Failure + +(*** Slice *) +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 = + 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) = + 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) = + 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) = + admit() + +let array_subslice_mut_back (a : Type0) (n : usize) (x : array a n) (r : 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) = + admit() + +let slice_subslice_mut_fwd (a : Type0) (x : slice a) (r : 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) = + admit() + (*** Vector *) type vec (a : Type0) = v:list a{length v <= usize_max} diff --git a/backends/lean/Base/Primitives/Array.lean b/backends/lean/Base/Primitives/Array.lean index 2d4a567b..6c95fd78 100644 --- a/backends/lean/Base/Primitives/Array.lean +++ b/backends/lean/Base/Primitives/Array.lean @@ -57,7 +57,7 @@ def Array.index_shared (α : Type u) (n : Usize) (v: Array α n) (i: Usize) : Re -/ @[pspec] -theorem Array.index_shared_spec {α : Type u} {n : Usize}[Inhabited α] (v: Array α n) (i: Usize) +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] @@ -202,32 +202,32 @@ theorem Slice.index_mut_back_spec {α : Type u} (v: Slice α) (i: Usize) (x : α /- 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. + 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 (α : Type u) (n : Usize) (v : Array α n) : Result (Slice α) := +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_spec {α : Type u} {n : Usize} (v : Array α n) : - ∃ s, to_slice α n v = ret s ∧ v.val = s.val := by simp [to_slice] +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_mut_slice (α : Type u) (n : Usize) (v : Array α n) : Result (Slice α) := - to_slice α n v +def Array.to_slice_mut (α : Type u) (n : Usize) (v : Array α n) : Result (Slice α) := + to_slice_shared α n v @[pspec] -theorem Array.to_mut_slice_spec {α : Type u} {n : Usize} (v : Array α n) : - ∃ s, Array.to_slice α n v = ret s ∧ v.val = s.val := to_slice_spec v +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_mut_slice_back (α : Type u) (n : Usize) (_ : Array α n) (s : Slice α) : Result (Array α n) := +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_mut_slice_back_spec {α : Type u} {n : Usize} (a : Array α n) (ns : Slice α) (h : ns.val.len = n.val) : - ∃ na, to_mut_slice_back α n a ns = ret na ∧ na.val = ns.val - := by simp [to_mut_slice_back, *] +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 diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 84d11895..297c182a 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -262,8 +262,8 @@ let assumed_adts () : (assumed_ty * string) list = let assumed_struct_constructors () : (assumed_ty * string) list = match !backend with | Lean -> [ (Range, "Range.mk"); (Array, "Array.make") ] - | Coq -> [ (Range, "range.mk"); (Array, "array.mk") ] - | FStar -> [ (Range, "mkrange"); (Array, "mkarray") ] + | Coq -> [ (Range, "mk_range"); (Array, "mk_array") ] + | FStar -> [ (Range, "Mkrange"); (Array, "mk_array") ] | HOL4 -> [ (Range, "mk_range"); (Array, "mk_array") ] let assumed_variants () : (assumed_ty * VariantId.id * string) list = @@ -332,19 +332,19 @@ let assumed_llbc_functions () : (ArraySharedIndex, None, "array_index_shared"); (ArrayMutIndex, None, "array_index_mut_fwd"); (ArrayMutIndex, rg0, "array_index_mut_back"); - (ArrayToSharedSlice, None, "array_to_slice"); - (ArrayToMutSlice, None, "array_to_mut_slice_fwd"); - (ArrayToMutSlice, rg0, "array_to_mut_slice_back"); + (ArrayToSharedSlice, None, "array_to_slice_shared"); + (ArrayToMutSlice, None, "array_to_slice_mut_fwd"); + (ArrayToMutSlice, rg0, "array_to_slice_mut_back"); (ArraySharedSubslice, None, "array_subslice_shared"); (ArrayMutSubslice, None, "array_subslice_mut_fwd"); (ArrayMutSubslice, rg0, "array_subslice_mut_back"); (SliceSharedIndex, None, "slice_index_shared"); (SliceMutIndex, None, "slice_index_mut_fwd"); (SliceMutIndex, rg0, "slice_index_mut_back"); - (SliceSharedSubslice, None, "slice_subslice_mut"); + (SliceSharedSubslice, None, "slice_subslice_shared"); (SliceMutSubslice, None, "slice_subslice_mut_fwd"); (SliceMutSubslice, rg0, "slice_subslice_mut_back"); - (SliceLen, None, "slice_len_fwd"); + (SliceLen, None, "slice_len"); ] | Lean -> [ @@ -360,14 +360,12 @@ let assumed_llbc_functions () : (VecIndex, rg0, "Vec.index_shared_back") (* shouldn't be used *); (VecIndexMut, None, "Vec.index_mut"); (VecIndexMut, rg0, "Vec.index_mut_back"); - (* TODO: it would be good to only use Array.index (no Array.index_mut) - (same for subslice, etc.) *) (ArraySharedIndex, None, "Array.index_shared"); (ArrayMutIndex, None, "Array.index_mut"); (ArrayMutIndex, rg0, "Array.index_mut_back"); - (ArrayToSharedSlice, None, "Array.to_slice"); - (ArrayToMutSlice, None, "Array.to_mut_slice"); - (ArrayToMutSlice, rg0, "Array.to_mut_slice_back"); + (ArrayToSharedSlice, None, "Array.to_slice_shared"); + (ArrayToMutSlice, None, "Array.to_slice_mut"); + (ArrayToMutSlice, rg0, "Array.to_slice_mut_back"); (ArraySharedSubslice, None, "Array.subslice_shared"); (ArrayMutSubslice, None, "Array.subslice_mut"); (ArrayMutSubslice, rg0, "Array.subslice_mut_back"); diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 17355dfd..dfc97246 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -833,6 +833,8 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info) Printf.fprintf out "Require Import Primitives.\n"; Printf.fprintf out "Import Primitives.\n"; Printf.fprintf out "Require Import Coq.ZArith.ZArith.\n"; + Printf.fprintf out "Require Import List.\n"; + Printf.fprintf out "Import ListNotations.\n"; Printf.fprintf out "Local Open Scope Primitives_scope.\n"; (* Add the custom imports *) |