From da56e1150e6356ddf7cb6a7ac2ba7fe07d6593bb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 7 May 2023 13:57:45 -0700 Subject: [PATCH] Tweaking rlimits for new F* --- src/Model.QUIC.fst | 15 ++++++++++----- src/Model.QUIC.fsti | 5 +++++ src/QUIC.Impl.Crypto.fsti | 3 +-- src/QUIC.Impl.Header.Public.fst | 6 +++--- src/QUIC.Spec.fst | 3 +++ src/QUIC.TotSpec.fst | 4 ++++ src/QUIC.fsti | 4 ++++ 7 files changed, 30 insertions(+), 10 deletions(-) diff --git a/src/Model.QUIC.fst b/src/Model.QUIC.fst index 7568e8e..c66d3c4 100644 --- a/src/Model.QUIC.fst +++ b/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 diff --git a/src/Model.QUIC.fsti b/src/Model.QUIC.fsti index e6167cf..df2e7c7 100644 --- a/src/Model.QUIC.fsti +++ b/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) diff --git a/src/QUIC.Impl.Crypto.fsti b/src/QUIC.Impl.Crypto.fsti index 55e5bf1..396d96d 100644 --- a/src/QUIC.Impl.Crypto.fsti +++ b/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 - diff --git a/src/QUIC.Impl.Header.Public.fst b/src/QUIC.Impl.Header.Public.fst index 26dd0d4..834571a 100644 --- a/src/QUIC.Impl.Header.Public.fst +++ b/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 diff --git a/src/QUIC.Spec.fst b/src/QUIC.Spec.fst index d347a59..035ac73 100644 --- a/src/QUIC.Spec.fst +++ b/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 diff --git a/src/QUIC.TotSpec.fst b/src/QUIC.TotSpec.fst index 69d6a67..8127d01 100644 --- a/src/QUIC.TotSpec.fst +++ b/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 diff --git a/src/QUIC.fsti b/src/QUIC.fsti index 036862b..51e45d0 100644 --- a/src/QUIC.fsti +++ b/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)