diff options
Diffstat (limited to 'tests/coq')
| -rw-r--r-- | tests/coq/Makefile | 3 | ||||
| -rw-r--r-- | tests/coq/misc/Constants.v | 138 | ||||
| -rw-r--r-- | tests/coq/misc/External__Funs.v | 100 | ||||
| -rw-r--r-- | tests/coq/misc/External__Opaque.v | 36 | ||||
| -rw-r--r-- | tests/coq/misc/External__Types.v | 15 | ||||
| -rw-r--r-- | tests/coq/misc/Makefile | 22 | ||||
| -rw-r--r-- | tests/coq/misc/NoNestedBorrows.v | 510 | ||||
| -rw-r--r-- | tests/coq/misc/Paper.v | 114 | ||||
| -rw-r--r-- | tests/coq/misc/Primitives.v | 478 | ||||
| -rw-r--r-- | tests/coq/misc/_CoqProject | 12 |
10 files changed, 1428 insertions, 0 deletions
diff --git a/tests/coq/Makefile b/tests/coq/Makefile new file mode 100644 index 00000000..5fead9c9 --- /dev/null +++ b/tests/coq/Makefile @@ -0,0 +1,3 @@ +# TODO: make this more general +all: + cd misc && $(MAKE) all diff --git a/tests/coq/misc/Constants.v b/tests/coq/misc/Constants.v new file mode 100644 index 00000000..677aae8c --- /dev/null +++ b/tests/coq/misc/Constants.v @@ -0,0 +1,138 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [constants] *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Local Open Scope Primitives_scope. +Module Constants . + +(** [constants::X0] *) +Definition x0_body : result u32 := Return (0 %u32) . +Definition x0_c : u32 := x0_body%global . + +(** [core::num::u32::{9}::MAX] *) +Definition core_num_u32_max_body : result u32 := Return (4294967295 %u32) . +Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global . + +(** [constants::X1] *) +Definition x1_body : result u32 := Return core_num_u32_max_c . +Definition x1_c : u32 := x1_body%global . + +(** [constants::X2] *) +Definition x2_body : result u32 := Return (3 %u32) . +Definition x2_c : u32 := x2_body%global . + +(** [constants::incr] *) +Definition incr_fwd (n : u32) : result u32 := i <- u32_add n 1 %u32; Return i . + +(** [constants::X3] *) +Definition x3_body : result u32 := i <- incr_fwd (32 %u32); Return i . +Definition x3_c : u32 := x3_body%global . + +(** [constants::mk_pair0] *) +Definition mk_pair0_fwd (x : u32) (y : u32) : result (u32 * u32) := + Return (x, y) . + +(** [constants::Pair] *) +Record Pair_t (T1 T2 : Type) := mkPair_t { Pair_x : T1; Pair_y : T2; } . + +Arguments mkPair_t {T1} {T2} _ _ . +Arguments Pair_x {T1} {T2} . +Arguments Pair_y {T1} {T2} . + +(** [constants::mk_pair1] *) +Definition mk_pair1_fwd (x : u32) (y : u32) : result (Pair_t u32 u32) := + Return (mkPair_t x y) . + +(** [constants::P0] *) +Definition p0_body : result (u32 * u32) := + p <- mk_pair0_fwd (0 %u32) (1 %u32); Return p + . +Definition p0_c : (u32 * u32) := p0_body%global . + +(** [constants::P1] *) +Definition p1_body : result (Pair_t u32 u32) := + p <- mk_pair1_fwd (0 %u32) (1 %u32); Return p + . +Definition p1_c : Pair_t u32 u32 := p1_body%global . + +(** [constants::P2] *) +Definition p2_body : result (u32 * u32) := Return (0 %u32, 1 %u32) . +Definition p2_c : (u32 * u32) := p2_body%global . + +(** [constants::P3] *) +Definition p3_body : result (Pair_t u32 u32) := + Return (mkPair_t (0 %u32) (1 %u32)) + . +Definition p3_c : Pair_t u32 u32 := p3_body%global . + +(** [constants::Wrap] *) +Record Wrap_t (T : Type) := mkWrap_t { Wrap_val : T; } . + +Arguments mkWrap_t {T} _ . +Arguments Wrap_val {T} . + +(** [constants::Wrap::{0}::new] *) +Definition wrap_new_fwd (T : Type) (val : T) : result (Wrap_t T) := + Return (mkWrap_t val) . + +(** [constants::Y] *) +Definition y_body : result (Wrap_t i32) := + w <- wrap_new_fwd i32 (2 %i32); Return w + . +Definition y_c : Wrap_t i32 := y_body%global . + +(** [constants::unwrap_y] *) +Definition unwrap_y_fwd : result i32 := + match y_c with | mkWrap_t i => Return i end . + +(** [constants::YVAL] *) +Definition yval_body : result i32 := i <- unwrap_y_fwd; Return i . +Definition yval_c : i32 := yval_body%global . + +(** [constants::get_z1::Z1] *) +Definition get_z1_z1_body : result i32 := Return (3 %i32) . +Definition get_z1_z1_c : i32 := get_z1_z1_body%global . + +(** [constants::get_z1] *) +Definition get_z1_fwd : result i32 := Return get_z1_z1_c . + +(** [constants::add] *) +Definition add_fwd (a : i32) (b : i32) : result i32 := + i <- i32_add a b; Return i . + +(** [constants::Q1] *) +Definition q1_body : result i32 := Return (5 %i32) . +Definition q1_c : i32 := q1_body%global . + +(** [constants::Q2] *) +Definition q2_body : result i32 := Return q1_c . +Definition q2_c : i32 := q2_body%global . + +(** [constants::Q3] *) +Definition q3_body : result i32 := i <- add_fwd q2_c (3 %i32); Return i . +Definition q3_c : i32 := q3_body%global . + +(** [constants::get_z2] *) +Definition get_z2_fwd : result i32 := + i <- get_z1_fwd; i0 <- add_fwd i q3_c; i1 <- add_fwd q1_c i0; Return i1 . + +(** [constants::S1] *) +Definition s1_body : result u32 := Return (6 %u32) . +Definition s1_c : u32 := s1_body%global . + +(** [constants::S2] *) +Definition s2_body : result u32 := i <- incr_fwd s1_c; Return i . +Definition s2_c : u32 := s2_body%global . + +(** [constants::S3] *) +Definition s3_body : result (Pair_t u32 u32) := Return p3_c . +Definition s3_c : Pair_t u32 u32 := s3_body%global . + +(** [constants::S4] *) +Definition s4_body : result (Pair_t u32 u32) := + p <- mk_pair1_fwd (7 %u32) (8 %u32); Return p + . +Definition s4_c : Pair_t u32 u32 := s4_body%global . + +End Constants . diff --git a/tests/coq/misc/External__Funs.v b/tests/coq/misc/External__Funs.v new file mode 100644 index 00000000..77b738b0 --- /dev/null +++ b/tests/coq/misc/External__Funs.v @@ -0,0 +1,100 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [external]: function definitions *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Local Open Scope Primitives_scope. +Require Export External__Types . +Import External__Types . +Require Export External__Opaque . +Import External__Opaque . +Module External__Funs . + +(** [external::swap] *) +Definition swap_fwd + (T : Type) (x : T) (y : T) (st : state) : result (state * unit) := + p <- core_mem_swap_fwd T x y st; + let (st0, _) := p in + p0 <- core_mem_swap_back0 T x y st st0; + let (st1, _) := p0 in + p1 <- core_mem_swap_back1 T x y st st1; + let (st2, _) := p1 in Return (st2, tt) + . + +(** [external::swap] *) +Definition swap_back + (T : Type) (x : T) (y : T) (st : state) (st0 : state) : + result (state * (T * T)) + := + p <- core_mem_swap_fwd T x y st; + let (st1, _) := p in + p0 <- core_mem_swap_back0 T x y st st1; + let (st2, x0) := p0 in + p1 <- core_mem_swap_back1 T x y st st2; + let (_, y0) := p1 in Return (st0, (x0, y0)) + . + +(** [external::test_new_non_zero_u32] *) +Definition test_new_non_zero_u32_fwd + (x : u32) (st : state) : result (state * Core_num_nonzero_non_zero_u32_t) := + p <- core_num_nonzero_non_zero_u32_new_fwd x st; + let (st0, opt) := p in + p0 <- core_option_option_unwrap_fwd Core_num_nonzero_non_zero_u32_t opt st0; + let (st1, nzu) := p0 in Return (st1, nzu) + . + +(** [external::test_vec] *) +Definition test_vec_fwd : result unit := + let v := vec_new u32 in + v0 <- vec_push_back u32 v (0 %u32); let _ := v0 in Return tt + . + +(** [external::custom_swap] *) +Definition custom_swap_fwd + (T : Type) (x : T) (y : T) (st : state) : result (state * T) := + p <- core_mem_swap_fwd T x y st; + let (st0, _) := p in + p0 <- core_mem_swap_back0 T x y st st0; + let (st1, x0) := p0 in + p1 <- core_mem_swap_back1 T x y st st1; + let (st2, _) := p1 in Return (st2, x0) + . + +(** [external::custom_swap] *) +Definition custom_swap_back + (T : Type) (x : T) (y : T) (st : state) (ret : T) (st0 : state) : + result (state * (T * T)) + := + p <- core_mem_swap_fwd T x y st; + let (st1, _) := p in + p0 <- core_mem_swap_back0 T x y st st1; + let (st2, _) := p0 in + p1 <- core_mem_swap_back1 T x y st st2; + let (_, y0) := p1 in Return (st0, (ret, y0)) + . + +(** [external::test_custom_swap] *) +Definition test_custom_swap_fwd + (x : u32) (y : u32) (st : state) : result (state * unit) := + p <- custom_swap_fwd u32 x y st; let (st0, _) := p in Return (st0, tt) . + +(** [external::test_custom_swap] *) +Definition test_custom_swap_back + (x : u32) (y : u32) (st : state) (st0 : state) : + result (state * (u32 * u32)) + := + p <- custom_swap_back u32 x y st (1 %u32) st0; + let (st1, tmp) := p in + let (x0, y0) := tmp in Return (st1, (x0, y0)) + . + +(** [external::test_swap_non_zero] *) +Definition test_swap_non_zero_fwd + (x : u32) (st : state) : result (state * u32) := + p <- swap_fwd u32 x (0 %u32) st; + let (st0, _) := p in + p0 <- swap_back u32 x (0 %u32) st st0; + let (st1, (x0, _)) := p0 in if x0 s= 0 %u32 then Fail_ else Return (st1, x0) + . + +End External__Funs . diff --git a/tests/coq/misc/External__Opaque.v b/tests/coq/misc/External__Opaque.v new file mode 100644 index 00000000..19111a37 --- /dev/null +++ b/tests/coq/misc/External__Opaque.v @@ -0,0 +1,36 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [external]: opaque function definitions *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Local Open Scope Primitives_scope. +Require Export External__Types . +Import External__Types . +Module External__Opaque . + +(** [core::mem::swap] *) +Axiom core_mem_swap_fwd : + forall(T : Type) , T -> T -> state -> result (state * unit) + . + +(** [core::mem::swap] *) +Axiom core_mem_swap_back0 : + forall(T : Type) , T -> T -> state -> state -> result (state * T) + . + +(** [core::mem::swap] *) +Axiom core_mem_swap_back1 : + forall(T : Type) , T -> T -> state -> state -> result (state * T) + . + +(** [core::num::nonzero::NonZeroU32::{14}::new] *) +Axiom core_num_nonzero_non_zero_u32_new_fwd + : u32 -> state -> result (state * (option Core_num_nonzero_non_zero_u32_t)) + . + +(** [core::option::Option::{0}::unwrap] *) +Axiom core_option_option_unwrap_fwd : + forall(T : Type) , option T -> state -> result (state * T) + . + +End External__Opaque . diff --git a/tests/coq/misc/External__Types.v b/tests/coq/misc/External__Types.v new file mode 100644 index 00000000..1513ec4a --- /dev/null +++ b/tests/coq/misc/External__Types.v @@ -0,0 +1,15 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [external]: type definitions *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Local Open Scope Primitives_scope. +Module External__Types . + +(** [core::num::nonzero::NonZeroU32] *) +Axiom Core_num_nonzero_non_zero_u32_t : Type . + +(** The state type used in the state-error monad *) +Axiom state : Type. + +End External__Types . diff --git a/tests/coq/misc/Makefile b/tests/coq/misc/Makefile new file mode 100644 index 00000000..ff1ccd39 --- /dev/null +++ b/tests/coq/misc/Makefile @@ -0,0 +1,22 @@ +# 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/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v new file mode 100644 index 00000000..6dc41204 --- /dev/null +++ b/tests/coq/misc/NoNestedBorrows.v @@ -0,0 +1,510 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [no_nested_borrows] *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Local Open Scope Primitives_scope. +Module NoNestedBorrows . + +(** [no_nested_borrows::Pair] *) +Record Pair_t (T1 T2 : Type) := mkPair_t { Pair_x : T1; Pair_y : T2; } . + +Arguments mkPair_t {T1} {T2} _ _ . +Arguments Pair_x {T1} {T2} . +Arguments Pair_y {T1} {T2} . + +(** [no_nested_borrows::List] *) +Inductive List_t (T : Type) := +| ListCons : T -> List_t T -> List_t T +| ListNil : List_t T +. + +Arguments ListCons {T} _ _ . +Arguments ListNil {T} . + +(** [no_nested_borrows::One] *) +Inductive One_t (T1 : Type) := | OneOne : T1 -> One_t T1 . + +Arguments OneOne {T1} _ . + +(** [no_nested_borrows::EmptyEnum] *) +Inductive Empty_enum_t := | EmptyEnumEmpty : Empty_enum_t . + +Arguments EmptyEnumEmpty . + +(** [no_nested_borrows::Enum] *) +Inductive Enum_t := | EnumVariant1 : Enum_t | EnumVariant2 : Enum_t . + +Arguments EnumVariant1 . +Arguments EnumVariant2 . + +(** [no_nested_borrows::EmptyStruct] *) +Record Empty_struct_t := mkEmpty_struct_t { } . + +Arguments mkEmpty_struct_t . + +(** [no_nested_borrows::Sum] *) +Inductive Sum_t (T1 T2 : Type) := +| SumLeft : T1 -> Sum_t T1 T2 +| SumRight : T2 -> Sum_t T1 T2 +. + +Arguments SumLeft {T1} {T2} _ . +Arguments SumRight {T1} {T2} _ . + +(** [no_nested_borrows::neg_test] *) +Definition neg_test_fwd (x : i32) : result i32 := i <- i32_neg x; Return i . + +(** [no_nested_borrows::add_test] *) +Definition add_test_fwd (x : u32) (y : u32) : result u32 := + i <- u32_add x y; Return i . + +(** [no_nested_borrows::subs_test] *) +Definition subs_test_fwd (x : u32) (y : u32) : result u32 := + i <- u32_sub x y; Return i . + +(** [no_nested_borrows::div_test] *) +Definition div_test_fwd (x : u32) (y : u32) : result u32 := + i <- u32_div x y; Return i . + +(** [no_nested_borrows::div_test1] *) +Definition div_test1_fwd (x : u32) : result u32 := + i <- u32_div x 2 %u32; Return i . + +(** [no_nested_borrows::rem_test] *) +Definition rem_test_fwd (x : u32) (y : u32) : result u32 := + i <- u32_rem x y; Return i . + +(** [no_nested_borrows::cast_test] *) +Definition cast_test_fwd (x : u32) : result i32 := + i <- scalar_cast U32 I32 x; Return i . + +(** [no_nested_borrows::test2] *) +Definition test2_fwd : result unit := + i <- u32_add 23 %u32 44 %u32; let _ := i in Return tt . + +(** Unit test for [no_nested_borrows::test2] *) +Check (test2_fwd )%return. + +(** [no_nested_borrows::get_max] *) +Definition get_max_fwd (x : u32) (y : u32) : result u32 := + if x s>= y then Return x else Return y . + +(** [no_nested_borrows::test3] *) +Definition test3_fwd : result unit := + x <- get_max_fwd (4 %u32) (3 %u32); + y <- get_max_fwd (10 %u32) (11 %u32); + z <- u32_add x y; if negb (z s= 15 %u32) then Fail_ else Return tt + . + +(** Unit test for [no_nested_borrows::test3] *) +Check (test3_fwd )%return. + +(** [no_nested_borrows::test_neg1] *) +Definition test_neg1_fwd : result unit := + y <- i32_neg (3 %i32); if negb (y s= (-3) %i32) then Fail_ else Return tt . + +(** Unit test for [no_nested_borrows::test_neg1] *) +Check (test_neg1_fwd )%return. + +(** [no_nested_borrows::refs_test1] *) +Definition refs_test1_fwd : result unit := + if negb (1 %i32 s= 1 %i32) then Fail_ else Return tt . + +(** Unit test for [no_nested_borrows::refs_test1] *) +Check (refs_test1_fwd )%return. + +(** [no_nested_borrows::refs_test2] *) +Definition refs_test2_fwd : result unit := + if negb (2 %i32 s= 2 %i32) + then Fail_ + else + if negb (0 %i32 s= 0 %i32) + then Fail_ + else + if negb (2 %i32 s= 2 %i32) + then Fail_ + else if negb (2 %i32 s= 2 %i32) then Fail_ else Return tt + . + +(** Unit test for [no_nested_borrows::refs_test2] *) +Check (refs_test2_fwd )%return. + +(** [no_nested_borrows::test_list1] *) +Definition test_list1_fwd : result unit := Return tt . + +(** Unit test for [no_nested_borrows::test_list1] *) +Check (test_list1_fwd )%return. + +(** [no_nested_borrows::test_box1] *) +Definition test_box1_fwd : result unit := + let b := 1 %i32 in + let x := b in if negb (x s= 1 %i32) then Fail_ else Return tt + . + +(** Unit test for [no_nested_borrows::test_box1] *) +Check (test_box1_fwd )%return. + +(** [no_nested_borrows::copy_int] *) +Definition copy_int_fwd (x : i32) : result i32 := Return x . + +(** [no_nested_borrows::test_unreachable] *) +Definition test_unreachable_fwd (b : bool) : result unit := + if b then Fail_ else Return tt . + +(** [no_nested_borrows::test_panic] *) +Definition test_panic_fwd (b : bool) : result unit := + if b then Fail_ else Return tt . + +(** [no_nested_borrows::test_copy_int] *) +Definition test_copy_int_fwd : result unit := + y <- copy_int_fwd (0 %i32); if negb (0 %i32 s= y) then Fail_ else Return tt . + +(** Unit test for [no_nested_borrows::test_copy_int] *) +Check (test_copy_int_fwd )%return. + +(** [no_nested_borrows::is_cons] *) +Definition is_cons_fwd (T : Type) (l : List_t T) : result bool := + match l with | ListCons t l0 => Return true | ListNil => Return false end . + +(** [no_nested_borrows::test_is_cons] *) +Definition test_is_cons_fwd : result unit := + let l := ListNil in + b <- is_cons_fwd i32 (ListCons (0 %i32) l); + if negb b then Fail_ else Return tt + . + +(** Unit test for [no_nested_borrows::test_is_cons] *) +Check (test_is_cons_fwd )%return. + +(** [no_nested_borrows::split_list] *) +Definition split_list_fwd + (T : Type) (l : List_t T) : result (T * (List_t T)) := + match l with | ListCons hd tl => Return (hd, tl) | ListNil => Fail_ end . + +(** [no_nested_borrows::test_split_list] *) +Definition test_split_list_fwd : result unit := + let l := ListNil in + p <- split_list_fwd i32 (ListCons (0 %i32) l); + let (hd, _) := p in if negb (hd s= 0 %i32) then Fail_ else Return tt + . + +(** Unit test for [no_nested_borrows::test_split_list] *) +Check (test_split_list_fwd )%return. + +(** [no_nested_borrows::choose] *) +Definition choose_fwd (T : Type) (b : bool) (x : T) (y : T) : result T := + if b then Return x else Return y . + +(** [no_nested_borrows::choose] *) +Definition choose_back + (T : Type) (b : bool) (x : T) (y : T) (ret : T) : result (T * T) := + if b then Return (ret, y) else Return (x, ret) . + +(** [no_nested_borrows::choose_test] *) +Definition choose_test_fwd : result unit := + z <- choose_fwd i32 true (0 %i32) (0 %i32); + z0 <- i32_add z 1 %i32; + if negb (z0 s= 1 %i32) + then Fail_ + else + ( + p <- choose_back i32 true (0 %i32) (0 %i32) z0; + let (x, y) := p in + if negb (x s= 1 %i32) + then Fail_ + else if negb (y s= 0 %i32) then Fail_ else Return tt ) + . + +(** Unit test for [no_nested_borrows::choose_test] *) +Check (choose_test_fwd )%return. + +(** [no_nested_borrows::test_char] *) +Definition test_char_fwd : result char := + Return (char_of_byte Coq.Init.Byte.x61) . + +(** [no_nested_borrows::NodeElem] *) +Inductive Node_elem_t (T : Type) := +| NodeElemCons : Tree_t T -> Node_elem_t T -> Node_elem_t T +| NodeElemNil : Node_elem_t T + +(** [no_nested_borrows::Tree] *) +with Tree_t (T : Type) := +| TreeLeaf : T -> Tree_t T +| TreeNode : T -> Node_elem_t T -> Tree_t T -> Tree_t T +. + +Arguments NodeElemCons {T} _ _ . +Arguments NodeElemNil {T} . + +Arguments TreeLeaf {T} _ . +Arguments TreeNode {T} _ _ _ . + +(** [no_nested_borrows::list_length] *) +Fixpoint list_length_fwd (T : Type) (l : List_t T) : result u32 := + match l with + | ListCons t l1 => + i <- list_length_fwd T l1; i0 <- u32_add 1 %u32 i; Return i0 + | ListNil => Return (0 %u32) + end + . + +(** [no_nested_borrows::list_nth_shared] *) +Fixpoint list_nth_shared_fwd (T : Type) (l : List_t T) (i : u32) : result T := + match l with + | ListCons x tl => + if i s= 0 %u32 + then Return x + else ( i0 <- u32_sub i 1 %u32; t <- list_nth_shared_fwd T tl i0; Return t ) + | ListNil => Fail_ + end + . + +(** [no_nested_borrows::list_nth_mut] *) +Fixpoint list_nth_mut_fwd (T : Type) (l : List_t T) (i : u32) : result T := + match l with + | ListCons x tl => + if i s= 0 %u32 + then Return x + else ( i0 <- u32_sub i 1 %u32; t <- list_nth_mut_fwd T tl i0; Return t ) + | ListNil => Fail_ + end + . + +(** [no_nested_borrows::list_nth_mut] *) +Fixpoint list_nth_mut_back + (T : Type) (l : List_t T) (i : u32) (ret : T) : result (List_t T) := + match l with + | ListCons x tl => + if i s= 0 %u32 + then Return (ListCons ret tl) + else + ( + i0 <- u32_sub i 1 %u32; + tl0 <- list_nth_mut_back T tl i0 ret; Return (ListCons x tl0) ) + | ListNil => Fail_ + end + . + +(** [no_nested_borrows::list_rev_aux] *) +Fixpoint list_rev_aux_fwd + (T : Type) (li : List_t T) (lo : List_t T) : result (List_t T) := + match li with + | ListCons hd tl => l <- list_rev_aux_fwd T tl (ListCons hd lo); Return l + | ListNil => Return lo + end + . + +(** [no_nested_borrows::list_rev] *) +Definition list_rev_fwd_back (T : Type) (l : List_t T) : result (List_t T) := + let li := mem_replace_fwd (List_t T) l ListNil in + l0 <- list_rev_aux_fwd T li ListNil; Return l0 + . + +(** [no_nested_borrows::test_list_functions] *) +Definition test_list_functions_fwd : result unit := + let l := ListNil in + let l0 := ListCons (2 %i32) l in + let l1 := ListCons (1 %i32) l0 in + i <- list_length_fwd i32 (ListCons (0 %i32) l1); + if negb (i s= 3 %u32) + then Fail_ + else + ( + i0 <- list_nth_shared_fwd i32 (ListCons (0 %i32) l1) (0 %u32); + if negb (i0 s= 0 %i32) + then Fail_ + else + ( + i1 <- list_nth_shared_fwd i32 (ListCons (0 %i32) l1) (1 %u32); + if negb (i1 s= 1 %i32) + then Fail_ + else + ( + i2 <- list_nth_shared_fwd i32 (ListCons (0 %i32) l1) (2 %u32); + if negb (i2 s= 2 %i32) + then Fail_ + else + ( + ls <- + list_nth_mut_back i32 (ListCons (0 %i32) l1) (1 %u32) (3 + %i32); + i3 <- list_nth_shared_fwd i32 ls (0 %u32); + if negb (i3 s= 0 %i32) + then Fail_ + else + ( + i4 <- list_nth_shared_fwd i32 ls (1 %u32); + if negb (i4 s= 3 %i32) + then Fail_ + else + ( + i5 <- list_nth_shared_fwd i32 ls (2 %u32); + if negb (i5 s= 2 %i32) then Fail_ else Return tt ) ) + ) ) ) ) + . + +(** Unit test for [no_nested_borrows::test_list_functions] *) +Check (test_list_functions_fwd )%return. + +(** [no_nested_borrows::id_mut_pair1] *) +Definition id_mut_pair1_fwd + (T1 T2 : Type) (x : T1) (y : T2) : result (T1 * T2) := + Return (x, y) . + +(** [no_nested_borrows::id_mut_pair1] *) +Definition id_mut_pair1_back + (T1 T2 : Type) (x : T1) (y : T2) (ret : (T1 * T2)) : result (T1 * T2) := + let (t, t0) := ret in Return (t, t0) . + +(** [no_nested_borrows::id_mut_pair2] *) +Definition id_mut_pair2_fwd + (T1 T2 : Type) (p : (T1 * T2)) : result (T1 * T2) := + let (t, t0) := p in Return (t, t0) . + +(** [no_nested_borrows::id_mut_pair2] *) +Definition id_mut_pair2_back + (T1 T2 : Type) (p : (T1 * T2)) (ret : (T1 * T2)) : result (T1 * T2) := + let (t, t0) := ret in Return (t, t0) . + +(** [no_nested_borrows::id_mut_pair3] *) +Definition id_mut_pair3_fwd + (T1 T2 : Type) (x : T1) (y : T2) : result (T1 * T2) := + Return (x, y) . + +(** [no_nested_borrows::id_mut_pair3] *) +Definition id_mut_pair3_back'a + (T1 T2 : Type) (x : T1) (y : T2) (ret : T1) : result T1 := + Return ret . + +(** [no_nested_borrows::id_mut_pair3] *) +Definition id_mut_pair3_back'b + (T1 T2 : Type) (x : T1) (y : T2) (ret : T2) : result T2 := + Return ret . + +(** [no_nested_borrows::id_mut_pair4] *) +Definition id_mut_pair4_fwd + (T1 T2 : Type) (p : (T1 * T2)) : result (T1 * T2) := + let (t, t0) := p in Return (t, t0) . + +(** [no_nested_borrows::id_mut_pair4] *) +Definition id_mut_pair4_back'a + (T1 T2 : Type) (p : (T1 * T2)) (ret : T1) : result T1 := + Return ret . + +(** [no_nested_borrows::id_mut_pair4] *) +Definition id_mut_pair4_back'b + (T1 T2 : Type) (p : (T1 * T2)) (ret : T2) : result T2 := + Return ret . + +(** [no_nested_borrows::StructWithTuple] *) +Record Struct_with_tuple_t (T1 T2 : Type) := +mkStruct_with_tuple_t +{ + Struct_with_tuple_p : (T1 * T2); +} +. + +Arguments mkStruct_with_tuple_t {T1} {T2} _ . +Arguments Struct_with_tuple_p {T1} {T2} . + +(** [no_nested_borrows::new_tuple1] *) +Definition new_tuple1_fwd : result (Struct_with_tuple_t u32 u32) := + Return (mkStruct_with_tuple_t (1 %u32, 2 %u32)) . + +(** [no_nested_borrows::new_tuple2] *) +Definition new_tuple2_fwd : result (Struct_with_tuple_t i16 i16) := + Return (mkStruct_with_tuple_t (1 %i16, 2 %i16)) . + +(** [no_nested_borrows::new_tuple3] *) +Definition new_tuple3_fwd : result (Struct_with_tuple_t u64 i64) := + Return (mkStruct_with_tuple_t (1 %u64, 2 %i64)) . + +(** [no_nested_borrows::StructWithPair] *) +Record Struct_with_pair_t (T1 T2 : Type) := +mkStruct_with_pair_t +{ + Struct_with_pair_p : Pair_t T1 T2; +} +. + +Arguments mkStruct_with_pair_t {T1} {T2} _ . +Arguments Struct_with_pair_p {T1} {T2} . + +(** [no_nested_borrows::new_pair1] *) +Definition new_pair1_fwd : result (Struct_with_pair_t u32 u32) := + Return (mkStruct_with_pair_t (mkPair_t (1 %u32) (2 %u32))) . + +(** [no_nested_borrows::test_constants] *) +Definition test_constants_fwd : result unit := + swt <- new_tuple1_fwd; + match swt with + | mkStruct_with_tuple_t p => + let (i, _) := p in + if negb (i s= 1 %u32) + then Fail_ + else + ( + swt0 <- new_tuple2_fwd; + match swt0 with + | mkStruct_with_tuple_t p0 => + let (i0, _) := p0 in + if negb (i0 s= 1 %i16) + then Fail_ + else + ( + swt1 <- new_tuple3_fwd; + match swt1 with + | mkStruct_with_tuple_t p1 => + let (i1, _) := p1 in + if negb (i1 s= 1 %u64) + then Fail_ + else + ( + swp <- new_pair1_fwd; + match swp with + | mkStruct_with_pair_t p2 => + match p2 with + | mkPair_t i2 i3 => + if negb (i2 s= 1 %u32) then Fail_ else Return tt + end + end ) + end ) + end ) + end + . + +(** Unit test for [no_nested_borrows::test_constants] *) +Check (test_constants_fwd )%return. + +(** [no_nested_borrows::test_weird_borrows1] *) +Definition test_weird_borrows1_fwd : result unit := Return tt . + +(** Unit test for [no_nested_borrows::test_weird_borrows1] *) +Check (test_weird_borrows1_fwd )%return. + +(** [no_nested_borrows::test_mem_replace] *) +Definition test_mem_replace_fwd_back (px : u32) : result u32 := + let y := mem_replace_fwd u32 px (1 %u32) in + if negb (y s= 0 %u32) then Fail_ else Return (2 %u32) + . + +(** [no_nested_borrows::test_shared_borrow_bool1] *) +Definition test_shared_borrow_bool1_fwd (b : bool) : result u32 := + if b then Return (0 %u32) else Return (1 %u32) . + +(** [no_nested_borrows::test_shared_borrow_bool2] *) +Definition test_shared_borrow_bool2_fwd : result u32 := Return (0 %u32) . + +(** [no_nested_borrows::test_shared_borrow_enum1] *) +Definition test_shared_borrow_enum1_fwd (l : List_t u32) : result u32 := + match l with + | ListCons i l0 => Return (1 %u32) + | ListNil => Return (0 %u32) + end + . + +(** [no_nested_borrows::test_shared_borrow_enum2] *) +Definition test_shared_borrow_enum2_fwd : result u32 := Return (0 %u32) . + +End NoNestedBorrows . diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v new file mode 100644 index 00000000..5d9598eb --- /dev/null +++ b/tests/coq/misc/Paper.v @@ -0,0 +1,114 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [paper] *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Local Open Scope Primitives_scope. +Module Paper . + +(** [paper::ref_incr] *) +Definition ref_incr_fwd_back (x : i32) : result i32 := + x0 <- i32_add x 1 %i32; Return x0 . + +(** [paper::test_incr] *) +Definition test_incr_fwd : result unit := + x <- ref_incr_fwd_back (0 %i32); + if negb (x s= 1 %i32) then Fail_ else Return tt + . + +(** Unit test for [paper::test_incr] *) +Check (test_incr_fwd )%return. + +(** [paper::choose] *) +Definition choose_fwd (T : Type) (b : bool) (x : T) (y : T) : result T := + if b then Return x else Return y . + +(** [paper::choose] *) +Definition choose_back + (T : Type) (b : bool) (x : T) (y : T) (ret : T) : result (T * T) := + if b then Return (ret, y) else Return (x, ret) . + +(** [paper::test_choose] *) +Definition test_choose_fwd : result unit := + z <- choose_fwd i32 true (0 %i32) (0 %i32); + z0 <- i32_add z 1 %i32; + if negb (z0 s= 1 %i32) + then Fail_ + else + ( + p <- choose_back i32 true (0 %i32) (0 %i32) z0; + let (x, y) := p in + if negb (x s= 1 %i32) + then Fail_ + else if negb (y s= 0 %i32) then Fail_ else Return tt ) + . + +(** Unit test for [paper::test_choose] *) +Check (test_choose_fwd )%return. + +(** [paper::List] *) +Inductive List_t (T : Type) := +| ListCons : T -> List_t T -> List_t T +| ListNil : List_t T +. + +Arguments ListCons {T} _ _ . +Arguments ListNil {T} . + +(** [paper::list_nth_mut] *) +Fixpoint list_nth_mut_fwd (T : Type) (l : List_t T) (i : u32) : result T := + match l with + | ListCons x tl => + if i s= 0 %u32 + then Return x + else ( i0 <- u32_sub i 1 %u32; t <- list_nth_mut_fwd T tl i0; Return t ) + | ListNil => Fail_ + end + . + +(** [paper::list_nth_mut] *) +Fixpoint list_nth_mut_back + (T : Type) (l : List_t T) (i : u32) (ret : T) : result (List_t T) := + match l with + | ListCons x tl => + if i s= 0 %u32 + then Return (ListCons ret tl) + else + ( + i0 <- u32_sub i 1 %u32; + tl0 <- list_nth_mut_back T tl i0 ret; Return (ListCons x tl0) ) + | ListNil => Fail_ + end + . + +(** [paper::sum] *) +Fixpoint sum_fwd (l : List_t i32) : result i32 := + match l with + | ListCons x tl => i <- sum_fwd tl; i0 <- i32_add x i; Return i0 + | ListNil => Return (0 %i32) + end + . + +(** [paper::test_nth] *) +Definition test_nth_fwd : result unit := + let l := ListNil in + let l0 := ListCons (3 %i32) l in + let l1 := ListCons (2 %i32) l0 in + x <- list_nth_mut_fwd i32 (ListCons (1 %i32) l1) (2 %u32); + x0 <- i32_add x 1 %i32; + l2 <- list_nth_mut_back i32 (ListCons (1 %i32) l1) (2 %u32) x0; + i <- sum_fwd l2; if negb (i s= 7 %i32) then Fail_ else Return tt + . + +(** Unit test for [paper::test_nth] *) +Check (test_nth_fwd )%return. + +(** [paper::call_choose] *) +Definition call_choose_fwd (p : (u32 * u32)) : result u32 := + let (px, py) := p in + pz <- choose_fwd u32 true px py; + pz0 <- u32_add pz 1 %u32; + p0 <- choose_back u32 true px py pz0; let (px0, _) := p0 in Return px0 + . + +End Paper . diff --git a/tests/coq/misc/Primitives.v b/tests/coq/misc/Primitives.v new file mode 100644 index 00000000..c27b8aed --- /dev/null +++ b/tests/coq/misc/Primitives.v @@ -0,0 +1,478 @@ +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 result A := + | Return : A -> result A + | Fail_ : result A. + +Arguments Return {_} a. +Arguments Fail_ {_}. + +Definition bind {A B} (m: result A) (f: A -> result B) : result B := + match m with + | Fail_ => Fail_ + | Return x => f x + end. + +Definition return_ {A: Type} (x: A) : result A := Return x . +Definition fail_ {A: Type} : result A := Fail_ . + +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_. + +(** 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_ => fun p' => + False_rect _ (eq_ind Fail_ + (fun e : result A => + match e with + | Return _ => False + | Fail_ => 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_)%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 . + +(*** 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_ + 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_ 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)). + +(** 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). + +(** Comparisons *) +Print Z.leb . + +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. + +(** 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. + +(*** 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)). + +Lemma le_0_usize_max : 0 <= usize_max. +Proof. + pose (H := usize_max_bound). + unfold u32_max in H. + lia. +Qed. + +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. +Proof. + unfold 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). + +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 vec_bind {A B} (v: vec A) (f: list A -> result (list B)) : result (vec B) := + l <- f (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_ + end. + +(* The **forward** function shouldn't be used *) +Definition vec_push_fwd (T: Type) (v: 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])). + +(* 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_. + +Definition vec_insert_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_). + +(* 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_ + 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_. + +(* 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_ + 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_). + +End Primitives. diff --git a/tests/coq/misc/_CoqProject b/tests/coq/misc/_CoqProject new file mode 100644 index 00000000..7f4981fa --- /dev/null +++ b/tests/coq/misc/_CoqProject @@ -0,0 +1,12 @@ +-R . Lib +-arg -w +-arg all + +Primitives.v + +Constants.v +External__Funs.v +External__Opaque.v +External__Types.v +NoNestedBorrows.v +Paper.v
\ No newline at end of file |