Merge pull request #8 from mtzguido/guido_2894

Tweaking rlimits for new F*

src/Model.QUIC.fst

@@ -208,7 +208,7 @@ without increasing the rlimit, but increasing it in the fsti wouldn't
 take effect here (see FStar issue #2854 and the others linked from
 there. So, increase rlimit here and pop it after `let coerce`, so we are
 sure to catch it. *)
-#push-options "--z3rlimit 20"
+#push-options "--z3rlimit 40"
 
 let create k u u1 u2 init =
   let open Model.Helpers in
@@ -246,7 +246,7 @@ let coerce k u u1 u2 init ts =
   PNE.frame_invariant pne M.loc_none h2 h3;
   Writer u init (reveal siv) ae u2 pne ctr
 
-#pop-options (* /HACK *)
+#push-options "--z3rlimit 400 --query_stats"
 
 let createReader rgn #k w =
   let h0 = get () in
@@ -256,11 +256,15 @@ let createReader rgn #k w =
   let aer = AEAD.gen_reader w.ae in
   Reader aer last
 
+(* Another HACK: set_pn gets interleaved here *)
+
+#pop-options
+#pop-options
+
+#push-options "--z3rlimit 256 --fuel 0"
 private let lemma_eq_add (a b c:nat) : Lemma (requires a == b - c)
   (ensures a + c == b) = ()
 
-#push-options "--z3rlimit 128 --fuel 0"
-
 let set_pne (h:Spec.header) (#ln:pnl) (pne:PNE.pne_cipher ln) (c1:Spec.bytes)
   : Pure Spec.packet
   (requires not (Spec.is_retry h) /\ ln == Lib.RawIntTypes.uint_to_nat (TSpec.pn_length h) /\
@@ -333,8 +337,9 @@ let encrypt #k w h #l p =
     let k1, k2 = writer_leak w in
     let plain = (writer_ae_info w).AEAD.plain_pkg.AEAD.repr (dfst k) l p in
     TSpec.encrypt alg (hide k1) (hide w.siv) (hide k2) h (reveal #l plain)
-#pop-options
 
 /// Decrypt follows in a similar fashion. A complete proof will be provided for the final version.
 
 let decrypt #_ #_ _ _ _ = admit ()
+
+#pop-options

src/Model.QUIC.fsti

@@ -199,6 +199,8 @@ val create: k:id -> u:info ->
     ))
   )
 
+#push-options "--z3rlimit 15"
+
 val coerce: k:unsafe_id -> u:info ->
   u1:AEAD.info (dfst k) -> u2:PNE.info (dsnd k) ->  
   init: pn -> ts:AEAD.traffic_secret u1.AEAD.halg ->
@@ -225,6 +227,7 @@ val coerce: k:unsafe_id -> u:info ->
     Model.Helpers.hide k2 == QUIC.Spec.derive_secret u2.PNE.halg ts
         QUIC.Spec.label_hp (PNE.key_len u2)
   )
+#pop-options
 
 val createReader: parent:rgn -> #k:id -> w:stream_writer k ->
   ST (stream_reader w)
@@ -271,11 +274,13 @@ let set_pn_long (l:Spec.long_header_specifics{not (Spec.MRetry? l)}) (pn:PN.pack
   | MZeroRTT r p pnl _ -> MZeroRTT r p pnl pn
   | MHandshake r p pnl _ -> MHandshake r p pnl pn
 
+#push-options "--z3rlimit 200"
 let set_pn (h:Spec.header{not (Spec.is_retry h)}) (pn:nat{pn <= max_ctr}) =
   let pn : PN.packet_number_t = Secret.hide (U62.uint_to_t pn) in
   match h with 
   | Spec.MLong b d s l -> Spec.MLong b d s (set_pn_long l pn)
   | Spec.MShort r s k d pnl _ -> Spec.MShort r s k d pnl pn
+#pop-options
 
 val encrypt
   (#k:id)

src/QUIC.Impl.Crypto.fsti

@@ -43,7 +43,7 @@ val label_hp : (label_hp : IB.ibuffer U8.t {
 /// Actual code
 /// -----------
 
-#push-options "--max_ifuel 1 --initial_ifuel 1"
+#push-options "--max_ifuel 1 --initial_ifuel 1 --z3rlimit 10"
 /// One ifuel for inverting on the hash algorithm for computing bounds (the
 /// various calls to assert_norm should help ensure this proof goes through
 /// reliably). Note that I'm breaking from the usual convention where lengths
@@ -67,4 +67,3 @@ val derive_secret: a: ha ->
       B.as_seq h1 dst == derive_secret a (B.as_seq h0 secret)
         (IB.as_seq h0 label) (U8.v dst_len))
 #pop-options
-

src/QUIC.Impl.Header.Public.fst

@@ -382,13 +382,13 @@ let read_header_body
   | (| Long, (| (), (| ZeroRTT, (protected_bits, ()) |) |) |) ->
     read_header_body_long_zero_rtt sl cid_len protected_bits len
 
-#push-options "--z3rlimit 512 --z3cliopt smt.arith.nl=false"
+#push-options "--z3rlimit 1024 --z3cliopt smt.arith.nl=false --fuel 4 --ifuel 4 --query_stats"
 
 let read_header packet packet_len cid_len =
   let h0 = HST.get () in
   let sl = LP.make_slice packet packet_len in
   LP.valid_facts (parse_header cid_len) h0 sl 0ul;
-  assert (B.as_seq h0 packet `Seq.equal` LP.bytes_of_slice_from h0 sl 0ul);
+  assert_spinoff (B.as_seq h0 packet `Seq.equal` LP.bytes_of_slice_from h0 sl 0ul);
   assert_norm (
     let k = parse_header_kind cid_len in
     Some? k.LP.parser_kind_high /\
@@ -859,7 +859,7 @@ val write_header_aux
     Seq.slice (B.as_seq h1 out) 0 (U32.v len) == s 
   ))
 
-#push-options "--z3rlimit 32"
+#push-options "--z3rlimit 64"
 
 #restart-solver
 

src/QUIC.Spec.fst

@@ -90,6 +90,8 @@ let decrypt
       | None -> Failure
       | Some plain -> Success h (Seq.seq_reveal plain) rem
 
+#push-options "--z3rlimit 20"
+
 let lemma_encrypt_correct
   a k siv hpk h cid_len last plain
 =
@@ -114,3 +116,4 @@ let lemma_encrypt_correct
     AEAD.correctness #a k iv aad (Seq.seq_hide plain)
   end
 
+#pop-options

src/QUIC.TotSpec.fst

@@ -183,12 +183,14 @@ let serialize32_reduced_pn
     PN.parse_packet_number_kind
     (LP.serialize32_bounded_integer (Declassify.uint_to_nat pn_len))
 
+#push-options "--z3rlimit 16"
 let synth_packet_number_recip'
   (last: PN.last_packet_number_t)
   (pn_len: PN.packet_number_length_t)
   (pn: PN.packet_number_t' last pn_len)
 : Tot (npn: LP.bounded_integer (Secret.v pn_len)  { npn == PN.synth_packet_number_recip last pn_len pn })
 = U32.uint_to_t (PN.reduce_pn' (Declassify.uint_to_nat pn_len - 1) (Declassify.uint_to_nat pn))
+#pop-options
 
 let serialize32_packet_number
   (last: PN.last_packet_number_t)
@@ -493,6 +495,7 @@ let pn_offset
   let (| ph, _ |) = synth_header_recip cid_len last h in
   Seq.length (LP.serialize_tot_seq_of_serializer32 (serialize32_public_header cid_len) ph)
 
+#push-options "--z3rlimit 32"
 let header_encrypt
   (a:ea)
   (hpk: Cipher.key (AEAD.cipher_alg_of_supported_alg a))
@@ -517,6 +520,7 @@ let header_encrypt
     let r = Lemmas.xor_inplace r pnmask pn_offset in
     let r = Seq.cons (U8.uint_to_t f') (Seq.slice r 1 (Seq.length r)) in
     r
+#pop-options
 
 [@"opaque_to_smt"]
 let putative_pn_offset

src/QUIC.fsti

@@ -72,6 +72,8 @@ let incrementable (#i: index) (s: state i) (h: HS.mem { invariant h s }) =
 let receivable (#i: index) (s: state i) (h: HS.mem { invariant h s }) =
   Secret.v (g_last_packet_number s h) + 1 < pow2 62
 
+#push-options "--z3rlimit 15"
+
 val encrypt: #i:(*G.erased *)index -> (
   //let i = G.reveal i in
   s: state i ->
@@ -122,6 +124,8 @@ val encrypt: #i:(*G.erased *)index -> (
       | _ ->
           False))
 
+#pop-options
+
 unfold
 let decrypt_post (i: index)
   (s:state i)