diff --git a/.github/workflows/bar.yml b/.github/workflows/bar.yml new file mode 100644 index 0000000..e8b9eda --- /dev/null +++ b/.github/workflows/bar.yml @@ -0,0 +1,21 @@ +name: verified bar + +on: + push: + pull_request: + # Rerun when the spec reviewer approves, or an approval is dismissed. + pull_request_review: + types: [submitted, dismissed] + +jobs: + bar: + # pull-requests: read lets the check confirm the spec approval on GitHub. + permissions: + contents: read + pull-requests: read + # Both lines pin the same commit of Proven-Commons/mission: the bar v2 + # checker, on mission's main branch. Move both to a release tag once + # mission publishes one. + uses: Proven-Commons/mission/.github/workflows/verified-bar.yml@6ba85c27abaaf07905c9316aa96dc29f7b5847a2 + with: + bar-ref: 6ba85c27abaaf07905c9316aa96dc29f7b5847a2 diff --git a/.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..edc31e5 --- /dev/null +++ b/Cbor/Basic.lean @@ -0,0 +1,221 @@ +/- + 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. + + The item type `Value` and its well-formedness `Value.wf` are part of + the specification, in `Spec/Value.lean`, so the approval covers them. +-/ + +import Cbor.Utf8 +import Spec.Value + +namespace Cbor + +/-! ## Depth -/ + +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..bc2aac6 --- /dev/null +++ b/Proofs.lean @@ -0,0 +1,8 @@ +/- + The proofs: each theorem of `Spec.lean`, proved under the same name. +-/ +import Proofs.Utf8 +import Proofs.Cbor +import Proofs.RoundTrip +import Proofs.Encode +import Proofs.Strict diff --git a/Proofs/Cbor.lean b/Proofs/Cbor.lean new file mode 100644 index 0000000..6654c25 --- /dev/null +++ b/Proofs/Cbor.lean @@ -0,0 +1,207 @@ +/- + 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 [ite_eq_right (by omega), ite_eq_right (by omega), ite_eq_right (by omega), ite_eq_right (by omega), + ite_eq_right (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] + by_cases h7 : b.toNat / 32 = 7 + · rw [ite_eq_left h7, ite_eq_right (by omega), ite_eq_right (by omega), ite_eq_right (by omega)] + · rw [ite_eq_right h7] + by_cases h6 : b.toNat / 32 = 6 + · rw [ite_eq_left h6] + · rw [ite_eq_right 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 [ite_eq_right (by omega), ite_eq_left 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 [ite_eq_left h7, ite_eq_right h4, ite_eq_right h5, ite_eq_right 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]) ∧ + decode (0x98 :: 0x19 :: ((List.range 23).map fun n => (n + 1).toUInt8) ++ + [0x18, 0x18, 0x18, 0x19]) = + some (.array ((List.range 25).map fun n => .uint (n + 1).toUInt64)) ∧ + -- 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] ∧ + decode [0xa5, 0x61, 0x61, 0x61, 0x41, 0x61, 0x62, 0x61, 0x42, 0x61, 0x63, 0x61, 0x43, + 0x61, 0x64, 0x61, 0x44, 0x61, 0x65, 0x61, 0x45] = + some (.map [(.text [0x61], .text [0x41]), (.text [0x62], .text [0x42]), + (.text [0x63], .text [0x43]), (.text [0x64], .text [0x44]), + (.text [0x65], .text [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 : + -- Bignums (tags 2 and 3) + 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 ∧ + -- Floats: half, single and double, including infinities and NaN + decode [0xf9, 0x00, 0x00] = none ∧ + decode [0xf9, 0x80, 0x00] = none ∧ + decode [0xf9, 0x3c, 0x00] = none ∧ + decode [0xfb, 0x3f, 0xf1, 0x99, 0x99, 0x99, 0x99, 0x99, 0x9a] = none ∧ + decode [0xf9, 0x3e, 0x00] = none ∧ + decode [0xf9, 0x7b, 0xff] = none ∧ + decode [0xfa, 0x47, 0xc3, 0x50, 0x00] = none ∧ + decode [0xfa, 0x7f, 0x7f, 0xff, 0xff] = none ∧ + decode [0xfb, 0x7e, 0x37, 0xe4, 0x3c, 0x88, 0x00, 0x75, 0x9c] = none ∧ + decode [0xf9, 0x00, 0x01] = none ∧ + decode [0xf9, 0x04, 0x00] = none ∧ + decode [0xf9, 0xc4, 0x00] = none ∧ + decode [0xfb, 0xc0, 0x10, 0x66, 0x66, 0x66, 0x66, 0x66, 0x66] = none ∧ + decode [0xf9, 0x7c, 0x00] = none ∧ + decode [0xf9, 0x7e, 0x00] = none ∧ + decode [0xf9, 0xfc, 0x00] = none ∧ + decode [0xfa, 0x7f, 0x80, 0x00, 0x00] = none ∧ + decode [0xfa, 0x7f, 0xc0, 0x00, 0x00] = none ∧ + decode [0xfa, 0xff, 0x80, 0x00, 0x00] = none ∧ + decode [0xfb, 0x7f, 0xf0, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] = none ∧ + decode [0xfb, 0x7f, 0xf8, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] = none ∧ + decode [0xfb, 0xff, 0xf0, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] = none ∧ + -- undefined, simple(16), simple(255) + decode [0xf7] = none ∧ + decode [0xf0] = none ∧ + decode [0xf8, 0xff] = none ∧ + -- Tags 0, 1, 23, 24, 32 + 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 [0xc1, 0xfb, 0x41, 0xd4, 0x52, 0xd9, 0xec, 0x20, 0x00, 0x00] = none ∧ + decode [0xd7, 0x44, 0x01, 0x02, 0x03, 0x04] = none ∧ + decode [0xd8, 0x18, 0x45, 0x64, 0x49, 0x45, 0x54, 0x46] = none ∧ + decode [0xd8, 0x20, 0x76, 0x68, 0x74, 0x74, 0x70, 0x3a, 0x2f, 0x2f, 0x77, 0x77, 0x77, 0x2e, + 0x65, 0x78, 0x61, 0x6d, 0x70, 0x6c, 0x65, 0x2e, 0x63, 0x6f, 0x6d] = none ∧ + -- Indefinite-length strings, arrays and maps, alone or nested + 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 [0x9f, 0x01, 0x82, 0x02, 0x03, 0x82, 0x04, 0x05, 0xff] = none ∧ + decode [0x83, 0x01, 0x82, 0x02, 0x03, 0x9f, 0x04, 0x05, 0xff] = none ∧ + decode [0x83, 0x01, 0x9f, 0x02, 0x03, 0xff, 0x82, 0x04, 0x05] = none ∧ + decode [0x9f, 0x01, 0x02, 0x03, 0x04, 0x05, 0x06, 0x07, 0x08, 0x09, 0x0a, 0x0b, 0x0c, 0x0d, + 0x0e, 0x0f, 0x10, 0x11, 0x12, 0x13, 0x14, 0x15, 0x16, 0x17, 0x18, 0x18, 0x18, 0x19, + 0xff] = none ∧ + decode [0xbf, 0x61, 0x61, 0x01, 0x61, 0x62, 0x9f, 0x02, 0x03, 0xff, 0xff] = none ∧ + decode [0x82, 0x61, 0x61, 0xbf, 0x61, 0x62, 0x61, 0x63, 0xff] = none ∧ + decode [0xbf, 0x63, 0x46, 0x75, 0x6e, 0xf5, 0x63, 0x41, 0x6d, 0x74, 0x21, 0xff] = none ∧ + -- Break, on its own + decode [0xff] = 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/Encode.lean b/Proofs/Encode.lean new file mode 100644 index 0000000..c7adca9 --- /dev/null +++ b/Proofs/Encode.lean @@ -0,0 +1,94 @@ +/- + The encoder writes the encoding of the specification: `Cbor.encode v` + is `Spec.enc v` for every item. +-/ + +import Cbor +import Spec.Defs + +namespace Cbor + +theorem toNat_toUInt8 (x : Nat) : x.toUInt8.toNat = x % 256 := by simp [Nat.toUInt8] + +/-- Two numbers give the same byte when they agree modulo 256. -/ +theorem toUInt8_eq (x y : Nat) (h : x % 256 = y % 256) : x.toUInt8 = y.toUInt8 := + UInt8.toNat_inj.mp (by rw [toNat_toUInt8, toNat_toUInt8, h]) + +/-- Peeling the last byte off `netBytes`. -/ +theorem netBytes_succ (n x : Nat) : + Spec.netBytes (n + 1) x = Spec.netBytes n (x / 256) ++ [(x % 256).toUInt8] := by + induction n generalizing x with + | zero => simp [Spec.netBytes] + | succ n ih => + rw [Spec.netBytes, ih x, Spec.netBytes, Nat.div_div_eq_div_mul, Nat.pow_succ, + Nat.mul_comm 256 (256 ^ n)] + rfl + +/-- The code's big-endian bytes are the specification's network byte + order. -/ +theorem beBytes_eq_netBytes (n x : Nat) : beBytes n x = Spec.netBytes n x := by + induction n generalizing x with + | zero => rfl + | succ n ih => rw [beBytes, ih, netBytes_succ] + +/-- The code's head is the specification's head. -/ +theorem head_eq_itemHead (mt arg : Nat) : head mt arg = Spec.itemHead mt arg := by + have hadd : ∀ k : Nat, (mt * 32).toUInt8 + k.toUInt8 = (mt * 32 + k).toUInt8 := by + intro k + apply UInt8.toNat_inj.mp + rw [UInt8.toNat_add, toNat_toUInt8, toNat_toUInt8, toNat_toUInt8, ← Nat.add_mod] + have hlit : ∀ k : Nat, k < 256 → (OfNat.ofNat k : UInt8) = k.toUInt8 := by + intro k hk + apply UInt8.toNat_inj.mp + rw [toNat_toUInt8, UInt8.toNat_ofNat] + unfold head Spec.itemHead + simp only [Spec.netBytes, beBytes_eq_netBytes] + by_cases h1 : arg < 24 + · rw [ite_eq_left h1, ite_eq_left h1, hadd] + · rw [ite_eq_right h1, ite_eq_right h1] + by_cases h2 : arg < 2 ^ 8 + · rw [ite_eq_left (by omega : arg ≤ 0xFF), ite_eq_left h2, + show (24 : UInt8) = (24 : Nat).toUInt8 from hlit 24 (by decide), hadd, + toUInt8_eq arg (arg / 256 ^ 0 % 256) (by simp)] + · rw [ite_eq_right (by omega : ¬ arg ≤ 0xFF), ite_eq_right h2] + by_cases h3 : arg < 2 ^ 16 + · rw [ite_eq_left (by omega : arg ≤ 0xFFFF), ite_eq_left h3, + show (25 : UInt8) = (25 : Nat).toUInt8 from hlit 25 (by decide), hadd] + rfl + · rw [ite_eq_right (by omega : ¬ arg ≤ 0xFFFF), ite_eq_right h3] + by_cases h4 : arg < 2 ^ 32 + · rw [ite_eq_left (by omega : arg ≤ 0xFFFFFFFF), ite_eq_left h4, + show (26 : UInt8) = (26 : Nat).toUInt8 from hlit 26 (by decide), hadd] + rfl + · rw [ite_eq_right (by omega : ¬ arg ≤ 0xFFFFFFFF), ite_eq_right h4, + show (27 : UInt8) = (27 : Nat).toUInt8 from hlit 27 (by decide), hadd] + rfl + +mutual +theorem encode_eq_enc : ∀ v : Value, encode v = Spec.enc v + | .uint n => by simp only [encode, Spec.enc, head_eq_itemHead] + | .nint n => by simp only [encode, Spec.enc, head_eq_itemHead] + | .bytes bs => by simp only [encode, Spec.enc, head_eq_itemHead] + | .text bs => by simp only [encode, Spec.enc, head_eq_itemHead] + | .array xs => by simp only [encode, Spec.enc, head_eq_itemHead, encodeList_eq_encList xs] + | .map kvs => by simp only [encode, Spec.enc, head_eq_itemHead, encodePairs_eq_encPairs kvs] + | .vfalse => rfl + | .vtrue => rfl + | .vnull => rfl + +theorem encodeList_eq_encList : ∀ xs : List Value, encodeList xs = Spec.encList xs + | [] => rfl + | x :: xs => by simp only [encodeList, Spec.encList, encode_eq_enc x, encodeList_eq_encList xs] + +theorem encodePairs_eq_encPairs : ∀ kvs : List (Value × Value), encodePairs kvs = Spec.encPairs kvs + | [] => rfl + | (k, v) :: kvs => by + simp only [encodePairs, Spec.encPairs, encode_eq_enc k, encode_eq_enc v, + encodePairs_eq_encPairs kvs] +end + +end Cbor + +/-- `Spec.cbor_encode_spec`. -/ +theorem Spec.cbor_encode_spec (v : Cbor.Value) : Cbor.encode v = Spec.enc v := + Cbor.encode_eq_enc v diff --git a/Proofs/RoundTrip.lean b/Proofs/RoundTrip.lean new file mode 100644 index 0000000..2c40cbd --- /dev/null +++ b/Proofs/RoundTrip.lean @@ -0,0 +1,1297 @@ +/- + The round trip: decoding an encoding returns the same item. +-/ + +import Cbor +import Spec.Defs +import Proofs.Utf8 + +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 [ite_eq_left 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] + rw [ite_eq_left (by omega : arg ≤ 23)] + · rw [ite_eq_right h1] + by_cases h2 : arg ≤ 0xFF + · rw [ite_eq_left 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, ite_eq_right (by decide : ¬(24:Nat) ≤ 23), ite_eq_left rfl] + show (if (arg.toUInt8).toNat ≥ 24 then some ((arg.toUInt8).toNat, rest) + else none) = some (arg, rest) + rw [e2, ite_eq_left (by omega : arg ≥ 24)] + · rw [ite_eq_right h2] + by_cases h3 : arg ≤ 0xFFFF + · rw [ite_eq_left 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, ite_eq_right (by decide : ¬(25:Nat) ≤ 23), + ite_eq_right (by decide : ¬(25:Nat) = 24), ite_eq_left 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, ite_eq_left ⟨by rw [beBytes_length], by omega⟩] + · rw [ite_eq_right h3] + by_cases h4 : arg ≤ 0xFFFFFFFF + · rw [ite_eq_left 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, ite_eq_right (by decide : ¬(26:Nat) ≤ 23), + ite_eq_right (by decide : ¬(26:Nat) = 24), ite_eq_right (by decide : ¬(26:Nat) = 25), + ite_eq_left 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, ite_eq_left ⟨by rw [beBytes_length], by omega⟩] + · rw [ite_eq_right 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, ite_eq_right (by decide : ¬(27:Nat) ≤ 23), + ite_eq_right (by decide : ¬(27:Nat) = 24), ite_eq_right (by decide : ¬(27:Nat) = 25), + ite_eq_right (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, ite_eq_left ⟨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 [ite_eq_left h1]; simp + · by_cases h2 : arg ≤ 255 + · rw [ite_eq_right h1, ite_eq_left h2]; simp + · by_cases h3 : arg ≤ 65535 + · rw [ite_eq_right h1, ite_eq_right h2, ite_eq_left h3]; simp [beBytes_length] + · by_cases h4 : arg ≤ 4294967295 + · rw [ite_eq_right h1, ite_eq_right h2, ite_eq_right h3, ite_eq_left h4]; simp [beBytes_length] + · rw [ite_eq_right h1, ite_eq_right h2, ite_eq_right h3, ite_eq_right 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, ite_eq_right (by omega : ¬(mt = 7)), ite_eq_right (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), + ite_eq_left rfl, UInt64.ofNat_toNat] + | nint n => + simp only [encode] + rw [decodeFuel_head 1 n.toNat rest (by decide) (UInt64.toNat_lt n) (F + 1), + ite_eq_right (by decide : ¬(1:Nat) = 0), ite_eq_left 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), + ite_eq_right (by decide : ¬(2:Nat) = 0), ite_eq_right (by decide : ¬(2:Nat) = 1), ite_eq_left rfl, + ite_eq_right (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 ⟨hwfu, hlen⟩ := hwf + have hval : Utf8.valid bs = true := by rw [Utf8.valid_eq_wellFormed]; exact hwfu + 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), + ite_eq_right (by decide : ¬(3:Nat) = 0), ite_eq_right (by decide : ¬(3:Nat) = 1), + ite_eq_right (by decide : ¬(3:Nat) = 2), ite_eq_left rfl, + ite_eq_right (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, + ite_eq_left 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), + ite_eq_right (by decide : ¬(4:Nat) = 0), ite_eq_right (by decide : ¬(4:Nat) = 1), + ite_eq_right (by decide : ¬(4:Nat) = 2), ite_eq_right (by decide : ¬(4:Nat) = 3), ite_eq_left 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), + ite_eq_right (by decide : ¬(5:Nat) = 0), ite_eq_right (by decide : ¬(5:Nat) = 1), + ite_eq_right (by decide : ¬(5:Nat) = 2), ite_eq_right (by decide : ¬(5:Nat) = 3), + ite_eq_right (by decide : ¬(5:Nat) = 4), ite_eq_left rfl, + ihp kvs rest hwfP hdep] + | vfalse => + simp only [encode] + show decodeFuel (F + 1 + 1) (0xf4 :: rest) = some (.vfalse, rest) + rw [decodeFuel_cons, ite_eq_left (by decide : (0xf4 : UInt8).toNat / 32 = 7), + ite_eq_left (by decide : (0xf4 : UInt8).toNat = 0xf4)] + | vtrue => + simp only [encode] + show decodeFuel (F + 1 + 1) (0xf5 :: rest) = some (.vtrue, rest) + rw [decodeFuel_cons, ite_eq_left (by decide : (0xf5 : UInt8).toNat / 32 = 7), + ite_eq_right (by decide : ¬(0xf5 : UInt8).toNat = 0xf4), + ite_eq_left (by decide : (0xf5 : UInt8).toNat = 0xf5)] + | vnull => + simp only [encode] + show decodeFuel (F + 1 + 1) (0xf6 :: rest) = some (.vnull, rest) + rw [decodeFuel_cons, ite_eq_left (by decide : (0xf6 : UInt8).toNat / 32 = 7), + ite_eq_right (by decide : ¬(0xf6 : UInt8).toNat = 0xf4), + ite_eq_right (by decide : ¬(0xf6 : UInt8).toNat = 0xf5), + ite_eq_left (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 [ite_eq_left h1] at h + injection h with hpair; injection hpair with hga hgr + subst hgr + refine ⟨?_, by omega⟩ + rw [← hga] + unfold head + rw [ite_eq_left (by omega : b.toNat % 32 < 24), ← hbyte (b.toNat % 32) (by omega) rfl] + rfl + · rw [ite_eq_right h1] at h + by_cases h2 : b.toNat % 32 = 24 + · rw [ite_eq_left 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 [ite_eq_left 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 [ite_eq_right (by omega : ¬b0.toNat < 24), ite_eq_left (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 [ite_eq_right hb0] at h + simp at h + · rw [ite_eq_right h2] at h + by_cases h3 : b.toNat % 32 = 25 + · rw [ite_eq_left 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 [ite_eq_left 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 [ite_eq_right (by omega : ¬readBe (rest.take 2) < 24), + ite_eq_right (by omega : ¬readBe (rest.take 2) ≤ 255), + ite_eq_left (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 [ite_eq_right hc] at h + simp at h + · rw [ite_eq_right h3] at h + by_cases h4 : b.toNat % 32 = 26 + · rw [ite_eq_left 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 [ite_eq_left 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 [ite_eq_right (by omega : ¬readBe (rest.take 4) < 24), + ite_eq_right (by omega : ¬readBe (rest.take 4) ≤ 255), + ite_eq_right (by omega : ¬readBe (rest.take 4) ≤ 65535), + ite_eq_left (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 [ite_eq_right hc] at h + simp at h + · rw [ite_eq_right h4] at h + by_cases h5 : b.toNat % 32 = 27 + · rw [ite_eq_left 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 [ite_eq_left 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 [ite_eq_right (by omega : ¬readBe (rest.take 8) < 24), + ite_eq_right (by omega : ¬readBe (rest.take 8) ≤ 255), + ite_eq_right (by omega : ¬readBe (rest.take 8) ≤ 65535), + ite_eq_right (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 [ite_eq_right hc] at h + simp at h + · rw [ite_eq_right 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 [ite_eq_left h7] at h + by_cases h4 : b.toNat = 0xf4 + · rw [ite_eq_left 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 [ite_eq_right h4] at h + by_cases h5 : b.toNat = 0xf5 + · rw [ite_eq_left 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 [ite_eq_right h5] at h + by_cases h6 : b.toNat = 0xf6 + · rw [ite_eq_left 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 [ite_eq_right h6] at h + simp at h + · rw [ite_eq_right h7] at h + by_cases h6 : b.toNat / 32 = 6 + · rw [ite_eq_left h6] at h + simp at h + · rw [ite_eq_right h6] at h + split at h + · simp at h + · rename_i arg r' hrd + by_cases h0 : b.toNat / 32 = 0 + · rw [ite_eq_left 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 [ite_eq_right h0] at h + by_cases h1 : b.toNat / 32 = 1 + · rw [ite_eq_left 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 [ite_eq_right h1] at h + by_cases h2 : b.toNat / 32 = 2 + · rw [ite_eq_left h2] at h + by_cases hlt : r'.length < arg + · rw [ite_eq_left hlt] at h + simp at h + · rw [ite_eq_right 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 [ite_eq_right h2] at h + by_cases h3 : b.toNat / 32 = 3 + · rw [ite_eq_left h3] at h + by_cases hlt : r'.length < arg + · rw [ite_eq_left hlt] at h + simp at h + · rw [ite_eq_right hlt] at h + by_cases hval : Utf8.valid (r'.take arg) = true + · rw [ite_eq_left 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 ⟨by rw [← Utf8.valid_eq_wellFormed]; exact 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 [ite_eq_right hval] at h + simp at h + · rw [ite_eq_right h3] at h + by_cases h4 : b.toNat / 32 = 4 + · rw [ite_eq_left 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 [ite_eq_right h4] at h + by_cases h5 : b.toNat / 32 = 5 + · rw [ite_eq_left 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 [ite_eq_right 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 [ite_eq_left h7] at h + by_cases h4 : b.toNat = 0xf4 + · rw [ite_eq_left 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 [ite_eq_right h4] at h + by_cases h5 : b.toNat = 0xf5 + · rw [ite_eq_left 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 [ite_eq_right h5] at h + by_cases h6 : b.toNat = 0xf6 + · rw [ite_eq_left 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 [ite_eq_right h6] at h + simp at h + · rw [ite_eq_right h7] at h + by_cases h6 : b.toNat / 32 = 6 + · rw [ite_eq_left h6] at h + simp at h + · rw [ite_eq_right h6] at h + split at h + · simp at h + · rename_i arg r' hrd + by_cases h0 : b.toNat / 32 = 0 + · rw [ite_eq_left 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 [ite_eq_right h0] at h + by_cases h1 : b.toNat / 32 = 1 + · rw [ite_eq_left 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 [ite_eq_right h1] at h + by_cases h2 : b.toNat / 32 = 2 + · rw [ite_eq_left h2] at h + by_cases hlt : r'.length < arg + · rw [ite_eq_left hlt] at h + simp at h + · rw [ite_eq_right 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 [ite_eq_right h2] at h + by_cases h3 : b.toNat / 32 = 3 + · rw [ite_eq_left h3] at h + by_cases hlt : r'.length < arg + · rw [ite_eq_left hlt] at h + simp at h + · rw [ite_eq_right hlt] at h + by_cases hval : Utf8.valid (r'.take arg) = true + · rw [ite_eq_left 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 ⟨by rw [← Utf8.valid_eq_wellFormed]; exact 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 [ite_eq_right hval] at h + simp at h + · rw [ite_eq_right h3] at h + by_cases h4 : b.toNat / 32 = 4 + · rw [ite_eq_left 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 [ite_eq_right h4] at h + by_cases h5 : b.toNat / 32 = 5 + · rw [ite_eq_left 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 [ite_eq_right 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: whatever the decoder accepts is the encoding of a + well-formed item, the one it returns. -/ +theorem encode_decode (bs : List UInt8) (v : Value) (h : decode bs = some v) : + v.wf = true ∧ 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 + cases h + exact ⟨hwf, hbs.symm⟩ + · simp at h + +/-- The decoder accepts exactly the encodings of well-formed items: + `Spec.cbor_encode_decode`. -/ +theorem Spec.cbor_encode_decode (bs : List UInt8) (v : Value) : + decode bs = some v ↔ v.wf = true ∧ encode v = bs := by + constructor + · exact encode_decode bs v + · rintro ⟨hwf, rfl⟩ + exact decode_encode v hwf diff --git a/Proofs/Strict.lean b/Proofs/Strict.lean new file mode 100644 index 0000000..0ff9640 --- /dev/null +++ b/Proofs/Strict.lean @@ -0,0 +1,312 @@ +/- + The decoder is strict, for every input of each shape: non-preferred + arguments, out-of-slice items at the top or inside a container, and + input cut short inside an item are all turned away. +-/ + +import Proofs.Cbor +import Proofs.Encode +import Proofs.RoundTrip + +open Cbor + +namespace Cbor + +/-! ## Reading an argument written by `Spec.netBytes` -/ + +theorem netBytes_length (k x : Nat) : (Spec.netBytes k x).length = k := by + rw [← beBytes_eq_netBytes, beBytes_length] + +theorem readBe_netBytes (k x : Nat) (h : x < 256 ^ k) : readBe (Spec.netBytes k x) = x := by + rw [← beBytes_eq_netBytes] + exact readBe_beBytes k x h + +theorem readArg_24 (c : UInt8) (r : List UInt8) : + readArg 24 (c :: r) = if c.toNat ≥ 24 then some (c.toNat, r) else none := by + rw [readArg.eq_def, ite_eq_right (by decide), ite_eq_left rfl] + +theorem readArg_25 (l : List UInt8) : + readArg 25 l = if (l.take 2).length = 2 ∧ readBe (l.take 2) ≥ 2 ^ 8 + then some (readBe (l.take 2), l.drop 2) else none := by + rw [readArg.eq_def, ite_eq_right (by decide), ite_eq_right (by decide), ite_eq_left rfl, + List.splitAt_eq] + +theorem readArg_26 (l : List UInt8) : + readArg 26 l = if (l.take 4).length = 4 ∧ readBe (l.take 4) ≥ 2 ^ 16 + then some (readBe (l.take 4), l.drop 4) else none := by + rw [readArg.eq_def, ite_eq_right (by decide), ite_eq_right (by decide), + ite_eq_right (by decide), ite_eq_left rfl, List.splitAt_eq] + +theorem readArg_27 (l : List UInt8) : + readArg 27 l = if (l.take 8).length = 8 ∧ readBe (l.take 8) ≥ 2 ^ 32 + then some (readBe (l.take 8), l.drop 8) else none := by + rw [readArg.eq_def, ite_eq_right (by decide), ite_eq_right (by decide), + ite_eq_right (by decide), ite_eq_right (by decide), ite_eq_left rfl, List.splitAt_eq] + +/-- The decoder turns away an item whose initial byte is not in major + type 6 or 7 and whose argument `readArg` turns away. -/ +theorem decode_none_of_readArg (b : UInt8) (rest : List UInt8) (h7 : ¬ b.toNat / 32 = 7) + (h6 : ¬ b.toNat / 32 = 6) (hr : readArg (b.toNat % 32) rest = none) : + decode (b :: rest) = none := by + unfold decode + rw [List.length_cons, decodeFuel_cons, ite_eq_right h7, ite_eq_right h6, hr] + +/-- The initial byte for major type `mt` and additional information + `ai`. -/ +theorem headByte (mt ai : Nat) (hmt : mt ≤ 5) (hai : ai < 32) : + ((mt * 32 + ai).toUInt8).toNat / 32 = mt ∧ ((mt * 32 + ai).toUInt8).toNat % 32 = ai := by + rw [toNat_toUInt8, Nat.mod_eq_of_lt (by omega)] + omega + +end Cbor + +/-- `Spec.cbor_rejects_nonpreferred`. -/ +theorem Spec.cbor_rejects_nonpreferred (mt x : Nat) (rest : List UInt8) (hmt : mt ≤ 5) : + (x < 24 → decode ((mt * 32 + 24).toUInt8 :: Spec.netBytes 1 x ++ rest) = none) ∧ + (x < 2 ^ 8 → decode ((mt * 32 + 25).toUInt8 :: Spec.netBytes 2 x ++ rest) = none) ∧ + (x < 2 ^ 16 → decode ((mt * 32 + 26).toUInt8 :: Spec.netBytes 4 x ++ rest) = none) ∧ + (x < 2 ^ 32 → decode ((mt * 32 + 27).toUInt8 :: Spec.netBytes 8 x ++ rest) = none) := by + refine ⟨fun hx => ?_, fun hx => ?_, fun hx => ?_, fun hx => ?_⟩ + · obtain ⟨h1, h2⟩ := headByte mt 24 hmt (by decide) + rw [List.cons_append] + apply decode_none_of_readArg _ _ (by omega) (by omega) + rw [h2] + simp only [Spec.netBytes, List.cons_append, List.nil_append] + rw [readArg_24, ite_eq_right] + rw [toNat_toUInt8] + omega + · obtain ⟨h1, h2⟩ := headByte mt 25 hmt (by decide) + rw [List.cons_append] + apply decode_none_of_readArg _ _ (by omega) (by omega) + rw [h2, readArg_25, List.take_left' (netBytes_length 2 x), + readBe_netBytes 2 x (by omega), ite_eq_right] + omega + · obtain ⟨h1, h2⟩ := headByte mt 26 hmt (by decide) + rw [List.cons_append] + apply decode_none_of_readArg _ _ (by omega) (by omega) + rw [h2, readArg_26, List.take_left' (netBytes_length 4 x), + readBe_netBytes 4 x (by omega), ite_eq_right] + omega + · obtain ⟨h1, h2⟩ := headByte mt 27 hmt (by decide) + rw [List.cons_append] + apply decode_none_of_readArg _ _ (by omega) (by omega) + rw [h2, readArg_27, List.take_left' (netBytes_length 8 x), + readBe_netBytes 8 x (by omega), ite_eq_right] + omega + +namespace Cbor + +/-! ## Out-of-slice items, at the top and inside containers -/ + +/-- The reader of one item turns away an out-of-slice initial byte, + whatever its fuel. -/ +theorem decodeFuel_outOfSlice (F : Nat) (b : UInt8) (rest : List UInt8) + (hb : Spec.outOfSlice b = true) : decodeFuel F (b :: rest) = none := by + simp [Spec.outOfSlice] at hb + have hlt : b.toNat < 256 := b.toBitVec.isLt + cases F with + | zero => rfl + | succ F => + rw [decodeFuel_cons] + by_cases h7 : b.toNat / 32 = 7 + · rw [ite_eq_left h7, ite_eq_right (by omega), ite_eq_right (by omega), + ite_eq_right (by omega)] + · rw [ite_eq_right h7] + by_cases h6 : b.toNat / 32 = 6 + · rw [ite_eq_left h6] + · rw [ite_eq_right h6, readArg_none_of_ge_28 (by omega)] + +theorem wfAll_mem {xs : List Value} (h : Value.wfAll xs = true) {x : Value} (hx : x ∈ xs) : + x.wf = true := by + induction xs with + | nil => cases hx + | cons y ys ih => + simp only [Value.wfAll, Bool.and_eq_true] at h + cases hx with + | head => exact h.1 + | tail _ hm => exact ih h.2 hm + +theorem wfPairs_mem {kvs : List (Value × Value)} (h : Value.wfPairs kvs = true) + {kv : Value × Value} (hkv : kv ∈ kvs) : kv.1.wf = true ∧ kv.2.wf = true := by + induction kvs with + | nil => cases hkv + | cons p ps ih => + obtain ⟨k, v⟩ := p + simp only [Value.wfPairs, Bool.and_eq_true] at h + cases hkv with + | head => exact h.1 + | tail _ hm => exact ih h.2 hm + +theorem depth_le_depthList {xs : List Value} {x : Value} (hx : x ∈ xs) : + x.depth ≤ Value.depthList xs := by + induction xs with + | nil => cases hx + | cons y ys ih => + simp only [Value.depthList] + cases hx with + | head => omega + | tail _ hm => have := ih hm; omega + +theorem depth_le_depthPairs {kvs : List (Value × Value)} {kv : Value × Value} + (hkv : kv ∈ kvs) : kv.1.depth ≤ Value.depthPairs kvs ∧ kv.2.depth ≤ Value.depthPairs kvs := by + induction kvs with + | nil => cases hkv + | cons p ps ih => + obtain ⟨k, v⟩ := p + simp only [Value.depthPairs] + cases hkv with + | head => dsimp only; omega + | tail _ hm => have := ih hm; omega + +/-- After items it reads back, the reader of `n` items fails where the + reader of the rest fails. -/ +theorem decodeItems_skip (dec : List UInt8 → Option (Value × List UInt8)) (xs : List Value) + (s : List UInt8) (j : Nat) (hdec : ∀ x ∈ xs, ∀ r, dec (encode x ++ r) = some (x, r)) + (hj : decodeItems dec j s = none) : + decodeItems dec (xs.length + j) (encodeList xs ++ s) = none := by + induction xs with + | nil => simpa [encodeList] using hj + | cons x xs ih => + rw [List.length_cons, show xs.length + 1 + j = (xs.length + j) + 1 by omega, decodeItems_succ, + encodeList, List.append_assoc, hdec x List.mem_cons_self] + show (match decodeItems dec (xs.length + j) (encodeList xs ++ s) with + | none => none + | some (ys, r') => some (x :: ys, r')) = none + rw [ih (fun y hy => hdec y (List.mem_cons_of_mem x hy))] + +/-- After pairs it reads back, the reader of `n` pairs fails where the + reader of the rest fails. -/ +theorem decodePairs_skip (dec : List UInt8 → Option (Value × List UInt8)) + (kvs : List (Value × Value)) (s : List UInt8) (j : Nat) + (hdec : ∀ kv ∈ kvs, ∀ r, dec (encode kv.1 ++ r) = some (kv.1, r) ∧ + dec (encode kv.2 ++ r) = some (kv.2, r)) + (hj : decodePairs dec j s = none) : + decodePairs dec (kvs.length + j) (encodePairs kvs ++ s) = none := by + induction kvs with + | nil => simpa [encodePairs] using hj + | cons kv kvs ih => + obtain ⟨k, v⟩ := kv + have hk := (hdec (k, v) List.mem_cons_self (encode v ++ (encodePairs kvs ++ s))).1 + have hv := (hdec (k, v) List.mem_cons_self (encodePairs kvs ++ s)).2 + rw [List.length_cons, show kvs.length + 1 + j = (kvs.length + j) + 1 by omega, + decodePairs_succ, encodePairs, List.append_assoc, List.append_assoc, hk] + show (match dec (encode v ++ (encodePairs kvs ++ s)) with + | none => none + | some (v', r') => + match decodePairs dec (kvs.length + j) r' with + | none => none + | some (kvs', r'') => some ((k, v') :: kvs', r'')) = none + rw [hv] + show (match decodePairs dec (kvs.length + j) (encodePairs kvs ++ s) with + | none => none + | some (kvs', r'') => some ((k, v) :: kvs', r'')) = none + rw [ih (fun kv hkv => hdec kv (List.mem_cons_of_mem _ hkv))] + +/-- The decoder, on a container head of `n` items or pairs followed by + `body`: it fails when the container's reader fails. -/ +theorem decode_container_none (mt n : Nat) (body : List UInt8) (hmt : mt = 4 ∨ mt = 5) + (hn : n < 2 ^ 64) + (hitems : (mt = 4 → decodeItems (decodeFuel (head mt n ++ body).length) n body = none) ∧ + (mt = 5 → decodePairs (decodeFuel (head mt n ++ body).length) n body = none)) : + decode (head mt n ++ body) = none := by + obtain ⟨hi, hp⟩ := hitems + unfold decode + rw [decodeFuel_head mt n body (by omega) hn] + rcases hmt with rfl | rfl + · rw [ite_eq_right (by decide), ite_eq_right (by decide), ite_eq_right (by decide), + ite_eq_right (by decide), ite_eq_left rfl, hi rfl] + · rw [ite_eq_right (by decide), ite_eq_right (by decide), ite_eq_right (by decide), + ite_eq_right (by decide), ite_eq_right (by decide), ite_eq_left rfl, hp rfl] + +end Cbor + +/-- `Spec.cbor_rejects_nested_out_of_slice`. -/ +theorem Spec.cbor_rejects_nested_out_of_slice (b : UInt8) (rest : List UInt8) (n : Nat) + (xs : List Value) (kvs : List (Value × Value)) (k : Value) + (hb : Spec.outOfSlice b = true) (hn : n < 2 ^ 64) (hxs : Value.wfAll xs = true) + (hkvs : Value.wfPairs kvs = true) (hk : k.wf = true) : + decode (b :: rest) = none ∧ + (xs.length < n → decode (Spec.itemHead 4 n ++ Spec.encList xs ++ b :: rest) = none) ∧ + (kvs.length < n → decode (Spec.itemHead 5 n ++ Spec.encPairs kvs ++ b :: rest) = none) ∧ + (kvs.length < n → + decode (Spec.itemHead 5 n ++ Spec.encPairs kvs ++ Spec.enc k ++ b :: rest) = none) := by + have hbad : ∀ F, decodeFuel F (b :: rest) = none := fun F => decodeFuel_outOfSlice F b rest hb + refine ⟨?_, fun hlt => ?_, fun hlt => ?_, fun hlt => ?_⟩ + · unfold decode + rw [hbad] + · obtain ⟨j, rfl⟩ : ∃ j, n = xs.length + (j + 1) := ⟨n - xs.length - 1, by omega⟩ + rw [← head_eq_itemHead, ← encodeList_eq_encList, List.append_assoc] + apply decode_container_none 4 _ _ (Or.inl rfl) hn + refine ⟨fun _ => ?_, fun h => absurd h (by decide)⟩ + have hpos := head_length_pos 4 (xs.length + (j + 1)) + have hdl := (depthLen (Value.depthList xs)).2.1 xs (Nat.le_refl _) + generalize hF : (head 4 (xs.length + (j + 1)) ++ (encodeList xs ++ b :: rest)).length = F + simp only [List.length_append, List.length_cons] at hF + obtain ⟨F', rfl⟩ : ∃ F', F = F' + 1 := ⟨F - 1, by omega⟩ + apply decodeItems_skip _ xs _ (j + 1) + · intro x hx r + exact (rtAll F').1 x r (wfAll_mem hxs hx) (by have := depth_le_depthList hx; omega) + · rw [decodeItems_succ, hbad] + · obtain ⟨j, rfl⟩ : ∃ j, n = kvs.length + (j + 1) := ⟨n - kvs.length - 1, by omega⟩ + rw [← head_eq_itemHead, ← encodePairs_eq_encPairs, List.append_assoc] + apply decode_container_none 5 _ _ (Or.inr rfl) hn + refine ⟨fun h => absurd h (by decide), fun _ => ?_⟩ + have hpos := head_length_pos 5 (kvs.length + (j + 1)) + have hdp := (depthLen (Value.depthPairs kvs)).2.2 kvs (Nat.le_refl _) + generalize hF : (head 5 (kvs.length + (j + 1)) ++ (encodePairs kvs ++ b :: rest)).length = F + simp only [List.length_append, List.length_cons] at hF + obtain ⟨F', rfl⟩ : ∃ F', F = F' + 1 := ⟨F - 1, by omega⟩ + apply decodePairs_skip _ kvs _ (j + 1) + · intro kv hkv r + obtain ⟨hwk, hwv⟩ := wfPairs_mem hkvs hkv + obtain ⟨hdk, hdv⟩ := depth_le_depthPairs hkv + exact ⟨(rtAll F').1 kv.1 r hwk (by omega), (rtAll F').1 kv.2 r hwv (by omega)⟩ + · rw [decodePairs_succ, hbad] + · obtain ⟨j, rfl⟩ : ∃ j, n = kvs.length + (j + 1) := ⟨n - kvs.length - 1, by omega⟩ + rw [← head_eq_itemHead, ← encodePairs_eq_encPairs, ← encode_eq_enc, List.append_assoc, + List.append_assoc] + apply decode_container_none 5 _ _ (Or.inr rfl) hn + refine ⟨fun h => absurd h (by decide), fun _ => ?_⟩ + have hpos := head_length_pos 5 (kvs.length + (j + 1)) + have hdp := (depthLen (Value.depthPairs kvs)).2.2 kvs (Nat.le_refl _) + have hdk := depth_le_length k + generalize hF : (head 5 (kvs.length + (j + 1)) ++ + (encodePairs kvs ++ (encode k ++ b :: rest))).length = F + simp only [List.length_append, List.length_cons] at hF + obtain ⟨F', rfl⟩ : ∃ F', F = F' + 1 := ⟨F - 1, by omega⟩ + apply decodePairs_skip _ kvs _ (j + 1) + · intro kv hkv r + obtain ⟨hwk, hwv⟩ := wfPairs_mem hkvs hkv + obtain ⟨hdk', hdv'⟩ := depth_le_depthPairs hkv + exact ⟨(rtAll F').1 kv.1 r hwk (by omega), (rtAll F').1 kv.2 r hwv (by omega)⟩ + · rw [decodePairs_succ, (rtAll F').1 k (b :: rest) hk (by omega)] + show (match decodeFuel (F' + 1) (b :: rest) with + | none => none + | some (v', r') => + match decodePairs (decodeFuel (F' + 1)) j r' with + | none => none + | some (kvs', r'') => some ((k, v') :: kvs', r'')) = none + rw [hbad] + +/-! ## Input cut short inside an item -/ + +/-- `Spec.cbor_rejects_truncated`. -/ +theorem Spec.cbor_rejects_truncated (v : Value) (pre post : List UInt8) (hv : v.wf = true) + (h : pre ++ post = Spec.enc v) (hpost : post ≠ []) : decode pre = none := by + rw [← encode_eq_enc] at h + cases hd : decode pre with + | none => rfl + | some w => + exfalso + obtain ⟨hw, hpre⟩ := encode_decode pre w hd + subst hpre + have hlen : (encode w).length ≤ (encode v).length := by + rw [← h, List.length_append]; omega + have h1 := (rtAll (encode v).length).1 v [] hv (depth_le_length v) + have h2 := (rtAll (encode v).length).1 w post hw + (by have := depth_le_length w; omega) + rw [List.append_nil] at h1 + rw [h, h1] at h2 + injection h2 with h3 + injection h3 with _ h4 + exact hpost h4.symm diff --git a/Proofs/Utf8.lean b/Proofs/Utf8.lean new file mode 100644 index 0000000..1cf9432 --- /dev/null +++ b/Proofs/Utf8.lean @@ -0,0 +1,82 @@ +/- + The decoder's UTF-8 check, `Cbor.Utf8.valid`, is the grammar of + RFC 3629, section 4, as `Spec.Utf8.wellFormed` writes it. + + `valid_step` shows that one step of the validator, which looks at the + first byte to pick a row, gives the same answer as trying every row + of the grammar: the rows' first bytes do not overlap. Induction on + the length then gives the equality for every byte list. +-/ + +import Cbor +import Spec.Defs + +namespace Cbor.Utf8 + +/-- One step of the validator: the first character matches one row of + the grammar, and the rest is valid. -/ +theorem valid_step (a : UInt8) (rest : List UInt8) : + valid (a :: rest) = + Spec.Utf8.rows.any (fun row => Spec.Utf8.fits row ((a :: rest).take row.length) && + valid ((a :: rest).drop row.length)) := by + have ha : a.toNat < 256 := a.toBitVec.isLt + have hcls : a.toNat ≤ 0x7F ∨ (0x80 ≤ a.toNat ∧ a.toNat ≤ 0xC1) ∨ + (0xC2 ≤ a.toNat ∧ a.toNat ≤ 0xDF) ∨ a.toNat = 0xE0 ∨ (0xE1 ≤ a.toNat ∧ a.toNat ≤ 0xEC) ∨ + a.toNat = 0xED ∨ (0xEE ≤ a.toNat ∧ a.toNat ≤ 0xEF) ∨ a.toNat = 0xF0 ∨ + (0xF1 ≤ a.toNat ∧ a.toNat ≤ 0xF3) ∨ a.toNat = 0xF4 ∨ 0xF5 ≤ a.toNat := by omega + rw [valid.eq_def (a :: rest)] + rcases rest with _ | ⟨b, _ | ⟨c, _ | ⟨d, r⟩⟩⟩ <;> + simp only [Spec.Utf8.rows, List.any_cons, List.any_nil, List.length_cons, List.length_nil, + List.take, List.drop, Spec.Utf8.fits, cont] <;> + rcases hcls with h | h | h | h | h | h | h | h | h | h | h <;> + simp (disch := omega) only [decide_eq_true, decide_eq_false, ite_eq_left, ite_eq_right, + Bool.true_and, Bool.false_and, Bool.and_true, Bool.and_false, Bool.or_false, + Bool.false_or, Bool.and_assoc] + +theorem any_congr_mem {α : Type} {l : List α} {p q : α → Bool} (h : ∀ x ∈ l, p x = q x) : + l.any p = l.any q := by + induction l with + | nil => rfl + | cons x xs ih => + simp only [List.any_cons] + rw [h x List.mem_cons_self, ih (fun y hy => h y (List.mem_cons_of_mem x hy))] + +/-- Every row of the grammar is at least one byte long. -/ +theorem rows_nonempty : ∀ row ∈ Spec.Utf8.rows, 1 ≤ row.length := by + have h : Spec.Utf8.rows.all (fun row => decide (1 ≤ row.length)) = true := by decide + intro row hrow + exact of_decide_eq_true (List.all_eq_true.1 h row hrow) + +/-- With enough room for one character per byte, splitting into + characters is the validator. -/ +theorem octets_eq_valid : ∀ n bs, bs.length ≤ n → Spec.Utf8.octets n bs = valid bs := by + intro n + induction n with + | zero => + intro bs h + cases bs with + | nil => rfl + | cons a rest => simp at h + | succ n ih => + intro bs h + cases bs with + | nil => rfl + | cons a rest => + rw [valid_step] + show (Spec.Utf8.rows.any fun row => Spec.Utf8.fits row ((a :: rest).take row.length) && + Spec.Utf8.octets n ((a :: rest).drop row.length)) = _ + apply any_congr_mem + intro row hrow + have h1 := rows_nonempty row hrow + rw [ih _ (by rw [List.length_drop, List.length_cons] at *; omega)] + +/-- The validator is the RFC 3629 grammar. -/ +theorem valid_eq_wellFormed (bs : List UInt8) : valid bs = Spec.Utf8.wellFormed bs := + (octets_eq_valid bs.length bs (Nat.le_refl _)).symm + +end Cbor.Utf8 + +/-- `Spec.cbor_utf8_valid_eq`. -/ +theorem Spec.cbor_utf8_valid_eq (bs : List UInt8) : + Cbor.Utf8.valid bs = Spec.Utf8.wellFormed bs := + Cbor.Utf8.valid_eq_wellFormed bs diff --git a/README.md b/README.md index 6e7f453..59f9001 100644 --- a/README.md +++ b/README.md @@ -1,2 +1,155 @@ -# 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, working toward the verified bar +published in the org's home repo, +[mission](https://github.com/Proven-Commons/mission). It does not meet +the bar yet. + +Status: in progress. The specification has no approval from a reviewer +who did not write it, and the bar check has not yet passed in CI with +the branch rule in place, so this project is not verified. + +## 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, `Spec.cbor_encode_decode` says the +encoding is the input's bytes, so the answer is the input in lowercase +hex. The tool's hex parsing and printing are not proved; see What is +not proved. + +## What is proved + +Each claim below is a theorem of `Spec.lean`, the challenge file, proved +under the same name in `Proofs/`. The definitions the statements use +besides the code are spec files too: the item type `Value` and +well-formedness `Value.wf` in `Spec/Value.lean`, well-formed UTF-8 in +`Spec/Utf8.lean`, and the encoding `Spec.enc` in `Spec/Defs.lean`. + +The round trip, and what the encoding is: + +| Claim | Theorem | +|-------|---------| +| Decoding the encoding of a well-formed item gives the item back. | `Spec.cbor_decode_encode` | +| The decoder accepts bytes `bs` and returns the item `v` if and only if `v` is well-formed (`Value.wf`) and `bs` is the encoding of `v`. So it accepts the encodings of the well-formed items and nothing else, and never returns an item that is not well-formed. | `Spec.cbor_encode_decode` | +| For every item, the encoder writes `Spec.enc`: the encoding `Spec/Defs.lean` writes from RFC 8949, sections 3, 3.1 and 3.3, with each argument in its preferred (shortest) form, as sections 4.1 and 4.2.1 ask. | `Spec.cbor_encode_spec` | +| The decoder's UTF-8 check gives the same answer, on every byte list, as the grammar of RFC 3629, section 4, written in `Spec/Utf8.lean`. `Value.wf` asks every text payload to meet that grammar. | `Spec.cbor_utf8_valid_eq` | + +What the decoder turns away, for every input of the shape named: + +| Claim | Theorem | +|-------|---------| +| An initial byte with additional information 28 to 31 (reserved, or the indefinite form), whatever follows. | `Spec.cbor_rejects_reserved_ai` | +| A tag (major type 6), whatever follows. | `Spec.cbor_rejects_tags` | +| In major type 7, any initial byte but false, true and null: undefined, other simple values, every float, and break, whatever follows. | `Spec.cbor_rejects_simple` | +| In major types 0 to 5, additional information 24, 25, 26 or 27 followed by an argument whose value fits a shorter form, whatever follows. | `Spec.cbor_rejects_nonpreferred` | +| An item whose initial byte is outside the slice (`Spec.outOfSlice`), at the top, or as the next item of an array or the next key or value of a map, after any well-formed items before it in that container, whatever follows. This theorem covers one level of nesting; see What is not proved for deeper ones. | `Spec.cbor_rejects_nested_out_of_slice` | +| Input that ends inside an item: no proper prefix of the encoding of a well-formed item decodes. | `Spec.cbor_rejects_truncated` | + +Examples, checked by the proofs: + +| Claim | Theorem | +|-------|---------| +| All 37 rows of RFC 8949 Appendix A that are in the slice hold in both directions: encoding the item gives the bytes, and decoding the bytes gives the item. | `Spec.cbor_rfc8949_vectors` | +| All 44 rows of Appendix A outside the slice are turned away (bignums, floats, undefined and other simple values, tags, indefinite-length items alone and nested), and so is break on its own. | `Spec.cbor_rejects_out_of_slice` | +| Five text items whose payloads are not well-formed UTF-8 are turned away. | `Spec.cbor_rejects_bad_utf8` | +| Eight inputs are turned away: the empty input, six that end inside an item, and one that goes on after an item. | `Spec.cbor_rejects_truncation` | + +`lake comparator --paranoid` checks that each proof proves exactly the +statement in `Spec.lean`, uses no axiom but `propext`, +`Classical.choice` and `Quot.sound`, and is accepted by every kernel +that ships with Lean. + +## 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 sections 4.1 and 4.2.1 define. + +Out, always turned away: tags, indefinite-length items and break, +reserved additional 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 key order is checked or produced. RFC 8949's + core deterministic encoding (section 4.2.1) also sorts map keys; this + slice takes only its rule for arguments. +- That `Spec.enc`, `Value.wf` and `Spec.Utf8.wellFormed` say what + RFC 8949 and RFC 3629 say is the judgment of the spec reviewer, not a + theorem. Examples in the spec files pin each boundary of the argument + table and each row of the UTF-8 grammar. +- `Spec.cbor_rejects_nested_out_of_slice` covers an out-of-slice item + one level inside an array or map. For deeper ones there is no + theorem of their own: `Spec.cbor_encode_decode` and + `Spec.cbor_encode_spec` say the decoder accepts only `Spec.enc v`, + and that `Spec.enc` never starts an item with such a byte is read + from its definition. No row of Appendix A nests an out-of-slice item + more than one level down. The three rows with an indefinite item + inside a definite array (`83018202039f0405ff`, `83019f0203ff820405` + and `826161bf61626163ff`) are instances of this theorem, and + `Spec.cbor_rejects_out_of_slice` also lists them. The tests nest + such items up to three levels down. +- The command-line tool in `Main.lean` calls the proved `decode` and + `encode`, but its hex parsing and the canonical text form it prints + are not proved; the tests exercise them. It is a thin wrapper for the + differential tests, not a file tool, and reads requests on stdin. +- Speed and memory use are not proved. + +## What you must trust + +- The Lean 4.35.0 kernel, and the five other kernels that + `lake comparator --paranoid` runs (`leanchecker-paranoid`, + `lean4lean`, `nanoda`, `con-leche`, `con-ron`): a bug that every one + of them shares would be outside the proof. +- The Lean compiler and runtime, which turn the proved definitions into + the program that runs: a bug in them could make it differ. +- The hardware and operating system the program runs on. +- The specification itself: `SPEC.md`, `Spec.lean`, and the + definitions in `Spec/Defs.lean`, `Spec/Value.lean` and + `Spec/Utf8.lean`, which say what the theorems mean. + +There are no dependencies: `lake-manifest.json` lists no packages. The +code uses none of the features bar item 4 forbids, so `bar.toml` lists +no exceptions. + +## Re-check it + +``` +lake build +lake comparator --paranoid +python3 tests/run_tests.py +``` + +`lake build` builds the code, the challenge file and the proofs. +`lake comparator --paranoid` checks, in a sandbox, that each theorem +named in `comparator.json` proves exactly the statement in `Spec.lean`, +uses only the three standard axioms, and passes every kernel. The test +script builds the tool if needed, runs every input against the oracle, +and rewrites `tests/TEST-RESULTS.md`. Where Python's cbor2 can be +imported, the script also has cbor2, a CBOR library written apart from +this project, judge the tool's answers, counted apart from the +record's inputs. The record says whether that ran, with which version, +and how to install it. diff --git a/SPEC.md b/SPEC.md new file mode 100644 index 0000000..37e6cc9 --- /dev/null +++ b/SPEC.md @@ -0,0 +1,132 @@ +# 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`, `Spec/Defs.lean`, `Spec/Value.lean` and `Spec/Utf8.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, with every argument in its +preferred (shortest) form (sections 4.1 and 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). + `Spec.Utf8.wellFormed` in `Spec/Utf8.lean` writes the grammar of + RFC 3629, section 4: its nine rows of byte ranges, and a split of the + payload into characters that each match a row. Each row has examples + there, checked by the build. +- Major type 4: arrays, definite length. +- Major type 5: maps, definite length. +- Major type 7, additional information 20, 21, 22: `false`, `true`, + `null`. + +Out of slice, always turned away: tags (major type 6), indefinite-length +items and break (additional information 31), reserved additional +information 28 to 30, `undefined`, other simple values, half, single, +and double floats, and any argument not in preferred form. +`Spec.outOfSlice` in `Spec/Defs.lean` names the initial bytes the slice +does not carry: major type 6, major type 7 except simple values 20 to +22, and additional information 28 to 31. + +## Well-formed items + +`Value` in `Spec/Value.lean` is the item type: one constructor for each +kind of item in the slice. `Value.wf` says when an item can be sent: +every text payload is well-formed UTF-8 (`Spec.Utf8.wellFormed`), and +every string and container length is below 2^64, so it fits the 64-bit +argument. Both are spec files, so the approval covers them. + +## Encoding + +`Spec.enc` in `Spec/Defs.lean` is the encoding, written from RFC 8949: + +- `Spec.itemHead mt arg` is the head (section 3): one initial byte with + the major type in its high 3 bits and the additional information in + its low 5 bits. An argument below 24 is the additional information + itself. A larger one follows in 1, 2, 4 or 8 bytes, the fewest that + hold it (below 2^8, 2^16, 2^32, or 2^64), with additional information + 24, 25, 26 or 27 (the preferred serialization of section 4.1, and the + table of section 4.2.1). +- `Spec.netBytes n x` is the `n` bytes of `x` in network byte order. +- Unsigned `n` has major type 0 and argument `n`; the negative integer + `-1 - n` has major type 1 and argument `n`; byte and text strings + have major type 2 or 3, their length as argument, then their bytes; + arrays and maps have major type 4 or 5, their count of items or pairs + as argument, then the items, or each key followed by its value, in + order (section 3.1). `false`, `true` and `null` are major type 7 with + simple values 20, 21 and 22 (section 3.3). + +Examples in the same file check each boundary of the argument table: +23 and 24, 255 and 256, 65535 and 65536, 2^32 - 1 and 2^32, and +2^64 - 1. `Spec.cbor_encode_spec` proves that `encode` in +`Cbor/Basic.lean` writes `Spec.enc` for every item. + +## 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. +`Spec.cbor_encode_decode` says exactly what it accepts: the encodings +of the well-formed items. The rejection theorems state each kind of +input it turns away for every input of that shape. + +## 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 the encoding of a well-formed item returns the item | `Spec.cbor_decode_encode` | +| The decoder accepts a byte list exactly when it is the encoding of a well-formed item, and returns that item | `Spec.cbor_encode_decode` | +| The encoder writes `Spec.enc`, for every item | `Spec.cbor_encode_spec` | +| The decoder's UTF-8 check is the RFC 3629 grammar, on every byte list | `Spec.cbor_utf8_valid_eq` | +| Additional information 28 to 31 is turned away, whatever follows | `Spec.cbor_rejects_reserved_ai` | +| Tags are turned away, whatever follows | `Spec.cbor_rejects_tags` | +| Major type 7 other than false, true, null is turned away, whatever follows | `Spec.cbor_rejects_simple` | +| Every non-preferred argument in major types 0 to 5 is turned away, whatever follows | `Spec.cbor_rejects_nonpreferred` | +| An out-of-slice item at the top, or one level inside an array or map after well-formed items, is turned away | `Spec.cbor_rejects_nested_out_of_slice` | +| No proper prefix of the encoding of a well-formed item decodes | `Spec.cbor_rejects_truncated` | +| The 37 in-slice rows of RFC 8949 Appendix A hold, both directions | `Spec.cbor_rfc8949_vectors` | +| The 44 out-of-slice rows of Appendix A, and break alone, are turned away | `Spec.cbor_rejects_out_of_slice` | +| Five example text items with bad UTF-8 are turned away | `Spec.cbor_rejects_bad_utf8` | +| Eight example inputs are turned away: empty, cut short inside an item, or going on after one | `Spec.cbor_rejects_truncation` | + +`Spec.cbor_encode_decode` is an if and only if: `decode bs = some v` +holds exactly when `v.wf = true` and `encode v = bs`. With +`Spec.cbor_encode_spec`, `encode v` is `Spec.enc v`. So the decoder +accepts the encodings of the well-formed items that RFC 8949 and this +slice define, and nothing else, and never returns an item that is not +well-formed. + +`Spec.cbor_rejects_nested_out_of_slice` states one level of nesting. At +any depth, the decoder accepts only `Spec.enc v` for a well-formed `v`, +and `Spec.enc` starts no item with a byte `Spec.outOfSlice` names; that +second point is read from the definition of `Spec.enc`, not stated as a +theorem. + +## 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, + `Spec.cbor_encode_decode` says the encoding is the input's bytes, so + the answer is the input in lowercase hex. + +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..25df30a --- /dev/null +++ b/Spec.lean @@ -0,0 +1,269 @@ +/- + 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 definitions the statements use besides the code are in + `Spec/Defs.lean`, `Spec/Value.lean` (the item type and `Value.wf`) + and `Spec/Utf8.lean` (well-formed UTF-8, from RFC 3629). They are + 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 exactly the encodings of well-formed items, and + nothing else: it accepts `bs` and returns `v` if and only if `v` is + well-formed (`Value.wf`) and `bs` is the encoding of `v`. -/ +theorem Spec.cbor_encode_decode (bs : List UInt8) (v : Value) : + decode bs = some v ↔ v.wf = true ∧ encode v = bs := sorry + +/-! ## The encoding is RFC 8949's preferred serialization -/ + +/-- The encoder writes `Spec.enc`, the encoding `Spec/Defs.lean` writes + from RFC 8949 (sections 3, 3.1 and 3.3, with the preferred + serialization of sections 4.1 and 4.2.1), for every item. So the + two claims above are about that encoding. -/ +theorem Spec.cbor_encode_spec (v : Value) : encode v = Spec.enc v := sorry + +/-! ## Text strings: the UTF-8 check is RFC 3629 + +`Value.wf` asks every text payload to be `Spec.Utf8.wellFormed`, the +grammar of RFC 3629, section 4. The decoder checks text payloads with +`Utf8.valid`; this says the two agree on every byte list. -/ + +theorem Spec.cbor_utf8_valid_eq (bs : List UInt8) : + Cbor.Utf8.valid bs = Spec.Utf8.wellFormed bs := sorry + +/-! ## Additional information the RFC holds back, and the indefinite form -/ + +/-- An initial byte with additional information 28 to 30 (reserved by + RFC 8949, section 3) 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 + +Appendix A has 81 rows. Each of the 37 rows in the slice holds in both +directions. The other 44 (bignums, floats, undefined and other simple +values, tags, and indefinite lengths) are turned away, in the theorem +after this one. The differential tests run all 81. -/ + +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]) ∧ + decode (0x98 :: 0x19 :: ((List.range 23).map fun n => (n + 1).toUInt8) ++ + [0x18, 0x18, 0x18, 0x19]) = + some (.array ((List.range 25).map fun n => .uint (n + 1).toUInt64)) ∧ + -- 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] ∧ + decode [0xa5, 0x61, 0x61, 0x61, 0x41, 0x61, 0x62, 0x61, 0x42, 0x61, 0x63, 0x61, 0x43, + 0x61, 0x64, 0x61, 0x44, 0x61, 0x65, 0x61, 0x45] = + some (.map [(.text [0x61], .text [0x41]), (.text [0x62], .text [0x42]), + (.text [0x63], .text [0x43]), (.text [0x64], .text [0x44]), + (.text [0x65], .text [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 + +/-- Every row of Appendix A outside the slice, all 44, is turned away: + bignums (tags 2 and 3), floats, undefined, simple(16), simple(255), + tags, and indefinite-length items, at the top or nested. Break on its + own is turned away too. -/ +theorem Spec.cbor_rejects_out_of_slice : + -- Bignums (tags 2 and 3) + 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 ∧ + -- Floats: half, single and double, including infinities and NaN + decode [0xf9, 0x00, 0x00] = none ∧ + decode [0xf9, 0x80, 0x00] = none ∧ + decode [0xf9, 0x3c, 0x00] = none ∧ + decode [0xfb, 0x3f, 0xf1, 0x99, 0x99, 0x99, 0x99, 0x99, 0x9a] = none ∧ + decode [0xf9, 0x3e, 0x00] = none ∧ + decode [0xf9, 0x7b, 0xff] = none ∧ + decode [0xfa, 0x47, 0xc3, 0x50, 0x00] = none ∧ + decode [0xfa, 0x7f, 0x7f, 0xff, 0xff] = none ∧ + decode [0xfb, 0x7e, 0x37, 0xe4, 0x3c, 0x88, 0x00, 0x75, 0x9c] = none ∧ + decode [0xf9, 0x00, 0x01] = none ∧ + decode [0xf9, 0x04, 0x00] = none ∧ + decode [0xf9, 0xc4, 0x00] = none ∧ + decode [0xfb, 0xc0, 0x10, 0x66, 0x66, 0x66, 0x66, 0x66, 0x66] = none ∧ + decode [0xf9, 0x7c, 0x00] = none ∧ + decode [0xf9, 0x7e, 0x00] = none ∧ + decode [0xf9, 0xfc, 0x00] = none ∧ + decode [0xfa, 0x7f, 0x80, 0x00, 0x00] = none ∧ + decode [0xfa, 0x7f, 0xc0, 0x00, 0x00] = none ∧ + decode [0xfa, 0xff, 0x80, 0x00, 0x00] = none ∧ + decode [0xfb, 0x7f, 0xf0, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] = none ∧ + decode [0xfb, 0x7f, 0xf8, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] = none ∧ + decode [0xfb, 0xff, 0xf0, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] = none ∧ + -- undefined, simple(16), simple(255) + decode [0xf7] = none ∧ + decode [0xf0] = none ∧ + decode [0xf8, 0xff] = none ∧ + -- Tags 0, 1, 23, 24, 32 + 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 [0xc1, 0xfb, 0x41, 0xd4, 0x52, 0xd9, 0xec, 0x20, 0x00, 0x00] = none ∧ + decode [0xd7, 0x44, 0x01, 0x02, 0x03, 0x04] = none ∧ + decode [0xd8, 0x18, 0x45, 0x64, 0x49, 0x45, 0x54, 0x46] = none ∧ + decode [0xd8, 0x20, 0x76, 0x68, 0x74, 0x74, 0x70, 0x3a, 0x2f, 0x2f, 0x77, 0x77, 0x77, 0x2e, + 0x65, 0x78, 0x61, 0x6d, 0x70, 0x6c, 0x65, 0x2e, 0x63, 0x6f, 0x6d] = none ∧ + -- Indefinite-length strings, arrays and maps, alone or nested + 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 [0x9f, 0x01, 0x82, 0x02, 0x03, 0x82, 0x04, 0x05, 0xff] = none ∧ + decode [0x83, 0x01, 0x82, 0x02, 0x03, 0x9f, 0x04, 0x05, 0xff] = none ∧ + decode [0x83, 0x01, 0x9f, 0x02, 0x03, 0xff, 0x82, 0x04, 0x05] = none ∧ + decode [0x9f, 0x01, 0x02, 0x03, 0x04, 0x05, 0x06, 0x07, 0x08, 0x09, 0x0a, 0x0b, 0x0c, 0x0d, + 0x0e, 0x0f, 0x10, 0x11, 0x12, 0x13, 0x14, 0x15, 0x16, 0x17, 0x18, 0x18, 0x18, 0x19, + 0xff] = none ∧ + decode [0xbf, 0x61, 0x61, 0x01, 0x61, 0x62, 0x9f, 0x02, 0x03, 0xff, 0xff] = none ∧ + decode [0x82, 0x61, 0x61, 0xbf, 0x61, 0x62, 0x61, 0x63, 0xff] = none ∧ + decode [0xbf, 0x63, 0x46, 0x75, 0x6e, 0xf5, 0x63, 0x41, 0x6d, 0x74, 0x21, 0xff] = none ∧ + -- Break, on its own + decode [0xff] = none := sorry + +/-- Non-preferred arguments are turned away (RFC 8949, section 4.2.1), + for every major type from 0 to 5, every value, and whatever bytes + follow: additional information 24, 25, 26 or 27, followed by an + argument in 1, 2, 4 or 8 bytes whose value fits a shorter form. + Every such argument is `Spec.netBytes` of its value. -/ +theorem Spec.cbor_rejects_nonpreferred (mt x : Nat) (rest : List UInt8) (hmt : mt ≤ 5) : + (x < 24 → decode ((mt * 32 + 24).toUInt8 :: Spec.netBytes 1 x ++ rest) = none) ∧ + (x < 2 ^ 8 → decode ((mt * 32 + 25).toUInt8 :: Spec.netBytes 2 x ++ rest) = none) ∧ + (x < 2 ^ 16 → decode ((mt * 32 + 26).toUInt8 :: Spec.netBytes 4 x ++ rest) = none) ∧ + (x < 2 ^ 32 → decode ((mt * 32 + 27).toUInt8 :: Spec.netBytes 8 x ++ rest) = none) := sorry + +/-- An item outside the slice is turned away at the top, and one level + down: as the next item of an array, or as the next key or the next + value of a map, after any well-formed items before it in that + container, and whatever bytes follow. `Spec.outOfSlice` says which + initial bytes the slice does not carry. -/ +theorem Spec.cbor_rejects_nested_out_of_slice (b : UInt8) (rest : List UInt8) (n : Nat) + (xs : List Value) (kvs : List (Value × Value)) (k : Value) + (hb : Spec.outOfSlice b = true) (hn : n < 2 ^ 64) (hxs : Value.wfAll xs = true) + (hkvs : Value.wfPairs kvs = true) (hk : k.wf = true) : + decode (b :: rest) = none ∧ + (xs.length < n → decode (Spec.itemHead 4 n ++ Spec.encList xs ++ b :: rest) = none) ∧ + (kvs.length < n → decode (Spec.itemHead 5 n ++ Spec.encPairs kvs ++ b :: rest) = none) ∧ + (kvs.length < n → + decode (Spec.itemHead 5 n ++ Spec.encPairs kvs ++ Spec.enc k ++ b :: rest) = 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: no proper prefix of + the encoding of a well-formed item decodes. -/ +theorem Spec.cbor_rejects_truncated (v : Value) (pre post : List UInt8) (hv : v.wf = true) + (h : pre ++ post = Spec.enc v) (hpost : post ≠ []) : decode pre = none := sorry + +/-- Examples: the empty input, input that ends inside an item, and + input that goes on after an item. -/ +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..457b2be --- /dev/null +++ b/Spec/Defs.lean @@ -0,0 +1,122 @@ +/- + The definitions the statements in `Spec.lean` use besides the code + under proof: the encoding of an item, written from RFC 8949, and the + initial bytes the slice does not carry. Part of the specification for + this slice, with `Spec.lean` and `SPEC.md`; the specification is + unreviewed (see `SPEC.md`). + + - `Spec/Utf8.lean`: well-formed UTF-8, written from the grammar of + RFC 3629, section 4, with one example for each row. + - `Spec/Value.lean`: the item type and its well-formedness. + - This file: `Spec.enc`, the preferred serialization of an item + (RFC 8949, sections 3, 3.1, 3.3, 4.1 and 4.2.1), with examples at + every boundary of the argument table, and `Spec.outOfSlice`. +-/ + +import Spec.Value + +namespace Spec + +open Cbor + +/-- The `n` bytes of `x` in network byte order, most significant byte + first (RFC 8949, section 3): the first byte is the base-256 digit + of `x` for 256^(n-1), the last is the digit for 256^0. -/ +def netBytes : Nat → Nat → List UInt8 + | 0, _ => [] + | n + 1, x => (x / 256 ^ n % 256).toUInt8 :: netBytes n x + +/-- The head of an item of major type `mt` with argument `arg` + (RFC 8949, section 3). The initial byte holds the major type in its + high 3 bits and the additional information in its low 5 bits. The + argument takes its preferred serialization (section 4.1; the + table in section 4.2.1): below 24 it is the additional information + itself; otherwise it follows the initial byte in 1, 2, 4 or 8 + bytes, the fewest that hold it, with additional information 24, + 25, 26 or 27. -/ +def itemHead (mt arg : Nat) : List UInt8 := + if arg < 24 then [(mt * 32 + arg).toUInt8] + else if arg < 2 ^ 8 then (mt * 32 + 24).toUInt8 :: netBytes 1 arg + else if arg < 2 ^ 16 then (mt * 32 + 25).toUInt8 :: netBytes 2 arg + else if arg < 2 ^ 32 then (mt * 32 + 26).toUInt8 :: netBytes 4 arg + else (mt * 32 + 27).toUInt8 :: netBytes 8 arg + +mutual +/-- The encoding of an item (RFC 8949, sections 3.1 and 3.3): + - an unsigned integer `n`: major type 0, argument `n`; + - the negative integer -1 - n: major type 1, argument `n`; + - a byte or text string: major type 2 or 3, argument the number of + bytes, then the bytes; + - an array: major type 4, argument the number of items, then the + items in order; + - a map: major type 5, argument the number of pairs, then each key + followed by its value, in order; + - false, true and null: major type 7, simple values 20, 21 and 22, + held in the additional information. -/ +def enc : Value → List UInt8 + | .uint n => itemHead 0 n.toNat + | .nint n => itemHead 1 n.toNat + | .bytes bs => itemHead 2 bs.length ++ bs + | .text bs => itemHead 3 bs.length ++ bs + | .array xs => itemHead 4 xs.length ++ encList xs + | .map kvs => itemHead 5 kvs.length ++ encPairs kvs + | .vfalse => itemHead 7 20 + | .vtrue => itemHead 7 21 + | .vnull => itemHead 7 22 + +/-- The items of an array, one after another. -/ +def encList : List Value → List UInt8 + | [] => [] + | x :: xs => enc x ++ encList xs + +/-- The pairs of a map, each key followed by its value. -/ +def encPairs : List (Value × Value) → List UInt8 + | [] => [] + | (k, v) :: kvs => enc k ++ enc v ++ encPairs kvs +end + +/-- An initial byte the slice does not carry: major type 6 (a tag); in + major type 7, anything but simple values 20, 21 and 22 (other + simple values, floats, and break); or additional information 28 + to 31 (held back by RFC 8949, section 3, and the indefinite form). + No encoding `enc` writes starts an item with such a byte. -/ +def outOfSlice (b : UInt8) : Bool := + b.toNat / 32 = 6 || + (b.toNat / 32 = 7 && !(b.toNat % 32 = 20 || b.toNat % 32 = 21 || b.toNat % 32 = 22)) || + 28 ≤ b.toNat % 32 + +/-! ## Examples at each boundary of the argument table (RFC 8949, 4.2.1) + +Each argument form at its smallest and largest value. A mistake in +`itemHead` fails the build. -/ + +example : enc (.uint 23) = [0x17] := rfl +example : enc (.uint 24) = [0x18, 0x18] := rfl +example : enc (.uint 255) = [0x18, 0xff] := rfl +example : enc (.uint 256) = [0x19, 0x01, 0x00] := rfl +example : enc (.uint 65535) = [0x19, 0xff, 0xff] := rfl +example : enc (.uint 65536) = [0x1a, 0x00, 0x01, 0x00, 0x00] := rfl +example : enc (.uint 4294967295) = [0x1a, 0xff, 0xff, 0xff, 0xff] := rfl +example : enc (.uint 4294967296) = [0x1b, 0x00, 0x00, 0x00, 0x01, 0x00, 0x00, 0x00, 0x00] := rfl +example : enc (.uint 18446744073709551615) = + [0x1b, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff] := rfl +example : enc (.nint 23) = [0x37] := rfl -- -24 +example : enc (.nint 24) = [0x38, 0x18] := rfl -- -25 +example : enc (.nint 255) = [0x38, 0xff] := rfl -- -256 +example : enc (.nint 256) = [0x39, 0x01, 0x00] := rfl -- -257 +example : enc (.bytes [0xaa]) = [0x41, 0xaa] := rfl +example : enc (.text [0x61, 0x62]) = [0x62, 0x61, 0x62] := rfl +example : enc (.array [.vfalse, .vtrue, .vnull]) = [0x83, 0xf4, 0xf5, 0xf6] := rfl +example : enc (.map [(.uint 1, .array [])]) = [0xa1, 0x01, 0x80] := rfl + +example : outOfSlice 0xc0 = true := rfl -- tag 0 +example : outOfSlice 0xf7 = true := rfl -- undefined +example : outOfSlice 0xf9 = true := rfl -- half float +example : outOfSlice 0xff = true := rfl -- break +example : outOfSlice 0x9f = true := rfl -- indefinite array +example : outOfSlice 0x1c = true := rfl -- reserved +example : outOfSlice 0xf6 = false := rfl -- null +example : outOfSlice 0x1b = false := rfl -- 8-byte unsigned +example : outOfSlice 0xbb = false := rfl -- map, 8-byte count + +end Spec diff --git a/Spec/Utf8.lean b/Spec/Utf8.lean new file mode 100644 index 0000000..2a3f46d --- /dev/null +++ b/Spec/Utf8.lean @@ -0,0 +1,118 @@ +/- + Well-formed UTF-8, written from the grammar in RFC 3629, section 4. + Unicode's Table 3-7 (Well-Formed UTF-8 Byte Sequences) has the same + rows. Part of the specification: `bar.toml` lists this file, so the + approval covers it. + + The grammar of RFC 3629, section 4: + + UTF8-octets = *( UTF8-char ) + UTF8-char = UTF8-1 / UTF8-2 / UTF8-3 / UTF8-4 + UTF8-1 = %x00-7F + UTF8-2 = %xC2-DF UTF8-tail + UTF8-3 = %xE0 %xA0-BF UTF8-tail / %xE1-EC 2( UTF8-tail ) / + %xED %x80-9F UTF8-tail / %xEE-EF 2( UTF8-tail ) + UTF8-4 = %xF0 %x90-BF 2( UTF8-tail ) / %xF1-F3 3( UTF8-tail ) / + %xF4 %x80-8F 2( UTF8-tail ) + UTF8-tail = %x80-BF + + `rows` below holds the nine alternatives of `UTF8-char`, with each + `UTF8-tail` written out as its range. `wellFormed` is + `UTF8-octets`: the bytes split into a run of characters, each one + matching a row. +-/ + +namespace Spec.Utf8 + +/-- The alternatives of `UTF8-char`, one per line of the grammar. Each + is a list of byte ranges, low and high inclusive, one range for + each byte of the character. -/ +def rows : List (List (Nat × Nat)) := + [ [(0x00, 0x7F)], -- UTF8-1 + [(0xC2, 0xDF), (0x80, 0xBF)], -- UTF8-2 + [(0xE0, 0xE0), (0xA0, 0xBF), (0x80, 0xBF)], -- UTF8-3 + [(0xE1, 0xEC), (0x80, 0xBF), (0x80, 0xBF)], + [(0xED, 0xED), (0x80, 0x9F), (0x80, 0xBF)], + [(0xEE, 0xEF), (0x80, 0xBF), (0x80, 0xBF)], + [(0xF0, 0xF0), (0x90, 0xBF), (0x80, 0xBF), (0x80, 0xBF)], -- UTF8-4 + [(0xF1, 0xF3), (0x80, 0xBF), (0x80, 0xBF), (0x80, 0xBF)], + [(0xF4, 0xF4), (0x80, 0x8F), (0x80, 0xBF), (0x80, 0xBF)] ] + +/-- Do the bytes match the row: as many bytes as ranges, and each byte + inside its range. -/ +def fits : List (Nat × Nat) → List UInt8 → Bool + | [], [] => true + | (lo, hi) :: row, b :: bs => decide (lo ≤ b.toNat ∧ b.toNat ≤ hi) && fits row bs + | _, _ => false + +/-- `UTF8-octets = *( UTF8-char )`, with at most `n` characters: the + bytes are empty, or some row matches their first bytes and the + rest splits the same way. -/ +def octets : Nat → List UInt8 → Bool + | _, [] => true + | 0, _ :: _ => false + | n + 1, bs => rows.any fun row => fits row (bs.take row.length) && octets n (bs.drop row.length) + +/-- Well-formed UTF-8 (RFC 3629, section 4): the bytes split into + characters. Every character takes at least one byte, so a split + never needs more characters than there are bytes. -/ +def wellFormed (bs : List UInt8) : Bool := octets bs.length bs + +/-! ## One example for each row of the grammar + +The smallest and the largest character of each row are well-formed. A +byte just outside a row's range is turned away: overlong forms, the +surrogate halves, values past U+10FFFF, lone and missing tails. A +mistake in `rows` fails the build. -/ + +example : wellFormed [] = true := rfl +-- UTF8-1: U+0000 and U+007F +example : wellFormed [0x00] = true := rfl +example : wellFormed [0x7F] = true := rfl +example : wellFormed [0x80] = false := rfl -- a lone tail +-- UTF8-2: U+0080 and U+07FF +example : wellFormed [0xC2, 0x80] = true := rfl +example : wellFormed [0xDF, 0xBF] = true := rfl +example : wellFormed [0xC1, 0xBF] = false := rfl -- overlong +example : wellFormed [0xC2, 0x7F] = false := rfl -- tail below 80 +example : wellFormed [0xC2, 0xC0] = false := rfl -- tail above BF +example : wellFormed [0xC2] = false := rfl -- cut short +-- UTF8-3, E0 row: U+0800 and U+0FFF +example : wellFormed [0xE0, 0xA0, 0x80] = true := rfl +example : wellFormed [0xE0, 0xBF, 0xBF] = true := rfl +example : wellFormed [0xE0, 0x9F, 0xBF] = false := rfl -- overlong +-- UTF8-3, E1-EC row: U+1000 and U+CFFF +example : wellFormed [0xE1, 0x80, 0x80] = true := rfl +example : wellFormed [0xEC, 0xBF, 0xBF] = true := rfl +example : wellFormed [0xE6, 0xB0, 0xB4] = true := rfl -- U+6C34 +example : wellFormed [0xE1, 0x80] = false := rfl -- cut short +-- UTF8-3, ED row: U+D000 and U+D7FF +example : wellFormed [0xED, 0x80, 0x80] = true := rfl +example : wellFormed [0xED, 0x9F, 0xBF] = true := rfl +example : wellFormed [0xED, 0xA0, 0x80] = false := rfl -- surrogate U+D800 +example : wellFormed [0xED, 0xBF, 0xBF] = false := rfl -- surrogate U+DFFF +-- UTF8-3, EE-EF row: U+E000 and U+FFFF +example : wellFormed [0xEE, 0x80, 0x80] = true := rfl +example : wellFormed [0xEF, 0xBF, 0xBF] = true := rfl +example : wellFormed [0xEF, 0xBF, 0xC0] = false := rfl -- tail above BF +-- UTF8-4, F0 row: U+10000 and U+3FFFF +example : wellFormed [0xF0, 0x90, 0x80, 0x80] = true := rfl +example : wellFormed [0xF0, 0xBF, 0xBF, 0xBF] = true := rfl +example : wellFormed [0xF0, 0x8F, 0xBF, 0xBF] = false := rfl -- overlong +-- UTF8-4, F1-F3 row: U+40000 and U+FFFFF +example : wellFormed [0xF1, 0x80, 0x80, 0x80] = true := rfl +example : wellFormed [0xF3, 0xBF, 0xBF, 0xBF] = true := rfl +example : wellFormed [0xF1, 0x80, 0x80] = false := rfl -- cut short +-- UTF8-4, F4 row: U+100000 and U+10FFFF +example : wellFormed [0xF4, 0x80, 0x80, 0x80] = true := rfl +example : wellFormed [0xF4, 0x8F, 0xBF, 0xBF] = true := rfl +example : wellFormed [0xF4, 0x90, 0x80, 0x80] = false := rfl -- past U+10FFFF +-- No row starts with C0, C1, or F5 to FF. +example : wellFormed [0xC0, 0x80] = false := rfl +example : wellFormed [0xF5, 0x80, 0x80, 0x80] = false := rfl +example : wellFormed [0xFF] = false := rfl +-- A run of characters, then one bad byte in the middle. +example : wellFormed [0x61, 0xC3, 0xBC, 0x62] = true := rfl -- "aüb" +example : wellFormed [0x61, 0x80, 0x62] = false := rfl + +end Spec.Utf8 diff --git a/Spec/Value.lean b/Spec/Value.lean new file mode 100644 index 0000000..e153e99 --- /dev/null +++ b/Spec/Value.lean @@ -0,0 +1,70 @@ +/- + The CBOR data item of this slice and its well-formedness. Part of the + specification: `bar.toml` lists this file, so the approval covers the + type the statements quantify over and the condition the round trips + assume. The code in `Cbor/Basic.lean` imports it. + + The slice is RFC 8949, definite-length items only: unsigned and + negative integers (major types 0 and 1), byte strings (2), text + strings (3), arrays (4), maps (5), and the simple values false, true, + and null (major type 7, additional information 20, 21, 22). +-/ + +import Spec.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, in order. -/ + | map (kvs : List (Value × Value)) + /-- Major type 7, additional information 20. -/ + | vfalse + /-- Major type 7, additional information 21. -/ + | vtrue + /-- Major type 7, additional information 22. -/ + | vnull + +mutual +/-- Does an item fit on the wire in this slice: every text payload is + well-formed UTF-8 (RFC 8949, section 3.1, asks for RFC 3629, and + `Spec.Utf8.wellFormed` is its section 4 grammar), and every string + and container length fits in the 64-bit argument. Any item small + enough to exist in memory passes the length checks. -/ +def Value.wf : Value → Bool + | .uint _ => Bool.true + | .nint _ => Bool.true + | .bytes bs => bs.length < 2 ^ 64 + | .text bs => Spec.Utf8.wellFormed 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 + +/-- Every item of the list is well-formed. -/ +def Value.wfAll : List Value → Bool + | [] => true + | x :: xs => x.wf && Value.wfAll xs + +/-- Every key and every value of the list is well-formed. -/ +def Value.wfPairs : List (Value × Value) → Bool + | [] => true + | (k, v) :: kvs => k.wf && v.wf && Value.wfPairs kvs +end + +example : (Value.text [0x61, 0xC3, 0xBC]).wf = true := rfl +example : (Value.text [0xFF]).wf = false := rfl +example : (Value.array [.text [0x61], .map [(.uint 1, .text [0xED, 0xA0, 0x80])]]).wf = false := rfl + +end Cbor diff --git a/bar.toml b/bar.toml new file mode 100644 index 0000000..028702d --- /dev/null +++ b/bar.toml @@ -0,0 +1,37 @@ +# 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, and +# revised by zero-aska to answer the reviews of pull request #2. +spec_authors = ["ahrazzle", "zero-aska"] +# The program people run. A change to it voids the approval. +entry_points = ["Main.lean"] + +[spec] +files = ["SPEC.md", "Spec.lean", "Spec/Defs.lean", "Spec/Value.lean", "Spec/Utf8.lean"] +# The code under proof: the functions the statements are about. The item +# type and Value.wf only give the statements their meaning, so they are +# in the spec files above, not here. +code = [ + "Cbor.encode", "Cbor.encodeList", "Cbor.encodePairs", + "Cbor.decode", "Cbor.decodeFuel", "Cbor.decodeItems", "Cbor.decodePairs", + "Cbor.head", "Cbor.readArg", "Cbor.Utf8.valid", +] + +# 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..bc3ad81 --- /dev/null +++ b/comparator.json @@ -0,0 +1,15 @@ +{ + "challenge_module": "Spec", + "solution_module": "Proofs", + "theorem_names": [ + "Spec.cbor_decode_encode", "Spec.cbor_encode_decode", "Spec.cbor_encode_spec", + "Spec.cbor_utf8_valid_eq", + "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_nested_out_of_slice", + "Spec.cbor_rejects_bad_utf8", "Spec.cbor_rejects_truncated", + "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..ff5ebb9 --- /dev/null +++ b/lakefile.toml @@ -0,0 +1,17 @@ +name = "cbor" +version = "0.1.0" +license = "Apache-2.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..bbc7c43 --- /dev/null +++ b/tests/TEST-RESULTS.md @@ -0,0 +1,83 @@ +# Test results + +Written by `python3 tests/run_tests.py`, which feeds each input to the +command-line tool built from the proved code (`.lake/build/bin/cbor`) +and compares its answer with the oracle's. + +- Oracle: reference codec in `tests/run_tests.py`, on Python 3.13.17; cross-checked against cbor2 6.1.5, counted apart +- Seed: 20261025 +- Inputs: 4298 +- Failures: 0 + +The oracle is a decoder and encoder of the slice written from RFC 8949 +apart from the Lean code, in the test script itself. It checks text +payloads with Python's strict UTF-8 decoder, which follows RFC 3629. + +Inputs by section: + + - RFC 8949 Appendix A rows and other out-of-slice shapes: 196 + - Generated well-formed items and their truncations: 1310 + - Random bytes: 611 + - Non-preferred arguments and preferred controls: 228 + - Out-of-slice initial bytes, at the top and nested: 595 + - Malformed UTF-8 examples: 6 + - UTF-8 grammar rows: 1350 + - Trailing bytes and empty input: 2 + +The RFC 8949 Appendix A section runs all 81 rows: the 37 in the slice +are decoded and encoded again, and the 44 outside it (bignums, floats, +`undefined` and other simple values, tags, indefinite-length items) are +turned away, in both directions. None is skipped. It also runs 17 other +shapes outside the slice: simple(24), more tags and indefinite items, +break on its own, and reserved additional information. + +Each input is one request to the tool: `d` (decode) or `r` (decode and +encode again). This script does not check proofs or axioms; `lake +comparator --paranoid` does. + +## Cross-check against cbor2 + +The plan in issue #1 named Python cbor2 as the oracle. The record's +oracle is the reference codec above instead, so that CI, which installs +nothing beyond Python's standard library, reruns the same inputs and +gets the same numbers. The reference codec is written apart from the +Lean code, but by the same project. So where cbor2, a CBOR library +written apart from this project, can be imported, the script also has +cbor2 judge the tool's answers. Those requests are counted apart, not +in Inputs, so a run with or without cbor2 records the same Inputs. A +disagreement is a failure, listed under Failures above. + +cbor2 accepts an input when `cbor2.loads` reads it, every value in it +is of a kind the slice carries (false, true, null, an integer from +-2^64 to 2^64 - 1, a byte or text string, an array, a map), and +`cbor2.dumps` writes the same bytes back. That last step turns away +what cbor2 reads but the slice does not: arguments not in preferred +form, indefinite lengths, tags that come back as plain values, and +bytes after the item. The tool's `d` answer must be the canonical text +of cbor2's value, or `error` when cbor2 does not accept; for an input +cbor2 accepts, the `r` answer must be the input. An input is left out +when cbor2 reads it, writes other bytes back, and a map in it holds +two keys that are equal as Python values (the same key twice, or 1 and +true, or 0 and false): cbor2 keeps one pair of those, and the slice +keeps every pair, since it applies no duplicate-key rule. + +In this run cbor2 6.1.5 could be imported, and the cross-check ran. The +requests by part, where each input cbor2 accepts is asked twice, `d` and +`r`: + + - All inputs of 0, 1 or 2 bytes: 66751 requests; cbor2 accepted 958 inputs, refused 64835 + - RFC 8949 Appendix A, all 81 rows: 118 requests; cbor2 accepted 37 inputs, refused 44 + - Random bytes, 3 to 9 long: 30206 requests; cbor2 accepted 206 inputs, refused 29794 + - Text items with 1 to 4 payload bytes, each random or from 80 to bf: 11012 requests; cbor2 accepted 1012 inputs, refused 8988 + - Random values written by cbor2.dumps, and 3 mutations of each: 28505 requests; cbor2 accepted 8516 inputs, refused 11473, left out 11 + +In all: 136592 requests, from 10729 inputs cbor2 accepted and 115134 it +refused, with 0 disagreements. 11 inputs were left out because a map in +them holds two keys that are equal as Python values. + +To run the cross-check, install cbor2 6.1.5, the version the committed +record used, where the script can import it. For example: + + python3 -m venv /tmp/cbor2-venv + /tmp/cbor2-venv/bin/pip install cbor2==6.1.5 + /tmp/cbor2-venv/bin/python tests/run_tests.py diff --git a/tests/run_tests.py b/tests/run_tests.py new file mode 100644 index 0000000..3c578ff --- /dev/null +++ b/tests/run_tests.py @@ -0,0 +1,809 @@ +#!/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. Where the cbor2 library can be imported, it also +has cbor2 judge the tool's answers, counted apart (see +`cbor2_cross_check`). 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 itertools +import random +import subprocess +import sys +import textwrap +import threading +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 +# Inputs fed to the Lean tool, by section of this script. +section = "start" +per_section = {} + + +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] + + +# The rows of RFC 3629, section 4 (Unicode Table 3-7): the code points +# each row encodes, and its byte ranges, one per byte. +UTF8_ROW_SCALARS = [ + (0x0000, 0x007F), (0x0080, 0x07FF), (0x0800, 0x0FFF), (0x1000, 0xCFFF), + (0xD000, 0xD7FF), (0xE000, 0xFFFF), (0x10000, 0x3FFFF), + (0x40000, 0xFFFFF), (0x100000, 0x10FFFF), +] +UTF8_ROW_BYTES = [ + [(0x00, 0x7F)], + [(0xC2, 0xDF), (0x80, 0xBF)], + [(0xE0, 0xE0), (0xA0, 0xBF), (0x80, 0xBF)], + [(0xE1, 0xEC), (0x80, 0xBF), (0x80, 0xBF)], + [(0xED, 0xED), (0x80, 0x9F), (0x80, 0xBF)], + [(0xEE, 0xEF), (0x80, 0xBF), (0x80, 0xBF)], + [(0xF0, 0xF0), (0x90, 0xBF), (0x80, 0xBF), (0x80, 0xBF)], + [(0xF1, 0xF3), (0x80, 0xBF), (0x80, 0xBF), (0x80, 0xBF)], + [(0xF4, 0xF4), (0x80, 0x8F), (0x80, 0xBF), (0x80, 0xBF)], +] + + +# ---------- 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 + per_section[section] = per_section.get(section, 0) + 1 + self.proc.stdin.write(f"{op} {hexs}\n") + self.proc.stdin.flush() + return self.proc.stdout.readline().rstrip("\n") + + def ask_many(self, reqs): + """Send many (op, hex) requests and read the answers in order. + Used by the cbor2 cross-check, whose inputs are not counted in + Inputs.""" + answers = [] + for i in range(0, len(reqs), 2000): + chunk = reqs[i:i + 2000] + + def write(): + self.proc.stdin.write("".join(f"{op} {h}\n" for op, h in chunk)) + self.proc.stdin.flush() + w = threading.Thread(target=write) + w.start() + answers += [self.proc.stdout.readline().rstrip("\n") for _ in chunk] + w.join() + return answers + + +# ---------- 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'}]"), + ("a56161614161626142616361436164614461656145", + "{t'61':t'41',t'62':t'42',t'63':t'43',t'64':t'44',t'65':t'45'}"), + ("f4", "false"), ("f5", "true"), ("f6", "null"), +] + +# The other 44 rows of RFC 8949 Appendix A, all outside the slice: +# bignums, floats, undefined and other simple values, tags, and +# indefinite-length items, alone or nested. With RFC_OK, this is every +# row of Appendix A (81). +RFC_A_OUT = [ + "c249010000000000000000", "c349010000000000000000", + "f90000", "f98000", "f93c00", "fb3ff199999999999a", "f93e00", "f97bff", + "fa47c35000", "fa7f7fffff", "fb7e37e43c8800759c", "f90001", "f90400", + "f9c400", "fbc010666666666666", "f97c00", "f97e00", "f9fc00", + "fa7f800000", "fa7fc00000", "faff800000", "fb7ff0000000000000", + "fb7ff8000000000000", "fbfff0000000000000", + "f7", "f0", "f8ff", + "c074323031332d30332d32315432303a30343a30305a", "c11a514b67b0", + "c1fb41d452d9ec200000", "d74401020304", "d818456449455446", + "d82076687474703a2f2f7777772e6578616d706c652e636f6d", + "5f42010243030405ff", "7f657374726561646d696e67ff", "9fff", + "9f018202039f0405ffff", "9f01820203820405ff", "83018202039f0405ff", + "83019f0203ff820405", + "9f0102030405060708090a0b0c0d0e0f101112131415161718181819ff", + "bf61610161629f0203ffff", "826161bf61626163ff", + "bf6346756ef563416d7421ff", +] + +# Other shapes outside the slice, not rows of Appendix A: simple(24), +# which section 3.3 calls not well-formed, more tags and indefinite +# items, break on its own, and reserved additional information. +OTHER_REJECT = [ + "f818", "d8204567696751554d", "d8234567696751554d", + "5f4100ff", "7f6141ff", "bf616101ff", "ff", + "1c", "1d", "1e", "1f", "3c", "5c", "7c", "9c", "bc", "dc", +] + + +def out_of_slice(b): + """An initial byte the slice does not carry: a tag, major type 7 + other than false, true and null, or additional information 28 to + 31. Written from RFC 8949 section 3, apart from the Lean code.""" + mt, ai = b >> 5, b & 31 + return mt == 6 or (mt == 7 and ai not in (20, 21, 22)) or ai >= 28 + + +def completion(b): + """Bytes that would finish an item that starts with b, if the slice + carried it: a tag's content, a float's or simple value's following + bytes, the end of an empty indefinite item.""" + mt, ai = b >> 5, b & 31 + if mt == 6: + return bytes([0x00]) + if mt == 7: + return bytes({24: 1, 25: 2, 26: 4, 27: 8}.get(ai, 0)) + if ai == 31: + return bytes([0xff]) + return b"" + + +# ---------- Cross-check against cbor2, when it can be imported ---------- +# cbor2 (https://github.com/agronholm/cbor2) is a CBOR library for +# Python written apart from this project, and the oracle the plan in +# issue #1 named. CI installs nothing beyond Python's standard library, +# so the record's oracle is the reference codec above, and this +# cross-check runs only where cbor2 can be imported. Its inputs are +# counted apart, not in Inputs, so a run with or without cbor2 records +# the same Inputs. A disagreement is a failure. + +CBOR2_PIN = "6.1.5" + + +class OutsideSlice(Exception): + pass + + +def cbor2_text(o): + """The tool's canonical text for a value cbor2 returned, or + OutsideSlice when the value is of a kind the slice does not carry + (a float, a tag cbor2 kept or turned into another type, undefined, + another simple value, or an integer outside -2^64 to 2^64 - 1).""" + from collections.abc import Mapping + if o is False: + return "false" + if o is True: + return "true" + if o is None: + return "null" + if type(o) is int: + if -2**64 <= o < 2**64: + return str(o) + raise OutsideSlice + if type(o) is bytes: + return "h'" + o.hex() + "'" + if type(o) is str: + return "t'" + o.encode("utf-8").hex() + "'" + if type(o) in (list, tuple): + return "[" + ",".join(cbor2_text(x) for x in o) + "]" + if isinstance(o, Mapping): + return "{" + ",".join(cbor2_text(k) + ":" + cbor2_text(v) + for k, v in o.items()) + "}" + raise OutsideSlice + + +def cbor2_cross_check(drv): + """Has cbor2 judge the tool's answers. Returns (None, reason) when + cbor2 cannot be imported or lacks the option the judge needs, else + (cbor2's version and the counts, None). + + cbor2 accepts an input when `cbor2.loads` reads it, every value in + it is of a kind the slice carries, and `cbor2.dumps` writes the + same bytes back. That last step turns away what cbor2 reads but the + slice does not: arguments not in preferred form, indefinite + lengths, tags that come back as plain values, and bytes after the + item. The tool's `d` answer must be the canonical text of cbor2's + value, or `error`; for each input cbor2 accepts, the `r` answer must + be the input. An input is left out when cbor2 reads it, writes other + bytes back, and a map in it holds two keys that are equal as Python + values (the same key twice, or 1 and true, or 0 and false): cbor2 + keeps one pair of those, and the slice keeps every pair.""" + try: + import cbor2 + from importlib.metadata import version + ver = version("cbor2") + except Exception: + return None, "cbor2 could not be imported" + try: + cbor2.loads(b"\xa0", allow_duplicate_keys=False) + except TypeError: + return None, f"cbor2 {ver} has no allow_duplicate_keys option" + + def judge(bs): + try: + o = cbor2.loads(bs) + except Exception: + return "error" + try: + text = cbor2_text(o) + except OutsideSlice: + return "error" + if cbor2.dumps(o) == bs: + return text + try: + cbor2.loads(bs, allow_duplicate_keys=False) + except Exception: + return None # keys equal as Python values: left out + return "error" + + rng = random.Random(SEED) + + def rand_value(depth): + kind = rng.randrange(9 if depth < 3 else 6) + if kind == 0: + return rng.choice([0, 1, 23, 24, 255, 256, 65535, 65536, 2**32 - 1, + 2**32, 2**64 - 1, rng.randrange(2**64)]) + if kind == 1: + return -1 - rng.choice([0, 23, 24, 255, 256, 65535, 2**32, + 2**64 - 1, rng.randrange(2**64)]) + if kind == 2: + return bytes(rng.randrange(256) + for _ in range(rng.choice([0, 1, 5, 23, 24, 30, 256]))) + if kind == 3: + chars = [] + for _ in range(rng.randrange(0, 12)): + lo, hi = rng.choice(UTF8_ROW_SCALARS) + chars.append(chr(rng.randrange(lo, hi + 1))) + return "".join(chars) + if kind == 4: + return rng.choice([False, True, None]) + if kind == 5: + return rng.randrange(-1000, 1000) + if kind in (6, 7): + return [rand_value(depth + 1) + for _ in range(rng.choice([0, 1, 2, 3, 24, 25]))] + keys = [rng.choice([rng.randrange(2**32), rng.randrange(-30, 30), + str(rng.randrange(100)), bytes([rng.randrange(256)]), + False, True, None, + tuple(rng.randrange(5) for _ in range(rng.randrange(3)))]) + for _ in range(rng.randrange(0, 5))] + return {k: rand_value(depth + 1) for k in keys} + + def mutate(e): + m = bytearray(e) + op = rng.randrange(5) + if op == 0 and m: + m[rng.randrange(len(m))] = rng.randrange(256) + elif op == 1: + m.insert(rng.randrange(len(m) + 1), rng.randrange(256)) + elif op == 2 and m: + del m[rng.randrange(len(m))] + elif op == 3 and m: + m[rng.randrange(len(m))] ^= 1 << rng.randrange(8) + elif m: + del m[rng.randrange(len(m)):] + return bytes(m) + + parts = [] + parts.append(("All inputs of 0, 1 or 2 bytes", + [bytes(t) for n in range(3) + for t in itertools.product(range(256), repeat=n)])) + parts.append(("RFC 8949 Appendix A, all 81 rows", + [bytes.fromhex(h) for h, _ in RFC_OK] + + [bytes.fromhex(h) for h in RFC_A_OUT])) + parts.append(("Random bytes, 3 to 9 long", + [bytes(rng.randrange(256) for _ in range(rng.randrange(3, 10))) + for _ in range(30000)])) + parts.append(("Text items with 1 to 4 payload bytes, each random or " + "from 80 to bf", + [bytes([0x60 + k]) + bytes(rng.choice([rng.randrange(256), + rng.randrange(0x80, 0xC0)]) + for _ in range(k)) + for k in (rng.randrange(1, 5) for _ in range(10000))])) + written = [] + for _ in range(5000): + e = cbor2.dumps(rand_value(0)) + written.append(e) + written += [mutate(e) for _ in range(3)] + parts.append(("Random values written by cbor2.dumps, and 3 mutations " + "of each", written)) + + rows = [] + totals = {"requests": 0, "accepted": 0, "refused": 0, "left out": 0} + failures_before = len(failures) + for name, items in parts: + reqs, wants, labels = [], [], [] + acc = ref = left = 0 + for bs in items: + want = judge(bs) + if want is None: + left += 1 + continue + reqs.append(("d", bs.hex())) + wants.append(want) + labels.append(f"cbor2 d {bs.hex()}") + if want == "error": + ref += 1 + else: + acc += 1 + reqs.append(("r", bs.hex())) + wants.append(bs.hex()) + labels.append(f"cbor2 r {bs.hex()}") + got = drv.ask_many(reqs) + for label, want, answer in zip(labels, wants, got): + check(label, answer == want, f"cbor2 says {want}, the tool {answer}") + rows.append((name, len(reqs), acc, ref, left)) + totals["requests"] += len(reqs) + totals["accepted"] += acc + totals["refused"] += ref + totals["left out"] += left + totals["disagreements"] = len(failures) - failures_before + return {"version": ver, "rows": rows, "totals": totals}, None + + +def main(): + global accepted, rejected, section + drv = LeanDriver() + + section = "RFC 8949 Appendix A rows and other out-of-slice shapes" + # 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_A_OUT + OTHER_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) + + def rand_scalar(): + """A Unicode scalar value from a random row of RFC 3629's + grammar (Unicode Table 3-7), often at a row's first or last + code point.""" + lo, hi = rng.choice(UTF8_ROW_SCALARS) + return rng.choice([lo, hi, rng.randrange(lo, hi + 1)]) + + # 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 = [rand_scalar() for _ in range(n)] + 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,) + + section = "Generated well-formed items and their truncations" + 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 + + section = "Random bytes" + # 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 + + section = "Non-preferred arguments and preferred controls" + # Non-preferred arguments, at every boundary of the argument table + # (RFC 8949 section 4.2.1) and at random values below it, for each + # major type 0 to 5: turned away. Strings, arrays and maps carry a + # full body, so only the argument's form is wrong. The same value in + # its preferred form is accepted, as a control. + def body(mt, n): + if mt < 2: + return b"" + return {2: b"\x00", 3: b"a", 4: b"\x00", 5: b"\x00\x00"}[mt] * n + limits = {24: 24, 25: 2**8, 26: 2**16, 27: 2**32} + widths = {24: 1, 25: 2, 26: 4, 27: 8} + for mt in [0, 1, 2, 3, 4, 5]: + for ai in [24, 25, 26, 27]: + lim = limits[ai] + values = sorted(v for v in {0, 1, 23, lim // 256 - 1, lim // 256, + lim - 1, rng.randrange(lim)} + if 0 <= v < lim) + for x in values: + if mt >= 2 and x > 300: + continue + np = bytes([(mt << 5) | ai]) + x.to_bytes(widths[ai], "big") + item = np + body(mt, x) + check(f"nonpref mt{mt} ai{ai} {x}", + drv.ask("d", item.hex()) == "error", item.hex()) + rejected += 1 + pref = ref_head(mt, x) + body(mt, x) + want = ref_full(list(pref)) + check(f"pref mt{mt} {x}", want is not None + and drv.ask("d", pref.hex()) == want, pref.hex()) + accepted += 1 + + section = "Out-of-slice initial bytes, at the top and nested" + # Every initial byte outside the slice, with the bytes that would + # finish its item, at the top and nested: as an array's first or + # later item, as a map's key or value, and two and three levels + # down. Turned away, by the Lean code and by the oracle. + def nestings(it): + return [it, b"\x81" + it, b"\x82\x01" + it, b"\xa1" + it + b"\x00", + b"\xa1\x01" + it, b"\x81\x81" + it, b"\xa1\x01\x81\xa1\x00" + it] + for b in range(256): + if not out_of_slice(b): + continue + for k, enc in enumerate(nestings(bytes([b]) + completion(b))): + want = ref_full(list(enc)) + check(f"nested out {b:02x} {k}", want is None + and drv.ask("d", enc.hex()) == "error", enc.hex()) + rejected += 1 + + section = "Malformed UTF-8 examples" + # 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 + + section = "UTF-8 grammar rows" + # Each row of the UTF-8 grammar: byte sequences built from the row's + # ranges, with some bytes moved just outside their range, alone or + # between other characters. The oracle is Python's strict UTF-8 + # decoder, which follows RFC 3629. + for row_i, row in enumerate(UTF8_ROW_BYTES): + for i in range(150): + seq = [] + for lo, hi in row: + seq.append(rng.choice([lo, hi, rng.randrange(lo, hi + 1), + rng.randrange(lo, hi + 1), + max(lo - 1, 0), min(hi + 1, 255), + rng.randrange(256)])) + if i % 3 == 1: + seq = seq[:rng.randrange(len(seq) + 1)] + if i % 3 == 2: + seq = (list(chr(rand_scalar()).encode("utf-8")) + seq + + list(chr(rand_scalar()).encode("utf-8"))) + p = bytes(seq) + enc = ref_head(3, len(p)) + p + want = ref_full(list(enc)) + got = drv.ask("d", enc.hex()) + check(f"utf8 row {row_i} {i}", got == (want or "error"), + f"{enc.hex()}: want {want or 'error'}, got {got}") + if want is None: + rejected += 1 + else: + accepted += 1 + + section = "Trailing bytes and empty input" + # Leftover bytes after a complete item: turned away. + check("trailing", drv.ask("d", "0102") == "error") + check("empty", drv.ask("d", "") == "error") + + cross, why_not = cbor2_cross_check(drv) + # Written in every run, so the record always says how to install cbor2. + install_text = textwrap.fill( + f"To run the cross-check, install cbor2 {CBOR2_PIN}, the version the " + "committed record used, where the script can import it. For " + "example:", 72) + f""" + + python3 -m venv /tmp/cbor2-venv + /tmp/cbor2-venv/bin/pip install cbor2=={CBOR2_PIN} + /tmp/cbor2-venv/bin/python tests/run_tests.py +""" + if cross is None: + oracle_note = f"; the cbor2 cross-check did not run ({why_not})" + cross_text = textwrap.fill( + f"In this run {why_not}, so the cross-check did not run.", 72) + cross_text += "\n\n" + install_text + else: + oracle_note = f"; cross-checked against cbor2 {cross['version']}, counted apart" + t = cross["totals"] + part_lines = "\n".join( + f" - {name}: {n} requests; cbor2 accepted {acc} inputs, " + f"refused {ref}" + (f", left out {left}" if left else "") + for name, n, acc, ref, left in cross["rows"]) + version_note = ("" if cross["version"] == CBOR2_PIN else + f" This is not cbor2 {CBOR2_PIN}, the version the " + "committed record used.") + cross_text = textwrap.fill( + f"In this run cbor2 {cross['version']} could be imported, and the " + f"cross-check ran.{version_note} The requests by part, where " + "each input cbor2 accepts is asked twice, `d` and `r`:", 72) + cross_text += "\n\n" + part_lines + "\n\n" + textwrap.fill( + f"In all: {t['requests']} requests, from {t['accepted']} inputs " + f"cbor2 accepted and {t['refused']} it refused, with " + f"{t['disagreements']} disagreements. {t['left out']} inputs were " + "left out because a map in them holds two keys that are equal " + "as Python values.", 72) + "\n\n" + install_text + + # The build is part of the check: lake build already ran if needed. + total = checks + ok = total - len(failures) + breakdown = "\n".join(f" - {name}: {n}" for name, n in per_section.items()) + failed = "".join(f"\n - {f}" for f in failures) + RESULTS.write_text(f"""# Test results + +Written by `python3 tests/run_tests.py`, which feeds each input to the +command-line tool built from the proved code (`.lake/build/bin/cbor`) +and compares its answer with the oracle's. + +- Oracle: reference codec in `tests/run_tests.py`, on Python {sys.version.split()[0]}{oracle_note} +- Seed: {SEED} +- Inputs: {inputs} +- Failures: {len(failures)}{failed} + +The oracle is a decoder and encoder of the slice written from RFC 8949 +apart from the Lean code, in the test script itself. It checks text +payloads with Python's strict UTF-8 decoder, which follows RFC 3629. + +Inputs by section: + +{breakdown} + +The RFC 8949 Appendix A section runs all 81 rows: the 37 in the slice +are decoded and encoded again, and the 44 outside it (bignums, floats, +`undefined` and other simple values, tags, indefinite-length items) are +turned away, in both directions. None is skipped. It also runs 17 other +shapes outside the slice: simple(24), more tags and indefinite items, +break on its own, and reserved additional information. + +Each input is one request to the tool: `d` (decode) or `r` (decode and +encode again). This script does not check proofs or axioms; `lake +comparator --paranoid` does. + +## Cross-check against cbor2 + +The plan in issue #1 named Python cbor2 as the oracle. The record's +oracle is the reference codec above instead, so that CI, which installs +nothing beyond Python's standard library, reruns the same inputs and +gets the same numbers. The reference codec is written apart from the +Lean code, but by the same project. So where cbor2, a CBOR library +written apart from this project, can be imported, the script also has +cbor2 judge the tool's answers. Those requests are counted apart, not +in Inputs, so a run with or without cbor2 records the same Inputs. A +disagreement is a failure, listed under Failures above. + +cbor2 accepts an input when `cbor2.loads` reads it, every value in it +is of a kind the slice carries (false, true, null, an integer from +-2^64 to 2^64 - 1, a byte or text string, an array, a map), and +`cbor2.dumps` writes the same bytes back. That last step turns away +what cbor2 reads but the slice does not: arguments not in preferred +form, indefinite lengths, tags that come back as plain values, and +bytes after the item. The tool's `d` answer must be the canonical text +of cbor2's value, or `error` when cbor2 does not accept; for an input +cbor2 accepts, the `r` answer must be the input. An input is left out +when cbor2 reads it, writes other bytes back, and a map in it holds +two keys that are equal as Python values (the same key twice, or 1 and +true, or 0 and false): cbor2 keeps one pair of those, and the slice +keeps every pair, since it applies no duplicate-key rule. + +{cross_text}""") + print(f"{ok}/{total} checks passed; results written to {RESULTS}") + return 1 if failures else 0 + + +if __name__ == "__main__": + sys.exit(main())