From 5a96e28b8706ed945ccbb569881ca1888cd73ace Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 14 Nov 2022 11:58:31 +0100 Subject: Regenerate the files and fix the proofs --- tests/coq/misc/External__Funs.v | 2 +- tests/coq/misc/NoNestedBorrows.v | 72 ++++++++++++++++++++++------------------ tests/coq/misc/Paper.v | 14 ++++---- tests/coq/misc/Primitives.v | 42 ++++++++++++----------- 4 files changed, 71 insertions(+), 59 deletions(-) (limited to 'tests/coq') diff --git a/tests/coq/misc/External__Funs.v b/tests/coq/misc/External__Funs.v index cd03ae3d..cc9e9461 100644 --- a/tests/coq/misc/External__Funs.v +++ b/tests/coq/misc/External__Funs.v @@ -107,7 +107,7 @@ Definition test_swap_non_zero_fwd p0 <- swap_back u32 x (0 %u32) st st0; let (st1, p1) := p0 in let (x0, _) := p1 in - if x0 s= 0 %u32 then Fail_ else Return (st1, x0) + if x0 s= 0 %u32 then Fail_ Failure else Return (st1, x0) . End External__Funs . diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v index 774b8a1e..6d7f7987 100644 --- a/tests/coq/misc/NoNestedBorrows.v +++ b/tests/coq/misc/NoNestedBorrows.v @@ -95,7 +95,7 @@ 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 + if negb (z s= 15 %u32) then Fail_ Failure else Return tt . (** Unit test for [no_nested_borrows::test3] *) @@ -103,14 +103,16 @@ 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 . + y <- i32_neg (3 %i32); + if negb (y s= (-3) %i32) then Fail_ Failure 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 . + if negb (1 %i32 s= 1 %i32) then Fail_ Failure else Return tt . (** Unit test for [no_nested_borrows::refs_test1] *) Check (refs_test1_fwd )%return. @@ -118,14 +120,14 @@ 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_ + then Fail_ Failure else if negb (0 %i32 s= 0 %i32) - then Fail_ + then Fail_ Failure else if negb (2 %i32 s= 2 %i32) - then Fail_ - else if negb (2 %i32 s= 2 %i32) then Fail_ else Return tt + then Fail_ Failure + else if negb (2 %i32 s= 2 %i32) then Fail_ Failure else Return tt . (** Unit test for [no_nested_borrows::refs_test2] *) @@ -141,7 +143,7 @@ Check (test_list1_fwd )%return. 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 + if negb (x s= 1 %i32) then Fail_ Failure else Return tt . (** Unit test for [no_nested_borrows::test_box1] *) @@ -152,15 +154,17 @@ 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 . + if b then Fail_ Failure else Return tt . (** [no_nested_borrows::test_panic] *) Definition test_panic_fwd (b : bool) : result unit := - if b then Fail_ else Return tt . + if b then Fail_ Failure 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 . + y <- copy_int_fwd (0 %i32); + if negb (0 %i32 s= y) then Fail_ Failure else Return tt + . (** Unit test for [no_nested_borrows::test_copy_int] *) Check (test_copy_int_fwd )%return. @@ -173,7 +177,7 @@ Definition is_cons_fwd (T : Type) (l : List_t T) : result bool := 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 + if negb b then Fail_ Failure else Return tt . (** Unit test for [no_nested_borrows::test_is_cons] *) @@ -182,14 +186,18 @@ 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 . + match l with + | ListCons hd tl => Return (hd, tl) + | ListNil => Fail_ Failure + 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 + if negb (hd s= 0 %i32) then Fail_ Failure else Return tt . (** Unit test for [no_nested_borrows::test_split_list] *) @@ -209,13 +217,13 @@ 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_ + then Fail_ Failure 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) + then Fail_ Failure + else if negb (y s= 0 %i32) then Fail_ Failure else Return tt) . (** Unit test for [no_nested_borrows::choose_test] *) @@ -258,7 +266,7 @@ Fixpoint list_nth_shared_fwd (T : Type) (l : List_t T) (i : u32) : result T := 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_ + | ListNil => Fail_ Failure end . @@ -269,7 +277,7 @@ Fixpoint list_nth_mut_fwd (T : Type) (l : List_t T) (i : u32) : result T := 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_ + | ListNil => Fail_ Failure end . @@ -284,7 +292,7 @@ Fixpoint list_nth_mut_back i0 <- u32_sub i 1 %u32; tl0 <- list_nth_mut_back T tl i0 ret; Return (ListCons x tl0)) - | ListNil => Fail_ + | ListNil => Fail_ Failure end . @@ -311,31 +319,31 @@ Definition test_list_functions_fwd : result unit := let l1 := ListCons (1 %i32) l0 in i <- list_length_fwd i32 (ListCons (0 %i32) l1); if negb (i s= 3 %u32) - then Fail_ + then Fail_ Failure else ( i0 <- list_nth_shared_fwd i32 (ListCons (0 %i32) l1) (0 %u32); if negb (i0 s= 0 %i32) - then Fail_ + then Fail_ Failure else ( i1 <- list_nth_shared_fwd i32 (ListCons (0 %i32) l1) (1 %u32); if negb (i1 s= 1 %i32) - then Fail_ + then Fail_ Failure else ( i2 <- list_nth_shared_fwd i32 (ListCons (0 %i32) l1) (2 %u32); if negb (i2 s= 2 %i32) - then Fail_ + then Fail_ Failure 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_ + then Fail_ Failure else ( i4 <- list_nth_shared_fwd i32 ls (1 %u32); if negb (i4 s= 3 %i32) - then Fail_ + then Fail_ Failure else ( i5 <- list_nth_shared_fwd i32 ls (2 %u32); - if negb (i5 s= 2 %i32) then Fail_ else Return tt)))))) + if negb (i5 s= 2 %i32) then Fail_ Failure else Return tt)))))) . (** Unit test for [no_nested_borrows::test_list_functions] *) @@ -436,28 +444,28 @@ Definition test_constants_fwd : result unit := | mkStruct_with_tuple_t p => let (i, _) := p in if negb (i s= 1 %u32) - then Fail_ + then Fail_ Failure 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_ + then Fail_ Failure 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_ + then Fail_ Failure 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 + if negb (i2 s= 1 %u32) then Fail_ Failure else Return tt end end) end) @@ -477,7 +485,7 @@ 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) + if negb (y s= 0 %u32) then Fail_ Failure else Return (2 %u32) . (** [no_nested_borrows::test_shared_borrow_bool1] *) diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v index 25c01d7b..d0c99883 100644 --- a/tests/coq/misc/Paper.v +++ b/tests/coq/misc/Paper.v @@ -13,7 +13,7 @@ Definition ref_incr_fwd_back (x : i32) : result i32 := (** [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 + if negb (x s= 1 %i32) then Fail_ Failure else Return tt . (** Unit test for [paper::test_incr] *) @@ -33,13 +33,13 @@ 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_ + then Fail_ Failure 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) + then Fail_ Failure + else if negb (y s= 0 %i32) then Fail_ Failure else Return tt) . (** Unit test for [paper::test_choose] *) @@ -61,7 +61,7 @@ Fixpoint list_nth_mut_fwd (T : Type) (l : List_t T) (i : u32) : result T := 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_ + | ListNil => Fail_ Failure end . @@ -76,7 +76,7 @@ Fixpoint list_nth_mut_back i0 <- u32_sub i 1 %u32; tl0 <- list_nth_mut_back T tl i0 ret; Return (ListCons x tl0)) - | ListNil => Fail_ + | ListNil => Fail_ Failure end . @@ -97,7 +97,7 @@ Definition test_nth_fwd : result unit := 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 + if negb (i s= 7 %i32) then Fail_ Failure else Return tt . (** Unit test for [paper::test_nth] *) diff --git a/tests/coq/misc/Primitives.v b/tests/coq/misc/Primitives.v index c27b8aed..9a97d6c7 100644 --- a/tests/coq/misc/Primitives.v +++ b/tests/coq/misc/Primitives.v @@ -13,40 +13,44 @@ Module Primitives. Declare Scope Primitives_scope. (*** Result *) - + +Inductive error := + | Failure + | OutOfFuel. + Inductive result A := | Return : A -> result A - | Fail_ : 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_ => Fail_ + | Fail_ e => Fail_ e | Return x => f x end. -Definition return_ {A: Type} (x: A) : result A := Return x . -Definition fail_ {A: Type} : result A := Fail_ . +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_. + 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_ => fun p' => - False_rect _ (eq_ind Fail_ + | Fail_ e => fun p' => + False_rect _ (eq_ind (Fail_ e) (fun e : result A => match e with | Return _ => False - | Fail_ => True + | Fail_ e => True end) I (Return x) p') end p. @@ -55,7 +59,7 @@ 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. +Check (if true then Return (1 + 2) else Fail_ Failure)%global = 3. (*** Misc *) @@ -232,7 +236,7 @@ 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_ + | right _ => Fail_ Failure end. Definition scalar_add {ty} (x y: scalar ty) : result (scalar ty) := mk_scalar ty (to_Z x + to_Z y). @@ -242,7 +246,7 @@ Definition scalar_sub {ty} (x y: scalar ty) : result (scalar ty) := mk_scalar ty 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 + 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)). @@ -433,7 +437,7 @@ Definition vec_bind {A B} (v: vec A) (f: list A -> result (list B)) : result (ve 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_ + | right _ => Fail_ Failure end. (* The **forward** function shouldn't be used *) @@ -444,35 +448,35 @@ Definition vec_push_back (T: Type) (v: vec T) (x: T) : result (vec T) := (* 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 if to_Z i Return n - | None => Fail_ + | None => Fail_ Failure end. Definition vec_index_back (T: Type) (v: vec T) (i: usize) (x: T) : result unit := - if to_Z i Return n - | None => Fail_ + | None => Fail_ Failure 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