Repository navigation
tls: make hello::bootstrap verify - #12
Merged
Merged
Conversation
Capture the pre-call mode and pending flight as ghost values (fail() overwrites them), compare the flight with the verified bytes_eq, and spell out the field-wise state equality in eof. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
bootstrap_lemmas gains spec helpers (terminal, hello_step, after_messages, fragment_step, alert_step, record_step) and lemma_feed_complete, which reduce bootstrap_spec::feed's Complete branch to record_step. The private handlers (fail, close, handle_*) now ensure exact state equalities against those helpers, so feed's proof is a short chain instead of one large body (clears the rlimit failure without raising it). Reassembler::snapshot (new, contract: copy of the view) lets the handlers restore the reassembly state when feed_record fails, as bootstrap_spec requires (the old code reset it to empty). framing::lemma_wf_mode bridges the closed Buffer::wf_mode to framing_spec::wf_mode. Alert records now check for exactly two bytes first and other record types fail with unexpected_message, mirroring bootstrap_spec::feed. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
atiernan
marked this pull request as ready for review
October 27, 2026 07:13
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
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.
Stacked on #8. The WIP
hello::bootstrapmodule, brought in byphase3/tls-handover, failed Verus with 4 errors: assertions inacknowledge_sendandeof, and an rlimit infeed. It now verifies. Its spec, its contract and therequires/ensuresof its public functions are unchanged. No escape hatches were added and rlimit was not raised.Proof changes
acknowledge_send: captures the old mode and pending flight as ghosts beforefail()overwrites them, and compares with the verifiedhandshake::bytes_eqandmatches!instead of==, which has no spec.eof: adds field-by-field state equalities.feed: the private handlers ensured onlywf(), so they could never provefeed_exec_ensures. They now ensure exact state against new spec helpers inbootstrap_lemmas.rs(record_step,fragment_step,alert_step,hello_step,after_messages,terminal, pluslemma_feed_completeandlemma_plain_fragment_bound). The Hello controller call moves intohandle_hello_message.framing.rsgainslemma_wf_mode, andreassemble.rsgainsReassembler::snapshot(contract:r@ == self@,r.wf() == self.wf()).Behaviour changes (code brought in line with the existing spec)
decode_error.unexpected_message.unexpected_message. Before, an empty message gavedecode_error.framer.is_emptycheck inhandle_messages, which the spec does not have, is removed.Local results (per module; I re-ran these myself after cleaning the Verus cache)
hello::bootstrap15 verified, 0 errors.hello::bootstrap_lemmas4 verified, 0 errors.connection::framing11 verified, 0 errors.reassemble7 verified, 0 errors.connection::exec31 verified, 0 errors.cargo test -p clazel-tls: 85 passed, 0 failed. Strict clippy,cargo fmt --checkandcargo xtask checkare clean.Not done
clazel-tlsstays at tier 0.🤖 Generated with Claude Code