Merge pull request #444 from hacspec/monomorphize-assoc-type-universe…

…-index

fix(proof-libs/fstar): make `t_Index.Output` universe zero

proof-libs/fstar-secret-integers/core/Alloc.Slice.fst

@@ -2,4 +2,4 @@ module Alloc.Slice
 open Rust_primitives.Arrays
 open Alloc.Vec
 
-let impl__to_vec (s: t_Slice 'a): t_Vec 'a Alloc.Alloc.t_Global = s
+let impl__to_vec #a (s: t_Slice a): t_Vec a Alloc.Alloc.t_Global = s

proof-libs/fstar-secret-integers/core/Alloc.Vec.fst

@@ -13,19 +13,19 @@ let impl__with_capacity (_capacity: usize) = impl__new
 // TODO: missing precondition For now, `impl_1__push` has a wrong
 // semantics: pushing on a "full" vector does nothing. It should panic
 // instead.
-let impl_1__push
-  (v: t_Vec 't ())// Removed: {Seq.length v + 1 <= max_usize})
-  (x: 't)
-   : t_Vec 't () = 
+let impl_1__push #t
+  (v: t_Vec t ())// Removed: {Seq.length v + 1 <= max_usize})
+  (x: t)
+   : t_Vec t () = 
      if Seq.length v <= max_usize then v else
      FStar.Seq.append v (FStar.Seq.create 1 x)
 
-let impl_1__len (v: t_Vec 't ()) =
+let impl_1__len #t (v: t_Vec t ()) =
   let n = Seq.length v in
   assert (n <= maxint usize_inttype);
   mk_int #usize_inttype (Seq.length v)
 
-let from_elem (item: 'a) (len: usize) = Seq.create (v len) item
+let from_elem #a (item: a) (len: usize) = Seq.create (v len) item
 
 open Rust_primitives.Hax
 open Core.Ops.Index

proof-libs/fstar-secret-integers/core/Core.Array.fst

@@ -3,8 +3,8 @@ open Rust_primitives
 
 type t_TryFromSliceError = | TryFromSliceError
 
-let impl_23__map n (arr: t_Array 'a n) (f: 'a -> 'b): t_Array 'b n 
+let impl_23__map #a #b n (arr: t_Array a n) (f: a -> b): t_Array b n 
   = map_array arr f
 
-let impl_23__as_slice len (arr: t_Array 'a len): t_Slice 'a = arr
+let impl_23__as_slice #a len (arr: t_Array a len): t_Slice a = arr
 

proof-libs/fstar-secret-integers/core/Core.Ops.Index.fst

@@ -1,7 +1,7 @@
 module Core.Ops.Index
 
 class t_Index (t_Self:Type0) (t_Idx:Type0) = {
-  f_Output: Type;
+  f_Output: Type0;
   in_range: t_Self -> t_Idx -> Type0;
   f_index: s:t_Self -> i:t_Idx{in_range s i} -> f_Output;
 }

proof-libs/fstar-secret-integers/core/Core.Option.fst

@@ -2,12 +2,12 @@ module Core.Option
 
 type t_Option t = | Option_Some of t | Option_None
 
-let impl__and_then (self: t_Option 'self) (f: 'self -> t_Option 't): t_Option 't = 
+let impl__and_then #t #t_Self (self: t_Option t_Self) (f: t_Self -> t_Option t): t_Option t = 
   match self with
   | Option_Some x -> f x
   | Option_None -> Option_None
 
 let impl__unwrap #t (x: t_Option t {Option_Some? x}): t = Option_Some?._0 x
 
-let impl__is_some (self: t_Option 'self): bool =  Option_Some? self
+let impl__is_some #t_Self (self: t_Option t_Self): bool =  Option_Some? self
 

proof-libs/fstar-secret-integers/core/Core.Slice.fsti

@@ -8,12 +8,12 @@ let impl__len (#t: Type) (s: t_Slice t)
 
 open Core.Slice.Iter
 
-val impl__chunks (x: t_Slice 'a) (cs: usize): t_Chunks 'a
+val impl__chunks #a (x: t_Slice a) (cs: usize): t_Chunks a
 
-let impl__iter (s: t_Slice 't): t_Slice 't = s
+let impl__iter #t (s: t_Slice t): t_Slice t = s
 
-val impl__chunks_exact (x: t_Slice 'a) (cs: usize):
-    Pure (t_Slice (t_Slice 'a))
+val impl__chunks_exact #a (x: t_Slice a) (cs: usize):
+    Pure (t_Slice (t_Slice a))
     (requires True)
     (ensures (fun r -> forall i. i < v (length x) ==> length x ==  cs))
 

proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Arrays.fst

@@ -8,7 +8,7 @@ let to_list (#t:Type) (s: t_Slice t): list t = Seq.seq_to_list s
 let to_of_list_lemma t l = Seq.lemma_list_seq_bij l
 let of_to_list_lemma t l = Seq.lemma_seq_list_bij l
 
-let map_array #n (arr: t_Array 'a n) (f: 'a -> 'b): t_Array 'b n 
+let map_array #a #b #n (arr: t_Array a n) (f: a -> b): t_Array b n 
   = FStar.Seq.map_seq_len f arr;
     FStar.Seq.map_seq f arr 
 

proof-libs/fstar/core/Alloc.Slice.fst

@@ -2,4 +2,4 @@ module Alloc.Slice
 open Rust_primitives.Arrays
 open Alloc.Vec
 
-let impl__to_vec (s: t_Slice 'a): t_Vec 'a Alloc.Alloc.t_Global = s
+let impl__to_vec #a (s: t_Slice a): t_Vec a Alloc.Alloc.t_Global = s

proof-libs/fstar/core/Alloc.Vec.fst

@@ -13,19 +13,19 @@ let impl__with_capacity (_capacity: usize) = impl__new ()
 // TODO: missing precondition For now, `impl_1__push` has a wrong
 // semantics: pushing on a "full" vector does nothing. It should panic
 // instead.
-let impl_1__push
-  (v: t_Vec 't ())// Removed: {Seq.length v + 1 <= max_usize})
-  (x: 't)
-   : t_Vec 't () = 
+let impl_1__push #t
+  (v: t_Vec t ())// Removed: {Seq.length v + 1 <= max_usize})
+  (x: t)
+   : t_Vec t () = 
      if Seq.length v <= max_usize then v else
      FStar.Seq.append v (FStar.Seq.create 1 x)
 
-let impl_1__len (v: t_Vec 't ()) =
+let impl_1__len #t (v: t_Vec t ()) =
   let n = Seq.length v in
   assert (n <= maxint usize_inttype);
   mk_int #usize_inttype (Seq.length v)
 
-let from_elem (item: 'a) (len: usize) = Seq.create (v len) item
+let from_elem #a (item: a) (len: usize) = Seq.create (v len) item
 
 open Rust_primitives.Hax
 open Core.Ops.Index

proof-libs/fstar/core/Core.Array.fst

@@ -3,8 +3,8 @@ open Rust_primitives
 
 type t_TryFromSliceError = | TryFromSliceError
 
-let impl_23__map n (arr: t_Array 'a n) (f: 'a -> 'b): t_Array 'b n 
+let impl_23__map #a #b n (arr: t_Array a n) (f: a -> b): t_Array b n 
   = map_array arr f
 
-let impl_23__as_slice len (arr: t_Array 'a len): t_Slice 'a = arr
+let impl_23__as_slice #a len (arr: t_Array a len): t_Slice a = arr
 

proof-libs/fstar/core/Core.Convert.fst

@@ -4,7 +4,7 @@ open Rust_primitives
 
 class try_into_tc self t = {
   [@@@FStar.Tactics.Typeclasses.no_method]
-  f_Error: Type;
+  f_Error: Type0;
   f_try_into: self -> Core.Result.t_Result t f_Error
 }
 
@@ -35,7 +35,7 @@ class t_From self t = {
 
 class t_TryFrom self t = {
   [@@@FStar.Tactics.Typeclasses.no_method]
-  f_Error: Type;
+  f_Error: Type0;
   f_try_from: t -> Core.Result.t_Result self f_Error;
 }
 

proof-libs/fstar/core/Core.Iter.Traits.Collect.fst

@@ -1,8 +1,8 @@
 module Core.Iter.Traits.Collect
 
 class into_iterator self = {
-  f_IntoIter: Type;
-  // f_Item: Type;
+  f_IntoIter: Type0;
+  // f_Item: Type0;
   f_into_iter: self -> f_IntoIter;
 }
 

proof-libs/fstar/core/Core.Iter.Traits.Iterator.fst

@@ -21,7 +21,7 @@ unfold type t_all self item
 
 (* Inference behaves strangly with type synonyms... :( *)
 // class iterator (self: Type) = {
-//   f_Item: Type;
+//   f_Item: Type0;
 //   f_next:      t_next      self f_Item;
 //   f_contains:  t_contains  self f_Item; (* hax-specific method *)
 //   f_fold:      t_fold      self f_Item f_contains;

proof-libs/fstar/core/Core.Ops.Index.IndexMut.fst

@@ -1,7 +1,7 @@
 module Core.Ops.Index.IndexMut
 
 class t_IndexMut t_Self t_Idx = {
-  f_Input: Type;
+  f_Input: Type0;
   in_range: t_Self -> t_Idx -> Type0;
   f_index_mut: s:t_Self -> i:t_Idx{in_range s i} -> v:f_Input -> t_Self;
 }

proof-libs/fstar/core/Core.Ops.Index.fst

@@ -1,7 +1,7 @@
 module Core.Ops.Index
 
 class t_Index t_Self t_Idx = {
-  f_Output: Type;
+  f_Output: Type0;
   in_range: t_Self -> t_Idx -> Type0;
   f_index: s:t_Self -> i:t_Idx{in_range s i} -> f_Output;
 }

proof-libs/fstar/core/Core.Ops.Range.fsti

@@ -8,10 +8,10 @@ type t_RangeFull           = | RangeFull
 
 open Core.Iter.Traits.Iterator
 
-let rec fold_range' #t
+let rec fold_range' #a #t
   (min: Rust_primitives.int_t t) (max: Rust_primitives.int_t t {v min <= v max})
-  (init: 'a) (f: ('a -> i:Rust_primitives.int_t t{v i < v max /\ v i >= v min} -> 'a))
-  : Tot 'a (decreases (v max - v min))
+  (init: a) (f: (a -> i:Rust_primitives.int_t t{v i < v max /\ v i >= v min} -> a))
+  : Tot a (decreases (v max - v min))
   = if min = max
     then init
     else fold_range' (add min (Rust_primitives.mk_int 1)) max (f init min) f

proof-libs/fstar/core/Core.Ops.Try_trait.fst

@@ -5,8 +5,8 @@ class t_FromResidual self r = {
 }
 
 class t_Try self = {
-   f_Output: Type;
-   f_Residual: Type;
+   f_Output: Type0;
+   f_Residual: Type0;
    [@@@FStar.Tactics.Typeclasses.tcresolve]
    parent_FromResidual: t_FromResidual f_Residual f_Residual;
 

proof-libs/fstar/core/Core.Option.fst

@@ -2,12 +2,12 @@ module Core.Option
 
 type t_Option t = | Option_Some of t | Option_None
 
-let impl__and_then (self: t_Option 'self) (f: 'self -> t_Option 't): t_Option 't = 
+let impl__and_then #t #t_Self (self: t_Option t_Self) (f: t_Self -> t_Option t): t_Option t = 
   match self with
   | Option_Some x -> f x
   | Option_None -> Option_None
 
 let impl__unwrap #t (x: t_Option t {Option_Some? x}): t = Option_Some?._0 x
 
-let impl__is_some (self: t_Option 'self): bool =  Option_Some? self
+let impl__is_some #t_Self (self: t_Option t_Self): bool =  Option_Some? self
 

proof-libs/fstar/core/Core.Result.fst

@@ -3,7 +3,7 @@ module Core.Result
 type t_Result t e = | Result_Ok: v:t -> t_Result t e
                     | Result_Err of e
 
-let impl__unwrap (x: t_Result 't 'e {Result_Ok? x}): 't = Result_Ok?.v x
+let impl__unwrap #t #e (x: t_Result t e {Result_Ok? x}): t = Result_Ok?.v x
 let impl__map_err #e1 #e2 (x: t_Result 't e1) (f: e1 -> e2): t_Result 't e2
   = match x with
   | Result_Ok v -> Result_Ok v

proof-libs/fstar/core/Core.Slice.fsti

@@ -8,12 +8,12 @@ let impl__len (#t: Type) (s: t_Slice t)
 
 open Core.Slice.Iter
 
-val impl__chunks (x: t_Slice 'a) (cs: usize): t_Chunks 'a
+val impl__chunks #a (x: t_Slice a) (cs: usize): t_Chunks a
 
-let impl__iter (s: t_Slice 't): t_Slice 't = s
+let impl__iter #t (s: t_Slice t): t_Slice t = s
 
-val impl__chunks_exact (x: t_Slice 'a) (cs: usize):
-    Pure (t_Slice (t_Slice 'a))
+val impl__chunks_exact #a (x: t_Slice a) (cs: usize):
+    Pure (t_Slice (t_Slice a))
     (requires True)
     (ensures (fun r -> forall i. i < v (length x) ==> length x ==  cs))
 

proof-libs/fstar/rust_primitives/Rust_primitives.Arrays.fst

@@ -8,7 +8,7 @@ let to_list (#t:Type) (s: t_Slice t): list t = Seq.seq_to_list s
 let to_of_list_lemma t l = Seq.lemma_list_seq_bij l
 let of_to_list_lemma t l = Seq.lemma_seq_list_bij l
 
-let map_array #n (arr: t_Array 'a n) (f: 'a -> 'b): t_Array 'b n 
+let map_array #a #b #n (arr: t_Array a n) (f: a -> b): t_Array b n 
   = FStar.Seq.map_seq_len f arr;
     FStar.Seq.map_seq f arr 
 

proof-libs/fstar/rust_primitives/Rust_primitives.Arrays.fsti

@@ -7,7 +7,7 @@ type t_Slice t = s:Seq.seq t{Seq.length s <= max_usize}
 type t_Array t (l:usize) = s: Seq.seq t { Seq.length s == v l }
 
 /// Length of a slice
-let length (s: t_Slice 'a): usize = sz (Seq.length s)
+let length (#a: Type) (s: t_Slice a): usize = sz (Seq.length s)
 
 /// Check whether a slice contains an item
 let contains (#t: eqtype) (s: t_Slice t) (x: t): bool = Seq.mem x s
@@ -18,17 +18,17 @@ val of_list (#t:Type) (l: list t {FStar.List.Tot.length l < maxint Lib.IntTypes.
 /// Converts an slice into a F* list
 val to_list (#t:Type) (s: t_Slice t): list t
 
-val map_array #n (arr: t_Array 'a n) (f: 'a -> 'b): t_Array 'b n
+val map_array (#a #b: Type) #n (arr: t_Array a n) (f: a -> b): t_Array b n
 
 /// Creates an array of size `l` using a function `f`
 val createi #t (l:usize) (f:(u:usize{u <. l} -> t))
     : Pure (t_Array t l)
       (requires True)
       (ensures (fun res -> (forall i. Seq.index res (v i) == f i)))
 
-unfold let map #p
-  (f:(x:'a{p x} -> 'b))
-  (s: t_Slice 'a {forall (i:nat). i < Seq.length s ==> p (Seq.index s i)}): t_Slice 'b
+unfold let map #a #b #p
+  (f:(x:a{p x} -> b))
+  (s: t_Slice a {forall (i:nat). i < Seq.length s ==> p (Seq.index s i)}): t_Slice b
   = createi (length s) (fun i -> f (Seq.index s (v i)))
 
 /// Concatenates two slices

proof-libs/fstar/rust_primitives/Rust_primitives.Hax.Control_flow_monad.Moption.fst

@@ -1,6 +1,6 @@
 module Rust_primitives.Hax.Control_flow_monad.Moption
 
-let run (f: Core.Option.t_Option (Core.Option.t_Option 'a)): Core.Option.t_Option 'a
+let run #a (f: Core.Option.t_Option (Core.Option.t_Option a)): Core.Option.t_Option a
     = match f with
     | Core.Option.Option_Some x -> x 
     | Core.Option.Option_None -> Core.Option.Option_None

proof-libs/fstar/rust_primitives/Rust_primitives.Hax.Control_flow_monad.Mresult.fst

@@ -1,6 +1,6 @@
 module Rust_primitives.Hax.Control_flow_monad.Mresult
 
-let run (f: Core.Result.t_Result (Core.Result.t_Result 'a 'e) 'e): Core.Result.t_Result 'a 'e
+let run #a #e (f: Core.Result.t_Result (Core.Result.t_Result a e) e): Core.Result.t_Result a e
     = match f with
     | Core.Result.Result_Ok x -> x 
     | Core.Result.Result_Err e -> Core.Result.Result_Err e

proof-libs/fstar/rust_primitives/Rust_primitives.Hax.Monomorphized_update_at.fsti

@@ -7,20 +7,21 @@ open Rust_primitives
 open Rust_primitives.Hax
 open Core.Ops.Range
 
-
 val update_at_usize
-  (s: t_Slice 't)
+  (#t: Type0)
+  (s: t_Slice t)
   (i: usize)
-  (x: 't)
-  : Pure (t_Array 't (length s))
+  (x: t)
+  : Pure (t_Array t (length s))
     (requires (v i < Seq.length s))
     (ensures (fun res -> res == Seq.upd s (v i) x))
 
 val update_at_range #n
-  (s: t_Slice 't)
+  (t: Type0)
+  (s: t_Slice t)
   (i: t_Range (int_t n))
-  (x: t_Slice 't)
-  : Pure (t_Array 't (length s))
+  (x: t_Slice t)
+  : Pure (t_Array t (length s))
     (requires (v i.f_start >= 0 /\ v i.f_start <= Seq.length s /\
                v i.f_end <= Seq.length s /\
                Seq.length x == v i.f_end - v i.f_start))
@@ -30,31 +31,34 @@ val update_at_range #n
                 Seq.slice res (v i.f_end) (Seq.length res) == Seq.slice s (v i.f_end) (Seq.length s)))
 
 val update_at_range_to #n
-  (s: t_Slice 't)
+  (t: Type0)
+  (s: t_Slice t)
   (i: t_RangeTo (int_t n))
-  (x: t_Slice 't)
-  : Pure (t_Array 't (length s))
+  (x: t_Slice t)
+  : Pure (t_Array t (length s))
     (requires (v i.f_end >= 0 /\ v i.f_end <= Seq.length s /\
                Seq.length x == v i.f_end))
     (ensures (fun res ->
                 Seq.slice res 0 (v i.f_end) == x /\
                 Seq.slice res (v i.f_end) (Seq.length res) == Seq.slice s (v i.f_end) (Seq.length s)))
 
 val update_at_range_from #n
-  (s: t_Slice 't)
+  (t: Type0)
+  (s: t_Slice t)
   (i: t_RangeFrom (int_t n))
-  (x: t_Slice 't)
-  : Pure (t_Array 't (length s))
+  (x: t_Slice t)
+  : Pure (t_Array t (length s))
     (requires ( v i.f_start >= 0 /\ v i.f_start <= Seq.length s /\
                 Seq.length x == Seq.length s - v i.f_start))
     (ensures (fun res ->
                 Seq.slice res 0 (v i.f_start) == Seq.slice s 0 (v i.f_start) /\
                 Seq.slice res (v i.f_start) (Seq.length res) == x))
 
 val update_at_range_full
-  (s: t_Slice 't)
+  (t: Type0)
+  (s: t_Slice t)
   (i: t_RangeFull)
-  (x: t_Slice 't)
-  : Pure (t_Array 't (length s))
+  (x: t_Slice t)
+  : Pure (t_Array t (length s))
     (requires (Seq.length x == Seq.length s))
     (ensures (fun res -> res == x))

proof-libs/fstar/rust_primitives/Rust_primitives.Hax.fst

@@ -6,7 +6,7 @@ open Rust_primitives.Arrays
 type t_Never = False
 let never_to_any #t: t_Never -> t = (fun _ -> match () with)
 
-let repeat (x: 'a) (len: usize): t_Array 'a len = 
+let repeat #a (x: a) (len: usize): t_Array a len = 
   FStar.Seq.create (v len) x
 
 open Core.Ops.Index