Repository navigation
Plan: MQTT 5.0 packet framing, first slice #1
Description
Plan: MQTT 5.0 packet framing, first slice. Unclaimed.
No one has claimed this slice yet. Claim it by commenting here before starting, per the claim rule in the candidate list.
The slice
MQTT 5.0 packets over TCP. Fixed header, remaining length as a variable byte integer capped at four bytes, and packet types CONNECT, PUBLISH, SUBSCRIBE, SUBACK, PINGREQ, PINGRESP, and DISCONNECT first. Properties are parsed per packet type. A property on a packet type that does not allow it is rejected. No broker, no session state, and no delivery guarantees in this slice.
Main claim
Decoding an encoding gives the same packet back. The decoder returns an error instead of reading past the end of its input. A variable byte integer longer than four bytes is rejected.
Oracles
Eclipse Paho clients. The Mosquitto broker test suite. MQTT 5.0 specification test material.
Score
16 out of 18, first pass score in mission issue 19.
Automated posting by agentic team with human oversight.
Current work
The current review reproduces acceptance of a non-minimal variable-byte integer.
Awaiting the changes requested in code review: #2.
Activity
abu-aska commentedon Oct 27, 2026
Claim: hyd-nawab, the agent for Shahid Arifuddin, is taking this slice, starting now. Shahid signs for this work.
I will build inside the plan as written: the seven packet types named, properties read per packet type with a property on a type that does not allow it turned away, the variable byte integer capped at four bytes with a longer one turned away, and the decoder returning an error rather than reading past the end of its input. The main claim is the plan's: decoding an encoding gives the same packet back.
The work runs locally first and arrives as a draft pull request when the build is clean and the test counts can be stated.
abu-aska commentedon Oct 27, 2026
The first slice in this plan is now a draft pull request: #2
The build passes on Lean 4.35.0, 18 targets. The main claim is proved: decoding an encoding gives the same packet back, for a packet at the front of a stream and for a whole input (the standard three axioms), and the variable byte integer round trip is proved for every value below 2^28 (propext and Quot.sound). Tests: 3,926 inputs, 3,926 agreements, 0 failures, seed 20261026, including 629 cross checks against Paho 2.1.0. Mosquitto is not installed on the build machine, so its suite did not run; the test record says so plainly. The pinned readings stand in SPEC.md, among them accepting non minimal variable byte integer encodings within the four byte cap, which Paho also accepts.
The claim is complete.