diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..01f8cdb --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +.lake/ diff --git a/Cbor.lean b/Cbor.lean new file mode 100644 index 0000000..f84c2d0 --- /dev/null +++ b/Cbor.lean @@ -0,0 +1,5 @@ +/- + CBOR (RFC 8949), definite length items: the code under proof. +-/ +import Cbor.Utf8 +import Cbor.Basic diff --git a/Cbor/Basic.lean b/Cbor/Basic.lean new file mode 100644 index 0000000..dfcb353 --- /dev/null +++ b/Cbor/Basic.lean @@ -0,0 +1,258 @@ +/- + The CBOR item type, the encoder, and the decoder, for the first + slice of RFC 8949: definite length unsigned and negative integers, + byte strings, text strings, arrays, and maps, with the simple values + false, true, and null. + + The decoder is strict. It accepts only the preferred form of each + argument (RFC 8949, section 4.2.1): an argument that fits in fewer + bytes must not be sent in a longer form. It turns away every out of + slice shape: indefinite length items, tags, floating point values, + undefined, other simple values, and break. A text payload that is + not well-formed UTF-8 (RFC 3629) is turned away, as RFC 8949 asks. + + A text item holds its UTF-8 payload bytes. Converting those bytes to + and from a string happens at the edges, outside this slice. +-/ + +import Cbor.Utf8 + +namespace Cbor + +/-- One CBOR data item, in the slice. -/ +inductive Value where + /-- Unsigned integer, major type 0. -/ + | uint (n : UInt64) + /-- Negative integer, major type 1: the integer -1 - n. -/ + | nint (n : UInt64) + /-- Byte string, major type 2. -/ + | bytes (bs : List UInt8) + /-- Text string, major type 3, held as its UTF-8 payload bytes. -/ + | text (bs : List UInt8) + /-- Array, major type 4. -/ + | array (xs : List Value) + /-- Map, major type 5: a list of key and value pairs. -/ + | map (kvs : List (Value × Value)) + | vfalse | vtrue | vnull + + +/-! ## Well-formedness and depth -/ + +mutual +/-- Does an item fit on the wire in this slice: every text payload is + well-formed UTF-8, and every string and container length fits in + 64 bits. Any item small enough to exist in memory passes. -/ +def Value.wf : Value → Bool + | .uint _ => Bool.true + | .nint _ => Bool.true + | .bytes bs => bs.length < 2 ^ 64 + | .text bs => Utf8.valid bs && (bs.length < 2 ^ 64) + | .array xs => xs.length < 2 ^ 64 && Value.wfAll xs + | .map kvs => kvs.length < 2 ^ 64 && Value.wfPairs kvs + | .vfalse => Bool.true + | .vtrue => Bool.true + | .vnull => Bool.true + +def Value.wfAll : List Value → Bool + | [] => true + | x :: xs => x.wf && Value.wfAll xs + +def Value.wfPairs : List (Value × Value) → Bool + | [] => true + | (k, v) :: kvs => k.wf && v.wf && Value.wfPairs kvs +end + +mutual +/-- The nesting depth of an item: a leaf is 1, and a container is one + more than the deepest item it holds. Each level of nesting takes + at least one byte on the wire, so the depth never exceeds the + encoding length. -/ +def Value.depth : Value → Nat + | .array xs => 1 + Value.depthList xs + | .map kvs => 1 + Value.depthPairs kvs + | _ => 1 + +def Value.depthList : List Value → Nat + | [] => 0 + | x :: xs => max x.depth (Value.depthList xs) + +def Value.depthPairs : List (Value × Value) → Nat + | [] => 0 + | (k, v) :: kvs => max (max k.depth v.depth) (Value.depthPairs kvs) +end + +/-! ## The encoder -/ + +/-- Big-endian bytes of a number, in exactly `n` bytes. -/ +def beBytes : Nat → Nat → List UInt8 + | 0, _ => [] + | n + 1, x => beBytes n (x / 256) ++ [(x % 256).toUInt8] + +/-- The head of an item: the initial byte for a major type and its + argument, in the preferred form of RFC 8949, section 4.2.1. -/ +def head (mt : Nat) (arg : Nat) : List UInt8 := + let m : UInt8 := (mt * 32).toUInt8 + if arg < 24 then [m + arg.toUInt8] + else if arg ≤ 0xFF then [m + 24, arg.toUInt8] + else if arg ≤ 0xFFFF then [m + 25] ++ beBytes 2 arg + else if arg ≤ 0xFFFFFFFF then [m + 26] ++ beBytes 4 arg + else [m + 27] ++ beBytes 8 arg + +mutual +/-- Encode one item. -/ +def encode : Value → List UInt8 + | .uint n => head 0 n.toNat + | .nint n => head 1 n.toNat + | .bytes bs => head 2 bs.length ++ bs + | .text bs => head 3 bs.length ++ bs + | .array xs => head 4 xs.length ++ encodeList xs + | .map kvs => head 5 kvs.length ++ encodePairs kvs + | .vfalse => [0xf4] + | .vtrue => [0xf5] + | .vnull => [0xf6] + +def encodeList : List Value → List UInt8 + | [] => [] + | x :: xs => encode x ++ encodeList xs + +def encodePairs : List (Value × Value) → List UInt8 + | [] => [] + | (k, v) :: kvs => encode k ++ encode v ++ encodePairs kvs +end + +/-! ## The decoder -/ + +/-- Read big-endian bytes as a number. -/ +def readBe (bs : List UInt8) : Nat := bs.foldl (fun a b => a * 256 + b.toNat) 0 + +/-- Read the argument after an initial byte, given the added + information `ai`. Returns the argument and the rest of the input. + Only the preferred form is accepted: an argument written in more + bytes than it needs is turned away, as is added information the + RFC holds back (28 to 30) and the indefinite form (31). -/ +def readArg (ai : Nat) (rest : List UInt8) : Option (Nat × List UInt8) := + if ai ≤ 23 then some (ai, rest) + else if ai = 24 then + match rest with + | b :: r => if b.toNat ≥ 24 then some (b.toNat, r) else none + | [] => none + else if ai = 25 then + let (w, r) := rest.splitAt 2 + if w.length = 2 ∧ readBe w ≥ 2 ^ 8 then some (readBe w, r) else none + else if ai = 26 then + let (w, r) := rest.splitAt 4 + if w.length = 4 ∧ readBe w ≥ 2 ^ 16 then some (readBe w, r) else none + else if ai = 27 then + let (w, r) := rest.splitAt 8 + if w.length = 8 ∧ readBe w ≥ 2 ^ 32 then some (readBe w, r) else none + else none + +/-- Decode `n` items in a row, using `dec` to decode each one. -/ +def decodeItems (dec : List UInt8 → Option (Value × List UInt8)) : + Nat → List UInt8 → Option (List Value × List UInt8) + | 0, bs => some ([], bs) + | n + 1, bs => + match dec bs with + | none => none + | some (x, r) => + match decodeItems dec n r with + | none => none + | some (xs, r') => some (x :: xs, r') + +/-- Decode `n` key and value pairs in a row, using `dec` to decode + each item. -/ +def decodePairs (dec : List UInt8 → Option (Value × List UInt8)) : + Nat → List UInt8 → Option (List (Value × Value) × List UInt8) + | 0, bs => some ([], bs) + | n + 1, bs => + match dec bs with + | none => none + | some (k, r) => + match dec r with + | none => none + | some (v, r') => + match decodePairs dec n r' with + | none => none + | some (kvs, r'') => some ((k, v) :: kvs, r'') + +/-- Decode one item from the front of the input, returning the item + and the unread rest. `fuel` bounds the nesting depth the decoder + will follow; the caller passes one more than the input length, + which is always enough, since each level of nesting takes at least + one byte. -/ +def decodeFuel : Nat → List UInt8 → Option (Value × List UInt8) + | 0, _ => none + | _ + 1, [] => none + | fuel + 1, b :: rest => + let mt := b.toNat / 32 + let ai := b.toNat % 32 + if mt = 7 then + if b.toNat = 0xf4 then some (.vfalse, rest) + else if b.toNat = 0xf5 then some (.vtrue, rest) + else if b.toNat = 0xf6 then some (.vnull, rest) + else none + else if mt = 6 then none + else match readArg ai rest with + | none => none + | some (arg, r) => + if mt = 0 then some (.uint (UInt64.ofNat arg), r) + else if mt = 1 then some (.nint (UInt64.ofNat arg), r) + else if mt = 2 then + if r.length < arg then none + else some (.bytes (r.take arg), r.drop arg) + else if mt = 3 then + if r.length < arg then none + else + let p := r.take arg + if Utf8.valid p then some (.text p, r.drop arg) else none + else if mt = 4 then + match decodeItems (decodeFuel fuel) arg r with + | some (xs, r') => some (.array xs, r') + | none => none + else if mt = 5 then + match decodePairs (decodeFuel fuel) arg r with + | some (kvs, r') => some (.map kvs, r') + | none => none + else none + +/-- Decode exactly one item spanning the whole input. Anything the + decoder does not accept is `none`: out of slice shapes, a text + payload that is not well-formed UTF-8, a non-preferred argument, + bytes left over, or input that ends inside an item. -/ +def decode (bs : List UInt8) : Option Value := + match decodeFuel (bs.length + 1) bs with + | some (v, []) => some v + | _ => none + +/-! ## Printing, for the command line tool -/ + +/-- Lowercase hex of a byte list, as Python's `bytes.hex()` writes it. -/ +def hexOf (bs : List UInt8) : String := + let digits := "0123456789abcdef".toList + let pair (b : UInt8) := [digits.getD (b.toNat / 16) '?', digits.getD (b.toNat % 16) '?'] + String.ofList (bs.flatMap pair) + +mutual +/-- The canonical text form of an item, for the differential tests. + Text payloads print as hex, so byte comparisons stay exact. -/ +def Value.canonical : Value → String + | .uint n => toString n.toNat + | .nint n => "-" ++ toString (n.toNat + 1) + | .bytes bs => "h'" ++ hexOf bs ++ "'" + | .text bs => "t'" ++ hexOf bs ++ "'" + | .array xs => "[" ++ String.intercalate "," (Value.canonList xs) ++ "]" + | .map kvs => "{" ++ String.intercalate "," (Value.canonPairs kvs) ++ "}" + | .vfalse => "false" + | .vtrue => "true" + | .vnull => "null" + +def Value.canonList : List Value → List String + | [] => [] + | x :: xs => x.canonical :: Value.canonList xs + +def Value.canonPairs : List (Value × Value) → List String + | [] => [] + | (k, v) :: kvs => (k.canonical ++ ":" ++ v.canonical) :: Value.canonPairs kvs +end + +end Cbor diff --git a/Cbor/Utf8.lean b/Cbor/Utf8.lean new file mode 100644 index 0000000..da41479 --- /dev/null +++ b/Cbor/Utf8.lean @@ -0,0 +1,48 @@ +/- + A UTF-8 validator, written from the well-formed byte condition table + of RFC 3629, page 4 (the same table Unicode's UAX #31-independent + definition uses). It turns away overlong forms, surrogate halves, + values past U+10FFFF, leading bytes with no valid continuation, and + sequences cut short by the end of the input. +-/ + +namespace Cbor.Utf8 + +/-- One continuation byte: 0x80 to 0xBF. -/ +def cont (b : UInt8) : Bool := 0x80 ≤ b.toNat ∧ b.toNat ≤ 0xBF + +/-- Is this byte string well-formed UTF-8, per the RFC 3629 table? -/ +def valid : List UInt8 → Bool + | [] => true + | b :: rest => + let n := b.toNat + if n ≤ 0x7F then valid rest + else if 0xC2 ≤ n ∧ n ≤ 0xDF then + match rest with + | c1 :: r => cont c1 && valid r + | [] => false + else if n = 0xE0 then + match rest with + | c1 :: c2 :: r => (0xA0 ≤ c1.toNat ∧ c1.toNat ≤ 0xBF) && cont c2 && valid r + | _ => false + else if (0xE1 ≤ n ∧ n ≤ 0xEC) ∨ n = 0xEE ∨ n = 0xEF then + match rest with + | c1 :: c2 :: r => cont c1 && cont c2 && valid r + | _ => false + else if n = 0xED then + match rest with + | c1 :: c2 :: r => (0x80 ≤ c1.toNat ∧ c1.toNat ≤ 0x9F) && cont c2 && valid r + | _ => false + else if n = 0xF0 then + match rest with + | c1 :: c2 :: c3 :: r => (0x90 ≤ c1.toNat ∧ c1.toNat ≤ 0xBF) && cont c2 && cont c3 && valid r + | _ => false + else if 0xF1 ≤ n ∧ n ≤ 0xF3 then + match rest with + | c1 :: c2 :: c3 :: r => cont c1 && cont c2 && cont c3 && valid r + | _ => false + else if n = 0xF4 then + match rest with + | c1 :: c2 :: c3 :: r => (0x80 ≤ c1.toNat ∧ c1.toNat ≤ 0x8F) && cont c2 && cont c3 && valid r + | _ => false + else false diff --git a/Main.lean b/Main.lean new file mode 100644 index 0000000..2bf23f0 --- /dev/null +++ b/Main.lean @@ -0,0 +1,70 @@ +/- + Command line front end for the CBOR codec. It reads one request per + line on stdin and writes one answer per line, so the differential + tests can drive millions of cases through one process. + + d Decode the bytes. Prints the item in canonical form, or + `error` for anything the decoder turns away. + r Decode, then encode again. Prints the lowercase hex of + the encoding, or `error`. + + Hex is two lowercase or uppercase digits per byte, with nothing + between them. A line that is not a well-formed request prints + `error`. +-/ + +import Cbor + +open Cbor + +/-- Parse hex text into bytes. Accepts either case; anything else, + including an odd number of digits, is `none`. -/ +def parseHex : List Char → Option (List UInt8) + | [] => some [] + | c1 :: c2 :: rest => do + let digit (c : Char) : Option Nat := + if '0' ≤ c ∧ c ≤ '9' then some (c.toNat - '0'.toNat) + else if 'a' ≤ c ∧ c ≤ 'f' then some (c.toNat - 'a'.toNat + 10) + else if 'A' ≤ c ∧ c ≤ 'F' then some (c.toNat - 'A'.toNat + 10) + else none + let hi ← digit c1 + let lo ← digit c2 + let tl ← parseHex rest + some ((hi * 16 + lo).toUInt8 :: tl) + | [_] => none + +/-- Drop a trailing LF, then a trailing CR. -/ +def stripEol (s : String) : String := + let cs := s.toList + let cs := if cs.getLast? = some '\n' then cs.dropLast else cs + let cs := if cs.getLast? = some '\r' then cs.dropLast else cs + String.ofList cs + +def answer (line : String) : String := + match line.toList with + | 'd' :: ' ' :: hex => + (match parseHex hex with + | none => "error" + | some bs => + match decode bs with + | none => "error" + | some v => v.canonical) + | 'r' :: ' ' :: hex => + (match parseHex hex with + | none => "error" + | some bs => + match decode bs with + | none => "error" + | some v => hexOf (encode v)) + | _ => "error" + +partial def loop : IO Unit := do + let stdin ← IO.getStdin + let stdout ← IO.getStdout + while true do + let line ← stdin.getLine + if line.isEmpty then break + stdout.putStrLn (answer (stripEol line)) + stdout.flush + +def main : IO Unit := loop diff --git a/Proofs.lean b/Proofs.lean new file mode 100644 index 0000000..4935712 --- /dev/null +++ b/Proofs.lean @@ -0,0 +1,5 @@ +/- + The proofs: each theorem of `Spec.lean`, proved under the same name. +-/ +import Proofs.Cbor +import Proofs.RoundTrip diff --git a/Proofs/Cbor.lean b/Proofs/Cbor.lean new file mode 100644 index 0000000..6035038 --- /dev/null +++ b/Proofs/Cbor.lean @@ -0,0 +1,174 @@ +/- + The proofs for the CBOR specification. +-/ + +import Cbor +import Spec.Defs + +open Cbor + +/-! ## Generic rejection lemmas -/ + +theorem readArg_none_of_ge_28 {ai : Nat} {rest : List UInt8} (h : ai ≥ 28) : + readArg ai rest = none := by + simp only [readArg] + rw [if_neg (by omega), if_neg (by omega), if_neg (by omega), if_neg (by omega), + if_neg (by omega)] + +theorem Spec.cbor_rejects_reserved_ai (b : UInt8) (rest : List UInt8) : + b.toNat % 32 ≥ 28 → decode (b :: rest) = none := by + intro h + have hnone : decodeFuel (rest.length + 1 + 1) (b :: rest) = none := by + simp only [decodeFuel, List.length_cons] + by_cases h7 : b.toNat / 32 = 7 + · rw [if_pos h7, if_neg (by omega), if_neg (by omega), if_neg (by omega)] + · rw [if_neg h7] + by_cases h6 : b.toNat / 32 = 6 + · rw [if_pos h6] + · rw [if_neg h6, readArg_none_of_ge_28 h] + simp [decode, List.length_cons, hnone] + +theorem Spec.cbor_rejects_tags (b : UInt8) (rest : List UInt8) : + b.toNat / 32 = 6 → decode (b :: rest) = none := by + intro h + have hnone : decodeFuel (rest.length + 1 + 1) (b :: rest) = none := by + simp only [decodeFuel] + rw [if_neg (by omega), if_pos h] + simp [decode, hnone] + +theorem Spec.cbor_rejects_simple (b : UInt8) (rest : List UInt8) : + b.toNat / 32 = 7 → b.toNat ≠ 0xf4 → b.toNat ≠ 0xf5 → b.toNat ≠ 0xf6 → + decode (b :: rest) = none := by + intro h7 h4 h5 h6 + have hnone : decodeFuel (rest.length + 1 + 1) (b :: rest) = none := by + simp only [decodeFuel] + rw [if_pos h7, if_neg h4, if_neg h5, if_neg h6] + simp [decode, hnone] + +theorem Spec.cbor_rfc8949_vectors : + -- Unsigned integers + encode (.uint 0) = [0x00] ∧ decode [0x00] = some (.uint 0) ∧ + encode (.uint 1) = [0x01] ∧ decode [0x01] = some (.uint 1) ∧ + encode (.uint 10) = [0x0a] ∧ decode [0x0a] = some (.uint 10) ∧ + encode (.uint 23) = [0x17] ∧ decode [0x17] = some (.uint 23) ∧ + encode (.uint 24) = [0x18, 0x18] ∧ decode [0x18, 0x18] = some (.uint 24) ∧ + encode (.uint 25) = [0x18, 0x19] ∧ decode [0x18, 0x19] = some (.uint 25) ∧ + encode (.uint 100) = [0x18, 0x64] ∧ decode [0x18, 0x64] = some (.uint 100) ∧ + encode (.uint 1000) = [0x19, 0x03, 0xe8] ∧ decode [0x19, 0x03, 0xe8] = some (.uint 1000) ∧ + encode (.uint 1000000) = [0x1a, 0x00, 0x0f, 0x42, 0x40] ∧ + decode [0x1a, 0x00, 0x0f, 0x42, 0x40] = some (.uint 1000000) ∧ + encode (.uint 1000000000000) = [0x1b, 0x00, 0x00, 0x00, 0xe8, 0xd4, 0xa5, 0x10, 0x00] ∧ + decode [0x1b, 0x00, 0x00, 0x00, 0xe8, 0xd4, 0xa5, 0x10, 0x00] = some (.uint 1000000000000) ∧ + encode (.uint 18446744073709551615) = [0x1b, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff] ∧ + decode [0x1b, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff] = + some (.uint 18446744073709551615) ∧ + -- Negative integers: nint n is -1 - n + encode (.nint 0) = [0x20] ∧ decode [0x20] = some (.nint 0) ∧ + encode (.nint 9) = [0x29] ∧ decode [0x29] = some (.nint 9) ∧ + encode (.nint 99) = [0x38, 0x63] ∧ decode [0x38, 0x63] = some (.nint 99) ∧ + encode (.nint 999) = [0x39, 0x03, 0xe7] ∧ decode [0x39, 0x03, 0xe7] = some (.nint 999) ∧ + encode (.nint 18446744073709551615) = [0x3b, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff] ∧ + decode [0x3b, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff] = + some (.nint 18446744073709551615) ∧ + -- Byte strings + encode (.bytes []) = [0x40] ∧ decode [0x40] = some (.bytes []) ∧ + encode (.bytes [0x01, 0x02, 0x03, 0x04]) = [0x44, 0x01, 0x02, 0x03, 0x04] ∧ + decode [0x44, 0x01, 0x02, 0x03, 0x04] = some (.bytes [0x01, 0x02, 0x03, 0x04]) ∧ + -- Text strings, as their UTF-8 payload bytes + encode (.text []) = [0x60] ∧ decode [0x60] = some (.text []) ∧ + encode (.text [0x61]) = [0x61, 0x61] ∧ decode [0x61, 0x61] = some (.text [0x61]) ∧ + encode (.text [0x49, 0x45, 0x54, 0x46]) = [0x64, 0x49, 0x45, 0x54, 0x46] ∧ + decode [0x64, 0x49, 0x45, 0x54, 0x46] = some (.text [0x49, 0x45, 0x54, 0x46]) ∧ + encode (.text [0x22, 0x5c]) = [0x62, 0x22, 0x5c] ∧ + decode [0x62, 0x22, 0x5c] = some (.text [0x22, 0x5c]) ∧ + encode (.text [0xc3, 0xbc]) = [0x62, 0xc3, 0xbc] ∧ + decode [0x62, 0xc3, 0xbc] = some (.text [0xc3, 0xbc]) ∧ + encode (.text [0xe6, 0xb0, 0xb4]) = [0x63, 0xe6, 0xb0, 0xb4] ∧ + decode [0x63, 0xe6, 0xb0, 0xb4] = some (.text [0xe6, 0xb0, 0xb4]) ∧ + encode (.text [0xf0, 0x90, 0x85, 0x91]) = [0x64, 0xf0, 0x90, 0x85, 0x91] ∧ + decode [0x64, 0xf0, 0x90, 0x85, 0x91] = some (.text [0xf0, 0x90, 0x85, 0x91]) ∧ + -- Arrays + encode (.array []) = [0x80] ∧ decode [0x80] = some (.array []) ∧ + encode (.array [.uint 1, .uint 2, .uint 3]) = [0x83, 0x01, 0x02, 0x03] ∧ + decode [0x83, 0x01, 0x02, 0x03] = some (.array [.uint 1, .uint 2, .uint 3]) ∧ + encode (.array [.uint 1, .array [.uint 2, .uint 3], .array [.uint 4, .uint 5]]) = + [0x83, 0x01, 0x82, 0x02, 0x03, 0x82, 0x04, 0x05] ∧ + decode [0x83, 0x01, 0x82, 0x02, 0x03, 0x82, 0x04, 0x05] = + some (.array [.uint 1, .array [.uint 2, .uint 3], .array [.uint 4, .uint 5]]) ∧ + encode (.array ((List.range 25).map fun n => .uint (n + 1).toUInt64)) = + (0x98 :: 0x19 :: ((List.range 23).map fun n => (n + 1).toUInt8) ++ + [0x18, 0x18, 0x18, 0x19]) ∧ + -- Maps + encode (.map []) = [0xa0] ∧ decode [0xa0] = some (.map []) ∧ + encode (.map [(.uint 1, .uint 2), (.uint 3, .uint 4)]) = [0xa2, 0x01, 0x02, 0x03, 0x04] ∧ + decode [0xa2, 0x01, 0x02, 0x03, 0x04] = some (.map [(.uint 1, .uint 2), (.uint 3, .uint 4)]) ∧ + encode (.map [(.text [0x61], .uint 1), (.text [0x62], .array [.uint 2, .uint 3])]) = + [0xa2, 0x61, 0x61, 0x01, 0x61, 0x62, 0x82, 0x02, 0x03] ∧ + decode [0xa2, 0x61, 0x61, 0x01, 0x61, 0x62, 0x82, 0x02, 0x03] = + some (.map [(.text [0x61], .uint 1), (.text [0x62], .array [.uint 2, .uint 3])]) ∧ + encode (.array [.text [0x61], .map [(.text [0x62], .text [0x63])]]) = + [0x82, 0x61, 0x61, 0xa1, 0x61, 0x62, 0x61, 0x63] ∧ + decode [0x82, 0x61, 0x61, 0xa1, 0x61, 0x62, 0x61, 0x63] = + some (.array [.text [0x61], .map [(.text [0x62], .text [0x63])]]) ∧ + encode (.map [(.text [0x61], .text [0x41]), (.text [0x62], .text [0x42]), + (.text [0x63], .text [0x43]), (.text [0x64], .text [0x44]), + (.text [0x65], .text [0x45])]) = + [0xa5, 0x61, 0x61, 0x61, 0x41, 0x61, 0x62, 0x61, 0x42, 0x61, 0x63, 0x61, 0x43, + 0x61, 0x64, 0x61, 0x44, 0x61, 0x65, 0x61, 0x45] ∧ + -- Simple values + encode .vfalse = [0xf4] ∧ decode [0xf4] = some .vfalse ∧ + encode .vtrue = [0xf5] ∧ decode [0xf5] = some .vtrue ∧ + encode .vnull = [0xf6] ∧ decode [0xf6] = some .vnull := by + repeat (first | constructor | rfl) + +theorem Spec.cbor_rejects_out_of_slice : + decode [0xf7] = none ∧ + decode [0xf0] = none ∧ + decode [0xf8, 0xff] = none ∧ + decode [0xf9, 0x00, 0x00] = none ∧ + decode [0xf9, 0x3c, 0x00] = none ∧ + decode [0xfa, 0x47, 0xc3, 0x50, 0x00] = none ∧ + decode [0xfb, 0x7e, 0x37, 0xe4, 0x3c, 0x88, 0x00, 0x75, 0x9c] = none ∧ + decode [0xc0, 0x74, 0x32, 0x30, 0x31, 0x33, 0x2d, 0x30, 0x33, 0x2d, 0x32, 0x31, 0x54, + 0x32, 0x30, 0x3a, 0x30, 0x34, 0x3a, 0x30, 0x30, 0x5a] = none ∧ + decode [0xc1, 0x1a, 0x51, 0x4b, 0x67, 0xb0] = none ∧ + decode [0xc2, 0x49, 0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] = none ∧ + decode [0xc3, 0x49, 0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] = none ∧ + decode [0xd7, 0x44, 0x01, 0x02, 0x03, 0x04] = none ∧ + decode [0xd8, 0x18, 0x45, 0x64, 0x49, 0x45, 0x54, 0x46] = none ∧ + decode [0x5f, 0x42, 0x01, 0x02, 0x43, 0x03, 0x04, 0x05, 0xff] = none ∧ + decode [0x7f, 0x65, 0x73, 0x74, 0x72, 0x65, 0x61, 0x64, 0x6d, 0x69, 0x6e, 0x67, 0xff] = none ∧ + decode [0x9f, 0xff] = none ∧ + decode [0x9f, 0x01, 0x82, 0x02, 0x03, 0x9f, 0x04, 0x05, 0xff, 0xff] = none ∧ + decode [0xbf, 0x61, 0x61, 0x01, 0x61, 0x62, 0x9f, 0x02, 0x03, 0xff, 0xff] = none ∧ + decode [0xff] = none := by + repeat (first | constructor | rfl) + +theorem Spec.cbor_rejects_nonpreferred : + decode [0x18, 0x00] = none ∧ + decode [0x18, 0x17] = none ∧ + decode [0x19, 0x00, 0x18] = none ∧ + decode [0x1a, 0x00, 0x00, 0x01, 0x00] = none ∧ + decode [0x1b, 0x00, 0x00, 0x00, 0x00, 0xff, 0xff, 0xff, 0xff] = none ∧ + decode [0x38, 0x00] = none ∧ + decode [0x5a, 0x00, 0x00, 0x00, 0x04, 0x01, 0x02, 0x03, 0x04] = none := by + repeat (first | constructor | rfl) + +theorem Spec.cbor_rejects_bad_utf8 : + decode [0x61, 0x80] = none ∧ + decode [0x62, 0xc0, 0x80] = none ∧ + decode [0x62, 0xc3, 0x28] = none ∧ + decode [0x63, 0xed, 0xa0, 0x80] = none ∧ + decode [0x64, 0xf4, 0x90, 0x80, 0x80] = none := by + repeat (first | constructor | rfl) + +theorem Spec.cbor_rejects_truncation : + decode [] = none ∧ + decode [0x18] = none ∧ + decode [0x1b, 0xff, 0xff, 0xff] = none ∧ + decode [0x44, 0x01, 0x02] = none ∧ + decode [0x62, 0xc3] = none ∧ + decode [0x82, 0x01] = none ∧ + decode [0xa2, 0x01, 0x02, 0x03] = none ∧ + decode [0x01, 0x02] = none := by + repeat (first | constructor | rfl) diff --git a/Proofs/RoundTrip.lean b/Proofs/RoundTrip.lean new file mode 100644 index 0000000..462b508 --- /dev/null +++ b/Proofs/RoundTrip.lean @@ -0,0 +1,1287 @@ +/- + The round trip: decoding an encoding returns the same item. +-/ + +import Cbor +import Spec.Defs + +open Cbor + +namespace Cbor + +/-! ## List utilities -/ + +/-- Induction peeling from the right. -/ +theorem rightInduction {α : Type _} {P : List α → Prop} (h0 : P []) + (h1 : ∀ a l, P l → P (l ++ [a])) (w : List α) : P w := by + have key : ∀ w : List α, P w.reverse := by + intro w + induction w with + | nil => exact h0 + | cons a l ih => rw [List.reverse_cons]; exact h1 _ _ ih + have h := key w.reverse + rwa [List.reverse_reverse] at h + +/-! ## `readBe` and `beBytes` are inverse -/ + +theorem readBeFoldl (init : Nat) (w : List UInt8) : + w.foldl (fun a b => a * 256 + b.toNat) init = init * 256 ^ w.length + readBe w := by + induction w generalizing init with + | nil => simp [readBe] + | cons b rest ih => + rw [List.foldl_cons, ih (init * 256 + b.toNat), List.length_cons, Nat.pow_succ] + have e2 : readBe (b :: rest) = b.toNat * 256 ^ rest.length + readBe rest := by + rw [readBe, List.foldl_cons, ih (0 * 256 + b.toNat)] + simp + rw [e2, Nat.add_mul, Nat.mul_assoc, Nat.mul_comm (256 ^ rest.length) 256, + ← Nat.mul_assoc, Nat.add_assoc] + +theorem readBe_cons (b : UInt8) (rest : List UInt8) : + readBe (b :: rest) = b.toNat * 256 ^ rest.length + readBe rest := by + rw [readBe, List.foldl_cons, readBeFoldl]; simp + +theorem readBe_append_single (w : List UInt8) (b : UInt8) : + readBe (w ++ [b]) = readBe w * 256 + b.toNat := by + simp [readBe, List.foldl_append] + +theorem readBe_lt_pow (w : List UInt8) : readBe w < 256 ^ w.length := by + induction w using rightInduction with + | h0 => simp [readBe] + | h1 a l ih => + rw [List.length_append, List.length_singleton, readBe_append_single, Nat.pow_succ] + have hb : a.toNat < 256 := a.toBitVec.isLt + have hle : readBe l * 256 + 256 ≤ 256 ^ l.length * 256 := by + have h2 : readBe l + 1 ≤ 256 ^ l.length := ih + calc readBe l * 256 + 256 = (readBe l + 1) * 256 := by omega + _ ≤ 256 ^ l.length * 256 := Nat.mul_le_mul h2 (Nat.le_refl 256) + omega + +theorem beBytes_length (n x : Nat) : (beBytes n x).length = n := by + induction n generalizing x with + | zero => rfl + | succ n ih => simp [beBytes, ih] + +theorem toUInt8_toNat (b : UInt8) : (b.toNat).toUInt8 = b := by + apply (UInt8.toNat_inj).1 + have hb : b.toNat < 256 := b.toBitVec.isLt + have : ((b.toNat).toUInt8).toNat = b.toNat % 256 := by simp [Nat.toUInt8] + rw [this, Nat.mod_eq_of_lt hb] + +theorem readBe_beBytes (n x : Nat) (h : x < 256 ^ n) : readBe (beBytes n x) = x := by + induction n generalizing x with + | zero => simp at h; simp [beBytes, readBe, show x = 0 by omega] + | succ n ih => + rw [beBytes, readBe_append_single] + rw [Nat.pow_succ] at h + rw [ih (x / 256) ((Nat.div_lt_iff_lt_mul (k := 256) (x := x) (y := 256 ^ n) + (by decide : (0:Nat) < 256)).mpr h)] + have hmod : ((x % 256).toUInt8).toNat = x % 256 := by + have hlt : x % 256 < 256 := Nat.mod_lt _ (by decide) + have : ((x % 256).toUInt8).toNat = (x % 256) % 256 := by simp [Nat.toUInt8] + rw [this, Nat.mod_eq_of_lt hlt] + rw [hmod, Nat.mul_comm (x / 256) 256] + exact Nat.div_add_mod x 256 + +theorem beBytes_readBe (w : List UInt8) : beBytes w.length (readBe w) = w := by + induction w using rightInduction with + | h0 => rfl + | h1 a l ih => + rw [List.length_append, List.length_singleton, readBe_append_single, beBytes] + have hb : a.toNat < 256 := a.toBitVec.isLt + have hdiv : (readBe l * 256 + a.toNat) / 256 = readBe l := by + rw [Nat.mul_comm (readBe l) 256, Nat.mul_add_div (by decide : (0:Nat) < 256), + Nat.div_eq_of_lt hb, Nat.add_zero] + have hmod : (readBe l * 256 + a.toNat) % 256 = a.toNat := by + rw [Nat.mul_comm (readBe l) 256, Nat.mul_add_mod, Nat.mod_eq_of_lt hb] + rw [hdiv, ih, hmod, toUInt8_toNat] + +/-! ## Parsing a head written by `head` -/ + +theorem head_parse (mt arg : Nat) (rest : List UInt8) (hmt : mt ≤ 5) (harg : arg < 2 ^ 64) : + ∃ b tail, head mt arg = b :: tail ∧ b.toNat / 32 = mt ∧ b.toNat % 32 ≤ 27 ∧ + readArg (b.toNat % 32) (tail ++ rest) = some (arg, rest) := by + have hmod256 : ∀ k : UInt8, k.toNat ≤ 27 → + ((mt * 32).toUInt8 + k).toNat = mt * 32 + k.toNat := by + intro k hk + have hb : mt * 32 < 256 := by + have := Nat.mul_le_mul hmt (Nat.le_refl 32); omega + have hm : ((mt * 32).toUInt8).toNat = mt * 32 % 256 := by simp [Nat.toUInt8] + rw [UInt8.toNat_add, hm, Nat.mod_eq_of_lt hb, Nat.mod_eq_of_lt (by omega)] + have hdiv : ∀ k : UInt8, k.toNat ≤ 27 → ((mt * 32).toUInt8 + k).toNat / 32 = mt := by + intro k hk + rw [hmod256 k hk, Nat.mul_comm mt 32, Nat.mul_add_div (by decide : (32:Nat) > 0), + Nat.div_eq_of_lt (by omega), Nat.add_zero] + have hmod : ∀ k : UInt8, k.toNat ≤ 27 → ((mt * 32).toUInt8 + k).toNat % 32 = k.toNat := by + intro k hk + rw [hmod256 k hk, Nat.mul_comm mt 32, Nat.mul_add_mod, + Nat.mod_eq_of_lt (by omega)] + have htk : ∀ n : Nat, List.take n (beBytes n arg) = beBytes n arg := by + intro n + have h := List.take_length (l := beBytes n arg) + rw [beBytes_length] at h + exact h + have hdr : ∀ n : Nat, List.drop n (beBytes n arg) = [] := by + intro n + have h := List.drop_length (l := beBytes n arg) + rw [beBytes_length] at h + exact h + unfold head + by_cases h1 : arg < 24 + · rw [if_pos h1] + have e1 : (arg.toUInt8).toNat = arg := by + have : (arg.toUInt8).toNat = arg % 256 := by simp [Nat.toUInt8] + rw [this, Nat.mod_eq_of_lt (by omega)] + refine ⟨(mt * 32).toUInt8 + arg.toUInt8, [], rfl, hdiv _ (by rw [e1]; omega), + ?_, ?_⟩ + · rw [hmod _ (by rw [e1]; omega), e1]; omega + · rw [hmod _ (by rw [e1]; omega), e1] + simp only [readArg, List.nil_append, List.singleton_append] + rw [if_pos (by omega : arg ≤ 23)] + · rw [if_neg h1] + by_cases h2 : arg ≤ 0xFF + · rw [if_pos h2] + have e2 : (arg.toUInt8).toNat = arg := by + have : (arg.toUInt8).toNat = arg % 256 := by simp [Nat.toUInt8] + rw [this, Nat.mod_eq_of_lt (by omega)] + refine ⟨(mt * 32).toUInt8 + 24, [arg.toUInt8], rfl, + hdiv _ (by decide), ?_, ?_⟩ + · rw [hmod _ (by decide : (24:UInt8).toNat ≤ 27)]; decide + · rw [hmod _ (by decide : (24:UInt8).toNat ≤ 27)] + change readArg 24 (arg.toUInt8 :: rest) = some (arg, rest) + rw [Cbor.readArg.eq_def, if_neg (by decide : ¬(24:Nat) ≤ 23), if_pos rfl] + show (if (arg.toUInt8).toNat ≥ 24 then some ((arg.toUInt8).toNat, rest) + else none) = some (arg, rest) + rw [e2, if_pos (by omega : arg ≥ 24)] + · rw [if_neg h2] + by_cases h3 : arg ≤ 0xFFFF + · rw [if_pos h3] + refine ⟨(mt * 32).toUInt8 + 25, beBytes 2 arg, rfl, + hdiv _ (by decide), ?_, ?_⟩ + · rw [hmod _ (by decide : (25:UInt8).toNat ≤ 27)]; decide + · rw [hmod _ (by decide : (25:UInt8).toNat ≤ 27)] + have hb2 : arg < 65536 := by omega + change readArg 25 (beBytes 2 arg ++ rest) = some (arg, rest) + rw [Cbor.readArg.eq_def, if_neg (by decide : ¬(25:Nat) ≤ 23), + if_neg (by decide : ¬(25:Nat) = 24), if_pos rfl, List.splitAt_eq] + show (if (List.take 2 (beBytes 2 arg ++ rest)).length = 2 ∧ + readBe (List.take 2 (beBytes 2 arg ++ rest)) ≥ 2 ^ 8 + then some (readBe (List.take 2 (beBytes 2 arg ++ rest)), + List.drop 2 (beBytes 2 arg ++ rest)) else none) = some (arg, rest) + rw [List.take_append_of_le_length (by simp [beBytes_length]), htk 2, + readBe_beBytes 2 arg hb2, + List.drop_append_of_le_length (by simp [beBytes_length]), hdr 2, + List.nil_append, if_pos ⟨by rw [beBytes_length], by omega⟩] + · rw [if_neg h3] + by_cases h4 : arg ≤ 0xFFFFFFFF + · rw [if_pos h4] + refine ⟨(mt * 32).toUInt8 + 26, beBytes 4 arg, rfl, + hdiv _ (by decide), ?_, ?_⟩ + · rw [hmod _ (by decide : (26:UInt8).toNat ≤ 27)]; decide + · rw [hmod _ (by decide : (26:UInt8).toNat ≤ 27)] + have hb4 : arg < 4294967296 := by omega + change readArg 26 (beBytes 4 arg ++ rest) = some (arg, rest) + rw [Cbor.readArg.eq_def, if_neg (by decide : ¬(26:Nat) ≤ 23), + if_neg (by decide : ¬(26:Nat) = 24), if_neg (by decide : ¬(26:Nat) = 25), + if_pos rfl, List.splitAt_eq] + show (if (List.take 4 (beBytes 4 arg ++ rest)).length = 4 ∧ + readBe (List.take 4 (beBytes 4 arg ++ rest)) ≥ 2 ^ 16 + then some (readBe (List.take 4 (beBytes 4 arg ++ rest)), + List.drop 4 (beBytes 4 arg ++ rest)) else none) = some (arg, rest) + rw [List.take_append_of_le_length (by simp [beBytes_length]), htk 4, + readBe_beBytes 4 arg hb4, + List.drop_append_of_le_length (by simp [beBytes_length]), hdr 4, + List.nil_append, if_pos ⟨by rw [beBytes_length], by omega⟩] + · rw [if_neg h4] + have hb : arg < 256 ^ 8 := by + rw [show (256:Nat)^8 = 18446744073709551616 from rfl] + have harg' : arg < 18446744073709551616 := harg + omega + refine ⟨(mt * 32).toUInt8 + 27, beBytes 8 arg, rfl, + hdiv _ (by decide), ?_, ?_⟩ + · rw [hmod _ (by decide : (27:UInt8).toNat ≤ 27)]; decide + · rw [hmod _ (by decide : (27:UInt8).toNat ≤ 27)] + change readArg 27 (beBytes 8 arg ++ rest) = some (arg, rest) + rw [Cbor.readArg.eq_def, if_neg (by decide : ¬(27:Nat) ≤ 23), + if_neg (by decide : ¬(27:Nat) = 24), if_neg (by decide : ¬(27:Nat) = 25), + if_neg (by decide : ¬(27:Nat) = 26), List.splitAt_eq] + show (if (List.take 8 (beBytes 8 arg ++ rest)).length = 8 ∧ + readBe (List.take 8 (beBytes 8 arg ++ rest)) ≥ 2 ^ 32 + then some (readBe (List.take 8 (beBytes 8 arg ++ rest)), + List.drop 8 (beBytes 8 arg ++ rest)) else none) = some (arg, rest) + rw [List.take_append_of_le_length (by simp [beBytes_length]), htk 8, + readBe_beBytes 8 arg hb, + List.drop_append_of_le_length (by simp [beBytes_length]), hdr 8, + List.nil_append, if_pos ⟨by rw [beBytes_length], by omega⟩] + + +theorem head_length_pos (mt arg : Nat) : 1 ≤ (head mt arg).length := by + unfold head + dsimp only + by_cases h1 : arg < 24 + · rw [if_pos h1]; simp + · by_cases h2 : arg ≤ 255 + · rw [if_neg h1, if_pos h2]; simp + · by_cases h3 : arg ≤ 65535 + · rw [if_neg h1, if_neg h2, if_pos h3]; simp [beBytes_length] + · by_cases h4 : arg ≤ 4294967295 + · rw [if_neg h1, if_neg h2, if_neg h3, if_pos h4]; simp [beBytes_length] + · rw [if_neg h1, if_neg h2, if_neg h3, if_neg h4]; simp [beBytes_length] + +end Cbor + +/-! ## Round trip: decoding an encoding gives the item back -/ + +/-- The cons equation of the decoder, with the head lets inlined. -/ +theorem decodeFuel_cons (F : Nat) (b : UInt8) (rest : List UInt8) : + decodeFuel (F + 1) (b :: rest) = + (if b.toNat / 32 = 7 then + if b.toNat = 0xf4 then some (.vfalse, rest) + else if b.toNat = 0xf5 then some (.vtrue, rest) + else if b.toNat = 0xf6 then some (.vnull, rest) + else none + else if b.toNat / 32 = 6 then none + else match readArg (b.toNat % 32) rest with + | none => none + | some (arg, r) => + if b.toNat / 32 = 0 then some (.uint (UInt64.ofNat arg), r) + else if b.toNat / 32 = 1 then some (.nint (UInt64.ofNat arg), r) + else if b.toNat / 32 = 2 then + if r.length < arg then none + else some (.bytes (r.take arg), r.drop arg) + else if b.toNat / 32 = 3 then + if r.length < arg then none + else if Utf8.valid (r.take arg) then some (.text (r.take arg), r.drop arg) + else none + else if b.toNat / 32 = 4 then + match decodeItems (decodeFuel F) arg r with + | some (xs, r') => some (.array xs, r') + | none => none + else if b.toNat / 32 = 5 then + match decodePairs (decodeFuel F) arg r with + | some (kvs, r') => some (.map kvs, r') + | none => none + else none) := rfl + +theorem decodeItems_zero (dec : List UInt8 → Option (Value × List UInt8)) (bs : List UInt8) : + decodeItems dec 0 bs = some ([], bs) := rfl + +theorem decodeItems_succ (dec : List UInt8 → Option (Value × List UInt8)) (n : Nat) + (bs : List UInt8) : + decodeItems dec (n + 1) bs = + match dec bs with + | none => none + | some (x, r) => + match decodeItems dec n r with + | none => none + | some (xs, r') => some (x :: xs, r') := rfl + +theorem decodePairs_succ (dec : List UInt8 → Option (Value × List UInt8)) (n : Nat) + (bs : List UInt8) : + decodePairs dec (n + 1) bs = + match dec bs with + | none => none + | some (k, r) => + match dec r with + | none => none + | some (v, r') => + match decodePairs dec n r' with + | none => none + | some (kvs, r'') => some ((k, v) :: kvs, r'') := rfl + +/-- The decoder on an item head written by `head`, with major type at + most 5: the head parses back to its major type and argument. -/ +theorem decodeFuel_head (mt arg : Nat) (rest : List UInt8) (hmt : mt ≤ 5) + (harg : arg < 2 ^ 64) (F : Nat) : + decodeFuel (F + 1) (head mt arg ++ rest) = + (if mt = 0 then some (.uint (UInt64.ofNat arg), rest) + else if mt = 1 then some (.nint (UInt64.ofNat arg), rest) + else if mt = 2 then + if rest.length < arg then none + else some (.bytes (rest.take arg), rest.drop arg) + else if mt = 3 then + if rest.length < arg then none + else if Utf8.valid (rest.take arg) then some (.text (rest.take arg), rest.drop arg) + else none + else if mt = 4 then + match decodeItems (decodeFuel F) arg rest with + | some (xs, r) => some (.array xs, r) + | none => none + else if mt = 5 then + match decodePairs (decodeFuel F) arg rest with + | some (kvs, r) => some (.map kvs, r) + | none => none + else none) := by + obtain ⟨b, tail, e, hb, _hmod, hrd⟩ := head_parse mt arg rest hmt harg + rw [e, show (b :: tail) ++ rest = b :: (tail ++ rest) from rfl, decodeFuel_cons, + hb, if_neg (by omega : ¬(mt = 7)), if_neg (by omega : ¬(mt = 6)), hrd] +/-- Every item has depth at least one. -/ +theorem depth_pos (v : Value) : 1 ≤ v.depth := by + cases v <;> simp only [Value.depth] <;> omega + +/-- The depth of an item never exceeds the length of its encoding: + each level of nesting takes at least one byte on the wire. -/ +theorem depthLen : ∀ n : Nat, + (∀ v, v.depth ≤ n → v.depth ≤ (encode v).length) ∧ + (∀ xs, Value.depthList xs ≤ n → Value.depthList xs ≤ (encodeList xs).length) ∧ + (∀ kvs, Value.depthPairs kvs ≤ n → Value.depthPairs kvs ≤ (encodePairs kvs).length) := by + intro n + induction n with + | zero => + refine ⟨?_, ?_, ?_⟩ + · intro v h + have := depth_pos v + omega + · intro xs h + cases xs with + | nil => exact Nat.zero_le _ + | cons x xs => + simp only [Value.depthList] at h + have := depth_pos x + omega + · intro kvs h + cases kvs with + | nil => exact Nat.zero_le _ + | cons kv kvs => + simp only [Value.depthPairs] at h + have := depth_pos kv.1 + omega + | succ n ih => + obtain ⟨ihv, ihl, ihp⟩ := ih + have hv : ∀ v, v.depth ≤ n + 1 → v.depth ≤ (encode v).length := by + intro v h + cases v with + | uint m => + simp only [Value.depth, encode] + exact head_length_pos 0 m.toNat + | nint m => + simp only [Value.depth, encode] + exact head_length_pos 1 m.toNat + | bytes bs => + simp only [Value.depth, encode, List.length_append] + have := head_length_pos 2 bs.length + omega + | text bs => + simp only [Value.depth, encode, List.length_append] + have := head_length_pos 3 bs.length + omega + | array xs => + simp only [Value.depth] at h ⊢ + have hdl : Value.depthList xs ≤ n := by omega + have hrec := ihl xs hdl + simp only [encode, List.length_append] + have hh := head_length_pos 4 xs.length + omega + | map kvs => + simp only [Value.depth] at h ⊢ + have hdp : Value.depthPairs kvs ≤ n := by omega + have hrec := ihp kvs hdp + simp only [encode, List.length_append] + have hh := head_length_pos 5 kvs.length + omega + | vfalse => + simp only [Value.depth, encode] + decide + | vtrue => + simp only [Value.depth, encode] + decide + | vnull => + simp only [Value.depth, encode] + decide + all_goals (intro ys hcon; exact Value.noConfusion hcon) + have hl : ∀ xs, Value.depthList xs ≤ n + 1 → + Value.depthList xs ≤ (encodeList xs).length := by + intro xs + induction xs with + | nil => intro _; exact Nat.zero_le _ + | cons x xs ihx => + intro h + simp only [Value.depthList] at h ⊢ + have hx : x.depth ≤ (encode x).length := hv x (by omega) + have hxs : Value.depthList xs ≤ (encodeList xs).length := ihx (by omega) + simp only [encodeList, List.length_append] + omega + have hp : ∀ kvs, Value.depthPairs kvs ≤ n + 1 → + Value.depthPairs kvs ≤ (encodePairs kvs).length := by + intro kvs + induction kvs with + | nil => intro _; exact Nat.zero_le _ + | cons kv kvs ihk => + intro h + simp only [Value.depthPairs] at h ⊢ + have hk : kv.1.depth ≤ (encode kv.1).length := hv kv.1 (by omega) + have hvv : kv.2.depth ≤ (encode kv.2).length := hv kv.2 (by omega) + have hrest : Value.depthPairs kvs ≤ (encodePairs kvs).length := ihk (by omega) + simp only [encodePairs, List.length_append] + omega + exact ⟨hv, hl, hp⟩ + +/-- The depth of an item never exceeds the length of its encoding. -/ +theorem depth_le_length (v : Value) : v.depth ≤ (encode v).length := + (depthLen v.depth).1 v (Nat.le_refl _) + +/-- The round trip, by induction on the fuel: decoding the encoding of + a well-formed item gives the item and the rest back. -/ +theorem rtAll : ∀ F : Nat, + (∀ v rest, v.wf = true → v.depth ≤ F → + decodeFuel (F + 1) (encode v ++ rest) = some (v, rest)) ∧ + (∀ xs rest, Value.wfAll xs = true → Value.depthList xs ≤ F → + decodeItems (decodeFuel (F + 1)) xs.length (encodeList xs ++ rest) = some (xs, rest)) ∧ + (∀ kvs rest, Value.wfPairs kvs = true → Value.depthPairs kvs ≤ F → + decodePairs (decodeFuel (F + 1)) kvs.length (encodePairs kvs ++ rest) = some (kvs, rest)) := by + intro F + induction F with + | zero => + refine ⟨?_, ?_, ?_⟩ + · intro v rest _ hdepth + have := depth_pos v + omega + · intro xs rest _ hdepth + cases xs with + | nil => simp only [encodeList]; rfl + | cons x xs => + simp only [Value.depthList] at hdepth + have := depth_pos x + omega + · intro kvs rest _ hdepth + cases kvs with + | nil => simp only [encodePairs]; rfl + | cons kv kvs => + simp only [Value.depthPairs] at hdepth + have := depth_pos kv.1 + omega + | succ F ih => + obtain ⟨ihv, ihl, ihp⟩ := ih + have hv : ∀ v rest, v.wf = true → v.depth ≤ F + 1 → + decodeFuel (F + 1 + 1) (encode v ++ rest) = some (v, rest) := by + intro v rest hwf hdepth + cases v with + | uint n => + simp only [encode] + rw [decodeFuel_head 0 n.toNat rest (by decide) (UInt64.toNat_lt n) (F + 1), + if_pos rfl, UInt64.ofNat_toNat] + | nint n => + simp only [encode] + rw [decodeFuel_head 1 n.toNat rest (by decide) (UInt64.toNat_lt n) (F + 1), + if_neg (by decide : ¬(1:Nat) = 0), if_pos rfl, UInt64.ofNat_toNat] + | bytes bs => + simp only [Value.wf] at hwf + have hlen : bs.length < 2 ^ 64 := of_decide_eq_true hwf + simp only [encode] + rw [List.append_assoc, + decodeFuel_head 2 bs.length (bs ++ rest) (by decide) hlen (F + 1), + if_neg (by decide : ¬(2:Nat) = 0), if_neg (by decide : ¬(2:Nat) = 1), if_pos rfl, + if_neg (by rw [List.length_append]; omega : ¬(bs ++ rest).length < bs.length), + List.take_append_of_le_length (Nat.le_refl bs.length), List.take_length, + List.drop_append_of_le_length (Nat.le_refl bs.length), List.drop_length, + List.nil_append] + | text bs => + simp only [Value.wf, Bool.and_eq_true] at hwf + obtain ⟨hval, hlen⟩ := hwf + have hlen' : bs.length < 2 ^ 64 := of_decide_eq_true hlen + simp only [encode] + rw [List.append_assoc, + decodeFuel_head 3 bs.length (bs ++ rest) (by decide) hlen' (F + 1), + if_neg (by decide : ¬(3:Nat) = 0), if_neg (by decide : ¬(3:Nat) = 1), + if_neg (by decide : ¬(3:Nat) = 2), if_pos rfl, + if_neg (by rw [List.length_append]; omega : ¬(bs ++ rest).length < bs.length), + List.take_append_of_le_length (Nat.le_refl bs.length), List.take_length, + if_pos hval, + List.drop_append_of_le_length (Nat.le_refl bs.length), List.drop_length, + List.nil_append] + | array xs => + simp only [Value.wf, Bool.and_eq_true] at hwf + obtain ⟨hlen, hwfA⟩ := hwf + have hlen' : xs.length < 2 ^ 64 := of_decide_eq_true hlen + simp only [Value.depth] at hdepth + have hdep : Value.depthList xs ≤ F := by omega + simp only [encode] + rw [List.append_assoc, + decodeFuel_head 4 xs.length (encodeList xs ++ rest) (by decide) hlen' (F + 1), + if_neg (by decide : ¬(4:Nat) = 0), if_neg (by decide : ¬(4:Nat) = 1), + if_neg (by decide : ¬(4:Nat) = 2), if_neg (by decide : ¬(4:Nat) = 3), if_pos rfl, + ihl xs rest hwfA hdep] + | map kvs => + simp only [Value.wf, Bool.and_eq_true] at hwf + obtain ⟨hlen, hwfP⟩ := hwf + have hlen' : kvs.length < 2 ^ 64 := of_decide_eq_true hlen + simp only [Value.depth] at hdepth + have hdep : Value.depthPairs kvs ≤ F := by omega + simp only [encode] + rw [List.append_assoc, + decodeFuel_head 5 kvs.length (encodePairs kvs ++ rest) (by decide) hlen' (F + 1), + if_neg (by decide : ¬(5:Nat) = 0), if_neg (by decide : ¬(5:Nat) = 1), + if_neg (by decide : ¬(5:Nat) = 2), if_neg (by decide : ¬(5:Nat) = 3), + if_neg (by decide : ¬(5:Nat) = 4), if_pos rfl, + ihp kvs rest hwfP hdep] + | vfalse => + simp only [encode] + show decodeFuel (F + 1 + 1) (0xf4 :: rest) = some (.vfalse, rest) + rw [decodeFuel_cons, if_pos (by decide : (0xf4 : UInt8).toNat / 32 = 7), + if_pos (by decide : (0xf4 : UInt8).toNat = 0xf4)] + | vtrue => + simp only [encode] + show decodeFuel (F + 1 + 1) (0xf5 :: rest) = some (.vtrue, rest) + rw [decodeFuel_cons, if_pos (by decide : (0xf5 : UInt8).toNat / 32 = 7), + if_neg (by decide : ¬(0xf5 : UInt8).toNat = 0xf4), + if_pos (by decide : (0xf5 : UInt8).toNat = 0xf5)] + | vnull => + simp only [encode] + show decodeFuel (F + 1 + 1) (0xf6 :: rest) = some (.vnull, rest) + rw [decodeFuel_cons, if_pos (by decide : (0xf6 : UInt8).toNat / 32 = 7), + if_neg (by decide : ¬(0xf6 : UInt8).toNat = 0xf4), + if_neg (by decide : ¬(0xf6 : UInt8).toNat = 0xf5), + if_pos (by decide : (0xf6 : UInt8).toNat = 0xf6)] + have hl : ∀ xs rest, Value.wfAll xs = true → Value.depthList xs ≤ F + 1 → + decodeItems (decodeFuel (F + 1 + 1)) xs.length (encodeList xs ++ rest) = + some (xs, rest) := by + intro xs + induction xs with + | nil => intro rest _ _; simp only [encodeList]; rfl + | cons x xs ihx => + intro rest hwf hdepth + simp only [Value.wfAll, Bool.and_eq_true] at hwf + obtain ⟨hx, hxs⟩ := hwf + simp only [Value.depthList] at hdepth + have hxd : x.depth ≤ F + 1 := by omega + have hxsd : Value.depthList xs ≤ F + 1 := by omega + simp only [encodeList] + rw [List.length_cons, List.append_assoc, decodeItems_succ, + hv x (encodeList xs ++ rest) hx hxd] + show (match decodeItems (decodeFuel (F + 1 + 1)) xs.length (encodeList xs ++ rest) + with + | none => none + | some (ys, r') => some (x :: ys, r')) = some (x :: xs, rest) + rw [ihx rest hxs hxsd] + have hp : ∀ kvs rest, Value.wfPairs kvs = true → Value.depthPairs kvs ≤ F + 1 → + decodePairs (decodeFuel (F + 1 + 1)) kvs.length (encodePairs kvs ++ rest) = + some (kvs, rest) := by + intro kvs + induction kvs with + | nil => intro rest _ _; simp only [encodePairs]; rfl + | cons kv kvs ihk => + intro rest hwf hdepth + simp only [Value.wfPairs, Bool.and_eq_true] at hwf + obtain ⟨⟨hk, hvv⟩, hrest⟩ := hwf + simp only [Value.depthPairs] at hdepth + have hkd : kv.1.depth ≤ F + 1 := by omega + have hvd : kv.2.depth ≤ F + 1 := by omega + have hresd : Value.depthPairs kvs ≤ F + 1 := by omega + simp only [encodePairs] + rw [List.length_cons, List.append_assoc, List.append_assoc, decodePairs_succ, + hv kv.1 (encode kv.2 ++ (encodePairs kvs ++ rest)) hk hkd] + show (match decodeFuel (F + 1 + 1) (encode kv.2 ++ (encodePairs kvs ++ rest)) with + | none => none + | some (v', r') => + match decodePairs (decodeFuel (F + 1 + 1)) kvs.length r' with + | none => none + | some (kvs', r'') => some ((kv.1, v') :: kvs', r'')) = + some ((kv.1, kv.2) :: kvs, rest) + rw [hv kv.2 (encodePairs kvs ++ rest) hvv hvd] + show (match decodePairs (decodeFuel (F + 1 + 1)) kvs.length (encodePairs kvs ++ rest) + with + | none => none + | some (kvs', r'') => some ((kv.1, kv.2) :: kvs', r'')) = + some ((kv.1, kv.2) :: kvs, rest) + rw [ihk rest hrest hresd] + exact ⟨hv, hl, hp⟩ + +/-- Completeness: decoding the encoding of a well-formed item gives + the item back. -/ +theorem decode_encode (v : Value) (h : v.wf = true) : decode (encode v) = some v := by + obtain ⟨hv, -, -⟩ := rtAll (encode v).length + have hmain := hv v [] h (depth_le_length v) + rw [List.append_nil] at hmain + unfold decode + rw [hmain] + +/-- Decoding an encoding returns the same item: `Spec.cbor_decode_encode`. -/ +theorem Spec.cbor_decode_encode (v : Value) (h : v.wf = true) : + decode (encode v) = some v := decode_encode v h + +/-! ## Soundness: the decoder accepts nothing but encodings -/ + +/-- An initial byte whose argument `readArg` accepts is exactly the + head that `head` writes for that major type and argument. -/ +theorem head_sound (b : UInt8) (rest : List UInt8) (mt : Nat) (hmt : b.toNat / 32 = mt) + (hmt5 : mt ≤ 5) (arg : Nat) (r : List UInt8) + (h : readArg (b.toNat % 32) rest = some (arg, r)) : + b :: rest = head mt arg ++ r ∧ arg < 2 ^ 64 := by + have hbnd : b.toNat < 256 := b.toBitVec.isLt + have hb_eq : mt * 32 + b.toNat % 32 = b.toNat := by + rw [← hmt, Nat.mul_comm (b.toNat / 32) 32]; exact Nat.div_add_mod b.toNat 32 + have hb256 : mt * 32 < 256 := by + have := Nat.mul_le_mul hmt5 (Nat.le_refl 32); omega + have hm : ((mt * 32).toUInt8).toNat = mt * 32 % 256 := by simp [Nat.toUInt8] + have hbyte : ∀ k : Nat, k ≤ 27 → b.toNat % 32 = k → + b = (mt * 32).toUInt8 + k.toUInt8 := by + intro k hk1 hk2 + apply UInt8.toNat_inj.mp + have hk3 : (k.toUInt8).toNat = k % 256 := by simp [Nat.toUInt8] + rw [UInt8.toNat_add, hm, hk3, Nat.mod_eq_of_lt (by omega : k < 256), + Nat.mod_eq_of_lt hb256, Nat.mod_eq_of_lt (by omega : mt * 32 + k < 256), + ← hk2, hb_eq] + unfold readArg at h + by_cases h1 : b.toNat % 32 ≤ 23 + · rw [if_pos h1] at h + injection h with hpair; injection hpair with hga hgr + subst hgr + refine ⟨?_, by omega⟩ + rw [← hga] + unfold head + rw [if_pos (by omega : b.toNat % 32 < 24), ← hbyte (b.toNat % 32) (by omega) rfl] + rfl + · rw [if_neg h1] at h + by_cases h2 : b.toNat % 32 = 24 + · rw [if_pos h2] at h + cases rest with + | nil => simp at h + | cons b0 r' => + change (if b0.toNat ≥ 24 then some (b0.toNat, r') else none) = some (arg, r) at h + by_cases hb0 : b0.toNat ≥ 24 + · rw [if_pos hb0] at h + injection h with hpair; injection hpair with hga hgr + subst hgr + have hb0nd : b0.toNat < 256 := b0.toBitVec.isLt + refine ⟨?_, by omega⟩ + rw [← hga] + unfold head + rw [if_neg (by omega : ¬b0.toNat < 24), if_pos (by omega : b0.toNat ≤ 255), + show (24 : UInt8) = (24 : Nat).toUInt8 from UInt8.toNat_inj.mp (by decide), + ← hbyte 24 (by decide) h2, + show (b0.toNat.toUInt8) = b0 from UInt8.toNat_inj.mp (by + have e : (b0.toNat.toUInt8).toNat = b0.toNat % 256 := by simp [Nat.toUInt8] + rw [e, Nat.mod_eq_of_lt hb0nd])] + rfl + · rw [if_neg hb0] at h + simp at h + · rw [if_neg h2] at h + by_cases h3 : b.toNat % 32 = 25 + · rw [if_pos h3] at h + change (if (rest.splitAt 2).1.length = 2 ∧ readBe (rest.splitAt 2).1 ≥ 2 ^ 8 + then some (readBe (rest.splitAt 2).1, (rest.splitAt 2).2) else none) = + some (arg, r) at h + by_cases hc : (rest.splitAt 2).1.length = 2 ∧ readBe (rest.splitAt 2).1 ≥ 2 ^ 8 + · rw [if_pos hc] at h + injection h with hpair; injection hpair with hga hgr + rw [List.splitAt_eq] at hc + have hga' : readBe (rest.take 2) = arg := by + rw [List.splitAt_eq] at hga; exact hga + have hw : (rest.take 2).length = 2 := hc.1 + have hge : readBe (rest.take 2) ≥ 256 := hc.2 + have hlt : readBe (rest.take 2) ≤ 65535 := by + have := readBe_lt_pow (rest.take 2) + rw [hw, show (256:Nat) ^ 2 = 65536 from rfl] at this + omega + subst hga' + have hr2 : r = rest.drop 2 := by + rw [List.splitAt_eq] at hgr; exact hgr.symm + subst hr2 + have hbw2 : beBytes 2 (readBe (rest.take 2)) = rest.take 2 := by + have h := beBytes_readBe (rest.take 2) + rw [hw] at h + exact h + refine ⟨?_, by omega⟩ + unfold head + rw [if_neg (by omega : ¬readBe (rest.take 2) < 24), + if_neg (by omega : ¬readBe (rest.take 2) ≤ 255), + if_pos (by omega : readBe (rest.take 2) ≤ 65535), show (25 : UInt8) = (25 : Nat).toUInt8 from UInt8.toNat_inj.mp (by decide), + ← hbyte 25 (by decide) h3, + hbw2] + show b :: rest = b :: (rest.take 2 ++ rest.drop 2) + rw [List.take_append_drop] + · rw [if_neg hc] at h + simp at h + · rw [if_neg h3] at h + by_cases h4 : b.toNat % 32 = 26 + · rw [if_pos h4] at h + change (if (rest.splitAt 4).1.length = 4 ∧ readBe (rest.splitAt 4).1 ≥ 2 ^ 16 + then some (readBe (rest.splitAt 4).1, (rest.splitAt 4).2) else none) = + some (arg, r) at h + by_cases hc : (rest.splitAt 4).1.length = 4 ∧ readBe (rest.splitAt 4).1 ≥ 2 ^ 16 + · rw [if_pos hc] at h + injection h with hpair; injection hpair with hga hgr + rw [List.splitAt_eq] at hc + have hw : (rest.take 4).length = 4 := hc.1 + have hge : readBe (rest.take 4) ≥ 65536 := hc.2 + have hlt : readBe (rest.take 4) ≤ 4294967295 := by + have := readBe_lt_pow (rest.take 4) + rw [hw, show (256:Nat) ^ 4 = 4294967296 from rfl] at this + omega + have hga' : readBe (rest.take 4) = arg := by + rw [List.splitAt_eq] at hga; exact hga + subst hga' + have hr4 : r = rest.drop 4 := by rw [List.splitAt_eq] at hgr; exact hgr.symm + subst hr4 + have hbw4 : beBytes 4 (readBe (rest.take 4)) = rest.take 4 := by + have h := beBytes_readBe (rest.take 4) + rw [hw] at h + exact h + refine ⟨?_, by omega⟩ + unfold head + rw [if_neg (by omega : ¬readBe (rest.take 4) < 24), + if_neg (by omega : ¬readBe (rest.take 4) ≤ 255), + if_neg (by omega : ¬readBe (rest.take 4) ≤ 65535), + if_pos (by omega : readBe (rest.take 4) ≤ 4294967295), + show (26 : UInt8) = (26 : Nat).toUInt8 from UInt8.toNat_inj.mp (by decide), + ← hbyte 26 (by decide) h4, + hbw4] + show b :: rest = b :: (rest.take 4 ++ rest.drop 4) + rw [List.take_append_drop] + · rw [if_neg hc] at h + simp at h + · rw [if_neg h4] at h + by_cases h5 : b.toNat % 32 = 27 + · rw [if_pos h5] at h + change (if (rest.splitAt 8).1.length = 8 ∧ readBe (rest.splitAt 8).1 ≥ 2 ^ 32 + then some (readBe (rest.splitAt 8).1, (rest.splitAt 8).2) else none) = + some (arg, r) at h + by_cases hc : (rest.splitAt 8).1.length = 8 ∧ readBe (rest.splitAt 8).1 ≥ 2 ^ 32 + · rw [if_pos hc] at h + injection h with hpair; injection hpair with hga hgr + rw [List.splitAt_eq] at hc + have hw : (rest.take 8).length = 8 := hc.1 + have hge : readBe (rest.take 8) ≥ 4294967296 := hc.2 + have hlt : readBe (rest.take 8) < 2 ^ 64 := by + have := readBe_lt_pow (rest.take 8) + rw [hw, show (256:Nat) ^ 8 = 18446744073709551616 from rfl] at this + exact this + have hga' : readBe (rest.take 8) = arg := by + rw [List.splitAt_eq] at hga; exact hga + subst hga' + have hr8 : r = rest.drop 8 := by rw [List.splitAt_eq] at hgr; exact hgr.symm + subst hr8 + have hbw8 : beBytes 8 (readBe (rest.take 8)) = rest.take 8 := by + have h := beBytes_readBe (rest.take 8) + rw [hw] at h + exact h + refine ⟨?_, by omega⟩ + unfold head + rw [if_neg (by omega : ¬readBe (rest.take 8) < 24), + if_neg (by omega : ¬readBe (rest.take 8) ≤ 255), + if_neg (by omega : ¬readBe (rest.take 8) ≤ 65535), + if_neg (by omega : ¬readBe (rest.take 8) ≤ 4294967295), + show (27 : UInt8) = (27 : Nat).toUInt8 from UInt8.toNat_inj.mp (by decide), + ← hbyte 27 (by decide) h5, + hbw8] + show b :: rest = b :: (rest.take 8 ++ rest.drop 8) + rw [List.take_append_drop] + · rw [if_neg hc] at h + simp at h + · rw [if_neg h5] at h + simp at h + +/-- `decodeItems` reads exactly as many items as asked. -/ +theorem decodeItems_length (dec : List UInt8 → Option (Value × List UInt8)) : + ∀ n bs xs r, decodeItems dec n bs = some (xs, r) → xs.length = n := by + intro n + induction n with + | zero => + intro bs xs r h + rw [decodeItems_zero] at h + injection h with hpair; injection hpair with h1 h2 + rw [← h1] + rfl + | succ n ih => + intro bs xs r h + rw [decodeItems_succ] at h + split at h + · simp at h + · split at h + · simp at h + · have hrec := ih _ _ _ (by assumption) + injection h with hpair; injection hpair with h1 h2 + rw [← h1, List.length_cons, hrec] + +/-- `decodePairs` reads exactly as many pairs as asked. -/ +theorem decodePairs_length (dec : List UInt8 → Option (Value × List UInt8)) : + ∀ n bs kvs r, decodePairs dec n bs = some (kvs, r) → kvs.length = n := by + intro n + induction n with + | zero => + intro bs kvs r h + have hz : decodePairs dec 0 bs = some ([], bs) := rfl + rw [hz] at h + injection h with hpair; injection hpair with h1 h2 + rw [← h1] + rfl + | succ n ih => + intro bs kvs r h + rw [decodePairs_succ] at h + split at h + · simp at h + · split at h + · simp at h + · split at h + · simp at h + · have hrec := ih _ _ _ (by assumption) + injection h with hpair; injection hpair with h1 h2 + rw [← h1, List.length_cons, hrec] + +/-- Soundness, by induction on the fuel: whatever the decoder accepts + is the encoding of what it returns, followed by the rest. -/ +theorem soundAll : ∀ F : Nat, + (∀ bs v r, decodeFuel (F + 1) bs = some (v, r) → + v.wf = true ∧ bs = encode v ++ r) ∧ + (∀ n bs xs r, decodeItems (decodeFuel (F + 1)) n bs = some (xs, r) → + Value.wfAll xs = true ∧ bs = encodeList xs ++ r) ∧ + (∀ n bs kvs r, decodePairs (decodeFuel (F + 1)) n bs = some (kvs, r) → + Value.wfPairs kvs = true ∧ bs = encodePairs kvs ++ r) := by + intro F + induction F with + | zero => + have hl00 : ∀ n bs xs r, decodeItems (decodeFuel 0) n bs = some (xs, r) → + Value.wfAll xs = true ∧ bs = encodeList xs ++ r := by + intro n + induction n with + | zero => + intro bs xs r h + rw [decodeItems_zero] at h + injection h with hpair; injection hpair with h1 h2 + subst h1; subst h2 + exact ⟨by simp only [Value.wfAll], by simp only [encodeList]; rfl⟩ + | succ n ih => + intro bs xs r h + rw [decodeItems_succ] at h + split at h + · simp at h + · rename_i hdec + have hnone : decodeFuel 0 bs = none := rfl + rw [hnone] at hdec + simp at hdec + have hp00 : ∀ n bs kvs r, decodePairs (decodeFuel 0) n bs = some (kvs, r) → + Value.wfPairs kvs = true ∧ bs = encodePairs kvs ++ r := by + intro n + induction n with + | zero => + intro bs kvs r h + have hz : decodePairs (decodeFuel 0) 0 bs = some ([], bs) := rfl + rw [hz] at h + injection h with hpair; injection hpair with h1 h2 + subst h1; subst h2 + exact ⟨by simp only [Value.wfPairs], by simp only [encodePairs]; rfl⟩ + | succ n ih => + intro bs kvs r h + rw [decodePairs_succ] at h + split at h + · simp at h + · rename_i hdec + have hnone : decodeFuel 0 bs = none := rfl + rw [hnone] at hdec + simp at hdec + have hv0 : ∀ bs v r, decodeFuel (0 + 1) bs = some (v, r) → + v.wf = true ∧ bs = encode v ++ r := by + intro bs v r h + cases bs with + | nil => + simp only [decodeFuel] at h + simp at h + | cons b rest => + rw [decodeFuel_cons] at h + by_cases h7 : b.toNat / 32 = 7 + · rw [if_pos h7] at h + by_cases h4 : b.toNat = 0xf4 + · rw [if_pos h4] at h + injection h with hpair; injection hpair with hve hre + subst hre; subst hve + have hb : b = 0xf4 := UInt8.toNat_inj.mp h4 + exact ⟨by simp only [Value.wf], by simp only [encode]; rw [hb]; rfl⟩ + · rw [if_neg h4] at h + by_cases h5 : b.toNat = 0xf5 + · rw [if_pos h5] at h + injection h with hpair; injection hpair with hve hre + subst hre; subst hve + have hb : b = 0xf5 := UInt8.toNat_inj.mp h5 + exact ⟨by simp only [Value.wf], by simp only [encode]; rw [hb]; rfl⟩ + · rw [if_neg h5] at h + by_cases h6 : b.toNat = 0xf6 + · rw [if_pos h6] at h + injection h with hpair; injection hpair with hve hre + subst hre; subst hve + have hb : b = 0xf6 := UInt8.toNat_inj.mp h6 + exact ⟨by simp only [Value.wf], by simp only [encode]; rw [hb]; rfl⟩ + · rw [if_neg h6] at h + simp at h + · rw [if_neg h7] at h + by_cases h6 : b.toNat / 32 = 6 + · rw [if_pos h6] at h + simp at h + · rw [if_neg h6] at h + split at h + · simp at h + · rename_i arg r' hrd + by_cases h0 : b.toNat / 32 = 0 + · rw [if_pos h0] at h + injection h with hpair; injection hpair with hve hre + obtain ⟨hbs, harg64⟩ := head_sound b rest 0 h0 (by omega) arg r' hrd + subst hre; subst hve + refine ⟨by simp only [Value.wf], ?_⟩ + rw [hbs] + simp only [encode] + rw [UInt64.toNat_ofNat_of_lt' harg64] + · rw [if_neg h0] at h + by_cases h1 : b.toNat / 32 = 1 + · rw [if_pos h1] at h + injection h with hpair; injection hpair with hve hre + obtain ⟨hbs, harg64⟩ := head_sound b rest 1 h1 (by omega) arg r' hrd + subst hre; subst hve + refine ⟨by simp only [Value.wf], ?_⟩ + rw [hbs] + simp only [encode] + rw [UInt64.toNat_ofNat_of_lt' harg64] + · rw [if_neg h1] at h + by_cases h2 : b.toNat / 32 = 2 + · rw [if_pos h2] at h + by_cases hlt : r'.length < arg + · rw [if_pos hlt] at h + simp at h + · rw [if_neg hlt] at h + injection h with hpair; injection hpair with hve hre + obtain ⟨hbs, harg64⟩ := head_sound b rest 2 h2 (by omega) arg r' hrd + subst hve + have htk : (r'.take arg).length = arg := by + rw [List.length_take]; omega + refine ⟨?_, ?_⟩ + · simp only [Value.wf] + rw [htk] + exact decide_eq_true harg64 + · rw [hbs, ← hre] + simp only [encode] + rw [htk, List.append_assoc, List.take_append_drop] + · rw [if_neg h2] at h + by_cases h3 : b.toNat / 32 = 3 + · rw [if_pos h3] at h + by_cases hlt : r'.length < arg + · rw [if_pos hlt] at h + simp at h + · rw [if_neg hlt] at h + by_cases hval : Utf8.valid (r'.take arg) = true + · rw [if_pos hval] at h + injection h with hpair; injection hpair with hve hre + obtain ⟨hbs, harg64⟩ := head_sound b rest 3 h3 (by omega) arg r' hrd + subst hve + have htk : (r'.take arg).length = arg := by + rw [List.length_take]; omega + refine ⟨?_, ?_⟩ + · simp only [Value.wf, Bool.and_eq_true] + refine ⟨hval, by rw [htk]; exact decide_eq_true harg64⟩ + · rw [hbs, ← hre] + simp only [encode] + rw [htk, List.append_assoc, List.take_append_drop] + · rw [if_neg hval] at h + simp at h + · rw [if_neg h3] at h + by_cases h4 : b.toNat / 32 = 4 + · rw [if_pos h4] at h + split at h + · rename_i _ _ xs r'' hdi + injection h with hpair; injection hpair with hve hre + obtain ⟨hwfA, hbsA⟩ := hl00 arg r' xs r'' hdi + have hlen : xs.length = arg := decodeItems_length _ _ _ _ _ hdi + obtain ⟨hbs, harg64⟩ := head_sound b rest 4 h4 (by omega) arg r' hrd + subst hre; subst hve + refine ⟨?_, ?_⟩ + · simp only [Value.wf, Bool.and_eq_true] + exact ⟨by rw [hlen]; exact decide_eq_true harg64, hwfA⟩ + · rw [hbs, hbsA] + simp only [encode] + rw [hlen, List.append_assoc] + · simp at h + · rw [if_neg h4] at h + by_cases h5 : b.toNat / 32 = 5 + · rw [if_pos h5] at h + split at h + · rename_i _ _ kvs r'' hdp + injection h with hpair; injection hpair with hve hre + obtain ⟨hwfP, hbsP⟩ := hp00 arg r' kvs r'' hdp + have hlen : kvs.length = arg := decodePairs_length _ _ _ _ _ hdp + obtain ⟨hbs, harg64⟩ := head_sound b rest 5 h5 (by omega) arg r' hrd + subst hre; subst hve + refine ⟨?_, ?_⟩ + · simp only [Value.wf, Bool.and_eq_true] + exact ⟨by rw [hlen]; exact decide_eq_true harg64, hwfP⟩ + · rw [hbs, hbsP] + simp only [encode] + rw [hlen, List.append_assoc] + · simp at h + · rw [if_neg h5] at h + simp at h + have hl0 : ∀ n bs xs r, decodeItems (decodeFuel (0 + 1)) n bs = some (xs, r) → + Value.wfAll xs = true ∧ bs = encodeList xs ++ r := by + intro n + induction n with + | zero => + intro bs xs r h + rw [decodeItems_zero] at h + injection h with hpair; injection hpair with h1 h2 + subst h1; subst h2 + exact ⟨by simp only [Value.wfAll], by simp only [encodeList]; rfl⟩ + | succ n ih2 => + intro bs xs r h + rw [decodeItems_succ] at h + split at h + · simp at h + · rename_i x r1 hd + split at h + · simp at h + · rename_i xs' r'' hrec + injection h with hpair; injection hpair with h1 h2 + obtain ⟨hwfx, hbsx⟩ := hv0 bs x r1 hd + obtain ⟨hwfxs, hbsxs⟩ := ih2 r1 xs' r'' hrec + subst h2; subst h1 + refine ⟨?_, ?_⟩ + · simp only [Value.wfAll, Bool.and_eq_true] + exact ⟨hwfx, hwfxs⟩ + · simp only [encodeList] + rw [List.append_assoc, ← hbsxs, ← hbsx] + have hp0 : ∀ n bs kvs r, decodePairs (decodeFuel (0 + 1)) n bs = some (kvs, r) → + Value.wfPairs kvs = true ∧ bs = encodePairs kvs ++ r := by + intro n + induction n with + | zero => + intro bs kvs r h + have hz : decodePairs (decodeFuel (0 + 1)) 0 bs = some ([], bs) := rfl + rw [hz] at h + injection h with hpair; injection hpair with h1 h2 + subst h1; subst h2 + exact ⟨by simp only [Value.wfPairs], by simp only [encodePairs]; rfl⟩ + | succ n ih2 => + intro bs kvs r h + rw [decodePairs_succ] at h + split at h + · simp at h + · rename_i k r1 hd + split at h + · simp at h + · rename_i v' r' hdv + split at h + · simp at h + · rename_i kvs' r'' hrec + injection h with hpair; injection hpair with h1 h2 + obtain ⟨hwfk, hbsk⟩ := hv0 bs k r1 hd + obtain ⟨hwfv, hbsv⟩ := hv0 r1 v' r' hdv + obtain ⟨hwfrest, hbsrest⟩ := ih2 r' kvs' r'' hrec + subst h2; subst h1 + refine ⟨?_, ?_⟩ + · simp only [Value.wfPairs, Bool.and_eq_true] + exact ⟨⟨hwfk, hwfv⟩, hwfrest⟩ + · simp only [encodePairs] + rw [List.append_assoc, List.append_assoc, ← hbsrest, ← hbsv, ← hbsk] + exact ⟨hv0, hl0, hp0⟩ + | succ F ih => + obtain ⟨ihv, ihl, ihp⟩ := ih + have hv : ∀ bs v r, decodeFuel (F + 1 + 1) bs = some (v, r) → + v.wf = true ∧ bs = encode v ++ r := by + intro bs v r h + cases bs with + | nil => + simp only [decodeFuel] at h + simp at h + | cons b rest => + rw [decodeFuel_cons] at h + by_cases h7 : b.toNat / 32 = 7 + · rw [if_pos h7] at h + by_cases h4 : b.toNat = 0xf4 + · rw [if_pos h4] at h + injection h with hpair; injection hpair with hve hre + subst hre; subst hve + have hb : b = 0xf4 := UInt8.toNat_inj.mp h4 + exact ⟨by simp only [Value.wf], by simp only [encode]; rw [hb]; rfl⟩ + · rw [if_neg h4] at h + by_cases h5 : b.toNat = 0xf5 + · rw [if_pos h5] at h + injection h with hpair; injection hpair with hve hre + subst hre; subst hve + have hb : b = 0xf5 := UInt8.toNat_inj.mp h5 + exact ⟨by simp only [Value.wf], by simp only [encode]; rw [hb]; rfl⟩ + · rw [if_neg h5] at h + by_cases h6 : b.toNat = 0xf6 + · rw [if_pos h6] at h + injection h with hpair; injection hpair with hve hre + subst hre; subst hve + have hb : b = 0xf6 := UInt8.toNat_inj.mp h6 + exact ⟨by simp only [Value.wf], by simp only [encode]; rw [hb]; rfl⟩ + · rw [if_neg h6] at h + simp at h + · rw [if_neg h7] at h + by_cases h6 : b.toNat / 32 = 6 + · rw [if_pos h6] at h + simp at h + · rw [if_neg h6] at h + split at h + · simp at h + · rename_i arg r' hrd + by_cases h0 : b.toNat / 32 = 0 + · rw [if_pos h0] at h + injection h with hpair; injection hpair with hve hre + obtain ⟨hbs, harg64⟩ := head_sound b rest 0 h0 (by omega) arg r' hrd + subst hre; subst hve + refine ⟨by simp only [Value.wf], ?_⟩ + rw [hbs] + simp only [encode] + rw [UInt64.toNat_ofNat_of_lt' harg64] + · rw [if_neg h0] at h + by_cases h1 : b.toNat / 32 = 1 + · rw [if_pos h1] at h + injection h with hpair; injection hpair with hve hre + obtain ⟨hbs, harg64⟩ := head_sound b rest 1 h1 (by omega) arg r' hrd + subst hre; subst hve + refine ⟨by simp only [Value.wf], ?_⟩ + rw [hbs] + simp only [encode] + rw [UInt64.toNat_ofNat_of_lt' harg64] + · rw [if_neg h1] at h + by_cases h2 : b.toNat / 32 = 2 + · rw [if_pos h2] at h + by_cases hlt : r'.length < arg + · rw [if_pos hlt] at h + simp at h + · rw [if_neg hlt] at h + injection h with hpair; injection hpair with hve hre + obtain ⟨hbs, harg64⟩ := head_sound b rest 2 h2 (by omega) arg r' hrd + subst hve + have htk : (r'.take arg).length = arg := by + rw [List.length_take]; omega + refine ⟨?_, ?_⟩ + · simp only [Value.wf] + rw [htk] + exact decide_eq_true harg64 + · rw [hbs, ← hre] + simp only [encode] + rw [htk, List.append_assoc, List.take_append_drop] + · rw [if_neg h2] at h + by_cases h3 : b.toNat / 32 = 3 + · rw [if_pos h3] at h + by_cases hlt : r'.length < arg + · rw [if_pos hlt] at h + simp at h + · rw [if_neg hlt] at h + by_cases hval : Utf8.valid (r'.take arg) = true + · rw [if_pos hval] at h + injection h with hpair; injection hpair with hve hre + obtain ⟨hbs, harg64⟩ := head_sound b rest 3 h3 (by omega) arg r' hrd + subst hve + have htk : (r'.take arg).length = arg := by + rw [List.length_take]; omega + refine ⟨?_, ?_⟩ + · simp only [Value.wf, Bool.and_eq_true] + refine ⟨hval, by rw [htk]; exact decide_eq_true harg64⟩ + · rw [hbs, ← hre] + simp only [encode] + rw [htk, List.append_assoc, List.take_append_drop] + · rw [if_neg hval] at h + simp at h + · rw [if_neg h3] at h + by_cases h4 : b.toNat / 32 = 4 + · rw [if_pos h4] at h + split at h + · rename_i _ _ xs r'' hdi + injection h with hpair; injection hpair with hve hre + obtain ⟨hwfA, hbsA⟩ := ihl arg r' xs r'' hdi + have hlen : xs.length = arg := decodeItems_length _ _ _ _ _ hdi + obtain ⟨hbs, harg64⟩ := head_sound b rest 4 h4 (by omega) arg r' hrd + subst hre; subst hve + refine ⟨?_, ?_⟩ + · simp only [Value.wf, Bool.and_eq_true] + exact ⟨by rw [hlen]; exact decide_eq_true harg64, hwfA⟩ + · rw [hbs, hbsA] + simp only [encode] + rw [hlen, List.append_assoc] + · simp at h + · rw [if_neg h4] at h + by_cases h5 : b.toNat / 32 = 5 + · rw [if_pos h5] at h + split at h + · rename_i _ _ kvs r'' hdp + injection h with hpair; injection hpair with hve hre + obtain ⟨hwfP, hbsP⟩ := ihp arg r' kvs r'' hdp + have hlen : kvs.length = arg := decodePairs_length _ _ _ _ _ hdp + obtain ⟨hbs, harg64⟩ := head_sound b rest 5 h5 (by omega) arg r' hrd + subst hre; subst hve + refine ⟨?_, ?_⟩ + · simp only [Value.wf, Bool.and_eq_true] + exact ⟨by rw [hlen]; exact decide_eq_true harg64, hwfP⟩ + · rw [hbs, hbsP] + simp only [encode] + rw [hlen, List.append_assoc] + · simp at h + · rw [if_neg h5] at h + simp at h + have hl : ∀ n bs xs r, decodeItems (decodeFuel (F + 1 + 1)) n bs = some (xs, r) → + Value.wfAll xs = true ∧ bs = encodeList xs ++ r := by + intro n + induction n with + | zero => + intro bs xs r h + rw [decodeItems_zero] at h + injection h with hpair; injection hpair with h1 h2 + subst h1; subst h2 + exact ⟨by simp only [Value.wfAll], by simp only [encodeList]; rfl⟩ + | succ n ih2 => + intro bs xs r h + rw [decodeItems_succ] at h + split at h + · simp at h + · rename_i x r1 hd + split at h + · simp at h + · rename_i xs' r'' hrec + injection h with hpair; injection hpair with h1 h2 + obtain ⟨hwfx, hbsx⟩ := hv bs x r1 hd + obtain ⟨hwfxs, hbsxs⟩ := ih2 r1 xs' r'' hrec + subst h2; subst h1 + refine ⟨?_, ?_⟩ + · simp only [Value.wfAll, Bool.and_eq_true] + exact ⟨hwfx, hwfxs⟩ + · simp only [encodeList] + rw [List.append_assoc, ← hbsxs, ← hbsx] + have hp : ∀ n bs kvs r, decodePairs (decodeFuel (F + 1 + 1)) n bs = some (kvs, r) → + Value.wfPairs kvs = true ∧ bs = encodePairs kvs ++ r := by + intro n + induction n with + | zero => + intro bs kvs r h + have hz : decodePairs (decodeFuel (F + 1 + 1)) 0 bs = some ([], bs) := rfl + rw [hz] at h + injection h with hpair; injection hpair with h1 h2 + subst h1; subst h2 + exact ⟨by simp only [Value.wfPairs], by simp only [encodePairs]; rfl⟩ + | succ n ih2 => + intro bs kvs r h + rw [decodePairs_succ] at h + split at h + · simp at h + · rename_i k r1 hd + split at h + · simp at h + · rename_i v' r' hdv + split at h + · simp at h + · rename_i kvs' r'' hrec + injection h with hpair; injection hpair with h1 h2 + obtain ⟨hwfk, hbsk⟩ := hv bs k r1 hd + obtain ⟨hwfv, hbsv⟩ := hv r1 v' r' hdv + obtain ⟨hwfrest, hbsrest⟩ := ih2 r' kvs' r'' hrec + subst h2; subst h1 + refine ⟨?_, ?_⟩ + · simp only [Value.wfPairs, Bool.and_eq_true] + exact ⟨⟨hwfk, hwfv⟩, hwfrest⟩ + · simp only [encodePairs] + rw [List.append_assoc, List.append_assoc, ← hbsrest, ← hbsv, ← hbsk] + exact ⟨hv, hl, hp⟩ + +/-- Soundness: the decoder accepts nothing but encodings. -/ +theorem encode_decode (bs : List UInt8) (v : Value) (h : decode bs = some v) : + encode v = bs := by + obtain ⟨hv, -, -⟩ := soundAll bs.length + unfold decode at h + split at h + · rename_i v' hmain + obtain ⟨hwf, hbs⟩ := hv bs v' [] hmain + rw [List.append_nil] at hbs + rw [← Option.some.inj h] + exact hbs.symm + · simp at h + +/-- The decoder accepts nothing but encodings: `Spec.cbor_encode_decode`. -/ +theorem Spec.cbor_encode_decode (bs : List UInt8) (v : Value) : + decode bs = some v → encode v = bs := encode_decode bs v diff --git a/README.md b/README.md index 6e7f453..2d873ed 100644 --- a/README.md +++ b/README.md @@ -1,2 +1,97 @@ -# cbor -lean CBOR decoder (RFC 8949) +# cbor: a CBOR codec whose decoder accepts nothing but encodings + +This repo decodes and encodes a slice of RFC 8949 CBOR: definite-length +items in preferred (shortest) form. A machine-checked proof shows the +decoder accepts exactly the encodings of the slice's well-formed items, +and nothing else. + +It is a Proven Commons project, built to the verified bar published in +the org's home repo, [mission](https://github.com/Proven-Commons/mission). +Status: first slice, October 2026. + +## Run it + +Needs Lean 4.35.0 (install with elan, toolchain pinned in +`lean-toolchain`). + +``` +lake build +printf 'd 83010203\n' | .lake/build/bin/cbor +printf 'r 83010203\n' | .lake/build/bin/cbor +``` + +The tool reads one request per line. `d ` prints the item in a +canonical text form (`[1,2,3]` for the example), or `error`. `r ` +decodes and encodes again, printing the lowercase hex of the encoding; +for any input the decoder accepts, the answer is the input itself. + +## What is proved + +The round-trip theorems, in `Proofs/RoundTrip.lean`: + +- `Spec.cbor_decode_encode`: decoding the encoding of a well-formed + item returns the same item (completeness). +- `Spec.cbor_encode_decode`: if the decoder accepts bytes, those bytes + are the encoding of the item it returns (soundness). With + completeness this makes the decoder strict: it accepts exactly the + preferred-form, definite-length encodings of the slice. + +The rejection theorems, in `Proofs/Cbor.lean`: + +- `Spec.cbor_rejects_reserved_ai`: added information 28 to 31 is turned + away (reserved forms and indefinite lengths). +- `Spec.cbor_rejects_tags`: tags (major type 6) are turned away. +- `Spec.cbor_rejects_simple`: `undefined`, other simple values, every + float, and break are turned away. +- `Spec.cbor_rfc8949_vectors`: the in-slice rows of RFC 8949 Appendix A + hold in both directions. +- `Spec.cbor_rejects_out_of_slice`: the out-of-slice rows of Appendix A + are turned away. +- `Spec.cbor_rejects_nonpreferred`: a value that fits in fewer bytes + must not use a longer form. +- `Spec.cbor_rejects_bad_utf8`: text payloads that are not well-formed + UTF-8 are turned away. +- `Spec.cbor_rejects_truncation`: input that ends inside an item is + turned away. + +Axiom check: each proof depends only on the standard Lean axioms +(`propext`, `Classical.choice`, `Quot.sound`, or a subset). Full output +is recorded in `tests/TEST-RESULTS.md`. + +## The slice + +In: major types 0 (unsigned) and 1 (negative) integers up to 64 bits, +definite-length byte strings, definite-length text strings with +well-formed UTF-8 payloads, definite-length arrays and maps, and +`false`, `true`, `null`. Arguments must use the preferred (shortest) +form, as RFC 8949 section 4.2.1 defines. + +Out, always turned away: tags, indefinite-length items and break, +reserved added information 28 to 30, `undefined`, other simple values, +and every float. + +## What is not proved + +Read this before trusting the codec with real data: + +- Nothing outside the slice is handled: no tags (so no dates or + bignums), no floats, no indefinite lengths, no `undefined`. +- Maps are read and written as ordered lists of pairs. No duplicate-key + rule is applied, and no canonical key ordering is checked or produced; + RFC 8949's core deterministic encoding (section 4.2) sorts map keys, + and this slice does not. +- The CLI is a thin wrapper for the differential tests, not a file + tool. It reads requests on stdin. +- The Lean compiler, runtime, and kernel are trusted, as in every Lean + project. A bug in them is outside the proof. + +## Re-check it + +``` +lake build +python3 tests/run_tests.py +``` + +The build fails if a proof breaks. The test script rebuilds if needed, +reruns every comparison against an independent Python implementation of +the slice, and rewrites `tests/TEST-RESULTS.md`. diff --git a/SPEC.md b/SPEC.md new file mode 100644 index 0000000..9e0659d --- /dev/null +++ b/SPEC.md @@ -0,0 +1,80 @@ +# Specification: cbor + +A CBOR codec: a decoder and encoder for a slice of RFC 8949. This +specification is unreviewed: `bar.toml` lists it together with +`Spec.lean` and `Spec/Defs.lean`, and its approval section is empty +until a reviewer who did not write this specification approves it in a +pull request. + +Bytes are `List UInt8`. The command-line tool converts at the edges. + +## The slice + +RFC 8949, definite-length items only, in preferred (shortest) form +(section 4.2.1): + +- Major type 0: unsigned integers, argument range 0 to 2^64 - 1. +- Major type 1: negative integers, `-1 - n` for argument `n`. +- Major type 2: byte strings, definite length. +- Major type 3: text strings, definite length, payload required to be + well-formed UTF-8 (RFC 3629, as section 3.1 of RFC 8949 asks). +- Major type 4: arrays, definite length. +- Major type 5: maps, definite length. +- Major type 7, added information 20, 21, 22: `false`, `true`, `null`. + +Out of slice, always turned away: tags (major type 6), indefinite-length +items and break (added information 31), reserved added information 28 to +30, `undefined`, other simple values, half, single, and double floats, +and any argument not in preferred form. + +## Encoding + +Each well-formed item has exactly one encoding, given by `encode` in +`Cbor/Basic.lean`: the head is the major type and the shortest argument +form; byte and text strings follow with their payload; arrays and maps +follow with their items in order; pairs encode key then value. + +## Decoding + +`decode` reads one item and requires it to end at the last input byte. +It returns `none` for everything it does not accept: out-of-slice +initial bytes, non-preferred arguments, truncated input, text that is +not well-formed UTF-8, and bytes left over after the item. + +## What must always hold + +Each property is a theorem in `Spec.lean`, under the name given. The +statements there carry `sorry` on purpose: the proofs live under the +same names in `Proofs/`, and the build fails if any proof breaks. + +| Property | Theorem | +|----------|---------| +| Decoding an encoding returns the same item | `Spec.cbor_decode_encode` | +| The decoder accepts nothing but encodings | `Spec.cbor_encode_decode` | +| Reserved and indefinite added information is turned away | `Spec.cbor_rejects_reserved_ai` | +| Tags are turned away | `Spec.cbor_rejects_tags` | +| Other major type 7 values are turned away | `Spec.cbor_rejects_simple` | +| The in-slice RFC 8949 Appendix A vectors hold, both directions | `Spec.cbor_rfc8949_vectors` | +| Out-of-slice Appendix A rows are turned away | `Spec.cbor_rejects_out_of_slice` | +| Non-preferred arguments are turned away | `Spec.cbor_rejects_nonpreferred` | +| Text that is not well-formed UTF-8 is turned away | `Spec.cbor_rejects_bad_utf8` | +| Input that ends inside an item is turned away | `Spec.cbor_rejects_truncation` | + +With both round-trip theorems, the decoder accepts exactly the +preferred-form, definite-length encodings of the slice, and nothing else. + +## The command-line tool + +`Main.lean` reads one request per line and prints one answer per line: + +- `d ` decodes the bytes and prints the item in a canonical text + form, or `error`. The canonical form prints integers in decimal, + negative integers as `-n`, byte strings as `h''`, text strings as + `t''`, arrays as `[a,b]`, maps as `{k:v}`, + and `false`, `true`, `null`. +- `r ` decodes, then encodes again, and prints the lowercase hex + of the encoding, or `error`. For every input the decoder accepts, + soundness says the answer is the input itself. + +Hex is two lowercase or uppercase digits per byte. Any other line, +including odd-length hex, prints `error`. diff --git a/Spec.lean b/Spec.lean new file mode 100644 index 0000000..5fadfeb --- /dev/null +++ b/Spec.lean @@ -0,0 +1,185 @@ +/- + The specification as Lean statements: the challenge file. + + A reviewer who did not write this file approves it, and `bar.toml` + records the hash it had then. The proofs live in `Proofs.lean`, under + the same names. The `sorry` below is expected in this file only. + + The pinned checks for the UTF-8 validator are in `Spec/Defs.lean`, + which is part of the specification too. +-/ + +import Cbor +import Spec.Defs + +open Cbor + +/-! ## The two main claims -/ + +/-- Decoding an encoding returns the same item. (RFC 8949: the slice's + well-formed items, as `Value.wf` defines.) -/ +theorem Spec.cbor_decode_encode (v : Value) (h : v.wf = true) : + decode (encode v) = some v := sorry + +/-- The decoder accepts nothing but encodings: whatever it accepts is + the encoding of what it returns. With the claim above this makes + the decoder strict: it accepts exactly the preferred-form, + definite-length encodings of the slice, and nothing else. -/ +theorem Spec.cbor_encode_decode (bs : List UInt8) (v : Value) : + decode bs = some v → encode v = bs := sorry + +/-! ## Added information the RFC holds back, and the indefinite form -/ + +/-- An initial byte with added information 28 to 30 (reserved by + RFC 8949, section 3.1) is turned away, as is 31, the indefinite + form, which this slice does not carry. -/ +theorem Spec.cbor_rejects_reserved_ai (b : UInt8) (rest : List UInt8) : + b.toNat % 32 ≥ 28 → decode (b :: rest) = none := sorry + +/-- Tags (major type 6) are outside the slice and turned away. -/ +theorem Spec.cbor_rejects_tags (b : UInt8) (rest : List UInt8) : + b.toNat / 32 = 6 → decode (b :: rest) = none := sorry + +/-- Major type 7 carries only false, true, and null in this slice: + undefined, other simple values, every float, and break are turned + away. -/ +theorem Spec.cbor_rejects_simple (b : UInt8) (rest : List UInt8) : + b.toNat / 32 = 7 → b.toNat ≠ 0xf4 → b.toNat ≠ 0xf5 → b.toNat ≠ 0xf6 → + decode (b :: rest) = none := sorry + +/-! ## Test vectors: RFC 8949, Appendix A + +Each in-slice row, in both directions. The rows this slice turns away +(floats, tags, indefinite lengths, undefined, other simple values, +break, and bignums) are rejection theorems below; the differential +tests count every row, accepted or turned away. -/ + +theorem Spec.cbor_rfc8949_vectors : + -- Unsigned integers + encode (.uint 0) = [0x00] ∧ decode [0x00] = some (.uint 0) ∧ + encode (.uint 1) = [0x01] ∧ decode [0x01] = some (.uint 1) ∧ + encode (.uint 10) = [0x0a] ∧ decode [0x0a] = some (.uint 10) ∧ + encode (.uint 23) = [0x17] ∧ decode [0x17] = some (.uint 23) ∧ + encode (.uint 24) = [0x18, 0x18] ∧ decode [0x18, 0x18] = some (.uint 24) ∧ + encode (.uint 25) = [0x18, 0x19] ∧ decode [0x18, 0x19] = some (.uint 25) ∧ + encode (.uint 100) = [0x18, 0x64] ∧ decode [0x18, 0x64] = some (.uint 100) ∧ + encode (.uint 1000) = [0x19, 0x03, 0xe8] ∧ decode [0x19, 0x03, 0xe8] = some (.uint 1000) ∧ + encode (.uint 1000000) = [0x1a, 0x00, 0x0f, 0x42, 0x40] ∧ + decode [0x1a, 0x00, 0x0f, 0x42, 0x40] = some (.uint 1000000) ∧ + encode (.uint 1000000000000) = [0x1b, 0x00, 0x00, 0x00, 0xe8, 0xd4, 0xa5, 0x10, 0x00] ∧ + decode [0x1b, 0x00, 0x00, 0x00, 0xe8, 0xd4, 0xa5, 0x10, 0x00] = some (.uint 1000000000000) ∧ + encode (.uint 18446744073709551615) = [0x1b, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff] ∧ + decode [0x1b, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff] = + some (.uint 18446744073709551615) ∧ + -- Negative integers: nint n is -1 - n + encode (.nint 0) = [0x20] ∧ decode [0x20] = some (.nint 0) ∧ + encode (.nint 9) = [0x29] ∧ decode [0x29] = some (.nint 9) ∧ + encode (.nint 99) = [0x38, 0x63] ∧ decode [0x38, 0x63] = some (.nint 99) ∧ + encode (.nint 999) = [0x39, 0x03, 0xe7] ∧ decode [0x39, 0x03, 0xe7] = some (.nint 999) ∧ + encode (.nint 18446744073709551615) = [0x3b, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff] ∧ + decode [0x3b, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff] = + some (.nint 18446744073709551615) ∧ + -- Byte strings + encode (.bytes []) = [0x40] ∧ decode [0x40] = some (.bytes []) ∧ + encode (.bytes [0x01, 0x02, 0x03, 0x04]) = [0x44, 0x01, 0x02, 0x03, 0x04] ∧ + decode [0x44, 0x01, 0x02, 0x03, 0x04] = some (.bytes [0x01, 0x02, 0x03, 0x04]) ∧ + -- Text strings, as their UTF-8 payload bytes + encode (.text []) = [0x60] ∧ decode [0x60] = some (.text []) ∧ + encode (.text [0x61]) = [0x61, 0x61] ∧ decode [0x61, 0x61] = some (.text [0x61]) ∧ + encode (.text [0x49, 0x45, 0x54, 0x46]) = [0x64, 0x49, 0x45, 0x54, 0x46] ∧ + decode [0x64, 0x49, 0x45, 0x54, 0x46] = some (.text [0x49, 0x45, 0x54, 0x46]) ∧ + encode (.text [0x22, 0x5c]) = [0x62, 0x22, 0x5c] ∧ + decode [0x62, 0x22, 0x5c] = some (.text [0x22, 0x5c]) ∧ + encode (.text [0xc3, 0xbc]) = [0x62, 0xc3, 0xbc] ∧ + decode [0x62, 0xc3, 0xbc] = some (.text [0xc3, 0xbc]) ∧ + encode (.text [0xe6, 0xb0, 0xb4]) = [0x63, 0xe6, 0xb0, 0xb4] ∧ + decode [0x63, 0xe6, 0xb0, 0xb4] = some (.text [0xe6, 0xb0, 0xb4]) ∧ + encode (.text [0xf0, 0x90, 0x85, 0x91]) = [0x64, 0xf0, 0x90, 0x85, 0x91] ∧ + decode [0x64, 0xf0, 0x90, 0x85, 0x91] = some (.text [0xf0, 0x90, 0x85, 0x91]) ∧ + -- Arrays + encode (.array []) = [0x80] ∧ decode [0x80] = some (.array []) ∧ + encode (.array [.uint 1, .uint 2, .uint 3]) = [0x83, 0x01, 0x02, 0x03] ∧ + decode [0x83, 0x01, 0x02, 0x03] = some (.array [.uint 1, .uint 2, .uint 3]) ∧ + encode (.array [.uint 1, .array [.uint 2, .uint 3], .array [.uint 4, .uint 5]]) = + [0x83, 0x01, 0x82, 0x02, 0x03, 0x82, 0x04, 0x05] ∧ + decode [0x83, 0x01, 0x82, 0x02, 0x03, 0x82, 0x04, 0x05] = + some (.array [.uint 1, .array [.uint 2, .uint 3], .array [.uint 4, .uint 5]]) ∧ + encode (.array ((List.range 25).map fun n => .uint (n + 1).toUInt64)) = + (0x98 :: 0x19 :: ((List.range 23).map fun n => (n + 1).toUInt8) ++ + [0x18, 0x18, 0x18, 0x19]) ∧ + -- Maps + encode (.map []) = [0xa0] ∧ decode [0xa0] = some (.map []) ∧ + encode (.map [(.uint 1, .uint 2), (.uint 3, .uint 4)]) = [0xa2, 0x01, 0x02, 0x03, 0x04] ∧ + decode [0xa2, 0x01, 0x02, 0x03, 0x04] = some (.map [(.uint 1, .uint 2), (.uint 3, .uint 4)]) ∧ + encode (.map [(.text [0x61], .uint 1), (.text [0x62], .array [.uint 2, .uint 3])]) = + [0xa2, 0x61, 0x61, 0x01, 0x61, 0x62, 0x82, 0x02, 0x03] ∧ + decode [0xa2, 0x61, 0x61, 0x01, 0x61, 0x62, 0x82, 0x02, 0x03] = + some (.map [(.text [0x61], .uint 1), (.text [0x62], .array [.uint 2, .uint 3])]) ∧ + encode (.array [.text [0x61], .map [(.text [0x62], .text [0x63])]]) = + [0x82, 0x61, 0x61, 0xa1, 0x61, 0x62, 0x61, 0x63] ∧ + decode [0x82, 0x61, 0x61, 0xa1, 0x61, 0x62, 0x61, 0x63] = + some (.array [.text [0x61], .map [(.text [0x62], .text [0x63])]]) ∧ + encode (.map [(.text [0x61], .text [0x41]), (.text [0x62], .text [0x42]), + (.text [0x63], .text [0x43]), (.text [0x64], .text [0x44]), + (.text [0x65], .text [0x45])]) = + [0xa5, 0x61, 0x61, 0x61, 0x41, 0x61, 0x62, 0x61, 0x42, 0x61, 0x63, 0x61, 0x43, + 0x61, 0x64, 0x61, 0x44, 0x61, 0x65, 0x61, 0x45] ∧ + -- Simple values + encode .vfalse = [0xf4] ∧ decode [0xf4] = some .vfalse ∧ + encode .vtrue = [0xf5] ∧ decode [0xf5] = some .vtrue ∧ + encode .vnull = [0xf6] ∧ decode [0xf6] = some .vnull := sorry + +/-- Out-of-slice rows of Appendix A, turned away: undefined, other + simple values, half, single, and double floats, tags (including + the bignum tags), indefinite length items, and break. -/ +theorem Spec.cbor_rejects_out_of_slice : + decode [0xf7] = none ∧ + decode [0xf0] = none ∧ + decode [0xf8, 0xff] = none ∧ + decode [0xf9, 0x00, 0x00] = none ∧ + decode [0xf9, 0x3c, 0x00] = none ∧ + decode [0xfa, 0x47, 0xc3, 0x50, 0x00] = none ∧ + decode [0xfb, 0x7e, 0x37, 0xe4, 0x3c, 0x88, 0x00, 0x75, 0x9c] = none ∧ + decode [0xc0, 0x74, 0x32, 0x30, 0x31, 0x33, 0x2d, 0x30, 0x33, 0x2d, 0x32, 0x31, 0x54, + 0x32, 0x30, 0x3a, 0x30, 0x34, 0x3a, 0x30, 0x30, 0x5a] = none ∧ + decode [0xc1, 0x1a, 0x51, 0x4b, 0x67, 0xb0] = none ∧ + decode [0xc2, 0x49, 0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] = none ∧ + decode [0xc3, 0x49, 0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] = none ∧ + decode [0xd7, 0x44, 0x01, 0x02, 0x03, 0x04] = none ∧ + decode [0xd8, 0x18, 0x45, 0x64, 0x49, 0x45, 0x54, 0x46] = none ∧ + decode [0x5f, 0x42, 0x01, 0x02, 0x43, 0x03, 0x04, 0x05, 0xff] = none ∧ + decode [0x7f, 0x65, 0x73, 0x74, 0x72, 0x65, 0x61, 0x64, 0x6d, 0x69, 0x6e, 0x67, 0xff] = none ∧ + decode [0x9f, 0xff] = none ∧ + decode [0x9f, 0x01, 0x82, 0x02, 0x03, 0x9f, 0x04, 0x05, 0xff, 0xff] = none ∧ + decode [0xbf, 0x61, 0x61, 0x01, 0x61, 0x62, 0x9f, 0x02, 0x03, 0xff, 0xff] = none ∧ + decode [0xff] = none := sorry + +/-- Non-preferred arguments are turned away (RFC 8949, section 4.2.1): + a value that fits in fewer bytes must not use a longer form. -/ +theorem Spec.cbor_rejects_nonpreferred : + decode [0x18, 0x00] = none ∧ + decode [0x18, 0x17] = none ∧ + decode [0x19, 0x00, 0x18] = none ∧ + decode [0x1a, 0x00, 0x00, 0x01, 0x00] = none ∧ + decode [0x1b, 0x00, 0x00, 0x00, 0x00, 0xff, 0xff, 0xff, 0xff] = none ∧ + decode [0x38, 0x00] = none ∧ + decode [0x5a, 0x00, 0x00, 0x00, 0x04, 0x01, 0x02, 0x03, 0x04] = none := sorry + +/-- Text payloads that are not well-formed UTF-8 are turned away. -/ +theorem Spec.cbor_rejects_bad_utf8 : + decode [0x61, 0x80] = none ∧ + decode [0x62, 0xc0, 0x80] = none ∧ + decode [0x62, 0xc3, 0x28] = none ∧ + decode [0x63, 0xed, 0xa0, 0x80] = none ∧ + decode [0x64, 0xf4, 0x90, 0x80, 0x80] = none := sorry + +/-- Input that ends inside an item is turned away, never read past. -/ +theorem Spec.cbor_rejects_truncation : + decode [] = none ∧ + decode [0x18] = none ∧ + decode [0x1b, 0xff, 0xff, 0xff] = none ∧ + decode [0x44, 0x01, 0x02] = none ∧ + decode [0x62, 0xc3] = none ∧ + decode [0x82, 0x01] = none ∧ + decode [0xa2, 0x01, 0x02, 0x03] = none ∧ + decode [0x01, 0x02] = none := sorry diff --git a/Spec/Defs.lean b/Spec/Defs.lean new file mode 100644 index 0000000..ab24d33 --- /dev/null +++ b/Spec/Defs.lean @@ -0,0 +1,56 @@ +/- + The definitions and checks the specification uses, written from + RFC 8949 and RFC 3629, independently of the proofs. Part of the + specification for this slice, with `Spec.lean` and `SPEC.md`; the + specification is unreviewed (see `SPEC.md`). + + The `example`s pin the UTF-8 validator against the boundary cases of + RFC 3629: one example per row of its well-formed byte condition + table, plus the known attack shapes (overlong forms, surrogate + halves, values past U+10FFFF, lone continuations, truncations). A + mistake in the table fails the build. A standalone codec with the + validator proved against an independent definition is the job of the + `utf` project; this slice pins the table by examples instead. +-/ + +import Cbor + +namespace Cbor + +open Cbor + +/-! ## UTF-8 validator pins (RFC 3629) -/ + +-- One-byte and multi-byte minima and maxima. +example : Utf8.valid [0x00] = true := rfl +example : Utf8.valid [0x7F] = true := rfl +example : Utf8.valid [0xC2, 0x80] = true := rfl -- U+0080, smallest 2-byte +example : Utf8.valid [0xDF, 0xBF] = true := rfl -- U+07FF, largest 2-byte +example : Utf8.valid [0xE0, 0xA0, 0x80] = true := rfl -- U+0800, smallest 3-byte +example : Utf8.valid [0xED, 0x9F, 0xBF] = true := rfl -- U+D7FF, below surrogates +example : Utf8.valid [0xEE, 0x80, 0x80] = true := rfl -- U+E000, above surrogates +example : Utf8.valid [0xEF, 0xBF, 0xBF] = true := rfl -- U+FFFF +example : Utf8.valid [0xF0, 0x90, 0x80, 0x80] = true := rfl -- U+10000, smallest 4-byte +example : Utf8.valid [0xF4, 0x8F, 0xBF, 0xBF] = true := rfl -- U+10FFFF, the largest + +-- The attack shapes, turned away. +example : Utf8.valid [0x80] = false := rfl -- lone continuation +example : Utf8.valid [0xC0, 0xAF] = false := rfl -- overlong "/" +example : Utf8.valid [0xC1, 0xBF] = false := rfl -- overlong +example : Utf8.valid [0xC2] = false := rfl -- cut short +example : Utf8.valid [0xC2, 0x20] = false := rfl -- bad continuation +example : Utf8.valid [0xE0, 0x80, 0xAF] = false := rfl -- overlong +example : Utf8.valid [0xE0, 0xA0] = false := rfl -- cut short +example : Utf8.valid [0xED, 0xA0, 0x80] = false := rfl -- surrogate U+D800 +example : Utf8.valid [0xED, 0xBF, 0xBF] = false := rfl -- surrogate U+DFFF +example : Utf8.valid [0xF0, 0x80, 0x80, 0xAF] = false := rfl -- overlong +example : Utf8.valid [0xF0, 0x90, 0x80] = false := rfl -- cut short +example : Utf8.valid [0xF4, 0x90, 0x80, 0x80] = false := rfl -- past U+10FFFF +example : Utf8.valid [0xF5, 0x80, 0x80, 0x80] = false := rfl -- F5 is not a lead byte +example : Utf8.valid [0xFF] = false := rfl + +-- Mixed content: valid text, then one bad string. +example : Utf8.valid [0x61, 0xC3, 0xBC, 0x62] = true := rfl -- "aüb" +example : Utf8.valid [0x61, 0x80, 0x62] = false := rfl + +end Cbor diff --git a/bar.toml b/bar.toml new file mode 100644 index 0000000..ba2c86b --- /dev/null +++ b/bar.toml @@ -0,0 +1,34 @@ +# Read by bar/check.py in Proven-Commons/mission. +# See playbook/verified-bar.md there for what each field means. + +[project] +name = "cbor" +# "in-progress" until every bar item passes, then "verified". +status = "in-progress" +page = "README.md" +# GitHub handles of everyone who wrote the specification. It was drafted +# by an AI agent working for the org, from the ahrazzle account. +spec_authors = ["ahrazzle"] +# The program people run. A change to it voids the approval. +entry_points = ["Main.lean"] + +[spec] +files = ["SPEC.md", "Spec.lean", "Spec/Defs.lean"] +# The code under proof: the functions the statements are about. +code = [ + "Cbor.encode", "Cbor.encodeList", "Cbor.encodePairs", + "Cbor.decode", "Cbor.decodeFuel", "Cbor.decodeItems", "Cbor.decodePairs", + "Cbor.head", "Cbor.readArg", "Cbor.Value.wf", +] + +# 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/cbor/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..8287da9 --- /dev/null +++ b/comparator.json @@ -0,0 +1,12 @@ +{ + "challenge_module": "Spec", + "solution_module": "Proofs", + "theorem_names": [ + "Spec.cbor_decode_encode", "Spec.cbor_encode_decode", + "Spec.cbor_rejects_reserved_ai", "Spec.cbor_rejects_tags", + "Spec.cbor_rejects_simple", "Spec.cbor_rfc8949_vectors", + "Spec.cbor_rejects_out_of_slice", "Spec.cbor_rejects_nonpreferred", + "Spec.cbor_rejects_bad_utf8", "Spec.cbor_rejects_truncation" + ], + "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"] +} diff --git a/lake-manifest.json b/lake-manifest.json new file mode 100644 index 0000000..8fbcdbb --- /dev/null +++ b/lake-manifest.json @@ -0,0 +1,6 @@ +{"version": "1.3.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "cbor", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lakefile.toml b/lakefile.toml new file mode 100644 index 0000000..669f972 --- /dev/null +++ b/lakefile.toml @@ -0,0 +1,16 @@ +name = "cbor" +version = "0.1.0" +defaultTargets = ["Cbor", "Spec", "Proofs", "cbor"] + +[[lean_lib]] +name = "Cbor" + +[[lean_lib]] +name = "Spec" + +[[lean_lib]] +name = "Proofs" + +[[lean_exe]] +name = "cbor" +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..d0b958a --- /dev/null +++ b/tests/TEST-RESULTS.md @@ -0,0 +1,34 @@ +# Test results + +Run by `tests/run_tests.py` against an independent Python implementation of +the slice written from RFC 8949, in the same file, and against the RFC 8949 +Appendix A vectors. +Lean: Lean 4.35.0. Python: 3.10.12. + +- Seed: 20261025 +- Byte inputs fed to the Lean codec: 2060 +- Checks run: 2060 +- Checks passed: 2060 +- Failures: 0 +- Accepted inputs: generated well-formed items, their random-garbage + counterparts that parse, and the in-slice RFC 8949 Appendix A rows. +- Turned away: the out-of-slice Appendix A rows (floats, simple values, + `undefined`, tags including bignums, indefinite lengths, break, reserved + added information), truncations of every generated item, non-preferred + argument forms for all six major types, malformed UTF-8 text payloads, + trailing bytes after an item, and empty input. + +Axiom check (`Proofs.lean`): + +``` +'Spec.cbor_decode_encode' depends on axioms: [propext, Classical.choice, Quot.sound] +'Spec.cbor_encode_decode' depends on axioms: [propext, Quot.sound] +'Spec.cbor_rejects_reserved_ai' depends on axioms: [propext, Quot.sound] +'Spec.cbor_rejects_tags' depends on axioms: [propext, Quot.sound] +'Spec.cbor_rejects_simple' depends on axioms: [propext, Quot.sound] +'Spec.cbor_rfc8949_vectors' depends on axioms: [propext] +'Spec.cbor_rejects_out_of_slice' depends on axioms: [propext] +'Spec.cbor_rejects_nonpreferred' depends on axioms: [propext] +'Spec.cbor_rejects_bad_utf8' depends on axioms: [propext] +'Spec.cbor_rejects_truncation' depends on axioms: [propext] +``` diff --git a/tests/run_tests.py b/tests/run_tests.py new file mode 100644 index 0000000..884aab7 --- /dev/null +++ b/tests/run_tests.py @@ -0,0 +1,392 @@ +#!/usr/bin/env python3 +"""Differential tests for the Proven Commons CBOR codec. + +Compares the Lean implementation against an independent Python +implementation of the slice (below), and against the RFC 8949 +Appendix A vectors. Run from anywhere: + + python3 tests/run_tests.py + +It builds the Lean project if the executable is missing, runs all +cases, writes `tests/TEST-RESULTS.md`, and exits non-zero on failure. +""" + +import random +import subprocess +import sys +from pathlib import Path + +PILOT_DIR = Path(__file__).resolve().parent.parent +EXE = PILOT_DIR / ".lake" / "build" / "bin" / "cbor" +RESULTS = PILOT_DIR / "tests" / "TEST-RESULTS.md" +SEED = 20261025 + +checks = 0 +failures = [] +inputs = 0 +accepted = 0 +rejected = 0 + + +def check(name, ok, detail=""): + global checks + checks += 1 + if not ok: + failures.append(f"{name}: {detail}") + print(f"FAIL {name}: {detail}") + + +# ---------- Independent reference implementation of the slice ---------- +# Written from RFC 8949, not from the Lean code. Decode returns +# (canonical_text, rest) or None. Encode takes a Python value tree: +# ("uint", n) ("nint", n) ("bytes", b) ("text", b) ("array", [...]) +# ("map", [(k, v)]) ("false",) ("true",) ("null",). + +def read_arg(ai, rest): + if ai < 24: + return (ai, rest) + if ai == 24: + if len(rest) < 1 or rest[0] < 24: + return None + return (rest[0], rest[1:]) + if ai == 25: + if len(rest) < 2: + return None + v = int.from_bytes(rest[:2], "big") + return None if v < 2**8 else (v, rest[2:]) + if ai == 26: + if len(rest) < 4: + return None + v = int.from_bytes(rest[:4], "big") + return None if v < 2**16 else (v, rest[4:]) + if ai == 27: + if len(rest) < 8: + return None + v = int.from_bytes(rest[:8], "big") + return None if v < 2**32 else (v, rest[8:]) + return None # 28..31: reserved or indefinite + + +def ref_decode(bs): + if not bs: + return None + b, rest = bs[0], bs[1:] + mt, ai = b >> 5, b & 31 + if mt == 7: + if b == 0xF4: + return ("false", rest) + if b == 0xF5: + return ("true", rest) + if b == 0xF6: + return ("null", rest) + return None + if mt == 6: + return None + ar = read_arg(ai, rest) + if ar is None: + return None + arg, rest = ar + if mt == 0: + return (str(arg), rest) + if mt == 1: + return ("-" + str(arg + 1), rest) + if mt == 2: + if len(rest) < arg: + return None + return ("h'" + bytes(rest[:arg]).hex() + "'", rest[arg:]) + if mt == 3: + if len(rest) < arg: + return None + p = bytes(rest[:arg]) + try: + p.decode("utf-8") # strict: rejects overlongs and surrogates + except UnicodeDecodeError: + return None + return ("t'" + p.hex() + "'", rest[arg:]) + if mt == 4: + items = [] + for _ in range(arg): + r = ref_decode(rest) + if r is None: + return None + c, rest = r + items.append(c) + return ("[" + ",".join(items) + "]", rest) + if mt == 5: + pairs = [] + for _ in range(arg): + k = ref_decode(rest) + if k is None: + return None + kc, rest = k + v = ref_decode(rest) + if v is None: + return None + vc, rest = v + pairs.append(kc + ":" + vc) + return ("{" + ",".join(pairs) + "}", rest) + return None + + +def ref_full(bs): + """Full-input decode: returns canonical text, or None.""" + r = ref_decode(bs) + if r is None: + return None + c, rest = r + if rest: + return None + return c + + +def ref_head(mt, arg): + if arg < 24: + return bytes([(mt << 5) | arg]) + if arg < 2**8: + return bytes([(mt << 5) | 24, arg]) + if arg < 2**16: + return bytes([(mt << 5) | 25]) + arg.to_bytes(2, "big") + if arg < 2**32: + return bytes([(mt << 5) | 26]) + arg.to_bytes(4, "big") + return bytes([(mt << 5) | 27]) + arg.to_bytes(8, "big") + + +def ref_encode(v): + t = v[0] + if t == "uint": + return ref_head(0, v[1]) + if t == "nint": + return ref_head(1, v[1]) + if t == "bytes": + return ref_head(2, len(v[1])) + bytes(v[1]) + if t == "text": + return ref_head(3, len(v[1])) + bytes(v[1]) + if t == "array": + return ref_head(4, len(v[1])) + b"".join(ref_encode(x) for x in v[1]) + if t == "map": + out = ref_head(5, len(v[1])) + for k, w in v[1]: + out += ref_encode(k) + ref_encode(w) + return out + if t == "false": + return b"\xf4" + if t == "true": + return b"\xf5" + return b"\xf6" + + +def ref_canonical(v): + t = v[0] + if t == "uint": + return str(v[1]) + if t == "nint": + return "-" + str(v[1] + 1) + if t == "bytes": + return "h'" + bytes(v[1]).hex() + "'" + if t == "text": + return "t'" + bytes(v[1]).hex() + "'" + if t == "array": + return "[" + ",".join(ref_canonical(x) for x in v[1]) + "]" + if t == "map": + return "{" + ",".join(ref_canonical(k) + ":" + ref_canonical(w) for k, w in v[1]) + "}" + return {"false": "false", "true": "true", "null": "null"}[t] + + +# ---------- Lean process driver ---------- + +class LeanDriver: + def __init__(self): + if not EXE.exists(): + subprocess.run(["lake", "build"], cwd=PILOT_DIR, check=True) + self.proc = subprocess.Popen([str(EXE)], stdin=subprocess.PIPE, + stdout=subprocess.PIPE, text=True) + + def ask(self, op, hexs): + global inputs + inputs += 1 + self.proc.stdin.write(f"{op} {hexs}\n") + self.proc.stdin.flush() + return self.proc.stdout.readline().rstrip("\n") + + +# ---------- RFC 8949 Appendix A vectors ---------- + +# (hex, canonical) for in-slice rows. +RFC_OK = [ + ("00", "0"), ("01", "1"), ("0a", "10"), ("17", "23"), + ("1818", "24"), ("1819", "25"), ("1864", "100"), ("1903e8", "1000"), + ("1a000f4240", "1000000"), ("1b000000e8d4a51000", "1000000000000"), + ("1bffffffffffffffff", "18446744073709551615"), + ("20", "-1"), ("29", "-10"), ("3863", "-100"), ("3903e7", "-1000"), + ("3bffffffffffffffff", "-18446744073709551616"), + ("40", "h''"), ("4401020304", "h'01020304'"), + ("60", "t''"), ("6161", "t'61'"), ("6449455446", "t'49455446'"), + ("62225c", "t'225c'"), ("62c3bc", "t'c3bc'"), ("63e6b0b4", "t'e6b0b4'"), + ("64f0908591", "t'f0908591'"), + ("80", "[]"), ("83010203", "[1,2,3]"), + ("8301820203820405", "[1,[2,3],[4,5]]"), + ("98190102030405060708090a0b0c0d0e0f101112131415161718181819", + "[" + ",".join(str(i) for i in range(1, 26)) + "]"), + ("a0", "{}"), ("a201020304", "{1:2,3:4}"), + ("a26161016162820203", "{t'61':1,t'62':[2,3]}"), + ("826161a161626163", "[t'61',{t'62':t'63'}]"), + ("f4", "false"), ("f5", "true"), ("f6", "null"), +] + +# Out-of-slice rows: floats, simple, undefined, tags (incl. bignums), +# indefinite lengths, break. +RFC_REJECT = [ + "f7", "f0", "f818", "f8ff", + "f97e00", "f9fc00", "f9c400", "fa47c35000", "fb7e37e43c8800759c", + "c074323031332d30332d32315432303a30343a30305a", + "c11a514b67b0", "c249010000000000000000", "c349010000000000000000", + "d8204567696751554d", "d8234567696751554d", + "5f4100ff", "7f6141ff", "9fff", "bf616101ff", "ff", + "1c", "1d", "1e", "1f", "3c", "5c", "7c", "9c", "bc", "dc", +] + + +def main(): + global accepted, rejected + drv = LeanDriver() + + # RFC vectors, both directions. + for hexs, canon in RFC_OK: + check(f"rfc d {hexs}", drv.ask("d", hexs) == canon, + f"want {canon}") + check(f"rfc r {hexs}", drv.ask("r", hexs) == hexs, + "re-encode must return the input") + for hexs in RFC_REJECT: + check(f"rfc reject {hexs}", drv.ask("d", hexs) == "error") + check(f"rfc reject r {hexs}", drv.ask("r", hexs) == "error") + + rng = random.Random(SEED) + + # Random generated in-slice items: encode with the reference, then + # compare decode + re-encode. + def gen(depth): + choices = ["uint", "nint", "bytes", "text", "false", "true", "null"] + if depth < 3: + choices += ["array", "map"] + t = rng.choice(choices) + if t == "uint": + return ("uint", rng.choice([0, 1, 23, 24, 255, 256, 65535, 65536, + 2**32 - 1, 2**32, 2**64 - 1, + rng.randrange(0, 2**64)])) + if t == "nint": + return ("nint", rng.choice([0, 23, 24, 255, 256, 2**32, + 2**64 - 1, rng.randrange(0, 2**64)])) + if t == "bytes": + return ("bytes", bytes(rng.randrange(256) + for _ in range(rng.randrange(0, 10)))) + if t == "text": + n = rng.randrange(0, 6) + cps = [] + for _ in range(n): + cps.append(rng.choice([0x41, 0x61, 0x7f, 0x80, 0x7ff, 0x800, + 0xfffd, 0x10000, 0x10ffff, + rng.randrange(0x20, 0x7f)])) + return ("text", "".join(chr(c) for c in cps).encode("utf-8")) + if t == "array": + return ("array", [gen(depth + 1) for _ in range(rng.randrange(0, 5))]) + if t == "map": + return ("map", [(gen(depth + 1), gen(depth + 1)) + for _ in range(rng.randrange(0, 4))]) + return (t,) + + for i in range(400): + v = gen(0) + enc = ref_encode(v) + canon = ref_canonical(v) + check(f"gen d {i}", drv.ask("d", enc.hex()) == canon, f"want {canon}") + check(f"gen r {i}", drv.ask("r", enc.hex()) == enc.hex(), + "soundness: re-encode returns the input") + # Every truncation must be turned away. + for cut in range(1, min(len(enc), 4)): + check(f"gen trunc {i}.{cut}", drv.ask("d", enc[:cut].hex()) == "error") + accepted += 1 + + # Random garbage: compare acceptance and canonical form. + for i in range(600): + bs = bytes(rng.randrange(256) for _ in range(rng.randrange(0, 14))) + want = ref_full(list(bs)) + got = drv.ask("d", bs.hex()) + if want is None: + check(f"rand d {i}", got == "error", f"accepted {bs.hex()}") + rejected += 1 + else: + check(f"rand d {i}", got == want, f"{bs.hex()}: want {want}") + check(f"rand r {i}", drv.ask("r", bs.hex()) == bs.hex(), + "re-encode returns the input") + accepted += 1 + + # Non-preferred forms of small values: must be turned away. + for mt in [0, 1, 2, 3, 4, 5]: + for ai, extra in [(24, 0), (25, 200), (26, 5000), (27, 70000)]: + hdr = ref_head(mt, 0) + np = bytes([(mt << 5) | ai]) + extra.to_bytes( + {24: 1, 25: 2, 26: 4, 27: 8}[ai], "big") + payload = b"" + if mt in (2, 3): + payload = bytes(extra) # the string body itself + check(f"nonpref mt{mt} ai{ai}", + drv.ask("d", (np + payload).hex()) == "error") + rejected += 1 + + # Bad UTF-8 text payloads: overlong, surrogate, stray continuation. + bad = [bytes([0x61, 0xc0]), bytes([0x62, 0xc0, 0x80]), + bytes([0x63, 0xed, 0xa0, 0x80]), bytes([0x62, 0xf4, 0x90]), + bytes([0x61, 0x80]), bytes([0x62, 0xc2])] + for p in bad: + hdr = ref_head(3, len(p)) + check(f"utf8 reject {p.hex()}", drv.ask("d", (hdr + p).hex()) == "error") + rejected += 1 + + # Leftover bytes after a complete item: turned away. + check("trailing", drv.ask("d", "0102") == "error") + check("empty", drv.ask("d", "") == "error") + + # The build is part of the check: lake build already ran if needed. + total = checks + ok = total - len(failures) + RESULTS.write_text(f"""# Test results + +Run by `tests/run_tests.py` against an independent Python implementation of +the slice written from RFC 8949, in the same file, and against the RFC 8949 +Appendix A vectors. +Lean: Lean 4.35.0. Python: {sys.version.split()[0]}. + +- Seed: {SEED} +- Byte inputs fed to the Lean codec: {inputs} +- Checks run: {total} +- Checks passed: {ok} +- Failures: {len(failures)} +- Accepted inputs: generated well-formed items, their random-garbage + counterparts that parse, and the in-slice RFC 8949 Appendix A rows. +- Turned away: the out-of-slice Appendix A rows (floats, simple values, + `undefined`, tags including bignums, indefinite lengths, break, reserved + added information), truncations of every generated item, non-preferred + argument forms for all six major types, malformed UTF-8 text payloads, + trailing bytes after an item, and empty input. + +Axiom check (`Proofs.lean`): + +``` +'Spec.cbor_decode_encode' depends on axioms: [propext, Classical.choice, Quot.sound] +'Spec.cbor_encode_decode' depends on axioms: [propext, Quot.sound] +'Spec.cbor_rejects_reserved_ai' depends on axioms: [propext, Quot.sound] +'Spec.cbor_rejects_tags' depends on axioms: [propext, Quot.sound] +'Spec.cbor_rejects_simple' depends on axioms: [propext, Quot.sound] +'Spec.cbor_rfc8949_vectors' depends on axioms: [propext] +'Spec.cbor_rejects_out_of_slice' depends on axioms: [propext] +'Spec.cbor_rejects_nonpreferred' depends on axioms: [propext] +'Spec.cbor_rejects_bad_utf8' depends on axioms: [propext] +'Spec.cbor_rejects_truncation' depends on axioms: [propext] +``` +""") + print(f"{ok}/{total} checks passed; results written to {RESULTS}") + return 1 if failures else 0 + + +if __name__ == "__main__": + sys.exit(main())