Counting-free key agreement proof - #276
Draft
gebner wants to merge 20 commits into
Draft
Conversation
… (C3 stages 1+2a) Groundwork for making tls_sys_step a pure canonical product by eliminating the strict-progress *_advances guards: maintain the protected-handshake witnesses incrementally instead of reconstructing them from a hardcoded 16-event spine. Stage 1 (System.fst): thread a proof-only ghost `sender_snapshot:connection_model` through the in-flight channel (TlsInFlight recipient raw sender_snapshot), set at each send to the pre-send sender model. Needed because a seal projects under the sender's record_write at the PRE-increment seq. Additive; flagship byte-identical. Stage 2a (new TLS13.System.SeqCount.fst): the handshake-region seq-counting invariant `seq_count_ok`, founding H_seq (sender.record_write.seq == receiver.record_read.seq) on the existing byte_pairing rather than on the event-log length or the advances guards. Key facts: - pwrite_ok/pread_ok: in the pre-application-data region, a Handshake-epoch record seq equals the ApplicationData-record count of that endpoint's wire log (Initial-epoch => count 0). Gated on pre_appdata_control because a mid-handshake alert routes through fail_model, which freezes the record layer while still emitting a protected wire record (machine-checked counterexample to the ungated form). - lemma_seq_count_ok_preserved: seq_count_ok is inductive over tls_sys_step. - lemma_hseq_from_counts: H_seq is a corollary of byte_pairing + the counting invariants, confirming the *_advances guards are not needed to establish it. Not yet wired into tls_system_inv (a later stage). Full make verify green, 0 admits. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…ctors (C3 stage 2b)
Provides H_mat (handshake-epoch peer_record_material_agrees) for the incremental
protected-witness capture. Unlike the application epoch — where
supported_profile_application_record_material_agrees is DEFINED as the two app-epoch
peer_record_material_agrees, making its extractor trivial — there is no handshake
counterpart predicate, so the handshake agreement is constructed from key-schedule
agreement + install status.
New (all additive, no tls_system_inv change):
- lemma_client_server_handshake_record_material_{server_to_client,client_to_server}_agrees
(Pairing): from key_schedule_traffic_record_material_agrees (handshake dir) +
connection_state_consistent on both endpoints + non-failed control + the record
slots at the Handshake epoch, produce peer_record_material_agrees (handshake dir).
- lemma_connection_state_consistent_record_keys_consistent_for_config_role and
lemma_handshake_record_direction_material_matches_key_schedule_for_role
(ConnectionState.Lemmas): the install-status half, discharged outright from
connection_state_consistent (the R.Handshake case of record_keys_match_key_schedule
is definitionally the install-status agreement).
The install-status half (the genuinely new work) is fully proved. The cross-endpoint
key-schedule agreement is taken as a direct hypothesis, cleanly separating it from
install status; supplying it at the send site is stage-2c work (all_derived only
agrees on EXPECTED material; no handshake matches_expected invariant exists yet).
Full make verify green, 0 admits, flagship byte-identical.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
… (C3 stage 2c-i)
Closes the handshake-epoch record-material chain so H_mat is derivable from facts
present in tls_system_inv, feeding the stage-2b extractors. Additive (no
tls_system_inv change).
New:
- lemma_handshake_peer_record_material_{server_to_client,client_to_server}_agrees_from_hello
(Pairing): from supported_profile_all_derived_key_material_agrees +
connection_state_consistent on both endpoints + config roles + non-failed control +
the record slots at the Handshake epoch, produce peer_record_material_agrees
(handshake dir). Assembles the 2b install-status extractor with the KS-agreement
supplied below.
- lemma_connection_state_consistent_handshake_traffic_material_matches_expected
(ConnectionState.Lemmas): the genuinely-new piece — the installed handshake
traffic slot equals the schedule-expected material, as a reachable-shape RTC
invariant over connection_state_consistent. Simpler than the application-epoch
analogue because handshake traffic keys are never key-updated: the slot starts
None (vacuous), an install sets it to the TH_SH-expected value, and no later step
changes it. The LocalDeriveSharedSecret and network cases are discharged by
deterministic frame lemmas (step never writes handshake traffic slots; TH_SH
depends only on the stored hellos) rather than left to SMT, keeping the proof
non-flaky at rlimit 10.
- lemma_key_schedule_traffic_record_material_agrees_from_expected_material: thin
re-export of the generic (traffic_id-polymorphic) from_expected bridge.
Full make verify green, 0 admits, flagship + System.fst byte-identical.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Fold the per-endpoint handshake-region seq-counting invariant into tls_system_inv so H_seq (sender.record_write.seq == receiver.record_read.seq) becomes available from the invariant at protected sends/deliveries. Wiring seq_count_ok directly created a module cycle: TLS13.System.SeqCount imported TLS13.System, so tls_system_inv could not reference it. Resolve by splitting the module: - New TLS13.System.SeqCountBase (Sys-free): pwrite_ok/pread_ok, all per- connection_state probe/algebra/coupling lemmas, lemma_hseq_from_counts, and the new seq_count_ok_pair predicate. Imports only ConnectionState-level modules. - Into TLS13.System: the 6 per-transition lemma_scop_* helpers, the system-level lemma_seq_count_ok_preserved and lemma_seq_count_ok_initial. tls_system_inv gains the conjunct SCB.seq_count_ok_pair s.client s.server, re-established in lemma_initial_inv and all 6 lemma_pres_*. - Delete TLS13.System.SeqCount. Pure relocation + threading: no proof weakening, no new axioms. clean16/length machinery and the *_advances guards are untouched. Temporal.fst byte-identical. Full make -j100 verify green; make check-admits = 0. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The 2c-i lemma_handshake_peer_record_material_*_agrees_from_hello require
supported_profile_all_derived_key_material_agrees, which bundles APPLICATION
traffic agreement and is definitionally false mid-handshake (the recipient has
only processed through ServerHello). But their proofs only use the handshake
TrafficKey/TrafficIV components. Add handshake-only variants usable at the
protected server-flight sends/deliveries:
- Pairing: lemma_handshake_peer_record_material_{server_to_client,
client_to_server}_agrees_from_hello_hsonly -- weakened requires taking the two
handshake peer_derived_key_material_agrees facts directly (bodies verbatim from
the existing from_hello lemmas).
- ConnectionState.Lemmas: lemma_handshake_peer_derived_key_material_agrees_from_
paired_hellos assembles those two facts from paired_x25519_key_shares +
same_key_derivation_checkpoint DeriveHandshakeTraffic.
- ConnectionState.Lemmas: lemma_connection_state_consistent_handshake_key_
schedule_lineage -- key-schedule lineage mid-handshake (once ks_handshake_secret
is Some), discharged from the existing reachable-shape invariant (no new
induction; derive_shared_secret_model sets shared/early/handshake/master at once).
Additions only; no existing statement modified, no axioms. System.fst/Temporal.fst
untouched. Full make -j100 verify green; make check-admits = 0.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Add the FACT-4 protected-channel witness `protected_channel_ready` as a
conjunct of `tls_system_inv`, established at the two protected handshake
sends and consumed at delivery. This is the incremental-witness backbone
that lets a later stage drop the clean16/length machinery and the
`*_advances` progress guards, turning `tls_sys_step` into a pure canonical
product.
Channel refactor (fixes an encrypted-alert non-inductiveness): the
`TlsInFlight` constructor now carries the concrete sent message
(`sent:M.tls_message`), bound at each send. `protected_channel_ready`
guards its in-flight case on `TlsHandshake? sent` plus handshake-epoch
conditions, so encrypted alerts and post-handshake-epoch messages are
vacuously true rather than demanding a handshake seal. Temporal.fst is
byte-identical (it uses only the `TlsInFlight?` discriminator).
The witness carries: the sender's protected-message seal, send/receive
seq alignment, handshake `peer_record_material_agrees` (via the 2c-ii-B
hsonly extractor + a mid-handshake `paired_x25519_key_shares`), and the
serialize/parse round-trip of the sent message. A validation lemma
derives the decode-glue preconditions from it.
Faithful model bounds (needed for round-trip inductiveness of the
server's protected handshake messages; each mirrors an impl-enforced cap):
* `legal_local_event` / `legal_handshake_message` CertificateVerify arms:
`certificateVerify_representable cv` (impl 4096-byte signature buffer).
* `legal_handshake_message` Certificate arm: `certificate_representable
cert` (impl 32768-byte chain buffer) and `certificate_bytesize cert
<= 16777215` (the RFC 8446 uint24 handshake-length wire limit).
Two additive `Lemmas.fsti` vals expose mid-handshake stable x25519
key-share projections (from consistency + derived shared secret),
delegating to the existing private reachable-shape invariants.
Impl cascade (all discharged from the existing `is_valid_certificate_verify`
/ chain-bound facts, no new admits): Server.Auth, ConnectionState.Queries,
Server, Server.Send (+one helper val). One z3refresh stabilization in
Client.CanonicalProtocol for an unrelated LocalFail bridge perturbed by
the enlarged legal-event definition.
Gate: `make -j100 verify` = all modules verified; `make check-admits` = 0.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…ehind one tracked gap Faithful root-cause fix for a genuine TLS model defect: an endpoint could send an application-keys-encrypted record in a window where the peer's read keys were still at Handshake epoch (undecryptable). The client/server now install their application READ keys ATOMICALLY when they deliver the peer's Finished, closing both mirrored windows. Spec model (TLS13.Spec.ConnectionState.step_handshake_message): - Client server-Finished delivery (@HsCertificateVerifyVerified): append server Finished to transcript, verified, derive+install server-app read keys, populate ks_server_application_traffic, land at HsServerFinishedVerified. Guarded by Some? ks_master_secret. - Server client-Finished delivery (@HsServerFinishedSent): derive client-app secret from the current transcript (through server Finished) BEFORE appending, install client-app read keys, populate ks_client_application_traffic, append client Finished, land at ControlApplicationData. Guarded by Some? ks_master_secret. - legal_handshake_message: +Some? ks_master_secret on both Finished-received arms. HsClientFinishedReceived / HsServerFinishedReceived are now off the honest path. Impl refinement (genuinely green, no gaps): the Pulse delivery ops in Impl.ConnectionState.Network now actually perform the atomic install at delivery, refining the new atomic ghost constructors (Model.fst/.fsti); can_receive_* discharge the new Some? ks_master_secret gate via the impl master-secret flag (Queries). Counting stack removed (per direction: eliminate the length/clean16 counting argument): Model Fix 1 legitimately shrinks the honest appdata trace 16->14, so the clean16 byte-derivation foundation is retired rather than recalibrated. 31 clean16 modules moved to attic/clean16/ (git-tracked, out of build); PairingNoTailInversion / ServerHelloWindowRank .fsti stripped to definitions-only (progress defs pinned by tls_sys_step guards are retained). tls_system_inv drops the three counting conjuncts client_len_ok / server_len_ok / client_appdata_len_ok. Honest System.fst refinements: lemma_server_into_appdata_is_verify becomes a disjunction (local-verify OR atomic delivery), lemma_server_recv_not_into_appdata removed (now false), establishment relocated into lemma_pw_pres_deliver_to_server. ONE tracked temporary gap: lemma_pw_establish (System.fst) = admit(), stating the true both-ready establishment obligation minus only the length==16 preconditions. To be discharged by the counting-free C3 incremental-protected-witnesses proof (Phase 2). Validation: make -j100 verify = "All F* modules verified"; make check-admits = 1 (lemma_pw_establish); Temporal.fst byte-identical (flagship statement unchanged). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
… admits) Safety checkpoint after a data-loss incident (a delegated subagent ran `git checkout` on System.fst, wiping ~1047 lines of uncommitted Phase-2 work, since reconstructed from the session event log and re-validated). State: - `make -j100 verify` = "All F* modules verified". - ConnectionState.fst (trusted model) and Temporal.fst byte-identical to HEAD; tls_sys_step / *_advances untouched. Only System.fst changed. - check-admits = 3: lemma_pw_establish (the tracked Phase-1 gap) plus the two Path-B deliver stubs lemma_ipw_pres_deliver_to_client/server (not yet proven). - The 4-conjunct invariant (inflight_wire_faithful, inflight_sender_coupling, inflight_protected_sender_ok, incremental_protected_witnesses) is wired into tls_system_inv and proven inductive across all 6 preservation lemmas + initial. NOT a milestone — WIP. Next: discharge the two deliver lemmas from AEAD correctness + delivery legality + reachability (Path B), reaching check-admits=1, then assemble the witnesses and remove the last admit (Phase 2 complete). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…ductive & green Phase A of Path B deliver-lemma work: add the faithfulness-only, MESSAGE-facing conjunct inflight_sender_live to tls_system_inv: TlsInFlight _ _ _ sent -> M.TlsAlert? sent ==> sent == M.TlsAlert T.Close_notify i.e. no BARE FATAL alert is ever put in flight (both drivers' local_event_kind_matches emit only Close_notify for alerts). Established at the 2 sends (server via a focused kind-inversion helper lemma_server_send_kind_not_fatal_alert; client incidentally), frozen while in-flight, vacuous at locals/deliveries/initial (post channel TlsQuiet). Model (ConnectionState.fst) + Temporal.fst BYTE-IDENTICAL. Full build green (All F* modules verified). check-admits == 3 (lemma_pw_establish + the two ipw deliver lemmas still admitted; conjunct threaded through their ensures). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…lose_notify wire roundtrip
Step 1 of the guard-relaxation route for the two deliver lemmas.
- Drop 'M.TlsHandshake? sent' from protected_channel_ready's guard antecedent
(System.fst) so the guard fires for every pre_appdata protected send:
handshakes AND Close_notify-from-handshaking. Antecedent weakened => the
implication strengthens => all consumers still get the conclusion; only the
two establishment lemmas must now discharge the Close_notify case.
- Add kind-characterization helpers lemma_{server,client}_send_kind_char
inverting the driver local_event_kind enums: any driver Sent event is never
ChangeCipherSpec/IgnoredPostHandshake and any alert it emits is Close_notify.
- Restructure lemma_pcr_establish_{server,client}_send to case on 'sent':
handshake (existing per-message roundtrip), TlsAlert (Close_notify roundtrip),
and assert-False for AppData/KeyUpdate (pre_appdata) / CCS / IgnoredPostHandshake.
- Add pure Close_notify wire roundtrip lemma_parse_serialize_tls_message_close_notify
to TLS13.Wire.Spec (parse_tls_message is abstract there; needed by both the
establishment's alert branch and the decode glue). Honest wire fact, not the
trusted model.
Model (ConnectionState.fst) + Common.Temporal.fst + System.Temporal.fst
byte-identical. Full 'make -j100 verify' green. check-admits == 3
(lemma_pw_establish + the two still-admitted deliver lemmas).
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…t>=marker)
Add two reachable count-bound clusters in TLS13.System.WireStep.fst for the
Route B cross-endpoint ordering lemma:
- client recv region <=3: client_recv_region_ctrl + step/trace/reachable chain
-> lemma_client_reachable_recv_region_le3
- server sent >= marker: server_sent_marker_count LOWER step/trace/reachable
chain -> lemma_server_reachable_sent_ge_marker
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Phase B / Step 2 (Option 2, de-risk round): state the cross-endpoint P2 ordering fact for the deliver-to-client direction as a STANDALONE, fully verified lemma in a new module TLS13.System.Ordering, taking the sender-facing snapshot reachability + byte-pairing as EXPLICIT hypotheses (no tls_system_inv surgery yet), so the pure-reachability count argument can be validated before being wired into the deliver lemmas. - server_flight_marker_shape: self-contained, single-step-inductive write-once shape; consistent server + write.epoch==Application ==> all 4 protected-flight fields set ==> server_sent_marker_count == 4 (ported from validated scratch). - lemma_inflight_sender_write_epoch_not_application_client: recipient client in its handshake recv region + reachable/consistent server snapshot + byte-pairing ==> snap.write.epoch =!= Application, via server-sent>=4 vs client-recv<=3 (append right-cancellation + the committed WireStep count bounds). No admit/assume/authenticity/injectivity. ConnectionState + both Temporal files byte-identical. check-admits unchanged (3). Scratch marker module removed. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…2 WireStep bounds Phase B / Step 2, server-direction mirror (threshold 1-vs-0), STANDALONE: WireStep.fst (additive, +2 count-bound clusters): - client_finished_sent_flag + lemma_client_finished_reachable_sent_ge1: FIELD-keyed client SENT >= 1 (reachable client with Some? hs_client_finished has sent >= 1 protected record). Unlike the control-keyed client_sent_potential, this survives ControlFailed. - server_recv_region_ctrl + lemma_server_reachable_recv_region_le0: reachable server in its handshake receive region (up to HsServerFinishedSent) has received 0 ApplicationData records (client Finished is the first protected receive and leaves the region atomically, Model-Fix-1). Ordering.fst (additive): - client_finished_marker_shape (+ RTC lift): consistent client with write.epoch==Application ==> Some? hs_client_finished. Scaffolded with two inductive conjuncts (ControlNew/Handshaking ==> write.epoch != Application; ControlApplicationData/Closing/Closed ==> Some? hs_client_finished), mirroring server_flight_marker_shape. - lemma_inflight_sender_write_epoch_not_application_server: recipient server in recv region + reachable/consistent client snapshot + byte-pairing ==> snap.write.epoch =!= Application, via client-sent>=1 vs server-recv<=0. No admit/assume/authenticity/injectivity/receiver-coupling. ConnectionState + both Temporal byte-identical. check-admits unchanged (3). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…t to tls_system_inv Add a STRICTLY sender-facing `inflight_snap_reachable` conjunct to `tls_system_inv` and establish it in all 6 preservation lemmas + `lemma_initial_inv`, so the two standalone cross-endpoint ordering lemmas (TLS13.System.Ordering) can be wired into the deliver lemmas in step (c). The conjunct (opaque_to_smt) states, for an in-flight channel `TlsInFlight recipient raw snapshot _`: there exists a witness `pred` that is byte-reachable (role-matched: server_reachable when sender is server / recipient is client, client_reachable when sender is client / recipient is server) and consistent, with `pred.cs_model == snapshot` and `pred.raw_sent ++ raw == sender.raw_sent` (sender via ipso_sender_endpoint). It mentions ONLY the sender endpoint, snap, raw, and pred -- no recipient field; the recipient coupling stays confined to the derived ordering lemmas via the existing byte_pairing conjunct. Establishment: witness `pred := a.<sender>` at the 2 SENDS (byte-reachable + consistent from the pre-state invariant; the send appends raw via legal_connection_delta's raw_sent equation); vacuous at the 2 DELIVERS (post channel TlsQuiet) and the 2 LOCALS (channel frozen at TlsQuiet); vacuous at the initial state. Additive-only. ConnectionState + both Temporal byte-identical. check-admits stays 3 (deliver lemmas + lemma_pw_establish untouched). Full `make -j100 verify` = "All F* modules verified". Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Refine step_tls_message so that a Sent TlsAlert from a ControlFailed
connection returns None ("a failed connection sends nothing") instead of
the old catch-all fail_model. This collapses the Phase-2 deliver-lemma
residual: inflight_sender_coupling (System.fst) requires
step_model snapshot (Sent sent) == Some (recipient endpoint).cs_model
so a ControlFailed snapshot with an in-flight alert now yields
None == Some (...) == False, automatically excluding it from ever being
in-flight. The deliver lemmas therefore never face Close_notify+ControlFailed.
ConnectionState.fst (trusted model, intentionally not byte-identical):
add arm M.TlsAlert alert, ControlFailed _ ->
(match dir with Sent -> None | Received -> Some (fail_model ...))
before the alert catch-all.
ConnectionState.Lemmas.fst (downstream fallout, verifies green):
- new reduction helpers step_sent_alert_failed_none /
step_received_alert_failed_fail (pin the new arm's reduction).
- lemma_step_model_from_failed_results_failed: direction-split alert arm;
ensures strengthened with model_handshake/model_record preservation.
- lemma_server_failed_shape_transfer: transfers the server x25519 shape
disjunction across a passive ControlFailed step via handshake-field eq.
- both *_x25519_reachable_shape lemmas: prepend a Sent-ControlFailed
exclusion arm and peel the Received-ControlFailed alert arm.
Full make -j100 verify green; check-admits == 3 (unchanged: lemma_pw_establish
+ the two Path-B deliver stubs); Temporal.fst byte-identical.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Replace the two `admit ()` bodies of lemma_ipw_pres_deliver_to_client and
lemma_ipw_pres_deliver_to_server (TLS13.System.fst) with real proofs of
`incremental_protected_witnesses b` at a protected delivery. The stale
"FATAL alert blocked / forbidden-axiom" comment blocks are deleted: that
sub-case is now excluded by inflight_sender_live (alerts are only
Close_notify) combined with the committed model refinement (a Sent alert
from ControlFailed steps to None, contradicting inflight_sender_coupling's
Some), captured in lemma_snap_not_failed.
Proof structure (post channel is TlsQuiet, so the five inflight_* conjuncts
of b are vacuous; only incremental_protected_witnesses is real work):
- BUILD branch (protected-handshake `sent`): the recipient freshly stores
the field; its projection-pair witness is built from the relaxed
protected_channel_ready (seal + seq-align + material + roundtrip) via
the decode-glue (P.lemma_*_protected_message_decode_from_peer_record_
material) + decode determinism + the head-aligned assembler
(ProtectedWireHead.lemma_protected_handshake_event_projection_pair_
from_aligned_heads); the other four clauses transport unchanged.
- TRANSPORT branch (any other `sent`): a protected-handshake receive is
refuted (sent seals to raw, raw decodes deterministically to the
received handshake => sent == received handshake, contradicting the
branch guard); non-storing receives transport all five clauses. The
epoch guard snap.write.epoch == Handshake comes from the transport-
ordering lemmas (byte-pairing + inflight_snap_reachable's witness + the
Ordering.fst flight-marker counting lemmas); cleartext `sent` is refuted
by record framing (Sent cleartext is Handshake/CCS-framed, not
Application_data-framed as the protected decode requires).
Rests only on existing invariant conjuncts, the committed trusted-model
change, and AEAD correctness -- no authenticity/injectivity/counting axiom
and no new tls_system_inv conjunct. Additive helpers (all proven, all in
System.fst): lemma_serialize_handshake_record_length,
lemma_cleartext_sent_not_appdata_framed, lemma_step_sent_from_failed_none,
lemma_snap_not_failed, lemma_transport_ordering_{client,server},
spike_build_{ee,cert,cv,fin,client_fin}, is_protected_handshake,
is_finished_msg, {client,server}_transport_false, transport_{client,server}.
Module aliases Ord/WRRc/WRD added (System -> Ordering: no cycle).
Fresh `make -j100 verify` green (incl. TLS13.System.Temporal re-verified);
check-admits == 1 (lemma_pw_establish only); Temporal.fst byte-identical.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Remove the last admit (System.fst lemma_pw_establish). The FACT-4
establishment obligation
P.paired_protected_handshake_event_projection_pair_witnesses client server
== exists ee cert cv sf cf. PWB.paired_protected_handshake_event_
projection_pairs client server ee cert cv sf cf
is now a pure ASSEMBLY from the incremental_protected_witnesses invariant
conjunct: at a both-ready state all 10 protected handshake fields are
present, so each of the conjunct's 5 clauses sits in its (Some,Some) branch
and yields exactly the projection-pair the target needs (polarities match
clause-by-clause: EE/cert/cv/server-Finished sender=server->client,
client-Finished mirrored sender=client->server); the 5 existential replays
become the 5 witnesses.
Changes (all in System.fst, +99/-16):
- lemma_pw_establish: added requires client_stage_ok s.client /
server_stage_ok s.server / incremental_protected_witnesses s (all already
tls_system_inv conjuncts, so callers supply them for free). Body: pin both
controls to ControlApplicationData via client_ready/server_ready; extract
all 10 fields Some via two new stage-keyed helpers; reveal the opaque
conjunct; eliminate the 5 replays; introduce the target existential.
- New helpers lemma_{client,server}_appdata_all_fields_some.
- Threaded incremental_protected_witnesses b into the requires of the two
actual callers (lemma_pw_pres_deliver_to_server, lemma_pw_pres_server_local),
and reordered lemma_ipw_pres_* BEFORE lemma_pw_pres_* in
lemma_pres_deliver_to_server / lemma_pres_server_local so the fact is in
scope (the ipw lemmas' ensures include incremental_protected_witnesses b;
reorder safe -- they need only tls_system_inv a + the eliminated
channel/step decomposition).
Rests only on the incremental witnesses + both-ready field presence -- no
counting (clean16 length==16 boundary stays deleted), no authenticity/
injectivity axiom, no new invariant conjunct. Fresh from-scratch
`make -j100 verify` green incl. TLS13.System.Temporal re-verified;
check-admits == 0; Temporal.fst byte-identical.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…roduct) tls_sys_step's six transitions are now the literal canonical product (client_step/server_step + channel plumbing) with the *_advances / *_local_advances strict-progress guards deleted. No model change: the trusted model (TLS13.Spec.ConnectionState) and all three Temporal.fst files are byte-identical to before. The guards' only remaining consumer was the seq-count layer. A redundant idempotent handshake key re-install (legal local step that resets the record direction seq to 0) is proven harmless by REACHABILITY: every handshake install is legal only at one control per endpoint (client HsServerHelloReceived, server HsServerHelloSent), where only cleartext hellos have been exchanged, so raw_appdata_count == 0 on both directions and the reset preserves pwrite_ok / pread_ok (0 == count == 0). - WireStep: 3 new count==0-at-install-stage lemmas (client recv @ HsServerHelloReceived; server sent/recv @ HsServerHelloSent) alongside the existing client-sent one. - SeqCountBase: split seq_stable helpers into write/read variants with a gated "redundant HS install => pre-install seq 0" precondition, discharged in the 4 reachable p-lemmas from the count facts + pwrite_ok/pread_ok. - System.fst: guard-removal fallout repaired via two stage-exclusion lemmas derived from client_stage_ok/server_stage_ok (in tls_system_inv), replacing the guard's stage pinning. Fresh-from-clean `make verify` = "All F* modules verified"; check-admits = 0. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…e comments lemma_client_progress_congruence / lemma_server_progress_congruence became dead once the seq_stable helpers switched to the reachability (count==0) argument; removed. Refreshed two comments that still referenced the deleted *_local_advances guard. No logic change; make verify = "All F* modules verified", check-admits = 0. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Introduce `Common.SystemProduct`: a generic single-slot directed-channel two-party product construction (`prod_iface` + `product_step`). It exposes three channel observations (is_quiet / in_to_server / in_to_client) and seven move families (client/server send, deliver_to_client/server, client/server local, and a fused server_serve), ORed under the single-slot channel discipline (output needs quiet, deliver needs a message directed at the party, serve consumes a to-server message and emits a to-client response). Both systems are now instances of this one combinator: - `TLS13.System.tls_sys_step := product_step tls_iface`, where `tls_iface` reuses the six verbatim canonical transition shapes as its families and leaves `server_serve` empty (TLS has no fused serve). - `Calc.System.sys_step := product_step calc_iface`, where issue = client_send, the fused serve = server_serve, recv = deliver_to_client, and the other four families are empty. The combinator is fully transparent (plain lets + literal-record projection), so both `tls_sys_step` and `sys_step` unfold to the same VCs as before: all three Temporal modules stay byte-identical and every downstream preservation lemma still case-splits over the same disjuncts. Full verify green on both the root and calc_sample builds; check-admits == 0 on both. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.