Merge pull request #440 from hacspec/fix-core-ops-range-tc

Fix core ops range tc

proof-libs/fstar-secret-integers/.envrc

@@ -0,0 +1 @@
+use flake .#fstar

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.Range.fsti

@@ -97,7 +97,7 @@ let update_at_tc_array_range_to_super t l n: t_Index (t_Array t l) (t_RangeTo (p
   = FStar.Tactics.Typeclasses.solve
 let update_at_tc_array_range_from_super t l n: t_Index (t_Array t l) (t_RangeFrom (pub_int_t n))
   = FStar.Tactics.Typeclasses.solve
-let update_at_tc_array_range_full_super t l n: t_Index (t_Array t l) t_RangeFull
+let update_at_tc_array_range_full_super t l: t_Index (t_Array t l) t_RangeFull
   = FStar.Tactics.Typeclasses.solve
 
 val update_at_array_range t l n
@@ -109,9 +109,9 @@ val update_at_array_range_to t l n
 val update_at_array_range_from t l n
   (s: t_Array t l) (i: t_RangeFrom (pub_int_t n) {(update_at_tc_array_range_from_super t l n).in_range s i})
   : (update_at_tc_array_range_from_super t l n).f_Output -> t_Array t l
-val update_at_array_range_full t l n
+val update_at_array_range_full t l
   (s: t_Array t l) (i: t_RangeFull)
-  : (update_at_tc_array_range_full_super t l n).f_Output -> t_Array t l
+  : (update_at_tc_array_range_full_super t l).f_Output -> t_Array t l
 
 instance update_at_tc_array_range t l n: update_at_tc (t_Array t l) (t_Range (pub_int_t n)) = {
   super_index = update_at_tc_array_range_super t l n;
@@ -125,7 +125,7 @@ instance update_at_tc_array_range_from t l n: update_at_tc (t_Array t l) (t_Rang
   super_index = update_at_tc_array_range_from_super t l n;
   update_at = update_at_array_range_from t l n
 }
-instance update_at_tc_array_range_full t l n: update_at_tc (t_Array t l) t_RangeFull = {
-  super_index = update_at_tc_array_range_full_super t l n;
-  update_at = update_at_array_range_full t l n
+instance update_at_tc_array_range_full t l: update_at_tc (t_Array t l) t_RangeFull = {
+  super_index = update_at_tc_array_range_full_super t l;
+  update_at = update_at_array_range_full t l
 }

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) :

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

@@ -96,7 +96,7 @@ let update_at_tc_array_range_to_super t l n: t_Index (t_Array t l) (t_RangeTo (i
   = FStar.Tactics.Typeclasses.solve
 let update_at_tc_array_range_from_super t l n: t_Index (t_Array t l) (t_RangeFrom (int_t n))
   = FStar.Tactics.Typeclasses.solve
-let update_at_tc_array_range_full_super t l n: t_Index (t_Array t l) t_RangeFull
+let update_at_tc_array_range_full_super t l: t_Index (t_Array t l) t_RangeFull
   = FStar.Tactics.Typeclasses.solve
 
 val update_at_array_range t l n
@@ -108,9 +108,9 @@ val update_at_array_range_to t l n
 val update_at_array_range_from t l n
   (s: t_Array t l) (i: t_RangeFrom (int_t n) {(update_at_tc_array_range_from_super t l n).in_range s i})
   : (update_at_tc_array_range_from_super t l n).f_Output -> t_Array t l
-val update_at_array_range_full t l n
+val update_at_array_range_full t l
   (s: t_Array t l) (i: t_RangeFull)
-  : (update_at_tc_array_range_full_super t l n).f_Output -> t_Array t l
+  : (update_at_tc_array_range_full_super t l).f_Output -> t_Array t l
 
 instance update_at_tc_array_range t l n: update_at_tc (t_Array t l) (t_Range (int_t n)) = {
   super_index = update_at_tc_array_range_super t l n;
@@ -124,7 +124,7 @@ instance update_at_tc_array_range_from t l n: update_at_tc (t_Array t l) (t_Rang
   super_index = update_at_tc_array_range_from_super t l n;
   update_at = update_at_array_range_from t l n
 }
-instance update_at_tc_array_range_full t l n: update_at_tc (t_Array t l) t_RangeFull = {
-  super_index = update_at_tc_array_range_full_super t l n;
-  update_at = update_at_array_range_full t l n
+instance update_at_tc_array_range_full t l: update_at_tc (t_Array t l) t_RangeFull = {
+  super_index = update_at_tc_array_range_full_super t l;
+  update_at = update_at_array_range_full t l
 }

proof-libs/fstar/core/Makefile

@@ -6,7 +6,7 @@
 #
 # We expect FSTAR_HOME to be set to your FSTAR repo/install directory
 # We expect HACL_HOME to be set to your HACL* repo location
-# We expect HAX_LIBS_HOME to be set to the folder containing core, rust_primitives etc.
+# We expect HAX_PROOF_LIBS_HOME to be set to the folder containing core, rust_primitives etc.
 #
 # ROOTS contains all the top-level F* files you wish to verify
 # The default target `verify` verified ROOTS and its dependencies
@@ -29,13 +29,13 @@
 # (setq fstar-subp-prover-args #'my-fstar-compute-prover-args-using-make)
 #
 
-HAX_LIBS_HOME ?= $(shell git rev-parse --show-toplevel)/proof-libs/fstar
-FSTAR_HOME    ?= $(HAX_LIBS_HOME)/../../../FStar
-HACL_HOME     ?= $(HAX_LIBS_HOME)/../../../hacl-star
+HAX_PROOF_LIBS_HOME ?= $(shell git rev-parse --show-toplevel)/proof-libs/fstar
+FSTAR_HOME    ?= $(HAX_PROOF_LIBS_HOME)/../../../FStar
+HACL_HOME     ?= $(HAX_PROOF_LIBS_HOME)/../../../hacl-star
 FSTAR_BIN     ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe")
 
-CACHE_DIR     ?= $(HAX_LIBS_HOME)/.cache
-HINT_DIR      ?= $(HAX_LIBS_HOME)/.hints
+CACHE_DIR     ?= $(HAX_PROOF_LIBS_HOME)/.cache
+HINT_DIR      ?= $(HAX_PROOF_LIBS_HOME)/.hints
 
 .PHONY: all verify clean
 
@@ -47,7 +47,7 @@ all:
 # *extend* the set of relevant files with the tests.
 ROOTS = $(wildcard *.fst)
 
-FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib $(HAX_LIBS_HOME)/rust_primitives $(HAX_LIBS_HOME)/core $(HAX_LIBS_HOME)/hax_lib
+FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib $(HAX_PROOF_LIBS_HOME)/rust_primitives $(HAX_PROOF_LIBS_HOME)/core $(HAX_PROOF_LIBS_HOME)/hax_lib
 
 FSTAR_FLAGS = --cmi \
   --warn_error -331 \