diff options
Diffstat (limited to 'tests/coq/array')
| -rw-r--r-- | tests/coq/array/Array.v | 519 | ||||
| -rw-r--r-- | tests/coq/array/Makefile | 23 | ||||
| -rw-r--r-- | tests/coq/array/Primitives.v | 899 | ||||
| -rw-r--r-- | tests/coq/array/_CoqProject | 7 |
4 files changed, 0 insertions, 1448 deletions
diff --git a/tests/coq/array/Array.v b/tests/coq/array/Array.v deleted file mode 100644 index 3a30413a..00000000 --- a/tests/coq/array/Array.v +++ /dev/null @@ -1,519 +0,0 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [array] *) -Require Import Primitives. -Import Primitives. -Require Import Coq.ZArith.ZArith. -Require Import List. -Import ListNotations. -Local Open Scope Primitives_scope. -Module Array. - -(** [array::AB] - Source: 'src/array.rs', lines 3:0-3:11 *) -Inductive AB_t := | AB_A : AB_t | AB_B : AB_t. - -(** [array::incr]: - Source: 'src/array.rs', lines 8:0-8:24 *) -Definition incr (x : u32) : result u32 := - u32_add x 1%u32. - -(** [array::array_to_shared_slice_]: - Source: 'src/array.rs', lines 16:0-16:53 *) -Definition array_to_shared_slice_ - (T : Type) (s : array T 32%usize) : result (slice T) := - array_to_slice T 32%usize s -. - -(** [array::array_to_mut_slice_]: - Source: 'src/array.rs', lines 21:0-21:58 *) -Definition array_to_mut_slice_ - (T : Type) (s : array T 32%usize) : - result ((slice T) * (slice T -> result (array T 32%usize))) - := - p <- array_to_slice_mut T 32%usize s; - let (s1, to_slice_mut_back) := p in - Return (s1, to_slice_mut_back) -. - -(** [array::array_len]: - Source: 'src/array.rs', lines 25:0-25:40 *) -Definition array_len (T : Type) (s : array T 32%usize) : result usize := - s1 <- array_to_slice T 32%usize s; let i := slice_len T s1 in Return i -. - -(** [array::shared_array_len]: - Source: 'src/array.rs', lines 29:0-29:48 *) -Definition shared_array_len (T : Type) (s : array T 32%usize) : result usize := - s1 <- array_to_slice T 32%usize s; let i := slice_len T s1 in Return i -. - -(** [array::shared_slice_len]: - Source: 'src/array.rs', lines 33:0-33:44 *) -Definition shared_slice_len (T : Type) (s : slice T) : result usize := - let i := slice_len T s in Return i -. - -(** [array::index_array_shared]: - Source: 'src/array.rs', lines 37:0-37:57 *) -Definition index_array_shared - (T : Type) (s : array T 32%usize) (i : usize) : result T := - array_index_usize T 32%usize s i -. - -(** [array::index_array_u32]: - Source: 'src/array.rs', lines 44:0-44:53 *) -Definition index_array_u32 (s : array u32 32%usize) (i : usize) : result u32 := - array_index_usize u32 32%usize s i -. - -(** [array::index_array_copy]: - Source: 'src/array.rs', lines 48:0-48:45 *) -Definition index_array_copy (x : array u32 32%usize) : result u32 := - array_index_usize u32 32%usize x 0%usize -. - -(** [array::index_mut_array]: - Source: 'src/array.rs', lines 52:0-52:62 *) -Definition index_mut_array - (T : Type) (s : array T 32%usize) (i : usize) : - result (T * (T -> result (array T 32%usize))) - := - p <- array_index_mut_usize T 32%usize s i; - let (t, index_mut_back) := p in - Return (t, index_mut_back) -. - -(** [array::index_slice]: - Source: 'src/array.rs', lines 56:0-56:46 *) -Definition index_slice (T : Type) (s : slice T) (i : usize) : result T := - slice_index_usize T s i -. - -(** [array::index_mut_slice]: - Source: 'src/array.rs', lines 60:0-60:58 *) -Definition index_mut_slice - (T : Type) (s : slice T) (i : usize) : - result (T * (T -> result (slice T))) - := - p <- slice_index_mut_usize T s i; - let (t, index_mut_back) := p in - Return (t, index_mut_back) -. - -(** [array::slice_subslice_shared_]: - Source: 'src/array.rs', lines 64:0-64:70 *) -Definition slice_subslice_shared_ - (x : slice u32) (y : usize) (z : usize) : result (slice u32) := - core_slice_index_Slice_index u32 (core_ops_range_Range usize) - (core_slice_index_SliceIndexRangeUsizeSliceTInst u32) x - {| core_ops_range_Range_start := y; core_ops_range_Range_end_ := z |} -. - -(** [array::slice_subslice_mut_]: - Source: 'src/array.rs', lines 68:0-68:75 *) -Definition slice_subslice_mut_ - (x : slice u32) (y : usize) (z : usize) : - result ((slice u32) * (slice u32 -> result (slice u32))) - := - p <- - core_slice_index_Slice_index_mut u32 (core_ops_range_Range usize) - (core_slice_index_SliceIndexRangeUsizeSliceTInst u32) x - {| core_ops_range_Range_start := y; core_ops_range_Range_end_ := z |}; - let (s, index_mut_back) := p in - Return (s, index_mut_back) -. - -(** [array::array_to_slice_shared_]: - Source: 'src/array.rs', lines 72:0-72:54 *) -Definition array_to_slice_shared_ - (x : array u32 32%usize) : result (slice u32) := - array_to_slice u32 32%usize x -. - -(** [array::array_to_slice_mut_]: - Source: 'src/array.rs', lines 76:0-76:59 *) -Definition array_to_slice_mut_ - (x : array u32 32%usize) : - result ((slice u32) * (slice u32 -> result (array u32 32%usize))) - := - p <- array_to_slice_mut u32 32%usize x; - let (s, to_slice_mut_back) := p in - Return (s, to_slice_mut_back) -. - -(** [array::array_subslice_shared_]: - Source: 'src/array.rs', lines 80:0-80:74 *) -Definition array_subslice_shared_ - (x : array u32 32%usize) (y : usize) (z : usize) : result (slice u32) := - core_array_Array_index u32 (core_ops_range_Range usize) 32%usize - (core_ops_index_IndexSliceTIInst u32 (core_ops_range_Range usize) - (core_slice_index_SliceIndexRangeUsizeSliceTInst u32)) x - {| core_ops_range_Range_start := y; core_ops_range_Range_end_ := z |} -. - -(** [array::array_subslice_mut_]: - Source: 'src/array.rs', lines 84:0-84:79 *) -Definition array_subslice_mut_ - (x : array u32 32%usize) (y : usize) (z : usize) : - result ((slice u32) * (slice u32 -> result (array u32 32%usize))) - := - p <- - core_array_Array_index_mut u32 (core_ops_range_Range usize) 32%usize - (core_ops_index_IndexMutSliceTIInst u32 (core_ops_range_Range usize) - (core_slice_index_SliceIndexRangeUsizeSliceTInst u32)) x - {| core_ops_range_Range_start := y; core_ops_range_Range_end_ := z |}; - let (s, index_mut_back) := p in - Return (s, index_mut_back) -. - -(** [array::index_slice_0]: - Source: 'src/array.rs', lines 88:0-88:38 *) -Definition index_slice_0 (T : Type) (s : slice T) : result T := - slice_index_usize T s 0%usize -. - -(** [array::index_array_0]: - Source: 'src/array.rs', lines 92:0-92:42 *) -Definition index_array_0 (T : Type) (s : array T 32%usize) : result T := - array_index_usize T 32%usize s 0%usize -. - -(** [array::index_index_array]: - Source: 'src/array.rs', lines 103:0-103:71 *) -Definition index_index_array - (s : array (array u32 32%usize) 32%usize) (i : usize) (j : usize) : - result u32 - := - a <- array_index_usize (array u32 32%usize) 32%usize s i; - array_index_usize u32 32%usize a j -. - -(** [array::update_update_array]: - Source: 'src/array.rs', lines 114:0-114:70 *) -Definition update_update_array - (s : array (array u32 32%usize) 32%usize) (i : usize) (j : usize) : - result unit - := - p <- array_index_mut_usize (array u32 32%usize) 32%usize s i; - let (a, index_mut_back) := p in - p1 <- array_index_mut_usize u32 32%usize a j; - let (_, index_mut_back1) := p1 in - a1 <- index_mut_back1 0%u32; - _ <- index_mut_back a1; - Return tt -. - -(** [array::array_local_deep_copy]: - Source: 'src/array.rs', lines 118:0-118:43 *) -Definition array_local_deep_copy (x : array u32 32%usize) : result unit := - Return tt -. - -(** [array::take_array]: - Source: 'src/array.rs', lines 122:0-122:30 *) -Definition take_array (a : array u32 2%usize) : result unit := - Return tt. - -(** [array::take_array_borrow]: - Source: 'src/array.rs', lines 123:0-123:38 *) -Definition take_array_borrow (a : array u32 2%usize) : result unit := - Return tt -. - -(** [array::take_slice]: - Source: 'src/array.rs', lines 124:0-124:28 *) -Definition take_slice (s : slice u32) : result unit := - Return tt. - -(** [array::take_mut_slice]: - Source: 'src/array.rs', lines 125:0-125:36 *) -Definition take_mut_slice (s : slice u32) : result (slice u32) := - Return s. - -(** [array::const_array]: - Source: 'src/array.rs', lines 127:0-127:32 *) -Definition const_array : result (array u32 2%usize) := - Return (mk_array u32 2%usize [ 0%u32; 0%u32 ]) -. - -(** [array::const_slice]: - Source: 'src/array.rs', lines 131:0-131:20 *) -Definition const_slice : result unit := - _ <- array_to_slice u32 2%usize (mk_array u32 2%usize [ 0%u32; 0%u32 ]); - Return tt -. - -(** [array::take_all]: - Source: 'src/array.rs', lines 141:0-141:17 *) -Definition take_all : result unit := - _ <- take_array (mk_array u32 2%usize [ 0%u32; 0%u32 ]); - _ <- take_array (mk_array u32 2%usize [ 0%u32; 0%u32 ]); - _ <- take_array_borrow (mk_array u32 2%usize [ 0%u32; 0%u32 ]); - s <- array_to_slice u32 2%usize (mk_array u32 2%usize [ 0%u32; 0%u32 ]); - _ <- take_slice s; - p <- array_to_slice_mut u32 2%usize (mk_array u32 2%usize [ 0%u32; 0%u32 ]); - let (s1, to_slice_mut_back) := p in - s2 <- take_mut_slice s1; - _ <- to_slice_mut_back s2; - Return tt -. - -(** [array::index_array]: - Source: 'src/array.rs', lines 155:0-155:38 *) -Definition index_array (x : array u32 2%usize) : result u32 := - array_index_usize u32 2%usize x 0%usize -. - -(** [array::index_array_borrow]: - Source: 'src/array.rs', lines 158:0-158:46 *) -Definition index_array_borrow (x : array u32 2%usize) : result u32 := - array_index_usize u32 2%usize x 0%usize -. - -(** [array::index_slice_u32_0]: - Source: 'src/array.rs', lines 162:0-162:42 *) -Definition index_slice_u32_0 (x : slice u32) : result u32 := - slice_index_usize u32 x 0%usize -. - -(** [array::index_mut_slice_u32_0]: - Source: 'src/array.rs', lines 166:0-166:50 *) -Definition index_mut_slice_u32_0 - (x : slice u32) : result (u32 * (slice u32)) := - i <- slice_index_usize u32 x 0%usize; Return (i, x) -. - -(** [array::index_all]: - Source: 'src/array.rs', lines 170:0-170:25 *) -Definition index_all : result u32 := - i <- index_array (mk_array u32 2%usize [ 0%u32; 0%u32 ]); - i1 <- index_array (mk_array u32 2%usize [ 0%u32; 0%u32 ]); - i2 <- u32_add i i1; - i3 <- index_array_borrow (mk_array u32 2%usize [ 0%u32; 0%u32 ]); - i4 <- u32_add i2 i3; - s <- array_to_slice u32 2%usize (mk_array u32 2%usize [ 0%u32; 0%u32 ]); - i5 <- index_slice_u32_0 s; - i6 <- u32_add i4 i5; - p <- array_to_slice_mut u32 2%usize (mk_array u32 2%usize [ 0%u32; 0%u32 ]); - let (s1, to_slice_mut_back) := p in - p1 <- index_mut_slice_u32_0 s1; - let (i7, s2) := p1 in - i8 <- u32_add i6 i7; - _ <- to_slice_mut_back s2; - Return i8 -. - -(** [array::update_array]: - Source: 'src/array.rs', lines 184:0-184:36 *) -Definition update_array (x : array u32 2%usize) : result unit := - p <- array_index_mut_usize u32 2%usize x 0%usize; - let (_, index_mut_back) := p in - _ <- index_mut_back 1%u32; - Return tt -. - -(** [array::update_array_mut_borrow]: - Source: 'src/array.rs', lines 187:0-187:48 *) -Definition update_array_mut_borrow - (x : array u32 2%usize) : result (array u32 2%usize) := - p <- array_index_mut_usize u32 2%usize x 0%usize; - let (_, index_mut_back) := p in - index_mut_back 1%u32 -. - -(** [array::update_mut_slice]: - Source: 'src/array.rs', lines 190:0-190:38 *) -Definition update_mut_slice (x : slice u32) : result (slice u32) := - p <- slice_index_mut_usize u32 x 0%usize; - let (_, index_mut_back) := p in - index_mut_back 1%u32 -. - -(** [array::update_all]: - Source: 'src/array.rs', lines 194:0-194:19 *) -Definition update_all : result unit := - _ <- update_array (mk_array u32 2%usize [ 0%u32; 0%u32 ]); - _ <- update_array (mk_array u32 2%usize [ 0%u32; 0%u32 ]); - a <- update_array_mut_borrow (mk_array u32 2%usize [ 0%u32; 0%u32 ]); - p <- array_to_slice_mut u32 2%usize a; - let (s, to_slice_mut_back) := p in - s1 <- update_mut_slice s; - _ <- to_slice_mut_back s1; - Return tt -. - -(** [array::range_all]: - Source: 'src/array.rs', lines 205:0-205:18 *) -Definition range_all : result unit := - p <- - core_array_Array_index_mut u32 (core_ops_range_Range usize) 4%usize - (core_ops_index_IndexMutSliceTIInst u32 (core_ops_range_Range usize) - (core_slice_index_SliceIndexRangeUsizeSliceTInst u32)) - (mk_array u32 4%usize [ 0%u32; 0%u32; 0%u32; 0%u32 ]) - {| - core_ops_range_Range_start := 1%usize; - core_ops_range_Range_end_ := 3%usize - |}; - let (s, index_mut_back) := p in - s1 <- update_mut_slice s; - _ <- index_mut_back s1; - Return tt -. - -(** [array::deref_array_borrow]: - Source: 'src/array.rs', lines 214:0-214:46 *) -Definition deref_array_borrow (x : array u32 2%usize) : result u32 := - array_index_usize u32 2%usize x 0%usize -. - -(** [array::deref_array_mut_borrow]: - Source: 'src/array.rs', lines 219:0-219:54 *) -Definition deref_array_mut_borrow - (x : array u32 2%usize) : result (u32 * (array u32 2%usize)) := - i <- array_index_usize u32 2%usize x 0%usize; Return (i, x) -. - -(** [array::take_array_t]: - Source: 'src/array.rs', lines 227:0-227:31 *) -Definition take_array_t (a : array AB_t 2%usize) : result unit := - Return tt. - -(** [array::non_copyable_array]: - Source: 'src/array.rs', lines 229:0-229:27 *) -Definition non_copyable_array : result unit := - _ <- take_array_t (mk_array AB_t 2%usize [ AB_A; AB_B ]); Return tt -. - -(** [array::sum]: loop 0: - Source: 'src/array.rs', lines 242:0-250:1 *) -Fixpoint sum_loop - (n : nat) (s : slice u32) (sum1 : u32) (i : usize) : result u32 := - match n with - | O => Fail_ OutOfFuel - | S n1 => - let i1 := slice_len u32 s in - if i s< i1 - then ( - i2 <- slice_index_usize u32 s i; - sum3 <- u32_add sum1 i2; - i3 <- usize_add i 1%usize; - sum_loop n1 s sum3 i3) - else Return sum1 - end -. - -(** [array::sum]: - Source: 'src/array.rs', lines 242:0-242:28 *) -Definition sum (n : nat) (s : slice u32) : result u32 := - sum_loop n s 0%u32 0%usize -. - -(** [array::sum2]: loop 0: - Source: 'src/array.rs', lines 252:0-261:1 *) -Fixpoint sum2_loop - (n : nat) (s : slice u32) (s2 : slice u32) (sum1 : u32) (i : usize) : - result u32 - := - match n with - | O => Fail_ OutOfFuel - | S n1 => - let i1 := slice_len u32 s in - if i s< i1 - then ( - i2 <- slice_index_usize u32 s i; - i3 <- slice_index_usize u32 s2 i; - i4 <- u32_add i2 i3; - sum3 <- u32_add sum1 i4; - i5 <- usize_add i 1%usize; - sum2_loop n1 s s2 sum3 i5) - else Return sum1 - end -. - -(** [array::sum2]: - Source: 'src/array.rs', lines 252:0-252:41 *) -Definition sum2 (n : nat) (s : slice u32) (s2 : slice u32) : result u32 := - let i := slice_len u32 s in - let i1 := slice_len u32 s2 in - if negb (i s= i1) then Fail_ Failure else sum2_loop n s s2 0%u32 0%usize -. - -(** [array::f0]: - Source: 'src/array.rs', lines 263:0-263:11 *) -Definition f0 : result unit := - p <- array_to_slice_mut u32 2%usize (mk_array u32 2%usize [ 1%u32; 2%u32 ]); - let (s, to_slice_mut_back) := p in - p1 <- slice_index_mut_usize u32 s 0%usize; - let (_, index_mut_back) := p1 in - s1 <- index_mut_back 1%u32; - _ <- to_slice_mut_back s1; - Return tt -. - -(** [array::f1]: - Source: 'src/array.rs', lines 268:0-268:11 *) -Definition f1 : result unit := - p <- - array_index_mut_usize u32 2%usize (mk_array u32 2%usize [ 1%u32; 2%u32 ]) - 0%usize; - let (_, index_mut_back) := p in - _ <- index_mut_back 1%u32; - Return tt -. - -(** [array::f2]: - Source: 'src/array.rs', lines 273:0-273:17 *) -Definition f2 (i : u32) : result unit := - Return tt. - -(** [array::f4]: - Source: 'src/array.rs', lines 282:0-282:54 *) -Definition f4 - (x : array u32 32%usize) (y : usize) (z : usize) : result (slice u32) := - core_array_Array_index u32 (core_ops_range_Range usize) 32%usize - (core_ops_index_IndexSliceTIInst u32 (core_ops_range_Range usize) - (core_slice_index_SliceIndexRangeUsizeSliceTInst u32)) x - {| core_ops_range_Range_start := y; core_ops_range_Range_end_ := z |} -. - -(** [array::f3]: - Source: 'src/array.rs', lines 275:0-275:18 *) -Definition f3 (n : nat) : result u32 := - i <- - array_index_usize u32 2%usize (mk_array u32 2%usize [ 1%u32; 2%u32 ]) - 0%usize; - _ <- f2 i; - let b := array_repeat u32 32%usize 0%u32 in - s <- array_to_slice u32 2%usize (mk_array u32 2%usize [ 1%u32; 2%u32 ]); - s1 <- f4 b 16%usize 18%usize; - sum2 n s s1 -. - -(** [array::SZ] - Source: 'src/array.rs', lines 286:0-286:19 *) -Definition sz_body : result usize := Return 32%usize. -Definition sz_c : usize := sz_body%global. - -(** [array::f5]: - Source: 'src/array.rs', lines 289:0-289:31 *) -Definition f5 (x : array u32 32%usize) : result u32 := - array_index_usize u32 32%usize x 0%usize -. - -(** [array::ite]: - Source: 'src/array.rs', lines 294:0-294:12 *) -Definition ite : result unit := - p <- array_to_slice_mut u32 2%usize (mk_array u32 2%usize [ 0%u32; 0%u32 ]); - let (s, to_slice_mut_back) := p in - p1 <- index_mut_slice_u32_0 s; - let (_, s1) := p1 in - p2 <- array_to_slice_mut u32 2%usize (mk_array u32 2%usize [ 0%u32; 0%u32 ]); - let (s2, to_slice_mut_back1) := p2 in - p3 <- index_mut_slice_u32_0 s2; - let (_, s3) := p3 in - _ <- to_slice_mut_back1 s3; - _ <- to_slice_mut_back s1; - Return tt -. - -End Array. diff --git a/tests/coq/array/Makefile b/tests/coq/array/Makefile deleted file mode 100644 index 1a5aee4a..00000000 --- a/tests/coq/array/Makefile +++ /dev/null @@ -1,23 +0,0 @@ -# This file was automatically generated - modify ../Makefile.template instead -# Makefile originally taken from coq-club - -%: Makefile.coq phony - +make -f Makefile.coq $@ - -all: Makefile.coq - +make -f Makefile.coq all - -clean: Makefile.coq - +make -f Makefile.coq clean - rm -f Makefile.coq - -Makefile.coq: _CoqProject Makefile - coq_makefile -f _CoqProject | sed 's/$$(COQCHK) $$(COQCHKFLAGS) $$(COQLIBS)/$$(COQCHK) $$(COQCHKFLAGS) $$(subst -Q,-R,$$(COQLIBS))/' > Makefile.coq - -_CoqProject: ; - -Makefile: ; - -phony: ; - -.PHONY: all clean phony diff --git a/tests/coq/array/Primitives.v b/tests/coq/array/Primitives.v deleted file mode 100644 index 990e27e4..00000000 --- a/tests/coq/array/Primitives.v +++ /dev/null @@ -1,899 +0,0 @@ -Require Import Lia. -Require Coq.Strings.Ascii. -Require Coq.Strings.String. -Require Import Coq.Program.Equality. -Require Import Coq.ZArith.ZArith. -Require Import Coq.ZArith.Znat. -Require Import List. -Import ListNotations. - -Module Primitives. - - (* TODO: use more *) -Declare Scope Primitives_scope. - -(*** Result *) - -Inductive error := - | Failure - | OutOfFuel. - -Inductive result A := - | Return : A -> result A - | Fail_ : error -> result A. - -Arguments Return {_} a. -Arguments Fail_ {_}. - -Definition bind {A B} (m: result A) (f: A -> result B) : result B := - match m with - | Fail_ e => Fail_ e - | Return x => f x - end. - -Definition return_ {A: Type} (x: A) : result A := Return x. -Definition fail_ {A: Type} (e: error) : result A := Fail_ e. - -Notation "x <- c1 ; c2" := (bind c1 (fun x => c2)) - (at level 61, c1 at next level, right associativity). - -(** Monadic assert *) -Definition massert (b: bool) : result unit := - if b then Return tt else Fail_ Failure. - -(** Normalize and unwrap a successful result (used for globals) *) -Definition eval_result_refl {A} {x} (a: result A) (p: a = Return x) : A := - match a as r return (r = Return x -> A) with - | Return a' => fun _ => a' - | Fail_ e => fun p' => - False_rect _ (eq_ind (Fail_ e) - (fun e : result A => - match e with - | Return _ => False - | Fail_ e => True - end) - I (Return x) p') - end p. - -Notation "x %global" := (eval_result_refl x eq_refl) (at level 40). -Notation "x %return" := (eval_result_refl x eq_refl) (at level 40). - -(* Sanity check *) -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 core_mem_replace (a : Type) (x : a) (y : a) : a * a := (x, x) . - -Record mut_raw_ptr (T : Type) := { mut_raw_ptr_v : T }. -Record const_raw_ptr (T : Type) := { const_raw_ptr_v : T }. - -(*** Scalars *) - -Definition i8_min : Z := -128%Z. -Definition i8_max : Z := 127%Z. -Definition i16_min : Z := -32768%Z. -Definition i16_max : Z := 32767%Z. -Definition i32_min : Z := -2147483648%Z. -Definition i32_max : Z := 2147483647%Z. -Definition i64_min : Z := -9223372036854775808%Z. -Definition i64_max : Z := 9223372036854775807%Z. -Definition i128_min : Z := -170141183460469231731687303715884105728%Z. -Definition i128_max : Z := 170141183460469231731687303715884105727%Z. -Definition u8_min : Z := 0%Z. -Definition u8_max : Z := 255%Z. -Definition u16_min : Z := 0%Z. -Definition u16_max : Z := 65535%Z. -Definition u32_min : Z := 0%Z. -Definition u32_max : Z := 4294967295%Z. -Definition u64_min : Z := 0%Z. -Definition u64_max : Z := 18446744073709551615%Z. -Definition u128_min : Z := 0%Z. -Definition u128_max : Z := 340282366920938463463374607431768211455%Z. - -(** The bounds of [isize] and [usize] vary with the architecture. *) -Axiom isize_min : Z. -Axiom isize_max : Z. -Definition usize_min : Z := 0%Z. -Axiom usize_max : Z. - -Open Scope Z_scope. - -(** We provide those lemmas to reason about the bounds of [isize] and [usize] *) -Axiom isize_min_bound : isize_min <= i32_min. -Axiom isize_max_bound : i32_max <= isize_max. -Axiom usize_max_bound : u32_max <= usize_max. - -Inductive scalar_ty := - | Isize - | I8 - | I16 - | I32 - | I64 - | I128 - | Usize - | U8 - | U16 - | U32 - | U64 - | U128 -. - -Definition scalar_min (ty: scalar_ty) : Z := - match ty with - | Isize => isize_min - | I8 => i8_min - | I16 => i16_min - | I32 => i32_min - | I64 => i64_min - | I128 => i128_min - | Usize => usize_min - | U8 => u8_min - | U16 => u16_min - | U32 => u32_min - | U64 => u64_min - | U128 => u128_min -end. - -Definition scalar_max (ty: scalar_ty) : Z := - match ty with - | Isize => isize_max - | I8 => i8_max - | I16 => i16_max - | I32 => i32_max - | I64 => i64_max - | I128 => i128_max - | Usize => usize_max - | U8 => u8_max - | U16 => u16_max - | U32 => u32_max - | U64 => u64_max - | U128 => u128_max -end. - -(** We use the following conservative bounds to make sure we can compute bound - checks in most situations *) -Definition scalar_min_cons (ty: scalar_ty) : Z := - match ty with - | Isize => i32_min - | Usize => u32_min - | _ => scalar_min ty -end. - -Definition scalar_max_cons (ty: scalar_ty) : Z := - match ty with - | Isize => i32_max - | Usize => u32_max - | _ => scalar_max ty -end. - -Lemma scalar_min_cons_valid : forall ty, scalar_min ty <= scalar_min_cons ty . -Proof. - destruct ty; unfold scalar_min_cons, scalar_min; try lia. - - pose isize_min_bound; lia. - - apply Z.le_refl. -Qed. - -Lemma scalar_max_cons_valid : forall ty, scalar_max ty >= scalar_max_cons ty . -Proof. - destruct ty; unfold scalar_max_cons, scalar_max; try lia. - - pose isize_max_bound; lia. - - pose usize_max_bound. lia. -Qed. - -Definition scalar (ty: scalar_ty) : Type := - { x: Z | scalar_min ty <= x <= scalar_max ty }. - -Definition to_Z {ty} (x: scalar ty) : Z := proj1_sig x. - -(** Bounds checks: we start by using the conservative bounds, to make sure we - can compute in most situations, then we use the real bounds (for [isize] - and [usize]). *) -Definition scalar_ge_min (ty: scalar_ty) (x: Z) : bool := - Z.leb (scalar_min_cons ty) x || Z.leb (scalar_min ty) x. - -Definition scalar_le_max (ty: scalar_ty) (x: Z) : bool := - Z.leb x (scalar_max_cons ty) || Z.leb x (scalar_max ty). - -Lemma scalar_ge_min_valid (ty: scalar_ty) (x: Z) : - scalar_ge_min ty x = true -> scalar_min ty <= x . -Proof. - unfold scalar_ge_min. - pose (scalar_min_cons_valid ty). - lia. -Qed. - -Lemma scalar_le_max_valid (ty: scalar_ty) (x: Z) : - scalar_le_max ty x = true -> x <= scalar_max ty . -Proof. - unfold scalar_le_max. - pose (scalar_max_cons_valid ty). - lia. -Qed. - -Definition scalar_in_bounds (ty: scalar_ty) (x: Z) : bool := - scalar_ge_min ty x && scalar_le_max ty x . - -Lemma scalar_in_bounds_valid (ty: scalar_ty) (x: Z) : - scalar_in_bounds ty x = true -> scalar_min ty <= x <= scalar_max ty . -Proof. - unfold scalar_in_bounds. - intros H. - destruct (scalar_ge_min ty x) eqn:Hmin. - - destruct (scalar_le_max ty x) eqn:Hmax. - + pose (scalar_ge_min_valid ty x Hmin). - pose (scalar_le_max_valid ty x Hmax). - lia. - + inversion H. - - inversion H. -Qed. - -Import Sumbool. - -Definition mk_scalar (ty: scalar_ty) (x: Z) : result (scalar ty) := - match sumbool_of_bool (scalar_in_bounds ty x) with - | left H => Return (exist _ x (scalar_in_bounds_valid _ _ H)) - | right _ => Fail_ Failure - end. - -Definition scalar_add {ty} (x y: scalar ty) : result (scalar ty) := mk_scalar ty (to_Z x + to_Z y). - -Definition scalar_sub {ty} (x y: scalar ty) : result (scalar ty) := mk_scalar ty (to_Z x - to_Z y). - -Definition scalar_mul {ty} (x y: scalar ty) : result (scalar ty) := mk_scalar ty (to_Z x * to_Z y). - -Definition scalar_div {ty} (x y: scalar ty) : result (scalar ty) := - if to_Z y =? 0 then Fail_ Failure else - mk_scalar ty (to_Z x / to_Z y). - -Definition scalar_rem {ty} (x y: scalar ty) : result (scalar ty) := mk_scalar ty (Z.rem (to_Z x) (to_Z y)). - -Definition scalar_neg {ty} (x: scalar ty) : result (scalar ty) := mk_scalar ty (-(to_Z x)). - -Axiom scalar_xor : forall ty, scalar ty -> scalar ty -> scalar ty. (* TODO *) -Axiom scalar_or : forall ty, scalar ty -> scalar ty -> scalar ty. (* TODO *) -Axiom scalar_and : forall ty, scalar ty -> scalar ty -> scalar ty. (* TODO *) -Axiom scalar_shl : forall ty0 ty1, scalar ty0 -> scalar ty1 -> result (scalar ty0). (* TODO *) -Axiom scalar_shr : forall ty0 ty1, scalar ty0 -> scalar ty1 -> result (scalar ty0). (* TODO *) - -(** Cast an integer from a [src_ty] to a [tgt_ty] *) -(* TODO: check the semantics of casts in Rust *) -Definition scalar_cast (src_ty tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) := - mk_scalar tgt_ty (to_Z x). - -(* This can't fail, but for now we make all casts faillible (easier for the translation) *) -Definition scalar_cast_bool (tgt_ty : scalar_ty) (x : bool) : result (scalar tgt_ty) := - mk_scalar tgt_ty (if x then 1 else 0). - -(** Comparisons *) -Definition scalar_leb {ty : scalar_ty} (x : scalar ty) (y : scalar ty) : bool := - Z.leb (to_Z x) (to_Z y) . - -Definition scalar_ltb {ty : scalar_ty} (x : scalar ty) (y : scalar ty) : bool := - Z.ltb (to_Z x) (to_Z y) . - -Definition scalar_geb {ty : scalar_ty} (x : scalar ty) (y : scalar ty) : bool := - Z.geb (to_Z x) (to_Z y) . - -Definition scalar_gtb {ty : scalar_ty} (x : scalar ty) (y : scalar ty) : bool := - Z.gtb (to_Z x) (to_Z y) . - -Definition scalar_eqb {ty : scalar_ty} (x : scalar ty) (y : scalar ty) : bool := - Z.eqb (to_Z x) (to_Z y) . - -Definition scalar_neqb {ty : scalar_ty} (x : scalar ty) (y : scalar ty) : bool := - negb (Z.eqb (to_Z x) (to_Z y)) . - - -(** The scalar types *) -Definition isize := scalar Isize. -Definition i8 := scalar I8. -Definition i16 := scalar I16. -Definition i32 := scalar I32. -Definition i64 := scalar I64. -Definition i128 := scalar I128. -Definition usize := scalar Usize. -Definition u8 := scalar U8. -Definition u16 := scalar U16. -Definition u32 := scalar U32. -Definition u64 := scalar U64. -Definition u128 := scalar U128. - -(** Negaion *) -Definition isize_neg := @scalar_neg Isize. -Definition i8_neg := @scalar_neg I8. -Definition i16_neg := @scalar_neg I16. -Definition i32_neg := @scalar_neg I32. -Definition i64_neg := @scalar_neg I64. -Definition i128_neg := @scalar_neg I128. - -(** Division *) -Definition isize_div := @scalar_div Isize. -Definition i8_div := @scalar_div I8. -Definition i16_div := @scalar_div I16. -Definition i32_div := @scalar_div I32. -Definition i64_div := @scalar_div I64. -Definition i128_div := @scalar_div I128. -Definition usize_div := @scalar_div Usize. -Definition u8_div := @scalar_div U8. -Definition u16_div := @scalar_div U16. -Definition u32_div := @scalar_div U32. -Definition u64_div := @scalar_div U64. -Definition u128_div := @scalar_div U128. - -(** Remainder *) -Definition isize_rem := @scalar_rem Isize. -Definition i8_rem := @scalar_rem I8. -Definition i16_rem := @scalar_rem I16. -Definition i32_rem := @scalar_rem I32. -Definition i64_rem := @scalar_rem I64. -Definition i128_rem := @scalar_rem I128. -Definition usize_rem := @scalar_rem Usize. -Definition u8_rem := @scalar_rem U8. -Definition u16_rem := @scalar_rem U16. -Definition u32_rem := @scalar_rem U32. -Definition u64_rem := @scalar_rem U64. -Definition u128_rem := @scalar_rem U128. - -(** Addition *) -Definition isize_add := @scalar_add Isize. -Definition i8_add := @scalar_add I8. -Definition i16_add := @scalar_add I16. -Definition i32_add := @scalar_add I32. -Definition i64_add := @scalar_add I64. -Definition i128_add := @scalar_add I128. -Definition usize_add := @scalar_add Usize. -Definition u8_add := @scalar_add U8. -Definition u16_add := @scalar_add U16. -Definition u32_add := @scalar_add U32. -Definition u64_add := @scalar_add U64. -Definition u128_add := @scalar_add U128. - -(** Substraction *) -Definition isize_sub := @scalar_sub Isize. -Definition i8_sub := @scalar_sub I8. -Definition i16_sub := @scalar_sub I16. -Definition i32_sub := @scalar_sub I32. -Definition i64_sub := @scalar_sub I64. -Definition i128_sub := @scalar_sub I128. -Definition usize_sub := @scalar_sub Usize. -Definition u8_sub := @scalar_sub U8. -Definition u16_sub := @scalar_sub U16. -Definition u32_sub := @scalar_sub U32. -Definition u64_sub := @scalar_sub U64. -Definition u128_sub := @scalar_sub U128. - -(** Multiplication *) -Definition isize_mul := @scalar_mul Isize. -Definition i8_mul := @scalar_mul I8. -Definition i16_mul := @scalar_mul I16. -Definition i32_mul := @scalar_mul I32. -Definition i64_mul := @scalar_mul I64. -Definition i128_mul := @scalar_mul I128. -Definition usize_mul := @scalar_mul Usize. -Definition u8_mul := @scalar_mul U8. -Definition u16_mul := @scalar_mul U16. -Definition u32_mul := @scalar_mul U32. -Definition u64_mul := @scalar_mul U64. -Definition u128_mul := @scalar_mul U128. - -(** Xor *) -Definition u8_xor := @scalar_xor U8. -Definition u16_xor := @scalar_xor U16. -Definition u32_xor := @scalar_xor U32. -Definition u64_xor := @scalar_xor U64. -Definition u128_xor := @scalar_xor U128. -Definition usize_xor := @scalar_xor Usize. -Definition i8_xor := @scalar_xor I8. -Definition i16_xor := @scalar_xor I16. -Definition i32_xor := @scalar_xor I32. -Definition i64_xor := @scalar_xor I64. -Definition i128_xor := @scalar_xor I128. -Definition isize_xor := @scalar_xor Isize. - -(** Or *) -Definition u8_or := @scalar_or U8. -Definition u16_or := @scalar_or U16. -Definition u32_or := @scalar_or U32. -Definition u64_or := @scalar_or U64. -Definition u128_or := @scalar_or U128. -Definition usize_or := @scalar_or Usize. -Definition i8_or := @scalar_or I8. -Definition i16_or := @scalar_or I16. -Definition i32_or := @scalar_or I32. -Definition i64_or := @scalar_or I64. -Definition i128_or := @scalar_or I128. -Definition isize_or := @scalar_or Isize. - -(** And *) -Definition u8_and := @scalar_and U8. -Definition u16_and := @scalar_and U16. -Definition u32_and := @scalar_and U32. -Definition u64_and := @scalar_and U64. -Definition u128_and := @scalar_and U128. -Definition usize_and := @scalar_and Usize. -Definition i8_and := @scalar_and I8. -Definition i16_and := @scalar_and I16. -Definition i32_and := @scalar_and I32. -Definition i64_and := @scalar_and I64. -Definition i128_and := @scalar_and I128. -Definition isize_and := @scalar_and Isize. - -(** Shift left *) -Definition u8_shl {ty} := @scalar_shl U8 ty. -Definition u16_shl {ty} := @scalar_shl U16 ty. -Definition u32_shl {ty} := @scalar_shl U32 ty. -Definition u64_shl {ty} := @scalar_shl U64 ty. -Definition u128_shl {ty} := @scalar_shl U128 ty. -Definition usize_shl {ty} := @scalar_shl Usize ty. -Definition i8_shl {ty} := @scalar_shl I8 ty. -Definition i16_shl {ty} := @scalar_shl I16 ty. -Definition i32_shl {ty} := @scalar_shl I32 ty. -Definition i64_shl {ty} := @scalar_shl I64 ty. -Definition i128_shl {ty} := @scalar_shl I128 ty. -Definition isize_shl {ty} := @scalar_shl Isize ty. - -(** Shift right *) -Definition u8_shr {ty} := @scalar_shr U8 ty. -Definition u16_shr {ty} := @scalar_shr U16 ty. -Definition u32_shr {ty} := @scalar_shr U32 ty. -Definition u64_shr {ty} := @scalar_shr U64 ty. -Definition u128_shr {ty} := @scalar_shr U128 ty. -Definition usize_shr {ty} := @scalar_shr Usize ty. -Definition i8_shr {ty} := @scalar_shr I8 ty. -Definition i16_shr {ty} := @scalar_shr I16 ty. -Definition i32_shr {ty} := @scalar_shr I32 ty. -Definition i64_shr {ty} := @scalar_shr I64 ty. -Definition i128_shr {ty} := @scalar_shr I128 ty. -Definition isize_shr {ty} := @scalar_shr Isize ty. - -(** Small utility *) -Definition usize_to_nat (x: usize) : nat := Z.to_nat (to_Z x). - -(** Notations *) -Notation "x %isize" := ((mk_scalar Isize x)%return) (at level 9). -Notation "x %i8" := ((mk_scalar I8 x)%return) (at level 9). -Notation "x %i16" := ((mk_scalar I16 x)%return) (at level 9). -Notation "x %i32" := ((mk_scalar I32 x)%return) (at level 9). -Notation "x %i64" := ((mk_scalar I64 x)%return) (at level 9). -Notation "x %i128" := ((mk_scalar I128 x)%return) (at level 9). -Notation "x %usize" := ((mk_scalar Usize x)%return) (at level 9). -Notation "x %u8" := ((mk_scalar U8 x)%return) (at level 9). -Notation "x %u16" := ((mk_scalar U16 x)%return) (at level 9). -Notation "x %u32" := ((mk_scalar U32 x)%return) (at level 9). -Notation "x %u64" := ((mk_scalar U64 x)%return) (at level 9). -Notation "x %u128" := ((mk_scalar U128 x)%return) (at level 9). - -Notation "x s= y" := (scalar_eqb x y) (at level 80) : Primitives_scope. -Notation "x s<> y" := (scalar_neqb x y) (at level 80) : Primitives_scope. -Notation "x s<= y" := (scalar_leb x y) (at level 80) : Primitives_scope. -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. - -(** 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_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 {_ _}. - -(* 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_derefInst.(core_ops_deref_Deref_target) -> result Self)); -}. -Arguments mk_core_ops_deref_DerefMut {_}. -Arguments core_ops_deref_DerefMut_derefInst {_}. -Arguments core_ops_deref_DerefMut_deref_mut {_}. - -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 * (T -> result T)) := - Return (x, fun x => 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; -|}. - - -(*** 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. - pose (H := usize_max_bound). - unfold u32_max in H. - 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. - -(* 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). - -Definition array_index_mut_usize (T : Type) (n : usize) (a : array T n) (i : usize) : - result (T * (T -> result (array T n))) := - match array_index_usize T n a i with - | Fail_ e => Fail_ e - | Return x => Return (x, array_update_usize T n a i) - end. - -(*** 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_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). - -Definition slice_index_mut_usize (T : Type) (s : slice T) (i : usize) : - result (T * (T -> result (slice T))) := - match slice_index_usize T s i with - | Fail_ e => Fail_ e - | Return x => Return (x, slice_update_usize T s i) - end. - -(*** Subslices *) - -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). - -Definition array_to_slice_mut (T : Type) (n : usize) (a : array T n) : - result (slice T * (slice T -> result (array T n))) := - match array_to_slice T n a with - | Fail_ e => Fail_ e - | Return x => Return (x, array_from_slice T n a) - end. - -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 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 alloc_vec_Vec T := { l: list T | Z.of_nat (length l) <= usize_max }. - -Definition alloc_vec_Vec_to_list {T: Type} (v: alloc_vec_Vec T) : list T := proj1_sig 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 alloc_vec_Vec_new (T: Type) : alloc_vec_Vec T := (exist _ [] le_0_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 alloc_vec_Vec_length, usize_min. - split. - - lia. - - apply (proj2_sig v). -Qed. - -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 := - match l with - | [] => [] - | x :: t => match n with - | 0%nat => a :: t - | S m => x :: (list_update t m a) -end end. - -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. - -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])). - -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). - -(* 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). - -Definition alloc_vec_Vec_index_mut_usize {T : Type} (v: alloc_vec_Vec T) (i: usize) : - result (T * (T -> result (alloc_vec_Vec T))) := - match alloc_vec_Vec_index_usize v i with - | Return x => - Return (x, alloc_vec_Vec_update_usize v i) - | Fail_ e => Fail_ e - end. - -(* 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 * (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_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_unchecked {_ _}. -Arguments core_slice_index_SliceIndex_get_unchecked_mut {_ _}. -Arguments core_slice_index_SliceIndex_index {_ _}. -Arguments core_slice_index_SliceIndex_index_mut {_ _}. - -(* [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. - -(* [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) * (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 * (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) * - (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) * - (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_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; -|}. - -(* 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; -|}. - -(* 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::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 * (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 * (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_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; -|}. - -(* [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) * - (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; -|}. - -(*** 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_mut_usize v i. - -End Primitives. diff --git a/tests/coq/array/_CoqProject b/tests/coq/array/_CoqProject deleted file mode 100644 index 87d8fc3d..00000000 --- a/tests/coq/array/_CoqProject +++ /dev/null @@ -1,7 +0,0 @@ -# This file was automatically generated - see ../Makefile --R . Lib --arg -w --arg all - -Primitives.v -Array.v |