Upgrade to F* Universes

README.md

@@ -329,6 +329,15 @@ Then, whenever you make a change in your clones:
 Then, in EverParse, `make` will automatically rebuild F\*, Karamel and
 Pulse from your clones with your patches.
 
+## Using a specific branch of F\*, Karamel, Pulse etc. 
+
+1. Run `make -C opt FStar pulse karamel` to clone the default branches of those repositories
+
+2. In the cloned directories, switch to your branch, e.g., `git checkout <mybranch>`
+
+3. Then run `make -C opt snapshot` to record the hashes you intend to use
+
+
 ## Using an existing opam root, F\*, etc.
 
 If you want to use existing dependencies instead of letting EverParse

deps.Makefile

@@ -13,7 +13,7 @@ export EVERPARSE_OPT_PATH := $(shell cygpath -m $(EVERPARSE_OPT_PATH))
 NO_PULSE := 1
 endif
 
-Z3_VERSION := 4.13.3
+EVERPARSE_Z3_VERSION ?= 4.13.3
 
 ifeq (1,$(EVERPARSE_USE_MY_DEPS))
 export EVERPARSE_USE_OPAMROOT:=1
@@ -51,7 +51,7 @@ NEED_FSTAR :=
 ifneq (1,$(EVERPARSE_USE_FSTAR_EXE))
 export FSTAR_EXE := $(EVERPARSE_OPT_PATH)/FStar/out/bin/fstar.exe
 NEED_FSTAR := $(EVERPARSE_OPT_PATH)/FStar.done
-z3_exe := $(shell $(FSTAR_EXE) --locate_z3 \$(Z3_VERSION) 2>/dev/null)
+z3_exe := $(shell $(FSTAR_EXE) --locate_z3 \$(EVERPARSE_Z3_VERSION) 2>/dev/null)
 ifneq (0,$(.SHELLSTATUS))
 z3_exe :=
 endif
@@ -74,7 +74,7 @@ endif
 
 NEED_Z3 :=
 ifeq (,$(z3_exe))
-z3_exe := $(shell which z3-$(Z3_VERSION))
+z3_exe := $(shell which z3-$(EVERPARSE_Z3_VERSION))
 ifneq (0,$(.SHELLSTATUS))
 z3_exe :=
 endif
@@ -170,6 +170,7 @@ ifeq ($(OS),Windows_NT)
 else
 	@echo export EVERPARSE_HOME=$(CURDIR)
 endif
+	@echo export EVERPARSE_Z3_VERSION=$(EVERPARSE_Z3_VERSION)
 	@echo export PATH=\"$(z3_dir):'$$PATH'\"
 
 .PHONY: env

fstar.sh

@@ -3,4 +3,4 @@ set -e
 unset CDPATH
 EVERPARSE_HOME="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
 source "$EVERPARSE_HOME"/env.sh
-exec "$FSTAR_EXE" --include "$KRML_HOME/krmllib" --include "$KRML_HOME/krmllib/obj" --include "$PULSE_HOME/lib/pulse" "$@"
+exec "$FSTAR_EXE" --z3version $EVERPARSE_Z3_VERSION --include "$KRML_HOME/krmllib" --include "$KRML_HOME/krmllib/obj" --include "$PULSE_HOME/lib/pulse" "$@"

opt/hashes.Makefile

@@ -1,3 +1,3 @@
-FStar_hash := 1cff8d796deed8834926389a986d015498780041
-karamel_hash := fb36fecb552c9fb202beb38a6c5a732c3f2cd49f
-pulse_hash := f51670f4c0117c8614e10c421025d77e1e44940e
+FStar_hash := f1a55bbbe7dcac6c99033bd22fd73b74a3bea237
+karamel_hash := 9c4744acf0d663c6fc079fb318820f4188971652
+pulse_hash := afc380e13aeacc0e4f18d605735056ef9789062e

src/ASN1/ASN1.X509.fst

@@ -1,4 +1,5 @@
 module ASN1.X509
+#push-options "--split_queries no --fuel 2 --ifuel 0"
 
 module U32 = FStar.UInt32
 module List = FStar.List.Tot
@@ -302,11 +303,12 @@ let id_pe = id_pkix /+ 1
 let id_pe_authorityInformationAccess = id_pe /+ 1
 
 //Warning: Partly using the mitls spec which is loosened from rfc5280
-
+#push-options "--fuel 3 --ifuel 1"
 let mk_expansion (critical : asn1_gen_item_k) (#s : _) (value : asn1_k s)
   (pf : squash (asn1_sequence_k_wf [proj2_of_3 critical; (Set.singleton octetstring_id, PLAIN)]))
 = let items = [critical; "extnValue" *^ (PLAIN ^: (ASN1_ILC octetstring_id (ASN1_PREFIXED value)))] in
   mk_gen_items items pf
+#pop-options
 
 let critical_field
 = mk_default_field asn1_boolean false
@@ -562,8 +564,7 @@ let extension
 let extensions
 = asn1_sequence_of extension
 
-#push-options "--z3rlimit 16"
-
+#push-options "--fuel 0 --z3rlimit_factor 2"
 let x509_TBSCertificate
 = asn1_sequence [
     "version" *^ (PLAIN ^: (mk_prefixed (mk_custom_id CONTEXT_SPECIFIC CONSTRUCTED 0) version));
@@ -578,14 +579,13 @@ let x509_TBSCertificate
     "extensions" *^ (OPTION ^: (mk_prefixed (mk_custom_id CONTEXT_SPECIFIC CONSTRUCTED 3) extensions))]
     (_ by (seq_tac ()))
 
-#pop-options
-
 let x509_certificate
 = asn1_sequence [
     "tbsCertificate" *^ (PLAIN ^: x509_TBSCertificate);
     "signatureAlgorithm" *^ (PLAIN ^: algorithmIdentifier);
     "signatureValue" *^ (PLAIN ^: asn1_bitstring)]
     (_ by (seq_tac ()))
+#pop-options
 
 // let's go boom!
 
@@ -605,4 +605,4 @@ let parse_cert (b:bytes) = x509_certificate_parser b
                              iota;
                              primops]]
 let dparse_cert (b:bytes) = dasn1_as_parser x509_certificate b
-
+#show-options

src/cbor/pulse/CBOR.Pulse.API.Base.fst

@@ -872,7 +872,7 @@ let mk_array_from_array_t
 inline_for_extraction
 noextract [@@noextract_to "krml"]
 fn mk_array_from_array'
-  (#t: Type)
+  (#t: Type0)
   (#vmatch: perm -> t -> cbor -> slprop)
   (mk_array_from_array: mk_array_from_array_t vmatch)
   (a: A.array t)
@@ -1154,8 +1154,10 @@ fn mk_map_gen
   let bres = mk_map_gen_by_ref a dest;
   if bres {
     let res = !dest;
+    with res' . rewrite mk_map_gen_post vmatch1 vmatch2 a va pv vv res' as mk_map_gen_post vmatch1 vmatch2 a va pv vv (Some res);
     Some res
   } else {
+    with res' . rewrite mk_map_gen_post vmatch1 vmatch2 a va pv vv res' as mk_map_gen_post vmatch1 vmatch2 a va pv vv None;
     None #t1
   }
 }
@@ -1411,6 +1413,7 @@ fn mk_map_from_ref
   PM.seq_list_match_length (vmatch2 pv) va vv;
   let _ = mk_map_gen a dest;
   let res = !dest;
+  with res' . rewrite (mk_map_gen_post vmatch1 vmatch2 a va pv vv res') as (mk_map_gen_post vmatch1 vmatch2 a va pv vv (Some res));
   unfold (mk_map_gen_post vmatch1 vmatch2 a va pv vv (Some res));
   res
 }
@@ -1514,8 +1517,10 @@ fn map_get_as_option
   let bres = m x k dest;
   if bres {
     let res = !dest;
+    with res' . rewrite map_get_post vmatch x px vx vk res' as map_get_post vmatch x px vx vk (Some res);
     Some res
   } else {
+    with res' . rewrite map_get_post vmatch x px vx vk res' as map_get_post vmatch x px vx vk None;
     None #t
   }
 }

src/cbor/pulse/CBOR.Pulse.API.Det.Rust.Macros.fst

@@ -20,7 +20,13 @@ fn cbor_det_mk_int64'
   (v: _)
 {
   let mty = (if ty = cbor_major_type_uint64 then UInt64 else NegInt64);
-  cbor_det_mk_int64 mty v
+  let res = cbor_det_mk_int64 mty v;
+  with ty' . rewrite cbor_det_match 1.0R
+      res
+      (CBOR.Spec.API.Type.pack (CBOR.Spec.API.Type.CInt64 ty' v)) as cbor_det_match 1.0R
+      res
+      (CBOR.Spec.API.Type.pack (CBOR.Spec.API.Type.CInt64 ty v));
+  res
 }
 
 inline_for_extraction
@@ -32,6 +38,11 @@ fn cbor_det_mk_simple'
 {
   let Some res = cbor_det_mk_simple_value v;
   unfold (cbor_det_mk_simple_value_post v (Some res));
+  with res' . rewrite cbor_det_match 1.0R
+      res
+      res' as cbor_det_match 1.0R
+      res
+      (CBOR.Spec.API.Type.pack (CBOR.Spec.API.Type.CSimple v));
   res
 }
 
@@ -49,6 +60,7 @@ fn cbor_det_mk_string0
   let mty = (if ty = cbor_major_type_byte_string then ByteString else TextString);
   let res = cbor_det_mk_string mty s;
   let Some c = res;
+  with ty' res' . rewrite (cbor_det_mk_string_post ty' s p v res') as (cbor_det_mk_string_post ty s p v (Some c));
   unfold (cbor_det_mk_string_post ty s p v (Some c));
   c
 }
@@ -230,7 +242,7 @@ fn cbor_det_array_iterator_start'
   with p' . assert (cbor_det_view_match p' v y);
   let Array a = v;
   Trade.rewrite_with_trade
-    (cbor_det_view_match p' v y)
+    (cbor_det_view_match p' _ y)
     (cbor_det_array_match p' a y);
   Trade.trans _ _ (cbor_det_match p x y);
   let res = cbor_det_array_iterator_start a;
@@ -252,7 +264,7 @@ fn cbor_det_get_array_item'
   with p' . assert (cbor_det_view_match p' v y);
   let Array a = v;
   Trade.rewrite_with_trade
-    (cbor_det_view_match p' v y)
+    (cbor_det_view_match p' _ y)
     (cbor_det_array_match p' a y);
   Trade.trans _ _ (cbor_det_match p x y);
   let ores = cbor_det_get_array_item a i;
@@ -295,7 +307,7 @@ fn cbor_det_map_iterator_start'
   with p' . assert (cbor_det_view_match p' v y);
   let Map a = v;
   Trade.rewrite_with_trade
-    (cbor_det_view_match p' v y)
+    (cbor_det_view_match p' _ y)
     (cbor_det_map_match p' a y);
   Trade.trans _ _ (cbor_det_match p x y);
   let res = cbor_det_map_iterator_start a;
@@ -326,13 +338,15 @@ ensures
       unfold (safe_map_get_post m p' vx vk None);
       Trade.elim _ _;
       fold (Base.map_get_post_none cbor_det_match x px vx vk);
-      fold (Base.map_get_post cbor_det_match x px vx vk None)
+      fold (Base.map_get_post cbor_det_match x px vx vk None);
+      rewrite (Base.map_get_post cbor_det_match x px vx vk None) as (Base.map_get_post cbor_det_match x px vx vk res)
     }
     Some x' -> {
       unfold (safe_map_get_post m p' vx vk (Some x'));
       Trade.trans _ _ (cbor_det_match px x vx);
       fold (Base.map_get_post_some cbor_det_match x px vx vk x');
-      fold (Base.map_get_post cbor_det_match x px vx vk (Some x'))
+      fold (Base.map_get_post cbor_det_match x px vx vk (Some x'));
+      rewrite (Base.map_get_post cbor_det_match x px vx vk (Some x')) as (Base.map_get_post cbor_det_match x px vx vk res);
     }
   }
 }
@@ -353,7 +367,7 @@ fn cbor_det_map_get'
   with p' . assert (cbor_det_view_match p' x' vx);
   let Map m = x';
   Trade.rewrite_with_trade
-    (cbor_det_view_match p' x' vx)
+    (cbor_det_view_match p' _ vx)
     (cbor_det_map_match p' m vx);
   Trade.trans _ _ (cbor_det_match px x vx);
   let res = cbor_det_map_get m k;

src/cbor/pulse/raw/CBOR.Pulse.API.Det.C.fst

@@ -216,6 +216,8 @@ ensures
       unfold (mk_map_gen_post vmatch1 vmatch2 s va pv vv None);
       S.to_array s;
       fold (mk_map_from_array_safe_post vmatch1 vmatch2 a va pv vv vdest false);
+      rewrite (mk_map_from_array_safe_post vmatch1 vmatch2 a va pv vv vdest false)
+        as (mk_map_from_array_safe_post vmatch1 vmatch2 a va pv vv vdest bres);
     }
     Some vres -> {
       unfold (mk_map_gen_post vmatch1 vmatch2 s va pv vv (Some vres));
@@ -233,6 +235,8 @@ ensures
       Trade.trans_concl_l _ _ _ _;
       rewrite each vres as vdest;
       fold (mk_map_from_array_safe_post vmatch1 vmatch2 a va pv vv vdest true);
+      rewrite (mk_map_from_array_safe_post vmatch1 vmatch2 a va pv vv vdest true)
+        as (mk_map_from_array_safe_post vmatch1 vmatch2 a va pv vv vdest bres);
     }
   }
 }