Make DY* library and implementations verify with Z3 4.13.3 and F* 2025.09.04. Update HACL* snapshot as well. Remove mac_pred requirement for verify_mac.

LabeledCryptoAPI.fsti

@@ -507,12 +507,12 @@ val mac_lemma: #p:global_usage -> #i:timestamp -> #l:label -> #l':label ->
 
 val verify_mac: #p:global_usage -> #i:timestamp -> #l:label -> #l':label ->
     k:lbytes p i l{is_publishable p i k \/ (exists s. is_mac_key p i k l s)} ->
-    m:msg p i l'{forall s. is_mac_key p i k l s ==> mac_pred p.usage_preds i s k m} -> 
+    m:msg p i l' -> 
     t:msg p i l' -> bool
 
 val verify_mac_lemma: #p:global_usage -> #i:timestamp -> #l:label -> #l':label ->
     k:lbytes p i l{is_publishable p i k \/ (exists s. is_mac_key p i k l s)} ->
-    m:msg p i l'{forall s. is_mac_key p i k l s ==> mac_pred p.usage_preds i s k m} ->
+    m:msg p i l' ->
     t:msg p i l' ->
     Lemma (if verify_mac k m t then 
 	      C.verify_mac k m t /\

Makefile

@@ -26,7 +26,7 @@ FSTAR_FLAGS = --cmi \
   --already_cached "+Prims +FStar +LowStar +C +Spec.Loops +TestLib" \
   $(addprefix --include ,$(FSTAR_INCLUDE_DIRS))
 
-FSTAR = $(FSTAR_HOME)/bin/fstar.exe $(FSTAR_FLAGS) $(OTHERFLAGS)
+FSTAR = $(FSTAR_HOME)/bin/fstar.exe $(FSTAR_FLAGS) $(OTHERFLAGS) --z3version 4.13.3
 
 ENABLE_HINTS = --use_hints --use_hint_hashes --record_hints # --query_stats
 

Makefile.concrete

@@ -28,7 +28,7 @@ FSTAR_FLAGS = --cmi \
   --already_cached "+Prims +FStar +LowStar +C +TestLib" \
   $(addprefix --include ,$(FSTAR_INCLUDE_DIRS))
 
-FSTAR = $(FSTAR_HOME)/bin/fstar.exe $(FSTAR_FLAGS) $(OTHERFLAGS)
+FSTAR = $(FSTAR_HOME)/bin/fstar.exe $(FSTAR_FLAGS) $(OTHERFLAGS) --z3version 4.13.3
 
 ENABLE_HINTS = --use_hints --use_hint_hashes --record_hints # --query_stats
 

SecurityLemmas.fst

@@ -43,7 +43,7 @@ val attacker_only_derives_public_values_:
     (requires (valid_trace pr h /\ later_than (trace_len h) i))
     (ensures (forall t. Att.attacker_can_derive i steps t ==> is_publishable pr.global_usage i t))
 
-#push-options "--z3rlimit 50"
+#push-options "--z3rlimit 200"
 let rec attacker_only_derives_public_values_ pr h i steps =
   if steps = 0 then (
         strings_are_publishable_forall pr.global_usage;

comparse/Comparse.Parser.Derived.fst

@@ -591,6 +591,7 @@ let ps_quic_nat #bytes #bl =
     a_to_b b_to_a
     a_to_b_to_a
     b_to_a_to_b
+#pop-options
 
 let ps_quic_nat_length #bytes #bl n =
   assert_norm(pow2 0 == 1);

comparse/Makefile

@@ -25,7 +25,7 @@ FSTAR_FLAGS = --cmi \
   --already_cached "+Prims +FStar +LowStar +C +Spec.Loops +TestLib" \
   $(addprefix --include ,$(FSTAR_INCLUDE_DIRS))
 
-FSTAR = $(FSTAR_HOME)/bin/fstar.exe $(FSTAR_FLAGS) $(OTHERFLAGS)
+FSTAR = $(FSTAR_HOME)/bin/fstar.exe $(FSTAR_FLAGS) $(OTHERFLAGS) --z3version 4.13.3
 
 ENABLE_HINTS = --use_hints --use_hint_hashes --record_hints # --query_stats
 

comparse/Makefile.concrete

@@ -28,7 +28,7 @@ FSTAR_FLAGS = --cmi \
   --already_cached "+Prims +FStar +LowStar +C +TestLib" \
   $(addprefix --include ,$(FSTAR_INCLUDE_DIRS))
 
-FSTAR = $(FSTAR_HOME)/bin/fstar.exe $(FSTAR_FLAGS) $(OTHERFLAGS)
+FSTAR = $(FSTAR_HOME)/bin/fstar.exe $(FSTAR_FLAGS) $(OTHERFLAGS) --z3version 4.13.3
 
 ENABLE_HINTS = --use_hints --use_hint_hashes --record_hints # --query_stats
 

concrete/hacl-star-snapshot/ml/FStar_Kremlin_Endianness.ml

@@ -33,7 +33,7 @@ let rec (n_to_le :
          let byte = FStar_UInt8.uint_to_t (n mod (Prims.of_int (256))) in
          let n' = n / (Prims.of_int (256)) in
          let b' = n_to_le len1 n' in
-         let b = FStar_Seq_Properties.cons byte b' in b)
+         let b = FStar_Seq_Base.cons byte b' in b)
 let rec (n_to_be :
   FStar_UInt32.t -> Prims.nat -> FStar_UInt8.t FStar_Seq_Base.seq) =
   fun len ->
@@ -86,7 +86,7 @@ let rec (seq_uint32_of_le :
         (let uu___1 = FStar_Seq_Properties.split b (Prims.of_int (4)) in
          match uu___1 with
          | (hd, tl) ->
-             FStar_Seq_Properties.cons (uint32_of_le hd)
+             FStar_Seq_Base.cons (uint32_of_le hd)
                (seq_uint32_of_le (l - Prims.int_one) tl))
 let rec (le_of_seq_uint32 :
   FStar_UInt32.t FStar_Seq_Base.seq -> FStar_UInt8.t FStar_Seq_Base.seq) =
@@ -108,7 +108,7 @@ let rec (seq_uint32_of_be :
         (let uu___1 = FStar_Seq_Properties.split b (Prims.of_int (4)) in
          match uu___1 with
          | (hd, tl) ->
-             FStar_Seq_Properties.cons (uint32_of_be hd)
+             FStar_Seq_Base.cons (uint32_of_be hd)
                (seq_uint32_of_be (l - Prims.int_one) tl))
 let rec (be_of_seq_uint32 :
   FStar_UInt32.t FStar_Seq_Base.seq -> FStar_UInt8.t FStar_Seq_Base.seq) =
@@ -130,7 +130,7 @@ let rec (seq_uint64_of_le :
         (let uu___1 = FStar_Seq_Properties.split b (Prims.of_int (8)) in
          match uu___1 with
          | (hd, tl) ->
-             FStar_Seq_Properties.cons (uint64_of_le hd)
+             FStar_Seq_Base.cons (uint64_of_le hd)
                (seq_uint64_of_le (l - Prims.int_one) tl))
 let rec (le_of_seq_uint64 :
   FStar_UInt64.t FStar_Seq_Base.seq -> FStar_UInt8.t FStar_Seq_Base.seq) =
@@ -152,7 +152,7 @@ let rec (seq_uint64_of_be :
         (let uu___1 = FStar_Seq_Properties.split b (Prims.of_int (8)) in
          match uu___1 with
          | (hd, tl) ->
-             FStar_Seq_Properties.cons (uint64_of_be hd)
+             FStar_Seq_Base.cons (uint64_of_be hd)
                (seq_uint64_of_be (l - Prims.int_one) tl))
 let rec (be_of_seq_uint64 :
   FStar_UInt64.t FStar_Seq_Base.seq -> FStar_UInt8.t FStar_Seq_Base.seq) =

concrete/hacl-star-snapshot/ml/Lib_Meta.ml

@@ -67,5 +67,5 @@ let rec (as_uint8s :
 let (from_hex :
   Prims.string -> (FStar_UInt8.t, unit) FStar_Seq_Properties.lseq) =
   fun s ->
-    FStar_Seq_Properties.seq_of_list
-      (as_uint8s [] (FStar_String.list_of_string s))
+    FStar_Seq_Base.seq_of_list
+      (as_uint8s [] (FStar_String.list_of_string s))

concrete/hacl-star-snapshot/ml/Lib_Sequence.ml

@@ -20,9 +20,9 @@ let op_At_Bar :
       Prims.nat -> ('a, unit) lseq -> ('a, unit) lseq -> ('a, unit) lseq
   = fun len0 -> fun len1 -> fun s0 -> fun s1 -> concat len0 len1 s0 s1
 let to_list : 'a . 'a seq -> 'a Prims.list =
-  fun s -> FStar_Seq_Properties.seq_to_list s
+  fun s -> FStar_Seq_Base.seq_to_list s
 let of_list : 'a . 'a Prims.list -> ('a, unit) lseq =
-  fun l -> FStar_Seq_Properties.seq_of_list l
+  fun l -> FStar_Seq_Base.seq_of_list l
 
 type ('a, 'len, 's1, 's2) equal = unit
 

concrete/hacl-star-snapshot/ml/Spec_HMAC_DRBG.ml

@@ -1,3 +1,7 @@
+module FStar_Seq_Properties = struct
+  include FStar_Seq_Base
+  include FStar_Seq_Properties
+end
 open Prims
 let (is_supported_alg : Spec_Hash_Definitions.hash_alg -> Prims.bool) =
   fun uu___ ->
@@ -227,4 +231,4 @@ let (generate' :
                                   (k1, v2,
                                     ((__proj__State__item__reseed_counter a
                                         st)
-                                       + Prims.int_one)))))))
+                                       + Prims.int_one)))))))

concrete/hacl-star-snapshot/ml/Spec_HMAC_DRBG_Test.ml

@@ -8,10 +8,10 @@ let (print_and_compare :
       fun test_result ->
         FStar_IO.print_string "\n\nResult:   ";
         FStar_List.iter (fun a -> FStar_IO.print_uint8_hex_pad a)
-          (FStar_Seq_Properties.seq_to_list test_result);
+          (FStar_Seq_Base.seq_to_list test_result);
         FStar_IO.print_string "\nExpected: ";
         FStar_List.iter (fun a -> FStar_IO.print_uint8_hex_pad a)
-          (FStar_Seq_Properties.seq_to_list test_expected);
+          (FStar_Seq_Base.seq_to_list test_expected);
         (let res =
            Obj.magic
              (Lib_ByteSequence.seq_eq_mask Lib_IntTypes.U8 len len

concrete/hacl-star-snapshot/ml/Spec_Hash_Test.ml

@@ -6167,11 +6167,11 @@ let (test_one : vec -> Prims.bool) =
     match uu___ with
     | Vec (a, plain, tag) ->
         let expected =
-          FStar_Seq_Properties.seq_of_list
+          FStar_Seq_Base.seq_of_list
             (FStar_List_Tot_Base.map (fun x -> x) tag) in
         let computed =
           Spec_Agile_Hash.hash a
-            (FStar_Seq_Properties.seq_of_list
+            (FStar_Seq_Base.seq_of_list
                (FStar_List_Tot_Base.map (fun x -> x) plain)) in
         print_and_compare "\nExpected: " "\nComputed: "
           (Spec_Hash_Definitions.hash_length a) expected computed

concrete/hacl-star-snapshot/ml/Spec_Loops.ml

@@ -7,7 +7,7 @@ let rec seq_map :
       then FStar_Seq_Base.empty ()
       else
         (let s' =
-           FStar_Seq_Properties.cons (f (FStar_Seq_Properties.head s))
+           FStar_Seq_Base.cons (f (FStar_Seq_Properties.head s))
              (seq_map f (FStar_Seq_Properties.tail s)) in
          s')
 let rec seq_map2 :
@@ -22,7 +22,7 @@ let rec seq_map2 :
         then FStar_Seq_Base.empty ()
         else
           (let s'' =
-             FStar_Seq_Properties.cons
+             FStar_Seq_Base.cons
                (f (FStar_Seq_Properties.head s)
                   (FStar_Seq_Properties.head s'))
                (seq_map2 f (FStar_Seq_Properties.tail s)

concrete/hacl-star-snapshot/ml/Spec_MD5.ml

@@ -1,3 +1,7 @@
+module FStar_Seq_Properties = struct
+  include FStar_Seq_Base
+  include FStar_Seq_Properties
+end
 open Prims
 let (init_as_list : FStar_UInt32.t Prims.list) =
   [FStar_UInt32.uint_to_t (Prims.parse_int "0x67452301");
@@ -546,4 +550,4 @@ let (update : unit Spec_Hash_Definitions.update_t) = update_aux
 let (pad : unit Spec_Hash_Definitions.pad_t) =
   Spec_Hash_PadFinish.pad Spec_Hash_Definitions.MD5
 let (finish : unit Spec_Hash_Definitions.finish_t) =
-  Spec_Hash_PadFinish.finish Spec_Hash_Definitions.MD5
+  Spec_Hash_PadFinish.finish Spec_Hash_Definitions.MD5

concrete/hacl-star-snapshot/ml/Spec_SHA1.ml

@@ -1,3 +1,7 @@
+module FStar_Seq_Properties = struct
+  include FStar_Seq_Base
+  include FStar_Seq_Properties
+end
 open Prims
 let (init_as_list : FStar_UInt32.t Prims.list) =
   [FStar_UInt32.uint_to_t (Prims.parse_int "0x67452301");
@@ -353,4 +357,4 @@ let (update : unit Spec_Hash_Definitions.update_t) = update_aux
 let (pad : unit Spec_Hash_Definitions.pad_t) =
   Spec_Hash_PadFinish.pad Spec_Hash_Definitions.SHA1
 let (finish : unit Spec_Hash_Definitions.finish_t) =
-  Spec_Hash_PadFinish.finish Spec_Hash_Definitions.SHA1
+  Spec_Hash_PadFinish.finish Spec_Hash_Definitions.SHA1

concrete/hacl-star-snapshot/ml/Spec_SHA2.ml

@@ -1,3 +1,8 @@
+module FStar_Seq_Properties = struct
+  include FStar_Seq_Base
+  include FStar_Seq_Properties
+end
+
 open Prims
 let (size_k_w : Spec_Hash_Definitions.sha2_alg -> Prims.nat) =
   fun uu___ ->
@@ -4871,4 +4876,4 @@ let (pad :
   Spec_Hash_PadFinish.pad
 let (finish :
   Spec_Hash_Definitions.sha2_alg -> unit Spec_Hash_Definitions.finish_t) =
-  Spec_Hash_PadFinish.finish
+  Spec_Hash_PadFinish.finish

concrete/hacl-star-snapshot/ml/Spec_SHA2_Constants.ml

@@ -1,3 +1,7 @@
+module FStar_Seq_Properties = struct
+  include FStar_Seq_Base
+  include FStar_Seq_Properties
+end
 open Prims
 let (k224_256_l : (FStar_UInt32.t, unit) FStar_List_Tot_Properties.llist) =
   [FStar_UInt32.uint_to_t (Prims.parse_int "0x428a2f98");
@@ -368,4 +372,4 @@ let (h512 : FStar_UInt64.t FStar_Seq_Base.seq) =
     FStar_UInt64.uint_to_t (Prims.parse_int "0x510e527fade682d1");
     FStar_UInt64.uint_to_t (Prims.parse_int "0x9b05688c2b3e6c1f");
     FStar_UInt64.uint_to_t (Prims.parse_int "0x1f83d9abfb41bd6b");
-    FStar_UInt64.uint_to_t (Prims.parse_int "0x5be0cd19137e2179")]
+    FStar_UInt64.uint_to_t (Prims.parse_int "0x5be0cd19137e2179")]

concrete/hacl-star-snapshot/ml/Spec_SHA2_Lemmas.ml

@@ -1,3 +1,7 @@
+module FStar_Seq_Properties = struct
+  include FStar_Seq_Base
+  include FStar_Seq_Properties
+end
 open Prims
 let rec (ws_aux :
   Spec_Hash_Definitions.sha2_alg ->

concrete/hacl-star-snapshot/ml/Vale_AES_GCTR_s.ml

@@ -1,3 +1,7 @@
+module FStar_Seq_Properties = struct
+  include FStar_Seq_Base
+  include FStar_Seq_Properties
+end
 open Prims
 type 'p is_gctr_plain_LE = unit
 type gctr_plain_LE = Vale_Def_Words_s.nat8 FStar_Seq_Base.seq

concrete/hacl-star-snapshot/ml/Vale_AES_OptPublic.ml

@@ -1,3 +1,7 @@
+module FStar_Seq_Properties = struct
+  include FStar_Seq_Base
+  include FStar_Seq_Properties
+end
 open Prims
 let (shift_gf128_key_1 : Vale_Math_Poly2_s.poly -> Vale_Math_Poly2_s.poly) =
   fun h ->

concrete/hacl-star-snapshot/ml/Vale_Def_Words_Seq_s.ml

@@ -1,3 +1,7 @@
+module FStar_Seq_Properties = struct
+  include FStar_Seq_Base
+  include FStar_Seq_Properties
+end
 open Prims
 type ('n, 'a) seqn = 'a FStar_Seq_Base.seq
 type 'a seq2 = (unit, 'a) seqn
@@ -219,4 +223,4 @@ let (seq_nat8_to_seq_uint8 :
 let (seq_uint8_to_seq_nat8 :
   FStar_UInt8.t FStar_Seq_Base.seq ->
     Vale_Def_Words_s.nat8 FStar_Seq_Base.seq)
-  = fun x -> Vale_Lib_Seqs_s.seq_map FStar_UInt8.v x
+  = fun x -> Vale_Lib_Seqs_s.seq_map FStar_UInt8.v x

concrete/hacl-star-snapshot/ml/Vale_Lib_Seqs.ml

@@ -1,3 +1,7 @@
+module FStar_Seq_Properties = struct
+  include FStar_Seq_Base
+  include FStar_Seq_Properties
+end
 open Prims
 
 

concrete/hacl-star-snapshot/ml/Vale_SHA_SHA_helpers.ml

@@ -1,3 +1,8 @@
+module FStar_Seq_Properties = struct
+  include FStar_Seq_Base
+  include FStar_Seq_Properties
+end
+
 open Prims
 let op_String_Access :
   'uuuuu . unit -> 'uuuuu FStar_Seq_Base.seq -> Prims.nat -> 'uuuuu =

iso-dh/ISODH.Sessions.fst

@@ -16,9 +16,11 @@ let parse_session_st (serialized_session:bytes) : result session_st =
   | Some s -> Success s
   | None -> Error "could not parse session"
 
+#push-options "--z3rlimit 25"
 let serialize_valid_session_st i p si vi st =
   serialize_wf_lemma session_st (ComparseGlue.is_msg isodh_global_usage (readers [V p si vi]) i) st;
   (serialize session_st st <: bytes)
+#pop-options
 
 let parse_valid_serialize_session_st_lemma i p si vi ss =
   parse_serialize_inv_lemma #bytes session_st ss

iso-kem/ISOKem.Sessions.fst

@@ -66,7 +66,7 @@ let serialize_valid_session_st i p si vi st =
 #push-options "--z3rlimit 100"
 let parse_valid_serialize_session_st_lemma i p si vi ss =
    match ss with
-   |InitiatorSentMsg1 b x -> ()
+   |InitiatorSentMsg1 b x -> A.can_flow_transitive i (A.get_label isokem_key_usages x) (readers [P p]) (readers [V p si vi])
    |ResponderSentMsg2 a gx gy k -> assert (includes_ids [P p] [V p si vi]);
      A.can_flow_transitive i (A.get_label isokem_key_usages k) (readers [P p]) (readers [V p si vi])
    |InitiatorSentMsg3 b gx gy k -> ()

nsl_pk/NSL.Protocol.fst

@@ -102,7 +102,7 @@ let n_b_pred i a b n_a n_b :prop =
 	  (did_event_occur_before i b (respond a b n_a n_b)) /\
 	    was_rand_generated_before i n_b (readers [P a;P b]) (nonce_usage "NSL.nonce"))
 
-#push-options "--z3rlimit 25"
+#push-options "--z3rlimit 50"
 let initiator_receive_msg_2_helper (i:nat) (a:principal) (b:principal) (c_msg2:msg i public)
 				   (ska:priv_key i a) (n_a:ns_nonce i a b) :
     LCrypto (msg i (readers [P a])) (pki nsl) (requires (fun _ -> True)) (ensures (fun t0 (n_b) t1 -> n_b_pred i a b n_a n_b))

start_dev_env.sh

@@ -21,7 +21,8 @@ fi
 # Initialize variables for docker call
 #docker_image="foa3ucuvi85/fstar-ocaml-emacs:3.5-b8b1265a"
 # docker_image="foa3ucuvi85/fstar-ocaml-emacs:3.7-master-71facac0"
-docker_image="foa3ucuvi85/fstar-ocaml-emacs:3.7-master-46b9698a"
+#docker_image="foa3ucuvi85/fstar-ocaml-emacs:3.7-master-46b9698a"
+docker_image="foa3ucuvi85/fstar-ocaml-emacs:latest"
 dy_home_host="${DIR}"
 dy_home_container="/home/build/dolev-yao-star"