Regenerate the files and fix the proofs

4 files changed, 71 insertions, 59 deletions

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 <? vec_length v then Return tt else Fail_.
+  if to_Z i <? vec_length v then Return tt else Fail_ Failure.
 
 Definition vec_insert_back (T: Type) (v: vec T) (i: usize) (x: T) : result (vec T) :=
   vec_bind v (fun l =>
     if to_Z i <? Z.of_nat (length l)
     then Return (list_update l (usize_to_nat i) x)
-    else Fail_).
+    else Fail_ Failure).
 
 (* The **backward** function shouldn't be used *)
 Definition vec_index_fwd (T: Type) (v: vec T) (i: usize) : result T :=
   match nth_error (vec_to_list v) (usize_to_nat i) with
   | Some n => Return n
-  | None   => Fail_
+  | None   => Fail_ Failure
   end.
 
 Definition vec_index_back (T: Type) (v: vec T) (i: usize) (x: T) : result unit :=
-  if to_Z i <? vec_length v then Return tt else Fail_.
+  if to_Z i <? vec_length v then Return tt else Fail_ Failure.
 
 (* The **backward** function shouldn't be used *)
 Definition vec_index_mut_fwd (T: Type) (v: vec T) (i: usize) : result T :=
   match nth_error (vec_to_list v) (usize_to_nat i) with
   | Some n => Return n
-  | None   => Fail_
+  | 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 <? Z.of_nat (length l)
     then Return (list_update l (usize_to_nat i) x)
-    else Fail_).
+    else Fail_ Failure).
 
 End Primitives.