Make [Result::Failure] type an [Error] parameter

3 files changed, 88 insertions, 33 deletions

diff --git a/backends/coq/Primitives.v b/backends/coq/Primitives.v
index c27b8aed..9a97d6c7 100644
--- a/backends/coq/Primitives.v
+++ b/backends/coq/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.
diff --git a/backends/fstar/Makefile b/backends/fstar/Makefile
new file mode 100644
index 00000000..a16b0edb
--- /dev/null
+++ b/backends/fstar/Makefile
@@ -0,0 +1,47 @@
+INCLUDE_DIRS = .
+
+FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS))
+
+FSTAR_HINTS ?= --use_hints --use_hint_hashes --record_hints
+
+FSTAR_OPTIONS = $(FSTAR_HINTS) \
+  --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
+  --warn_error '+241@247+285-274' \
+
+FSTAR_NO_FLAGS = fstar.exe --already_cached 'Prims FStar LowStar Steel' --odir obj --cache_dir obj
+
+FSTAR = $(FSTAR_NO_FLAGS) $(FSTAR_OPTIONS)
+
+# The F* roots are used to compute the dependency graph, and generate the .depend file
+FSTAR_ROOTS ?= $(wildcard *.fst *.fsti)
+
+# Build all the files
+all: $(addprefix obj/,$(addsuffix .checked,$(FSTAR_ROOTS)))
+
+# This is the right way to ensure the .depend file always gets re-built.
+ifeq (,$(filter %-in,$(MAKECMDGOALS)))
+ifndef NODEPEND
+ifndef MAKE_RESTARTS
+.depend: .FORCE
+	$(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) > $@
+
+.PHONY: .FORCE
+.FORCE:
+endif
+endif
+
+include .depend
+endif
+
+# For the interactive mode
+%.fst-in %.fsti-in:
+	@echo $(FSTAR_OPTIONS)
+
+# Generete the .checked files in batch mode
+%.checked:
+	$(FSTAR) $(FSTAR_OPTIONS) $< && \
+	touch -c $@
+
+.PHONY: clean
+clean:
+	rm -f obj/*
diff --git a/backends/fstar/Primitives.fst b/backends/fstar/Primitives.fst
index 96138e46..82622656 100644
--- a/backends/fstar/Primitives.fst
+++ b/backends/fstar/Primitives.fst
@@ -18,9 +18,13 @@ let rec list_update #a ls i x =
 #pop-options
 
 (*** Result *)
+type error : Type0 =
+| Failure
+| OutOfFuel
+
 type result (a : Type0) : Type0 =
 | Return : v:a -> result a
-| Fail : result a
+| Fail : e:error -> result a
 
 // Monadic bind and return.
 // Re-definining those allows us to customize the result of the monadic notations
@@ -29,10 +33,10 @@ let return (#a : Type0) (x:a) : result a = Return x
 let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b =
     match m with
     | Return x -> f x
-    | Fail -> Fail
+    | Fail e -> Fail e
 
 // Monadic assert(...)
-let massert (b:bool) : result unit = if b then Return () else Fail
+let massert (b:bool) : result unit = if b then Return () else Fail Failure
 
 // Normalize and unwrap a successful result (used for globals).
 let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x
@@ -119,12 +123,12 @@ let scalar_max (ty : scalar_ty) : int =
 type scalar (ty : scalar_ty) : eqtype = x:int{scalar_min ty <= x && x <= scalar_max ty}
 
 let mk_scalar (ty : scalar_ty) (x : int) : result (scalar ty) =
-  if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail
+  if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail Failure
 
 let scalar_neg (#ty : scalar_ty) (x : scalar ty) : result (scalar ty) = mk_scalar ty (-x)
 
 let scalar_div (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
-  if y <> 0 then mk_scalar ty (x / y) else Fail
+  if y <> 0 then mk_scalar ty (x / y) else Fail Failure
 
 /// The remainder operation
 let int_rem (x : int) (y : int{y <> 0}) : int =
@@ -137,7 +141,7 @@ let _ = assert_norm(int_rem 1 (-2) = 1)
 let _ = assert_norm(int_rem (-1) (-2) = -1)
 
 let scalar_rem (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
-  if y <> 0 then mk_scalar ty (int_rem x y) else Fail
+  if y <> 0 then mk_scalar ty (int_rem x y) else Fail Failure
 
 let scalar_add (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
   mk_scalar ty (x + y)
@@ -258,7 +262,7 @@ let vec_push_back (a  : Type0) (v : vec a) (x : a) :
   (requires True)
   (ensures (fun res ->
     match res with
-    | Fail -> True
+    | Fail e -> e == Failure
     | Return v' -> length v' = length v + 1)) =
   if length v < usize_max then begin
     (**) assert_norm(length [x] == 1);
@@ -266,22 +270,22 @@ let vec_push_back (a  : Type0) (v : vec a) (x : a) :
     (**) assert(length (append v [x]) = length v + 1);
     Return (append v [x])
     end
-  else Fail
+  else Fail Failure
 
 // The **forward** function shouldn't be used
 let vec_insert_fwd (a : Type0) (v : vec a) (i : usize) (x : a) : result unit =
-  if i < length v then Return () else Fail
+  if i < length v then Return () else Fail Failure
 let vec_insert_back (a : Type0) (v : vec a) (i : usize) (x : a) : result (vec a) =
-  if i < length v then Return (list_update v i x) else Fail
+  if i < length v then Return (list_update v i x) else Fail Failure
 
 // The **backward** function shouldn't be used
 let vec_index_fwd (a : Type0) (v : vec a) (i : usize) : result a =
-  if i < length v then Return (index v i) else Fail
+  if i < length v then Return (index v i) else Fail Failure
 let vec_index_back (a : Type0) (v : vec a) (i : usize) (x : a) : result unit =
-  if i < length v then Return () else Fail
+  if i < length v then Return () else Fail Failure
 
 let vec_index_mut_fwd (a : Type0) (v : vec a) (i : usize) : result a =
-  if i < length v then Return (index v i) else Fail
+  if i < length v then Return (index v i) else Fail Failure
 let vec_index_mut_back (a : Type0) (v : vec a) (i : usize) (nx : a) : result (vec a) =
-  if i < length v then Return (list_update v i nx) else Fail
+  if i < length v then Return (list_update v i nx) else Fail Failure