trying to set universes

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

@@ -1,6 +1,6 @@
 module Core.Ops.Index
 
-class t_Index t_Self t_Idx = {
+class t_Index (t_Self:Type0) (t_Idx:Type0) = {
   f_Output: Type;
   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.Ops.fst

@@ -21,7 +21,7 @@ instance negation_for_bool: negation_tc bool = {
 
 open Core.Ops.Index
 
-let ( .[] ) #self #idx {| inst: t_Index self idx |}
+let ( .[] ) (#self:Type0) (#idx:Type0) {| inst: t_Index self idx |}
   : s:self -> i:idx{in_range s i} -> inst.f_Output
   = f_index
 

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

@@ -7,18 +7,20 @@ open Core.Ops.Range
 #set-options "--z3rlimit 30"
 
 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 (pub_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))
@@ -28,31 +30,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 (pub_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 (pub_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-secret-integers/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 (#t:Type0) (x: t) (len: usize): t_Array t len = 
   FStar.Seq.create (v len) x
 
 open Core.Ops.Index

proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Integers.fsti

@@ -87,8 +87,8 @@ type pub_i64=  pub_int_t LI.S64
 type pub_u128 = pub_int_t LI.U128
 type pub_i128 = pub_int_t LI.S128
 
-type usize = int_t_l usize_inttype LI.PUB
-type isize = int_t_l isize_inttype LI.PUB
+type usize = pub_int_t usize_inttype
+type isize = pub_int_t isize_inttype
 
 let minint (t:LI.inttype) =
   if unsigned t then 0 else -(pow2 (bits t - 1))
@@ -117,7 +117,7 @@ val mk_int_l (#t:inttype) (#l:LI.secrecy_level) (n:range_t t) : int_t_l t l
 let mk_int (#t:inttype) (n:range_t t) : int_t t = mk_int_l n
 
 [@(strict_on_arguments [0])]
-let mk_pub_int (#t:inttype) (n:range_t t) : int_t_l t LI.PUB = mk_int_l n
+let mk_pub_int (#t:inttype) (n:range_t t) : pub_int_t t = mk_int_l n
 
 [@(strict_on_arguments [0])]
 val mk_int_equiv_lemma #t (n:range_t t) :