From 612695d653ebd5e0859ef669bb07ff25343d7658 Mon Sep 17 00:00:00 2001 From: shah Date: Mon, 26 Oct 2026 23:13:54 -0500 Subject: [PATCH 1/2] Add MQTT 5.0 packet framing for seven types, with proved round trip --- .gitignore | 3 + Main.lean | 90 +++ Mqtt.lean | 2 + Mqtt/Parse.lean | 370 +++++++++++++ Mqtt/Utf8.lean | 85 +++ Mqtt/Value.lean | 513 +++++++++++++++++ Mqtt/Verify.lean | 22 + Proofs.lean | 3 + Proofs/Examples.lean | 105 ++++ Proofs/RoundTrip.lean | 1221 +++++++++++++++++++++++++++++++++++++++++ Proofs/Utf8.lean | 148 +++++ README.md | 71 ++- SPEC.md | 330 +++++++++++ lake-manifest.json | 6 + lakefile.toml | 13 + lean-toolchain | 1 + tests/TEST-RESULTS.md | 20 + tests/run_tests.py | 1048 +++++++++++++++++++++++++++++++++++ 18 files changed, 4031 insertions(+), 20 deletions(-) create mode 100644 Main.lean create mode 100644 Mqtt.lean create mode 100644 Mqtt/Parse.lean create mode 100644 Mqtt/Utf8.lean create mode 100644 Mqtt/Value.lean create mode 100644 Mqtt/Verify.lean create mode 100644 Proofs.lean create mode 100644 Proofs/Examples.lean create mode 100644 Proofs/RoundTrip.lean create mode 100644 Proofs/Utf8.lean create mode 100644 SPEC.md create mode 100644 lake-manifest.json create mode 100644 lakefile.toml create mode 100644 lean-toolchain create mode 100644 tests/TEST-RESULTS.md create mode 100644 tests/run_tests.py diff --git a/.gitignore b/.gitignore index 01f8cdb..9a366ff 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,4 @@ .lake/ +venv/ +scratch/ +__pycache__/ diff --git a/Main.lean b/Main.lean new file mode 100644 index 0000000..2cce051 --- /dev/null +++ b/Main.lean @@ -0,0 +1,90 @@ +/- + Command line front end for the MQTT packet codec. + + One request per line, in the shape `op numbers`, where the op + and the numbers are parted by one space, and the numbers are + decimal numbers parted by commas, with no spaces inside the + number list. A line holds a number in plain decimal: no sign, + no leading zeros (the number 0 itself is written `0`), and at + most twenty digits. An empty line is passed over with no + answer. A request that breaks the line shape prints `error`. + + The one operation: + + - `parse` takes comma parted byte numbers and prints `ok:` and + the bytes of the packet printed back when the bytes are + exactly one packet this slice reads, and `none` when they + are not. The reprint is the packet read and written again, + byte for byte when the packet arrived in its printed form. + The full rules are in SPEC.md. +-/ + +import Mqtt + +open Mqtt + +/-- Read one number token: plain decimal digits, no sign, no + leading zeros but for the number 0 itself, at most twenty + digits. -/ +def parseNat (s : String) : Option Nat := + let cs := s.toList + if cs.isEmpty ∨ 20 < cs.length then none + else if 1 < cs.length ∧ cs.head! = '0' then none + else if cs.all Char.isDigit then + some (cs.foldl (fun n c => n * 10 + (c.toNat - 48)) 0) + else none + +/-- Read the number list of a payload. The empty payload is the + empty list. -/ +def numsOf (payload : String) : Option (List Nat) := + if payload.isEmpty then some [] + else (payload.splitOn ",").mapM parseNat + +/-- Read the byte list of a payload: every number at most 255. -/ +def bytesOf (payload : String) : Option (List UInt8) := + (numsOf payload).bind fun ns => + if ns.all (· ≤ 255) then some (ns.map Nat.toUInt8) else none + +/-- Print a number list as comma parted decimal numbers. -/ +def joinNums (ns : List Nat) : String := + ns.foldl (fun acc n => if acc.isEmpty then toString n else acc ++ "," ++ toString n) "" + +/-- Run one operation on one payload. The answer is `error` for a + malformed request, and `none` for well formed bytes that this + slice rejects. -/ +def run (op payload : String) : String := + match op with + | "parse" => + match bytesOf payload with + | none => "error" + | some bs => + match parse bs with + | some v => "ok:" ++ joinNums ((print v).map UInt8.toNat) + | none => "none" + | _ => "error" + +/-- Answer one request line. An empty line gets no answer. -/ +def processLine (line : String) : Option String := + if line.isEmpty then none + else + match line.splitOn " " with + | [op] => some (run op "") + | [op, payload] => some (run op payload) + | _ => some "error" + +/-- The line without its line ending: LF, or CR LF. -/ +def chomp (line : String) : String := + let cs := line.toList + if cs.getLast? = some '\n' then + let cs := cs.dropLast + String.ofList (if cs.getLast? = some '\r' then cs.dropLast else cs) + else line + +def main : IO Unit := do + let stdin ← IO.getStdin + repeat + let line ← stdin.getLine + if line.isEmpty then break + match processLine (chomp line) with + | some out => IO.println out + | none => pure () diff --git a/Mqtt.lean b/Mqtt.lean new file mode 100644 index 0000000..b802af6 --- /dev/null +++ b/Mqtt.lean @@ -0,0 +1,2 @@ +import Mqtt.Value +import Mqtt.Parse diff --git a/Mqtt/Parse.lean b/Mqtt/Parse.lean new file mode 100644 index 0000000..628cc33 --- /dev/null +++ b/Mqtt/Parse.lean @@ -0,0 +1,370 @@ +/- + The MQTT 5.0 packet reader. + + The reader works on a byte list and reads one packet from its + front, returning the packet and the bytes after it, so a + caller can walk a stream of packets arriving over TCP. It + never reads past the end of its input: every length in the + packet (the remaining length, a property length, a string or + binary length) is checked against the bytes that actually + remain before any of them are taken. + + Rules the reader follows, beyond the layout in SPEC.md: + + - A variable byte integer stops at four bytes: a continuation + bit on the fourth byte is rejected, and a value cut off by + the end of the input is rejected. An encoding that uses more + bytes than the value needs is accepted, as long as it fits + in four bytes (see SPEC.md for this pinned reading). + - A packet type outside the seven this slice covers is + rejected, and so is a fixed header flags nibble other than + the one the specification fixes for the type; PUBLISH is + the only type whose flags carry meaning, and its reserved + QoS value 3 is rejected. + - The body of a packet is cut out by its remaining length + first, and the type's reader must consume the cut exactly: + bytes left over inside the cut are rejected, and a field + that runs past the cut is rejected. + - Properties are checked against the specification's table: + an identifier with no table entry, an identifier not + allowed on the packet kind at hand, and a repeat of a single + use property are all rejected. +-/ + +import Mqtt.Value + +namespace Mqtt + +/-! ## Byte readers -/ + +/-- Read a big endian number of exactly `k` bytes from the + front of a byte list. Returns the number and the bytes + after it, or `none` when fewer than `k` bytes stand there. -/ +def readNat : Nat → List UInt8 → Option (Nat × List UInt8) + | 0, bs => some (0, bs) + | _ + 1, [] => none + | k + 1, b :: bs => + (readNat k bs).map fun (u, r) => (b.toNat * 256 ^ k + u, r) + +/-- The unfolding rule for `readNat` at a successor width on a + list with a head byte. -/ +theorem readNat_succ_cons (k : Nat) (b : UInt8) (bs : List UInt8) : + readNat (k + 1) (b :: bs) = + (readNat k bs).map fun (u, r) => (b.toNat * 256 ^ k + u, r) := by + rw [readNat] + +/-- Take `n` bytes off the front of a byte list, or `none` when + fewer than `n` bytes stand there. Returns the bytes taken + and the bytes after them. -/ +def readBytes (n : Nat) (bs : List UInt8) : Option (List UInt8 × List UInt8) := + if bs.length ≥ n then some (bs.take n, bs.drop n) else none + +/-- Read one byte as a number. -/ +def readByte : List UInt8 → Option (Nat × List UInt8) + | [] => none + | b :: bs => some (b.toNat, bs) + +/-! ## The variable byte integer reader -/ + +/-- Read a variable byte integer with at most `k` bytes left to + spend, accumulating `mult` times the groups still to come. + A byte below 128 ends the number. A continuation byte on + the last byte the count allows is rejected, and so is the + end of the input while a continuation bit stands. -/ +def decVBIGo (k acc mult : Nat) : List UInt8 → Option (Nat × List UInt8) + | [] => none + | b :: bs => + if b.toNat < 128 then some (acc + mult * b.toNat, bs) + else if k ≤ 1 then none + else decVBIGo (k - 1) (acc + mult * (b.toNat - 128)) (mult * 128) bs + +/-- Read a variable byte integer (section 2.1.4): at most four + bytes. Returns the value and the bytes after it. -/ +def decVBI (bs : List UInt8) : Option (Nat × List UInt8) := + decVBIGo 4 0 1 bs + +/-! ## String and binary readers -/ + +/-- Check a decoded string field's characters: the strict + decoder has already settled well formedness; the null + character must also be absent (section 1.5.4). -/ +def checkChars (s : List Char) : Option (List Char) := + if hasNul s then none else some s + +/-- Read a string field: the two byte length, that many bytes, + read as strict UTF-8 with no null character. -/ +def readStr (bs : List UInt8) : Option (List Char × List UInt8) := do + let (len, r1) ← readNat 2 bs + let (chunk, r2) ← readBytes len r1 + let s ← (Utf8.decode chunk).bind checkChars + pure (s, r2) + +/-- Read a binary data field: the two byte length, then that + many bytes. -/ +def readBin (bs : List UInt8) : Option (List UInt8 × List UInt8) := do + let (len, r1) ← readNat 2 bs + readBytes len r1 + +/-! ## Property readers -/ + +/-- Read a property value of the given type. -/ +def readPropVal (t : PropType) : List UInt8 → Option (PropVal × List UInt8) + | bs => + match t with + | .byte => (readNat 1 bs).map fun (n, r) => (.byte n, r) + | .twoByte => (readNat 2 bs).map fun (n, r) => (.twoByte n, r) + | .fourByte => (readNat 4 bs).map fun (n, r) => (.fourByte n, r) + | .varByte => (decVBI bs).map fun (n, r) => (.varByte n, r) + | .utf8 => (readStr bs).map fun (s, r) => (.utf8 s, r) + | .utf8Pair => do + let (k, r1) ← readStr bs + let (v, r2) ← readStr r1 + pure (.utf8Pair k v, r2) + | .binary => (readBin bs).map fun (chunk, r) => (.binary chunk, r) + +/-- Read one property: the identifier as a variable byte + integer, checked against the table and the block's allowed + list, then the value in the shape of the table's type for + the identifier. A repeat of a single use property whose + identifier already stands in `seen` is rejected. -/ +def readEntry (s : PropSet) (seen : List Nat) (bs : List UInt8) : + Option (Property × List UInt8) := do + let (id, r1) ← decVBI bs + if (allowedOf s).contains id && (repeatableIn s id || !seen.contains id) then + match propTypeOf id with + | none => none + | some t => (readPropVal t r1).map fun (v, r2) => (⟨id, v⟩, r2) + else none + +/-- Read properties until the input runs out, or `none` when + one fails to read. The fuel is a bound on the number of + properties: each property takes at least two bytes (an + identifier and one value byte at the least), so the input + length is always fuel enough. The `seen` list carries the + identifiers already read in this block. -/ +def readEntriesGo : Nat → PropSet → List Nat → List UInt8 → + Option (List Property × List UInt8) + | 0, _, _, bs => if bs.isEmpty then some ([], bs) else none + | fuel + 1, s, seen, bs => + if bs.isEmpty then some ([], bs) + else match readEntry s seen bs with + | none => none + | some (p, r1) => + match readEntriesGo fuel s (p.id :: seen) r1 with + | none => none + | some (ps, r2) => some (p :: ps, r2) + +/-- Read a whole property block's insides: exactly the given + bytes, all consumed. -/ +def readEntries (s : PropSet) (seg : List UInt8) : Option (List Property) := + match readEntriesGo seg.length s [] seg with + | some (ps, []) => some ps + | _ => none + +/-- Read a property block: the property length as a variable + byte integer, then exactly that many bytes of properties. + Bytes left over inside the block, or a block that runs past + the bytes at hand, are rejected. -/ +def readProps (s : PropSet) (bs : List UInt8) : + Option (List Property × List UInt8) := do + let (len, r1) ← decVBI bs + let (seg, r2) ← readBytes len r1 + let ps ← readEntries s seg + pure (ps, r2) + +/-! ## SUBSCRIBE filter readers -/ + +/-- Read a subscription options byte. The reserved bits 6 and + 7 must be clear, and neither the QoS field nor the retain + handling field may hold the reserved value 3. -/ +def readOptsByte (b : Nat) : Option SubOpts := + if b < 64 ∧ b % 4 ≠ 3 ∧ (b / 16) % 4 ≠ 3 then + some ⟨b % 4, (b / 4) % 2 = 1, (b / 8) % 2 = 1, (b / 16) % 4⟩ + else none + +/-- Read topic filters until the input runs out, or `none` + when one fails to read. The fuel is a bound on the number + of filters: each filter takes at least three bytes (a two + byte length and an options byte), so the input length is + always fuel enough. -/ +def readFiltersGo : Nat → List UInt8 → + Option (List (List Char × SubOpts) × List UInt8) + | 0, bs => if bs.isEmpty then some ([], bs) else none + | fuel + 1, bs => + if bs.isEmpty then some ([], bs) + else match readStr bs with + | none => none + | some (f, ob :: r2) => + match readOptsByte ob.toNat with + | none => none + | some o => + match readFiltersGo fuel r2 with + | none => none + | some (fs, r3) => some ((f, o) :: fs, r3) + | some (_, []) => none + +/-! ## Body readers -/ + +/-- The `k`th bit of a number, as a boolean: bit 0 is the least + significant. -/ +def flagBit (n k : Nat) : Bool := (n / 2 ^ k) % 2 = 1 + +/-- A topic name check for a read string: not empty, and + neither wildcard character stands in it. -/ +def checkTopic (s : List Char) : Option (List Char) := + if s.isEmpty || s.any (fun c => decide (c = '+')) || s.any (fun c => decide (c = '#')) then + none + else some s + +/-- Read the will step of a CONNECT body: the will + properties, will topic and will payload when the will + flag is set, nothing when it is clear. The will QoS and + will retain come from the connect flags byte. -/ +def readWillPart (flags : Nat) (r6 : List UInt8) : + Option (Option Will × List UInt8) := + if flagBit flags 2 then + (readProps .will r6).bind fun (wprops, s1) => + (readStr s1).bind fun (wtopic, s2) => + (checkTopic wtopic).bind fun wtopic => + (readBin s2).bind fun (wpay, s3) => + some (some ⟨(flags / 8) % 4, flagBit flags 5, wprops, wtopic, wpay⟩, s3) + else some (none, r6) + +/-- Read an optional string field of a CONNECT payload, + present exactly when its connect flag bit is set. -/ +def readOptStrField (cond : Bool) (r : List UInt8) : + Option (Option (List Char) × List UInt8) := + if cond then (readStr r).map fun (u, r') => (some u, r') + else some (none, r) + +/-- Read an optional binary field of a CONNECT payload, + present exactly when its connect flag bit is set. -/ +def readOptBinField (cond : Bool) (r : List UInt8) : + Option (Option (List UInt8) × List UInt8) := + if cond then (readBin r).map fun (p, r') => (some p, r') + else some (none, r) + +/-- Read a CONNECT body: the whole body cut, nothing left + over. The protocol name must be "MQTT" and the level 5. The + reserved connect flag bit must be clear and the will QoS + must not be the reserved value 3. The payload fields stand + exactly when the connect flags say they stand. -/ +def readConnectBody (seg : List UInt8) : Option Connect := + (readStr seg).bind fun (proto, r1) => + if proto = ['M', 'Q', 'T', 'T'] then + (readByte r1).bind fun (level, r2) => + if level = 5 then + (readByte r2).bind fun (flags, r3) => + if flags % 2 = 0 then + if (flags / 8) % 4 ≠ 3 then + (readNat 2 r3).bind fun (ka, r4) => + (readProps .connect r4).bind fun (props, r5) => + (readStr r5).bind fun (cid, r6) => + (readWillPart flags r6).bind fun (will, r7) => + (readOptStrField (flagBit flags 7) r7).bind fun (username, r8) => + (readOptBinField (flagBit flags 6) r8).bind fun (password, r9) => + if r9.isEmpty then + some ⟨flagBit flags 1, ka, props, cid, will, username, password⟩ + else none + else none + else none + else none + else none + +/-- Read the packet identifier step of a PUBLISH body: no + identifier at QoS 0, a two byte nonzero identifier at + QoS 1 and 2. -/ +def readPacketId (flags : Nat) (r1 : List UInt8) : + Option (Option Nat × List UInt8) := + if (flags / 2) % 4 = 0 then some (none, r1) + else (readNat 2 r1).bind fun (id, r) => + if id ≠ 0 then some (some id, r) else none + +/-- Read a PUBLISH body: topic name, the packet identifier + when the QoS is 1 or 2 (and never 0), the properties, and + the payload, which is all the bytes that remain in the cut. + The QoS comes from the fixed header flags; the reserved + value 3 has already been turned away by the caller. -/ +def readPublishBody (flags : Nat) (seg : List UInt8) : Option Publish := + (readStr seg).bind fun (topic, r1) => + (checkTopic topic).bind fun topic => + (readPacketId flags r1).bind fun (pid, r2) => + (readProps .publish r2).bind fun (props, payload) => + some ⟨flagBit flags 3, (flags / 2) % 4, flagBit flags 0, topic, pid, + props, payload⟩ + +/-- Read a SUBSCRIBE body: a nonzero packet identifier, the + properties, and a nonempty list of topic filters that + fills the rest of the cut exactly. -/ +def readSubscribeBody (seg : List UInt8) : Option Packet := do + let (id, r1) ← readNat 2 seg + if id ≠ 0 then pure () else none + let (props, r2) ← readProps .subscribe r1 + let (fs, r3) ← readFiltersGo r2.length r2 + if r3.isEmpty && !fs.isEmpty then pure (.subscribe id props fs) else none + +/-- Read a SUBACK body: a nonzero packet identifier, the + properties, and a nonempty list of reason codes filling + the rest of the cut. -/ +def readSubackBody (seg : List UInt8) : Option Packet := do + let (id, r1) ← readNat 2 seg + if id ≠ 0 then pure () else none + let (props, r2) ← readProps .suback r1 + if !r2.isEmpty then pure (.suback id props (r2.map UInt8.toNat)) else none + +/-- Read a DISCONNECT body: an empty cut is a normal + disconnection with no body. A cut of one byte is a reason + code on its own: the specification omits the property + length when the remaining length is 1 (section 3.14.2). + A longer cut is a reason code and a property block that + fills the rest of the cut. -/ +def readDisconnectBody (seg : List UInt8) : Option Packet := + match seg with + | [] => some (.disconnect none) + | rc :: r1 => + if r1.isEmpty then some (.disconnect (some (rc.toNat, []))) + else do + let (props, r2) ← readProps .disconnect r1 + if r2.isEmpty then pure (.disconnect (some (rc.toNat, props))) else none + +/-- Read a packet body of the given type, with the given fixed + header flags, from a body cut out by the remaining length. + The reader must consume the cut exactly. Packet types + outside the seven this slice covers are rejected, and so + is a flags nibble other than the one the specification + fixes for the type. -/ +def parseBody (typ flags : Nat) (seg : List UInt8) : Option Packet := + match typ with + | 1 => if flags = 0 then (readConnectBody seg).map Packet.connect else none + | 3 => + if (flags / 2) % 4 = 3 then none + else (readPublishBody flags seg).map Packet.publish + | 8 => if flags = 2 then readSubscribeBody seg else none + | 9 => if flags = 0 then readSubackBody seg else none + | 12 => if flags = 0 && seg.isEmpty then some .pingreq else none + | 13 => if flags = 0 && seg.isEmpty then some .pingresp else none + | 14 => if flags = 0 then readDisconnectBody seg else none + | _ => none + +/-! ## The packet reader -/ + +/-- Read one packet from the front of a byte list: the fixed + header byte, the remaining length, and exactly that many + body bytes. Returns the packet and the bytes after it. -/ +def parsePacket (bs : List UInt8) : Option (Packet × List UInt8) := + match bs with + | [] => none + | b :: r0 => do + let (len, r1) ← decVBI r0 + let (seg, r2) ← readBytes len r1 + let p ← parseBody (b.toNat / 16) (b.toNat % 16) seg + pure (p, r2) + +/-- Read one whole packet: exactly one packet, with nothing + after it. -/ +def parse (bs : List UInt8) : Option Packet := + match parsePacket bs with + | some (p, []) => some p + | _ => none + +end Mqtt diff --git a/Mqtt/Utf8.lean b/Mqtt/Utf8.lean new file mode 100644 index 0000000..05ca366 --- /dev/null +++ b/Mqtt/Utf8.lean @@ -0,0 +1,85 @@ +/- + UTF-8, by hand: MQTT strings travel on the wire as bytes, and + the string fields in this slice are held as lists of + characters, so the packet code needs both directions between + characters and bytes. + + The encoder writes the standard one to four bytes per + character. The decoder is strict. It turns away stray + continuation bytes, overlong forms (a character written with + more bytes than it needs, including any lead byte below C2), + lead bytes above F4, encodings of the surrogate values D800 to + DFFF, values above 10FFFF, and truncated sequences. + + This file is carried in from the jws project's Jws/Utf8.lean, + written for the Proven Commons jws slice, with the namespace + renamed. The repos in this programme do not share a library, + so the code travels. +-/ + +namespace Mqtt.Utf8 + +/-- The bytes of one character. -/ +def encodeChar (c : Char) : List UInt8 := + let n := c.toNat + if n < 0x80 then [n.toUInt8] + else if n < 0x800 then + [(0xC0 + n / 64).toUInt8, (0x80 + n % 64).toUInt8] + else if n < 0x10000 then + [(0xE0 + n / 4096).toUInt8, (0x80 + (n / 64) % 64).toUInt8, (0x80 + n % 64).toUInt8] + else + [(0xF0 + n / 262144).toUInt8, (0x80 + (n / 4096) % 64).toUInt8, + (0x80 + (n / 64) % 64).toUInt8, (0x80 + n % 64).toUInt8] + +/-- The bytes of a text. -/ +def encode (cs : List Char) : List UInt8 := + cs.flatMap encodeChar + +/-- The payload bits of a continuation byte (80 to BF). -/ +def contVal (b : UInt8) : Option Nat := + if 0x80 ≤ b.toNat ∧ b.toNat < 0xC0 then some (b.toNat - 0x80) else none + +/-- Strict decoding. The side conditions on the three and four + byte forms are the overlong, surrogate, and range rules: + after E0 the first continuation value is at least 32, after + ED it is below 32, after F0 it is at least 16, after F4 it + is below 16. -/ +def decode : List UInt8 → Option (List Char) + | [] => some [] + | b :: rest => + if b.toNat < 0x80 then + (decode rest).map fun cs => Char.ofNat b.toNat :: cs + else if b.toNat < 0xC2 then none + else if b.toNat < 0xE0 then + match rest with + | b1 :: rest1 => + match contVal b1 with + | some v1 => (decode rest1).map fun cs => + Char.ofNat ((b.toNat - 0xC0) * 64 + v1) :: cs + | none => none + | [] => none + else if b.toNat < 0xF0 then + match rest with + | b1 :: b2 :: rest1 => + match contVal b1, contVal b2 with + | some v1, some v2 => + if (b.toNat = 0xE0 → 0x20 ≤ v1) ∧ (b.toNat = 0xED → v1 < 0x20) then + (decode rest1).map fun cs => + Char.ofNat ((b.toNat - 0xE0) * 4096 + v1 * 64 + v2) :: cs + else none + | _, _ => none + | _ => none + else if b.toNat < 0xF5 then + match rest with + | b1 :: b2 :: b3 :: rest1 => + match contVal b1, contVal b2, contVal b3 with + | some v1, some v2, some v3 => + if (b.toNat = 0xF0 → 0x10 ≤ v1) ∧ (b.toNat = 0xF4 → v1 < 0x10) then + (decode rest1).map fun cs => + Char.ofNat ((b.toNat - 0xF0) * 262144 + v1 * 4096 + v2 * 64 + v3) :: cs + else none + | _, _, _ => none + | _ => none + else none + +end Mqtt.Utf8 diff --git a/Mqtt/Value.lean b/Mqtt/Value.lean new file mode 100644 index 0000000..4261678 --- /dev/null +++ b/Mqtt/Value.lean @@ -0,0 +1,513 @@ +/- + MQTT 5.0 packet values and the printer. + + A packet is one of the seven control packet types this slice + covers: CONNECT, PUBLISH, SUBSCRIBE, SUBACK, PINGREQ, + PINGRESP, and DISCONNECT. The printer writes a packet as the + fixed header byte, the remaining length as a variable byte + integer, and the body: the variable header and payload for the + packet's type. + + Properties are held as an identifier and a typed value. The + value type of an identifier is fixed by the specification's + property table (section 2.2.2, Table 2-4), which also says + which packets a property may appear on. Will properties, the + property block inside a CONNECT packet's will, count as their + own packet kind for that table, as the specification's table + lists them on their own line. + + Strings are held as lists of characters. What a string means + as bytes is settled by the strict UTF-8 codec in Mqtt/Utf8. +-/ + +import Mqtt.Utf8 + +namespace Mqtt + +/-! ## Big endian byte strings -/ + +/-- Write a number in exactly `k` bytes, most significant byte + first. Bytes past the number's own width are zero, and a + number too wide for `k` bytes loses its top bytes: the + printer only calls this with a width the number fits. -/ +def writeBE : Nat → Nat → List UInt8 + | 0, _ => [] + | k + 1, n => ((n / 256 ^ k) % 256).toUInt8 :: writeBE k (n % 256 ^ k) + +/-- The unfolding rule for `writeBE` at a successor width. -/ +theorem writeBE_succ (k n : Nat) : + writeBE (k + 1) n = ((n / 256 ^ k) % 256).toUInt8 :: writeBE k (n % 256 ^ k) := by + rw [writeBE] + +/-- A big endian writing is exactly as long as its width. -/ +theorem writeBE_length : ∀ (k n : Nat), (writeBE k n).length = k + | 0, _ => rfl + | k + 1, n => by rw [writeBE_succ]; simp [writeBE_length k] + +/-! ## The variable byte integer -/ + +/-- Write a number as a variable byte integer (section 2.1.4): + seven bits per byte, low groups first, the top bit of each + byte but the last set as a continuation mark. The format + carries at most four bytes, so numbers below 2^28 are the + ones with a complete writing; a larger number loses its top + groups here, and the well formedness rules below keep every + written number under the bound. -/ +def printVBI (n : Nat) : List UInt8 := + if n < 128 then [n.toUInt8] + else (128 + n % 128).toUInt8 :: printVBI (n / 128) +termination_by n +decreasing_by + exact Nat.div_lt_self (by omega) (by decide) + +/-- The unfolding rule for `printVBI`. -/ +theorem printVBI_def (n : Nat) : + printVBI n = if n < 128 then [n.toUInt8] + else (128 + n % 128).toUInt8 :: printVBI (n / 128) := by + rw [printVBI] + +/-! ## Properties: the table -/ + +/-- The value type of a property, as the specification's + property table gives it. -/ +inductive PropType where + | byte : PropType + | twoByte : PropType + | fourByte : PropType + | varByte : PropType + | utf8 : PropType + | utf8Pair : PropType + | binary : PropType + deriving DecidableEq, Repr + +/-- A property value, in the shape of its type. Strings are + lists of characters; binary data is a list of bytes. -/ +inductive PropVal where + | byte (n : Nat) : PropVal + | twoByte (n : Nat) : PropVal + | fourByte (n : Nat) : PropVal + | varByte (n : Nat) : PropVal + | utf8 (s : List Char) : PropVal + | utf8Pair (k v : List Char) : PropVal + | binary (bs : List UInt8) : PropVal + deriving DecidableEq, Repr + +/-- The type of a property value. -/ +def valType : PropVal → PropType + | .byte _ => .byte + | .twoByte _ => .twoByte + | .fourByte _ => .fourByte + | .varByte _ => .varByte + | .utf8 _ => .utf8 + | .utf8Pair _ _ => .utf8Pair + | .binary _ => .binary + +/-- One property: an identifier and a value. -/ +structure Property where + id : Nat + val : PropVal + deriving DecidableEq, Repr + +/-- The specification's property table (section 2.2.2, + Table 2-4): the value type of each identifier the + specification defines. An identifier the table does not + list has no type here, and the reader rejects it. -/ +def propTypeOf : Nat → Option PropType + | 0x01 => some .byte + | 0x02 => some .fourByte + | 0x03 => some .utf8 + | 0x08 => some .utf8 + | 0x09 => some .binary + | 0x0B => some .varByte + | 0x11 => some .fourByte + | 0x12 => some .utf8 + | 0x13 => some .twoByte + | 0x15 => some .utf8 + | 0x16 => some .binary + | 0x17 => some .byte + | 0x18 => some .fourByte + | 0x19 => some .byte + | 0x1A => some .utf8 + | 0x1C => some .utf8 + | 0x1F => some .utf8 + | 0x21 => some .twoByte + | 0x22 => some .twoByte + | 0x23 => some .twoByte + | 0x24 => some .byte + | 0x25 => some .byte + | 0x26 => some .utf8Pair + | 0x27 => some .fourByte + | 0x28 => some .byte + | 0x29 => some .byte + | 0x2A => some .byte + | _ => none + +/-- The places a property block can stand, for the table's + packet column: the CONNECT packet's own block, the will + block inside CONNECT, and one block each for PUBLISH, + SUBSCRIBE, SUBACK, and DISCONNECT. -/ +inductive PropSet where + | connect : PropSet + | will : PropSet + | publish : PropSet + | subscribe : PropSet + | suback : PropSet + | disconnect : PropSet + deriving DecidableEq, Repr + +/-- The identifiers the specification's table allows on each + property block, by the table's packet column. -/ +def allowedOf : PropSet → List Nat + | .connect => [0x11, 0x15, 0x16, 0x17, 0x19, 0x21, 0x22, 0x26, 0x27] + | .will => [0x01, 0x02, 0x03, 0x08, 0x09, 0x18, 0x26] + | .publish => [0x01, 0x02, 0x03, 0x08, 0x09, 0x0B, 0x23, 0x26] + | .subscribe => [0x0B, 0x26] + | .suback => [0x1F, 0x26] + | .disconnect => [0x11, 0x1C, 0x1F, 0x26] + +/-- May this property appear more than once in one block? The + user property (0x26) may, wherever it is allowed. The + subscription identifier (0x0B) may repeat on PUBLISH: a + server sending one message for several matching + subscriptions carries one identifier per subscription, and + the identifiers may be equal (section 3.3.4). Every other + property is single use: a second copy in one block is + rejected. -/ +def repeatableIn (s : PropSet) (id : Nat) : Bool := + id = 0x26 || (id = 0x0B && s = .publish) + +/-! ## String checks + + The specification's string rules (section 1.5.4): a string is + well formed UTF-8 and must not contain the null character + U+0000. The byte length of a string field must also fit the + two byte length prefix. -/ + +/-- Does this text contain the null character? -/ +def hasNul (s : List Char) : Bool := + s.any fun c => decide (c = '\u0000') + +/-- A string fit to print: no null character, and its UTF-8 + byte length fits the two byte length prefix. -/ +def StrWF (s : List Char) : Prop := + '\u0000' ∉ s ∧ (Utf8.encode s).length ≤ 65535 + +/-- Binary data fit to print: its length fits the two byte + length prefix. -/ +def BinWF (bs : List UInt8) : Prop := + bs.length ≤ 65535 + +/-- A topic name fit to print (section 4.7.1): a string, not + empty, holding neither wildcard character. -/ +def TopicWF (s : List Char) : Prop := + StrWF s ∧ s ≠ [] ∧ '+' ∉ s ∧ '#' ∉ s + +/-! ## Field printers -/ + +/-- Print a string field: the two byte length of its UTF-8 + bytes, then the bytes (section 1.5.4). -/ +def printStr (s : List Char) : List UInt8 := + writeBE 2 (Utf8.encode s).length ++ Utf8.encode s + +/-- Print a binary data field: the two byte length, then the + bytes (section 1.5.3). -/ +def printBin (bs : List UInt8) : List UInt8 := + writeBE 2 bs.length ++ bs + +/-- Print a property value, in the shape of its type. -/ +def printPropVal : PropVal → List UInt8 + | .byte n => [n.toUInt8] + | .twoByte n => writeBE 2 n + | .fourByte n => writeBE 4 n + | .varByte n => printVBI n + | .utf8 s => printStr s + | .utf8Pair k v => printStr k ++ printStr v + | .binary bs => printBin bs + +/-- Print one property: the identifier as a variable byte + integer, then the value. -/ +def printProperty (p : Property) : List UInt8 := + printVBI p.id ++ printPropVal p.val + +/-- Print a list of properties, one after the other. -/ +def printPropsList : List Property → List UInt8 + | [] => [] + | p :: ps => printProperty p ++ printPropsList ps + +/-- Print a property block: the property length as a variable + byte integer, then the properties themselves (section + 2.2.2). -/ +def printProps (ps : List Property) : List UInt8 := + printVBI (printPropsList ps).length ++ printPropsList ps + +/-! ## The packet values -/ + +/-- The subscription options of one topic filter in a SUBSCRIBE + packet (section 3.8.3): a maximum QoS, the no local and + retain as published flags, and a retain handling choice. -/ +structure SubOpts where + qos : Nat + noLocal : Bool + retainAsPublished : Bool + retainHandling : Nat + deriving DecidableEq, Repr + +/-- The options byte of a filter: QoS in bits 0 and 1, no local + at bit 2, retain as published at bit 3, retain handling in + bits 4 and 5, and the reserved bits 6 and 7 clear. -/ +def printOptsByte (o : SubOpts) : UInt8 := + (o.qos + (if o.noLocal then 4 else 0) + (if o.retainAsPublished then 8 else 0) + + o.retainHandling * 16).toUInt8 + +/-- A will, the part of a CONNECT packet that stands when its + will flag is set (section 3.1.3): will properties, a will + topic, and a will payload, with the QoS and retain flag the + connect flags byte carries. -/ +structure Will where + qos : Nat + retain : Bool + props : List Property + topic : List Char + payload : List UInt8 + deriving DecidableEq, Repr + +/-- A CONNECT packet's fields (section 3.1). The protocol name + and level are not fields: this slice reads and writes MQTT + 5.0 only, so they are fixed at "MQTT" and 5. The connect + flags byte is computed from the fields that drive it: the + username and password options, the will option with its QoS + and retain flag, and the clean start flag. -/ +structure Connect where + cleanStart : Bool + keepAlive : Nat + props : List Property + clientId : List Char + will : Option Will + username : Option (List Char) + password : Option (List UInt8) + deriving DecidableEq, Repr + +/-- A PUBLISH packet's fields (section 3.3). The packet + identifier stands exactly when the QoS is 1 or 2, so it is + an option beside the QoS. -/ +structure Publish where + dup : Bool + qos : Nat + retain : Bool + topic : List Char + packetId : Option Nat + props : List Property + payload : List UInt8 + deriving DecidableEq, Repr + +/-- A control packet of one of the seven types this slice + covers. -/ +inductive Packet where + | connect (c : Connect) : Packet + | publish (p : Publish) : Packet + | subscribe (packetId : Nat) (props : List Property) + (filters : List (List Char × SubOpts)) : Packet + | suback (packetId : Nat) (props : List Property) + (reasons : List Nat) : Packet + | pingreq : Packet + | pingresp : Packet + | disconnect (body : Option (Nat × List Property)) : Packet + deriving DecidableEq, Repr + +/-! ## Body printers -/ + +/-- The connect flags byte (section 3.1.2): username flag at + bit 7, password flag at bit 6, will retain at bit 5, will + QoS at bits 4 and 3, will flag at bit 2, clean start at + bit 1, and the reserved bit 0 clear. -/ +def connectFlags (c : Connect) : Nat := + (if c.username.isSome then 128 else 0) + + (if c.password.isSome then 64 else 0) + + (match c.will with + | some w => (if w.retain then 32 else 0) + w.qos * 8 + 4 + | none => 0) + + (if c.cleanStart then 2 else 0) + +/-- Print the will part of a CONNECT payload, or nothing when + there is no will. -/ +def printWillPart : Option Will → List UInt8 + | none => [] + | some w => printProps w.props ++ (printStr w.topic ++ printBin w.payload) + +/-- Print an optional string field, or nothing. -/ +def printOptStr : Option (List Char) → List UInt8 + | none => [] + | some s => printStr s + +/-- Print an optional binary field, or nothing. -/ +def printOptBin : Option (List UInt8) → List UInt8 + | none => [] + | some bs => printBin bs + +/-- The body of a CONNECT packet: the protocol name, protocol + level, connect flags, and keep alive, then the properties, + then the payload: client identifier, the will fields when + the will flag is set, the username when its flag is set, + and the password when its flag is set. -/ +def printConnectBody (c : Connect) : List UInt8 := + printStr ['M', 'Q', 'T', 'T'] ++ ([5, (connectFlags c).toUInt8] + ++ (writeBE 2 c.keepAlive ++ (printProps c.props ++ (printStr c.clientId + ++ (printWillPart c.will ++ (printOptStr c.username + ++ printOptBin c.password)))))) + +/-- The fixed header byte of a PUBLISH packet: the type 3, the + DUP flag at bit 3, the QoS at bits 2 and 1, and RETAIN at + bit 0. -/ +def publishHeader (p : Publish) : Nat := + 0x30 + (if p.dup then 8 else 0) + p.qos * 2 + (if p.retain then 1 else 0) + +/-- Print a packet identifier when one stands, or nothing. -/ +def printIdOpt : Option Nat → List UInt8 + | none => [] + | some id => writeBE 2 id + +/-- The body of a PUBLISH packet: topic name, the packet + identifier when the QoS carries one, the properties, then + the payload, which is all the bytes that remain. -/ +def printPublishBody (p : Publish) : List UInt8 := + printStr p.topic ++ (printIdOpt p.packetId ++ (printProps p.props ++ p.payload)) + +/-- Print one topic filter of a SUBSCRIBE payload: the filter + string, then its options byte. -/ +def printFilter (f : List Char × SubOpts) : List UInt8 := + printStr f.1 ++ [printOptsByte f.2] + +/-- Print a list of topic filters, one after the other. -/ +def printFilters : List (List Char × SubOpts) → List UInt8 + | [] => [] + | f :: fs => printFilter f ++ printFilters fs + +/-- The body of a SUBSCRIBE packet: packet identifier, + properties, then the topic filters. -/ +def printSubscribeBody (id : Nat) (ps : List Property) + (fs : List (List Char × SubOpts)) : List UInt8 := + writeBE 2 id ++ (printProps ps ++ printFilters fs) + +/-- The body of a SUBACK packet: packet identifier, properties, + then one reason code byte per granted subscription. -/ +def printSubackBody (id : Nat) (ps : List Property) (rs : List Nat) : List UInt8 := + writeBE 2 id ++ (printProps ps ++ rs.map Nat.toUInt8) + +/-- The body of a packet: everything after the fixed header + byte and the remaining length. -/ +def bodyOf : Packet → List UInt8 + | .connect c => printConnectBody c + | .publish p => printPublishBody p + | .subscribe id ps fs => printSubscribeBody id ps fs + | .suback id ps rs => printSubackBody id ps rs + | .pingreq => [] + | .pingresp => [] + | .disconnect none => [] + | .disconnect (some (rc, ps)) => [rc.toUInt8] ++ printProps ps + +/-- The fixed header byte of a packet: the type in the high + nibble, and the flags the specification fixes in the low + nibble (section 2.1.2). SUBSCRIBE carries 0010; PUBLISH + carries its own DUP, QoS, and RETAIN bits; the rest carry + 0000. -/ +def headerOf : Packet → UInt8 + | .connect _ => 0x10 + | .publish p => (publishHeader p).toUInt8 + | .subscribe _ _ _ => 0x82 + | .suback _ _ _ => 0x90 + | .pingreq => 0xC0 + | .pingresp => 0xD0 + | .disconnect _ => 0xE0 + +/-- Print a packet: the fixed header byte, the remaining length + as a variable byte integer, and the body. -/ +def print (p : Packet) : List UInt8 := + headerOf p :: printVBI (bodyOf p).length ++ bodyOf p + +/-! ## Well formed values + + The round trip claim in `Proofs` holds for well formed + packets: the fields the printer can write exactly. Numbers + fit the widths that carry them, strings obey the string + rules, properties match the table in type and place and do + not repeat a single use property, and the whole body fits + the remaining length's four byte variable byte integer. -/ + +/-- A property value in the shape the printer writes exactly. -/ +def ValWF : PropVal → Prop + | .byte n => n < 256 + | .twoByte n => n < 65536 + | .fourByte n => n < 4294967296 + | .varByte n => n < 268435456 + | .utf8 s => StrWF s + | .utf8Pair k v => StrWF k ∧ StrWF v + | .binary bs => BinWF bs + +/-- A property list in the shape of one block: every property + is allowed on the block's packet kind, its value matches + the table's type for its identifier and is itself well + formed, and no single use property repeats. The `seen` + list carries the identifiers already standing in the + block; calls start it empty. -/ +def PropsWF (s : PropSet) : List Nat → List Property → Prop + | _, [] => True + | seen, p :: ps => + p.id ∈ allowedOf s ∧ propTypeOf p.id = some (valType p.val) ∧ ValWF p.val + ∧ (repeatableIn s p.id = true ∨ p.id ∉ seen) + ∧ PropsWF s (p.id :: seen) ps + +/-- A property block fit to print: the list is well formed and + its printed length fits a variable byte integer. -/ +def PropsBlockWF (s : PropSet) (ps : List Property) : Prop := + PropsWF s [] ps ∧ (printPropsList ps).length < 268435456 + +/-- A will fit to print. -/ +def WillWF (w : Will) : Prop := + w.qos ≤ 2 ∧ PropsBlockWF .will w.props ∧ TopicWF w.topic ∧ BinWF w.payload + +/-- A CONNECT packet fit to print. -/ +def ConnectWF (c : Connect) : Prop := + c.keepAlive < 65536 ∧ PropsBlockWF .connect c.props ∧ StrWF c.clientId + ∧ (∀ w, c.will = some w → WillWF w) + ∧ (∀ u, c.username = some u → StrWF u) + ∧ (∀ p, c.password = some p → BinWF p) + +/-- A PUBLISH packet fit to print. The packet identifier + stands exactly when the QoS is 1 or 2, and is never 0. -/ +def PublishWF (p : Publish) : Prop := + p.qos ≤ 2 ∧ TopicWF p.topic + ∧ (∀ id, p.packetId = some id → 1 ≤ id ∧ id < 65536 ∧ (p.qos = 1 ∨ p.qos = 2)) + ∧ (p.packetId = none → p.qos = 0) + ∧ PropsBlockWF .publish p.props + +/-- Subscription options fit to print: the QoS and the retain + handling choice are at most 2 (3 is reserved in both). -/ +def OptsWF (o : SubOpts) : Prop := + o.qos ≤ 2 ∧ o.retainHandling ≤ 2 + +/-- A topic filter list fit to print, member by member. -/ +def FiltersWF : List (List Char × SubOpts) → Prop + | [] => True + | (f, o) :: fs => StrWF f ∧ OptsWF o ∧ FiltersWF fs + +/-- The per type half of well formedness for a packet. -/ +def PacketFieldsWF : Packet → Prop + | .connect c => ConnectWF c + | .publish p => PublishWF p + | .subscribe id ps fs => + 1 ≤ id ∧ id < 65536 ∧ PropsBlockWF .subscribe ps ∧ fs ≠ [] ∧ FiltersWF fs + | .suback id ps rs => + 1 ≤ id ∧ id < 65536 ∧ PropsBlockWF .suback ps ∧ rs ≠ [] + ∧ (∀ r ∈ rs, r < 256) + | .pingreq => True + | .pingresp => True + | .disconnect none => True + | .disconnect (some (rc, ps)) => rc < 256 ∧ PropsBlockWF .disconnect ps + +/-- A packet fit to print: its fields are well formed and its + body fits the remaining length, a variable byte integer of + at most four bytes. -/ +def PacketWF (p : Packet) : Prop := + PacketFieldsWF p ∧ (bodyOf p).length < 268435456 + +end Mqtt diff --git a/Mqtt/Verify.lean b/Mqtt/Verify.lean new file mode 100644 index 0000000..1d0b3a7 --- /dev/null +++ b/Mqtt/Verify.lean @@ -0,0 +1,22 @@ +/- + Axiom check for the claims this package makes. Run with: + + lake env lean Mqtt/Verify.lean + + Every claim should list only the standard axioms (propext, + Classical.choice, Quot.sound). A line naming sorryAx would mean + a proof rests on an admitted gap, and the claim is not proved. +-/ + +import Proofs +import Proofs.Examples + +open Mqtt.Proofs Mqtt.Examples + +#print axioms parse_print +#print axioms parsePacket_print +#print axioms decVBI_printVBI +#print axioms parse_connect +#print axioms parse_publish_qos1 +#print axioms vbi_max +#print axioms vbi_five_bytes diff --git a/Proofs.lean b/Proofs.lean new file mode 100644 index 0000000..5aede97 --- /dev/null +++ b/Proofs.lean @@ -0,0 +1,3 @@ +import Proofs.Utf8 +import Proofs.RoundTrip +import Proofs.Examples diff --git a/Proofs/Examples.lean b/Proofs/Examples.lean new file mode 100644 index 0000000..6a49abf --- /dev/null +++ b/Proofs/Examples.lean @@ -0,0 +1,105 @@ +/- + Worked examples, proved. The variable byte integer examples + are the MQTT 5.0 specification's own table (section 2.1.4). + The packet examples are hand built from the specification + text, one for each packet type in this slice, plus the + rejections this slice promises. The same packets run + through the command line tool in the test harness, where + they are checked byte by byte a second time. + + The examples are stated on the reading side. The printer's + variable byte integer is defined by well founded recursion, + which the kernel will not evaluate here; the round trip + theorem covers the printer instead. +-/ + +import Mqtt + +namespace Mqtt.Examples + +open Mqtt + +/-! ## The variable byte integer table (spec section 2.1.4) -/ + +theorem vbi_zero : decVBI [0] = some (0, []) := by decide + +theorem vbi_127 : decVBI [127] = some (127, []) := by decide + +theorem vbi_128 : decVBI [128, 1] = some (128, []) := by decide + +theorem vbi_16383 : decVBI [255, 127] = some (16383, []) := by decide + +theorem vbi_16384 : decVBI [128, 128, 1] = some (16384, []) := by decide + +theorem vbi_2097151 : decVBI [255, 255, 127] = some (2097151, []) := by + decide + +theorem vbi_2097152 : decVBI [128, 128, 128, 1] = some (2097152, []) := by + decide + +theorem vbi_max : decVBI [255, 255, 255, 127] = some (268435455, []) := by + decide + +/-- A continuation bit on the fourth byte rejects: the value + would need a fifth byte. -/ +theorem vbi_five_bytes : decVBI [255, 255, 255, 255] = none := by decide + +/-- The pinned reading: a non minimal encoding within four + bytes is accepted. Here 0 carried in two bytes. -/ +theorem vbi_non_minimal : decVBI [128, 0] = some (0, []) := by decide + +/-- The decoder returns the rest of the stream untouched. -/ +theorem vbi_rest : decVBI [128, 1, 99] = some (128, [99]) := by decide + +/-! ## One packet of each type -/ + +theorem parse_pingreq : parse [192, 0] = some .pingreq := by decide + +theorem parse_pingresp : parse [208, 0] = some .pingresp := by decide + +/-- A DISCONNECT with no body is a normal disconnection. -/ +theorem parse_disconnect_empty : + parse [224, 0] = some (.disconnect none) := by decide + +/-- A DISCONNECT body of one byte is a reason code with an + empty property block. It is legal. -/ +theorem parse_disconnect_reason : + parse [224, 1, 0] = some (.disconnect (some (0, []))) := by decide + +theorem parse_publish_qos0 : + parse [48, 6, 0, 1, 97, 0, 1, 2] + = some (.publish ⟨false, 0, false, ['a'], none, [], [1, 2]⟩) := by + decide + +theorem parse_publish_qos1 : + parse [50, 6, 0, 1, 97, 0, 1, 0] + = some (.publish ⟨false, 1, false, ['a'], some 1, [], []⟩) := by + decide + +theorem parse_subscribe : + parse [130, 7, 0, 1, 0, 0, 1, 97, 0] + = some (.subscribe 1 [] [(['a'], ⟨0, false, false, 0⟩)]) := by + decide + +theorem parse_suback : + parse [144, 4, 0, 1, 0, 0] = some (.suback 1 [] [0]) := by decide + +theorem parse_connect : + parse [16, 14, 0, 4, 77, 81, 84, 84, 5, 2, 0, 0, 0, 0, 1, 120] + = some (.connect ⟨true, 0, [], ['x'], none, none, none⟩) := by + decide + +/-! ## Rejections -/ + +/-- A PINGREQ with a body rejects: its remaining length must + be 0. -/ +theorem parse_pingreq_body : parse [192, 1, 0] = none := by decide + +/-- An empty PUBLISH topic rejects. -/ +theorem parse_publish_empty_topic : parse [48, 2, 0, 0] = none := by + decide + +/-- A packet type outside this slice rejects, here type 2. -/ +theorem parse_wrong_type : parse [32, 0] = none := by decide + +end Mqtt.Examples diff --git a/Proofs/RoundTrip.lean b/Proofs/RoundTrip.lean new file mode 100644 index 0000000..c3fcadc --- /dev/null +++ b/Proofs/RoundTrip.lean @@ -0,0 +1,1221 @@ +/- + The round trip proofs for the MQTT packet codec: reading what + the printer wrote gives the packet back. + + The main claim is `Mqtt.Proofs.parse_print`: for a well + formed packet `p`, `parse (print p) = some p`. It is built + from one lemma per field reader, each in the shape "reading + the printed field, with any bytes after it left in place, + gives the field and leaves the bytes after it". Property + blocks and filter lists read to the end of their bytes, so + their lemmas are stated on the printed bytes exactly. +-/ + +import Mqtt +import Proofs.Utf8 + +namespace Mqtt.Proofs + +open Mqtt + +/-- A number below 256 written as a byte reads back as itself. -/ +theorem toNat_toUInt8 {k : Nat} (h : k < 256) : k.toUInt8.toNat = k := + Mqtt.Utf8.Proofs.toNat_toUInt8 h + +/-! ## The byte readers on writings -/ + +/-- A big endian writing reads back: at every width, the number + written is the number read, and the bytes after the writing + are left alone. -/ +theorem readNat_writeBE : ∀ (k n : Nat) (rest : List UInt8), + n < 256 ^ k → readNat k (writeBE k n ++ rest) = some (n, rest) := by + intro k + induction k with + | zero => + intro n rest hn + rw [Nat.pow_zero] at hn + have hn0 : n = 0 := by omega + rw [hn0] + rfl + | succ k ih => + intro n rest hn + have hP : 0 < 256 ^ k := Nat.pow_pos (by decide) + have hlt : n / 256 ^ k < 256 := by + rw [Nat.pow_succ] at hn + exact Nat.div_lt_of_lt_mul hn + have hd : ((n / 256 ^ k) % 256).toUInt8.toNat = n / 256 ^ k := by + have h1 : ((n / 256 ^ k) % 256).toUInt8.toNat = (n / 256 ^ k) % 256 := + UInt8.toNat_ofNat_of_lt (Nat.mod_lt _ (by decide : 0 < 256)) + rw [h1, Nat.mod_eq_of_lt hlt] + rw [writeBE_succ, List.cons_append, readNat_succ_cons, + ih (n % 256 ^ k) rest (Nat.mod_lt _ hP), hd] + simp only [Option.map_some, Option.some.injEq, Prod.mk.injEq] + constructor + · rw [Nat.mul_comm]; exact Nat.div_add_mod _ _ + · trivial + +/-- A byte run reads back whole: taking the front of a list that + starts with the run gives the run, and leaves the rest. -/ +theorem readBytes_append : ∀ (n : Nat) (bs rest : List UInt8), + bs.length = n → readBytes n (bs ++ rest) = some (bs, rest) := by + intro n bs rest h + unfold readBytes + rw [if_pos (by simp [List.length_append, h] : (bs ++ rest).length ≥ n), + ← h, List.take_left, List.drop_left] + +/-! ## The variable byte integer -/ + +/-- A variable byte integer writing is never empty. -/ +theorem printVBI_pos : ∀ (n : Nat), 0 < (printVBI n).length := by + intro n + rw [printVBI_def] + by_cases h : n < 128 + · rw [if_pos h]; simp + · rw [if_neg h]; simp + +/-- Reading a printed variable byte integer, with the counting + form of the reader: with at most `k + 1` bytes to spend and + a value that fits in `k + 1` groups, the reader returns the + accumulated value and leaves the bytes after the writing. + Induction on `k`: a value below 128 is one byte, and a + larger value is its low group, marked as continued, in + front of the writing of the rest of the value. -/ +theorem decVBIGo_printVBI : ∀ (k : Nat) (n acc mult : Nat) (rest : List UInt8), + n < 128 ^ (k + 1) → + decVBIGo (k + 1) acc mult (printVBI n ++ rest) = some (acc + mult * n, rest) := by + intro k + induction k with + | zero => + intro n acc mult rest hn + rw [Nat.pow_one] at hn + rw [printVBI_def, if_pos hn] + show decVBIGo 1 acc mult (n.toUInt8 :: rest) = some (acc + mult * n, rest) + rw [decVBIGo, if_pos (by rw [toNat_toUInt8 (by omega : n < 256)]; exact hn), + toNat_toUInt8 (by omega : n < 256)] + | succ k ih => + intro n acc mult rest hn + by_cases h1 : n < 128 + · rw [printVBI_def, if_pos h1] + show decVBIGo (k + 2) acc mult (n.toUInt8 :: rest) = some (acc + mult * n, rest) + rw [decVBIGo, if_pos (by rw [toNat_toUInt8 (by omega : n < 256)]; exact h1), + toNat_toUInt8 (by omega : n < 256)] + · have hmod : n % 128 < 128 := Nat.mod_lt _ (by decide) + rw [printVBI_def, if_neg h1] + show decVBIGo (k + 2) acc mult + ((128 + n % 128).toUInt8 :: (printVBI (n / 128) ++ rest)) = + some (acc + mult * n, rest) + rw [decVBIGo, toNat_toUInt8 (by omega : 128 + n % 128 < 256), + if_neg (by omega : ¬ (128 + n % 128 < 128)), + if_neg (by omega : ¬ k + 2 ≤ 1), Nat.add_sub_cancel_left] + show decVBIGo (k + 1) (acc + mult * (n % 128)) (mult * 128) + (printVBI (n / 128) ++ rest) = some (acc + mult * n, rest) + have hdiv : n / 128 < 128 ^ (k + 1) := by + rw [Nat.pow_succ] at hn + omega + rw [ih (n / 128) (acc + mult * (n % 128)) (mult * 128) rest hdiv] + have key : acc + mult * (n % 128) + mult * 128 * (n / 128) = acc + mult * n := by + have h := Nat.mod_add_div n 128 + have h3 : mult * (n % 128) + mult * 128 * (n / 128) = mult * n := by + rw [Nat.mul_assoc, ← Nat.left_distrib, h] + omega + rw [key] + +/-- Reading a printed variable byte integer gives the number + back: any number below 2^28, the most four bytes carry. -/ +theorem decVBI_printVBI (n : Nat) (rest : List UInt8) (hn : n < 268435456) : + decVBI (printVBI n ++ rest) = some (n, rest) := by + have e : (128 : Nat) ^ (3 + 1) = 268435456 := by decide + rw [← e] at hn + have h := decVBIGo_printVBI 3 n 0 1 rest hn + simpa [decVBI] using h + +/-! ## Step lemmas + + The readers written with `do` notation are unfolded one step + at a time through these equations, each proved by `rfl`, so + the proofs below can rewrite one field at a time. -/ + +/-- One step of the string reader, stated for rewriting. -/ +theorem readStr_step (bs : List UInt8) : + readStr bs = (readNat 2 bs).bind fun (len, r1) => + (readBytes len r1).bind fun (chunk, r2) => + ((Utf8.decode chunk).bind checkChars).bind fun s => some (s, r2) := rfl + +/-- One step of the binary reader, stated for rewriting. -/ +theorem readBin_step (bs : List UInt8) : + readBin bs = (readNat 2 bs).bind fun (len, r1) => readBytes len r1 := rfl + +/-- One step of the string pair value reader, stated for + rewriting. -/ +theorem readPropVal_pair_step (bs : List UInt8) : + readPropVal .utf8Pair bs = (readStr bs).bind fun (k, r1) => + (readStr r1).bind fun (v, r2) => some (.utf8Pair k v, r2) := rfl + +/-- One step of the property reader, stated for rewriting. -/ +theorem readEntry_step (s : PropSet) (seen : List Nat) (bs : List UInt8) : + readEntry s seen bs = (decVBI bs).bind fun (id, r1) => + if (allowedOf s).contains id && (repeatableIn s id || !seen.contains id) then + match propTypeOf id with + | none => none + | some t => (readPropVal t r1).map fun (v, r2) => (⟨id, v⟩, r2) + else none := rfl + +/-- One step of the property block reader, stated for + rewriting. -/ +theorem readProps_step (s : PropSet) (bs : List UInt8) : + readProps s bs = (decVBI bs).bind fun (len, r1) => + (readBytes len r1).bind fun (seg, r2) => + (readEntries s seg).bind fun ps => some (ps, r2) := rfl + +/-! ## Strings and binary data -/ + +/-- The null character check passes on a well formed string. -/ +theorem hasNul_false {s : List Char} (h : '\u0000' ∉ s) : hasNul s = false := by + simp only [hasNul, List.any_eq_false] + intro c hc hcc + have hceq : c = '\u0000' := of_decide_eq_true hcc + subst hceq + exact h hc + +/-- The character check passes on a well formed string. -/ +theorem checkChars_of_wf {s : List Char} (h : StrWF s) : checkChars s = some s := by + simp [checkChars, hasNul_false h.1] + +/-- A printed string field reads back: the string, with the + bytes after the field left in place. -/ +theorem readStr_printStr (s : List Char) (rest : List UInt8) (h : StrWF s) : + readStr (printStr s ++ rest) = some (s, rest) := by + have hlen : (Utf8.encode s).length < 256 ^ 2 := by + have h2 := h.2 + have e : (256 : Nat) ^ 2 = 65536 := by decide + rw [e] + omega + rw [readStr_step, printStr, List.append_assoc, readNat_writeBE 2 _ _ hlen] + simp only [Option.bind_some] + rw [readBytes_append _ _ _ rfl] + simp only [Option.bind_some] + rw [Mqtt.Utf8.Proofs.decode_encode] + simp only [Option.bind_some] + rw [checkChars_of_wf h] + simp only [Option.bind_some] + +/-- A printed binary field reads back: the bytes, with the + bytes after the field left in place. -/ +theorem readBin_printBin (bs : List UInt8) (rest : List UInt8) (h : BinWF bs) : + readBin (printBin bs ++ rest) = some (bs, rest) := by + have hlen : bs.length < 256 ^ 2 := by + have h2 : bs.length ≤ 65535 := h + have e : (256 : Nat) ^ 2 = 65536 := by decide + rw [e] + omega + rw [readBin_step, printBin, List.append_assoc, readNat_writeBE 2 _ _ hlen] + simp only [Option.bind_some] + rw [readBytes_append _ _ _ rfl] + +/-! ## Properties -/ + +/-- An identifier with a table entry is below 2^28. -/ +theorem propTypeOf_id_lt {id : Nat} {t : PropType} + (h : propTypeOf id = some t) : id < 268435456 := by + unfold propTypeOf at h + split at h <;> simp_all <;> omega + +/-- A printed property value reads back, at the type the table + gives it. -/ +theorem readPropVal_printPropVal (v : PropVal) (rest : List UInt8) (h : ValWF v) : + readPropVal (valType v) (printPropVal v ++ rest) = some (v, rest) := by + cases v with + | byte n => + have hn : n < 256 := h + simp only [valType, printPropVal, readPropVal] + rw [List.cons_append, List.nil_append, readNat_succ_cons, + show readNat 0 rest = some (0, rest) from rfl, Option.map_some, + Option.map_some, toNat_toUInt8 hn] + simp + | twoByte n => + simp only [valType, printPropVal, readPropVal] + rw [readNat_writeBE 2 n rest (by + have e : (256 : Nat) ^ 2 = 65536 := by decide + rw [e]; exact h)] + rfl + | fourByte n => + simp only [valType, printPropVal, readPropVal] + rw [readNat_writeBE 4 n rest (by + have e : (256 : Nat) ^ 4 = 4294967296 := by decide + rw [e]; exact h)] + rfl + | varByte n => + simp only [valType, printPropVal, readPropVal] + rw [decVBI_printVBI n rest h] + rfl + | utf8 s => + simp only [valType, printPropVal, readPropVal] + rw [readStr_printStr s rest h] + rfl + | utf8Pair k v => + obtain ⟨hk, hv⟩ := h + show readPropVal .utf8Pair ((printStr k ++ printStr v) ++ rest) + = some (.utf8Pair k v, rest) + rw [readPropVal_pair_step, List.append_assoc, readStr_printStr k _ hk] + simp only [Option.bind_some] + rw [readStr_printStr v rest hv] + simp only [Option.bind_some] + | binary bs => + simp only [valType, printPropVal, readPropVal] + rw [readBin_printBin bs rest h] + rfl + +/-- A printed property reads back, when the property stands in + the block it is read for: its identifier is allowed there, + its value matches the table's type, the value is well + formed, and the block's repeat rule is respected. -/ +theorem readEntry_printProperty (s : PropSet) (seen : List Nat) (p : Property) + (rest : List UInt8) + (hid : p.id ∈ allowedOf s) (hty : propTypeOf p.id = some (valType p.val)) + (hval : ValWF p.val) + (hrep : repeatableIn s p.id = true ∨ p.id ∉ seen) : + readEntry s seen (printProperty p ++ rest) = some (p, rest) := by + have hc : (allowedOf s).contains p.id = true := List.contains_iff_mem.mpr hid + have hr : (repeatableIn s p.id || !seen.contains p.id) = true := by + cases hrep with + | inl h => rw [h]; rfl + | inr h => + have h2 : seen.contains p.id = false := by + cases hseen : seen.contains p.id with + | false => rfl + | true => exact absurd (List.contains_iff_mem.mp hseen) h + rw [h2] + cases repeatableIn s p.id <;> rfl + rw [readEntry_step, printProperty, List.append_assoc, + decVBI_printVBI p.id _ (propTypeOf_id_lt hty)] + simp only [Option.bind_some] + rw [if_pos (by rw [hc, hr]; rfl), hty] + simp only [] + rw [readPropVal_printPropVal p.val rest hval] + rfl + +/-- A printed property list reads back whole, when the list is + well formed for its block: the reader spends one fuel per + property and each property takes at least a byte, so the + list's own length is fuel enough. -/ +theorem readEntriesGo_printPropsList : ∀ (fuel : Nat) (s : PropSet) + (seen : List Nat) (ps : List Property), + ps.length ≤ fuel → PropsWF s seen ps → + readEntriesGo fuel s seen (printPropsList ps) = some (ps, []) := by + intro fuel + induction fuel with + | zero => + intro s seen ps hlen _ + have hps : ps = [] := by + cases ps with + | nil => rfl + | cons p ps' => simp at hlen + rw [hps] + rfl + | succ fuel ih => + intro s seen ps hlen hwf + cases ps with + | nil => rfl + | cons p ps' => + have hne : ¬ (printProperty p ++ printPropsList ps').isEmpty := by + have h1 : 0 < (printVBI p.id).length := printVBI_pos p.id + intro hcon + rw [List.isEmpty_iff] at hcon + have h3 : printProperty p = [] := (List.append_eq_nil_iff.mp hcon).1 + rw [printProperty] at h3 + have h4 : printVBI p.id = [] := (List.append_eq_nil_iff.mp h3).1 + rw [h4] at h1 + exact absurd h1 (by decide) + obtain ⟨hid, hty, hval, hrep, htail⟩ := hwf + rw [List.length_cons] at hlen + show readEntriesGo (fuel + 1) s seen (printPropsList (p :: ps')) = _ + rw [printPropsList, readEntriesGo, if_neg hne, + readEntry_printProperty s seen p (printPropsList ps') hid hty hval hrep] + simp only [] + rw [ih s (p.id :: seen) ps' (by omega) htail] + +/-- A property list is never longer than its printing: each + property takes at least the byte of its identifier. -/ +theorem propsList_length_le (ps : List Property) : + ps.length ≤ (printPropsList ps).length := by + induction ps with + | nil => simp [printPropsList] + | cons p ps' ih => + have h1 : 0 < (printVBI p.id).length := printVBI_pos p.id + simp only [printPropsList, printProperty, List.length_cons, + List.length_append] + omega + +/-- A whole printed property block's insides read back. -/ +theorem readEntries_printPropsList (s : PropSet) (ps : List Property) + (h : PropsWF s [] ps) : readEntries s (printPropsList ps) = some ps := by + unfold readEntries + rw [readEntriesGo_printPropsList (printPropsList ps).length s [] ps + (propsList_length_le ps) h] + +/-- A printed property block reads back: the properties, with + the bytes after the block left in place. -/ +theorem readProps_printProps (s : PropSet) (ps : List Property) + (rest : List UInt8) (h : PropsBlockWF s ps) : + readProps s (printProps ps ++ rest) = some (ps, rest) := by + obtain ⟨hwf, hlen⟩ := h + rw [readProps_step, printProps, List.append_assoc, decVBI_printVBI _ _ hlen] + simp only [Option.bind_some] + rw [readBytes_append _ _ _ rfl] + simp only [Option.bind_some] + rw [readEntries_printPropsList s ps hwf] + simp only [Option.bind_some] + +/-! ## Topic names and flag bits -/ + +/-- An `any` test for one character fails when the character + does not stand in the text. -/ +theorem any_eq_false_of_not_mem {s : List Char} {c : Char} (h : c ∉ s) : + s.any (fun x => decide (x = c)) = false := by + simp only [List.any_eq_false] + intro x hx hxc + have hxcq : x = c := of_decide_eq_true hxc + subst hxcq + exact h hx + +/-- The topic name check passes on a well formed topic name. -/ +theorem checkTopic_of_wf {s : List Char} (h : TopicWF s) : checkTopic s = some s := by + obtain ⟨hstr, hne, hp, hh⟩ := h + have e1 : s.isEmpty = false := by + cases s with + | nil => exact absurd rfl hne + | cons a t => rfl + have e2 : s.any (fun c => decide (c = '+')) = false := + any_eq_false_of_not_mem hp + have e3 : s.any (fun c => decide (c = '#')) = false := + any_eq_false_of_not_mem hh + unfold checkTopic + rw [e1, e2, e3] + exact if_neg (by decide) + +/-- An `if` on a boolean, in the flags builders' shape, is the + bit as a number times the place value. -/ +theorem if_bool_mul (b : Bool) (x : Nat) : + (if b then x else 0) = (if b then 1 else 0) * x := by + cases b <;> simp + +/-- The bits of a number built as `q + a * 4 + b * 8 + rh * 16`, + with `a` and `b` bits and `q` and `rh` at most 2: the fields + an options byte carries. Pure arithmetic. -/ +theorem optsByte_fields (q rh a b : Nat) (hq : q ≤ 2) (hr : rh ≤ 2) + (ha : a ≤ 1) (hb : b ≤ 1) : + readOptsByte (q + a * 4 + b * 8 + rh * 16) = some ⟨q, a = 1, b = 1, rh⟩ := by + unfold readOptsByte + rw [if_pos ⟨by omega, by omega, by omega⟩] + simp only [Option.some.injEq, SubOpts.mk.injEq] + refine ⟨by omega, ?_, ?_, by omega⟩ + · rw [show (q + a * 4 + b * 8 + rh * 16) / 4 % 2 = a by omega] + · rw [show (q + a * 4 + b * 8 + rh * 16) / 8 % 2 = b by omega] + +/-- A printed options byte reads back as the options. -/ +theorem readOptsByte_printOptsByte (o : SubOpts) (h : OptsWF o) : + readOptsByte (printOptsByte o).toNat = some o := by + obtain ⟨q, nl, rap, rh⟩ := o + have hq : q ≤ 2 := h.1 + have hr : rh ≤ 2 := h.2 + have ha : (if nl then (1 : Nat) else 0) ≤ 1 := by cases nl <;> decide + have hb : (if rap then (1 : Nat) else 0) ≤ 1 := by cases rap <;> decide + have hbound : q + (if nl then 1 else 0) * 4 + (if rap then 1 else 0) * 8 + + rh * 16 < 256 := by omega + have hsum : (printOptsByte ⟨q, nl, rap, rh⟩).toNat + = q + (if nl then 1 else 0) * 4 + (if rap then 1 else 0) * 8 + rh * 16 := by + show ((q + (if nl then 4 else 0) + (if rap then 8 else 0) + rh * 16).toUInt8).toNat = _ + rw [if_bool_mul nl 4, if_bool_mul rap 8, toNat_toUInt8 hbound] + rw [hsum, optsByte_fields q rh _ _ hq hr ha hb] + cases nl <;> cases rap <;> rfl + +/-! ## SUBSCRIBE filters -/ + +/-- A printed filter list is at least as long as the list: each + filter takes at least the byte of its options. -/ +theorem printFilters_length_ge : ∀ (fs : List (List Char × SubOpts)), + fs.length ≤ (printFilters fs).length := by + intro fs + induction fs with + | nil => simp [printFilters] + | cons f fs' ih => + have h1 : 0 < (printFilter f).length := by + simp only [printFilter, List.length_append, List.length_cons, + List.length_nil] + omega + simp only [printFilters, List.length_cons, List.length_append] + omega + +/-- A printed filter list reads back whole, when its members + are well formed: the reader spends one fuel per filter and + each filter takes at least a byte, so the list's own length + is fuel enough. -/ +theorem readFiltersGo_printFilters : ∀ (fuel : Nat) + (fs : List (List Char × SubOpts)), + fs.length ≤ fuel → FiltersWF fs → + readFiltersGo fuel (printFilters fs) = some (fs, []) := by + intro fuel + induction fuel with + | zero => + intro fs hlen _ + have hfs : fs = [] := by + cases fs with + | nil => rfl + | cons f fs' => simp at hlen + rw [hfs] + rfl + | succ fuel ih => + intro fs hlen hwf + cases fs with + | nil => rfl + | cons fr fs' => + obtain ⟨f, o⟩ := fr + obtain ⟨hf, ho, htail⟩ := hwf + have hne : ¬ (printFilter (f, o) ++ printFilters fs').isEmpty := by + have h1 : 0 < (printFilter (f, o)).length := by + simp only [printFilter, List.length_append, List.length_cons, + List.length_nil] + omega + intro hcon + rw [List.isEmpty_iff] at hcon + have h3 : printFilter (f, o) = [] := (List.append_eq_nil_iff.mp hcon).1 + rw [h3] at h1 + exact absurd h1 (by decide) + rw [List.length_cons] at hlen + show readFiltersGo (fuel + 1) (printFilters ((f, o) :: fs')) = _ + rw [printFilters, readFiltersGo, if_neg hne, printFilter, + List.append_assoc, readStr_printStr f _ hf] + rw [List.cons_append, List.nil_append] + simp only [] + rw [readOptsByte_printOptsByte o ho] + simp only [] + rw [ih fs' (by omega) htail] + +/-! ## Packet bodies -/ + +/-- One step of the single byte reader, stated for rewriting. -/ +theorem readByte_cons (b : UInt8) (bs : List UInt8) : + readByte (b :: bs) = some (b.toNat, bs) := rfl + +/-- The bits of a PUBLISH flags nibble built from a packet's + fields: the QoS sits at bits 2 and 1, DUP at bit 3, RETAIN + at bit 0. -/ +theorem publish_bits (dup retain : Bool) (qos : Nat) (hq : qos ≤ 2) : + ((if dup then 8 else 0) + qos * 2 + (if retain then 1 else 0)) / 2 % 4 = qos + ∧ flagBit ((if dup then 8 else 0) + qos * 2 + (if retain then 1 else 0)) 3 = dup + ∧ flagBit ((if dup then 8 else 0) + qos * 2 + (if retain then 1 else 0)) 0 + = retain := by + have e1 : (if dup then (8 : Nat) else 0) = (if dup then 1 else 0) * 8 := + if_bool_mul dup 8 + have e2 : (if retain then (1 : Nat) else 0) = (if retain then 1 else 0) * 1 := + if_bool_mul retain 1 + have ha : (if dup then (1 : Nat) else 0) ≤ 1 := by cases dup <;> decide + have hb : (if retain then (1 : Nat) else 0) ≤ 1 := by cases retain <;> decide + rw [e1, e2] + refine ⟨by omega, ?_, ?_⟩ + · unfold flagBit + rw [show (2 : Nat) ^ 3 = 8 by decide, + show ((if dup then 1 else 0) * 8 + qos * 2 + (if retain then 1 else 0) * 1) + / 8 % 2 = (if dup then 1 else 0) by omega] + cases dup <;> rfl + · unfold flagBit + rw [show (2 : Nat) ^ 0 = 1 by decide, + show ((if dup then 1 else 0) * 8 + qos * 2 + (if retain then 1 else 0) * 1) + / 1 % 2 = (if retain then 1 else 0) by omega] + cases retain <;> rfl + +/-- The properties reader on exactly the printed bytes. -/ +theorem readProps_printProps_exact (s : PropSet) (ps : List Property) + (h : PropsBlockWF s ps) : readProps s (printProps ps) = some (ps, []) := by + have h2 := readProps_printProps s ps [] h + rwa [List.append_nil] at h2 + +/-- The SUBSCRIBE body reader as one bind chain; the form the + round trip proof rewrites through. -/ +theorem readSubscribeBody_step (seg : List UInt8) : + readSubscribeBody seg = + (readNat 2 seg).bind fun (id, r1) => + if id ≠ 0 then + (readProps .subscribe r1).bind fun (props, r2) => + (readFiltersGo r2.length r2).bind fun (fs, r3) => + if r3.isEmpty && !fs.isEmpty then some (.subscribe id props fs) + else none + else none := rfl + +/-- A printed SUBSCRIBE body reads back as the packet. -/ +theorem readSubscribeBody_printSubscribeBody (id : Nat) (ps : List Property) + (fs : List (List Char × SubOpts)) (hid : 1 ≤ id ∧ id < 65536) + (hps : PropsBlockWF .subscribe ps) (hfs : fs ≠ [] ∧ FiltersWF fs) : + readSubscribeBody (printSubscribeBody id ps fs) = some (.subscribe id ps fs) := by + rw [readSubscribeBody_step, + show printSubscribeBody id ps fs + = writeBE 2 id ++ (printProps ps ++ printFilters fs) from rfl, + readNat_writeBE 2 id _ (by omega)] + simp only [Option.bind_some] + rw [if_pos (by omega : id ≠ 0), readProps_printProps .subscribe ps _ hps] + simp only [Option.bind_some] + rw [readFiltersGo_printFilters (printFilters fs).length fs + (printFilters_length_ge fs) hfs.2] + simp only [Option.bind_some] + have h2 : fs.isEmpty = false := by + cases fs with + | nil => exact absurd rfl hfs.1 + | cons a t => rfl + rw [if_pos (by rw [h2]; rfl : ([].isEmpty && !fs.isEmpty) = true)] + +/-- Reason codes written as bytes read back as themselves. -/ +theorem map_toUInt8_toNat (rs : List Nat) (h : ∀ r ∈ rs, r < 256) : + (rs.map Nat.toUInt8).map UInt8.toNat = rs := by + induction rs with + | nil => rfl + | cons r rs' ih => + simp only [List.map_cons] + rw [toNat_toUInt8 (h r (by simp)), ih (fun x hx => h x (by simp [hx]))] + +/-- The SUBACK body reader as one bind chain. -/ +theorem readSubackBody_step (seg : List UInt8) : + readSubackBody seg = + (readNat 2 seg).bind fun (id, r1) => + if id ≠ 0 then + (readProps .suback r1).bind fun (props, r2) => + if !r2.isEmpty then some (.suback id props (r2.map UInt8.toNat)) + else none + else none := rfl + +/-- A printed SUBACK body reads back as the packet. -/ +theorem readSubackBody_printSubackBody (id : Nat) (ps : List Property) + (rs : List Nat) (hid : 1 ≤ id ∧ id < 65536) + (hps : PropsBlockWF .suback ps) (hrs : rs ≠ [] ∧ ∀ r ∈ rs, r < 256) : + readSubackBody (printSubackBody id ps rs) = some (.suback id ps rs) := by + rw [readSubackBody_step, + show printSubackBody id ps rs + = writeBE 2 id ++ (printProps ps ++ rs.map Nat.toUInt8) from rfl, + readNat_writeBE 2 id _ (by omega)] + simp only [Option.bind_some] + rw [if_pos (by omega : id ≠ 0), readProps_printProps .suback ps _ hps] + simp only [Option.bind_some] + have h2 : (rs.map Nat.toUInt8).isEmpty = false := by + cases rs with + | nil => exact absurd rfl hrs.1 + | cons a t => rfl + rw [if_pos (by rw [h2]; rfl : (!(rs.map Nat.toUInt8).isEmpty) = true), + map_toUInt8_toNat rs hrs.2] + +/-- A printed DISCONNECT body reads back as the packet. -/ +theorem readDisconnectBody_print (x : Option (Nat × List Property)) + (h : match x with + | none => True + | some (rc, ps) => rc < 256 ∧ PropsBlockWF PropSet.disconnect ps) : + readDisconnectBody (bodyOf (Packet.disconnect x)) + = some (Packet.disconnect x) := by + cases x with + | none => rfl + | some rp => + obtain ⟨rc, ps⟩ := rp + obtain ⟨hrc, hps⟩ := h + show readDisconnectBody ([rc.toUInt8] ++ printProps ps) + = some (Packet.disconnect (some (rc, ps))) + rw [show [rc.toUInt8] ++ printProps ps = rc.toUInt8 :: printProps ps from rfl] + have hpos : 0 < (printProps ps).length := by + show 0 < (printVBI (printPropsList ps).length + ++ printPropsList ps).length + rw [List.length_append] + have h1 := printVBI_pos (printPropsList ps).length + omega + have hne : ¬ ((printProps ps).isEmpty = true) := by + intro hcon + rw [List.isEmpty_iff] at hcon + have hz : (printProps ps).length = 0 := congrArg List.length hcon + omega + show (if (printProps ps).isEmpty + then some (Packet.disconnect (some ((rc.toUInt8).toNat, []))) + else (readProps PropSet.disconnect (printProps ps)).bind + fun (props, r2) => + if r2.isEmpty + then some (Packet.disconnect (some ((rc.toUInt8).toNat, props))) + else none) = some (Packet.disconnect (some (rc, ps))) + rw [if_neg hne] + simp only [readProps_printProps_exact PropSet.disconnect ps hps, + Option.bind_some] + rw [if_pos (by decide : List.isEmpty [] = true), toNat_toUInt8 hrc] + +/-- The facts about a well formed connect flags byte: it + fits in a byte, the reserved bit is clear, and every field + the reader recovers from the byte (the will QoS, the will + retain, the will flag, the username and password flags, + the clean start) is the field that was written. -/ +theorem connectFlags_facts (c : Connect) (h : ConnectWF c) : + (connectFlags c).toUInt8.toNat = connectFlags c + ∧ connectFlags c % 2 = 0 + ∧ (connectFlags c / 8) % 4 + = (match c.will with | some w => w.qos | none => 0) + ∧ flagBit (connectFlags c) 7 = c.username.isSome + ∧ flagBit (connectFlags c) 6 = c.password.isSome + ∧ flagBit (connectFlags c) 5 + = (match c.will with | some w => w.retain | none => false) + ∧ flagBit (connectFlags c) 2 = c.will.isSome + ∧ flagBit (connectFlags c) 1 = c.cleanStart := by + have e1 : (if c.username.isSome then (128 : Nat) else 0) + = (if c.username.isSome then 1 else 0) * 128 := if_bool_mul _ _ + have e2 : (if c.password.isSome then (64 : Nat) else 0) + = (if c.password.isSome then 1 else 0) * 64 := if_bool_mul _ _ + have e3 : (if c.cleanStart then (2 : Nat) else 0) + = (if c.cleanStart then 1 else 0) * 2 := if_bool_mul _ _ + have hub : (if c.username.isSome then (1 : Nat) else 0) ≤ 1 := by + cases h : c.username.isSome <;> decide + have hpb : (if c.password.isSome then (1 : Nat) else 0) ≤ 1 := by + cases h : c.password.isSome <;> decide + have hcs : (if c.cleanStart then (1 : Nat) else 0) ≤ 1 := by + cases h : c.cleanStart <;> decide + cases hw : c.will with + | none => + have hf : connectFlags c + = (if c.username.isSome then 1 else 0) * 128 + + (if c.password.isSome then 1 else 0) * 64 + + (if c.cleanStart then 1 else 0) * 2 := by + unfold connectFlags + rw [e1, e2, e3, hw] + dsimp only + omega + refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ + · rw [hf] + exact toNat_toUInt8 (by omega) + · rw [hf]; omega + · show (connectFlags c / 8) % 4 = 0 + rw [hf]; omega + · rw [hf] + unfold flagBit + rw [show (2 : Nat) ^ 7 = 128 by decide, + show ((if c.username.isSome then 1 else 0) * 128 + + (if c.password.isSome then 1 else 0) * 64 + + (if c.cleanStart then 1 else 0) * 2) / 128 % 2 + = (if c.username.isSome then 1 else 0) by omega] + cases h : c.username.isSome <;> rfl + · rw [hf] + unfold flagBit + rw [show (2 : Nat) ^ 6 = 64 by decide, + show ((if c.username.isSome then 1 else 0) * 128 + + (if c.password.isSome then 1 else 0) * 64 + + (if c.cleanStart then 1 else 0) * 2) / 64 % 2 + = (if c.password.isSome then 1 else 0) by omega] + cases h : c.password.isSome <;> rfl + · show flagBit (connectFlags c) 5 = false + rw [hf] + unfold flagBit + rw [show (2 : Nat) ^ 5 = 32 by decide, + show ((if c.username.isSome then 1 else 0) * 128 + + (if c.password.isSome then 1 else 0) * 64 + + (if c.cleanStart then 1 else 0) * 2) / 32 % 2 = 0 by omega] + rfl + · show flagBit (connectFlags c) 2 = false + rw [hf] + unfold flagBit + rw [show (2 : Nat) ^ 2 = 4 by decide, + show ((if c.username.isSome then 1 else 0) * 128 + + (if c.password.isSome then 1 else 0) * 64 + + (if c.cleanStart then 1 else 0) * 2) / 4 % 2 = 0 by omega] + rfl + · rw [hf] + unfold flagBit + rw [show (2 : Nat) ^ 1 = 2 by decide, + show ((if c.username.isSome then 1 else 0) * 128 + + (if c.password.isSome then 1 else 0) * 64 + + (if c.cleanStart then 1 else 0) * 2) / 2 % 2 + = (if c.cleanStart then 1 else 0) by omega] + cases h : c.cleanStart <;> rfl + | some w => + have hwf : WillWF w := h.2.2.2.1 w hw + have hwq : w.qos ≤ 2 := hwf.1 + have hrb : (if w.retain then (1 : Nat) else 0) ≤ 1 := by + cases w.retain <;> decide + have e4 : (if w.retain then (32 : Nat) else 0) + = (if w.retain then 1 else 0) * 32 := if_bool_mul _ _ + have hf : connectFlags c + = (if c.username.isSome then 1 else 0) * 128 + + (if c.password.isSome then 1 else 0) * 64 + + ((if w.retain then 1 else 0) * 32 + w.qos * 8 + 4) + + (if c.cleanStart then 1 else 0) * 2 := by + unfold connectFlags + rw [e1, e2, e3, hw] + dsimp only + rw [e4] + refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ + · rw [hf] + exact toNat_toUInt8 (by omega) + · rw [hf]; omega + · show (connectFlags c / 8) % 4 = w.qos + rw [hf]; omega + · rw [hf] + unfold flagBit + rw [show (2 : Nat) ^ 7 = 128 by decide, + show ((if c.username.isSome then 1 else 0) * 128 + + (if c.password.isSome then 1 else 0) * 64 + + ((if w.retain then 1 else 0) * 32 + w.qos * 8 + 4) + + (if c.cleanStart then 1 else 0) * 2) / 128 % 2 + = (if c.username.isSome then 1 else 0) by omega] + cases h : c.username.isSome <;> rfl + · rw [hf] + unfold flagBit + rw [show (2 : Nat) ^ 6 = 64 by decide, + show ((if c.username.isSome then 1 else 0) * 128 + + (if c.password.isSome then 1 else 0) * 64 + + ((if w.retain then 1 else 0) * 32 + w.qos * 8 + 4) + + (if c.cleanStart then 1 else 0) * 2) / 64 % 2 + = (if c.password.isSome then 1 else 0) by omega] + cases h : c.password.isSome <;> rfl + · show flagBit (connectFlags c) 5 = w.retain + rw [hf] + unfold flagBit + rw [show (2 : Nat) ^ 5 = 32 by decide, + show ((if c.username.isSome then 1 else 0) * 128 + + (if c.password.isSome then 1 else 0) * 64 + + ((if w.retain then 1 else 0) * 32 + w.qos * 8 + 4) + + (if c.cleanStart then 1 else 0) * 2) / 32 % 2 + = (if w.retain then 1 else 0) by omega] + cases w.retain <;> rfl + · show flagBit (connectFlags c) 2 = true + rw [hf] + unfold flagBit + rw [show (2 : Nat) ^ 2 = 4 by decide, + show ((if c.username.isSome then 1 else 0) * 128 + + (if c.password.isSome then 1 else 0) * 64 + + ((if w.retain then 1 else 0) * 32 + w.qos * 8 + 4) + + (if c.cleanStart then 1 else 0) * 2) / 4 % 2 = 1 by omega] + rfl + · rw [hf] + unfold flagBit + rw [show (2 : Nat) ^ 1 = 2 by decide, + show ((if c.username.isSome then 1 else 0) * 128 + + (if c.password.isSome then 1 else 0) * 64 + + ((if w.retain then 1 else 0) * 32 + w.qos * 8 + 4) + + (if c.cleanStart then 1 else 0) * 2) / 2 % 2 + = (if c.cleanStart then 1 else 0) by omega] + cases h : c.cleanStart <;> rfl + +/-- The CONNECT tail: the optional username and password + fields read back as themselves, and nothing is left + over, so the assembled packet is the one that was + printed. The three flag values are the reader's own + recoveries from the flags byte; the hypotheses tie them + to the fields. -/ +theorem readOptFields (u : Option (List Char)) (p : Option (List UInt8)) + (hu : ∀ s, u = some s → StrWF s) (hp : ∀ b, p = some b → BinWF b) + (cs : Bool) (ka : Nat) (props : List Property) (cid : List Char) + (will : Option Will) (f7 f6 f1 : Bool) + (h7 : f7 = u.isSome) (h6 : f6 = p.isSome) (h1 : f1 = cs) : + ((readOptStrField f7 (printOptStr u ++ printOptBin p)).bind + fun (u', r8) => + (readOptBinField f6 r8).bind fun (p', r9) => + (if r9.isEmpty + then some (⟨f1, ka, props, cid, will, u', p'⟩ : Connect) else none) + : Option Connect) + = some (⟨cs, ka, props, cid, will, u, p⟩ : Connect) := by + subst h7 + subst h6 + subst h1 + cases u with + | none => + rw [show printOptStr none = [] from rfl, List.nil_append] + unfold readOptStrField + rw [if_neg (by decide : ¬ (Option.isSome none = true))] + simp only [Option.bind_some] + cases p with + | none => + rw [show printOptBin none = [] from rfl] + unfold readOptBinField + rw [if_neg (by decide : ¬ (Option.isSome none = true))] + simp only [Option.bind_some] + rw [if_pos (by decide : List.isEmpty [] = true)] + | some b => + rw [show printOptBin (some b) = printBin b from rfl] + unfold readOptBinField + rw [if_pos (by rfl : Option.isSome (some b) = true), + ← List.append_nil (printBin b), readBin_printBin b [] (hp b rfl)] + simp only [Option.map_some, Option.bind_some] + rw [if_pos (by decide : List.isEmpty [] = true)] + | some s => + rw [show printOptStr (some s) = printStr s from rfl] + unfold readOptStrField + rw [if_pos (by rfl : Option.isSome (some s) = true), + readStr_printStr s _ (hu s rfl)] + simp only [Option.map_some, Option.bind_some] + cases p with + | none => + rw [show printOptBin none = [] from rfl] + unfold readOptBinField + rw [if_neg (by decide : ¬ (Option.isSome none = true))] + simp only [Option.bind_some] + rw [if_pos (by decide : List.isEmpty [] = true)] + | some b => + rw [show printOptBin (some b) = printBin b from rfl] + unfold readOptBinField + rw [if_pos (by rfl : Option.isSome (some b) = true), + ← List.append_nil (printBin b), readBin_printBin b [] (hp b rfl)] + simp only [Option.map_some, Option.bind_some] + rw [if_pos (by decide : List.isEmpty [] = true)] + +/-- A printed CONNECT body reads back as the packet. -/ +theorem readConnectBody_printConnectBody (c : Connect) (h : ConnectWF c) : + readConnectBody (printConnectBody c) = some c := by + obtain ⟨hka, hprops, hcid, hwill, huser, hpass⟩ := h + obtain ⟨hf1, hf2, hf3, hf4, hf5, hf6, hf7, hf8⟩ := connectFlags_facts c + ⟨hka, hprops, hcid, hwill, huser, hpass⟩ + have hfin : ∀ (w : Option Will), w = c.will → + (⟨c.cleanStart, c.keepAlive, c.props, c.clientId, w, c.username, + c.password⟩ : Connect) = c := by + intro w hw + subst hw + rfl + have hproto : StrWF ['M', 'Q', 'T', 'T'] := by + constructor + · decide + · decide + unfold readConnectBody + rw [show printConnectBody c + = printStr ['M', 'Q', 'T', 'T'] ++ ([5, (connectFlags c).toUInt8] + ++ (writeBE 2 c.keepAlive ++ (printProps c.props + ++ (printStr c.clientId ++ (printWillPart c.will + ++ (printOptStr c.username ++ printOptBin c.password)))))) + from rfl, + readStr_printStr _ _ hproto] + simp only [Option.bind_some] + rw [if_pos trivial] + simp only [List.cons_append, List.nil_append] + rw [readByte_cons] + simp only [Option.bind_some] + rw [if_pos (by decide : (5 : UInt8).toNat = 5), readByte_cons] + simp only [Option.bind_some] + rw [hf1, if_pos hf2] + by_cases hwn : c.will = none + · have hf3' : (connectFlags c / 8) % 4 = 0 := by rw [hf3, hwn] + have hf7' : flagBit (connectFlags c) 2 = false := by simp [hf7, hwn] + rw [if_pos (by rw [hf3']; omega : (connectFlags c / 8) % 4 ≠ 3), + readNat_writeBE 2 c.keepAlive _ (by omega)] + simp only [Option.bind_some] + rw [readProps_printProps .connect c.props _ hprops] + simp only [Option.bind_some] + rw [readStr_printStr c.clientId _ hcid] + simp only [Option.bind_some] + rw [hwn, show printWillPart none = [] from rfl, List.nil_append] + unfold readWillPart + rw [if_neg (by rw [hf7']; decide : ¬ (flagBit (connectFlags c) 2 = true))] + simp only [Option.bind_some] + rw [readOptFields c.username c.password huser hpass c.cleanStart + c.keepAlive c.props c.clientId none (flagBit (connectFlags c) 7) + (flagBit (connectFlags c) 6) (flagBit (connectFlags c) 1) hf4 hf5 hf8] + exact congrArg Option.some (hfin none hwn.symm) + · obtain ⟨w, hw⟩ : ∃ w, c.will = some w := by + cases hw2 : c.will with + | none => exact absurd hw2 hwn + | some w => exact ⟨w, rfl⟩ + obtain ⟨wq, wr, wps, wt, wpay⟩ := w + have hwf : WillWF ⟨wq, wr, wps, wt, wpay⟩ := hwill _ hw + have hwq : wq ≤ 2 := hwf.1 + have hwprops : PropsBlockWF .will wps := hwf.2.1 + have hwtopic : TopicWF wt := hwf.2.2.1 + have hwpay : BinWF wpay := hwf.2.2.2 + have hf3' : (connectFlags c / 8) % 4 = wq := by rw [hf3, hw] + have hf6' : flagBit (connectFlags c) 5 = wr := by rw [hf6, hw] + have hf7' : flagBit (connectFlags c) 2 = true := by simp [hf7, hw] + rw [if_pos (by rw [hf3']; omega : (connectFlags c / 8) % 4 ≠ 3), + readNat_writeBE 2 c.keepAlive _ (by omega)] + simp only [Option.bind_some] + rw [readProps_printProps .connect c.props _ hprops] + simp only [Option.bind_some] + rw [readStr_printStr c.clientId _ hcid] + simp only [Option.bind_some] + rw [hw, show printWillPart (some ⟨wq, wr, wps, wt, wpay⟩) + = printProps wps ++ (printStr wt ++ printBin wpay) from rfl] + unfold readWillPart + rw [if_pos hf7', List.append_assoc, readProps_printProps .will wps _ hwprops] + simp only [Option.bind_some] + rw [List.append_assoc, readStr_printStr wt _ hwtopic.1] + simp only [Option.bind_some] + rw [checkTopic_of_wf hwtopic] + simp only [Option.bind_some] + rw [readBin_printBin wpay _ hwpay] + simp only [Option.bind_some] + rw [readOptFields c.username c.password huser hpass c.cleanStart + c.keepAlive c.props c.clientId + (some ⟨(connectFlags c / 8) % 4, flagBit (connectFlags c) 5, wps, wt, + wpay⟩) + (flagBit (connectFlags c) 7) (flagBit (connectFlags c) 6) + (flagBit (connectFlags c) 1) hf4 hf5 hf8] + rw [hf3', hf6'] + exact congrArg Option.some (hfin _ hw.symm) + +/-- The packet identifier step at QoS 0 reads nothing. -/ +theorem readPacketId_qos0 (flags : Nat) (r : List UInt8) + (h : (flags / 2) % 4 = 0) : + readPacketId flags r = some (none, r) := by + unfold readPacketId + rw [if_pos h] + +/-- The packet identifier step at QoS 1 and 2 reads a printed + nonzero identifier. -/ +theorem readPacketId_print (flags : Nat) (i : Nat) (rest : List UInt8) + (h : (flags / 2) % 4 ≠ 0) (hi : 1 ≤ i ∧ i < 65536) : + readPacketId flags (printIdOpt (some i) ++ rest) = some (some i, rest) := by + unfold readPacketId + rw [if_neg h, show printIdOpt (some i) = writeBE 2 i from rfl, + readNat_writeBE 2 i _ (by omega)] + simp only [Option.bind_some] + rw [if_pos (by omega : i ≠ 0)] + +/-- A printed PUBLISH body reads back as the packet, when the + flags word carries the packet's own QoS, DUP and RETAIN. -/ +theorem readPublishBody_printPublishBody (flags : Nat) (pub : Publish) + (hq : (flags / 2) % 4 = pub.qos) (h3 : flagBit flags 3 = pub.dup) + (h0 : flagBit flags 0 = pub.retain) (h : PublishWF pub) : + readPublishBody flags (printPublishBody pub) = some pub := by + obtain ⟨dup, qos, retain, topic, pid, props, payload⟩ := pub + obtain ⟨hqos, htopic, hidf, hnone, hprops⟩ := h + have htopic' : TopicWF topic := htopic + have hidf' : ∀ id, pid = some id → + 1 ≤ id ∧ id < 65536 ∧ (qos = 1 ∨ qos = 2) := hidf + have hnone' : pid = none → qos = 0 := hnone + have hprops' : PropsBlockWF .publish props := hprops + have hq' : (flags / 2) % 4 = qos := hq + have h3' : flagBit flags 3 = dup := h3 + have h0' : flagBit flags 0 = retain := h0 + unfold readPublishBody + rw [show printPublishBody ⟨dup, qos, retain, topic, pid, props, payload⟩ + = printStr topic ++ (printIdOpt pid ++ (printProps props ++ payload)) + from rfl, + readStr_printStr topic _ htopic'.1] + simp only [Option.bind_some] + rw [checkTopic_of_wf htopic'] + simp only [Option.bind_some] + by_cases hq0 : qos = 0 + · have hpid : pid = none := by + cases hp : pid with + | none => rfl + | some i => + have h2 := hidf' i hp + omega + rw [hpid, show printIdOpt none = [] from rfl, List.nil_append, + readPacketId_qos0 flags _ (by omega)] + simp only [Option.bind_some] + rw [readProps_printProps .publish props payload hprops'] + simp only [Option.bind_some] + rw [h3', h0', hq'] + · have hpid : ∃ i, pid = some i ∧ 1 ≤ i ∧ i < 65536 := by + cases hp : pid with + | none => exact absurd (hnone' hp) hq0 + | some i => + have h2 := hidf' i hp + exact ⟨i, rfl, h2.1, h2.2.1⟩ + obtain ⟨i, hi, hi1, hi2⟩ := hpid + rw [hi, readPacketId_print flags i _ (by omega) ⟨hi1, hi2⟩] + simp only [Option.bind_some] + rw [readProps_printProps .publish props payload hprops'] + simp only [Option.bind_some] + rw [h3', h0', hq'] + +/-! ## Whole packets -/ + +/-- A well formed PUBLISH header byte value fits in a + byte: the fixed part is 0x30 and the flags part is at + most 8 + 4 + 1. -/ +theorem publishHeader_bound (pub : Publish) (h : PublishWF pub) : + publishHeader pub < 256 := by + have hA : (if pub.dup then (8 : Nat) else 0) ≤ 8 := by + cases pub.dup <;> decide + have hB : (if pub.retain then (1 : Nat) else 0) ≤ 1 := by + cases pub.retain <;> decide + have hqos : pub.qos ≤ 2 := h.1 + unfold publishHeader + omega + +/-- The body dispatcher on a printed CONNECT body. -/ +theorem parseBody_connect (c : Connect) (h : ConnectWF c) : + parseBody 1 0 (printConnectBody c) = some (.connect c) := by + show (readConnectBody (printConnectBody c)).map Packet.connect + = some (.connect c) + rw [readConnectBody_printConnectBody c h] + simp only [Option.map_some] + +/-- The body dispatcher on a printed PUBLISH body. -/ +theorem parseBody_publish (pub : Publish) (h : PublishWF pub) : + parseBody 3 (publishHeader pub % 16) (printPublishBody pub) + = some (.publish pub) := by + have hqos : pub.qos ≤ 2 := h.1 + have hA : (if pub.dup then (8 : Nat) else 0) ≤ 8 := by + cases pub.dup <;> decide + have hB : (if pub.retain then (1 : Nat) else 0) ≤ 1 := by + cases pub.retain <;> decide + have hE : (if pub.dup then 8 else 0) + pub.qos * 2 + + (if pub.retain then 1 else 0) ≤ 15 := by omega + have hphv : publishHeader pub + = 48 + ((if pub.dup then 8 else 0) + pub.qos * 2 + + (if pub.retain then 1 else 0)) := by + unfold publishHeader + omega + have hmod : publishHeader pub % 16 + = (if pub.dup then 8 else 0) + pub.qos * 2 + + (if pub.retain then 1 else 0) := by omega + have hb := publish_bits pub.dup pub.retain pub.qos hqos + show (if (publishHeader pub % 16 / 2) % 4 = 3 then none + else (readPublishBody (publishHeader pub % 16) (printPublishBody pub)).map + Packet.publish) = some (.publish pub) + rw [hmod, if_neg (by rw [hb.1]; omega : + ¬ ((if pub.dup then 8 else 0) + pub.qos * 2 + + (if pub.retain then 1 else 0)) / 2 % 4 = 3), + readPublishBody_printPublishBody _ pub hb.1 hb.2.1 hb.2.2 h] + simp only [Option.map_some] + +/-- The body dispatcher on a printed SUBSCRIBE body. -/ +theorem parseBody_subscribe (id : Nat) (ps : List Property) + (fs : List (List Char × SubOpts)) (hid : 1 ≤ id ∧ id < 65536) + (hps : PropsBlockWF .subscribe ps) (hfs : fs ≠ [] ∧ FiltersWF fs) : + parseBody 8 2 (printSubscribeBody id ps fs) + = some (.subscribe id ps fs) := by + show (if (2 : Nat) = 2 then readSubscribeBody (printSubscribeBody id ps fs) + else none) = some (.subscribe id ps fs) + rw [if_pos rfl, readSubscribeBody_printSubscribeBody id ps fs hid hps hfs] + +/-- The body dispatcher on a printed SUBACK body. -/ +theorem parseBody_suback (id : Nat) (ps : List Property) (rs : List Nat) + (hid : 1 ≤ id ∧ id < 65536) (hps : PropsBlockWF .suback ps) + (hrs : rs ≠ [] ∧ ∀ r ∈ rs, r < 256) : + parseBody 9 0 (printSubackBody id ps rs) = some (.suback id ps rs) := by + show (if (0 : Nat) = 0 then readSubackBody (printSubackBody id ps rs) + else none) = some (.suback id ps rs) + rw [if_pos rfl, readSubackBody_printSubackBody id ps rs hid hps hrs] + +/-- The body dispatcher on an empty PINGREQ body: a closed + computation. -/ +theorem parseBody_pingreq : parseBody 12 0 [] = some .pingreq := by decide + +/-- The body dispatcher on an empty PINGRESP body. -/ +theorem parseBody_pingresp : parseBody 13 0 [] = some .pingresp := by decide + +/-- The body dispatcher on an empty DISCONNECT body. -/ +theorem parseBody_disconnect_none : + parseBody 14 0 (bodyOf (.disconnect none)) = some (.disconnect none) := by + show (if (0 : Nat) = 0 then readDisconnectBody (bodyOf (.disconnect none)) + else none) = some (.disconnect none) + rw [if_pos rfl, readDisconnectBody_print none trivial] + +/-- The body dispatcher on a printed DISCONNECT body with a + reason code and properties. -/ +theorem parseBody_disconnect_some (rc : Nat) (ps : List Property) + (h : rc < 256 ∧ PropsBlockWF PropSet.disconnect ps) : + parseBody 14 0 (bodyOf (.disconnect (some (rc, ps)))) + = some (.disconnect (some (rc, ps))) := by + show (if (0 : Nat) = 0 + then readDisconnectBody (bodyOf (.disconnect (some (rc, ps)))) + else none) = some (.disconnect (some (rc, ps))) + rw [if_pos rfl, readDisconnectBody_print (some (rc, ps)) h] + +/-- One packet at the head of a stream: a printed packet + followed by any bytes parses to the packet and leaves + the rest of the stream untouched. -/ +theorem parsePacket_print (p : Packet) (rest : List UInt8) (h : PacketWF p) : + parsePacket (print p ++ rest) = some (p, rest) := by + obtain ⟨hfields, hlen⟩ := h + have hnorm : print p ++ rest + = headerOf p :: (printVBI (bodyOf p).length ++ (bodyOf p ++ rest)) := by + show (headerOf p :: (printVBI (bodyOf p).length ++ bodyOf p)) ++ rest + = headerOf p :: (printVBI (bodyOf p).length ++ (bodyOf p ++ rest)) + rw [List.cons_append, List.append_assoc] + rw [hnorm] + show ((decVBI (printVBI (bodyOf p).length ++ (bodyOf p ++ rest))).bind + fun (len, r1) => + (readBytes len r1).bind fun (seg, r2) => + (parseBody ((headerOf p).toNat / 16) ((headerOf p).toNat % 16) seg).bind + fun q => some (q, r2)) = some (p, rest) + rw [decVBI_printVBI _ _ hlen] + simp only [Option.bind_some] + rw [readBytes_append _ _ _ rfl] + simp only [Option.bind_some] + cases p with + | connect c => + have hfc : ConnectWF c := hfields + have e1 : (headerOf (.connect c)).toNat / 16 = 1 := by + rw [show headerOf (.connect c) = (0x10 : UInt8) from rfl]; decide + have e2 : (headerOf (.connect c)).toNat % 16 = 0 := by + rw [show headerOf (.connect c) = (0x10 : UInt8) from rfl]; decide + have e3 : bodyOf (.connect c) = printConnectBody c := rfl + rw [e1, e2, e3] + simp only [parseBody_connect c hfc, Option.bind_some] + | publish pub => + have hfp : PublishWF pub := hfields + have hph : (publishHeader pub).toUInt8.toNat = publishHeader pub := + toNat_toUInt8 (publishHeader_bound pub hfp) + have hqos : pub.qos ≤ 2 := hfp.1 + have hA : (if pub.dup then (8 : Nat) else 0) ≤ 8 := by + cases pub.dup <;> decide + have hB : (if pub.retain then (1 : Nat) else 0) ≤ 1 := by + cases pub.retain <;> decide + have hphv : publishHeader pub + = 48 + ((if pub.dup then 8 else 0) + pub.qos * 2 + + (if pub.retain then 1 else 0)) := by + unfold publishHeader + omega + have hE : (if pub.dup then 8 else 0) + pub.qos * 2 + + (if pub.retain then 1 else 0) ≤ 15 := by omega + have hdiv : publishHeader pub / 16 = 3 := by omega + have e3 : bodyOf (.publish pub) = printPublishBody pub := rfl + have e0 : headerOf (.publish pub) = (publishHeader pub).toUInt8 := rfl + rw [e3, e0, hph, hdiv] + simp only [parseBody_publish pub hfp, Option.bind_some] + | subscribe id ps fs => + have hid : 1 ≤ id ∧ id < 65536 := ⟨hfields.1, hfields.2.1⟩ + have hps : PropsBlockWF .subscribe ps := hfields.2.2.1 + have hfs : fs ≠ [] ∧ FiltersWF fs := ⟨hfields.2.2.2.1, hfields.2.2.2.2⟩ + have e1 : (headerOf (.subscribe id ps fs)).toNat / 16 = 8 := by + rw [show headerOf (.subscribe id ps fs) = (0x82 : UInt8) from rfl]; decide + have e2 : (headerOf (.subscribe id ps fs)).toNat % 16 = 2 := by + rw [show headerOf (.subscribe id ps fs) = (0x82 : UInt8) from rfl]; decide + have e3 : bodyOf (.subscribe id ps fs) = printSubscribeBody id ps fs := rfl + rw [e1, e2, e3] + simp only [parseBody_subscribe id ps fs hid hps hfs, Option.bind_some] + | suback id ps rs => + have hid : 1 ≤ id ∧ id < 65536 := ⟨hfields.1, hfields.2.1⟩ + have hps : PropsBlockWF .suback ps := hfields.2.2.1 + have hrs : rs ≠ [] ∧ ∀ r ∈ rs, r < 256 := + ⟨hfields.2.2.2.1, hfields.2.2.2.2⟩ + have e1 : (headerOf (.suback id ps rs)).toNat / 16 = 9 := by + rw [show headerOf (.suback id ps rs) = (0x90 : UInt8) from rfl]; decide + have e2 : (headerOf (.suback id ps rs)).toNat % 16 = 0 := by + rw [show headerOf (.suback id ps rs) = (0x90 : UInt8) from rfl]; decide + have e3 : bodyOf (.suback id ps rs) = printSubackBody id ps rs := rfl + rw [e1, e2, e3] + simp only [parseBody_suback id ps rs hid hps hrs, Option.bind_some] + | pingreq => + have e1 : (headerOf .pingreq).toNat / 16 = 12 := by decide + have e2 : (headerOf .pingreq).toNat % 16 = 0 := by decide + have e3 : bodyOf .pingreq = [] := rfl + rw [e1, e2, e3] + simp only [parseBody_pingreq, Option.bind_some] + | pingresp => + have e1 : (headerOf .pingresp).toNat / 16 = 13 := by decide + have e2 : (headerOf .pingresp).toNat % 16 = 0 := by decide + have e3 : bodyOf .pingresp = [] := rfl + rw [e1, e2, e3] + simp only [parseBody_pingresp, Option.bind_some] + | disconnect x => + have e1 : (headerOf (.disconnect x)).toNat / 16 = 14 := by + rw [show headerOf (.disconnect x) = (0xE0 : UInt8) from rfl]; decide + have e2 : (headerOf (.disconnect x)).toNat % 16 = 0 := by + rw [show headerOf (.disconnect x) = (0xE0 : UInt8) from rfl]; decide + rw [e1, e2] + cases x with + | none => + simp only [parseBody_disconnect_none, Option.bind_some] + | some rp => + obtain ⟨rc, ps⟩ := rp + have h2 : rc < 256 ∧ PropsBlockWF PropSet.disconnect ps := hfields + simp only [parseBody_disconnect_some rc ps h2, Option.bind_some] + +/-- The main round trip claim: a well formed packet, + printed and parsed back on its own, is the same + packet. -/ +theorem parse_print (p : Packet) (h : PacketWF p) : parse (print p) = some p := by + unfold parse + have h2 := parsePacket_print p [] h + rw [List.append_nil] at h2 + simp only [h2] + +end Mqtt.Proofs diff --git a/Proofs/Utf8.lean b/Proofs/Utf8.lean new file mode 100644 index 0000000..6fe01b2 --- /dev/null +++ b/Proofs/Utf8.lean @@ -0,0 +1,148 @@ +/- + Proofs for the strict UTF-8 codec in Mqtt/Utf8.lean: the one + claim the packet round trip needs is that decoding the + encoding of any text gives the text back. + + Carried in with the codec from the Proven Commons jws slice, + where this proof was first written, and adapted to the + renamed namespace. +-/ + +import Mqtt.Utf8 + +namespace Mqtt.Utf8.Proofs + +open Mqtt.Utf8 + +/-- A number below 256 written as a byte reads back as itself. -/ +theorem toNat_toUInt8 {k : Nat} (h : k < 256) : k.toUInt8.toNat = k := by + simp; omega + +/-- A character value is below 110000, and no character value + lies in the surrogate gap D800 to DFFF: the Unicode scalar + range every `Char` lives in. -/ +theorem char_bounds (c : Char) : + c.toNat < 0x110000 ∧ ¬ (0xD800 ≤ c.toNat ∧ c.toNat < 0xE000) := by + have h := c.valid + show c.val.toNat < 0x110000 ∧ ¬ (0xD800 ≤ c.val.toNat ∧ c.val.toNat < 0xE000) + rcases h with h | ⟨h1, h2⟩ + · exact ⟨by omega, by omega⟩ + · exact ⟨by omega, by omega⟩ + +/-- A byte whose value is known to be a continuation byte reads + back as its payload value. -/ +theorem contVal_of_toNat {b : UInt8} {k : Nat} (h : b.toNat = 0x80 + k) (hk : k < 64) : + contVal b = some k := by + unfold contVal + rw [h, if_pos ⟨by omega, by omega⟩, Nat.add_sub_cancel_left] + +/-- One step of the decoder on a plain byte. -/ +theorem decode_one (b : UInt8) (bs : List UInt8) (hb : b.toNat < 0x80) : + decode (b :: bs) = (decode bs).map (Char.ofNat b.toNat :: ·) := by + cases bs with + | nil => rw [decode.eq_3, if_pos hb] + | cons b1 bs' => rw [decode.eq_2, if_pos hb] + +/-- One step of the decoder on a two byte form. -/ +theorem decode_two (b b1 : UInt8) (bs : List UInt8) (v : Nat) + (hb : 0xC2 ≤ b.toNat ∧ b.toNat < 0xE0) (hv : contVal b1 = some v) : + decode (b :: b1 :: bs) = + (decode bs).map (Char.ofNat ((b.toNat - 0xC0) * 64 + v) :: ·) := by + rw [decode.eq_2, if_neg (by omega : ¬ b.toNat < 0x80), + if_neg (by omega : ¬ b.toNat < 0xC2), if_pos (by omega : b.toNat < 0xE0), hv] + +/-- One step of the decoder on a three byte form. -/ +theorem decode_three (b b1 b2 : UInt8) (bs : List UInt8) (v1 v2 : Nat) + (hb : 0xE0 ≤ b.toNat ∧ b.toNat < 0xF0) + (hside : (b.toNat = 0xE0 → 0x20 ≤ v1) ∧ (b.toNat = 0xED → v1 < 0x20)) + (hv1 : contVal b1 = some v1) (hv2 : contVal b2 = some v2) : + decode (b :: b1 :: b2 :: bs) = + (decode bs).map (Char.ofNat ((b.toNat - 0xE0) * 4096 + v1 * 64 + v2) :: ·) := by + rw [decode.eq_2, if_neg (by omega : ¬ b.toNat < 0x80), + if_neg (by omega : ¬ b.toNat < 0xC2), if_neg (by omega : ¬ b.toNat < 0xE0), + if_pos (by omega : b.toNat < 0xF0)] + dsimp only + rw [hv1, hv2] + dsimp only + rw [if_pos hside] + +/-- One step of the decoder on a four byte form. -/ +theorem decode_four (b b1 b2 b3 : UInt8) (bs : List UInt8) (v1 v2 v3 : Nat) + (hb : 0xF0 ≤ b.toNat ∧ b.toNat < 0xF5) + (hside : (b.toNat = 0xF0 → 0x10 ≤ v1) ∧ (b.toNat = 0xF4 → v1 < 0x10)) + (hv1 : contVal b1 = some v1) (hv2 : contVal b2 = some v2) + (hv3 : contVal b3 = some v3) : + decode (b :: b1 :: b2 :: b3 :: bs) = + (decode bs).map + (Char.ofNat ((b.toNat - 0xF0) * 262144 + v1 * 4096 + v2 * 64 + v3) :: ·) := by + rw [decode.eq_2, if_neg (by omega : ¬ b.toNat < 0x80), + if_neg (by omega : ¬ b.toNat < 0xC2), if_neg (by omega : ¬ b.toNat < 0xE0), + if_neg (by omega : ¬ b.toNat < 0xF0), if_pos (by omega : b.toNat < 0xF5)] + dsimp only + rw [hv1, hv2, hv3] + dsimp only + rw [if_pos hside] + +/-- Decoding one encoded character in front of any bytes decodes + the character and then the bytes. The four cases are the + four lengths; each one applies the step lemma for its + length, checks the side conditions with arithmetic, and + rebuilds the character value. -/ +theorem decode_append_char (c : Char) (bs : List UInt8) : + decode (encodeChar c ++ bs) = (decode bs).map (c :: ·) := by + obtain ⟨hmax, hnsur⟩ := char_bounds c + by_cases h1 : c.toNat < 0x80 + · rw [encodeChar, if_pos h1, List.cons_append, List.nil_append, + decode_one _ _ (by rw [toNat_toUInt8 (by omega)]; exact h1), + toNat_toUInt8 (by omega), Char.ofNat_toNat] + · rw [encodeChar, if_neg h1] + by_cases h2 : c.toNat < 0x800 + · have hlead : (0xC0 + c.toNat / 64).toUInt8.toNat = 0xC0 + c.toNat / 64 := + toNat_toUInt8 (by omega) + rw [if_pos h2, List.cons_append, List.cons_append, List.nil_append, + decode_two _ _ _ _ ⟨by omega, by omega⟩ + (contVal_of_toNat (toNat_toUInt8 (by omega)) (Nat.mod_lt _ (by decide))), + hlead, + show (0xC0 + c.toNat / 64 - 0xC0) * 64 + c.toNat % 64 = c.toNat by omega, + Char.ofNat_toNat] + · rw [if_neg h2] + by_cases h3 : c.toNat < 0x10000 + · have hlead : (0xE0 + c.toNat / 4096).toUInt8.toNat = 0xE0 + c.toNat / 4096 := + toNat_toUInt8 (by omega) + rw [if_pos h3, List.cons_append, List.cons_append, List.cons_append, + List.nil_append, + decode_three _ _ _ _ _ _ ⟨by omega, by omega⟩ + ⟨fun hb => by rw [hlead] at hb; omega, + fun hb => by rw [hlead] at hb; omega⟩ + (contVal_of_toNat (toNat_toUInt8 (by omega)) (Nat.mod_lt _ (by decide))) + (contVal_of_toNat (toNat_toUInt8 (by omega)) (Nat.mod_lt _ (by decide))), + hlead, + show (0xE0 + c.toNat / 4096 - 0xE0) * 4096 + (c.toNat / 64) % 64 * 64 + + c.toNat % 64 = c.toNat by omega, + Char.ofNat_toNat] + · have hlead : (0xF0 + c.toNat / 262144).toUInt8.toNat = 0xF0 + c.toNat / 262144 := + toNat_toUInt8 (by omega) + rw [if_neg h3, List.cons_append, List.cons_append, List.cons_append, + List.cons_append, List.nil_append, + decode_four _ _ _ _ _ _ _ _ ⟨by omega, by omega⟩ + ⟨fun hb => by rw [hlead] at hb; omega, + fun hb => by rw [hlead] at hb; omega⟩ + (contVal_of_toNat (toNat_toUInt8 (by omega)) (Nat.mod_lt _ (by decide))) + (contVal_of_toNat (toNat_toUInt8 (by omega)) (Nat.mod_lt _ (by decide))) + (contVal_of_toNat (toNat_toUInt8 (by omega)) (Nat.mod_lt _ (by decide))), + hlead, + show (0xF0 + c.toNat / 262144 - 0xF0) * 262144 + (c.toNat / 4096) % 64 * 4096 + + (c.toNat / 64) % 64 * 64 + c.toNat % 64 = c.toNat by omega, + Char.ofNat_toNat] + +/-- Decoding the encoding of any text gives the text back. -/ +theorem decode_encode : ∀ cs : List Char, decode (encode cs) = some cs := by + intro cs + induction cs with + | nil => rfl + | cons c cs ih => + show decode (encodeChar c ++ encode cs) = some (c :: cs) + rw [decode_append_char, ih] + rfl + +end Mqtt.Utf8.Proofs diff --git a/README.md b/README.md index 6d3fa52..98b4584 100644 --- a/README.md +++ b/README.md @@ -1,35 +1,66 @@ -# mqtt +# mqtt: an MQTT 5.0 packet reader and printer, with a proved round trip -A Lean parser for MQTT 5.0 packet framing. This is a Proven Commons project: it rebuilds a widely used format in Lean and proves the new code follows its written specification. +An MQTT 5.0 control packet reader and printer in Lean, covering the seven packet types CONNECT, PUBLISH, SUBSCRIBE, SUBACK, PINGREQ, PINGRESP, and DISCONNECT, with their property blocks. The reader reads one packet from the front of a byte list and returns the rest of the input, so a caller can walk a stream of packets. The main claim is proved: parsing what the printer wrote returns the same packet. The tests run the tool against a strict oracle written from the standard and, for the pieces it covers, against the Paho Python library; see `tests/TEST-RESULTS.md` for the counts. -Status: not verified. No code has landed yet. Plan issue 1 holds the first slice, and it is unclaimed. The specification has not been approved by a reviewer, so do not call this verified. +Status: in progress. The specification has not yet been approved by a reviewer apart from its author, and no statement file (`Spec.lean`) has been added by a reviewer, so this is not verified. -## First slice +## What is proved -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. +The definitions are in `Mqtt/Value.lean` (the packet types, the property table, the printer, and the well-formedness rules), `Mqtt/Parse.lean` (the reader), and `Mqtt/Utf8.lean` (a strict UTF-8 codec, carried in from the Proven Commons `jws` slice with its namespace renamed, as the header of that file records). The proofs are in `Proofs/RoundTrip.lean` and `Proofs/Utf8.lean`, and worked examples from the standard are proved in `Proofs/Examples.lean`. -This is distinct from the websocket repo. MQTT can run over websockets as a transport, but this slice is MQTT packets over TCP, not websocket frames. +| Claim | Theorem | +|-------|---------| +| Parsing the printed form of a well formed packet, with more stream bytes after it, gives the packet and those bytes back. | `Mqtt.Proofs.parsePacket_print` | +| Parsing the printed form of a well formed packet on its own gives the packet back. | `Mqtt.Proofs.parse_print` | +| Reading a printed variable byte integer gives the number back, for every value below 2^28. | `Mqtt.Proofs.decVBI_printVBI` | +| Decoding the UTF-8 encoding of any text gives the text back. | `Mqtt.Utf8.Proofs.decode_encode` | -## Main claim +Under those, the field and body steps are proved one by one: big endian numbers, byte cuts, string and binary fields, typed property values, single properties, property lists and whole property blocks, the subscription options byte, topic filter lists, and the body of each of the seven packet types. -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. +A packet is well formed when its numbers fit the widths that carry them, its strings obey the string rules and fit the two byte length prefix, its properties match the property table in type and place with no single use property repeated, its packet identifiers stand where the type requires them and are never 0 there, and its whole body is shorter than 2^28, the largest remaining length a variable byte integer can carry. The full list is in `SPEC.md`. `parse_print` checks against the standard axioms only (`propext`, `Classical.choice`, `Quot.sound`), which a reader can confirm with `#print axioms Mqtt.Proofs.parse_print`, or by running `lake env lean Mqtt/Verify.lean`. -## Test oracles +The command-line tool in `Main.lean` calls these functions directly. -- Eclipse Paho clients. -- The Mosquitto broker test suite. -- MQTT 5.0 specification test material. +## What is not proved -## Score +- That the reader accepts every byte string the standard allows, and rejects every one it forbids. The round trip does not need either, so neither is proved. The oracle differential and the mutation tests check that behaviour instead, and the results file records the outcome. +- Any reading of what a property means. A property is an identifier and a typed value; that a Receive Maximum of 10 asks the peer to hold back after ten packets is broker and session behaviour, and none of it is in this slice. +- Anything about packets outside the seven types, or property identifiers outside the table in `SPEC.md`. Both are rejected, and that rejection is tested, not proved. +- Broker or session behaviour of any kind: connections, subscriptions as state, retained messages, keep alive timing, and what any peer does with a packet. +- The worked examples on the printing side. The examples in `Proofs/Examples.lean` are stated on the reading side, because the printer's variable byte integer is defined by well founded recursion, which the kernel will not evaluate in a `decide` proof here. The round trip theorem covers the printer. +- Reading requests and printing answers in `Main.lean`: splitting lines, and the decimal number reader. The tests cover them, malformed requests included. +- Speed. The code works on lists of bytes, which suits proofs, not large packets. -16 out of 18, first pass score in mission issue 19, the round 4 sheet. Created at the org owner's direction on that sheet, on the judgement that the slice, claim, and oracles are sound and that it duplicates no existing repo. +## What you must trust -## What is not in this slice +- The Lean kernel, which checks the proofs. +- The Lean compiler, with the C compiler and linker shipped with it, and the runtime, which turn the proved definitions into the program that runs. +- Lean's core library, including the compiled code it puts in place of some definitions the proofs reason about. +- The operating system and hardware it runs on. +- The strict oracle in the test harness, written from the MQTT 5.0 standard, and Paho's Python library in the parts of the differential it covers. The results file names the version used, and states plainly which oracles were and were not available. -- A broker. -- Session state. -- Delivery guarantees. +This project has no dependencies beyond Lean itself. -## Layout, when the first slice lands +## Run it -The layout follows the Proven Commons template in the mission repo, under bar/template. Spec.lean holds the statements a reviewer approves. Proofs.lean holds the proofs under the same names. Main.lean holds the command line tool used by the tests. The bar check runs in CI on every change. +Needs Linux and [elan](https://github.com/leanprover/elan). Build, then feed request lines to the tool: + +``` +lake build +echo "parse 192,0" | .lake/build/bin/mqtt +``` + +That request is a PINGREQ, and the answer is `ok:192,0`: the packet read back and reprinted. Bytes the reader rejects, such as a PINGREQ carrying a body (`parse 192,1,0`), answer `none`. A malformed request answers `error`. See `SPEC.md` for the full protocol. + +## Re-check it + +Needs Linux, elan, and Python 3. The test harness uses the Paho library from the virtual environment in the work directory (`venv`) when it is there, and says so in the results file when it is not. + +``` +lake build +grep -rn "sorry" --include="*.lean" Mqtt Proofs Main.lean Mqtt.lean Proofs.lean +lake env lean Mqtt/Verify.lean +python3 tests/run_tests.py +``` + +The grep should print only the one line in `Mqtt/Verify.lean` that explains what a `sorryAx` in its output would mean: there is no `sorry` anywhere. The test script rebuilds the tool, runs the fixed cases, the differential against the strict oracle, the Paho cross-check when the library is importable, and the mutation and rejection cases, and writes the counts to `tests/TEST-RESULTS.md`. diff --git a/SPEC.md b/SPEC.md new file mode 100644 index 0000000..ce1cab6 --- /dev/null +++ b/SPEC.md @@ -0,0 +1,330 @@ +# MQTT packet codec: specification + +This is the specification of the first slice for the `mqtt` +package: MQTT 5.0 control packet framing at the level of bytes, +in Lean, with the round trip proved. The format itself is +defined by the OASIS MQTT Version 5.0 standard; section numbers +below are that standard's. This file states what the slice does +with it, including the points where the standard leaves a +reading open and this slice pins one. + +What the slice is: a reader and a printer for one control +packet of seven types, and a reader that can walk a stream of +packets one at a time. What it is not: a broker, a client, or +any session behaviour. Nothing here opens a connection, keeps +state between packets, acts on a packet's meaning, or checks a +packet against a subscription or a session. + +## The packet on the wire + +A packet is three parts, in order: + +1. One fixed header byte: the packet type in the high four + bits, and type specific flags in the low four bits. +2. The remaining length: a variable byte integer (below) that + counts the bytes of the third part. +3. The body: the variable header and the payload for the type, + exactly as many bytes as the remaining length says. + +The packet types in this slice are CONNECT (1), PUBLISH (3), +SUBSCRIBE (8), SUBACK (9), PINGREQ (12), PINGRESP (13), and +DISCONNECT (14). A fixed header byte whose type nibble is any +other value is rejected in this slice. + +## The variable byte integer + +A variable byte integer (section 2.1.4) carries seven bits per +byte, low groups first. The top bit of a byte is a continuation +mark: it is set on every byte but the last. At most four bytes +are used, so the largest value is 268435455 (2^28 - 1). The +standard's worked table: + +| Value | Bytes | +| --- | --- | +| 0 | 0 | +| 127 | 127 | +| 128 | 128, 1 | +| 16383 | 255, 127 | +| 16384 | 128, 128, 1 | +| 2097151 | 255, 255, 127 | +| 2097152 | 128, 128, 128, 1 | +| 268435455 | 255, 255, 255, 127 | + +The reader rejects a value whose fourth byte still carries a +continuation mark (a fifth byte would be needed), and rejects +a value cut off by the end of the input. + +Pinned reading, non-minimal encodings: a value may be written +with more bytes than it needs, as long as the writing uses at +most four bytes and the value fits. The reader accepts such +encodings. So 0 written as 128, 0 reads as 0. This matches the +behaviour of common libraries, including Paho. The printer +always writes the minimal form, so a packet that arrived with +a non-minimal remaining length is reprinted with the minimal +one. The same rule applies to every variable byte integer in +a packet, including property lengths and variable byte +integer property values. + +## Fixed header flags + +For every type in this slice except PUBLISH, the flags nibble +must be exactly the value the standard fixes (section 2.1.2): +0010 for SUBSCRIBE, and 0000 for CONNECT, SUBACK, PINGREQ, +PINGRESP, and DISCONNECT. Any other nibble is rejected. + +PUBLISH flags carry meaning and are part of the packet value: +the DUP flag at bit 3, the QoS level at bits 2 and 1, and the +RETAIN flag at bit 0. The QoS value 3 is reserved and is +rejected. + +## Strings and binary data + +A UTF-8 string field (section 1.5.4) is a two byte length, +counting bytes, then that many bytes of UTF-8 text. The reader +decodes the bytes with a strict UTF-8 decoder: it rejects +stray continuation bytes, overlong forms, lead bytes above +F4, encodings of the surrogate values D800 to DFFF, values +above 10FFFF, and truncated sequences. It also rejects the +null character U+0000, which the standard forbids in strings. +Nothing else about the text is checked. + +A binary data field (section 1.5.3) is a two byte length, then +that many bytes, with no check on the bytes. + +## Properties + +Most packet types carry a property block (section 2.2.2): a +property length as a variable byte integer, then that many +bytes of properties. Each property is an identifier, written +as a variable byte integer, and a value whose shape is fixed +by the identifier's row in the standard's property table +(Table 2-4). The block must be filled exactly: a property that +runs past the end of the block, and bytes left over inside the +block after the last whole property, are both rejected. + +The table as implemented in this slice: + +| Id | Name | Value type | Blocks it may stand on | +| --- | --- | --- | --- | +| 0x01 | Payload Format Indicator | byte | will, PUBLISH | +| 0x02 | Message Expiry Interval | four byte integer | will, PUBLISH | +| 0x03 | Content Type | UTF-8 string | will, PUBLISH | +| 0x08 | Response Topic | UTF-8 string | will, PUBLISH | +| 0x09 | Correlation Data | binary data | will, PUBLISH | +| 0x0B | Subscription Identifier | variable byte integer | PUBLISH, SUBSCRIBE | +| 0x11 | Session Expiry Interval | four byte integer | CONNECT, DISCONNECT | +| 0x12 | Assigned Client Identifier | UTF-8 string | none in this slice | +| 0x13 | Server Keep Alive | two byte integer | none in this slice | +| 0x15 | Authentication Method | UTF-8 string | CONNECT | +| 0x16 | Authentication Data | binary data | CONNECT | +| 0x17 | Request Problem Information | byte | CONNECT | +| 0x18 | Will Delay Interval | four byte integer | will | +| 0x19 | Request Response Information | byte | CONNECT | +| 0x1A | Response Information | UTF-8 string | none in this slice | +| 0x1C | Server Reference | UTF-8 string | DISCONNECT | +| 0x1F | Reason String | UTF-8 string | SUBACK, DISCONNECT | +| 0x21 | Receive Maximum | two byte integer | CONNECT | +| 0x22 | Topic Alias Maximum | two byte integer | CONNECT | +| 0x23 | Topic Alias | two byte integer | PUBLISH | +| 0x24 | Maximum QoS | byte | none in this slice | +| 0x25 | Retain Available | byte | none in this slice | +| 0x26 | User Property | UTF-8 string pair | CONNECT, will, PUBLISH, SUBSCRIBE, SUBACK, DISCONNECT | +| 0x27 | Maximum Packet Size | four byte integer | CONNECT | +| 0x28 | Wildcard Subscription Available | byte | none in this slice | +| 0x29 | Subscription Identifier Available | byte | none in this slice | +| 0x2A | Shared Subscription Available | byte | none in this slice | + +Rows marked "none in this slice" name properties the standard +assigns to packet types this slice does not read (chiefly +CONNACK). The identifier has a known value type, but it is on +no allowed list here, so the reader rejects it everywhere in +this slice. + +Three property checks reject a packet: + +- An identifier with no row in the table is rejected. +- A property standing on a block whose allowed list does not + include it is rejected. For example, a Subscription + Identifier on a CONNECT packet is rejected. +- A repeated single use property is rejected. Two properties + may repeat: the User Property (0x26) may repeat on any block + that allows it, and the Subscription Identifier (0x0B) may + repeat on PUBLISH, where one message can match several + subscriptions (section 3.3.4). Every other allowed property + may stand at most once in one block. + +## The seven packet types + +### CONNECT (section 3.1) + +The body is: the protocol name as a string field, which must +be exactly the text "MQTT"; one protocol level byte, which +must be 5; one connect flags byte; the keep alive as two +bytes; the CONNECT property block; then the payload. + +The connect flags byte is: username flag at bit 7, password +flag at bit 6, will retain at bit 5, will QoS at bits 4 and 3, +will flag at bit 2, clean start at bit 1, and a reserved bit +at bit 0. The reader rejects a packet whose reserved bit is +set, and rejects a will QoS field of 3. The will QoS and will +retain bits are part of the packet value only when the will +flag is set; when it is clear, the printer writes them as 0. + +The payload is: the client identifier as a string field +(always present, and it may be empty); then, when the will +flag is set, the will property block, the will topic as a +string field, and the will payload as a binary data field; +then the username as a string field when the username flag is +set; then the password as a binary data field when the +password flag is set. The fields stand exactly when the flags +say they stand, and the body must be consumed exactly: bytes +left over, or a field the flags demand but the bytes do not +hold, are rejected. The will topic must pass the topic name +check below, like a PUBLISH topic. + +### PUBLISH (section 3.3) + +The body is: the topic name as a string field; the packet +identifier as two bytes, present exactly when the QoS is 1 or +2 and never present at QoS 0; the PUBLISH property block; +then the payload, which is all the bytes that remain in the +body, and may be empty. + +The topic name must be nonempty and must contain neither +wildcard character, `+` or `#` (section 4.7.1). A packet +identifier, where one stands, must not be 0. + +### SUBSCRIBE (section 3.8) + +The body is: the packet identifier as two bytes, which must +not be 0; the SUBSCRIBE property block; then a list of topic +filters that fills the rest of the body exactly. The list +must be nonempty. Each filter is a filter string as a string +field, then one subscription options byte. A filter string +follows the string rules above; wildcards are allowed in it, +as the standard allows. The reader adds no nonemptiness check +of its own to a single filter string. + +The subscription options byte is: the maximum QoS at bits 0 +and 1, the no local flag at bit 2, the retain as published +flag at bit 3, and the retain handling choice at bits 4 and +5. The reader rejects a byte of 64 or more (the reserved bits +6 and 7 must be clear), a QoS field of 3, and a retain +handling field of 3. + +### SUBACK (section 3.9) + +The body is: the packet identifier as two bytes, which must +not be 0; the SUBACK property block; then the list of reason +codes, one byte each, filling the rest of the body. The list +must be nonempty. Reason code values are not checked beyond +being bytes. + +### PINGREQ (section 3.12) and PINGRESP (section 3.13) + +Both packets have an empty body: the remaining length must be +0, and any body byte is rejected. + +### DISCONNECT (section 3.14) + +Three body forms are legal: + +- A remaining length of 0: a normal disconnection with no + body. +- A remaining length of 1: one reason code byte and no + property block. The standard omits the property length when + the remaining length is 1 (section 3.14.2), so this form is + accepted, and reads as that reason code with an empty + property block. +- A remaining length of 2 or more: one reason code byte, then + a DISCONNECT property block that fills the rest of the body + exactly. + +The printer always writes the second kind of packet with an +explicit property block, so a packet read from the one byte +form is reprinted in the longer form: the packet with reason +code 0 and no properties prints as remaining length 2, reason +0, property length 0. Reason code values are not checked +beyond being bytes. + +## The reader + +The reader reads one packet from the front of a byte list and +returns the packet together with the rest of the input, so a +caller can walk a stream of packets: trailing bytes are not +an error at that level. The whole input form of the reader +adds the check that nothing follows the packet. + +Safety: the reader never reads past the end of its input. It +first cuts the body out by the remaining length, and each +field reader checks its length against the bytes that +actually remain before taking any of them. Any shortfall, at +any point, is a rejection, not a partial read. Each type's +reader must consume its body cut exactly. + +## Well formed values + +The round trip claim holds for well formed packets: the +fields the printer can write exactly. In outline: + +- Every number fits the width that carries it: keep alive and + packet identifiers and two byte property values below + 65536, four byte property values below 2^32, variable byte + integer values and any single property block's printed + length below 2^28, and the whole body below 2^28, the + largest remaining length four bytes can carry. +- Strings obey the string rules and their UTF-8 byte length + fits the two byte length prefix; binary data fields fit the + same prefix. +- Properties match the table in type and in place, and no + single use property repeats in one block. +- CONNECT: the will, when one stands, has QoS at most 2, a + well formed will property block, a topic that passes the + topic name check, and a payload that fits its prefix. +- PUBLISH: QoS at most 2; a topic that passes the topic name + check; a packet identifier standing exactly when the QoS is + 1 or 2, and never 0. +- SUBSCRIBE: a nonzero packet identifier, a nonempty filter + list, and options with QoS and retain handling at most 2. +- SUBACK: a nonzero packet identifier and a nonempty reason + list of byte values. +- DISCONNECT with a body: a reason code below 256 and a well + formed property block. + +## The printer + +The printer writes a packet as the fixed header byte, the +remaining length as a minimal variable byte integer, and the +body in the layouts above. Property blocks are written with a +minimal property length. A packet read by the reader and +printed again is in this canonical form; a packet that +arrived already in canonical form reprints byte for byte. + +## The line protocol + +The command line tool reads one request per line: the +operation and a payload, parted by one space. The payload is +decimal byte numbers parted by commas, with no spaces. A +number is plain decimal: no sign, no leading zeros (the +number 0 itself is written `0`), at most twenty digits. An +empty line gets no answer. A request that breaks these rules +prints `error`, as does an unknown operation. + +The one operation is `parse`. It parses the bytes as exactly +one whole packet and prints `ok:` followed by the bytes of +the canonical reprint, comma parted, when the bytes are one +packet this slice reads. It prints `none` when the bytes are +well formed as a request but are not one packet this slice +reads. The empty payload is the empty byte list and answers +`none`. + +Example: the request `parse 192,0` is a PINGREQ. The answer +is `ok:192,0`. The request `parse 224,1,0` is the one byte +body form of DISCONNECT with reason code 0. The answer is +`ok:224,2,0,0`: the same packet reprinted with its explicit +property block. + +The tool prints only the re-encoded bytes. It does not print +a rendering of the packet, so test harnesses check the parsed +structure through the re-encoding together with their own +oracle. diff --git a/lake-manifest.json b/lake-manifest.json new file mode 100644 index 0000000..8cae1c0 --- /dev/null +++ b/lake-manifest.json @@ -0,0 +1,6 @@ +{"version": "1.3.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "mqtt", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lakefile.toml b/lakefile.toml new file mode 100644 index 0000000..2a89053 --- /dev/null +++ b/lakefile.toml @@ -0,0 +1,13 @@ +name = "mqtt" +version = "0.1.0" +defaultTargets = ["Mqtt", "Proofs", "mqtt"] + +[[lean_lib]] +name = "Mqtt" + +[[lean_lib]] +name = "Proofs" + +[[lean_exe]] +name = "mqtt" +root = "Main" diff --git a/lean-toolchain b/lean-toolchain new file mode 100644 index 0000000..a6aff06 --- /dev/null +++ b/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.35.0 diff --git a/tests/TEST-RESULTS.md b/tests/TEST-RESULTS.md new file mode 100644 index 0000000..838f533 --- /dev/null +++ b/tests/TEST-RESULTS.md @@ -0,0 +1,20 @@ +# Test results: mqtt + +Seed: 20261026. Tool: the Lean command line program, one process per section, requests batched. The harness checks parsed structure through the re-encoding the tool prints, together with its own oracle. + +Paho's Python library (`paho-mqtt`, version 2.1.0) was importable in the interpreter that ran this harness; the Paho cross-check ran. It covers variable byte integers and PUBLISH property blocks, the pieces the library exposes without a broker. + +Mosquitto was NOT present on this machine (no `mosquitto` or `mosquitto_sub` binary), so no Mosquitto tests ran. + +| Section | Inputs | Agreements | +| --- | --- | --- | +| Fixed cases (spec VBI table, one packet per type, richer hand built packets) | 30 | 30 | +| Oracle differential, random packets of all seven types (seed 20261026) | 3000 | 3000 | +| Paho 2.1.0 cross-check (variable byte integers and PUBLISH property blocks) | 629 | 629 | +| Mutations and named rejections, settled by the oracle | 258 | 258 | +| Line protocol cases | 9 | 9 | + +Named differences from the oracles: +- Paho's variable byte integer decoder also accepts the non-minimal encoding 128, 0 as the value 0, matching the pinned reading in SPEC.md. + +Failures: none. diff --git a/tests/run_tests.py b/tests/run_tests.py new file mode 100644 index 0000000..c08b7e5 --- /dev/null +++ b/tests/run_tests.py @@ -0,0 +1,1048 @@ +#!/usr/bin/env python3 +"""Test harness for the Lean MQTT 5.0 packet codec. + +Layers, all settled against independent expectations: + +1. Fixed cases: the variable byte integer table from section + 2.1.4 of the standard, hand built packets for each of the + seven packet types in this slice, and the DISCONNECT one + byte body form, which is legal and reprints in the longer + canonical form. + +2. A differential against a strict oracle written here from + the standard and from SPEC.md (including the pinned + readings: non-minimal variable byte integers within four + bytes are accepted, and the DISCONNECT body of length 1 is + a reason code with an empty property block): random packets + of all seven types with varied properties are encoded by + the oracle, read by the Lean tool, and the answer must be + the canonical reprint. + +3. A cross-check against Paho's Python library when it is + importable: its variable byte integer encoder must match + the oracle's, and property blocks it packs for PUBLISH are + read by the oracle, wrapped in packets, and fed to the Lean + tool. When the library is absent, the run says so and the + oracle carries accept and reject alone. The Mosquitto test + suite is a separate program, not a Python library; the run + checks for its binary and the results file states whether + it was present. + +Mutations of rich packets (truncation at every length, byte +flips at every position) and a list of named rejection cases +are settled by comparing the Lean answer with the oracle's +answer on the same bytes. + +Results are written to tests/TEST-RESULTS.md. Seed 20261026. + +Usage: python3 tests/run_tests.py [--skip-build] +Run it with the work directory's virtual environment +(./venv/bin/python tests/run_tests.py) to get the Paho +cross-check; without the library that part is skipped and +the results file says so. +""" + +import os +import random +import shutil +import subprocess +import sys + +HERE = os.path.dirname(os.path.abspath(__file__)) +ROOT = os.path.dirname(HERE) +EXE = os.path.join(ROOT, ".lake", "build", "bin", "mqtt") +SEED = 20261026 + +failures = [] + + +def check(cond, label, detail=""): + if not cond: + failures.append(f"{label}: {detail}") + print(f"FAIL {label}: {detail}") + + +# --------------------------------------------------------------------------- +# Batch runner: one process for many requests. +# --------------------------------------------------------------------------- + +class Tool: + def __init__(self): + self.lines = [] + + def ask(self, line): + self.lines.append(line) + return len(self.lines) - 1 + + def run(self): + proc = subprocess.run([EXE], input="\n".join(self.lines) + "\n", + capture_output=True, text=True, timeout=1200) + if proc.returncode != 0: + raise RuntimeError(f"tool exited {proc.returncode}: {proc.stderr[:500]}") + self.answers = proc.stdout.splitlines() + if len(self.answers) != len(self.lines): + raise RuntimeError( + f"answer count {len(self.answers)} != request count {len(self.lines)}") + return self.answers + + +def req(bs): + return "parse " + ",".join(str(b) for b in bs) + + +def want_ok(canon): + return "ok:" + ",".join(str(b) for b in canon) + + +# --------------------------------------------------------------------------- +# Oracle: canonical encoder and strict decoder, written from the +# MQTT 5.0 standard and SPEC.md. +# +# Packet representation: +# ("connect", clean, keep_alive, props, client_id, will, +# username, password) +# will is None or (qos, retain, props, topic, payload bytes) +# username is None or str; password is None or bytes +# ("publish", dup, qos, retain, topic, packet_id, props, payload) +# packet_id is None at QoS 0 +# ("subscribe", packet_id, props, filters) +# filters is a list of (str, (qos, no_local, retain_as_published, +# retain_handling)) +# ("suback", packet_id, props, [reason, ...]) +# ("pingreq",) ("pingresp",) +# ("disconnect", None) or ("disconnect", (reason, props)) +# A property is (id, value): an int for byte, two byte, four byte, +# and variable byte integer values; a str for a UTF-8 string value; +# a (str, str) pair for a user property; bytes for binary data. +# --------------------------------------------------------------------------- + +class Reject(Exception): + pass + + +def enc_vbi(n): + out = bytearray() + while True: + d = n % 128 + n //= 128 + if n: + out.append(d + 128) + else: + out.append(d) + return bytes(out) + + +def dec_vbi(bs, i): + acc = 0 + mult = 1 + for k in range(4): + if i >= len(bs): + raise Reject() + b = bs[i] + i += 1 + if b < 128: + return acc + mult * b, i + if k == 3: + raise Reject() + acc += mult * (b - 128) + mult *= 128 + raise Reject() + + +def be16(n): + return n.to_bytes(2, "big") + + +def dec_uint(bs, i, w): + if i + w > len(bs): + raise Reject() + return int.from_bytes(bs[i:i + w], "big"), i + w + + +def enc_str(s): + raw = s.encode("utf-8") + return be16(len(raw)) + raw + + +def dec_str(bs, i): + ln, i = dec_uint(bs, i, 2) + if i + ln > len(bs): + raise Reject() + raw = bytes(bs[i:i + ln]) + try: + s = raw.decode("utf-8") + except UnicodeDecodeError: + raise Reject() + if "\x00" in s: + raise Reject() + return s, i + ln + + +def enc_bin(b): + return be16(len(b)) + bytes(b) + + +def dec_bin(bs, i): + ln, i = dec_uint(bs, i, 2) + if i + ln > len(bs): + raise Reject() + return bytes(bs[i:i + ln]), i + ln + + +PROP_TYPE = { + 0x01: "byte", 0x02: "four", 0x03: "utf8", 0x08: "utf8", + 0x09: "binary", 0x0B: "var", 0x11: "four", 0x12: "utf8", + 0x13: "two", 0x15: "utf8", 0x16: "binary", 0x17: "byte", + 0x18: "four", 0x19: "byte", 0x1A: "utf8", 0x1C: "utf8", + 0x1F: "utf8", 0x21: "two", 0x22: "two", 0x23: "two", + 0x24: "byte", 0x25: "byte", 0x26: "pair", 0x27: "four", + 0x28: "byte", 0x29: "byte", 0x2A: "byte", +} + +ALLOWED = { + "connect": [0x11, 0x15, 0x16, 0x17, 0x19, 0x21, 0x22, 0x26, 0x27], + "will": [0x01, 0x02, 0x03, 0x08, 0x09, 0x18, 0x26], + "publish": [0x01, 0x02, 0x03, 0x08, 0x09, 0x0B, 0x23, 0x26], + "subscribe": [0x0B, 0x26], + "suback": [0x1F, 0x26], + "disconnect": [0x11, 0x1C, 0x1F, 0x26], +} + + +def repeatable(setname, pid): + return pid == 0x26 or (pid == 0x0B and setname == "publish") + + +def enc_prop_val(t, v): + if t == "byte": + return bytes([v]) + if t == "two": + return be16(v) + if t == "four": + return v.to_bytes(4, "big") + if t == "var": + return enc_vbi(v) + if t == "utf8": + return enc_str(v) + if t == "pair": + return enc_str(v[0]) + enc_str(v[1]) + if t == "binary": + return enc_bin(v) + raise ValueError(t) + + +def dec_prop_val(t, bs, i): + if t == "byte": + return dec_uint(bs, i, 1) + if t == "two": + return dec_uint(bs, i, 2) + if t == "four": + return dec_uint(bs, i, 4) + if t == "var": + return dec_vbi(bs, i) + if t == "utf8": + return dec_str(bs, i) + if t == "pair": + k, i = dec_str(bs, i) + v, i = dec_str(bs, i) + return (k, v), i + if t == "binary": + return dec_bin(bs, i) + raise ValueError(t) + + +def enc_props(ps): + body = b"".join(enc_vbi(pid) + enc_prop_val(PROP_TYPE[pid], v) + for pid, v in ps) + return enc_vbi(len(body)) + body + + +def dec_props(setname, bs, i): + ln, i = dec_vbi(bs, i) + if i + ln > len(bs): + raise Reject() + seg = bytes(bs[i:i + ln]) + end = i + ln + ps = [] + seen = [] + j = 0 + while j < len(seg): + pid, j = dec_vbi(seg, j) + if pid not in PROP_TYPE or pid not in ALLOWED[setname]: + raise Reject() + if pid in seen and not repeatable(setname, pid): + raise Reject() + seen.append(pid) + v, j = dec_prop_val(PROP_TYPE[pid], seg, j) + ps.append((pid, v)) + if j != len(seg): + raise Reject() + return ps, end + + +def check_topic(s): + if s == "" or "+" in s or "#" in s: + raise Reject() + return s + + +def flagbit(n, k): + return (n // (2 ** k)) % 2 == 1 + + +def enc_opts(o): + qos, no_local, rap, rh = o + return qos + (4 if no_local else 0) + (8 if rap else 0) + rh * 16 + + +def dec_opts(b): + if b >= 64 or b % 4 == 3 or (b // 16) % 4 == 3: + raise Reject() + return (b % 4, (b // 4) % 2 == 1, (b // 8) % 2 == 1, (b // 16) % 4) + + +def enc_packet(pkt): + tag = pkt[0] + if tag == "connect": + _, clean, ka, props, cid, will, username, password = pkt + flags = ((128 if username is not None else 0) + + (64 if password is not None else 0) + + ((32 if will[1] else 0) + will[0] * 8 + 4 + if will is not None else 0) + + (2 if clean else 0)) + body = enc_str("MQTT") + bytes([5, flags]) + be16(ka) + body += enc_props(props) + body += enc_str(cid) + if will is not None: + body += enc_props(will[2]) + enc_str(will[3]) + enc_bin(will[4]) + if username is not None: + body += enc_str(username) + if password is not None: + body += enc_bin(password) + header = 0x10 + elif tag == "publish": + _, dup, qos, retain, topic, pid, props, payload = pkt + header = 0x30 + (8 if dup else 0) + qos * 2 + (1 if retain else 0) + body = enc_str(topic) + if pid is not None: + body += be16(pid) + body += enc_props(props) + bytes(payload) + elif tag == "subscribe": + _, pid, props, filters = pkt + header = 0x82 + body = be16(pid) + enc_props(props) + for f, o in filters: + body += enc_str(f) + bytes([enc_opts(o)]) + elif tag == "suback": + _, pid, props, reasons = pkt + header = 0x90 + body = be16(pid) + enc_props(props) + bytes(reasons) + elif tag == "pingreq": + header, body = 0xC0, b"" + elif tag == "pingresp": + header, body = 0xD0, b"" + elif tag == "disconnect": + header = 0xE0 + if pkt[1] is None: + body = b"" + else: + body = bytes([pkt[1][0]]) + enc_props(pkt[1][1]) + else: + raise ValueError(tag) + return bytes([header]) + enc_vbi(len(body)) + body + + +def raw_packet(header, body): + return bytes([header]) + enc_vbi(len(body)) + bytes(body) + + +def dec_connect(seg): + proto, i = dec_str(seg, 0) + if proto != "MQTT": + raise Reject() + level, i = dec_uint(seg, i, 1) + if level != 5: + raise Reject() + flags, i = dec_uint(seg, i, 1) + if flags % 2 != 0 or (flags // 8) % 4 == 3: + raise Reject() + ka, i = dec_uint(seg, i, 2) + props, i = dec_props("connect", seg, i) + cid, i = dec_str(seg, i) + will = None + if flagbit(flags, 2): + wprops, i = dec_props("will", seg, i) + wtopic, i = dec_str(seg, i) + check_topic(wtopic) + wpay, i = dec_bin(seg, i) + will = ((flags // 8) % 4, flagbit(flags, 5), wprops, wtopic, wpay) + username = None + if flagbit(flags, 7): + username, i = dec_str(seg, i) + password = None + if flagbit(flags, 6): + password, i = dec_bin(seg, i) + if i != len(seg): + raise Reject() + return ("connect", flagbit(flags, 1), ka, props, cid, will, + username, password) + + +def dec_publish(flags, seg): + topic, i = dec_str(seg, 0) + check_topic(topic) + qos = (flags // 2) % 4 + pid = None + if qos != 0: + pid, i = dec_uint(seg, i, 2) + if pid == 0: + raise Reject() + props, i = dec_props("publish", seg, i) + return ("publish", flagbit(flags, 3), qos, flagbit(flags, 0), + topic, pid, props, bytes(seg[i:])) + + +def dec_subscribe(seg): + pid, i = dec_uint(seg, 0, 2) + if pid == 0: + raise Reject() + props, i = dec_props("subscribe", seg, i) + filters = [] + while i < len(seg): + f, i = dec_str(seg, i) + if i >= len(seg): + raise Reject() + o = dec_opts(seg[i]) + i += 1 + filters.append((f, o)) + if not filters: + raise Reject() + return ("subscribe", pid, props, filters) + + +def dec_suback(seg): + pid, i = dec_uint(seg, 0, 2) + if pid == 0: + raise Reject() + props, i = dec_props("suback", seg, i) + reasons = list(seg[i:]) + if not reasons: + raise Reject() + return ("suback", pid, props, reasons) + + +def dec_disconnect(seg): + if len(seg) == 0: + return ("disconnect", None) + if len(seg) == 1: + return ("disconnect", (seg[0], [])) + props, j = dec_props("disconnect", seg, 1) + if j != len(seg): + raise Reject() + return ("disconnect", (seg[0], props)) + + +def oracle_parse(bs): + """The whole input form: exactly one packet, nothing after it. + Returns the packet, or None when the oracle rejects.""" + try: + if not bs: + return None + header = bs[0] + ln, i = dec_vbi(bs, 1) + if i + ln > len(bs): + return None + seg = bytes(bs[i:i + ln]) + rest = i + ln + typ, flags = header // 16, header % 16 + if typ == 1 and flags == 0: + pkt = dec_connect(seg) + elif typ == 3 and (flags // 2) % 4 != 3: + pkt = dec_publish(flags, seg) + elif typ == 8 and flags == 2: + pkt = dec_subscribe(seg) + elif typ == 9 and flags == 0: + pkt = dec_suback(seg) + elif typ == 12 and flags == 0 and not seg: + pkt = ("pingreq",) + elif typ == 13 and flags == 0 and not seg: + pkt = ("pingresp",) + elif typ == 14 and flags == 0: + pkt = dec_disconnect(seg) + else: + return None + except Reject: + return None + if rest != len(bs): + return None + return pkt + + +def settled_answer(bs): + pkt = oracle_parse(bs) + return want_ok(enc_packet(pkt)) if pkt is not None else "none" + + +# --------------------------------------------------------------------------- +# Random packets. +# --------------------------------------------------------------------------- + +TEXT = "abcdefgXYZ 019._-/" +UNICODE = ["é", "ü", "世", "☕"] + + +def rand_text(rng, lo=0, hi=10, topic_safe=False): + n = rng.randint(lo, hi) + pool = TEXT if topic_safe else TEXT + "".join(UNICODE) + return "".join(rng.choice(pool) for _ in range(n)) + + +def rand_topic(rng): + parts = [rand_text(rng, 1, 5, topic_safe=True) + for _ in range(rng.randint(1, 3))] + return "/".join(parts) + + +def rand_filter(rng): + parts = [] + for _ in range(rng.randint(1, 3)): + parts.append(rng.choice(["+", "#", rand_text(rng, 1, 4, + topic_safe=True)])) + return "/".join(parts) + + +def rand_bytes(rng, hi=12): + return bytes(rng.randrange(256) for _ in range(rng.randint(0, hi))) + + +def rand_prop_value(rng, t): + if t == "byte": + return rng.choice([0, 1, 2, 255, rng.randrange(256)]) + if t == "two": + return rng.choice([0, 1, 256, 65535, rng.randrange(65536)]) + if t == "four": + return rng.choice([0, 1, 65536, 4294967295, + rng.randrange(1 << 32)]) + if t == "var": + return rng.choice([0, 1, 127, 128, 16383, 16384, 2097151, + 268435455, rng.randrange(1 << 28)]) + if t == "utf8": + return rand_text(rng, 0, 8) + if t == "pair": + return (rand_text(rng, 1, 5), rand_text(rng, 0, 5)) + if t == "binary": + return rand_bytes(rng, 8) + raise ValueError(t) + + +def rand_props(rng, setname): + ids = list(ALLOWED[setname]) + rng.shuffle(ids) + ids = ids[:rng.randint(0, min(4, len(ids)))] + ps = [] + for pid in ids: + ps.append((pid, rand_prop_value(rng, PROP_TYPE[pid]))) + if repeatable(setname, pid) and rng.random() < 0.4: + ps.append((pid, rand_prop_value(rng, PROP_TYPE[pid]))) + return ps + + +def rand_packet(rng): + tag = rng.choice(["connect", "publish", "publish", "subscribe", + "suback", "pingreq", "pingresp", "disconnect"]) + if tag == "connect": + will = None + if rng.random() < 0.5: + will = (rng.randint(0, 2), rng.random() < 0.5, + rand_props(rng, "will"), rand_topic(rng), + rand_bytes(rng)) + return ("connect", rng.random() < 0.5, + rng.choice([0, 1, 60, 65535, rng.randrange(65536)]), + rand_props(rng, "connect"), rand_text(rng, 0, 8), will, + rand_text(rng, 1, 6) if rng.random() < 0.4 else None, + rand_bytes(rng) if rng.random() < 0.4 else None) + if tag == "publish": + qos = rng.choice([0, 1, 2]) + return ("publish", rng.random() < 0.5, qos, rng.random() < 0.5, + rand_topic(rng), + rng.randint(1, 65535) if qos else None, + rand_props(rng, "publish"), rand_bytes(rng, 20)) + if tag == "subscribe": + filters = [(rand_filter(rng), + (rng.randint(0, 2), rng.random() < 0.5, + rng.random() < 0.5, rng.randint(0, 2))) + for _ in range(rng.randint(1, 3))] + return ("subscribe", rng.randint(1, 65535), + rand_props(rng, "subscribe"), filters) + if tag == "suback": + return ("suback", rng.randint(1, 65535), + rand_props(rng, "suback"), + [rng.choice([0, 1, 2, 128, 131, 135, 144, 161, + rng.randrange(256)]) + for _ in range(rng.randint(1, 4))]) + if tag == "pingreq": + return ("pingreq",) + if tag == "pingresp": + return ("pingresp",) + if rng.random() < 0.3: + return ("disconnect", None) + return ("disconnect", + (rng.choice([0, 4, 129, 135, 142, rng.randrange(256)]), + rand_props(rng, "disconnect"))) + + +# --------------------------------------------------------------------------- +# Test sections. +# --------------------------------------------------------------------------- + +VBI_TABLE = [ + (0, [0]), (127, [127]), (128, [128, 1]), (16383, [255, 127]), + (16384, [128, 128, 1]), (2097151, [255, 255, 127]), + (2097152, [128, 128, 128, 1]), + (268435455, [255, 255, 255, 127]), +] + + +def fixed_cases(): + tool = Tool() + entries = [] + + def add(label, bs, expected=None): + idx = tool.ask(req(bs)) + entries.append((label, idx, + expected if expected is not None + else want_ok(bytes(bs)))) + + # The section 2.1.4 table, checked at the oracle first, then + # exercised through the tool as Subscription Identifier values + # on SUBSCRIBE packets, and as remaining lengths where the + # body size is practical. + for value, enc in VBI_TABLE: + check(list(enc_vbi(value)) == enc, f"fixed/vbi {value}", + "oracle encoder differs from the spec table") + pkt = ("subscribe", 1, [(0x0B, value)], + [("a", (0, False, False, 0))]) + add(f"vbi {value} as a property value", enc_packet(pkt)) + for value in (0, 127, 128, 16383, 16384): + if value == 0: + add("remaining length 0", bytes([192, 0])) + else: + body_len = value + payload = bytes(body_len - 4) + pkt = ("publish", False, 0, False, "a", None, [], payload) + bs = enc_packet(pkt) + check(list(bs[1:1 + len(enc_vbi(value))]) == list(enc_vbi(value)), + f"fixed/remaining length {value}", "header bytes differ") + add(f"remaining length {value}", bs) + # The pinned reading: a non-minimal encoding within four bytes + # is accepted, and reprints in the minimal form. + add("vbi non-minimal 128,0 as remaining length", + bytes([48, 134, 0, 0, 1, 97, 0, 1, 2]), + want_ok(bytes([48, 6, 0, 1, 97, 0, 1, 2]))) + add("vbi with rest in one packet stream position", + bytes([192, 0]), want_ok(bytes([192, 0]))) + + # One hand built packet per type; the literal ones are the + # same bytes proved in Proofs/Examples.lean. + add("pingreq", bytes([192, 0])) + add("pingresp", bytes([208, 0])) + add("disconnect empty", bytes([224, 0])) + add("disconnect reason only, canonical reprint", + bytes([224, 1, 0]), want_ok(bytes([224, 2, 0, 0]))) + add("publish qos0", bytes([48, 6, 0, 1, 97, 0, 1, 2])) + add("publish qos1", bytes([50, 6, 0, 1, 97, 0, 1, 0])) + add("subscribe one filter", bytes([130, 7, 0, 1, 0, 0, 1, 97, 0])) + add("suback", bytes([144, 4, 0, 1, 0, 0])) + add("connect plain", + bytes([16, 14, 0, 4, 77, 81, 84, 84, 5, 2, 0, 0, 0, 0, 1, 120])) + + richer = [ + ("connect with will, username, password", + ("connect", True, 60, + [(0x11, 3600), (0x26, ("k", "v"))], "client-1", + (1, True, [(0x18, 30), (0x03, "text/plain")], + "last/will", b"\x01\x02"), + "user", b"secret")), + ("publish qos2 with properties", + ("publish", True, 2, True, "sensors/temp", 4242, + [(0x01, 1), (0x02, 600), (0x0B, 7), (0x0B, 9), + (0x26, ("a", "b")), (0x23, 3)], b"hello")), + ("subscribe two filters", + ("subscribe", 9, [(0x0B, 12)], + [("sensors/+", (1, True, False, 1)), + ("alerts/#", (2, False, True, 2))])), + ("suback with reason string", + ("suback", 9, [(0x1F, "done")], [0, 1, 128])), + ("disconnect with properties", + ("disconnect", (142, [(0x11, 0), (0x1F, "bye")]))), + ("disconnect reason with empty properties", + ("disconnect", (0, []))), + ] + for label, pkt in richer: + bs = enc_packet(pkt) + check(oracle_parse(bs) == pkt, f"fixed/{label}", + "oracle does not read its own packet back") + add(label, bs) + + answers = tool.run() + for label, idx, expected in entries: + check(answers[idx] == expected, f"fixed/{label}", + f"got {answers[idx]}, want {expected}") + return len(entries) + + +def oracle_differential(rng, count): + tool = Tool() + entries = [] + for _ in range(count): + pkt = rand_packet(rng) + bs = enc_packet(pkt) + idx = tool.ask(req(bs)) + entries.append((idx, want_ok(bs), pkt[0])) + answers = tool.run() + agree = 0 + seen_types = set() + for idx, expected, tag in entries: + seen_types.add(tag) + if answers[idx] == expected: + agree += 1 + else: + check(False, "oracle differential", + f"got {answers[idx]}, want {expected}") + check(seen_types == {"connect", "publish", "subscribe", "suback", + "pingreq", "pingresp", "disconnect"}, + "oracle differential coverage", f"types seen: {seen_types}") + return len(entries), agree + + +def paho_section(rng, count_props): + """Cross-checks against Paho: variable byte integers, and + PUBLISH property blocks packed by the library. Returns + (inputs, agreements).""" + from paho.mqtt.properties import Properties, VariableByteIntegers + from paho.mqtt.packettypes import PacketTypes + tool = Tool() + entries = [] + total = 0 + agree = 0 + block_agree = 0 + + values = [v for v, _ in VBI_TABLE] + values += [rng.randrange(1 << 28) for _ in range(120)] + for v in values: + total += 1 + if bytes(VariableByteIntegers.encode(v)) == enc_vbi(v): + agree += 1 + else: + check(False, "paho vbi", f"encode {v} differs") + total += 1 + if VariableByteIntegers.decode(bytes([128, 0])) == (0, 2): + agree += 1 + else: + check(False, "paho vbi", "non-minimal decode differs") + + attr = {0x01: "PayloadFormatIndicator", 0x02: "MessageExpiryInterval", + 0x03: "ContentType", 0x08: "ResponseTopic", + 0x09: "CorrelationData", 0x0B: "SubscriptionIdentifier", + 0x23: "TopicAlias", 0x26: "UserProperty"} + for _ in range(count_props): + props = Properties(PacketTypes.PUBLISH) + chosen = [] + if rng.random() < 0.7: + props.PayloadFormatIndicator = rng.randint(0, 1) + if rng.random() < 0.5: + props.MessageExpiryInterval = rng.randrange(1 << 32) + if rng.random() < 0.5: + props.ContentType = rand_text(rng, 1, 6, topic_safe=True) + if rng.random() < 0.4: + props.ResponseTopic = rand_topic(rng) + if rng.random() < 0.4: + props.CorrelationData = rand_bytes(rng, 6) + if rng.random() < 0.5: + props.SubscriptionIdentifier = [rng.randint(1, 1000) + for _ in range(rng.randint(1, 2))] + if rng.random() < 0.5: + props.TopicAlias = rng.randint(1, 65535) + if rng.random() < 0.5: + props.UserProperty = [(rand_text(rng, 1, 4, topic_safe=True), + rand_text(rng, 0, 4, topic_safe=True))] + packed = bytes(props.pack()) + try: + parsed, j = dec_props("publish", packed, 0) + okshape = j == len(packed) + except Reject: + okshape = False + total += 1 + if not okshape or enc_props(parsed) != packed: + check(False, "paho properties", + f"oracle cannot read paho block {list(packed)}") + continue + block_agree += 1 + pkt = ("publish", False, 1, False, "paho/topic", 7, parsed, + b"\x10\x20") + bs = enc_packet(pkt) + idx = tool.ask(req(bs)) + entries.append((idx, want_ok(bs))) + total += 1 + answers = tool.run() + packet_agree = 0 + for idx, expected in entries: + if answers[idx] == expected: + packet_agree += 1 + else: + check(False, "paho packet", + f"got {answers[idx]}, want {expected}") + agree += block_agree + packet_agree + return total, agree + + +def mutation_cases(rng): + tool = Tool() + entries = [] + + def settle(label, bs): + idx = tool.ask(req(bs)) + entries.append((label, idx, settled_answer(bs))) + + def expect(label, bs, expected): + idx = tool.ask(req(bs)) + entries.append((label, idx, expected)) + check(settled_answer(bs) == expected, f"mutation/{label}", + "oracle disagrees with the named expectation") + + rich_connect = enc_packet( + ("connect", True, 60, [(0x11, 3600), (0x26, ("k", "v"))], + "client-1", + (1, True, [(0x18, 30)], "last/will", b"\x01\x02"), + "user", b"secret")) + rich_publish = enc_packet( + ("publish", False, 1, False, "sensors/temp", 4242, + [(0x02, 600), (0x26, ("a", "b"))], b"hello world")) + for name, base in (("connect", rich_connect), + ("publish", rich_publish)): + for cut in range(len(base)): + settle(f"{name} truncate {cut}", base[:cut]) + for off in range(len(base)): + mut = bytearray(base) + mut[off] = (mut[off] + 37) % 256 + settle(f"{name} flip at {off}", bytes(mut)) + + def props_packet(setname_header, body_props, tail): + return raw_packet(setname_header, body_props + tail) + + named = [] + # Five byte remaining length: a continuation mark on the + # fourth byte. + named.append(("five byte remaining length", + bytes([192, 255, 255, 255, 255, 127]), "none")) + named.append(("remaining length larger than input", + bytes([192, 5, 0]), "none")) + named.append(("remaining length larger than a publish body", + bytes([48, 100, 0, 1, 97]), "none")) + named.append(("truncated connect variable header", + bytes([16, 8, 0, 4, 77, 81, 84, 84, 5]), "none")) + named.append(("wrong flags on connect", bytes([17, 0]), "none")) + named.append(("wrong flags on suback", + bytes([146, 4, 0, 1, 0, 0]), "none")) + named.append(("wrong flags on pingreq", bytes([193, 0]), "none")) + sub_body = be16(1) + b"\x00" + enc_str("a") + b"\x00" + named.append(("subscribe with flags 0000", + raw_packet(0x80, sub_body), "none")) + pub_body = enc_str("a") + be16(1) + b"\x00" + b"x" + named.append(("publish qos 3", raw_packet(0x36, pub_body), "none")) + wild_body = enc_str("a/#") + b"\x00" + b"x" + named.append(("publish wildcard topic", + raw_packet(0x30, wild_body), "none")) + badname = (enc_str("MQTU") + bytes([5, 2]) + be16(0) + b"\x00" + + enc_str("x")) + named.append(("connect wrong protocol name", + raw_packet(0x10, badname), "none")) + reserved = bytearray(rich_connect) + # The connect flags byte: header(1) + length(1) + name(6) + # + level(1) puts it at index 9. + reserved[9] = reserved[9] | 1 + named.append(("connect reserved flag bit", bytes(reserved), "none")) + willqos = (enc_str("MQTT") + bytes([5, 2 | 4 | 24]) + be16(0) + + b"\x00" + enc_str("x") + b"\x00" + enc_str("w") + + enc_bin(b"")) + named.append(("connect will qos 3", raw_packet(0x10, willqos), "none")) + wrong_prop = (enc_str("MQTT") + bytes([5, 2]) + be16(0) + + enc_props([(0x0B, 5)]) + enc_str("x")) + named.append(("subscription identifier on connect", + raw_packet(0x10, wrong_prop), "none")) + table_only = raw_packet(0xE0, bytes([0]) + enc_props([(0x12, "x")])) + named.append(("assigned client identifier on disconnect", + table_only, "none")) + unknown_prop = raw_packet( + 0x30, enc_str("a") + b"\x04\x7f\x01\x00\x00" + b"") + named.append(("unknown property identifier", unknown_prop, "none")) + repeated = raw_packet( + 0x32, enc_str("a") + be16(3) + enc_props([(0x23, 1), (0x23, 2)])) + named.append(("repeated single use property", repeated, "none")) + overrun = raw_packet(0x30, enc_str("a") + b"\x0a\x01\x01") + named.append(("property block length overruns", overrun, "none")) + named.append(("packet identifier 0 in subscribe", + raw_packet(0x82, be16(0) + b"\x00" + enc_str("a") + + b"\x00"), "none")) + named.append(("packet identifier 0 in publish qos1", + raw_packet(0x32, enc_str("a") + be16(0) + b"\x00"), + "none")) + named.append(("empty topic filter list", + raw_packet(0x82, be16(1) + b"\x00"), "none")) + named.append(("empty reason list in suback", + raw_packet(0x90, be16(1) + b"\x00"), "none")) + named.append(("disconnect body of length 1, accepted", + bytes([224, 1, 0]), want_ok(bytes([224, 2, 0, 0])))) + named.append(("pingreq with a body", bytes([192, 1, 0]), "none")) + named.append(("packet type 2, outside this slice", + bytes([32, 0]), "none")) + named.append(("packet type 0", bytes([0, 0]), "none")) + named.append(("trailing byte after one packet", + bytes([192, 0, 0]), "none")) + named.append(("empty input", b"", "none")) + nul_topic = raw_packet(0x30, be16(2) + b"a\x00" + b"\x00") + named.append(("null character in publish topic", nul_topic, "none")) + bad_utf8 = raw_packet(0x30, be16(1) + b"\xff" + b"\x00") + named.append(("ill formed utf-8 in publish topic", bad_utf8, "none")) + overlong = raw_packet(0x30, be16(2) + b"\xc0\x80" + b"\x00") + named.append(("overlong utf-8 in publish topic", overlong, "none")) + for opts_byte, label in ((64, "options byte reserved bits set"), + (3, "options byte qos 3"), + (48, "options byte retain handling 3")): + named.append((label, + raw_packet(0x82, be16(1) + b"\x00" + enc_str("a") + + bytes([opts_byte])), "none")) + for label, bs, expected in named: + expect(label, bs, expected) + answers = tool.run() + agree = 0 + for label, idx, expected in entries: + if answers[idx] == expected: + agree += 1 + else: + check(False, f"mutation/{label}", + f"got {answers[idx]}, want {expected}") + return len(entries), agree + + +def protocol_cases(): + lines = ["parse 192,0", "parse", "parse 01", "parse 256", + "parse 192,0,0", "bogus 1", "parse 1 2", "Parse 192,0", + "parse 0", ""] + expected = ["ok:192,0", "none", "error", "error", "none", + "error", "error", "error", "none"] + proc = subprocess.run([EXE], input="\n".join(lines) + "\n", + capture_output=True, text=True, timeout=120) + got = proc.stdout.splitlines() + check(got == expected, "protocol", f"got {got}, want {expected}") + return len(expected) + + +# --------------------------------------------------------------------------- + +def main(): + if "--skip-build" not in sys.argv: + subprocess.run(["lake", "build"], cwd=ROOT, check=True, + capture_output=True, text=True, timeout=1200) + rng = random.Random(SEED) + sections = [] + + n_fixed = fixed_cases() + sections.append(("Fixed cases (spec VBI table, one packet per type, " + "richer hand built packets)", n_fixed, n_fixed)) + + n_or, a_or = oracle_differential(rng, 3000) + sections.append(("Oracle differential, random packets of all seven " + "types (seed 20261026)", n_or, a_or)) + + try: + import paho.mqtt + import importlib.metadata as md + try: + paho_version = md.version("paho-mqtt") + except Exception: + paho_version = "unknown" + paho_present = True + except ImportError: + paho_present = False + paho_version = None + named = [] + if paho_present: + n_pa, a_pa = paho_section(rng, 250) + sections.append((f"Paho {paho_version} cross-check (variable byte " + "integers and PUBLISH property blocks)", + n_pa, a_pa)) + named.append("Paho's variable byte integer decoder also accepts " + "the non-minimal encoding 128, 0 as the value 0, " + "matching the pinned reading in SPEC.md.") + + n_mut, a_mut = mutation_cases(rng) + sections.append(("Mutations and named rejections, settled by the " + "oracle", n_mut, a_mut)) + n_proto = protocol_cases() + sections.append(("Line protocol cases", n_proto, n_proto)) + + mosquitto = shutil.which("mosquitto") or shutil.which("mosquitto_sub") + failed = len(failures) + lines = [] + lines.append("# Test results: mqtt") + lines.append("") + lines.append(f"Seed: {SEED}. Tool: the Lean command line program, " + "one process per section, requests batched. The harness " + "checks parsed structure through the re-encoding the " + "tool prints, together with its own oracle.") + lines.append("") + if paho_present: + lines.append(f"Paho's Python library (`paho-mqtt`, version " + f"{paho_version}) was importable in the interpreter " + "that ran this harness; the Paho cross-check ran. " + "It covers variable byte integers and PUBLISH " + "property blocks, the pieces the library exposes " + "without a broker.") + else: + lines.append("Paho's Python library (`paho-mqtt`) was NOT " + "importable in the interpreter that ran this " + "harness; the Paho cross-check did not run, and " + "the strict oracle carried accept and reject " + "alone.") + lines.append("") + if mosquitto: + lines.append(f"A Mosquitto binary was found at {mosquitto}; " + "no Mosquitto test cases are wired into this " + "harness.") + else: + lines.append("Mosquitto was NOT present on this machine (no " + "`mosquitto` or `mosquitto_sub` binary), so no " + "Mosquitto tests ran.") + lines.append("") + lines.append("| Section | Inputs | Agreements |") + lines.append("| --- | --- | --- |") + for name, total, agree in sections: + lines.append(f"| {name} | {total} | {agree} |") + lines.append("") + if named: + lines.append("Named differences from the oracles:") + for d in named: + lines.append(f"- {d}") + else: + lines.append("Named differences from the oracles: none.") + lines.append("") + if failed: + lines.append(f"Failures: {failed}.") + for f in failures[:40]: + lines.append(f"- {f}") + else: + lines.append("Failures: none.") + lines.append("") + with open(os.path.join(HERE, "TEST-RESULTS.md"), "w") as fh: + fh.write("\n".join(lines)) + total = sum(t for _, t, _ in sections) + agree = sum(a for _, _, a in sections) + print(f"sections={len(sections)} inputs={total} agreements={agree} " + f"failures={failed} paho={'yes ' + str(paho_version) if paho_present else 'no'} " + f"mosquitto={'yes' if mosquitto else 'no'}") + return 1 if failed else 0 + + +if __name__ == "__main__": + sys.exit(main()) From 0f7b515abbc897b68aaebefd3b517ea79cf70b46 Mon Sep 17 00:00:00 2001 From: shah Date: Tue, 27 Oct 2026 20:01:05 -0500 Subject: [PATCH 2/2] Add the bar file set: Spec.lean, comparator.json, bar.toml, CI workflow --- .github/workflows/bar.yml | 21 ++++ Proofs.lean | 1 + Proofs/SpecProofs.lean | 91 +++++++++++++++ README.md | 230 ++++++++++++++++++++++++++++++-------- SPEC.md | 26 +++++ Spec.lean | 115 +++++++++++++++++++ bar.toml | 67 +++++++++++ comparator.json | 1 + lakefile.toml | 3 + 9 files changed, 507 insertions(+), 48 deletions(-) create mode 100644 .github/workflows/bar.yml create mode 100644 Proofs/SpecProofs.lean create mode 100644 Spec.lean create mode 100644 bar.toml create mode 100644 comparator.json diff --git a/.github/workflows/bar.yml b/.github/workflows/bar.yml new file mode 100644 index 0000000..32457ed --- /dev/null +++ b/.github/workflows/bar.yml @@ -0,0 +1,21 @@ +name: verified bar + +on: + push: + pull_request: + # Rerun when the spec reviewer approves, or an approval is dismissed. + pull_request_review: + types: [submitted, dismissed] + +jobs: + bar: + # pull-requests: read lets the check confirm the spec approval on GitHub. + permissions: + contents: read + pull-requests: read + # Both lines pin the same commit of Proven-Commons/mission: bar v2, as + # proposed in its pull request #2. Move both to a release tag once + # mission publishes one. + uses: Proven-Commons/mission/.github/workflows/verified-bar.yml@6ba85c27abaaf07905c9316aa96dc29f7b5847a2 + with: + bar-ref: 6ba85c27abaaf07905c9316aa96dc29f7b5847a2 diff --git a/Proofs.lean b/Proofs.lean index 5aede97..6bfe916 100644 --- a/Proofs.lean +++ b/Proofs.lean @@ -1,3 +1,4 @@ import Proofs.Utf8 import Proofs.RoundTrip import Proofs.Examples +import Proofs.SpecProofs diff --git a/Proofs/SpecProofs.lean b/Proofs/SpecProofs.lean new file mode 100644 index 0000000..77d2d1b --- /dev/null +++ b/Proofs/SpecProofs.lean @@ -0,0 +1,91 @@ +/- + Proofs of the statements in `Spec.lean`, under the same names. + + The round trips are the theorems proved in + `Proofs/RoundTrip.lean`. The refusals are single inputs, + checked in the kernel with `decide +kernel`: no native + evaluation, which the bar forbids. +-/ + +import Mqtt +import Proofs.RoundTrip + +open Mqtt + +theorem Spec.parsePacket_print (p : Packet) (rest : List UInt8) + (h : PacketWF p) : + parsePacket (print p ++ rest) = some (p, rest) := + Mqtt.Proofs.parsePacket_print p rest h + +theorem Spec.parse_print (p : Packet) (h : PacketWF p) : + parse (print p) = some p := + Mqtt.Proofs.parse_print p h + +theorem Spec.decVBI_printVBI (n : Nat) (rest : List UInt8) + (hn : n < 268435456) : + decVBI (printVBI n ++ rest) = some (n, rest) := + Mqtt.Proofs.decVBI_printVBI n rest hn + + +theorem Spec.rejects_five_byte_remaining_length : + (parse ([192, 255, 255, 255, 255, 127] : List UInt8)).isSome + = false := by + decide +kernel + + +theorem Spec.rejects_subscribe_flags : + (parse ([128, 7, 0, 1, 0, 0, 1, 97, 0] : List UInt8)).isSome + = false := by + decide +kernel + + +theorem Spec.rejects_publish_qos3 : + (parse ([54, 7, 0, 1, 97, 0, 1, 0, 120] : List UInt8)).isSome + = false := by + decide +kernel + + +theorem Spec.rejects_wildcard_topic : + (parse ([48, 7, 0, 3, 97, 47, 35, 0, 120] : List UInt8)).isSome + = false := by + decide +kernel + + +theorem Spec.rejects_wrong_protocol_name : + (parse ([16, 14, 0, 4, 77, 81, 84, 85, 5, 2, 0, 0, 0, 0, 1, 120] + : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_reserved_connect_flag : + (parse ([16, 14, 0, 4, 77, 81, 84, 84, 5, 3, 0, 0, 0, 0, 1, 120] + : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_property_wrong_type : + (parse ([16, 16, 0, 4, 77, 81, 84, 84, 5, 2, 0, 0, 2, 11, 5, 0, + 1, 120] : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_repeated_property : + (parse ([50, 12, 0, 1, 97, 0, 3, 6, 35, 0, 1, 35, 0, 2] + : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_subscribe_id_zero : + (parse ([130, 7, 0, 0, 0, 0, 1, 97, 0] : List UInt8)).isSome + = false := by + decide +kernel + + +theorem Spec.rejects_pingreq_body : + (parse ([192, 1, 0] : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_unknown_type : + (parse ([32, 0] : List UInt8)).isSome = false := by + decide +kernel diff --git a/README.md b/README.md index 98b4584..a94ed12 100644 --- a/README.md +++ b/README.md @@ -1,66 +1,200 @@ # mqtt: an MQTT 5.0 packet reader and printer, with a proved round trip -An MQTT 5.0 control packet reader and printer in Lean, covering the seven packet types CONNECT, PUBLISH, SUBSCRIBE, SUBACK, PINGREQ, PINGRESP, and DISCONNECT, with their property blocks. The reader reads one packet from the front of a byte list and returns the rest of the input, so a caller can walk a stream of packets. The main claim is proved: parsing what the printer wrote returns the same packet. The tests run the tool against a strict oracle written from the standard and, for the pieces it covers, against the Paho Python library; see `tests/TEST-RESULTS.md` for the counts. +Status: in-progress + +An MQTT 5.0 control packet reader and printer in Lean, +covering the seven packet types CONNECT, PUBLISH, SUBSCRIBE, +SUBACK, PINGREQ, PINGRESP, and DISCONNECT, with their +property blocks. The reader reads one packet from the front +of a byte list and returns the rest of the input, so a +caller can walk a stream of packets. The definitions are in +`Mqtt/Value.lean` (the packet types, the property table, +the printer, and the well-formedness rules), `Mqtt/Parse.lean` +(the reader), and `Mqtt/Utf8.lean` (a strict UTF-8 codec, +carried in from the Proven Commons `jws` slice with its +namespace renamed, as the header of that file records). The +rules are written out in `SPEC.md`. This slice is framing +only: no broker, no client, and no session behaviour. + +The statements a reviewer approves are in `Spec.lean`, +with their proofs in `Proofs/SpecProofs.lean`. No reviewer +has approved them yet, so this project is not called +verified. + +## How to run it + +`lake build` builds the library, the proofs, and the +command line tool. The tool reads one request per line: +the word `parse`, a space, and the packet as +comma-separated decimal byte codes. It answers `ok:` and +the byte codes of the canonical reprint when the bytes are +one packet, `none` when they are rejected, and `error` when +the request itself is malformed. -Status: in progress. The specification has not yet been approved by a reviewer apart from its author, and no statement file (`Spec.lean`) has been added by a reviewer, so this is not verified. +``` +lake build +echo "parse 192,0" | .lake/build/bin/mqtt +``` + +That request is a PINGREQ, and the answer is `ok:192,0`: the +packet read back and reprinted. A PINGREQ carrying a body +(`parse 192,1,0`) answers `none`. See `SPEC.md` for the full +protocol. + +`python3 tests/run_tests.py` rebuilds the tool, runs the +fixed cases, the differential run against the harness +oracle, the Paho cross-check when the library is +importable, and the mutation and rejection cases, and +writes the outcome to `tests/TEST-RESULTS.md`. ## What is proved -The definitions are in `Mqtt/Value.lean` (the packet types, the property table, the printer, and the well-formedness rules), `Mqtt/Parse.lean` (the reader), and `Mqtt/Utf8.lean` (a strict UTF-8 codec, carried in from the Proven Commons `jws` slice with its namespace renamed, as the header of that file records). The proofs are in `Proofs/RoundTrip.lean` and `Proofs/Utf8.lean`, and worked examples from the standard are proved in `Proofs/Examples.lean`. +Each claim below names the theorem behind it. The +theorems are stated in `Spec.lean` (the challenge file, +where they end in `sorry`) and proved in +`Proofs/SpecProofs.lean`, under the same names. +`comparator.json` lists all of them. | Claim | Theorem | |-------|---------| -| Parsing the printed form of a well formed packet, with more stream bytes after it, gives the packet and those bytes back. | `Mqtt.Proofs.parsePacket_print` | -| Parsing the printed form of a well formed packet on its own gives the packet back. | `Mqtt.Proofs.parse_print` | -| Reading a printed variable byte integer gives the number back, for every value below 2^28. | `Mqtt.Proofs.decVBI_printVBI` | -| Decoding the UTF-8 encoding of any text gives the text back. | `Mqtt.Utf8.Proofs.decode_encode` | - -Under those, the field and body steps are proved one by one: big endian numbers, byte cuts, string and binary fields, typed property values, single properties, property lists and whole property blocks, the subscription options byte, topic filter lists, and the body of each of the seven packet types. - -A packet is well formed when its numbers fit the widths that carry them, its strings obey the string rules and fit the two byte length prefix, its properties match the property table in type and place with no single use property repeated, its packet identifiers stand where the type requires them and are never 0 there, and its whole body is shorter than 2^28, the largest remaining length a variable byte integer can carry. The full list is in `SPEC.md`. `parse_print` checks against the standard axioms only (`propext`, `Classical.choice`, `Quot.sound`), which a reader can confirm with `#print axioms Mqtt.Proofs.parse_print`, or by running `lake env lean Mqtt/Verify.lean`. - -The command-line tool in `Main.lean` calls these functions directly. +| Parsing the printed form of a well formed packet, with more stream bytes after it, gives the packet and those bytes back. | `Spec.parsePacket_print` | +| Parsing the printed form of a well formed packet on its own gives the packet back. | `Spec.parse_print` | +| Reading a printed variable byte integer gives the number back, for every value below 2^28. | `Spec.decVBI_printVBI` | +| A remaining length whose fourth byte carries a continuation mark, so the value would need a fifth byte, is refused. | `Spec.rejects_five_byte_remaining_length` | +| A SUBSCRIBE packet with flags 0000 is refused: the value the standard fixes is 0010. | `Spec.rejects_subscribe_flags` | +| A PUBLISH packet with the reserved QoS value 3 is refused. | `Spec.rejects_publish_qos3` | +| A PUBLISH topic name holding a wildcard is refused. | `Spec.rejects_wildcard_topic` | +| A CONNECT whose protocol name is not `MQTT` is refused. | `Spec.rejects_wrong_protocol_name` | +| A CONNECT with the reserved bit of the connect flags byte set is refused. | `Spec.rejects_reserved_connect_flag` | +| A property standing on a packet type that does not allow it, here a subscription identifier on a CONNECT, is refused. | `Spec.rejects_property_wrong_type` | +| A single use property standing twice in one block, here the topic alias on a PUBLISH, is refused. | `Spec.rejects_repeated_property` | +| A SUBSCRIBE with packet identifier 0 is refused. | `Spec.rejects_subscribe_id_zero` | +| A PINGREQ with a body is refused: its remaining length must be 0. | `Spec.rejects_pingreq_body` | +| A packet type outside the seven in this slice, here type 2, is refused. | `Spec.rejects_unknown_type` | + +A packet is well formed when its numbers fit the widths +that carry them, its strings obey the string rules and fit +the two byte length prefix, its properties match the +property table in type and place with no single use +property repeated, its packet identifiers stand where the +type requires them and are never 0 there, and its whole +body is shorter than 2^28, the largest remaining length a +variable byte integer can carry. The full list is in +`SPEC.md`. + +The round trip theorems rest on the proofs in +`Proofs/RoundTrip.lean`, where they are +`Mqtt.Proofs.parsePacket_print`, `Mqtt.Proofs.parse_print`, +and `Mqtt.Proofs.decVBI_printVBI`. All three check against +the standard axioms only (`propext`, `Classical.choice`, +`Quot.sound`), which a reader can confirm with +`#print axioms`, or by running +`lake env lean Mqtt/Verify.lean`. The refusal theorems are +single inputs checked in the kernel with `decide +kernel`. +Under the round trips, the field and body steps are proved +one by one in the same file: big endian numbers, byte cuts, +string and binary fields, typed property values, single +properties, property lists and whole property blocks, the +subscription options byte, topic filter lists, and the body +of each of the seven packet types. The UTF-8 round trip, +`Mqtt.Utf8.Proofs.decode_encode`, is proved in +`Proofs/Utf8.lean`, and worked examples from the standard +are proved in `Proofs/Examples.lean`. + +The command line tool in `Main.lean` calls `Mqtt.parse` +and `Mqtt.print` directly, the same functions the theorems +are about. ## What is not proved -- That the reader accepts every byte string the standard allows, and rejects every one it forbids. The round trip does not need either, so neither is proved. The oracle differential and the mutation tests check that behaviour instead, and the results file records the outcome. -- Any reading of what a property means. A property is an identifier and a typed value; that a Receive Maximum of 10 asks the peer to hold back after ten packets is broker and session behaviour, and none of it is in this slice. -- Anything about packets outside the seven types, or property identifiers outside the table in `SPEC.md`. Both are rejected, and that rejection is tested, not proved. -- Broker or session behaviour of any kind: connections, subscriptions as state, retained messages, keep alive timing, and what any peer does with a packet. -- The worked examples on the printing side. The examples in `Proofs/Examples.lean` are stated on the reading side, because the printer's variable byte integer is defined by well founded recursion, which the kernel will not evaluate in a `decide` proof here. The round trip theorem covers the printer. -- Reading requests and printing answers in `Main.lean`: splitting lines, and the decimal number reader. The tests cover them, malformed requests included. -- Speed. The code works on lists of bytes, which suits proofs, not large packets. +- That the reader accepts every byte string the standard + allows, and rejects every one it forbids. The round trips + do not need either, and the refusal theorems pin single + inputs only, so neither holds in general as a proof. The + oracle differential and the mutation tests in `tests/` + check that behaviour instead, and the results file + records the outcome, including any failure. +- The pinned reading of the variable byte integer: an + encoding that uses more bytes than the value needs is + accepted, as long as it fits in four bytes. Section + 1.5.5 of the standard states the shortest form as a + requirement on senders; this reader accepts the longer + forms, and the printer always writes the shortest. The + reading is pinned in `SPEC.md`, and it is a reading, not + a proof. +- Any reading of what a property means. A property is an + identifier and a typed value; that a Receive Maximum of + 10 asks the peer to hold back after ten packets is broker + and session behaviour, and none of it is in this slice. +- Anything about packets outside the seven types, or + property identifiers outside the table in `SPEC.md`. + Both are rejected, and that rejection is tested, apart + from the single inputs the refusal theorems pin. +- Broker or session behaviour of any kind: connections, + subscriptions as state, retained messages, keep alive + timing, and what any peer does with a packet. +- The worked examples on the printing side. The examples + in `Proofs/Examples.lean` are stated on the reading side, + because the printer's variable byte integer is defined + by well founded recursion, which the kernel will not + evaluate in a `decide` proof here. The round trip + theorems cover the printer. +- Reading requests and printing answers in `Main.lean`: + splitting lines, and the decimal number reader. The tests + cover them, malformed requests included. +- Speed. The code works on lists of bytes, which suits + proofs, not large packets. ## What you must trust -- The Lean kernel, which checks the proofs. -- The Lean compiler, with the C compiler and linker shipped with it, and the runtime, which turn the proved definitions into the program that runs. -- Lean's core library, including the compiled code it puts in place of some definitions the proofs reason about. -- The operating system and hardware it runs on. -- The strict oracle in the test harness, written from the MQTT 5.0 standard, and Paho's Python library in the parts of the differential it covers. The results file names the version used, and states plainly which oracles were and were not available. - -This project has no dependencies beyond Lean itself. - -## Run it - -Needs Linux and [elan](https://github.com/leanprover/elan). Build, then feed request lines to the tool: - -``` -lake build -echo "parse 192,0" | .lake/build/bin/mqtt -``` - -That request is a PINGREQ, and the answer is `ok:192,0`: the packet read back and reprinted. Bytes the reader rejects, such as a PINGREQ carrying a body (`parse 192,1,0`), answer `none`. A malformed request answers `error`. See `SPEC.md` for the full protocol. +- The Lean kernel (Lean 4.35.0, pinned in + `lean-toolchain`), which checks every proof. +- The Lean compiler, with the C compiler and linker + shipped with it, which turns the proved definitions into + the program that runs. +- The Lean runtime, which runs that program. +- The hardware the program runs on. +- Every dependency in `lake-manifest.json`: the manifest + lists no packages, so there are no library dependencies + to trust beyond the Lean toolchain itself. +- Lean's core library, including the compiled code it puts + in place of some definitions the proofs reason about. +- The operating system the program runs on. +- That `SPEC.md` states the reading of the MQTT 5.0 + standard you intend. The proofs are about the reader and + printer in this repo following each other exactly; the + fidelity of the spec to the standard is a reading, pinned + in `SPEC.md` where the standard leaves a choice open. +- The strict oracle in `tests/run_tests.py`, written from + the standard, and Paho's Python library in the parts of + the differential it covers. Both are evidence, not proof. + The results file names the versions used, and states + plainly which oracles were and were not available. +- The line handling in `Main.lean` (splitting a request + line, reading decimal codes). The tests drive it, and no + proof covers it. +- There are no exceptions to item 4 of the bar: the + project uses none of the features it forbids. ## Re-check it -Needs Linux, elan, and Python 3. The test harness uses the Paho library from the virtual environment in the work directory (`venv`) when it is there, and says so in the results file when it is not. - -``` -lake build -grep -rn "sorry" --include="*.lean" Mqtt Proofs Main.lean Mqtt.lean Proofs.lean -lake env lean Mqtt/Verify.lean -python3 tests/run_tests.py -``` - -The grep should print only the one line in `Mqtt/Verify.lean` that explains what a `sorryAx` in its output would mean: there is no `sorry` anywhere. The test script rebuilds the tool, runs the fixed cases, the differential against the strict oracle, the Paho cross-check when the library is importable, and the mutation and rejection cases, and writes the counts to `tests/TEST-RESULTS.md`. +1. `lake comparator --paranoid`: builds the challenge + file `Spec.lean` and the proofs in a sandbox and + checks that each theorem named in `comparator.json` + proves exactly the statement in the challenge file, + uses no axiom but the three standard ones, and is + accepted by Lean's kernel and every other kernel + shipped with Lean. +2. `python3 tests/run_tests.py`: the fixed cases, the + differential against the strict oracle, the Paho + cross-check when the library is importable, and the + mutation and rejection cases, with counts and any + failures written to `tests/TEST-RESULTS.md`. The + harness uses the Paho library from the virtual + environment in the work directory (`venv`) when it is + there, and says so in the results file when it is not. +3. `lake build`: the library, the proofs, and the tool + build clean, and `lake env lean Mqtt/Verify.lean` + prints the axiom list for the round trip theorems. +4. Read `SPEC.md` against the MQTT 5.0 standard and check + the pinned readings are the ones you want. diff --git a/SPEC.md b/SPEC.md index ce1cab6..856ff19 100644 --- a/SPEC.md +++ b/SPEC.md @@ -328,3 +328,29 @@ The tool prints only the re-encoded bytes. It does not print a rendering of the packet, so test harnesses check the parsed structure through the re-encoding together with their own oracle. + +## Properties and their theorems + +Each property a reader can check in the page (`README.md`) +names its theorem. The theorems are stated in `Spec.lean` +and proved in `Proofs/SpecProofs.lean`. The refusal theorems +are single inputs, one for each named rejection case in the +test harness; the tests in `tests/` cover each rule on many +more inputs. + +| Property | Theorem | +|----------|---------| +| Parsing the printed form of a well formed packet, with more stream bytes after it, gives the packet and those bytes back | `Spec.parsePacket_print` | +| Parsing the printed form of a well formed packet on its own gives the packet back | `Spec.parse_print` | +| Reading a printed variable byte integer gives the number back, below 2^28 | `Spec.decVBI_printVBI` | +| A remaining length needing a fifth byte is refused | `Spec.rejects_five_byte_remaining_length` | +| A SUBSCRIBE with flags other than 0010 is refused | `Spec.rejects_subscribe_flags` | +| A PUBLISH with the reserved QoS value 3 is refused | `Spec.rejects_publish_qos3` | +| A PUBLISH topic name holding a wildcard is refused | `Spec.rejects_wildcard_topic` | +| A CONNECT with a protocol name other than `MQTT` is refused | `Spec.rejects_wrong_protocol_name` | +| A CONNECT with the reserved connect flag bit set is refused | `Spec.rejects_reserved_connect_flag` | +| A property on a packet type that does not allow it is refused | `Spec.rejects_property_wrong_type` | +| A single use property standing twice in one block is refused | `Spec.rejects_repeated_property` | +| A SUBSCRIBE with packet identifier 0 is refused | `Spec.rejects_subscribe_id_zero` | +| A PINGREQ with a body is refused | `Spec.rejects_pingreq_body` | +| A packet type outside the seven in this slice is refused | `Spec.rejects_unknown_type` | diff --git a/Spec.lean b/Spec.lean new file mode 100644 index 0000000..b2e91c7 --- /dev/null +++ b/Spec.lean @@ -0,0 +1,115 @@ +/- + The specification as Lean statements: the challenge file. + + A reviewer who did not write this file approves it, and `bar.toml` + records the SHA-256 it had then. The proofs live in `Proofs` + (`Proofs/SpecProofs.lean`); `lake comparator` checks that each one + proves exactly the statement written here. The `sorry` below is + expected in this file only. + + The statements use only the definitions in `Mqtt/Value.lean`, + `Mqtt/Parse.lean`, and `Mqtt/Utf8.lean`, the code under proof + named in `bar.toml`. No definition of their own is needed, so + this project has no `Spec/Defs.lean`. +-/ + +import Mqtt + +open Mqtt + +/-! ## The round trips + +The statements the slice stands on. Each one is the statement of +the proved theorem of the same shape in `Proofs/RoundTrip.lean`, +over the same well formedness predicate, `Mqtt.PacketWF`. -/ + +/-- Parsing the printed form of a well formed packet, with more + stream bytes after it, gives the packet and those bytes back. + So a printer that wrote nothing, or wrote something shorter, + fails this statement. -/ +theorem Spec.parsePacket_print (p : Packet) (rest : List UInt8) + (h : PacketWF p) : + parsePacket (print p ++ rest) = some (p, rest) := sorry + +/-- Parsing the printed form of a well formed packet on its own + gives the packet back. -/ +theorem Spec.parse_print (p : Packet) (h : PacketWF p) : + parse (print p) = some p := sorry + +/-- Reading a printed variable byte integer gives the number + back, for every value below 2^28, the most four bytes carry. -/ +theorem Spec.decVBI_printVBI (n : Nat) (rest : List UInt8) + (hn : n < 268435456) : + decVBI (printVBI n ++ rest) = some (n, rest) := sorry + +/-! ## Refused inputs + +Single inputs the reader refuses, one for each headline rule of +`SPEC.md`. Each input is one of the named rejection cases in the +test harness. The differential tests cover these rules on many +more inputs; these statements pin them so a reader of the +specification can check each rule against one concrete case. -/ + +/-- A remaining length whose fourth byte carries a continuation + mark is refused: the value would need a fifth byte, and four + is the limit. -/ +theorem Spec.rejects_five_byte_remaining_length : + (parse ([192, 255, 255, 255, 255, 127] : List UInt8)).isSome + = false := sorry + +/-- A SUBSCRIBE packet with flags 0000 is refused: the value the + standard fixes for SUBSCRIBE is 0010. -/ +theorem Spec.rejects_subscribe_flags : + (parse ([128, 7, 0, 1, 0, 0, 1, 97, 0] : List UInt8)).isSome + = false := sorry + +/-- A PUBLISH packet with QoS 3 is refused: that QoS value is + reserved. -/ +theorem Spec.rejects_publish_qos3 : + (parse ([54, 7, 0, 1, 97, 0, 1, 0, 120] : List UInt8)).isSome + = false := sorry + +/-- A PUBLISH topic name holding a wildcard is refused: `a/#` is + a filter, not a topic name. -/ +theorem Spec.rejects_wildcard_topic : + (parse ([48, 7, 0, 3, 97, 47, 35, 0, 120] : List UInt8)).isSome + = false := sorry + +/-- A CONNECT whose protocol name is not `MQTT` is refused. -/ +theorem Spec.rejects_wrong_protocol_name : + (parse ([16, 14, 0, 4, 77, 81, 84, 85, 5, 2, 0, 0, 0, 0, 1, 120] + : List UInt8)).isSome = false := sorry + +/-- A CONNECT with the reserved bit of the connect flags byte + set is refused. -/ +theorem Spec.rejects_reserved_connect_flag : + (parse ([16, 14, 0, 4, 77, 81, 84, 84, 5, 3, 0, 0, 0, 0, 1, 120] + : List UInt8)).isSome = false := sorry + +/-- A property standing on a packet type that does not allow it + is refused: here a subscription identifier on a CONNECT. -/ +theorem Spec.rejects_property_wrong_type : + (parse ([16, 16, 0, 4, 77, 81, 84, 84, 5, 2, 0, 0, 2, 11, 5, 0, + 1, 120] : List UInt8)).isSome = false := sorry + +/-- A single use property standing twice in one block is + refused: here the topic alias on a PUBLISH, twice. -/ +theorem Spec.rejects_repeated_property : + (parse ([50, 12, 0, 1, 97, 0, 3, 6, 35, 0, 1, 35, 0, 2] + : List UInt8)).isSome = false := sorry + +/-- A SUBSCRIBE with packet identifier 0 is refused: + identifiers are never 0. -/ +theorem Spec.rejects_subscribe_id_zero : + (parse ([130, 7, 0, 0, 0, 0, 1, 97, 0] : List UInt8)).isSome + = false := sorry + +/-- A PINGREQ with a body is refused: its remaining length must + be 0. -/ +theorem Spec.rejects_pingreq_body : + (parse ([192, 1, 0] : List UInt8)).isSome = false := sorry + +/-- A packet type outside the seven in this slice is refused: + here type 2. -/ +theorem Spec.rejects_unknown_type : + (parse ([32, 0] : List UInt8)).isSome = false := sorry diff --git a/bar.toml b/bar.toml new file mode 100644 index 0000000..d1edcaa --- /dev/null +++ b/bar.toml @@ -0,0 +1,67 @@ +# Read by bar/check.py in Proven-Commons/mission. +# See playbook/verified-bar.md there for what each field means. + +[project] +name = "mqtt" +# "in-progress" until every bar item passes, then "verified". +status = "in-progress" +page = "README.md" +# GitHub handles of everyone who wrote the specification. +spec_authors = ["abu-aska"] +# The program people run. A change to it voids the approval. +entry_points = ["Main.lean"] + +[spec] +files = ["SPEC.md", "Spec.lean"] +# The code under proof: the functions the statements are about. +code = [ + # The data types the statements are about, and their constructors. + "Mqtt.PropType", "Mqtt.PropVal", "Mqtt.PropVal.byte", + "Mqtt.PropVal.twoByte", "Mqtt.PropVal.fourByte", "Mqtt.PropVal.varByte", + "Mqtt.PropVal.utf8", "Mqtt.PropVal.utf8Pair", "Mqtt.PropVal.binary", + "Mqtt.Property", "Mqtt.PropSet", "Mqtt.SubOpts", "Mqtt.Will", + "Mqtt.Connect", "Mqtt.Publish", "Mqtt.Packet", "Mqtt.Packet.connect", + "Mqtt.Packet.publish", "Mqtt.Packet.subscribe", "Mqtt.Packet.suback", + "Mqtt.Packet.pingreq", "Mqtt.Packet.pingresp", "Mqtt.Packet.disconnect", + # The property table. + "Mqtt.valType", "Mqtt.propTypeOf", "Mqtt.allowedOf", "Mqtt.repeatableIn", + # The byte forms and the printer. + "Mqtt.writeBE", "Mqtt.printVBI", "Mqtt.printStr", "Mqtt.printBin", + "Mqtt.printPropVal", "Mqtt.printProperty", "Mqtt.printPropsList", + "Mqtt.printProps", "Mqtt.printOptsByte", "Mqtt.connectFlags", + "Mqtt.printWillPart", "Mqtt.printOptStr", "Mqtt.printOptBin", + "Mqtt.printConnectBody", "Mqtt.publishHeader", "Mqtt.printIdOpt", + "Mqtt.printPublishBody", "Mqtt.printFilter", "Mqtt.printFilters", + "Mqtt.printSubscribeBody", "Mqtt.printSubackBody", "Mqtt.bodyOf", + "Mqtt.headerOf", "Mqtt.print", + # Well formedness. + "Mqtt.hasNul", "Mqtt.StrWF", "Mqtt.BinWF", "Mqtt.TopicWF", "Mqtt.ValWF", + "Mqtt.PropsWF", "Mqtt.PropsBlockWF", "Mqtt.WillWF", "Mqtt.ConnectWF", + "Mqtt.PublishWF", "Mqtt.OptsWF", "Mqtt.FiltersWF", "Mqtt.PacketFieldsWF", + "Mqtt.PacketWF", + # The strict UTF-8 codec the string reader rests on. + "Mqtt.Utf8.encodeChar", "Mqtt.Utf8.encode", "Mqtt.Utf8.contVal", + "Mqtt.Utf8.decode", + # The length checked readers and the parser. + "Mqtt.readNat", "Mqtt.readBytes", "Mqtt.readByte", "Mqtt.decVBIGo", + "Mqtt.decVBI", "Mqtt.checkChars", "Mqtt.readStr", "Mqtt.readBin", + "Mqtt.readPropVal", "Mqtt.readEntry", "Mqtt.readEntriesGo", + "Mqtt.readEntries", "Mqtt.readProps", "Mqtt.readOptsByte", + "Mqtt.readFiltersGo", "Mqtt.flagBit", "Mqtt.checkTopic", + "Mqtt.readWillPart", "Mqtt.readOptStrField", "Mqtt.readOptBinField", + "Mqtt.readConnectBody", "Mqtt.readPacketId", "Mqtt.readPublishBody", + "Mqtt.readSubscribeBody", "Mqtt.readSubackBody", "Mqtt.readDisconnectBody", + "Mqtt.parseBody", "Mqtt.parsePacket", "Mqtt.parse", +] + +# One entry per approval, added in a pull request the reviewer approves. +# [[spec.approval]] +# reviewer = "github-handle" +# date = "2026-11-02" +# sha256 = "..." +# record = "https://github.com/Proven-Commons/mqtt/pull/" + +[tests] +results = "tests/TEST-RESULTS.md" +command = "python3 tests/run_tests.py" +files = ["tests/run_tests.py"] diff --git a/comparator.json b/comparator.json new file mode 100644 index 0000000..72b4ed5 --- /dev/null +++ b/comparator.json @@ -0,0 +1 @@ +{"challenge_module":"Spec","permitted_axioms":["propext","Classical.choice","Quot.sound"],"solution_module":"Proofs","theorem_names":["Spec.parsePacket_print","Spec.parse_print","Spec.decVBI_printVBI","Spec.rejects_five_byte_remaining_length","Spec.rejects_subscribe_flags","Spec.rejects_publish_qos3","Spec.rejects_wildcard_topic","Spec.rejects_wrong_protocol_name","Spec.rejects_reserved_connect_flag","Spec.rejects_property_wrong_type","Spec.rejects_repeated_property","Spec.rejects_subscribe_id_zero","Spec.rejects_pingreq_body","Spec.rejects_unknown_type"]} \ No newline at end of file diff --git a/lakefile.toml b/lakefile.toml index 2a89053..b5601e5 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -8,6 +8,9 @@ name = "Mqtt" [[lean_lib]] name = "Proofs" +[[lean_lib]] +name = "Spec" + [[lean_exe]] name = "mqtt" root = "Main"