CBOR codec: #2 carried forward with the review fixes (bar v2)

.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

.gitignore

@@ -0,0 +1 @@
+.lake/

Cbor.lean

@@ -0,0 +1,5 @@
+/-
+  CBOR (RFC 8949), definite length items: the code under proof.
+-/
+import Cbor.Utf8
+import Cbor.Basic

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

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

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 <hex>    Decode the bytes. Prints the item in canonical form, or
+               `error` for anything the decoder turns away.
+    r <hex>    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

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