From e6fbd9e3bf36d777efe4a8634135ce5257b9bdc0 Mon Sep 17 00:00:00 2001 From: shah Date: Mon, 26 Oct 2026 21:53:48 -0500 Subject: [PATCH 1/3] Add JWS compact parser and claims checker, with proved round trip --- .gitignore | 1 + Json.lean | 2 + Json/Parse.lean | 264 ++++++++++ Json/Value.lean | 124 +++++ Jws.lean | 3 + Jws/Base64url.lean | 79 +++ Jws/Token.lean | 290 +++++++++++ Jws/Utf8.lean | 79 +++ Main.lean | 127 +++++ Proofs.lean | 4 + Proofs/B64.lean | 211 ++++++++ Proofs/RoundTrip.lean | 1104 +++++++++++++++++++++++++++++++++++++++++ Proofs/Token.lean | 114 +++++ Proofs/Utf8.lean | 135 +++++ README.md | 78 ++- SPEC.md | 178 +++++++ lake-manifest.json | 6 + lakefile.toml | 16 + lean-toolchain | 1 + tests/TEST-RESULTS.md | 47 ++ tests/run_tests.py | 918 ++++++++++++++++++++++++++++++++++ 21 files changed, 3756 insertions(+), 25 deletions(-) create mode 100644 Json.lean create mode 100644 Json/Parse.lean create mode 100644 Json/Value.lean create mode 100644 Jws.lean create mode 100644 Jws/Base64url.lean create mode 100644 Jws/Token.lean create mode 100644 Jws/Utf8.lean create mode 100644 Main.lean create mode 100644 Proofs.lean create mode 100644 Proofs/B64.lean create mode 100644 Proofs/RoundTrip.lean create mode 100644 Proofs/Token.lean create mode 100644 Proofs/Utf8.lean create mode 100644 SPEC.md create mode 100644 lake-manifest.json create mode 100644 lakefile.toml create mode 100644 lean-toolchain create mode 100644 tests/TEST-RESULTS.md create mode 100644 tests/run_tests.py diff --git a/.gitignore b/.gitignore index 01f8cdb..da49d2d 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,2 @@ .lake/ +venv/ diff --git a/Json.lean b/Json.lean new file mode 100644 index 0000000..c060478 --- /dev/null +++ b/Json.lean @@ -0,0 +1,2 @@ +import Json.Value +import Json.Parse diff --git a/Json/Parse.lean b/Json/Parse.lean new file mode 100644 index 0000000..d01ce14 --- /dev/null +++ b/Json/Parse.lean @@ -0,0 +1,264 @@ +/- + The JSON parser. It reads a list of characters and returns a value + and the characters that follow it, or `none` when the text up to + that point sits outside the grammar of RFC 8259. + + Rules the parser follows: + + - Whitespace is space, tab, line feed, and carriage return, and + nothing else. It may sit before a value, after a value, and + around the marks inside an array or an object. + - A control character inside a string must be escaped. The escapes + are the ones RFC 8259 lists, plus `\uXXXX`. + - A `\uXXXX` escape in the high surrogate range must be followed + by a second `\uXXXX` escape in the low surrogate range, and the + pair is read as one character. A lone surrogate escape is + rejected, because Lean `Char` cannot hold a surrogate half. + - A number is read by the grammar of RFC 8259 and held as its + source text. + + `parseValue`, `parseEls`, and `parseObjEls` take a fuel count. + Each step into an array or an object spends one unit, so the + functions are total on hostile input: a text that nests deeper + than its own length is rejected, never looped on. The top level + `parse` passes one more than the length of the text, which is + always enough for a text the grammar accepts. +-/ + +import Json.Value + +namespace Json + +/-- Whitespace in JSON: space, tab, line feed, carriage return. -/ +def isWs (c : Char) : Bool := + c == ' ' || c == '\t' || c == '\n' || c == '\r' + +/-- Drop the whitespace at the head of the text. -/ +def skipWs : List Char → List Char + | [] => [] + | c :: cs => if isWs c then skipWs cs else c :: cs + +/-- A digit, as a test. -/ +def isDigit (c : Char) : Bool := + decide ('0' ≤ c ∧ c ≤ '9') + +/-- The value of one hex digit, in either case. -/ +def hexVal (c : Char) : Option Nat := + if '0' ≤ c ∧ c ≤ '9' then some (c.toNat - 48) + else if 'a' ≤ c ∧ c ≤ 'f' then some (c.toNat - 87) + else if 'A' ≤ c ∧ c ≤ 'F' then some (c.toNat - 55) + else none + +/-- The character a one letter escape stands for. -/ +def simpleEscape (c : Char) : Option Char := + if c = '"' then some '"' + else if c = '\\' then some '\\' + else if c = '/' then some '/' + else if c = 'b' then some (Char.ofNat 8) + else if c = 'f' then some (Char.ofNat 12) + else if c = 'n' then some (Char.ofNat 10) + else if c = 'r' then some (Char.ofNat 13) + else if c = 't' then some (Char.ofNat 9) + else none + +/-- Read a string body, up to the closing quote. The opening quote is + already consumed. Returns the characters read and the text after + the closing quote. -/ +def parseStrBody : List Char → Option (List Char × List Char) + | [] => none + | c :: rest => + if c = '"' then some ([], rest) + else if c = '\\' then + match rest with + | [] => none + | e :: rest1 => + if e = 'u' then + match rest1 with + | a :: b :: cc :: d :: rest2 => + match hexVal a, hexVal b, hexVal cc, hexVal d with + | some w, some x, some y, some z => + let n := w * 4096 + x * 256 + y * 16 + z + if n < 0xD800 then + (parseStrBody rest2).map fun (cs, r) => (Char.ofNat n :: cs, r) + else if n < 0xDC00 then + match rest2 with + | '\\' :: 'u' :: a2 :: b2 :: c2 :: d2 :: rest3 => + match hexVal a2, hexVal b2, hexVal c2, hexVal d2 with + | some w2, some x2, some y2, some z2 => + let m := w2 * 4096 + x2 * 256 + y2 * 16 + z2 + if 0xDC00 ≤ m ∧ m < 0xE000 then + (parseStrBody rest3).map fun (cs, r) => + (Char.ofNat (0x10000 + (n - 0xD800) * 0x400 + (m - 0xDC00)) :: cs, r) + else none + | _, _, _, _ => none + | _ => none + else if n < 0xE000 then none + else + (parseStrBody rest2).map fun (cs, r) => (Char.ofNat n :: cs, r) + | _, _, _, _ => none + | _ => none + else + match simpleEscape e with + | some ch => (parseStrBody rest1).map fun (cs, r) => (ch :: cs, r) + | none => none + else if c.toNat < 0x20 then none + else (parseStrBody rest).map fun (cs, r) => (c :: cs, r) + +/-- The longest run of digits at the head of the text, and the text + after it. -/ +def takeDigits : List Char → List Char × List Char + | [] => ([], []) + | c :: rest => + if isDigit c then + let (ds, r) := takeDigits rest + (c :: ds, r) + else ([], c :: rest) + +/-- The integer part of a number: a single zero, or a non-zero digit + and the digits after it. -/ +def parseIntPart (cs : List Char) : Option (List Char × List Char) := + match cs with + | [] => none + | c :: rest => + if c = '0' then some (['0'], rest) + else if '1' ≤ c ∧ c ≤ '9' then + let (ds, r) := takeDigits rest + some (c :: ds, r) + else none + +/-- The fraction part of a number when one is there: a point and one + or more digits. When the next character is not a point, the part + is empty. -/ +def parseFracOpt (cs : List Char) : Option (List Char × List Char) := + if cs.head? = some '.' then + match takeDigits cs.tail with + | (d :: ds, r) => some ('.' :: d :: ds, r) + | _ => none + else some ([], cs) + +/-- The exponent part of a number when one is there: `e` or `E`, an + optional sign, and one or more digits. When the next character is + not one of the two letters, the part is empty. -/ +def parseExpOpt (cs : List Char) : Option (List Char × List Char) := + match cs with + | e :: rest => + if e = 'e' ∨ e = 'E' then + let (sgn, rest1) : List Char × List Char := + if rest.head? = some '+' then (['+'], rest.tail) + else if rest.head? = some '-' then (['-'], rest.tail) + else ([], rest) + match takeDigits rest1 with + | (d :: ds, r) => some (e :: (sgn ++ d :: ds), r) + | _ => none + else some ([], cs) + | [] => some ([], []) + +/-- Read a number at the head of the text. Returns the number text + and the text after it. The grammar is the one in RFC 8259: an + optional minus, an integer part, a fraction part, an exponent + part. -/ +def parseNumber (cs : List Char) : Option (List Char × List Char) := + let (sgn, rest) : List Char × List Char := + if cs.head? = some '-' then (['-'], cs.tail) else ([], cs) + match parseIntPart rest with + | none => none + | some (i, r1) => + match parseFracOpt r1 with + | none => none + | some (f, r2) => + match parseExpOpt r2 with + | none => none + | some (e, r3) => some (sgn ++ i ++ f ++ e, r3) + +mutual +/-- Read one value at the head of the text, after any whitespace. + The fuel count bounds how deep arrays and objects may nest. -/ +def parseValue : Nat → List Char → Option (Json × List Char) + | 0, _ => none + | fuel + 1, cs => + match skipWs cs with + | [] => none + | c :: rest => + if c = '"' then + (parseStrBody rest).map fun (s, r) => (Json.str s, r) + else if c = '[' then + (parseEls fuel rest).map fun (vs, r) => (Json.arr vs, r) + else if c = '{' then + (parseObjEls fuel rest).map fun (kvs, r) => (Json.obj kvs, r) + else if c = 't' then + match rest with + | 'r' :: 'u' :: 'e' :: r => some (Json.bool true, r) + | _ => none + else if c = 'f' then + match rest with + | 'a' :: 'l' :: 's' :: 'e' :: r => some (Json.bool false, r) + | _ => none + else if c = 'n' then + match rest with + | 'u' :: 'l' :: 'l' :: r => some (Json.null, r) + | _ => none + else if c = '-' ∨ isDigit c then + (parseNumber (c :: rest)).map fun (n, r) => (Json.num n, r) + else none + +/-- Read the inside of an array, after the opening bracket: values + split by commas, then the closing bracket. -/ +def parseEls : Nat → List Char → Option (List Json × List Char) + | 0, _ => none + | fuel + 1, cs => + match skipWs cs with + | [] => none + | c :: rest => + if c = ']' then some ([], rest) + else + match parseValue fuel (c :: rest) with + | none => none + | some (v, r) => + match skipWs r with + | ']' :: r2 => some ([v], r2) + | ',' :: r2 => + match skipWs r2 with + | ']' :: _ => none + | [] => none + | _ => + (parseEls fuel r2).map fun (vs, r3) => (v :: vs, r3) + | _ => none + +/-- Read the inside of an object, after the opening brace: key and + value pairs split by commas, then the closing brace. -/ +def parseObjEls : Nat → List Char → Option (List (List Char × Json) × List Char) + | 0, _ => none + | fuel + 1, cs => + match skipWs cs with + | [] => none + | c :: rest => + if c = '}' then some ([], rest) + else if c = '"' then + match parseStrBody rest with + | none => none + | some (k, r1) => + match skipWs r1 with + | ':' :: r2 => + match parseValue fuel r2 with + | none => none + | some (v, r3) => + match skipWs r3 with + | '}' :: r4 => some ([(k, v)], r4) + | ',' :: r4 => + match skipWs r4 with + | '"' :: _ => + (parseObjEls fuel r4).map fun (kvs, r5) => ((k, v) :: kvs, r5) + | _ => none + | _ => none + | _ => none + else none +end + +/-- Parse a whole text: one value, with whitespace allowed around it + and nothing after it. -/ +def parse (cs : List Char) : Option Json := + match parseValue (cs.length + 1) cs with + | some (v, rest) => if skipWs rest = [] then some v else none + | none => none + +end Json diff --git a/Json/Value.lean b/Json/Value.lean new file mode 100644 index 0000000..01711c0 --- /dev/null +++ b/Json/Value.lean @@ -0,0 +1,124 @@ +/- + The JSON value type, the canonical printer, and the well formed + predicate that the round trip proof in `Proofs` uses. + + A number is held as its source text. The printer writes that text + back word for word, and no claim is made about the numeric value. + The parser in `Json.Parse` checks the text against the number + grammar of RFC 8259 before it builds a `num` value. + + A string is held as a list of characters. Lean `Char` is a Unicode + scalar value, so a string here can never hold a lone surrogate half. + + An object is held as a list of key and value pairs, in the order + written. Duplicate keys are kept as written. +-/ + +namespace Json + +/-- A JSON value. Numbers and strings and object keys are held as + lists of characters. -/ +inductive Json where + | null + | bool (b : Bool) + | num (cs : List Char) + | str (cs : List Char) + | arr (vs : List Json) + | obj (kvs : List (List Char × Json)) + +/-- The sixteen hex digits, lowercase. -/ +def hexDigits : List Char := + ['0', '1', '2', '3', '4', '5', '6', '7', '8', '9', 'a', 'b', 'c', 'd', 'e', 'f'] + +/-- The hex digit for a value below 16. -/ +def hexDigit (n : Nat) : Char := + hexDigits.getD n '0' + +/-- The printed form of one character inside a string. The quote and + the backslash take a backslash before them. The five control + characters that have a short form in RFC 8259 use it. Any other + character below U+0020 is written as `\u00XX`. Every other + character is written as it is. -/ +def escape (c : Char) : List Char := + if c = '"' then ['\\', '"'] + else if c = '\\' then ['\\', '\\'] + else if c.toNat = 8 then ['\\', 'b'] + else if c.toNat = 9 then ['\\', 't'] + else if c.toNat = 10 then ['\\', 'n'] + else if c.toNat = 12 then ['\\', 'f'] + else if c.toNat = 13 then ['\\', 'r'] + else if c.toNat < 32 then + ['\\', 'u', '0', '0', hexDigit (c.toNat / 16), hexDigit (c.toNat % 16)] + else [c] + +/-- The printed form of a whole string body, without the quotes. -/ +def escapeAll (cs : List Char) : List Char := + cs.flatMap escape + +/-- A string in its printed form, with quotes. -/ +def printStr (cs : List Char) : List Char := + '"' :: (escapeAll cs ++ ['"']) + +/-- Join printed parts with a comma between each two. -/ +def join : List (List Char) → List Char + | [] => [] + | [x] => x + | x :: y :: rest => x ++ ',' :: join (y :: rest) + +mutual +/-- The canonical printed form of a value: no spaces anywhere, + object pairs in the order held, numbers as their source text. -/ +def print : Json → List Char + | .null => ['n', 'u', 'l', 'l'] + | .bool true => ['t', 'r', 'u', 'e'] + | .bool false => ['f', 'a', 'l', 's', 'e'] + | .num cs => cs + | .str cs => printStr cs + | .arr vs => '[' :: join (vs.map print) ++ [']'] + | .obj kvs => '{' :: join (kvs.map printPair) ++ ['}'] + +/-- One object pair in its printed form. -/ +def printPair : List Char × Json → List Char + | (k, v) => printStr k ++ ':' :: print v +end + +/-- A digit, as a proposition. -/ +def IsDigit (c : Char) : Prop := + '0' ≤ c ∧ c ≤ '9' + +/-- The fraction part of a number text, as RFC 8259 allows it: either + absent, or a point and one or more digits. -/ +def FracOk (f : List Char) : Prop := + f = [] ∨ ∃ d ds, f = '.' :: d :: ds ∧ IsDigit d ∧ ∀ x ∈ ds, IsDigit x + +/-- The exponent part of a number text: either absent, or `e` or `E`, + an optional sign, and one or more digits. -/ +def ExpOk (e : List Char) : Prop := + e = [] ∨ ∃ (ec : Char) (sgn : List Char) (d : Char) (ds : List Char), + e = ec :: (sgn ++ d :: ds) ∧ (ec = 'e' ∨ ec = 'E') ∧ + (sgn = [] ∨ sgn = ['-'] ∨ sgn = ['+']) ∧ + IsDigit d ∧ ∀ x ∈ ds, IsDigit x + +/-- A number text that follows the grammar of RFC 8259: an optional + minus, then either a single zero or a non-zero digit and more + digits, then a fraction part and an exponent part. Stated as a + split of the text into its parts. -/ +def WFNum (cs : List Char) : Prop := + ∃ (neg : Bool) (hd : Char) (intDs frac exp : List Char), + cs = (if neg then ['-'] else []) ++ (hd :: intDs) ++ frac ++ exp ∧ + ((hd = '0' ∧ intDs = []) ∨ ('1' ≤ hd ∧ hd ≤ '9')) ∧ + (∀ d ∈ intDs, IsDigit d) ∧ FracOk frac ∧ ExpOk exp + +/-- A value whose number texts all follow the grammar. Strings, + object keys, and the shape of arrays and objects need no further + condition: every such value prints in a form the parser reads + back. -/ +inductive WF : Json → Prop + | null : WF .null + | bool (b : Bool) : WF (.bool b) + | num {cs : List Char} : WFNum cs → WF (.num cs) + | str (cs : List Char) : WF (.str cs) + | arr {vs : List Json} : (∀ v ∈ vs, WF v) → WF (.arr vs) + | obj {kvs : List (List Char × Json)} : (∀ kv ∈ kvs, WF kv.2) → WF (.obj kvs) + +end Json diff --git a/Jws.lean b/Jws.lean new file mode 100644 index 0000000..671a5fd --- /dev/null +++ b/Jws.lean @@ -0,0 +1,3 @@ +import Jws.Base64url +import Jws.Utf8 +import Jws.Token diff --git a/Jws/Base64url.lean b/Jws/Base64url.lean new file mode 100644 index 0000000..e6f5226 --- /dev/null +++ b/Jws/Base64url.lean @@ -0,0 +1,79 @@ +/- + Base64url, as RFC 4648 section 5 defines it and RFC 7515 uses it: + the URL and filename safe alphabet, with no padding. + + The shape follows the Base64 code in the codec repo: three bytes + at a time into four characters on the way out, four characters at + a time into three bytes on the way back. The differences are the + last two alphabet characters (`-` and `_`) and the missing + padding: a final byte is carried by two characters, two final + bytes by three, and no `=` is ever written or read. + + `decode` is strict. It turns away: any character outside the + alphabet (`=` among them, since padding is not part of the + compact form), a length that is 1 mod 4, and a last character + whose unused bits are not zero. +-/ + +namespace Jws.Base64url + +/-- The character for a value below 64: the alphabet in order, + capitals (values 0 to 25), small letters (26 to 51), digits + (52 to 61), then `-` (62) and `_` (63). -/ +def char (n : Nat) : Char := + if n < 26 then Char.ofNat (n + 65) + else if n < 52 then Char.ofNat (n + 71) + else if n < 62 then Char.ofNat (n - 4) + else if n = 62 then '-' + else '_' + +/-- Encode bytes, three at a time into four characters, with a + short last group and no padding. -/ +def encode : List UInt8 → List Char + | a :: b :: c :: rest => + let n := a.toNat * 65536 + b.toNat * 256 + c.toNat + char (n / 262144) :: char (n / 4096 % 64) :: char (n / 64 % 64) :: char (n % 64) :: + encode rest + | [a, b] => + let n := a.toNat * 65536 + b.toNat * 256 + [char (n / 262144), char (n / 4096 % 64), char (n / 64 % 64)] + | [a] => + let n := a.toNat * 65536 + [char (n / 262144), char (n / 4096 % 64)] + | [] => [] + +/-- The value of one character of the alphabet. -/ +def value (c : Char) : Option Nat := + if 'A' ≤ c ∧ c ≤ 'Z' then some (c.toNat - 65) + else if 'a' ≤ c ∧ c ≤ 'z' then some (c.toNat - 71) + else if '0' ≤ c ∧ c ≤ '9' then some (c.toNat + 4) + else if c = '-' then some 62 + else if c = '_' then some 63 + else none + +/-- Decode, four characters at a time into three bytes. A short + last group of two or three characters gives one or two bytes, + and its unused bits must be zero. -/ +def decode : List Char → Option (List UInt8) + | [] => some [] + | [c0, c1] => + match value c0, value c1 with + | some v0, some v1 => + if v1 % 16 = 0 then some [(v0 * 4 + v1 / 16).toUInt8] else none + | _, _ => none + | [c0, c1, c2] => + match value c0, value c1, value c2 with + | some v0, some v1, some v2 => + if v2 % 4 = 0 then + some [(v0 * 4 + v1 / 16).toUInt8, (v1 % 16 * 16 + v2 / 4).toUInt8] + else none + | _, _, _ => none + | c0 :: c1 :: c2 :: c3 :: rest => + match value c0, value c1, value c2, value c3, decode rest with + | some v0, some v1, some v2, some v3, some tail => + some ((v0 * 4 + v1 / 16).toUInt8 :: (v1 % 16 * 16 + v2 / 4).toUInt8 :: + (v2 % 4 * 64 + v3).toUInt8 :: tail) + | _, _, _, _, _ => none + | _ => none + +end Jws.Base64url diff --git a/Jws/Token.lean b/Jws/Token.lean new file mode 100644 index 0000000..9a222cc --- /dev/null +++ b/Jws/Token.lean @@ -0,0 +1,290 @@ +import Json +import Jws.Base64url +import Jws.Utf8 + +/- + The JWS compact form (RFC 7515 section 5.2): three base64url + parts joined by dots. Part one is the header, a JSON object. + Part two is the payload, the claims set, also a JSON object. + Part three is the signature bytes. + + This slice parses the compact form and runs the plan's checks: + the algorithm against a caller allowlist, the required claims, + and the exp, nbf, iss, and aud claims against a context the + caller supplies. It does not verify the signature; a token that + passes these checks is not thereby verified. Signature + verification belongs to the second slice. + + The JSON code is the json repo's, carried in unchanged (the + repos in this org do not import each other): `Json.parse` reads + a text, `Json.print` writes a value in the canonical form, and + the round trip between them is proved there for well formed + values. +-/ + +namespace Jws + +open Json + +/-- Split a text at every copy of a separator character. The + parts never contain the separator. Splitting also serves the + comma separated name lists of the command line front end. -/ +def splitSep (sep : Char) : List Char → List (List Char) + | [] => [[]] + | c :: rest => + if c = sep then [] :: splitSep sep rest + else + match splitSep sep rest with + | p :: ps => (c :: p) :: ps + | [] => [[c]] + +/-- Join parts with a separator character between them. -/ +def joinSep (sep : Char) : List (List Char) → List Char + | [] => [] + | [p] => p + | p :: q :: ps => p ++ sep :: joinSep sep (q :: ps) + +/-- A parsed token: the header value, the claims value, and the + signature bytes, returned unchanged. -/ +structure Token where + header : Json + claims : Json + sig : List UInt8 + +/-- Print a token: each JSON part in the canonical printer's + form, UTF-8 bytes, base64url without padding, the parts + joined by dots, the signature last. -/ +def printToken (t : Token) : List Char := + joinSep '.' [Base64url.encode (Utf8.encode (Json.print t.header)), + Base64url.encode (Utf8.encode (Json.print t.claims)), + Base64url.encode t.sig] + +/-- Parse the compact form. Framing first: exactly three parts. + Each part must decode as strict base64url, the first two must + then decode as UTF-8 and parse as JSON. Object shape and the + claim rules are the checker's work, not the parser's. -/ +def parseToken (cs : List Char) : Option Token := + match splitSep '.' cs with + | [h, p, s] => + match Base64url.decode h, Base64url.decode p, Base64url.decode s with + | some hb, some pb, some sb => + match Utf8.decode hb, Utf8.decode pb with + | some hc, some pc => + match Json.parse hc, Json.parse pc with + | some hv, some pv => some ⟨hv, pv, sb⟩ + | _, _ => none + | _, _ => none + | _, _, _ => none + | _ => none + +/-- An exact decimal number value, read from a JSON number text: + the value is (if neg then -1 else 1) times sig times ten to + the exp. The form is normalized: zero is (false, 0, 0), and + any other sig does not end in zero. -/ +structure NumVal where + neg : Bool + sig : Nat + exp : Int +deriving DecidableEq + +/-- The value of a run of digit characters. -/ +def digitsVal (ds : List Char) : Nat := + ds.foldl (fun a c => a * 10 + (c.toNat - 48)) 0 + +/-- Divide factors of ten out of a significand, raising the + exponent to match. The fuel is the significand itself, which + is always more steps than stripping can take. -/ +def strip (neg : Bool) : Nat → Nat → Int → NumVal + | 0, s, e => ⟨neg, s, e⟩ + | fuel + 1, s, e => + if s % 10 = 0 ∧ s ≠ 0 then strip neg fuel (s / 10) (e + 1) + else ⟨neg, s, e⟩ + +/-- Build a normalized number value. -/ +def mkNumVal (neg : Bool) (sig : Nat) (exp : Int) : NumVal := + if sig = 0 then ⟨false, 0, 0⟩ else strip neg sig sig exp + +/-- Read a JSON number text as an exact decimal value. The text + is one the JSON parser accepted, so its shape is the number + grammar; anything else is turned away by returning none. -/ +def numVal (cs : List Char) : Option NumVal := + let (neg, r0) := match cs with + | '-' :: r => (true, r) + | _ => (false, cs) + let (ids, r1) := r0.span (·.isDigit) + if ids.isEmpty then none + else + match r1 with + | '.' :: r => + let (fds, r2) := r.span (·.isDigit) + if fds.isEmpty then none + else finish neg ids fds r2 + | _ => finish neg ids [] r1 +where + finish (neg : Bool) (ids fds : List Char) (r : List Char) : Option NumVal := + match r with + | [] => some (mkNumVal neg (digitsVal (ids ++ fds)) (-(fds.length : Int))) + | 'e' :: t => withExp neg ids fds t + | 'E' :: t => withExp neg ids fds t + | _ => none + withExp (neg : Bool) (ids fds : List Char) (r : List Char) : Option NumVal := + let (sgn, r1) := match r with + | '-' :: t => ((-1 : Int), t) + | '+' :: t => ((1 : Int), t) + | _ => ((1 : Int), r) + let (eds, r2) := r1.span (·.isDigit) + if eds.isEmpty ∨ ¬ r2.isEmpty then none + else + some (mkNumVal neg (digitsVal (ids ++ fds)) + (sgn * (digitsVal eds : Int) - (fds.length : Int))) + +/-- Whether a number value is a whole number of seconds. -/ +def NumVal.isInt (v : NumVal) : Bool := + v.sig = 0 || 0 ≤ v.exp + +/-- A whole number as a number value. -/ +def NumVal.ofInt (n : Int) : NumVal := + mkNumVal (n < 0) n.natAbs 0 + +/-- The count of digits a number is written with. -/ +def numDigits (n : Nat) : Nat := + if n < 10 then 1 else 1 + numDigits (n / 10) +termination_by n +decreasing_by omega + +/-- Compare the magnitudes of two nonzero number values. The + decimal point position decides first. On a tie the + significands are aligned by padding the shorter one with + zeros, and the padding counts are digit counts, so a wild + exponent never turns into a wild power of ten. -/ +def magCmp (a b : NumVal) : Ordering := + let da := (numDigits a.sig : Int) + a.exp + let db := (numDigits b.sig : Int) + b.exp + if da < db then .lt + else if da > db then .gt + else + let dsa := numDigits a.sig + let dsb := numDigits b.sig + if dsb ≤ dsa then compare a.sig (b.sig * 10 ^ (dsa - dsb)) + else compare (a.sig * 10 ^ (dsb - dsa)) b.sig + +/-- Compare two number values exactly. -/ +def NumVal.cmp (a b : NumVal) : Ordering := + let sa : Int := if a.sig = 0 then 0 else if a.neg then -1 else 1 + let sb : Int := if b.sig = 0 then 0 else if b.neg then -1 else 1 + if sa < sb then .lt + else if sa > sb then .gt + else if sa = 0 then .eq + else if sa = 1 then magCmp a b + else magCmp b a + +/-- Look a name up in the members of a JSON object. When a name + appears more than once, the first copy is the one found, as + in the JSON code. Anything that is not an object has no + members. -/ +def lookup (name : List Char) (j : Json) : Option Json := + match j with + | .obj kvs => kvs.lookup name + | _ => none + +/-- The state of one date claim (exp, nbf, iat) in a claims set: + absent, present but not a whole number of seconds (a + non-number, or a number with a fraction), or present with a + whole number value. -/ +inductive ClaimDate where + | absent + | bad + | ok (v : NumVal) + +def dateClaim (name : List Char) (claims : Json) : ClaimDate := + match lookup name claims with + | none => .absent + | some (.num cs) => + match numVal cs with + | some v => if v.isInt then .ok v else .bad + | none => .bad + | some _ => .bad + +/-- The check context a caller supplies: the algorithms allowed, + the current time in seconds (none means the time comparisons + are skipped; the type rules still hold), the claims that must + be present, the expected issuer if any, the expected audience + if any. -/ +structure Context where + allow : List (List Char) + now : Option Int + required : List (List Char) + issuer : Option (List Char) + audience : Option (List Char) + +/-- When iss is present it must be a string. -/ +def issShapeOk (claims : Json) : Bool := + match lookup "iss".toList claims with + | none => true + | some (.str _) => true + | some _ => false + +/-- When aud is present it must be a string or an array of + strings. -/ +def audShapeOk (claims : Json) : Bool := + match lookup "aud".toList claims with + | none => true + | some (.str _) => true + | some (.arr vs) => vs.all fun v => match v with + | .str _ => true + | _ => false + | some _ => false + +/-- The audience check itself: aud is the expected string, or an + array holding it. A missing aud fails. -/ +def audOk (claims : Json) (a : List Char) : Bool := + match lookup "aud".toList claims with + | some (.str s) => s == a + | some (.arr vs) => vs.any fun v => match v with + | .str s => s == a + | _ => false + | _ => false + +/-- Run the checks. Every rule must hold; SPEC.md states them one + by one. This checks the token's shape and claims only. It + does not verify the signature, and a true answer here is not + a verified token. -/ +def accept (t : Token) (ctx : Context) : Bool := + if ctx.allow.contains "none".toList then false + else + match t.header, t.claims with + | .obj _, .obj _ => + match lookup "alg".toList t.header with + | some (.str alg) => + alg != "none".toList && + ctx.allow.contains alg && + ctx.required.all (fun n => (lookup n t.claims).isSome) && + (match dateClaim "exp".toList t.claims with + | .bad => false + | .absent => true + | .ok v => match ctx.now with + | none => true + | some n => NumVal.cmp (NumVal.ofInt n) v == .lt) && + (match dateClaim "nbf".toList t.claims with + | .bad => false + | .absent => true + | .ok v => match ctx.now with + | none => true + | some n => NumVal.cmp (NumVal.ofInt n) v != .lt) && + (match dateClaim "iat".toList t.claims with + | .bad => false + | _ => true) && + issShapeOk t.claims && + audShapeOk t.claims && + (match ctx.issuer with + | none => true + | some i => match lookup "iss".toList t.claims with + | some (.str s) => s == i + | _ => false) && + (match ctx.audience with + | none => true + | some a => audOk t.claims a) + | _ => false + | _, _ => false + +end Jws diff --git a/Jws/Utf8.lean b/Jws/Utf8.lean new file mode 100644 index 0000000..06223a4 --- /dev/null +++ b/Jws/Utf8.lean @@ -0,0 +1,79 @@ +/- + UTF-8, by hand: the byte form of JSON text is UTF-8 (RFC 7515 + says BASE64URL(UTF8(text))), and the JSON values this project + carries hold their strings as lists of characters, so the token + code needs both directions between characters and bytes. + + The encoder writes the standard one to four bytes per character. + The decoder is strict. It turns away stray continuation bytes, + overlong forms (a character written with more bytes than it + needs, including any lead byte below C2), lead bytes above F4, + encodings of the surrogate values D800 to DFFF, values above + 10FFFF, and truncated sequences. +-/ + +namespace Jws.Utf8 + +/-- The bytes of one character. -/ +def encodeChar (c : Char) : List UInt8 := + let n := c.toNat + if n < 0x80 then [n.toUInt8] + else if n < 0x800 then + [(0xC0 + n / 64).toUInt8, (0x80 + n % 64).toUInt8] + else if n < 0x10000 then + [(0xE0 + n / 4096).toUInt8, (0x80 + (n / 64) % 64).toUInt8, (0x80 + n % 64).toUInt8] + else + [(0xF0 + n / 262144).toUInt8, (0x80 + (n / 4096) % 64).toUInt8, + (0x80 + (n / 64) % 64).toUInt8, (0x80 + n % 64).toUInt8] + +/-- The bytes of a text. -/ +def encode (cs : List Char) : List UInt8 := + cs.flatMap encodeChar + +/-- The payload bits of a continuation byte (80 to BF). -/ +def contVal (b : UInt8) : Option Nat := + if 0x80 ≤ b.toNat ∧ b.toNat < 0xC0 then some (b.toNat - 0x80) else none + +/-- Strict decoding. The side conditions on the three and four + byte forms are the overlong, surrogate, and range rules: after + E0 the first continuation value is at least 32, after ED it is + below 32, after F0 it is at least 16, after F4 it is below 16. -/ +def decode : List UInt8 → Option (List Char) + | [] => some [] + | b :: rest => + if b.toNat < 0x80 then + (decode rest).map fun cs => Char.ofNat b.toNat :: cs + else if b.toNat < 0xC2 then none + else if b.toNat < 0xE0 then + match rest with + | b1 :: rest1 => + match contVal b1 with + | some v1 => (decode rest1).map fun cs => + Char.ofNat ((b.toNat - 0xC0) * 64 + v1) :: cs + | none => none + | [] => none + else if b.toNat < 0xF0 then + match rest with + | b1 :: b2 :: rest1 => + match contVal b1, contVal b2 with + | some v1, some v2 => + if (b.toNat = 0xE0 → 0x20 ≤ v1) ∧ (b.toNat = 0xED → v1 < 0x20) then + (decode rest1).map fun cs => + Char.ofNat ((b.toNat - 0xE0) * 4096 + v1 * 64 + v2) :: cs + else none + | _, _ => none + | _ => none + else if b.toNat < 0xF5 then + match rest with + | b1 :: b2 :: b3 :: rest1 => + match contVal b1, contVal b2, contVal b3 with + | some v1, some v2, some v3 => + if (b.toNat = 0xF0 → 0x10 ≤ v1) ∧ (b.toNat = 0xF4 → v1 < 0x10) then + (decode rest1).map fun cs => + Char.ofNat ((b.toNat - 0xF0) * 262144 + v1 * 4096 + v2 * 64 + v3) :: cs + else none + | _, _, _ => none + | _ => none + else none + +end Jws.Utf8 diff --git a/Main.lean b/Main.lean new file mode 100644 index 0000000..09da9f2 --- /dev/null +++ b/Main.lean @@ -0,0 +1,127 @@ +import Jws + +/- + Command line front end. The shape follows the other slices in + this org: one request per line on stdin, one answer per line + on stdout. A request is a word, a space, and a payload. The + payload is decimal character codes separated by commas. + + One operation: + + check the payload carries six fields separated by + semicolons (code 59). Each field is text written as + character codes, as above. Field 1: the token text. + Field 2: the current time as decimal digits, or empty + for no time comparisons. Field 3: the allowed + algorithms, names separated by commas inside the + field text. Field 4: the required claims, same style. + Field 5: the expected issuer, or empty. Field 6: the + expected audience, or empty. + + The answer is `ok:` and the codes of the canonical reprinted + token when the token is accepted, `none` when it is not, and + `error` when the request itself is malformed. + + Full statement of the format and the rules: SPEC.md. +-/ + +/-- One decimal number, at most seven digits, the way the house + writes a character code. -/ +def number (s : String) : Option Nat := + if s.isEmpty ∨ ¬ s.all (·.isDigit) then none + else + let n := s.foldl (fun a c => a * 10 + (c.toNat - 48)) 0 + if n < 10000000 then some n else none + +/-- The comma separated numbers of a payload or a field. -/ +def numbers (s : String) : Option (List Nat) := + if s.isEmpty then some [] + else (s.splitOn ",").mapM number + +/-- Numbers into characters, asking each number to be a scalar + value: below the surrogate gap or above it, within range. -/ +def toChars (ns : List Nat) : Option (List Char) := + ns.mapM fun n => + if n < 0xD800 ∨ (0xE000 ≤ n ∧ n ≤ 0x10FFFF) then some (Char.ofNat n) + else none + +/-- Characters back into the comma separated answer codes. -/ +def showCodes (cs : List Char) : String := + ",".intercalate (cs.map fun c => toString c.toNat) + +/-- Remove one trailing newline and carriage return. -/ +def chomp (line : String) : String := + let cs := line.toList + if cs.getLast? = some '\n' then + let cs := cs.dropLast + String.ofList (if cs.getLast? = some '\r' then cs.dropLast else cs) + else line + +/-- Split a field text into names at its commas. An empty field + names nothing. -/ +def names (cs : List Char) : List (List Char) := + if cs.isEmpty then [] else Jws.splitSep ',' cs + +/-- Read the current time field: empty for no time comparisons, + else an optional minus sign and at most 19 digits. -/ +def readNow (cs : List Char) : Option (Option Int) := + match cs with + | [] => some none + | _ => + let (neg, ds) := match cs with + | '-' :: r => (true, r) + | _ => (false, cs) + if ds.isEmpty ∨ ds.length > 19 ∨ ¬ ds.all (·.isDigit) then none + else + let n : Nat := ds.foldl (fun a c => a * 10 + (c.toNat - 48)) 0 + some (some (if neg then -(n : Int) else (n : Int))) + +/-- Answer one `check` request: the codes of the six fields. -/ +def answerCheck (fields : List (List Nat)) : Option String := + match fields with + | [tf, nf, af, rf, isf, auf] => + match toChars tf, toChars nf, toChars af, toChars rf, toChars isf, toChars auf with + | some t, some nowCs, some allowCs, some reqCs, some issCs, some audCs => + match readNow nowCs with + | none => none + | some now => + let ctx : Jws.Context := + { allow := names allowCs + now := now + required := names reqCs + issuer := if issCs.isEmpty then none else some issCs + audience := if audCs.isEmpty then none else some audCs } + match Jws.parseToken t with + | none => some "none" + | some tok => + some (if Jws.accept tok ctx then "ok:" ++ showCodes (Jws.printToken tok) + else "none") + | _, _, _, _, _, _ => none + | _ => none + +/-- Answer one request line. -/ +def answer (line : String) : String := + let line := chomp line + if line.isEmpty then "error" + else + match line.splitOn " " with + | [op, arg] => + if op = "check" then + match (arg.splitOn ";").mapM numbers with + | some fields => + match answerCheck fields with + | some out => out + | none => "error" + | none => "error" + else "error" + | _ => "error" + +partial def loop : IO Unit := do + let stdin ← IO.getStdin + match ← stdin.getLine with + | "" => return + | line => + IO.println (answer line) + loop + +def main : IO Unit := loop diff --git a/Proofs.lean b/Proofs.lean new file mode 100644 index 0000000..8a82bf6 --- /dev/null +++ b/Proofs.lean @@ -0,0 +1,4 @@ +import Proofs.RoundTrip +import Proofs.B64 +import Proofs.Utf8 +import Proofs.Token diff --git a/Proofs/B64.lean b/Proofs/B64.lean new file mode 100644 index 0000000..3aeaecb --- /dev/null +++ b/Proofs/B64.lean @@ -0,0 +1,211 @@ +import Jws.Base64url + +open Jws.Base64url + +namespace Jws.Base64url.Proofs + +theorem charLe (a c : Char) : a ≤ c ↔ a.toNat ≤ c.toNat := by + simp [Char.le_def, UInt32.le_iff_toNat_le] + +set_option maxRecDepth 10000 in +/-- The finite table check, delegated to the kernel: every value + below 64 reads back through the alphabet. -/ +theorem value_tbl : ∀ n : Fin 64, value (char n.val) = some n.val := by + decide +kernel + +theorem value_char {n : Nat} (h : n < 64) : value (char n) = some n := + value_tbl ⟨n, h⟩ + +/-- The dot that joins the parts is never a character of the + encoding. The token round trip proof needs this. -/ +theorem char_ne_dot {n : Nat} (h : n < 64) : char n ≠ '.' := by + intro e + have hv : value '.' = none := by decide + have hvc := value_char h + rw [e, hv] at hvc + cases hvc + +set_option maxRecDepth 10000 in +theorem upper_tbl : ∀ k : Fin 26, (char k.val).toNat = k.val + 65 := by decide +kernel +set_option maxRecDepth 10000 in +theorem lower_tbl : ∀ k : Fin 26, (char (k.val + 26)).toNat = k.val + 97 := by decide +kernel +set_option maxRecDepth 10000 in +theorem digit_tbl : ∀ k : Fin 10, (char (k.val + 52)).toNat = k.val + 48 := by decide +kernel +theorem char_62 : char 62 = '-' := by decide +kernel +theorem char_63 : char 63 = '_' := by decide +kernel + +/-- Anything the decoder accepts is a character the encoder + writes, with the same value. -/ +theorem value_some {c : Char} {v : Nat} (h : value c = some v) : + v < 64 ∧ char v = c := by + unfold value at h + simp only [charLe] at h + have hA : 'A'.toNat = 65 := rfl + have hZ : 'Z'.toNat = 90 := rfl + have ha : 'a'.toNat = 97 := rfl + have hz : 'z'.toNat = 122 := rfl + have h0 : '0'.toNat = 48 := rfl + have h9 : '9'.toNat = 57 := rfl + rw [hA, hZ, ha, hz, h0, h9] at h + split at h + · rename_i hc + cases h + refine ⟨by omega, ?_⟩ + apply Char.toNat_inj.mp + have htb := upper_tbl ⟨c.toNat - 65, by omega⟩ + simp only at htb + rw [htb]; omega + split at h + · rename_i _ hc + cases h + refine ⟨by omega, ?_⟩ + apply Char.toNat_inj.mp + have htb := lower_tbl ⟨c.toNat - 97, by omega⟩ + simp only at htb + have e : c.toNat - 97 + 26 = c.toNat - 71 := by omega + rw [e] at htb + rw [htb]; omega + split at h + · rename_i _ _ hc + cases h + refine ⟨by omega, ?_⟩ + apply Char.toNat_inj.mp + have htb := digit_tbl ⟨c.toNat - 48, by omega⟩ + simp only at htb + have e : c.toNat - 48 + 52 = c.toNat + 4 := by omega + rw [e] at htb + rw [htb]; omega + split at h + · rename_i hc + cases h; subst hc; exact ⟨by omega, char_62⟩ + split at h + · rename_i hc + cases h; subst hc; exact ⟨by omega, char_63⟩ + · cases h + +theorem toNat_toUInt8 {k : Nat} (h : k < 256) : k.toUInt8.toNat = k := by + simp; omega + +/-- Decoding the encoding of any bytes gives the bytes back. -/ +theorem decode_encode : ∀ bs : List UInt8, decode (encode bs) = some bs := by + intro bs + induction bs using encode.induct with + | case1 a b c rest ih => + have ha := UInt8.toNat_lt a + have hb := UInt8.toNat_lt b + have hc := UInt8.toNat_lt c + rw [encode.eq_1, decode.eq_4, value_char (by omega), value_char (by omega), + value_char (by omega), value_char (by omega), ih] + simp only [Option.some.injEq, List.cons.injEq, and_true] + refine ⟨?_, ?_, ?_⟩ <;> apply UInt8.toNat_inj.mp <;> + rw [toNat_toUInt8 (by omega)] <;> omega + | case2 a b => + have ha := UInt8.toNat_lt a + have hb := UInt8.toNat_lt b + rw [encode.eq_2, decode.eq_3, value_char (by omega), value_char (by omega), + value_char (by omega)] + simp only + rw [ite_eq_left (by omega)] + simp only [Option.some.injEq, List.cons.injEq, and_true] + refine ⟨?_, ?_⟩ <;> apply UInt8.toNat_inj.mp <;> + rw [toNat_toUInt8 (by omega)] <;> omega + | case3 a => + have ha := UInt8.toNat_lt a + rw [encode.eq_3, decode.eq_2, value_char (by omega), value_char (by omega)] + simp only + rw [ite_eq_left (by omega)] + simp only [Option.some.injEq, List.cons.injEq, and_true] + apply UInt8.toNat_inj.mp; rw [toNat_toUInt8 (by omega)]; omega + | case4 => rfl + +/-- Encoding the decoding of a text the decoder accepted gives + the text back. -/ +theorem encode_decode : ∀ (cs : List Char) (bs : List UInt8), + decode cs = some bs → encode bs = cs := by + intro cs bs + induction cs using decode.induct generalizing bs with + | case1 => + intro h + rw [decode.eq_1, Option.some.injEq] at h + subst h; rfl + | case2 c0 c1 v0 v1 h1 h0 hm => + intro h + rw [decode.eq_2, h0, h1] at h + simp only [ite_eq_left hm, Option.some.injEq] at h + subst h + obtain ⟨lt0, ch0⟩ := value_some h0 + obtain ⟨lt1, ch1⟩ := value_some h1 + rw [encode.eq_3, toNat_toUInt8 (by omega)] + have e1 : (v0 * 4 + v1 / 16) * 65536 / 262144 = v0 := by omega + have e2 : (v0 * 4 + v1 / 16) * 65536 / 4096 % 64 = v1 := by omega + rw [e1, e2, ch0, ch1] + | case3 c0 c1 v0 v1 h1 h0 hm => + intro h + rw [decode.eq_2, h0, h1] at h + simp only [ite_eq_right hm] at h + cases h + | case4 c0 c1 hn => + intro h + rw [decode.eq_2] at h + split at h + · exact (hn _ _ ‹_› ‹_›).elim + · cases h + | case5 c0 c1 c2 v0 v1 v2 h2 h1 h0 hm => + intro h + rw [decode.eq_3, h0, h1, h2] at h + simp only [ite_eq_left hm, Option.some.injEq] at h + subst h + obtain ⟨lt0, ch0⟩ := value_some h0 + obtain ⟨lt1, ch1⟩ := value_some h1 + obtain ⟨lt2, ch2⟩ := value_some h2 + rw [encode.eq_2, toNat_toUInt8 (by omega), toNat_toUInt8 (by omega)] + have e1 : ((v0 * 4 + v1 / 16) * 65536 + (v1 % 16 * 16 + v2 / 4) * 256) / 262144 = + v0 := by omega + have e2 : ((v0 * 4 + v1 / 16) * 65536 + (v1 % 16 * 16 + v2 / 4) * 256) / 4096 % 64 = + v1 := by omega + have e3 : ((v0 * 4 + v1 / 16) * 65536 + (v1 % 16 * 16 + v2 / 4) * 256) / 64 % 64 = + v2 := by omega + rw [e1, e2, e3, ch0, ch1, ch2] + | case6 c0 c1 c2 v0 v1 v2 h2 h1 h0 hm => + intro h + rw [decode.eq_3, h0, h1, h2] at h + simp only [ite_eq_right hm] at h + cases h + | case7 c0 c1 c2 hn => + intro h + rw [decode.eq_3] at h + split at h + · exact (hn _ _ _ ‹_› ‹_› ‹_›).elim + · cases h + | case8 c0 c1 c2 c3 rest v0 v1 v2 v3 tail hrec h3 h2 h1 h0 ih => + intro h + rw [decode.eq_4, h0, h1, h2, h3, hrec] at h + simp only [Option.some.injEq] at h + subst h + obtain ⟨lt0, ch0⟩ := value_some h0 + obtain ⟨lt1, ch1⟩ := value_some h1 + obtain ⟨lt2, ch2⟩ := value_some h2 + obtain ⟨lt3, ch3⟩ := value_some h3 + rw [encode.eq_1, toNat_toUInt8 (by omega), toNat_toUInt8 (by omega), + toNat_toUInt8 (by omega), ih tail hrec] + have e1 : ((v0 * 4 + v1 / 16) * 65536 + (v1 % 16 * 16 + v2 / 4) * 256 + + (v2 % 4 * 64 + v3)) / 262144 = v0 := by omega + have e2 : ((v0 * 4 + v1 / 16) * 65536 + (v1 % 16 * 16 + v2 / 4) * 256 + + (v2 % 4 * 64 + v3)) / 4096 % 64 = v1 := by omega + have e3 : ((v0 * 4 + v1 / 16) * 65536 + (v1 % 16 * 16 + v2 / 4) * 256 + + (v2 % 4 * 64 + v3)) / 64 % 64 = v2 := by omega + have e4 : ((v0 * 4 + v1 / 16) * 65536 + (v1 % 16 * 16 + v2 / 4) * 256 + + (v2 % 4 * 64 + v3)) % 64 = v3 := by omega + rw [e1, e2, e3, e4, ch0, ch1, ch2, ch3] + | case9 c0 c1 c2 c3 rest hn ih => + intro h + rw [decode.eq_4] at h + split at h + · exact (hn _ _ _ _ _ ‹_› ‹_› ‹_› ‹_› ‹_›).elim + · cases h + | case10 t h0 h1 h2 h3 => + intro h + rw [decode.eq_5 _ h0 h1 h2 h3] at h + cases h + +end Jws.Base64url.Proofs diff --git a/Proofs/RoundTrip.lean b/Proofs/RoundTrip.lean new file mode 100644 index 0000000..a7682d8 --- /dev/null +++ b/Proofs/RoundTrip.lean @@ -0,0 +1,1104 @@ +/- + The round trip proof: for every well formed value, parsing its + printed form gives the value back. + + The statement proved here is `parse_print`. A matching statement + in a spec file still has to be added by a reviewer, so this file + builds on its own, in the same shape as the codec proofs. + + Helper lemmas live in `Json.Proofs`. The main step is `key`, a + strong induction on the length of the printed form that proves + three statements together: one for a value, one for the inside of + an array, and one for the inside of an object. The array and + object statements spend the value statement at the same bound, + and the value statement spends them at a smaller bound, because + the brackets around a body add two characters to its length. +-/ + +import Json + +namespace Json.Proofs + +open Json + +set_option maxRecDepth 10000 + +/-- What may follow a printed number inside a printed array or + object, or at the end of a text: the next character, if there + is one, is not a digit, a point, or an exponent letter, so the + number parser stops at the end of the number. -/ +def TailOk (rest : List Char) : Prop := + ∀ c, rest.head? = some c → + isDigit c = false ∧ c ≠ '.' ∧ c ≠ 'e' ∧ c ≠ 'E' + +theorem tailOk_nil : TailOk [] := by + intro c h + simp at h + +theorem tailOk_comma (rest : List Char) : TailOk (',' :: rest) := by + intro c h + simp at h + subst h + exact ⟨by decide, by decide, by decide, by decide⟩ + +theorem tailOk_rbracket (rest : List Char) : TailOk (']' :: rest) := by + intro c h + simp at h + subst h + exact ⟨by decide, by decide, by decide, by decide⟩ + +theorem tailOk_rbrace (rest : List Char) : TailOk ('}' :: rest) := by + intro c h + simp at h + subst h + exact ⟨by decide, by decide, by decide, by decide⟩ + +theorem char_le_toNat {a b : Char} (h : a ≤ b) : a.toNat ≤ b.toNat := by + rw [Char.le_def, UInt32.le_iff_toNat_le] at h + exact h + +theorem char_le_of_toNat {a b : Char} (h : a.toNat ≤ b.toNat) : a ≤ b := by + rw [Char.le_def, UInt32.le_iff_toNat_le] + exact h + +/-- The digit range of a character, in code points. -/ +theorem isDigit_range {c : Char} (h : IsDigit c) : 48 ≤ c.toNat ∧ c.toNat ≤ 57 := by + have h1 : ('0' : Char).toNat ≤ c.toNat := by + have := h.1 + rwa [Char.le_def] at this + have h2 : c.toNat ≤ ('9' : Char).toNat := by + have := h.2 + rwa [Char.le_def] at this + exact ⟨by simpa using h1, by simpa using h2⟩ + +/-- A character the grammar treats as a digit passes the digit + test. -/ +theorem isDigit_of_isDigit {c : Char} (h : IsDigit c) : isDigit c = true := by + show decide ('0' ≤ c ∧ c ≤ '9') = true + rw [decide_eq_true_eq] + exact h + +/-- A character that passes the digit test is a digit. -/ +theorem isDigit_of_test {c : Char} (h : isDigit c = true) : IsDigit c := by + have h2 : decide ('0' ≤ c ∧ c ≤ '9') = true := h + rwa [decide_eq_true_eq] at h2 + +/-- A digit differs from each character with a code point outside + the digit range. -/ +theorem IsDigit.ne_of_toNat {c d : Char} (h : IsDigit c) + (hd : d.toNat < 48 ∨ 57 < d.toNat) : c ≠ d := by + intro e + have h1 := isDigit_range h + have h2 : c.toNat = d.toNat := by rw [e] + omega + +/-- Whitespace fails on a character that is none of the four + whitespace characters. -/ +theorem isWs_of_ne {c : Char} (h1 : c ≠ ' ') (h2 : c ≠ '\t') + (h3 : c ≠ '\n') (h4 : c ≠ '\r') : isWs c = false := by + simp [isWs, h1, h2, h3, h4] + +/-- A digit is not whitespace, and is not one of the marks that can + follow or extend a number. -/ +theorem IsDigit.isWs_false {c : Char} (h : IsDigit c) : isWs c = false := + isWs_of_ne + (IsDigit.ne_of_toNat h (by decide)) + (IsDigit.ne_of_toNat h (by decide)) + (IsDigit.ne_of_toNat h (by decide)) + (IsDigit.ne_of_toNat h (by decide)) + +theorem IsDigit.ne_rbracket {c : Char} (h : IsDigit c) : c ≠ ']' := + IsDigit.ne_of_toNat h (by decide) + +theorem IsDigit.ne_rbrace {c : Char} (h : IsDigit c) : c ≠ '}' := + IsDigit.ne_of_toNat h (by decide) + +theorem IsDigit.ne_comma {c : Char} (h : IsDigit c) : c ≠ ',' := + IsDigit.ne_of_toNat h (by decide) + +/-- The hex digit for a value below 16 reads back as that value. -/ +theorem hexVal_hexDigit : ∀ n : Fin 16, hexVal (hexDigit n.val) = some n.val := by + decide + +theorem hexVal_of_hexDigit {n : Nat} (h : n < 16) : hexVal (hexDigit n) = some n := + hexVal_hexDigit ⟨n, h⟩ + +/-- Skipping whitespace over a list whose head is not whitespace + changes nothing. -/ +theorem skipWs_cons {c : Char} {cs : List Char} (h : isWs c = false) : + skipWs (c :: cs) = c :: cs := by + simp [skipWs, h] + +/-- The same, for a list followed by more text. -/ +theorem skipWs_append_of_head {l rest : List Char} {c : Char} + (h : l.head? = some c) (hw : isWs c = false) : + skipWs (l ++ rest) = l ++ rest := by + cases l with + | nil => simp at h + | cons d l => + simp at h + subst h + simp [List.cons_append, skipWs_cons hw] + +/-- A run of digits at the head of a text is read whole: when the + text after the run does not start with a digit, the digit run + reader stops at the end of the run. -/ +theorem takeDigits_append {ds rest : List Char} + (hd : ∀ d ∈ ds, isDigit d = true) + (hr : ∀ c, rest.head? = some c → isDigit c = false) : + takeDigits (ds ++ rest) = (ds, rest) := by + induction ds generalizing rest with + | nil => + cases rest with + | nil => rfl + | cons c r => + have hc : isDigit c = false := hr c rfl + simp [takeDigits, hc] + | cons d ds ih => + have hdd : isDigit d = true := hd d (by simp) + have ih' := ih (fun x hx => hd x (List.mem_cons_of_mem d hx)) hr + simp [takeDigits, hdd, ih'] + +/-- The head of a text built from a fraction part, an exponent + part, and a tail is never a digit. -/ +theorem head_not_digit_of_parts {frac exp rest : List Char} + (hf : FracOk frac) (he : ExpOk exp) (ht : TailOk rest) : + ∀ c, (frac ++ exp ++ rest).head? = some c → isDigit c = false := by + obtain rfl | ⟨d, ds, hfr, hd, -⟩ := hf + · obtain rfl | ⟨ec, sgn, d, ds, hex, hec, -, -, -⟩ := he + · intro c hc + exact (ht c hc).1 + · intro c hc + have hthis : (exp ++ rest).head? = some ec := by + rw [hex] + cases sgn <;> simp + have h1 : (exp ++ rest).head? = some c := by simpa using hc + rw [hthis] at h1 + have hcc : ec = c := Option.some.inj h1 + subst hcc + cases hec with + | inl h => rw [h]; decide + | inr h => rw [h]; decide + · intro c hc + have h1 : (frac ++ exp ++ rest).head? = some '.' := by + rw [hfr]; simp + have hcc : c = '.' := by + rw [h1] at hc + exact (Option.some.inj hc).symm + subst hcc + decide + +/-- The head of a text built from an exponent part and a tail is + never a digit and never a point. -/ +theorem head_not_digit_or_dot_of_exp {exp rest : List Char} + (he : ExpOk exp) (ht : TailOk rest) : + ∀ c, (exp ++ rest).head? = some c → isDigit c = false ∧ c ≠ '.' := by + obtain rfl | ⟨ec, sgn, d, ds, hex, hec, -, -, -⟩ := he + · intro c hc + exact ⟨(ht c hc).1, (ht c hc).2.1⟩ + · intro c hc + have h1 : (exp ++ rest).head? = some ec := by + rw [hex] + cases sgn <;> simp + have h2 : (exp ++ rest).head? = some c := by simpa using hc + rw [h1] at h2 + have hcc : ec = c := Option.some.inj h2 + subst hcc + cases hec with + | inl h => rw [h]; exact ⟨by decide, by decide⟩ + | inr h => rw [h]; exact ⟨by decide, by decide⟩ + +/-- The integer part of a well formed number text is read whole. -/ +theorem parseIntPart_append {hd : Char} {intDs tail : List Char} + (h0 : (hd = '0' ∧ intDs = []) ∨ ('1' ≤ hd ∧ hd ≤ '9')) + (hds : ∀ d ∈ intDs, IsDigit d) + (ht : ∀ c, tail.head? = some c → isDigit c = false) : + parseIntPart ((hd :: intDs) ++ tail) = some (hd :: intDs, tail) := by + have hdig : ∀ d ∈ intDs, isDigit d = true := + fun d hd' => isDigit_of_isDigit (hds d hd') + cases h0 with + | inl h => + obtain ⟨rfl, rfl⟩ := h + simp [parseIntPart] + | inr h => + have hne : hd ≠ '0' := by + intro e + have h1 : ('1' : Char).val ≤ hd.val := h.1 + rw [e] at h1 + exact (by decide : ¬ ((49 : UInt32) ≤ (48 : UInt32))) h1 + have htk : takeDigits (intDs ++ tail) = (intDs, tail) := + takeDigits_append hdig ht + simp [parseIntPart, hne, h, htk] + +/-- The fraction part of a well formed number text is read whole. -/ +theorem parseFracOpt_append {frac tail : List Char} (hf : FracOk frac) + (ht : ∀ c, tail.head? = some c → isDigit c = false ∧ c ≠ '.') : + parseFracOpt (frac ++ tail) = some (frac, tail) := by + cases hf with + | inl h => + rw [h] + simp only [List.nil_append] + cases tail with + | nil => simp [parseFracOpt] + | cons c r => + have hc : c ≠ '.' := (ht c rfl).2 + simp [parseFracOpt, hc] + | inr h => + obtain ⟨d, ds, rfl, hd, hds⟩ := h + have hdig : ∀ x ∈ d :: ds, isDigit x = true := + fun x hx => isDigit_of_isDigit (by + cases hx with + | head => exact hd + | tail _ hx => exact hds x hx) + have ht' : ∀ c, tail.head? = some c → isDigit c = false := + fun c hc => (ht c hc).1 + have htk : takeDigits ((d :: ds) ++ tail) = (d :: ds, tail) := + takeDigits_append hdig ht' + simp only [List.cons_append] at htk + simp [parseFracOpt, htk] + +/-- The exponent part of a well formed number text is read + whole. -/ +theorem parseExpOpt_append {exp rest : List Char} (he : ExpOk exp) + (ht : TailOk rest) : + parseExpOpt (exp ++ rest) = some (exp, rest) := by + cases he with + | inl h => + rw [h] + simp only [List.nil_append] + cases rest with + | nil => rfl + | cons c r => + have hc := ht c rfl + have hne : ¬ (c = 'e' ∨ c = 'E') := by + intro hp + cases hp with + | inl h1 => exact hc.2.2.1 h1 + | inr h2 => exact hc.2.2.2 h2 + simp [parseExpOpt, hne] + | inr h => + obtain ⟨ec, sgn, d, ds, rfl, hec, hsgn, hd, hds⟩ := h + have hdig : ∀ x ∈ d :: ds, isDigit x = true := + fun x hx => isDigit_of_isDigit (by + cases hx with + | head => exact hd + | tail _ hx => exact hds x hx) + have ht' : ∀ c, rest.head? = some c → isDigit c = false := + fun c hc => (ht c hc).1 + have htk : takeDigits ((d :: ds) ++ rest) = (d :: ds, rest) := + takeDigits_append hdig ht' + simp only [List.cons_append] at htk + have hdp : d ≠ '+' := IsDigit.ne_of_toNat hd (by decide) + have hdm : d ≠ '-' := IsDigit.ne_of_toNat hd (by decide) + cases hsgn with + | inl h => + rw [h] + simp [parseExpOpt, hec, htk, hdp, hdm] + | inr h => + cases h with + | inl h => + rw [h] + simp [parseExpOpt, hec, htk, hdp, hdm] + | inr h => + rw [h] + simp [parseExpOpt, hec, htk, hdp, hdm] + +/-- A well formed number text at the head of a text is read whole, + when what follows cannot extend the number. -/ +theorem parseNumber_append {cs rest : List Char} (h : WFNum cs) + (ht : TailOk rest) : + parseNumber (cs ++ rest) = some (cs, rest) := by + obtain ⟨neg, hd, intDs, frac, exp, hcs, hhd, hds, hfrac, hexp⟩ := h + have ht1 : ∀ c, (frac ++ exp ++ rest).head? = some c → isDigit c = false := + head_not_digit_of_parts hfrac hexp ht + have ht2 : ∀ c, (exp ++ rest).head? = some c → isDigit c = false ∧ c ≠ '.' := + head_not_digit_or_dot_of_exp hexp ht + have hint : parseIntPart ((hd :: intDs) ++ (frac ++ exp ++ rest)) = + some (hd :: intDs, frac ++ exp ++ rest) := + parseIntPart_append hhd hds ht1 + have hfrac' : parseFracOpt (frac ++ (exp ++ rest)) = some (frac, exp ++ rest) := + parseFracOpt_append hfrac ht2 + have hexp' : parseExpOpt (exp ++ rest) = some (exp, rest) := + parseExpOpt_append hexp ht + have hshape : cs ++ rest = + (if neg then ['-'] else []) ++ ((hd :: intDs) ++ (frac ++ (exp ++ rest))) := by + rw [hcs] + simp [List.append_assoc] + rw [hshape] + have hint2 : parseIntPart (hd :: (intDs ++ (frac ++ (exp ++ rest)))) = + some (hd :: intDs, frac ++ exp ++ rest) := by + simpa only [List.cons_append, List.append_assoc] using hint + cases neg with + | true => + simp [parseNumber, hint2, hfrac', hexp', List.append_assoc, List.cons_append, hcs] + | false => + have hne : hd ≠ '-' := by + cases hhd with + | inl h => rw [h.1]; decide + | inr h => + have h01 : ('0' : Char).toNat ≤ ('1' : Char).toNat := by decide + have hdig : IsDigit hd := + ⟨char_le_of_toNat (Nat.le_trans h01 (char_le_toNat h.1)), h.2⟩ + exact IsDigit.ne_of_toNat hdig (by decide) + simp [parseNumber, hne, hint2, hfrac', hexp', List.append_assoc, List.cons_append, hcs] + +/-- The hex value of the character `0`. -/ +theorem hexVal_zero : hexVal '0' = some 0 := by decide + +/-- A list of length under four is not a list of four or more cells. + Used for the side condition of the parser's short-tail equation. -/ +theorem not_four_cons (xs : List Char) (n : Nat) (h : xs.length = n) (hn : n < 4) : + ∀ (a b cc d : Char) (r : List Char), xs ≠ a :: b :: cc :: d :: r := by + intro a b cc d r he + have hl := congrArg List.length he + simp only [List.length_cons] at hl + omega + +/-- One step of the string body reader at a closing quote. -/ +theorem parseStrBody_quote (T : List Char) : + parseStrBody ('"' :: T) = some ([], T) := by + cases T with + | nil => + rw [Json.parseStrBody.eq_2] + simp + | cons d T => + cases T with + | nil => + rw [Json.parseStrBody.eq_4 _ _ _ (not_four_cons [] 0 rfl (by decide))] + simp + | cons e T => + cases T with + | nil => + rw [Json.parseStrBody.eq_4 _ _ _ (not_four_cons [e] 1 rfl (by decide))] + simp + | cons f T => + cases T with + | nil => + rw [Json.parseStrBody.eq_4 _ _ _ (not_four_cons [e, f] 2 rfl (by decide))] + simp + | cons g T => + cases T with + | nil => + rw [Json.parseStrBody.eq_4 _ _ _ (not_four_cons [e, f, g] 3 rfl (by decide))] + simp + | cons h T => + rw [Json.parseStrBody.eq_3] + simp + +/-- One step of the string body reader at a raw character. -/ +theorem parseStrBody_raw {c : Char} (h1 : c ≠ '"') (h2 : c ≠ '\\') + (h3 : ¬ c.toNat < 32) (T : List Char) : + parseStrBody (c :: T) = (parseStrBody T).map (fun (cs, r) => (c :: cs, r)) := by + cases T with + | nil => + rw [Json.parseStrBody.eq_2] + simp [h1, h2, h3, Json.parseStrBody.eq_1] + | cons d T => + cases T with + | nil => + rw [Json.parseStrBody.eq_4 _ _ _ (not_four_cons [] 0 rfl (by decide))] + simp [h1, h2, h3] + | cons e T => + cases T with + | nil => + rw [Json.parseStrBody.eq_4 _ _ _ (not_four_cons [e] 1 rfl (by decide))] + simp [h1, h2, h3] + | cons f T => + cases T with + | nil => + rw [Json.parseStrBody.eq_4 _ _ _ (not_four_cons [e, f] 2 rfl (by decide))] + simp [h1, h2, h3] + | cons g T => + cases T with + | nil => + rw [Json.parseStrBody.eq_4 _ _ _ (not_four_cons [e, f, g] 3 rfl (by decide))] + simp [h1, h2, h3] + | cons h T => + rw [Json.parseStrBody.eq_3] + simp [h1, h2, h3] + +/-- One step of the string body reader at a one-letter escape. -/ +theorem parseStrBody_escape (e ch : Char) (hne : e ≠ 'u') (hse : simpleEscape e = some ch) + (T : List Char) : + parseStrBody ('\\' :: e :: T) = + (parseStrBody T).map (fun (cs, r) => (ch :: cs, r)) := by + cases T with + | nil => + rw [Json.parseStrBody.eq_4 _ _ _ (not_four_cons [] 0 rfl (by decide))] + simp [hne, hse] + | cons a T => + cases T with + | nil => + rw [Json.parseStrBody.eq_4 _ _ _ (not_four_cons [a] 1 rfl (by decide))] + simp [hne, hse] + | cons b T => + cases T with + | nil => + rw [Json.parseStrBody.eq_4 _ _ _ (not_four_cons [a, b] 2 rfl (by decide))] + simp [hne, hse] + | cons cc T => + cases T with + | nil => + rw [Json.parseStrBody.eq_4 _ _ _ (not_four_cons [a, b, cc] 3 rfl (by decide))] + simp [hne, hse] + | cons d T => + rw [Json.parseStrBody.eq_3] + simp [hne, hse] + +/-- One step of the string body reader at a `\uXXXX` escape whose + value is below the surrogate range. -/ +theorem parseStrBody_unicode {a b cc d : Char} {w x y z : Nat} + (ha : hexVal a = some w) (hb : hexVal b = some x) + (hc : hexVal cc = some y) (hd : hexVal d = some z) + (hsmall : w * 4096 + x * 256 + y * 16 + z < 55296) (T : List Char) : + parseStrBody ('\\' :: 'u' :: a :: b :: cc :: d :: T) = + (parseStrBody T).map + (fun (cs, r) => (Char.ofNat (w * 4096 + x * 256 + y * 16 + z) :: cs, r)) := by + rw [Json.parseStrBody.eq_3] + simp [ha, hb, hc, hd, hsmall] + +/-- Reading back an escaped string body gives the string back: + the escapes the printer writes are read as the characters + they stand for, and the closing quote ends the body. -/ +theorem parseStrBody_escapeAll (cs : List Char) (rest : List Char) : + parseStrBody (escapeAll cs ++ '"' :: rest) = some (cs, rest) := by + induction cs generalizing rest with + | nil => exact parseStrBody_quote rest + | cons c cs ih => + have hinput : escapeAll (c :: cs) ++ '"' :: rest = + escape c ++ (escapeAll cs ++ '"' :: rest) := by + simp [escapeAll, List.append_assoc] + rw [hinput] + by_cases h1 : c = '"' + · subst h1 + show parseStrBody ('\\' :: '"' :: (escapeAll cs ++ '"' :: rest)) = + some ('"' :: cs, rest) + rw [parseStrBody_escape '"' '"' (by decide) (by decide) _] + simp [ih] + · by_cases h2 : c = '\\' + · subst h2 + show parseStrBody ('\\' :: '\\' :: (escapeAll cs ++ '"' :: rest)) = + some ('\\' :: cs, rest) + rw [parseStrBody_escape '\\' '\\' (by decide) (by decide) _] + simp [ih] + · by_cases h3 : c.toNat = 8 + · have hch : Char.ofNat 8 = c := by + have h4 := Char.ofNat_toNat c + rw [h3] at h4 + exact h4 + simp only [escape, h1, h2, h3, List.cons_append, List.nil_append, if_true, if_false] + rw [parseStrBody_escape 'b' (Char.ofNat 8) (by decide) (by decide) _] + rw [ih, hch] + rfl + · by_cases h4 : c.toNat = 9 + · have hch : Char.ofNat 9 = c := by + have h5 := Char.ofNat_toNat c + rw [h4] at h5 + exact h5 + simp [escape, h1, h2, h3, h4] + rw [parseStrBody_escape 't' (Char.ofNat 9) (by decide) (by decide) _] + rw [ih, hch] + rfl + · by_cases h5 : c.toNat = 10 + · have hch : Char.ofNat 10 = c := by + have h6 := Char.ofNat_toNat c + rw [h5] at h6 + exact h6 + simp [escape, h1, h2, h3, h4, h5] + rw [parseStrBody_escape 'n' (Char.ofNat 10) (by decide) (by decide) _] + rw [ih, hch] + rfl + · by_cases h6 : c.toNat = 12 + · have hch : Char.ofNat 12 = c := by + have h7 := Char.ofNat_toNat c + rw [h6] at h7 + exact h7 + simp [escape, h1, h2, h3, h4, h5, h6] + rw [parseStrBody_escape 'f' (Char.ofNat 12) (by decide) (by decide) _] + rw [ih, hch] + rfl + · by_cases h7 : c.toNat = 13 + · have hch : Char.ofNat 13 = c := by + have h8 := Char.ofNat_toNat c + rw [h7] at h8 + exact h8 + simp [escape, h1, h2, h3, h4, h5, h6, h7] + rw [parseStrBody_escape 'r' (Char.ofNat 13) (by decide) (by decide) _] + rw [ih, hch] + rfl + · by_cases h8 : c.toNat < 32 + · have hA : hexVal (hexDigit (c.toNat / 16)) = some (c.toNat / 16) := + hexVal_of_hexDigit (by omega) + have hB : hexVal (hexDigit (c.toNat % 16)) = some (c.toNat % 16) := + hexVal_of_hexDigit (by omega) + have hm : 0 * 4096 + 0 * 256 + (c.toNat / 16) * 16 + + (c.toNat % 16) = c.toNat := by omega + have hch : Char.ofNat (0 * 4096 + 0 * 256 + (c.toNat / 16) * 16 + + (c.toNat % 16)) = c := by + rw [hm] + exact Char.ofNat_toNat c + have hsmall : 0 * 4096 + 0 * 256 + (c.toNat / 16) * 16 + + (c.toNat % 16) < 55296 := by omega + simp [escape, h1, h2, h3, h4, h5, h6, h7, h8] + rw [parseStrBody_unicode hexVal_zero hexVal_zero hA hB hsmall _] + rw [ih, hch] + rfl + · simp [escape, h1, h2, h3, h4, h5, h6, h7, h8] + rw [parseStrBody_raw h1 h2 h8 _] + simp [ih] + +/-! ## Printed forms: lengths and head characters -/ + +/-- A member of a joined list is no longer than the whole join. -/ +theorem mem_join_length {y : List Char} {ys : List (List Char)} (h : y ∈ ys) : + y.length ≤ (join ys).length := by + induction ys with + | nil => simp at h + | cons z zs ih => + cases zs with + | nil => + have hy : y = z := by simpa using h + simp [join, hy] + | cons w ws => + have hjoin : join (z :: w :: ws) = z ++ ',' :: join (w :: ws) := by simp [join] + rw [hjoin] + cases List.mem_cons.mp h with + | inl h1 => + rw [h1] + simp only [List.length_append, List.length_cons] + omega + | inr h2 => + have hle := ih h2 + simp only [List.length_append, List.length_cons] + omega + +/-- The printed length of an array is its body length plus the + two brackets. -/ +theorem print_length_arr (vs : List Json) : + (print (Json.arr vs)).length = (join (vs.map print)).length + 2 := by + simp [print, List.length_append] + +/-- The printed length of an object is its body length plus the + two braces. -/ +theorem print_length_obj (kvs : List (List Char × Json)) : + (print (Json.obj kvs)).length = (join (kvs.map printPair)).length + 2 := by + simp [print, List.length_append] + +/-- The printed length of one object pair. -/ +theorem printPair_length (kv : List Char × Json) : + (printPair kv).length = (printStr kv.1).length + 1 + (print kv.2).length := by + cases kv with + | mk k v => + simp only [printPair, List.length_append, List.length_cons] + omega + +/-- The head character of a printed well formed value: never a + closing bracket, a closing brace, a comma, or whitespace. + The parser's body readers rely on this. -/ +theorem print_head {v : Json} (hv : WF v) : + ∃ c cs, print v = c :: cs ∧ c ≠ ']' ∧ c ≠ '}' ∧ c ≠ ',' ∧ isWs c = false := by + cases v with + | null => + exact ⟨'n', ['u', 'l', 'l'], by simp [print], by decide, by decide, by decide, + by decide⟩ + | bool b => + cases b with + | true => + exact ⟨'t', ['r', 'u', 'e'], by simp [print], by decide, by decide, by decide, + by decide⟩ + | false => + exact ⟨'f', ['a', 'l', 's', 'e'], by simp [print], by decide, by decide, by decide, + by decide⟩ + | str cs => + exact ⟨'"', escapeAll cs ++ ['"'], by simp [print, printStr], by decide, by decide, + by decide, by decide⟩ + | arr vs => + exact ⟨'[', join (vs.map print) ++ [']'], by simp [print], by decide, by decide, + by decide, by decide⟩ + | obj kvs => + exact ⟨'{', join (kvs.map printPair) ++ ['}'], by simp [print], by decide, by decide, + by decide, by decide⟩ + | num cs => + have hnum : WFNum cs := by + cases hv with + | num h => exact h + obtain ⟨neg, hd, intDs, frac, exp, hcs, hhd, -, -, -⟩ := hnum + have hdig : IsDigit hd := by + cases hhd with + | inl h => rw [h.1]; exact ⟨by decide, by decide⟩ + | inr h => + exact ⟨char_le_of_toNat (Nat.le_trans (by decide) (char_le_toNat h.1)), h.2⟩ + cases neg with + | true => + exact ⟨'-', (hd :: intDs) ++ frac ++ exp, by simp [print, hcs, List.append_assoc], + by decide, by decide, by decide, by decide⟩ + | false => + exact ⟨hd, intDs ++ frac ++ exp, by simp [print, hcs, List.append_assoc], + IsDigit.ne_of_toNat hdig (by decide), IsDigit.ne_of_toNat hdig (by decide), + IsDigit.ne_of_toNat hdig (by decide), IsDigit.isWs_false hdig⟩ + +/-- A printed well formed value has at least one character. -/ +theorem print_length_pos {v : Json} (hv : WF v) : 0 < (print v).length := by + obtain ⟨c, cs, h, -, -, -, -⟩ := print_head hv + rw [h] + simp + +/-! ## The round trip -/ + +/-- The three round trip statements at a printed length bound: + one for a value, one for the inside of an array, and one for + the inside of an object. -/ +def Triple (n : Nat) : Prop := + (∀ v, WF v → (print v).length ≤ n → ∀ (f : Nat) (rest : List Char), + (print v).length + 1 ≤ f → TailOk rest → + parseValue f (print v ++ rest) = some (v, rest)) ∧ + (∀ vs, (∀ v ∈ vs, WF v) → (join (vs.map print)).length ≤ n → + ∀ (f : Nat) (rest : List Char), (join (vs.map print)).length + 2 ≤ f → + parseEls f (join (vs.map print) ++ ']' :: rest) = some (vs, rest)) ∧ + (∀ kvs, (∀ kv ∈ kvs, WF kv.2) → (join (kvs.map printPair)).length ≤ n → + ∀ (f : Nat) (rest : List Char), (join (kvs.map printPair)).length + 2 ≤ f → + parseObjEls f (join (kvs.map printPair) ++ '}' :: rest) = some (kvs, rest)) + +/-- The round trip at any bound, by induction on a larger bound: + the bounded form of strong induction. The value statement calls + the two body statements at a smaller bound, spending the two + enclosing brackets. Each body statement calls the value + statement at the same bound for its members, and its own tail + recursion is structural. The fuel each call needs is bounded by + the printed length, which is what makes the counts line up. -/ +theorem key : ∀ n : Nat, Triple n := by + have aux : ∀ k n, n ≤ k → Triple n := by + intro k + induction k with + | zero => + intro n hn + have hn0 : n = 0 := Nat.eq_zero_of_le_zero hn + subst hn0 + refine ⟨?_, ?_, ?_⟩ + · intro v hv hlen _ _ _ _ + have hpos := print_length_pos hv + omega + · intro vs hvs hlen f rest hf + cases vs with + | nil => + cases f with + | zero => omega + | succ fuel => + show parseEls (fuel + 1) (']' :: rest) = some ([], rest) + rw [Json.parseEls.eq_2] + have hsk : skipWs (']' :: rest) = ']' :: rest := skipWs_cons (by decide) + simp [hsk] + | cons v vs => + have hmem : print v ∈ (v :: vs).map print := + List.mem_map.mpr ⟨v, List.mem_cons_self, rfl⟩ + have hle := mem_join_length hmem + have hpos := print_length_pos (hvs v (List.mem_cons_self)) + omega + · intro kvs hkvs hlen f rest hf + cases kvs with + | nil => + cases f with + | zero => omega + | succ fuel => + show parseObjEls (fuel + 1) ('}' :: rest) = some ([], rest) + rw [Json.parseObjEls.eq_2] + have hsk : skipWs ('}' :: rest) = '}' :: rest := skipWs_cons (by decide) + simp [hsk] + | cons kv kvs => + have hmem : printPair kv ∈ (kv :: kvs).map printPair := + List.mem_map.mpr ⟨kv, List.mem_cons_self, rfl⟩ + have hle := mem_join_length hmem + have hpos : 0 < (printPair kv).length := by + rw [printPair_length] + omega + omega + | succ k ihk => + intro n hn + have ih : ∀ m, m < n → Triple m := fun m hm => ihk m (by omega) + have hP : ∀ v, WF v → (print v).length ≤ n → ∀ (f : Nat) (rest : List Char), + (print v).length + 1 ≤ f → TailOk rest → + parseValue f (print v ++ rest) = some (v, rest) := by + intro v hv hlen f rest hf htail + cases f with + | zero => omega + | succ fuel => + cases v with + | null => simp [print, Json.parseValue.eq_2, skipWs, isWs] + | bool b => cases b <;> simp [print, Json.parseValue.eq_2, skipWs, isWs] + | str cs => + have hform : print (Json.str cs) ++ rest = + '"' :: (escapeAll cs ++ '"' :: rest) := by + simp [print, printStr, List.append_assoc] + rw [hform] + have hsk : skipWs ('"' :: (escapeAll cs ++ '"' :: rest)) = + '"' :: (escapeAll cs ++ '"' :: rest) := skipWs_cons (by decide) + simp [Json.parseValue.eq_2, hsk, parseStrBody_escapeAll] + | num cs => + have hnum : WFNum cs := by + cases hv with + | num h => exact h + have hnumc := hnum + obtain ⟨neg, hd, intDs, frac, exp, hcs, hhd, -, -, -⟩ := hnumc + have hdig : IsDigit hd := by + cases hhd with + | inl h => rw [h.1]; exact ⟨by decide, by decide⟩ + | inr h => + exact ⟨char_le_of_toNat (Nat.le_trans (by decide) (char_le_toNat h.1)), + h.2⟩ + cases neg with + | true => + have hform : print (Json.num cs) ++ rest = + '-' :: hd :: (intDs ++ (frac ++ (exp ++ rest))) := by + simp [print, hcs, List.append_assoc] + rw [hform] + have hsk : skipWs ('-' :: hd :: (intDs ++ (frac ++ (exp ++ rest)))) = + '-' :: hd :: (intDs ++ (frac ++ (exp ++ rest))) := + skipWs_cons (by decide) + have hnumres : parseNumber ('-' :: hd :: (intDs ++ (frac ++ (exp ++ rest)))) = + some (cs, rest) := by + have h := parseNumber_append hnum htail + rwa [show cs ++ rest = '-' :: hd :: (intDs ++ (frac ++ (exp ++ rest))) from + by simp [hcs, List.append_assoc]] at h + simp [Json.parseValue.eq_2, hsk, hnumres] + | false => + have hform : print (Json.num cs) ++ rest = + hd :: (intDs ++ (frac ++ (exp ++ rest))) := by + simp [print, hcs, List.append_assoc] + rw [hform] + have hsk : skipWs (hd :: (intDs ++ (frac ++ (exp ++ rest)))) = + hd :: (intDs ++ (frac ++ (exp ++ rest))) := + skipWs_cons (IsDigit.isWs_false hdig) + have hdis : hd = '-' ∨ isDigit hd := Or.inr (isDigit_of_isDigit hdig) + have hne_q : hd ≠ '"' := IsDigit.ne_of_toNat hdig (by decide) + have hne_lb : hd ≠ '[' := IsDigit.ne_of_toNat hdig (by decide) + have hne_lc : hd ≠ '{' := IsDigit.ne_of_toNat hdig (by decide) + have hne_t : hd ≠ 't' := IsDigit.ne_of_toNat hdig (by decide) + have hne_f : hd ≠ 'f' := IsDigit.ne_of_toNat hdig (by decide) + have hne_n : hd ≠ 'n' := IsDigit.ne_of_toNat hdig (by decide) + have hnumres : parseNumber (hd :: (intDs ++ (frac ++ (exp ++ rest)))) = + some (cs, rest) := by + have h := parseNumber_append hnum htail + rwa [show cs ++ rest = hd :: (intDs ++ (frac ++ (exp ++ rest))) from + by simp [hcs, List.append_assoc]] at h + simp [Json.parseValue.eq_2, hsk, hdis, hnumres, hne_q, hne_lb, hne_lc, hne_t, + hne_f, hne_n] + | arr vs => + have hvs : ∀ x ∈ vs, WF x := by + cases hv with + | arr h => exact h + have hlenE : (join (vs.map print)).length < n := by + have h1 : (print (Json.arr vs)).length = + (join (vs.map print)).length + 2 := print_length_arr vs + omega + have hE := (ih _ hlenE).2.1 vs hvs (Nat.le_refl _) fuel rest (by + have h1 : (print (Json.arr vs)).length = + (join (vs.map print)).length + 2 := print_length_arr vs + omega) + have hform : print (Json.arr vs) ++ rest = + '[' :: (join (vs.map print) ++ ']' :: rest) := by + simp [print, List.append_assoc] + rw [hform] + have hsk : skipWs ('[' :: (join (vs.map print) ++ ']' :: rest)) = + '[' :: (join (vs.map print) ++ ']' :: rest) := skipWs_cons (by decide) + simp [Json.parseValue.eq_2, hsk, hE] + | obj kvs => + have hkvs : ∀ kv ∈ kvs, WF kv.2 := by + cases hv with + | obj h => exact h + have hlenO : (join (kvs.map printPair)).length < n := by + have h1 : (print (Json.obj kvs)).length = + (join (kvs.map printPair)).length + 2 := print_length_obj kvs + omega + have hO := (ih _ hlenO).2.2 kvs hkvs (Nat.le_refl _) fuel rest (by + have h1 : (print (Json.obj kvs)).length = + (join (kvs.map printPair)).length + 2 := print_length_obj kvs + omega) + have hform : print (Json.obj kvs) ++ rest = + '{' :: (join (kvs.map printPair) ++ '}' :: rest) := by + simp [print, List.append_assoc] + rw [hform] + have hsk : skipWs ('{' :: (join (kvs.map printPair) ++ '}' :: rest)) = + '{' :: (join (kvs.map printPair) ++ '}' :: rest) := skipWs_cons (by decide) + simp [Json.parseValue.eq_2, hsk, hO] + have hE : ∀ vs, (∀ v ∈ vs, WF v) → (join (vs.map print)).length ≤ n → + ∀ (f : Nat) (rest : List Char), (join (vs.map print)).length + 2 ≤ f → + parseEls f (join (vs.map print) ++ ']' :: rest) = some (vs, rest) := by + intro vs + induction vs with + | nil => + intro _ _ f rest hf + cases f with + | zero => omega + | succ fuel => + show parseEls (fuel + 1) (']' :: rest) = some ([], rest) + rw [Json.parseEls.eq_2] + have hsk : skipWs (']' :: rest) = ']' :: rest := skipWs_cons (by decide) + simp [hsk] + | cons v vs ih => + intro hvs hlen f rest hf + have hv : WF v := hvs v (List.mem_cons_self) + have hvs' : ∀ x ∈ vs, WF x := fun x hx => hvs x (List.mem_cons_of_mem v hx) + obtain ⟨c, cs, hprint, hcne1, -, -, hcws⟩ := print_head hv + have hmemE : print v ∈ (v :: vs).map print := + List.mem_map.mpr ⟨v, List.mem_cons_self, rfl⟩ + have hple : (print v).length ≤ n := + Nat.le_trans (mem_join_length hmemE) hlen + cases f with + | zero => omega + | succ fuel => + cases vs with + | nil => + have hjoin : join ((v :: []).map print) = print v := by simp [join] + have hPv := hP v hv hple fuel (']' :: rest) (by + have hmem : print v ∈ (v :: []).map print := + List.mem_map.mpr ⟨v, List.mem_cons_self, rfl⟩ + have hle := mem_join_length hmem + simp only [List.map_cons, List.map_nil, join] at hf + omega) (tailOk_rbracket rest) + rw [hjoin] + show parseEls (fuel + 1) (print v ++ ']' :: rest) = some (v :: [], rest) + have hsk1 : skipWs (print v ++ ']' :: rest) = print v ++ ']' :: rest := + skipWs_append_of_head (by simp [hprint]) hcws + have hPv2 : parseValue fuel (c :: (cs ++ ']' :: rest)) = + some (v, ']' :: rest) := by + have e : print v ++ ']' :: rest = c :: (cs ++ ']' :: rest) := by + simp [hprint] + rw [e] at hPv + exact hPv + have hsk3 : skipWs (']' :: rest) = ']' :: rest := skipWs_cons (by decide) + rw [Json.parseEls.eq_2, hsk1, hprint] + simp [hcne1, hPv2, hsk3] + | cons w ws => + have hjoin : join ((v :: w :: ws).map print) = + print v ++ ',' :: join ((w :: ws).map print) := by simp [join] + have hmono : (join ((w :: ws).map print)).length ≤ + (join ((v :: w :: ws).map print)).length := by + rw [hjoin] + simp only [List.length_append, List.length_cons] + omega + have hlen' : (join ((w :: ws).map print)).length ≤ n := Nat.le_trans hmono hlen + have hf' : (join ((w :: ws).map print)).length + 2 ≤ fuel := by + have hbl : (join ((v :: w :: ws).map print)).length = + (print v).length + 1 + (join ((w :: ws).map print)).length := by + rw [hjoin] + simp only [List.length_append, List.length_cons] + omega + omega + have hEls := ih hvs' hlen' fuel rest hf' + have hPv := hP v hv hple fuel + ((',' :: join ((w :: ws).map print)) ++ ']' :: rest) (by + have hmem : print v ∈ (v :: w :: ws).map print := + List.mem_map.mpr ⟨v, List.mem_cons_self, rfl⟩ + have hle := mem_join_length hmem + omega) (tailOk_comma _) + have hPvT : parseValue fuel + (print v ++ (',' :: (join ((w :: ws).map print) ++ ']' :: rest))) = + some (v, ',' :: (join ((w :: ws).map print) ++ ']' :: rest)) := hPv + have hPv2 : parseValue fuel + (c :: (cs ++ (',' :: (join ((w :: ws).map print) ++ ']' :: rest)))) = + some (v, ',' :: (join ((w :: ws).map print) ++ ']' :: rest)) := by + have e : print v ++ (',' :: (join ((w :: ws).map print) ++ ']' :: rest)) = + c :: (cs ++ (',' :: (join ((w :: ws).map print) ++ ']' :: rest))) := by + simp [hprint] + rw [e] at hPvT + exact hPvT + obtain ⟨c2, cs2, hprint2, hc2ne1, -, -, hc2ws⟩ := + print_head (hvs' w (List.mem_cons_self)) + have hjoinw : join ((w :: ws).map print) = + print w ++ (if ws = [] then [] else ',' :: join (ws.map print)) := by + cases ws with + | nil => simp [join] + | cons x xs => simp [join] + have hskA : skipWs + (c :: (cs ++ (',' :: (join ((w :: ws).map print) ++ ']' :: rest)))) = + c :: (cs ++ (',' :: (join ((w :: ws).map print) ++ ']' :: rest))) := + skipWs_cons hcws + have hskB : skipWs (',' :: (join ((w :: ws).map print) ++ ']' :: rest)) = + ',' :: (join ((w :: ws).map print) ++ ']' :: rest) := + skipWs_cons (by decide) + have hsk2 : skipWs (join ((w :: ws).map print) ++ ']' :: rest) = + c2 :: (cs2 ++ + ((if ws = [] then [] else ',' :: join (ws.map print)) ++ + ']' :: rest)) := by + have e1 : join ((w :: ws).map print) ++ ']' :: rest = + print w ++ + ((if ws = [] then [] else ',' :: join (ws.map print)) ++ + ']' :: rest) := by + rw [hjoinw, List.append_assoc] + rw [e1] + have e2 := skipWs_append_of_head (l := print w) + (rest := (if ws = [] then [] else ',' :: join (ws.map print)) ++ + ']' :: rest) (by simp [hprint2]) hc2ws + rw [e2, hprint2] + exact List.cons_append + rw [hjoin, List.append_assoc, hprint] + show parseEls (fuel + 1) + (c :: (cs ++ (',' :: (join ((w :: ws).map print) ++ ']' :: rest)))) = + some (v :: w :: ws, rest) + rw [Json.parseEls.eq_2] + simp only [hskA, hPv2, hskB, hsk2, hEls] + simp [hcne1, hc2ne1] + have hO : ∀ kvs, (∀ kv ∈ kvs, WF kv.2) → (join (kvs.map printPair)).length ≤ n → + ∀ (f : Nat) (rest : List Char), (join (kvs.map printPair)).length + 2 ≤ f → + parseObjEls f (join (kvs.map printPair) ++ '}' :: rest) = some (kvs, rest) := by + intro kvs + induction kvs with + | nil => + intro _ _ f rest hf + cases f with + | zero => omega + | succ fuel => + show parseObjEls (fuel + 1) ('}' :: rest) = some ([], rest) + rw [Json.parseObjEls.eq_2] + have hsk : skipWs ('}' :: rest) = '}' :: rest := skipWs_cons (by decide) + simp [hsk] + | cons kv kvs ih => + intro hkvs hlen f rest hf + cases kv with + | mk k v => + have hv2 : WF v := hkvs (k, v) (List.mem_cons_self) + have hkvs' : ∀ x ∈ kvs, WF x.2 := + fun x hx => hkvs x (List.mem_cons_of_mem (k, v) hx) + have hpp : printPair (k, v) = '"' :: (escapeAll k ++ '"' :: ':' :: print v) := by + simp [printPair, printStr, List.append_assoc] + have hple : (print v).length ≤ n := by + have h1 : (print v).length ≤ (printPair (k, v)).length := by + have h := printPair_length (k, v) + dsimp only at h + omega + have hmem : printPair (k, v) ∈ ((k, v) :: kvs).map printPair := + List.mem_map.mpr ⟨(k, v), List.mem_cons_self, rfl⟩ + have h2 := mem_join_length hmem + omega + cases f with + | zero => omega + | succ fuel => + cases kvs with + | nil => + have hjoin : join (((k, v) :: []).map printPair) = printPair (k, v) := by + simp [join] + have hPv := hP v hv2 hple fuel ('}' :: rest) (by + have h1 : (print v).length ≤ (printPair (k, v)).length := by + have h := printPair_length (k, v) + dsimp only at h + omega + have hmem : printPair (k, v) ∈ ((k, v) :: []).map printPair := + List.mem_map.mpr ⟨(k, v), List.mem_cons_self, rfl⟩ + have h2 := mem_join_length hmem + simp only [List.map_cons, List.map_nil, join] at hf + omega) (tailOk_rbrace rest) + rw [hjoin] + show parseObjEls (fuel + 1) (printPair (k, v) ++ '}' :: rest) = + some ((k, v) :: [], rest) + have hsk1 : skipWs (printPair (k, v) ++ '}' :: rest) = + printPair (k, v) ++ '}' :: rest := + skipWs_append_of_head (c := '"') (by simp [hpp]) (by decide) + have hskC : skipWs (':' :: (print v ++ '}' :: rest)) = + ':' :: (print v ++ '}' :: rest) := skipWs_cons (by decide) + rw [Json.parseObjEls.eq_2] + simp [hsk1, hpp, parseStrBody_escapeAll, hskC, hPv, skipWs, isWs] + | cons kv' kvs' => + have hjoin : join (((k, v) :: kv' :: kvs').map printPair) = + printPair (k, v) ++ ',' :: join ((kv' :: kvs').map printPair) := by + simp [join] + have hmono : (join ((kv' :: kvs').map printPair)).length ≤ + (join (((k, v) :: kv' :: kvs').map printPair)).length := by + rw [hjoin] + simp only [List.length_append, List.length_cons] + omega + have hlen' : (join ((kv' :: kvs').map printPair)).length ≤ n := + Nat.le_trans hmono hlen + have hf' : (join ((kv' :: kvs').map printPair)).length + 2 ≤ fuel := by + have hbl : (join (((k, v) :: kv' :: kvs').map printPair)).length = + (printPair (k, v)).length + 1 + + (join ((kv' :: kvs').map printPair)).length := by + rw [hjoin] + simp only [List.length_append, List.length_cons] + omega + omega + have hO' := ih hkvs' hlen' fuel rest hf' + have hPv := hP v hv2 hple fuel + ((',' :: join ((kv' :: kvs').map printPair)) ++ '}' :: rest) (by + have h1 : (print v).length ≤ (printPair (k, v)).length := by + have h := printPair_length (k, v) + dsimp only at h + omega + have hmem : printPair (k, v) ∈ ((k, v) :: kv' :: kvs').map printPair := + List.mem_map.mpr ⟨(k, v), List.mem_cons_self, rfl⟩ + have h2 := mem_join_length hmem + omega) (tailOk_comma _) + cases kv' with + | mk k' v' => + have hPv2 : parseValue fuel + (print v ++ + (',' :: (join (((k', v') :: kvs').map printPair) ++ + '}' :: rest))) = + some (v, ',' :: (join (((k', v') :: kvs').map printPair) ++ + '}' :: rest)) := hPv + have hskA : skipWs ('"' :: (escapeAll k ++ '"' :: ':' :: + (print v ++ + (',' :: (join (((k', v') :: kvs').map printPair) ++ + '}' :: rest))))) = + '"' :: (escapeAll k ++ '"' :: ':' :: + (print v ++ + (',' :: (join (((k', v') :: kvs').map printPair) ++ + '}' :: rest)))) := + skipWs_cons (by decide) + have hskC2 : skipWs (':' :: (print v ++ + (',' :: (join (((k', v') :: kvs').map printPair) ++ + '}' :: rest)))) = + ':' :: (print v ++ + (',' :: (join (((k', v') :: kvs').map printPair) ++ + '}' :: rest))) := + skipWs_cons (by decide) + have hskT2 : skipWs + (',' :: (join (((k', v') :: kvs').map printPair) ++ + '}' :: rest)) = + ',' :: (join (((k', v') :: kvs').map printPair) ++ + '}' :: rest) := + skipWs_cons (by decide) + have hpp' : printPair (k', v') = + '"' :: (escapeAll k' ++ '"' :: ':' :: print v') := by + simp [printPair, printStr, List.append_assoc] + have hjoin' : join (((k', v') :: kvs').map printPair) = + printPair (k', v') ++ + (if kvs' = [] then [] else ',' :: join (kvs'.map printPair)) := by + cases kvs' with + | nil => simp [join] + | cons x xs => simp [join] + have hsk4 : skipWs (join (((k', v') :: kvs').map printPair) ++ + '}' :: rest) = + '"' :: (escapeAll k' ++ '"' :: (':' :: (print v' ++ + ((if kvs' = [] then [] else ',' :: join (kvs'.map printPair)) ++ + '}' :: rest)))) := by + have e1 : join (((k', v') :: kvs').map printPair) ++ '}' :: rest = + printPair (k', v') ++ + ((if kvs' = [] then [] else ',' :: join (kvs'.map printPair)) ++ + '}' :: rest) := by + rw [hjoin', List.append_assoc] + rw [e1] + have e2 := skipWs_append_of_head (l := printPair (k', v')) (c := '"') + (rest := (if kvs' = [] then [] else ',' :: join (kvs'.map printPair)) ++ + '}' :: rest) (by simp [hpp']) (by decide) + rw [e2, hpp'] + simp [List.append_assoc] + rw [hjoin, List.append_assoc, hpp] + rw [Json.parseObjEls.eq_2] + simp only [List.cons_append, List.append_assoc] + simp only [hskA, parseStrBody_escapeAll, hskC2, hPv2, hskT2, hsk4, hO'] + simp + exact ⟨hP, hE, hO⟩ + intro n + exact aux n n (Nat.le_refl n) + +/-- The round trip: parsing the printed form of a well formed value + gives the value back. -/ +theorem parse_print {v : Json} (hv : WF v) : parse (print v) = some v := by + have h := (key (print v).length).1 v hv (Nat.le_refl _) ((print v).length + 1) [] + (Nat.le_refl _) tailOk_nil + have h2 : parseValue ((print v).length + 1) (print v) = some (v, []) := by + simpa using h + unfold parse + simp [h2, skipWs] + +end Json.Proofs diff --git a/Proofs/Token.lean b/Proofs/Token.lean new file mode 100644 index 0000000..1abdee7 --- /dev/null +++ b/Proofs/Token.lean @@ -0,0 +1,114 @@ +import Jws.Token +import Proofs.RoundTrip +import Proofs.B64 +import Proofs.Utf8 + +namespace Jws.Proofs + +open Jws + +/-- Splitting reads back a join whose first part is free of the + separator: the first part comes off whole. -/ +theorem splitSep_append (sep : Char) (p rest : List Char) (h : sep ∉ p) : + splitSep sep (p ++ sep :: rest) = p :: splitSep sep rest := by + induction p with + | nil => + simp only [List.nil_append] + rw [splitSep] + exact if_pos rfl + | cons c cs ih => + have hc : c ≠ sep := by + intro e + apply h + rw [e] + exact List.mem_cons_self + have hcs : sep ∉ cs := fun hm => h (List.mem_cons_of_mem _ hm) + rw [List.cons_append, splitSep, if_neg hc, ih hcs] + +/-- Splitting a text with no separator in it gives the text back + as the one part. -/ +theorem splitSep_of_not_mem (sep : Char) (p : List Char) (h : sep ∉ p) : + splitSep sep p = [p] := by + induction p with + | nil => rfl + | cons c cs ih => + have hc : c ≠ sep := by + intro e + apply h + rw [e] + exact List.mem_cons_self + have hcs : sep ∉ cs := fun hm => h (List.mem_cons_of_mem _ hm) + rw [splitSep, if_neg hc, ih hcs] + +/-- No character the base64url encoder writes is the dot. -/ +theorem encode_ne_dot : ∀ (bs : List UInt8) (c : Char), + c ∈ Base64url.encode bs → c ≠ '.' := by + intro bs + induction bs using Base64url.encode.induct with + | case1 a b d rest ih => + intro c h + rw [Base64url.encode] at h + simp only [List.mem_cons] at h + have ha := UInt8.toNat_lt a + have hb := UInt8.toNat_lt b + have hd := UInt8.toNat_lt d + rcases h with rfl | rfl | rfl | rfl | h + · exact Base64url.Proofs.char_ne_dot (by omega) + · exact Base64url.Proofs.char_ne_dot (Nat.mod_lt _ (by decide)) + · exact Base64url.Proofs.char_ne_dot (Nat.mod_lt _ (by decide)) + · exact Base64url.Proofs.char_ne_dot (Nat.mod_lt _ (by decide)) + · exact ih c h + | case2 a b => + intro c h + rw [Base64url.encode] at h + simp only [List.mem_cons, List.mem_singleton] at h + have ha := UInt8.toNat_lt a + have hb := UInt8.toNat_lt b + rcases h with rfl | rfl | rfl | h + · exact Base64url.Proofs.char_ne_dot (by omega) + · exact Base64url.Proofs.char_ne_dot (Nat.mod_lt _ (by decide)) + · exact Base64url.Proofs.char_ne_dot (Nat.mod_lt _ (by decide)) + · cases h + | case3 a => + intro c h + rw [Base64url.encode] at h + simp only [List.mem_cons, List.mem_singleton] at h + have ha := UInt8.toNat_lt a + rcases h with rfl | rfl | h + · exact Base64url.Proofs.char_ne_dot (by omega) + · exact Base64url.Proofs.char_ne_dot (Nat.mod_lt _ (by decide)) + · cases h + | case4 => + intro c h + cases h + +/-- The printed token splits into its three printed parts. -/ +theorem splitSep_print (t : Token) : + splitSep '.' (printToken t) = + [Base64url.encode (Utf8.encode (Json.print t.header)), + Base64url.encode (Utf8.encode (Json.print t.claims)), + Base64url.encode t.sig] := by + have n1 : ∀ c ∈ Base64url.encode (Utf8.encode (Json.print t.header)), c ≠ '.' := + fun c hc => encode_ne_dot _ c hc + have n2 : ∀ c ∈ Base64url.encode (Utf8.encode (Json.print t.claims)), c ≠ '.' := + fun c hc => encode_ne_dot _ c hc + have n3 : ∀ c ∈ Base64url.encode t.sig, c ≠ '.' := + fun c hc => encode_ne_dot _ c hc + simp only [printToken, joinSep] + rw [splitSep_append _ _ _ (fun hm => n1 _ hm rfl), + splitSep_append _ _ _ (fun hm => n2 _ hm rfl), + splitSep_of_not_mem _ _ (fun hm => n3 _ hm rfl)] + +/-- The plan's main claim: parsing a printed token gives the + token back, for tokens whose JSON parts are well formed in + the json slice's sense. The proof is a chain of the three + round trips under it: the JSON text round trip, the UTF-8 + round trip, and the base64url round trip, with the split and + join of the three parts read back by the two lemmas above. -/ +theorem parseToken_print (t : Token) (hh : Json.WF t.header) (hc : Json.WF t.claims) : + parseToken (printToken t) = some t := by + obtain ⟨h, c, s⟩ := t + simp only [parseToken, splitSep_print, Base64url.Proofs.decode_encode, + Utf8.Proofs.decode_encode, Json.Proofs.parse_print hh, Json.Proofs.parse_print hc] + +end Jws.Proofs diff --git a/Proofs/Utf8.lean b/Proofs/Utf8.lean new file mode 100644 index 0000000..0735767 --- /dev/null +++ b/Proofs/Utf8.lean @@ -0,0 +1,135 @@ +import Jws.Utf8 +import Proofs.B64 + +namespace Jws.Utf8.Proofs + +open Jws.Utf8 Jws.Base64url.Proofs + +/-- A character value is below 110000, and no character value + lies in the surrogate gap D800 to DFFF: the Unicode scalar + range every `Char` lives in. -/ +theorem char_bounds (c : Char) : + c.toNat < 0x110000 ∧ ¬ (0xD800 ≤ c.toNat ∧ c.toNat < 0xE000) := by + have h := c.valid + show c.val.toNat < 0x110000 ∧ ¬ (0xD800 ≤ c.val.toNat ∧ c.val.toNat < 0xE000) + rcases h with h | ⟨h1, h2⟩ + · exact ⟨by omega, by omega⟩ + · exact ⟨by omega, by omega⟩ + +/-- A byte whose value is known to be a continuation byte reads + back as its payload value. -/ +theorem contVal_of_toNat {b : UInt8} {k : Nat} (h : b.toNat = 0x80 + k) (hk : k < 64) : + contVal b = some k := by + unfold contVal + rw [h, if_pos ⟨by omega, by omega⟩, Nat.add_sub_cancel_left] + +/-- One step of the decoder on a plain byte. -/ +theorem decode_one (b : UInt8) (bs : List UInt8) (hb : b.toNat < 0x80) : + decode (b :: bs) = (decode bs).map (Char.ofNat b.toNat :: ·) := by + cases bs with + | nil => rw [decode.eq_3, if_pos hb] + | cons b1 bs' => rw [decode.eq_2, if_pos hb] + +/-- One step of the decoder on a two byte form. -/ +theorem decode_two (b b1 : UInt8) (bs : List UInt8) (v : Nat) + (hb : 0xC2 ≤ b.toNat ∧ b.toNat < 0xE0) (hv : contVal b1 = some v) : + decode (b :: b1 :: bs) = + (decode bs).map (Char.ofNat ((b.toNat - 0xC0) * 64 + v) :: ·) := by + rw [decode.eq_2, if_neg (by omega : ¬ b.toNat < 0x80), + if_neg (by omega : ¬ b.toNat < 0xC2), if_pos (by omega : b.toNat < 0xE0), hv] + +/-- One step of the decoder on a three byte form. -/ +theorem decode_three (b b1 b2 : UInt8) (bs : List UInt8) (v1 v2 : Nat) + (hb : 0xE0 ≤ b.toNat ∧ b.toNat < 0xF0) + (hside : (b.toNat = 0xE0 → 0x20 ≤ v1) ∧ (b.toNat = 0xED → v1 < 0x20)) + (hv1 : contVal b1 = some v1) (hv2 : contVal b2 = some v2) : + decode (b :: b1 :: b2 :: bs) = + (decode bs).map (Char.ofNat ((b.toNat - 0xE0) * 4096 + v1 * 64 + v2) :: ·) := by + rw [decode.eq_2, if_neg (by omega : ¬ b.toNat < 0x80), + if_neg (by omega : ¬ b.toNat < 0xC2), if_neg (by omega : ¬ b.toNat < 0xE0), + if_pos (by omega : b.toNat < 0xF0)] + dsimp only + rw [hv1, hv2] + dsimp only + rw [if_pos hside] + +/-- One step of the decoder on a four byte form. -/ +theorem decode_four (b b1 b2 b3 : UInt8) (bs : List UInt8) (v1 v2 v3 : Nat) + (hb : 0xF0 ≤ b.toNat ∧ b.toNat < 0xF5) + (hside : (b.toNat = 0xF0 → 0x10 ≤ v1) ∧ (b.toNat = 0xF4 → v1 < 0x10)) + (hv1 : contVal b1 = some v1) (hv2 : contVal b2 = some v2) + (hv3 : contVal b3 = some v3) : + decode (b :: b1 :: b2 :: b3 :: bs) = + (decode bs).map + (Char.ofNat ((b.toNat - 0xF0) * 262144 + v1 * 4096 + v2 * 64 + v3) :: ·) := by + rw [decode.eq_2, if_neg (by omega : ¬ b.toNat < 0x80), + if_neg (by omega : ¬ b.toNat < 0xC2), if_neg (by omega : ¬ b.toNat < 0xE0), + if_neg (by omega : ¬ b.toNat < 0xF0), if_pos (by omega : b.toNat < 0xF5)] + dsimp only + rw [hv1, hv2, hv3] + dsimp only + rw [if_pos hside] + +/-- Decoding one encoded character in front of any bytes decodes + the character and then the bytes. The four cases are the four + lengths; each one applies the step lemma for its length, + checks the side conditions with arithmetic, and rebuilds the + character value. -/ +theorem decode_append_char (c : Char) (bs : List UInt8) : + decode (encodeChar c ++ bs) = (decode bs).map (c :: ·) := by + obtain ⟨hmax, hnsur⟩ := char_bounds c + by_cases h1 : c.toNat < 0x80 + · rw [encodeChar, if_pos h1, List.cons_append, List.nil_append, + decode_one _ _ (by rw [toNat_toUInt8 (by omega)]; exact h1), + toNat_toUInt8 (by omega), Char.ofNat_toNat] + · rw [encodeChar, if_neg h1] + by_cases h2 : c.toNat < 0x800 + · have hlead : (0xC0 + c.toNat / 64).toUInt8.toNat = 0xC0 + c.toNat / 64 := + toNat_toUInt8 (by omega) + rw [if_pos h2, List.cons_append, List.cons_append, List.nil_append, + decode_two _ _ _ _ ⟨by omega, by omega⟩ + (contVal_of_toNat (toNat_toUInt8 (by omega)) (Nat.mod_lt _ (by decide))), + hlead, + show (0xC0 + c.toNat / 64 - 0xC0) * 64 + c.toNat % 64 = c.toNat by omega, + Char.ofNat_toNat] + · rw [if_neg h2] + by_cases h3 : c.toNat < 0x10000 + · have hlead : (0xE0 + c.toNat / 4096).toUInt8.toNat = 0xE0 + c.toNat / 4096 := + toNat_toUInt8 (by omega) + rw [if_pos h3, List.cons_append, List.cons_append, List.cons_append, + List.nil_append, + decode_three _ _ _ _ _ _ ⟨by omega, by omega⟩ + ⟨fun hb => by rw [hlead] at hb; omega, + fun hb => by rw [hlead] at hb; omega⟩ + (contVal_of_toNat (toNat_toUInt8 (by omega)) (Nat.mod_lt _ (by decide))) + (contVal_of_toNat (toNat_toUInt8 (by omega)) (Nat.mod_lt _ (by decide))), + hlead, + show (0xE0 + c.toNat / 4096 - 0xE0) * 4096 + (c.toNat / 64) % 64 * 64 + + c.toNat % 64 = c.toNat by omega, + Char.ofNat_toNat] + · have hlead : (0xF0 + c.toNat / 262144).toUInt8.toNat = 0xF0 + c.toNat / 262144 := + toNat_toUInt8 (by omega) + rw [if_neg h3, List.cons_append, List.cons_append, List.cons_append, + List.cons_append, List.nil_append, + decode_four _ _ _ _ _ _ _ _ ⟨by omega, by omega⟩ + ⟨fun hb => by rw [hlead] at hb; omega, + fun hb => by rw [hlead] at hb; omega⟩ + (contVal_of_toNat (toNat_toUInt8 (by omega)) (Nat.mod_lt _ (by decide))) + (contVal_of_toNat (toNat_toUInt8 (by omega)) (Nat.mod_lt _ (by decide))) + (contVal_of_toNat (toNat_toUInt8 (by omega)) (Nat.mod_lt _ (by decide))), + hlead, + show (0xF0 + c.toNat / 262144 - 0xF0) * 262144 + (c.toNat / 4096) % 64 * 4096 + + (c.toNat / 64) % 64 * 64 + c.toNat % 64 = c.toNat by omega, + Char.ofNat_toNat] + +/-- Decoding the encoding of any text gives the text back. -/ +theorem decode_encode : ∀ cs : List Char, decode (encode cs) = some cs := by + intro cs + induction cs with + | nil => rfl + | cons c cs ih => + show decode (encodeChar c ++ encode cs) = some (c :: cs) + rw [decode_append_char, ih] + rfl + +end Jws.Utf8.Proofs diff --git a/README.md b/README.md index fd90273..b8a3dc2 100644 --- a/README.md +++ b/README.md @@ -1,44 +1,72 @@ -# jws +# jws: a JWS compact parser and checker, with a proved round trip -A Lean parser for JWS compact serialization. This is a Proven Commons project: it rebuilds a widely used format in Lean and proves the new code follows its written specification. +A parser and checker for the JWS compact form (RFC 7515) in Lean, with the plan's main claim proved: printing a parsed token gives the token back. The parser reads the three base64url parts, decodes the header and payload as JSON, and holds the signature bytes unchanged. The checker runs the shape and claims rules of `SPEC.md` (algorithm allowlist, required claims, and the `exp`, `nbf`, `iss`, and `aud` claims against a caller supplied context). Tests run the RFC 7515 Appendix A examples and a differential corpus against an oracle implementing the same rules; see `tests/TEST-RESULTS.md` for the counts. -Status: not verified. No code has landed yet. Plan issue 1 holds the first slice, and it is unclaimed. The specification has not been approved by a reviewer, so do not call this verified. +Status: in progress. The first slice from plan issue 1 has landed locally. The specification has not yet been approved by a reviewer apart from its author, and no statement file (`Spec.lean`) has been added by a reviewer, so this is not verified. ## Limit, stated up front This slice does not verify a signature. It must never be described as a verified token on its own. Signature verification is the second slice. A caller that reads claims from this slice without verifying the signature has not checked authenticity. -## First slice +## Where the JSON code came from -A JSON Web Signature in compact form is three base64url parts joined by dots. The first part is the header. The second part is the payload. The third part is the signature. +The JSON parser, printer, value type, and round trip proof are the json repo's, carried in unchanged under `Json/` and `Proofs/RoundTrip.lean` (the repos in this org do not import each other). Everything else is new here: the base64url codec (`Jws/Base64url.lean`), a strict UTF-8 codec (`Jws/Utf8.lean`), and the token framing, claims reading, and checker (`Jws/Token.lean`). The base64url code follows the shape of the codec repo's Base64 work, with the URL safe alphabet and no padding. -- Parse the compact form. -- Decode the header and payload as JSON, using the json repo. -- Read the registered claims exp, nbf, iss, aud, and iat. -- Reject a header with alg set to none. -- Reject an alg outside a caller supplied allowlist. -- Reject a missing required claim, an expired exp, a not yet valid nbf, and a mismatched iss or aud. -- Return the signature bytes unchanged, for a verifier the caller supplies. +## What is proved -## Main claim +| Claim | Theorem | +|-------|---------| +| Parsing the printed form of a token gives the token back, for tokens whose JSON parts are well formed in the json slice's sense. | `Jws.Proofs.parseToken_print` | +| Decoding the base64url encoding of any bytes gives the bytes back. | `Jws.Base64url.Proofs.decode_encode` | +| Encoding the decoding of any text the decoder accepts gives the text back. | `Jws.Base64url.Proofs.encode_decode` | +| Decoding the UTF-8 encoding of any text gives the text back. | `Jws.Utf8.Proofs.decode_encode` | +| Parsing the canonical printed form of a well formed JSON value gives the value back (carried in with the JSON code). | `Json.Proofs.parse_print` | -Printing a parsed token gives the same token back. A token is accepted only when its framing matches the compact form, its header alg is on the allowlist, and its registered claims pass the checks above. +The two base64url round trips check against `propext` and `Quot.sound` only. The token and UTF-8 round trips check against the standard three (`propext`, `Classical.choice`, `Quot.sound`). A reader can confirm with `#print axioms` on each name. -## Test oracles +## What is not proved -- PyJWT and Go JWT libraries. -- RFC 7515 Appendix A and B test vectors. -- RFC 7519 examples. +- That the checker accepts exactly the tokens `SPEC.md` says it should. The acceptance rules live in one function (`Jws.accept`) and their completeness rests on the tests: the RFC examples, the mutation cases, and the differential corpus against the harness oracle. +- Signature verification, as stated above: nothing about keys, signing inputs, or any algorithm. +- The reverse printing direction at the token level (printing a parsed token is how the round trip is stated; the base64url and JSON layers each prove their own reverse directions). +- Anything about the numeric meaning of claims beyond the exact decimal reading the checker itself uses (whole seconds, comparisons). The reading code is exercised by the tests, including exponent spellings and very large exponents. +- Reading requests and printing answers in `Main.lean`: line splitting, the field format, the decimal code reading. The tests cover them, malformed requests included. +- Speed. The code works on lists, which suits proofs, not large tokens. -## Score +Two readings worth naming, both stated in `SPEC.md` and pinned by tests: -16 out of 18, first pass score in mission issue 19, the round 4 sheet. Created at the org owner's direction on that sheet, on the judgement that the slice, claim, and oracles are sound and that it duplicates no existing repo. +- An empty signature part is well formed, so it can pass the checks. Only the algorithm name `none` is turned away outright, together with any context whose allowlist names `none`. +- When a JSON object repeats a name, lookup reads the first copy, as the JSON code's lookup does. -## What is not in this slice +## What you must trust -- Signature verification. -- Any claim that a token read here is authentic. +- The Lean kernel, which checks the proofs. +- The Lean compiler, with the C compiler and linker shipped with it, and the runtime, which turn the proved definitions into the program that runs. +- Lean's core library, including the compiled code it puts in place of some definitions the proofs reason about. +- The operating system and hardware it runs on. +- For the tests: Python's standard library (the oracle's JSON reading and exact decimals), PyJWT and cryptography in the test venv when present (token building and decode cross checks only; verdicts never come from PyJWT), and the RFC 7515 text for the fixed examples. The results file names the versions used. -## Layout, when the first slice lands +This project has no dependencies beyond Lean itself. The test harness's PyJWT corpus is optional and lives in a venv inside the work directory. -The layout follows the Proven Commons template in the mission repo, under bar/template. Spec.lean holds the statements a reviewer approves. Proofs.lean holds the proofs under the same names. Main.lean holds the command line tool used by the tests. The bar check runs in CI on every change. +## Run it + +Needs Linux and [elan](https://github.com/leanprover/elan). Build, then feed request lines to the tool: + +``` +lake build +python3 tests/run_tests.py +``` + +A request is one `check` line; `SPEC.md` states the field format in full. The token text, the current time, the allowlist, the required claims, the expected issuer, and the expected audience are the six fields, each written as comma separated decimal character codes, the fields separated by semicolons. The answer is `ok:` and the codes of the canonical reprinted token, `none` when the token is not accepted, and `error` when the request is malformed. + +## Re-check it + +Needs Linux, elan, and Python 3.11 or later. + +``` +lake build +grep -rn "sorry" --include="*.lean" Json Jws Proofs Main.lean Json.lean Jws.lean Proofs.lean +python3 tests/run_tests.py +``` + +The grep should print nothing: there is no `sorry` anywhere. The test script runs the fixed RFC cases, the mutation cases, the malformed request cases, and the differential corpus (PyJWT built tokens when the venv is present, plus a seeded random corpus), and writes the counts to `tests/TEST-RESULTS.md`. diff --git a/SPEC.md b/SPEC.md new file mode 100644 index 0000000..ef172de --- /dev/null +++ b/SPEC.md @@ -0,0 +1,178 @@ +# JWS compact form: parser and checker — specification + +This is the first slice of the jws repo: parse a JWS in compact +form (RFC 7515 section 5.2), run a set of shape and claims +checks on it, and print it back in a canonical form. + +**This slice does not verify the signature.** A token that +passes every check below is well formed and its claims are +consistent with the check context. It is not thereby verified: +nothing here shows the signature was made by the holder of any +key, or that it covers these header and payload bytes at all. +Signature verification is the second slice and is out of scope +here. Do not treat a passing answer from this code as a verified +token. + +## Framing + +A compact token is three base64url parts joined by dots: + +``` +part1 "." part2 "." part3 +``` + +- Part 1 is the header: UTF-8 JSON text, encoded in base64url. +- Part 2 is the payload, the claims set: UTF-8 JSON text, + encoded in base64url. +- Part 3 is the signature: raw bytes, encoded in base64url. + +Exactly three parts. Two parts or four parts are turned away. +An empty part is allowed by the framing (the empty text is +well formed base64url for zero bytes); the checks below decide +whether what it decodes to is acceptable. In particular an +empty signature part is well formed. + +## Base64url, strict + +Decoding follows RFC 4648 section 5 with no padding, and is +strict: + +- The alphabet is `A-Z a-z 0-9 - _`. Any other character turns + the part away, including `=` (padding is not part of the + compact form, so a padded part is turned away) and the + standard base64 characters `+` and `/`. +- A part whose length is 1 mod 4 is impossible and is turned + away. +- The unused bits in the final character must be zero. In a + final group of two characters (one byte), the second + character's low four bits are unused and must be zero. In a + final group of three characters (two bytes), the third + character's low two bits must be zero. + +Encoding writes no padding and always sets the unused bits to +zero, so decoding an encoding and encoding a decoding are both +the identity. Both directions are proved in this repo. + +The header and payload bytes must then be UTF-8, read strictly: +overlong forms, encodings of the surrogate values U+D800 to +U+DFFF, values above U+10FFFF, stray continuation bytes, and +truncated sequences are all turned away. The texts must then +parse as JSON under the rules of the json slice carried into +this repo (RFC 8259 grammar; lone surrogate escapes in strings +are turned away, as that slice's parser cannot hold them). + +## The check + +The caller supplies a context: + +- an allowlist of algorithm names; +- the current time in seconds, an integer, or no time (see + below); +- a list of required claim names; +- an expected issuer, or none; +- an expected audience, or none. + +The token is accepted only when every rule holds: + +1. The framing is exactly three parts, each strict base64url + (above). The signature bytes are returned unchanged; their + content is not examined. +2. The header decodes to a JSON object. +3. The payload decodes to a JSON object (the claims set). +4. The header carries `alg`, and its value is a string. +5. `alg` is not `none`. This holds whatever the allowlist says. + As a companion rule, an allowlist that itself names `none` + is an error at the check level: such a context rejects every + token. (Asking to allow `none` is asking for unsecured + tokens; this slice does not accept them under any context.) +6. `alg` is on the allowlist. Names are compared exactly, + character for character: `None` and `hs256` are different + names from `none` and `HS256`. +7. Every required claim is present in the claims set. Presence + is all this rule asks; the value's type does not matter for + this rule. +8. When `exp`, `nbf`, or `iat` is present, its value must be a + JSON number whose value is a whole number of seconds. A + non-number, or a number with a fractional part (for example + `2000000000.5`), turns the token away. This type rule holds + even when no current time is supplied. The value is judged + as an exact decimal, not by its spelling: `2.0e9` is the + whole number 2000000000, and a value like `1e999999999` is + compared exactly, without ever being written out in full. +9. When `exp` is present and a current time is supplied, the + current time must be before `exp`. A current time equal to + `exp` rejects (the token is expired at that second). +10. When `nbf` is present and a current time is supplied, the + current time must be at or after `nbf`. A current time + equal to `nbf` accepts. +11. `iat` carries no comparison rule in this slice; only the + type rule (rule 8) applies to it. +12. When `iss` is present, its value must be a string. +13. When `aud` is present, its value must be a string or an + array of strings (every member a string). +14. When an expected issuer is given, `iss` must be present + and exactly equal to it. A missing `iss` rejects. +15. When an expected audience is given, `aud` must be that + string, or an array holding that string as a member. A + missing `aud` rejects. + +When no current time is supplied, rules 9 and 10 are skipped; +every other rule, including the type rule 8, still applies. + +Names are read from objects with the JSON code's lookup: when a +name appears more than once in an object, the first copy is the +one read. + +## Model and printing + +A token value holds the header JSON value, the claims JSON +value, and the signature bytes. Printing a token prints each +JSON part with the json slice's canonical printer (no spaces, +object pairs in the order held, numbers kept as their source +text, strings escaped in that printer's fixed way), encodes the +text as UTF-8, base64url-encodes without padding, and joins the +three parts with dots, the signature last. + +The main claim, proved in this repo: for a token whose JSON +parts are well formed in the json slice's sense (its `WF`), +parsing the printed token gives the token back +(`Jws.Proofs.parseToken_print`). Under it, the base64url round +trips (both directions, for arbitrary bytes and for every text +the decoder accepts) and the UTF-8 decode-after-encode round +trip are also proved, and the json slice's own parse-after-print +theorem is carried in with its code. + +## The command line front end + +One request per line on stdin, one answer per line on stdout. +A request is a word, a space, and a payload. The payload is +decimal character codes separated by commas. The one operation +is `check`: + +``` +check ;;;;; +``` + +The six fields are separated by semicolons (code 59). Each +field is a text written as character codes, in the same comma +separated decimal form as the payload: + +- Field 1: the token text. +- Field 2: the current time as decimal digits, with an optional + leading minus sign, at most 19 digits. Empty means no current + time (rules 9 and 10 skipped). +- Field 3: the allowlist. The field text is the algorithm names + joined by commas inside the text itself, for example the text + `HS256,RS256`. Empty means no algorithms are allowed. +- Field 4: the required claims, in the same comma joined style. + Empty means no claims are required. +- Field 5: the expected issuer. Empty means none. +- Field 6: the expected audience. Empty means none. + +The answer is `ok:` followed by the character codes of the +canonical reprinted token when the token is accepted, `none` +when it is not accepted, and `error` when the request itself +is malformed (wrong field count, a field that is not a code +list, a code that is not a Unicode scalar value, a current +time field that is not an optional minus sign plus at most 19 +digits, an unknown operation). diff --git a/lake-manifest.json b/lake-manifest.json new file mode 100644 index 0000000..c53f76e --- /dev/null +++ b/lake-manifest.json @@ -0,0 +1,6 @@ +{"version": "1.3.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "jws", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lakefile.toml b/lakefile.toml new file mode 100644 index 0000000..a6ad22a --- /dev/null +++ b/lakefile.toml @@ -0,0 +1,16 @@ +name = "jws" +version = "0.1.0" +defaultTargets = ["Json", "Jws", "Proofs", "jws"] + +[[lean_lib]] +name = "Json" + +[[lean_lib]] +name = "Jws" + +[[lean_lib]] +name = "Proofs" + +[[lean_exe]] +name = "jws" +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..86ca850 --- /dev/null +++ b/tests/TEST-RESULTS.md @@ -0,0 +1,47 @@ +# Test results: JWS compact parser and checker + +Run with `python3 tests/run_tests.py`. The record is +written by the run. Seed 20261026 for the random corpus. +The run happened on 2026-10-26/27. + +## The oracle and PyJWT + +PyJWT 2.15.1 was present (a venv inside the work directory, with cryptography). It built 20 tokens (HS256, RS256, ES256, and none algorithms). +Its unverified decode was compared with the oracle's parse on 20 tokens: 20 agreements, 0 differences. +Verdicts are always the oracle's (SPEC.md rules reimplemented in the harness). PyJWT built well formed tokens and cross checked decoding only. + +## Counts + +- Total check and request inputs: 425 +- Agreements with the oracle: 425 +- Failures: 0 +- Of the verdict cases: 55 accepted, 360 rejected, 10 malformed requests answered error + +## RFC 7515 fixed cases + +The A.5 example is the RFC's unsecured (alg none) compact example; in the final RFC text A.6 and A.7 are JSON Serialization examples, not compact tokens, so the none cases use A.5. The RFC 7519 section 3.1 example token is byte for byte the A.1 token, so it is covered by the A.1 cases. + +- [ok] A.1 accept (HS256 allowed, now before exp, issuer joe) +- [ok] A.1 reject (alg not allowed) +- [ok] A.1 reject (now equal to exp) +- [ok] A.1 reject (now after exp) +- [ok] A.1 reject (wrong issuer) +- [ok] A.1 accept (required claims present) +- [ok] A.1 reject (required claim missing) +- [ok] A.1 accept (no time checks, issuer checked) +- [ok] A.2 accept (RS256 allowed, now before exp, issuer joe) +- [ok] A.2 reject (alg not allowed) +- [ok] A.3 accept (ES256 allowed, now before exp) +- [ok] A.3 reject (now equal to exp) +- [ok] A.5 reject (alg none, HS256 allowed) +- [ok] A.5 reject (alg none, allowlist names none) +- [ok] A.5 reject (alg none, allowlist names none and HS256) + +## Named differences and pinned readings + +- An empty signature part is well formed base64url, so a token with an empty third part can pass the checks. Only alg none itself is turned away, not the empty signature. +- Claim and header name lookup reads the first copy of a repeated name (the JSON code's List.lookup order). The duplicate iss and alg cases pin this. +- The none rule is the exact name `none`. An alg of `None` is a different name and can be allowed. +- Date claims are judged by value, not by spelling: `2.0e9` and `20000000000e-1` are the whole number 2000000000, and `1e999999999` compares without ever being written out. +- PyJWT decode differences (its parser against the oracle's on well formed tokens): 0. + diff --git a/tests/run_tests.py b/tests/run_tests.py new file mode 100644 index 0000000..51fae4e --- /dev/null +++ b/tests/run_tests.py @@ -0,0 +1,918 @@ +#!/usr/bin/env python3 +"""Test harness for the JWS compact parser and checker. + +Three parts, matching the slice plan: + +1. Fixed cases: the RFC 7515 Appendix A examples (A.1 HS256, + A.2 RS256, A.3 ES256, A.5 the unsecured none example; the + RFC 7519 section 3.1 example token is byte for byte the A.1 + token, so the A.1 cases cover it), each with contexts that + accept and contexts that reject. + +2. Differential: tokens built with PyJWT (in the work dir venv) + when it is present, plus hand built tokens, each run under + several check contexts. Every verdict (and, on acceptance, + the canonical reprinted token) is compared against an oracle + that reimplements SPEC.md in Python. PyJWT also cross checks + the parsing: its own unverified decode of each well formed + token is compared with the oracle's parse. + +3. Mutations and malformed requests: padding added, characters + outside the alphabet, two or four parts, a header that is not + an object, alg missing, alg none with an empty signature, + exp equal to now, nbf equal to now, audience arrays that do + and do not hold the expected value, a fractional exp, and + more; plus request lines that must be answered with `error`. + +The oracle is the authority for verdicts. PyJWT never decides a +verdict here: it builds well formed tokens and cross checks +decoding, because its own checks differ from this slice's rules +(it verifies signatures and registered claims its own way when +asked, and accepts some framings this slice turns away). + +Run: python3 tests/run_tests.py (uses .lake/build/bin/jws and +the venv's python when present for the PyJWT corpus). +Writes tests/TEST-RESULTS.md with real counts. +""" + +import base64 +import json +import random +import re +import subprocess +import sys +from decimal import Decimal +from pathlib import Path + +ROOT = Path(__file__).resolve().parent.parent +EXE = ROOT / ".lake" / "build" / "bin" / "jws" +SEED = 20261026 + +# --------------------------------------------------------------- +# The oracle: SPEC.md reimplemented in Python. +# JSON values are tuples mirroring the Lean Json type: +# ('null',) ('bool', b) ('num', source text) ('str', s) +# ('arr', [v ...]) ('obj', [(k, v) ...]) pairs in source order +# --------------------------------------------------------------- + +ALPHABET = set("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789-_") + + +def b64url_decode_strict(part): + """Bytes for a base64url part under the strict rules, or None.""" + if any(ch not in ALPHABET for ch in part): + return None + if len(part) % 4 == 1: + return None + pad = "=" * (-len(part) % 4) + try: + raw = base64.urlsafe_b64decode(part + pad) + except Exception: + return None + # Re-encoding must reproduce the part exactly. This is what + # turns away nonzero unused bits in the final character. + if base64.urlsafe_b64encode(raw).rstrip(b"=").decode() != part: + return None + return raw + + +def b64url_encode(raw): + return base64.urlsafe_b64encode(raw).rstrip(b"=").decode() + + +class BadJson(Exception): + pass + + +def _no_constant(x): + raise BadJson(x) + + +def _walk_check(v): + """Reject lone surrogates anywhere, as the Lean parser does.""" + if isinstance(v, tuple): + tag = v[0] + if tag == "str": + if any(0xD800 <= ord(ch) <= 0xDFFF for ch in v[1]): + raise BadJson("lone surrogate") + elif tag == "arr": + for item in v[1]: + _walk_check(item) + elif tag == "obj": + for k, item in v[1]: + if any(0xD800 <= ord(ch) <= 0xDFFF for ch in k): + raise BadJson("lone surrogate in key") + _walk_check(item) + + +def json_parse(text): + """Parse a JSON text into the tuple form, or None.""" + try: + val = json.loads( + text, + object_pairs_hook=lambda pairs: ("obj", list(pairs)), + parse_int=lambda s: ("num", s), + parse_float=lambda s: ("num", s), + parse_constant=_no_constant, + ) + except Exception: + return None + + def conv(v): + if isinstance(v, tuple): + if v[0] == "obj": + return ("obj", [(k, conv(x)) for (k, x) in v[1]]) + return v + if isinstance(v, list): + return ("arr", [conv(x) for x in v]) + if isinstance(v, str): + return ("str", v) + if isinstance(v, bool): + return ("bool", v) + if v is None: + return ("null",) + raise BadJson("unexpected") + + try: + out = conv(val) + _walk_check(out) + except BadJson: + return None + return out + + +HEX = "0123456789abcdef" + + +def json_print(v): + tag = v[0] + if tag == "null": + return "null" + if tag == "bool": + return "true" if v[1] else "false" + if tag == "num": + return v[1] + if tag == "str": + out = ['"'] + for ch in v[1]: + n = ord(ch) + if ch == '"': + out.append('\\"') + elif ch == "\\": + out.append("\\\\") + elif n == 8: + out.append("\\b") + elif n == 9: + out.append("\\t") + elif n == 10: + out.append("\\n") + elif n == 12: + out.append("\\f") + elif n == 13: + out.append("\\r") + elif n < 32: + out.append("\\u00" + HEX[n // 16] + HEX[n % 16]) + else: + out.append(ch) + out.append('"') + return "".join(out) + if tag == "arr": + return "[" + ",".join(json_print(x) for x in v[1]) + "]" + if tag == "obj": + return "{" + ",".join(json_print(("str", k)) + ":" + json_print(x) + for (k, x) in v[1]) + "}" + raise BadJson(tag) + + +def lookup(name, obj): + """First copy wins, as in the Lean code.""" + if obj[0] != "obj": + return None + for (k, v) in obj[1]: + if k == name: + return v + return None + + +NUM_RE = re.compile(r"^-?(0|[0-9]+)(\.[0-9]+)?([eE][+-]?[0-9]+)?$") + + +def date_claim(claims, name): + """'absent', 'bad', or a Decimal integer value.""" + v = lookup(name, claims) + if v is None: + return "absent" + if v[0] != "num" or not NUM_RE.match(v[1]): + return "bad" + d = Decimal(v[1]) + if d != d.to_integral_value(): + return "bad" + return d + + +def shape_ok(claims): + iss = lookup("iss", claims) + if iss is not None and iss[0] != "str": + return False + aud = lookup("aud", claims) + if aud is not None: + if aud[0] == "str": + pass + elif aud[0] == "arr" and all(x[0] == "str" for x in aud[1]): + pass + else: + return False + return True + + +def oracle_check(token_text, now, allow, required, issuer, audience): + """The canonical reprinted token when accepted, else None. + + now is None for no time comparisons. allow, required are + lists of names. issuer, audience are strings or None.""" + if "none" in allow: + return None + parts = token_text.split(".") + if len(parts) != 3: + return None + raws = [b64url_decode_strict(p) for p in parts] + if any(r is None for r in raws): + return None + try: + header_text = raws[0].decode("utf-8") + claims_text = raws[1].decode("utf-8") + except UnicodeDecodeError: + return None + header = json_parse(header_text) + claims = json_parse(claims_text) + if header is None or claims is None: + return None + if header[0] != "obj" or claims[0] != "obj": + return None + alg = lookup("alg", header) + if alg is None or alg[0] != "str": + return None + if alg[1] == "none" or alg[1] not in allow: + return None + for name in required: + if lookup(name, claims) is None: + return None + for name in ("exp", "nbf", "iat"): + if date_claim(claims, name) == "bad": + return None + if now is not None: + exp = date_claim(claims, "exp") + if exp not in ("absent", "bad") and not (Decimal(now) < exp): + return None + nbf = date_claim(claims, "nbf") + if nbf not in ("absent", "bad") and (Decimal(now) < nbf): + return None + if not shape_ok(claims): + return None + if issuer is not None: + iss = lookup("iss", claims) + if iss is None or iss[0] != "str" or iss[1] != issuer: + return None + if audience is not None: + aud = lookup("aud", claims) + if aud is None: + return None + if aud[0] == "str": + if aud[1] != audience: + return None + elif aud[0] == "arr": + if not any(x[0] == "str" and x[1] == audience for x in aud[1]): + return None + else: + return None + canon = ".".join([ + b64url_encode(json_print(header).encode("utf-8")), + b64url_encode(json_print(claims).encode("utf-8")), + b64url_encode(raws[2]), + ]) + return canon + + +# --------------------------------------------------------------- +# The Lean side: request encoding and the runner. +# --------------------------------------------------------------- + +def codes_of(text): + return ",".join(str(ord(ch)) for ch in text) + + +def check_request(token_text, now, allow, required, issuer, audience): + now_text = "" if now is None else str(now) + allow_text = ",".join(allow) + req_text = ",".join(required) + iss_text = "" if issuer is None else issuer + aud_text = "" if audience is None else audience + fields = [token_text, now_text, allow_text, req_text, iss_text, aud_text] + return "check " + ";".join(codes_of(f) for f in fields) + + +def run_lean(lines): + proc = subprocess.run([str(EXE)], input="\n".join(lines) + "\n", + capture_output=True, text=True, timeout=1200) + if proc.returncode != 0: + raise RuntimeError("lean exe failed: " + proc.stderr[:2000]) + return proc.stdout.splitlines() + + +def decode_answer(ans): + """'ok:' -> token text; 'none' -> None; 'error' -> 'error'.""" + if ans == "none": + return None + if ans == "error": + return "error" + if ans.startswith("ok:"): + body = ans[3:] + if body == "": + return "" + return "".join(chr(int(x)) for x in body.split(",")) + raise ValueError("bad answer: " + ans[:80]) + + +# --------------------------------------------------------------- +# Case collection. Each entry: (name, request line, expected) +# where expected is a token text (accepted, canonical), None +# (rejected), or "error" (malformed request). +# --------------------------------------------------------------- + +CASES = [] + + +def add_check(name, token, now, allow, required, issuer, audience): + want = oracle_check(token, now, allow, required, issuer, audience) + CASES.append((name, check_request(token, now, allow, required, issuer, + audience), want)) + + +def add_raw(name, line, want): + CASES.append((name, line, want)) + + +# --- RFC 7515 Appendix A ------------------------------------- + +PAYLOAD_B64 = ("eyJpc3MiOiJqb2UiLA0KICJleHAiOjEzMDA4MTkzODAsDQogImh0dHA6Ly9" + "leGFtcGxlLmNvbS9pc19yb290Ijp0cnVlfQ") +A1 = ("eyJ0eXAiOiJKV1QiLA0KICJhbGciOiJIUzI1NiJ9." + PAYLOAD_B64 + + ".dBjftJeZ4CVP-mB92K27uhbUJU1p1r_wW1gFWFOEjXk") +A2 = ("eyJhbGciOiJSUzI1NiJ9." + PAYLOAD_B64 + + ".cC4hiUPoj9Eetdgtv3hF80EGrhuB__dzERat0XF9g2VtQgr9PJbu3XOiZj5RZmh7AAuH" + "Im4Bh-0Qc_lF5YKt_O8W2Fp5jujGbds9uJdbF9CUAr7t1dnZcAcQjbKBYNX4BAynRFdiu" + "B--f_nZLgrnbyTyWzO75vRK5h6xBArLIARNPvkSjtQBMHlb1L07Qe7K0GarZRmB_eSN93" + "83LcOLn6_dO--xi12jzDwusC-eOkHWEsqtFZESc6BfI7noOPqvhJ1phCnvWh6IeYI2w9Q" + "OYEUipUTI8np6LbgGY9Fs98rqVt5AXLIhWkWywlVmtVrBp0igcN_IoypGlUPQGe77Rw") +A3 = ("eyJhbGciOiJFUzI1NiJ9." + PAYLOAD_B64 + + ".DtEhU3ljbEg8L38VWAfUAqOyKAM6-Xx-F4GawxaepmXFCgfTjDxw5djxLa8ISlSApmWQ" + "xfKTUJqPP3-Kg6NU1Q") +A5 = "eyJhbGciOiJub25lIn0." + PAYLOAD_B64 + "." + +add_check("A.1 accept (HS256 allowed, now before exp, issuer joe)", + A1, 1300819000, ["HS256"], [], "joe", None) +add_check("A.1 reject (alg not allowed)", A1, 1300819000, ["RS256"], [], + None, None) +add_check("A.1 reject (now equal to exp)", A1, 1300819380, ["HS256"], [], + None, None) +add_check("A.1 reject (now after exp)", A1, 1400000000, ["HS256"], [], + None, None) +add_check("A.1 reject (wrong issuer)", A1, 1300819000, ["HS256"], [], + "bob", None) +add_check("A.1 accept (required claims present)", A1, 1300819000, + ["HS256"], ["exp", "iss"], None, None) +add_check("A.1 reject (required claim missing)", A1, 1300819000, + ["HS256"], ["sub"], None, None) +add_check("A.1 accept (no time checks, issuer checked)", A1, None, + ["HS256"], [], "joe", None) +add_check("A.2 accept (RS256 allowed, now before exp, issuer joe)", + A2, 1300819000, ["RS256"], [], "joe", None) +add_check("A.2 reject (alg not allowed)", A2, 1300819000, ["HS256"], [], + None, None) +add_check("A.3 accept (ES256 allowed, now before exp)", A3, 1300819000, + ["ES256"], [], None, None) +add_check("A.3 reject (now equal to exp)", A3, 1300819380, ["ES256"], [], + None, None) +add_check("A.5 reject (alg none, HS256 allowed)", A5, 1300819000, + ["HS256"], [], None, None) +add_check("A.5 reject (alg none, allowlist names none)", A5, 1300819000, + ["none"], [], None, None) +add_check("A.5 reject (alg none, allowlist names none and HS256)", + A5, 1300819000, ["none", "HS256"], [], None, None) +add_check("HS256 token reject (allowlist names none at all)", A1, + 1300819000, ["none", "HS256"], [], None, None) + +# --- Hand built tokens for mutations -------------------------- + +def hand_token(header_bytes, payload_bytes, sig_bytes): + return ".".join([b64url_encode(header_bytes), + b64url_encode(payload_bytes), + b64url_encode(sig_bytes)]) + + +GOOD_H = b'{"alg":"HS256"}' +GOOD_P = b'{"iss":"joe","exp":2000000000}' +SIG = bytes(range(32)) +BASE = hand_token(GOOD_H, GOOD_P, SIG) +NOW = 1500000000 + +add_check("base accept", BASE, NOW, ["HS256"], [], "joe", None) + +parts = BASE.split(".") +add_check("mutation: padding on header part", + parts[0] + "=." + parts[1] + "." + parts[2], + NOW, ["HS256"], [], None, None) +add_check("mutation: padding on payload part", + parts[0] + "." + parts[1] + "=." + parts[2], + NOW, ["HS256"], [], None, None) +add_check("mutation: padding on signature part", + parts[0] + "." + parts[1] + "." + parts[2] + "=", + NOW, ["HS256"], [], None, None) +add_check("mutation: plus character in signature", + parts[0] + "." + parts[1] + "." + parts[2][:-1] + "+", + NOW, ["HS256"], [], None, None) +add_check("mutation: slash character in payload", + parts[0] + "." + "/" + parts[1][1:] + "." + parts[2], + NOW, ["HS256"], [], None, None) +add_check("mutation: star character in header", + "*" + parts[0][1:] + "." + parts[1] + "." + parts[2], + NOW, ["HS256"], [], None, None) +add_check("mutation: two parts only", parts[0] + "." + parts[1], + NOW, ["HS256"], [], None, None) +add_check("mutation: four parts", BASE + ".AAAA", + NOW, ["HS256"], [], None, None) +add_check("mutation: empty token", "", NOW, ["HS256"], [], None, None) +add_check("mutation: two dots only", "..", NOW, ["HS256"], [], None, None) +add_check("mutation: header part length 1 mod 4", + "AAAAA." + parts[1] + "." + parts[2], + NOW, ["HS256"], [], None, None) +add_check("mutation: signature part length 1 mod 4", + parts[0] + "." + parts[1] + ".AAAAA", + NOW, ["HS256"], [], None, None) +# signature 'AR': last character value 17, unused bits nonzero in a +# two character (one byte) final group. +add_check("mutation: signature unused bits set", + parts[0] + "." + parts[1] + ".AR", + NOW, ["HS256"], [], None, None) +add_check("empty signature part is well formed (accepted)", + parts[0] + "." + parts[1] + ".", + NOW, ["HS256"], [], "joe", None) +add_check("one byte signature (accepted)", + hand_token(GOOD_H, GOOD_P, b"\x01"), + NOW, ["HS256"], [], None, None) + +add_check("mutation: header is an array", + hand_token(b'["HS256"]', GOOD_P, SIG), + NOW, ["HS256"], [], None, None) +add_check("mutation: header is a string", + hand_token(b'"HS256"', GOOD_P, SIG), + NOW, ["HS256"], [], None, None) +add_check("mutation: payload is a number", + hand_token(GOOD_H, b'42', SIG), + NOW, ["HS256"], [], None, None) +add_check("mutation: payload is not JSON", + hand_token(GOOD_H, b'{oops', SIG), + NOW, ["HS256"], [], None, None) +add_check("mutation: header is not UTF-8", + hand_token(b'\xff\xfe{"alg":"HS256"}', GOOD_P, SIG), + NOW, ["HS256"], [], None, None) +add_check("mutation: alg missing", + hand_token(b'{"typ":"JWT"}', GOOD_P, SIG), + NOW, ["HS256"], [], None, None) +add_check("mutation: alg not a string", + hand_token(b'{"alg":256}', GOOD_P, SIG), + NOW, ["HS256"], [], None, None) +add_check("mutation: alg none with a signature present", + hand_token(b'{"alg":"none"}', GOOD_P, SIG), + NOW, ["HS256", "none"], [], None, None) +add_check("alg None capital (case differs, accepted when allowed)", + hand_token(b'{"alg":"None"}', GOOD_P, SIG), + NOW, ["None"], [], None, None) + +def claims_token(claims_bytes, header_bytes=GOOD_H, sig=SIG): + return hand_token(header_bytes, claims_bytes, sig) + +add_check("mutation: exp equal to now (reject)", + claims_token(b'{"exp":1500000000}'), + NOW, ["HS256"], [], None, None) +add_check("mutation: exp one second after now (accept)", + claims_token(b'{"exp":1500000001}'), + NOW, ["HS256"], [], None, None) +add_check("nbf equal to now (accept)", + claims_token(b'{"nbf":1500000000,"exp":2000000000}'), + NOW, ["HS256"], [], None, None) +add_check("mutation: nbf one second after now (reject)", + claims_token(b'{"nbf":1500000001,"exp":2000000000}'), + NOW, ["HS256"], [], None, None) +add_check("mutation: fractional exp (reject)", + claims_token(b'{"exp":2000000000.5}'), + NOW, ["HS256"], [], None, None) +add_check("mutation: fractional exp with no time checks (reject)", + claims_token(b'{"exp":2000000000.5}'), + None, ["HS256"], [], None, None) +add_check("mutation: exp as a string (reject)", + claims_token(b'{"exp":"2000000000"}'), + NOW, ["HS256"], [], None, None) +add_check("exp in exponent form, same value (accept)", + claims_token(b'{"exp":2.0e9}'), + NOW, ["HS256"], [], None, None) +add_check("exp with scaled exponent (accept)", + claims_token(b'{"exp":20000000000e-1}'), + NOW, ["HS256"], [], None, None) +add_check("exp huge exponent text (accept, no bulk)", + claims_token(b'{"exp":1e999999999}'), + NOW, ["HS256"], [], None, None) +add_check("mutation: negative exp, now zero (reject)", + claims_token(b'{"exp":-1}'), + 0, ["HS256"], [], None, None) +add_check("negative now before a small exp (accept)", + claims_token(b'{"exp":100}'), + -5, ["HS256"], [], None, None) +add_check("mutation: fractional iat (reject)", + claims_token(b'{"iat":1.5,"exp":2000000000}'), + NOW, ["HS256"], [], None, None) +add_check("iat whole in exponent form (accept)", + claims_token(b'{"iat":1.5e9,"exp":2000000000}'), + NOW, ["HS256"], [], None, None) +add_check("mutation: nbf as a boolean (reject)", + claims_token(b'{"nbf":true,"exp":2000000000}'), + NOW, ["HS256"], [], None, None) +add_check("mutation: iss a number (reject)", + claims_token(b'{"iss":7,"exp":2000000000}'), + NOW, ["HS256"], [], None, None) +add_check("mutation: aud a number (reject)", + claims_token(b'{"aud":7,"exp":2000000000}'), + NOW, ["HS256"], [], None, None) +add_check("mutation: aud array with a number inside (reject)", + claims_token(b'{"aud":["api",7],"exp":2000000000}'), + NOW, ["HS256"], [], None, None) +add_check("aud array containing the expected value (accept)", + claims_token(b'{"aud":["api","web"],"exp":2000000000}'), + NOW, ["HS256"], [], None, "web") +add_check("mutation: aud array missing the expected value (reject)", + claims_token(b'{"aud":["api","web"],"exp":2000000000}'), + NOW, ["HS256"], [], None, "mobile") +add_check("aud string equal to the expected value (accept)", + claims_token(b'{"aud":"api","exp":2000000000}'), + NOW, ["HS256"], [], None, "api") +add_check("mutation: expected audience, aud missing (reject)", + claims_token(b'{"exp":2000000000}'), + NOW, ["HS256"], [], None, "api") +add_check("mutation: expected issuer, iss missing (reject)", + claims_token(b'{"exp":2000000000}'), + NOW, ["HS256"], [], "joe", None) +add_check("required claim of number type still counts as present", + claims_token(b'{"foo":42,"exp":2000000000}'), + NOW, ["HS256"], ["foo"], None, None) +add_check("duplicate iss: the first copy is the one read (accept joe)", + claims_token(b'{"iss":"joe","iss":"bob","exp":2000000000}'), + NOW, ["HS256"], [], "joe", None) +add_check("duplicate iss: the second copy is not read (reject bob)", + claims_token(b'{"iss":"joe","iss":"bob","exp":2000000000}'), + NOW, ["HS256"], [], "bob", None) +add_check("duplicate alg: the first copy is the one read", + hand_token(b'{"alg":"HS256","alg":"none"}', GOOD_P, SIG), + NOW, ["HS256"], [], None, None) +add_check("payload whitespace and key order kept in the reprint", + claims_token(b'{ "exp" : 2000000000 , "iss" : "joe" }'), + NOW, ["HS256"], [], "joe", None) + +# Unicode handling in strings. +add_check("iss with a raw UTF-8 character (accept)", + claims_token('{"iss":"jé","exp":2000000000}'.encode("utf-8")), + NOW, ["HS256"], [], "jé", None) +add_check("iss with an escaped character, same value (accept)", + claims_token(b'{"iss":"j\\u00e9","exp":2000000000}'), + NOW, ["HS256"], [], "jé", None) +add_check("iss with a surrogate pair escape (accept)", + claims_token(b'{"iss":"\\uD83D\\uDE00","exp":2000000000}'), + NOW, ["HS256"], [], "\U0001F600", None) +add_check("mutation: iss with a lone surrogate escape (reject)", + claims_token(b'{"iss":"\\uD83D","exp":2000000000}'), + NOW, ["HS256"], [], None, None) +add_check("mutation: payload with an overlong UTF-8 lead (reject)", + hand_token(GOOD_H, b'{"iss":"j\xc0\xaf","exp":2000000000}', SIG), + NOW, ["HS256"], [], None, None) + +# --- Malformed requests --------------------------------------- + +add_raw("malformed: unknown operation", "peek " + codes_of(BASE), "error") +add_raw("malformed: five fields", + "check " + ";".join([codes_of(BASE), codes_of("1500000000"), + codes_of("HS256"), "", ""]), "error") +add_raw("malformed: seven fields", + "check " + ";".join([codes_of(BASE), codes_of("1500000000"), + codes_of("HS256"), "", "", "", ""]), "error") +add_raw("malformed: a field that is not numbers", + "check " + ";".join(["1,2,x", "", "", "", "", ""]), "error") +add_raw("malformed: a code above the scalar range", + "check " + ";".join([codes_of(BASE), "1114112", "", "", "", ""]), + "error") +add_raw("malformed: a surrogate code in the token field", + "check " + ";".join(["55296", "", "", "", "", ""]), "error") +add_raw("malformed: now field with letters", + "check " + ";".join([codes_of(BASE), codes_of("12a3"), + codes_of("HS256"), "", "", ""]), "error") +add_raw("malformed: now field over 19 digits", + "check " + ";".join([codes_of(BASE), codes_of("99999999999999999999"), + codes_of("HS256"), "", "", ""]), "error") +add_raw("malformed: empty line", "", "error") +add_raw("malformed: check with no payload", "check", "error") +add_check("now field with a minus sign and digits (read as negative)", + claims_token(b'{"exp":100,"nbf":-50}'), + -5, ["HS256"], [], None, None) + +# --------------------------------------------------------------- +# PyJWT corpus: tokens built by PyJWT when present, contexts +# varied. Verdicts still come from the oracle. PyJWT decode +# (signature check off) cross checks the oracle's parse. +# --------------------------------------------------------------- + +PYJWT_INFO = {"present": False, "version": None, "tokens": 0, + "decode_comparisons": 0, "decode_agreements": 0, + "decode_differences": []} + + +def build_pyjwt_cases(): + venv_python = ROOT / "venv" / "bin" / "python" + if not venv_python.exists(): + return + script = r''' +import json, sys +import jwt +from jwt import __version__ as v +from cryptography.hazmat.primitives.asymmetric import rsa, ec + +out = {"version": v, "tokens": []} +rsa_key = rsa.generate_private_key(public_exponent=65537, key_size=2048) +ec_key = ec.generate_private_key(ec.SECP256R1()) + +payloads = [ + {"iss": "joe", "exp": 2000000000, "nbf": 1400000000, "iat": 1400000000, + "aud": "api", "sub": "user-1"}, + {"iss": "issuer.example", "exp": 2000000000, "aud": ["api", "web"]}, + {"exp": 2000000000}, + {"iss": "joe", "exp": 1200000000, "aud": "api"}, + {"iss": "jé", "exp": 2000000000, "name": "José"}, + {"iss": "joe", "exp": 2000000000, "nbf": 1600000000}, + {"iss": "joe", "exp": 9999999999, "aud": ["a", "b", "c"], "admin": True}, + {"iss": "joe", "exp": 2000000000, "scope": ["read", "write"], "n": 42}, +] +builders = [] +for p in payloads: + builders.append(("HS256", jwt.encode(p, "secret", algorithm="HS256"))) + builders.append(("none", jwt.encode(p, "", algorithm="none"))) +builders.append(("RS256", jwt.encode(payloads[0], rsa_key, algorithm="RS256"))) +builders.append(("RS256", jwt.encode(payloads[1], rsa_key, algorithm="RS256"))) +builders.append(("ES256", jwt.encode(payloads[0], ec_key, algorithm="ES256"))) +builders.append(("ES256", jwt.encode(payloads[6], ec_key, algorithm="ES256"))) +for alg, tok in builders: + decoded = jwt.decode(tok, options={"verify_signature": False}) + header = jwt.get_unverified_header(tok) + out["tokens"].append({"alg": alg, "token": tok, + "header": header, "claims": decoded}) +print(json.dumps(out)) +''' + proc = subprocess.run([str(venv_python), "-c", script], + capture_output=True, text=True, timeout=300) + if proc.returncode != 0: + PYJWT_INFO["error"] = proc.stderr[-500:] + return + data = json.loads(proc.stdout) + PYJWT_INFO["present"] = True + PYJWT_INFO["version"] = data["version"] + random.seed(SEED) + contexts = [ + ("right alg, inside validity", lambda alg: (1500000000, [alg], [], + None, None)), + ("wrong alg", lambda alg: (1500000000, ["HS256"] if alg != "HS256" + else ["RS256"], [], None, None)), + ("issuer and audience set", lambda alg: (1500000000, [alg], [], + "joe", "api")), + ("after the common exp", lambda alg: (2100000000, [alg], [], + None, None)), + ("no time checks", lambda alg: (None, [alg], [], None, None)), + ] + for item in data["tokens"]: + tok = item["token"] + PYJWT_INFO["tokens"] += 1 + # Cross check the oracle parse against PyJWT's decode. + parts = tok.split(".") + header = json_parse(b64url_decode_strict(parts[0]).decode("utf-8")) + claims = json_parse(b64url_decode_strict(parts[1]).decode("utf-8")) + + def plain(v): + if v[0] == "obj": + return {k: plain(x) for (k, x) in v[1]} + if v[0] == "arr": + return [plain(x) for x in v[1]] + if v[0] == "num": + d = Decimal(v[1]) + return int(d) if d == d.to_integral_value() else float(d) + return v[1] + + PYJWT_INFO["decode_comparisons"] += 1 + if plain(header) == item["header"] and plain(claims) == item["claims"]: + PYJWT_INFO["decode_agreements"] += 1 + else: + PYJWT_INFO["decode_differences"].append(tok[:40]) + for label, make in contexts: + now, allow, required, issuer, audience = make(item["alg"]) + if item["alg"] == "none": + allow = ["none"] if "wrong" not in label else ["HS256"] + add_check("pyjwt %s token, %s" % (item["alg"], label), + tok, now, allow, required, issuer, audience) + + +# --------------------------------------------------------------- +# Random differential corpus (oracle builds and settles all). +# --------------------------------------------------------------- + +def build_random_cases(count=240): + rng = random.Random(SEED) + algs = ["HS256", "HS384", "RS256", "ES256", "PS256", "EdDSA", "none", + "None", "hs256"] + issuers = ["joe", "issuer.example", "jé", "api-issuer"] + auds = ["api", "web", "mobile"] + + def rand_claims(): + claims = {} + if rng.random() < 0.8: + claims["iss"] = rng.choice(issuers) + if rng.random() < 0.8: + claims["exp"] = rng.choice( + [1400000000, 1500000000, 1600000000, 2000000000, 9999999999]) + if rng.random() < 0.4: + claims["nbf"] = rng.choice([1400000000, 1500000000, 1600000000]) + if rng.random() < 0.4: + claims["iat"] = rng.choice([1400000000, 1500000000]) + if rng.random() < 0.6: + claims["aud"] = (rng.choice(auds) if rng.random() < 0.5 + else rng.sample(auds, rng.randint(1, 3))) + if rng.random() < 0.3: + claims["sub"] = "user-%d" % rng.randint(1, 99) + return claims + + for i in range(count): + alg = rng.choice(algs) + header = {"alg": alg} + if rng.random() < 0.4: + header["typ"] = "JWT" + if rng.random() < 0.2: + header["kid"] = "key-%d" % rng.randint(1, 5) + claims = rand_claims() + sig = bytes(rng.randrange(256) for _ in range(rng.choice( + [0, 1, 16, 32, 64]))) + tok = hand_token( + json.dumps(header, separators=(",", ":")).encode("utf-8"), + json.dumps(claims, separators=(",", ":"), + ensure_ascii=False).encode("utf-8"), + sig) + now = rng.choice([None, 1450000000, 1500000000, 1550000000, + 1700000000, 2100000000]) + allow = rng.sample(algs, rng.randint(1, 3)) + required = rng.sample(["iss", "exp", "aud", "sub", "nbf"], + rng.randint(0, 2)) + issuer = rng.choice([None, "joe", "issuer.example", "bob"]) + audience = rng.choice([None, "api", "web", "desktop"]) + add_check("random %d (alg %s)" % (i, alg), tok, now, allow, + required, issuer, audience) + + +# --------------------------------------------------------------- +# Run everything and write the record. +# --------------------------------------------------------------- + +def main(): + if not EXE.exists(): + print("executable missing; run lake build first", file=sys.stderr) + return 1 + build_pyjwt_cases() + build_random_cases() + lines = [req for (_, req, _) in CASES] + answers = run_lean(lines) + if len(answers) != len(CASES): + print("answer count mismatch: %d vs %d" % (len(answers), len(CASES)), + file=sys.stderr) + return 1 + failures = [] + accepted = 0 + rejected = 0 + errors = 0 + for (name, _, want), ans in zip(CASES, answers): + try: + got = decode_answer(ans) + except ValueError: + failures.append((name, "unreadable answer " + ans[:60], want)) + continue + if want == "error": + errors += 1 + ok = got == "error" + elif want is None: + rejected += 1 + ok = got is None + else: + accepted += 1 + ok = got == want + if not ok: + failures.append((name, got, want)) + + fixed = [c for c in CASES if c[0].startswith("A.")] + fixed_fail = [f for f in failures if f[0].startswith("A.")] + + lines_out = [] + lines_out.append("# Test results: JWS compact parser and checker") + lines_out.append("") + lines_out.append("Run with `python3 tests/run_tests.py`. The record is") + lines_out.append("written by the run. Seed %d for the random corpus." + % SEED) + lines_out.append("The run happened on 2026-10-26/27.") + lines_out.append("") + lines_out.append("## The oracle and PyJWT") + lines_out.append("") + if PYJWT_INFO["present"]: + lines_out.append("PyJWT %s was present (a venv inside the work" + " directory, with cryptography). It built %d tokens" + " (HS256, RS256, ES256, and none algorithms)." + % (PYJWT_INFO["version"], PYJWT_INFO["tokens"])) + lines_out.append("Its unverified decode was compared with the oracle's" + " parse on %d tokens: %d agreements, %d differences." + % (PYJWT_INFO["decode_comparisons"], + PYJWT_INFO["decode_agreements"], + len(PYJWT_INFO["decode_differences"]))) + elif "error" in PYJWT_INFO: + lines_out.append("PyJWT was attempted in the work directory venv but" + " the builder failed; the oracle built and settled" + " every corpus token. Error: " + + PYJWT_INFO["error"].replace("\n", " ")) + else: + lines_out.append("PyJWT was not present. The oracle built and" + " settled every corpus token.") + lines_out.append("Verdicts are always the oracle's (SPEC.md rules" + " reimplemented in the harness). PyJWT built well" + " formed tokens and cross checked decoding only.") + lines_out.append("") + lines_out.append("## Counts") + lines_out.append("") + lines_out.append("- Total check and request inputs: %d" % len(CASES)) + lines_out.append("- Agreements with the oracle: %d" + % (len(CASES) - len(failures))) + lines_out.append("- Failures: %d" % len(failures)) + lines_out.append("- Of the verdict cases: %d accepted, %d rejected," + " %d malformed requests answered error" + % (accepted, rejected, errors)) + lines_out.append("") + lines_out.append("## RFC 7515 fixed cases") + lines_out.append("") + lines_out.append("The A.5 example is the RFC's unsecured (alg none)" + " compact example; in the final RFC text A.6 and A.7" + " are JSON Serialization examples, not compact" + " tokens, so the none cases use A.5. The RFC 7519" + " section 3.1 example token is byte for byte the" + " A.1 token, so it is covered by the A.1 cases.") + lines_out.append("") + for (name, _, _) in fixed: + mark = "FAIL" if any(f[0] == name for f in fixed_fail) else "ok" + lines_out.append("- [%s] %s" % (mark, name)) + lines_out.append("") + lines_out.append("## Named differences and pinned readings") + lines_out.append("") + lines_out.append("- An empty signature part is well formed base64url," + " so a token with an empty third part can pass the" + " checks. Only alg none itself is turned away, not" + " the empty signature.") + lines_out.append("- Claim and header name lookup reads the first copy" + " of a repeated name (the JSON code's List.lookup" + " order). The duplicate iss and alg cases pin this.") + lines_out.append("- The none rule is the exact name `none`. An alg of" + " `None` is a different name and can be allowed.") + lines_out.append("- Date claims are judged by value, not by spelling:" + " `2.0e9` and `20000000000e-1` are the whole number" + " 2000000000, and `1e999999999` compares without" + " ever being written out.") + lines_out.append("- PyJWT decode differences (its parser against the" + " oracle's on well formed tokens): %d." + % len(PYJWT_INFO["decode_differences"])) + if failures: + lines_out.append("") + lines_out.append("## Failures") + lines_out.append("") + for (name, got, want) in failures: + lines_out.append("- %s: got %r, wanted %r" % (name, got, want)) + lines_out.append("") + text = "\n".join(lines_out) + (ROOT / "tests" / "TEST-RESULTS.md").write_text(text + "\n") + print("cases: %d, agreements: %d, failures: %d" + % (len(CASES), len(CASES) - len(failures), len(failures))) + print("accepted: %d, rejected: %d, error answers: %d" + % (accepted, rejected, errors)) + print("pyjwt present: %s, decode comparisons: %d, agreements: %d" + % (PYJWT_INFO["present"], PYJWT_INFO["decode_comparisons"], + PYJWT_INFO["decode_agreements"])) + for f in failures[:20]: + print("FAIL:", f) + return 0 if not failures else 1 + + +if __name__ == "__main__": + sys.exit(main()) From 593f7d73733a3a22ae17bc03ff75d6525bfc064b Mon Sep 17 00:00:00 2001 From: shah Date: Tue, 27 Oct 2026 19:48:29 -0500 Subject: [PATCH 2/3] Reject an empty signature part at the check, per review --- Jws/Token.lean | 1 + README.md | 2 +- SPEC.md | 50 ++++++++++++++++++++++++------------------- tests/TEST-RESULTS.md | 9 ++++---- tests/run_tests.py | 34 +++++++++++++++++++++++------ 5 files changed, 63 insertions(+), 33 deletions(-) diff --git a/Jws/Token.lean b/Jws/Token.lean index 9a222cc..27c8f34 100644 --- a/Jws/Token.lean +++ b/Jws/Token.lean @@ -257,6 +257,7 @@ def accept (t : Token) (ctx : Context) : Bool := match lookup "alg".toList t.header with | some (.str alg) => alg != "none".toList && + !t.sig.isEmpty && ctx.allow.contains alg && ctx.required.all (fun n => (lookup n t.claims).isSome) && (match dateClaim "exp".toList t.claims with diff --git a/README.md b/README.md index b8a3dc2..2947a8b 100644 --- a/README.md +++ b/README.md @@ -35,7 +35,7 @@ The two base64url round trips check against `propext` and `Quot.sound` only. The Two readings worth naming, both stated in `SPEC.md` and pinned by tests: -- An empty signature part is well formed, so it can pass the checks. Only the algorithm name `none` is turned away outright, together with any context whose allowlist names `none`. +- An empty signature part is well formed base64url, but the checker turns it away: RFC 7515 never produces an empty signature for a signing algorithm, and the algorithm name `none` is turned away outright, together with any context whose allowlist names `none`, so the none case never reaches acceptance. - When a JSON object repeats a name, lookup reads the first copy, as the JSON code's lookup does. ## What you must trust diff --git a/SPEC.md b/SPEC.md index ef172de..cdffc50 100644 --- a/SPEC.md +++ b/SPEC.md @@ -30,7 +30,8 @@ Exactly three parts. Two parts or four parts are turned away. An empty part is allowed by the framing (the empty text is well formed base64url for zero bytes); the checks below decide whether what it decodes to is acceptable. In particular an -empty signature part is well formed. +empty signature part is well formed base64url, and rule 2 +below turns it away at the check. ## Base64url, strict @@ -76,22 +77,27 @@ The token is accepted only when every rule holds: 1. The framing is exactly three parts, each strict base64url (above). The signature bytes are returned unchanged; their - content is not examined. -2. The header decodes to a JSON object. -3. The payload decodes to a JSON object (the claims set). -4. The header carries `alg`, and its value is a string. -5. `alg` is not `none`. This holds whatever the allowlist says. + content is not examined beyond the emptiness rule below. +2. An empty signature part is always turned away. RFC 7515 + never produces an empty signature for a signing algorithm, + and the one algorithm that uses no signature, `none`, is + itself turned away by rule 6, so the none case never + reaches acceptance. +3. The header decodes to a JSON object. +4. The payload decodes to a JSON object (the claims set). +5. The header carries `alg`, and its value is a string. +6. `alg` is not `none`. This holds whatever the allowlist says. As a companion rule, an allowlist that itself names `none` is an error at the check level: such a context rejects every token. (Asking to allow `none` is asking for unsecured tokens; this slice does not accept them under any context.) -6. `alg` is on the allowlist. Names are compared exactly, +7. `alg` is on the allowlist. Names are compared exactly, character for character: `None` and `hs256` are different names from `none` and `HS256`. -7. Every required claim is present in the claims set. Presence +8. Every required claim is present in the claims set. Presence is all this rule asks; the value's type does not matter for this rule. -8. When `exp`, `nbf`, or `iat` is present, its value must be a +9. When `exp`, `nbf`, or `iat` is present, its value must be a JSON number whose value is a whole number of seconds. A non-number, or a number with a fractional part (for example `2000000000.5`), turns the token away. This type rule holds @@ -99,25 +105,25 @@ The token is accepted only when every rule holds: as an exact decimal, not by its spelling: `2.0e9` is the whole number 2000000000, and a value like `1e999999999` is compared exactly, without ever being written out in full. -9. When `exp` is present and a current time is supplied, the - current time must be before `exp`. A current time equal to - `exp` rejects (the token is expired at that second). -10. When `nbf` is present and a current time is supplied, the +10. When `exp` is present and a current time is supplied, the + current time must be before `exp`. A current time equal to + `exp` rejects (the token is expired at that second). +11. When `nbf` is present and a current time is supplied, the current time must be at or after `nbf`. A current time equal to `nbf` accepts. -11. `iat` carries no comparison rule in this slice; only the - type rule (rule 8) applies to it. -12. When `iss` is present, its value must be a string. -13. When `aud` is present, its value must be a string or an +12. `iat` carries no comparison rule in this slice; only the + type rule (rule 9) applies to it. +13. When `iss` is present, its value must be a string. +14. When `aud` is present, its value must be a string or an array of strings (every member a string). -14. When an expected issuer is given, `iss` must be present +15. When an expected issuer is given, `iss` must be present and exactly equal to it. A missing `iss` rejects. -15. When an expected audience is given, `aud` must be that +16. When an expected audience is given, `aud` must be that string, or an array holding that string as a member. A missing `aud` rejects. -When no current time is supplied, rules 9 and 10 are skipped; -every other rule, including the type rule 8, still applies. +When no current time is supplied, rules 10 and 11 are skipped; +every other rule, including the type rule 9, still applies. Names are read from objects with the JSON code's lookup: when a name appears more than once in an object, the first copy is the @@ -160,7 +166,7 @@ separated decimal form as the payload: - Field 1: the token text. - Field 2: the current time as decimal digits, with an optional leading minus sign, at most 19 digits. Empty means no current - time (rules 9 and 10 skipped). + time (rules 10 and 11 skipped). - Field 3: the allowlist. The field text is the algorithm names joined by commas inside the text itself, for example the text `HS256,RS256`. Empty means no algorithms are allowed. diff --git a/tests/TEST-RESULTS.md b/tests/TEST-RESULTS.md index 86ca850..0ed6e30 100644 --- a/tests/TEST-RESULTS.md +++ b/tests/TEST-RESULTS.md @@ -12,10 +12,10 @@ Verdicts are always the oracle's (SPEC.md rules reimplemented in the harness). P ## Counts -- Total check and request inputs: 425 -- Agreements with the oracle: 425 +- Total check and request inputs: 426 +- Agreements with the oracle: 426 - Failures: 0 -- Of the verdict cases: 55 accepted, 360 rejected, 10 malformed requests answered error +- Of the verdict cases: 53 accepted, 363 rejected, 10 malformed requests answered error ## RFC 7515 fixed cases @@ -29,6 +29,7 @@ The A.5 example is the RFC's unsecured (alg none) compact example; in the final - [ok] A.1 accept (required claims present) - [ok] A.1 reject (required claim missing) - [ok] A.1 accept (no time checks, issuer checked) +- [ok] A.1 reject (signature part emptied, otherwise passing context) - [ok] A.2 accept (RS256 allowed, now before exp, issuer joe) - [ok] A.2 reject (alg not allowed) - [ok] A.3 accept (ES256 allowed, now before exp) @@ -39,7 +40,7 @@ The A.5 example is the RFC's unsecured (alg none) compact example; in the final ## Named differences and pinned readings -- An empty signature part is well formed base64url, so a token with an empty third part can pass the checks. Only alg none itself is turned away, not the empty signature. +- Named change from the 2026-10-27 review: an empty signature part is now always turned away (SPEC rule 2). RFC 7515 never produces an empty signature for a signing algorithm, and alg none is turned away on its own, so the none case never reaches acceptance. The earlier reading accepted an empty signature part for a signing algorithm. The fixed case that pinned that reading now expects rejection, a new fixed case empties the A.1 token's signature part under an otherwise passing context and expects rejection, and generated corpus tokens with empty signature parts follow the same new rule in the oracle. - Claim and header name lookup reads the first copy of a repeated name (the JSON code's List.lookup order). The duplicate iss and alg cases pin this. - The none rule is the exact name `none`. An alg of `None` is a different name and can be allowed. - Date claims are judged by value, not by spelling: `2.0e9` and `20000000000e-1` are the whole number 2000000000, and `1e999999999` compares without ever being written out. diff --git a/tests/run_tests.py b/tests/run_tests.py index 51fae4e..c22d2e1 100644 --- a/tests/run_tests.py +++ b/tests/run_tests.py @@ -7,7 +7,9 @@ A.2 RS256, A.3 ES256, A.5 the unsecured none example; the RFC 7519 section 3.1 example token is byte for byte the A.1 token, so the A.1 cases cover it), each with contexts that - accept and contexts that reject. + accept and contexts that reject. The A.1 token with its + signature part emptied, under an otherwise passing context, + is a fixed reject case. 2. Differential: tokens built with PyJWT (in the work dir venv) when it is present, plus hand built tokens, each run under @@ -238,6 +240,11 @@ def oracle_check(token_text, now, allow, required, issuer, audience): raws = [b64url_decode_strict(p) for p in parts] if any(r is None for r in raws): return None + if len(raws[2]) == 0: + # An empty signature part is always turned away (SPEC + # rule 2): no signing algorithm produces one, and alg + # none is turned away on its own below. + return None try: header_text = raws[0].decode("utf-8") claims_text = raws[1].decode("utf-8") @@ -385,6 +392,10 @@ def add_raw(name, line, want): ["HS256"], ["sub"], None, None) add_check("A.1 accept (no time checks, issuer checked)", A1, None, ["HS256"], [], "joe", None) +A1_EMPTY_SIG = A1.rsplit(".", 1)[0] + "." +add_check("A.1 reject (signature part emptied, otherwise passing" + " context)", A1_EMPTY_SIG, 1300819000, ["HS256"], [], + "joe", None) add_check("A.2 accept (RS256 allowed, now before exp, issuer joe)", A2, 1300819000, ["RS256"], [], "joe", None) add_check("A.2 reject (alg not allowed)", A2, 1300819000, ["HS256"], [], @@ -454,7 +465,9 @@ def hand_token(header_bytes, payload_bytes, sig_bytes): add_check("mutation: signature unused bits set", parts[0] + "." + parts[1] + ".AR", NOW, ["HS256"], [], None, None) -add_check("empty signature part is well formed (accepted)", +add_check("empty signature part (reject; this case pinned the" + " earlier reading as an accept, flipped by the" + " 2026-10-27 review change)", parts[0] + "." + parts[1] + ".", NOW, ["HS256"], [], "joe", None) add_check("one byte signature (accepted)", @@ -877,10 +890,19 @@ def main(): lines_out.append("") lines_out.append("## Named differences and pinned readings") lines_out.append("") - lines_out.append("- An empty signature part is well formed base64url," - " so a token with an empty third part can pass the" - " checks. Only alg none itself is turned away, not" - " the empty signature.") + lines_out.append("- Named change from the 2026-10-27 review: an" + " empty signature part is now always turned away" + " (SPEC rule 2). RFC 7515 never produces an empty" + " signature for a signing algorithm, and alg none" + " is turned away on its own, so the none case" + " never reaches acceptance. The earlier reading" + " accepted an empty signature part for a signing" + " algorithm. The fixed case that pinned that" + " reading now expects rejection, a new fixed case" + " empties the A.1 token's signature part under an" + " otherwise passing context and expects rejection," + " and generated corpus tokens with empty signature" + " parts follow the same new rule in the oracle.") lines_out.append("- Claim and header name lookup reads the first copy" " of a repeated name (the JSON code's List.lookup" " order). The duplicate iss and alg cases pin this.") From a1c8467fb2be646e7c26e987a357f76b854f4ff1 Mon Sep 17 00:00:00 2001 From: shah Date: Tue, 27 Oct 2026 20:38:48 -0500 Subject: [PATCH 3/3] Add the bar file set: Spec.lean, comparator.json, bar.toml, CI workflow --- .github/workflows/bar.yml | 21 ++++ Proofs.lean | 1 + Proofs/SpecProofs.lean | 114 ++++++++++++++++++ README.md | 240 +++++++++++++++++++++++++++++--------- SPEC.md | 24 ++++ Spec.lean | 159 +++++++++++++++++++++++++ bar.toml | 62 ++++++++++ comparator.json | 1 + lakefile.toml | 3 + 9 files changed, 571 insertions(+), 54 deletions(-) create mode 100644 .github/workflows/bar.yml create mode 100644 Proofs/SpecProofs.lean create mode 100644 Spec.lean create mode 100644 bar.toml create mode 100644 comparator.json diff --git a/.github/workflows/bar.yml b/.github/workflows/bar.yml new file mode 100644 index 0000000..32457ed --- /dev/null +++ b/.github/workflows/bar.yml @@ -0,0 +1,21 @@ +name: verified bar + +on: + push: + pull_request: + # Rerun when the spec reviewer approves, or an approval is dismissed. + pull_request_review: + types: [submitted, dismissed] + +jobs: + bar: + # pull-requests: read lets the check confirm the spec approval on GitHub. + permissions: + contents: read + pull-requests: read + # Both lines pin the same commit of Proven-Commons/mission: bar v2, as + # proposed in its pull request #2. Move both to a release tag once + # mission publishes one. + uses: Proven-Commons/mission/.github/workflows/verified-bar.yml@6ba85c27abaaf07905c9316aa96dc29f7b5847a2 + with: + bar-ref: 6ba85c27abaaf07905c9316aa96dc29f7b5847a2 diff --git a/Proofs.lean b/Proofs.lean index 8a82bf6..e363d86 100644 --- a/Proofs.lean +++ b/Proofs.lean @@ -2,3 +2,4 @@ import Proofs.RoundTrip import Proofs.B64 import Proofs.Utf8 import Proofs.Token +import Proofs.SpecProofs diff --git a/Proofs/SpecProofs.lean b/Proofs/SpecProofs.lean new file mode 100644 index 0000000..b6cc346 --- /dev/null +++ b/Proofs/SpecProofs.lean @@ -0,0 +1,114 @@ +/- + Proofs of the statements in `Spec.lean`, under the same + names. + + The round trips are the theorems proved in + `Proofs/Token.lean` and `Proofs/B64.lean`. The single + tokens are checked in the kernel with `decide +kernel`: no + native evaluation, which the bar forbids. +-/ + +import Jws +import Proofs.Token +import Proofs.B64 + +open Jws + +theorem Spec.parseToken_print (t : Token) (hh : Json.WF t.header) + (hc : Json.WF t.claims) : + parseToken (printToken t) = some t := + Jws.Proofs.parseToken_print t hh hc + +theorem Spec.decode_encode (bs : List UInt8) : + Base64url.decode (Base64url.encode bs) = some bs := + Jws.Base64url.Proofs.decode_encode bs + + +theorem Spec.accepts_rfc_a1 : + (match parseToken + "eyJ0eXAiOiJKV1QiLA0KICJhbGciOiJIUzI1NiJ9.eyJpc3MiOiJqb2UiLA0KICJleHAiOjEzMDA4MTkzODAsDQogImh0dHA6Ly9leGFtcGxlLmNvbS9pc19yb290Ijp0cnVlfQ.dBjftJeZ4CVP-mB92K27uhbUJU1p1r_wW1gFWFOEjXk".toList with + | some t => accept t + { allow := ["HS256".toList], now := none, required := [], + issuer := some "joe".toList, audience := none } + | none => false) = true := by + decide +kernel + + +theorem Spec.accepts_hand_built : + (match parseToken + "eyJhbGciOiJIUzI1NiJ9.eyJpc3MiOiJqb2UiLCJleHAiOjIwMDAwMDAwMDB9.AAECAwQFBgcICQoLDA0ODxAREhMUFRYXGBkaGxwdHh8".toList with + | some t => accept t + { allow := ["HS256".toList], now := some 1500000000, + required := [], issuer := some "joe".toList, + audience := none } + | none => false) = true := by + decide +kernel + + +theorem Spec.rejects_unsecured_none : + (match parseToken + "eyJhbGciOiJub25lIn0.eyJpc3MiOiJqb2UiLA0KICJleHAiOjEzMDA4MTkzODAsDQogImh0dHA6Ly9leGFtcGxlLmNvbS9pc19yb290Ijp0cnVlfQ.".toList with + | some t => accept t + { allow := ["HS256".toList], now := some 1300819000, + required := [], issuer := none, audience := none } + | none => false) = false := by + decide +kernel + + +theorem Spec.rejects_unsecured_none_when_allowlist_names_none : + (match parseToken + "eyJhbGciOiJub25lIn0.eyJpc3MiOiJqb2UiLA0KICJleHAiOjEzMDA4MTkzODAsDQogImh0dHA6Ly9leGFtcGxlLmNvbS9pc19yb290Ijp0cnVlfQ.".toList with + | some t => accept t + { allow := ["none".toList], now := some 1300819000, + required := [], issuer := none, audience := none } + | none => false) = false := by + decide +kernel + + +theorem Spec.rejects_unsecured_none_when_allowlist_mixes_none : + (match parseToken + "eyJhbGciOiJub25lIn0.eyJpc3MiOiJqb2UiLA0KICJleHAiOjEzMDA4MTkzODAsDQogImh0dHA6Ly9leGFtcGxlLmNvbS9pc19yb290Ijp0cnVlfQ.".toList with + | some t => accept t + { allow := ["none".toList, "HS256".toList], + now := some 1300819000, required := [], issuer := none, + audience := none } + | none => false) = false := by + decide +kernel + + +theorem Spec.rejects_empty_signature : + (match parseToken + "eyJ0eXAiOiJKV1QiLA0KICJhbGciOiJIUzI1NiJ9.eyJpc3MiOiJqb2UiLA0KICJleHAiOjEzMDA4MTkzODAsDQogImh0dHA6Ly9leGFtcGxlLmNvbS9pc19yb290Ijp0cnVlfQ.".toList with + | some t => accept t + { allow := ["HS256".toList], now := some 1300819000, + required := [], issuer := some "joe".toList, + audience := none } + | none => false) = false := by + decide +kernel + + +theorem Spec.rejects_alg_outside_allowlist : + (match parseToken + "eyJ0eXAiOiJKV1QiLA0KICJhbGciOiJIUzI1NiJ9.eyJpc3MiOiJqb2UiLA0KICJleHAiOjEzMDA4MTkzODAsDQogImh0dHA6Ly9leGFtcGxlLmNvbS9pc19yb290Ijp0cnVlfQ.dBjftJeZ4CVP-mB92K27uhbUJU1p1r_wW1gFWFOEjXk".toList with + | some t => accept t + { allow := ["RS256".toList], now := some 1300819000, + required := [], issuer := none, audience := none } + | none => false) = false := by + decide +kernel + + +theorem Spec.rejects_part_not_base64url : + (parseToken + "eyJhbGciOiJIUzI1NiJ9=.eyJpc3MiOiJqb2UiLCJleHAiOjIwMDAwMDAwMDB9.AAECAwQFBgcICQoLDA0ODxAREhMUFRYXGBkaGxwdHh8".toList).isSome + = false := by + decide +kernel + + +theorem Spec.rejects_header_not_object : + (match parseToken + "WyJIUzI1NiJd.eyJpc3MiOiJqb2UiLCJleHAiOjIwMDAwMDAwMDB9.AAECAwQFBgcICQoLDA0ODxAREhMUFRYXGBkaGxwdHh8".toList with + | some t => accept t + { allow := ["HS256".toList], now := some 1500000000, + required := [], issuer := none, audience := none } + | none => false) = false := by + decide +kernel diff --git a/README.md b/README.md index 2947a8b..f4adb6c 100644 --- a/README.md +++ b/README.md @@ -1,72 +1,204 @@ # jws: a JWS compact parser and checker, with a proved round trip -A parser and checker for the JWS compact form (RFC 7515) in Lean, with the plan's main claim proved: printing a parsed token gives the token back. The parser reads the three base64url parts, decodes the header and payload as JSON, and holds the signature bytes unchanged. The checker runs the shape and claims rules of `SPEC.md` (algorithm allowlist, required claims, and the `exp`, `nbf`, `iss`, and `aud` claims against a caller supplied context). Tests run the RFC 7515 Appendix A examples and a differential corpus against an oracle implementing the same rules; see `tests/TEST-RESULTS.md` for the counts. +Status: in-progress + +A parser and checker for the JWS compact form (RFC 7515) +in Lean. The parser reads the three base64url parts, +decodes the header and payload as JSON, and holds the +signature bytes unchanged. The checker runs the shape and +claims rules of `SPEC.md`: the algorithm against a caller +allowlist, the required claims, and the `exp`, `nbf`, +`iss`, and `aud` claims against a context the caller +supplies. The definitions are in `Jws/Base64url.lean` (the +base64url codec), `Jws/Utf8.lean` (a strict UTF-8 codec), +and `Jws/Token.lean` (the framing, the claims reading, and +the checker). The JSON parser, printer, value type, and +round trip proof are the json repo's, carried in unchanged +under `Json/` and `Proofs/RoundTrip.lean`, because the +repos in this org do not import each other. The rules are +written out in `SPEC.md`. + +The statements a reviewer approves are in `Spec.lean`, +with their proofs in `Proofs/SpecProofs.lean`. No reviewer +has approved them yet, so this project is not called +verified. + +One limit stands up front: this slice does not verify a +signature. A token that passes every check is well formed +and its claims are consistent with the check context; it +is not thereby verified, and it must never be described as +a verified token on its own. Signature verification is +the second slice. + +## How to run it + +`lake build` builds the libraries, the proofs, and the +command line tool. The tool reads one request per line: +the word `check`, a space, and six fields separated by +semicolons. Each field is text written as comma separated +decimal character codes: the token text, the current time +(or empty for no time comparisons), the allowed +algorithms, the required claims, the expected issuer, and +the expected audience. It answers `ok:` and the codes of +the canonical reprinted token when the token is accepted, +`none` when it is not, and `error` when the request itself +is malformed. `SPEC.md` states the field format in full. -Status: in progress. The first slice from plan issue 1 has landed locally. The specification has not yet been approved by a reviewer apart from its author, and no statement file (`Spec.lean`) has been added by a reviewer, so this is not verified. - -## Limit, stated up front - -This slice does not verify a signature. It must never be described as a verified token on its own. Signature verification is the second slice. A caller that reads claims from this slice without verifying the signature has not checked authenticity. - -## Where the JSON code came from +``` +lake build +python3 tests/run_tests.py +``` -The JSON parser, printer, value type, and round trip proof are the json repo's, carried in unchanged under `Json/` and `Proofs/RoundTrip.lean` (the repos in this org do not import each other). Everything else is new here: the base64url codec (`Jws/Base64url.lean`), a strict UTF-8 codec (`Jws/Utf8.lean`), and the token framing, claims reading, and checker (`Jws/Token.lean`). The base64url code follows the shape of the codec repo's Base64 work, with the URL safe alphabet and no padding. +`python3 tests/run_tests.py` runs the fixed RFC 7515 +Appendix A cases, the mutation cases, the malformed +request cases, and the differential corpus against an +oracle implementing the same rules (with tokens built by +PyJWT when the work directory venv is present), and +writes the counts to `tests/TEST-RESULTS.md`. ## What is proved +Each claim below names the theorem behind it. The +theorems are stated in `Spec.lean` (the challenge file, +where they end in `sorry`) and proved in +`Proofs/SpecProofs.lean`, under the same names. +`comparator.json` lists all of them. + | Claim | Theorem | |-------|---------| -| Parsing the printed form of a token gives the token back, for tokens whose JSON parts are well formed in the json slice's sense. | `Jws.Proofs.parseToken_print` | -| Decoding the base64url encoding of any bytes gives the bytes back. | `Jws.Base64url.Proofs.decode_encode` | -| Encoding the decoding of any text the decoder accepts gives the text back. | `Jws.Base64url.Proofs.encode_decode` | -| Decoding the UTF-8 encoding of any text gives the text back. | `Jws.Utf8.Proofs.decode_encode` | -| Parsing the canonical printed form of a well formed JSON value gives the value back (carried in with the JSON code). | `Json.Proofs.parse_print` | - -The two base64url round trips check against `propext` and `Quot.sound` only. The token and UTF-8 round trips check against the standard three (`propext`, `Classical.choice`, `Quot.sound`). A reader can confirm with `#print axioms` on each name. +| Parsing the printed form of a token gives the token back, for tokens whose JSON parts are well formed in the json slice's sense. | `Spec.parseToken_print` | +| Decoding the base64url encoding of any bytes gives the bytes back. | `Spec.decode_encode` | +| The RFC 7515 A.1 token is accepted when HS256 is allowed and the issuer must be `joe`, with no current time supplied. | `Spec.accepts_rfc_a1` | +| A hand built token with header `{"alg":"HS256"}`, claims `{"iss":"joe","exp":2000000000}`, and a 32 byte signature is accepted under HS256 allowed, current time 1500000000, and issuer `joe`. | `Spec.accepts_hand_built` | +| The RFC 7515 A.5 unsecured token (algorithm `none`, empty signature part) is refused when HS256 is the allowed algorithm. | `Spec.rejects_unsecured_none` | +| The A.5 token is refused when the allowlist itself names `none`: such a context refuses every token. | `Spec.rejects_unsecured_none_when_allowlist_names_none` | +| The A.5 token is refused when the allowlist names `none` alongside HS256. | `Spec.rejects_unsecured_none_when_allowlist_mixes_none` | +| The A.1 token with its signature part emptied is refused, under a context that accepts the token as it stands. | `Spec.rejects_empty_signature` | +| The A.1 token is refused when its algorithm, HS256, is outside the allowlist (RS256 alone). | `Spec.rejects_alg_outside_allowlist` | +| A token whose first part carries a padding character does not parse: `=` is not in the base64url alphabet. | `Spec.rejects_part_not_base64url` | +| A token whose header part decodes to a JSON array, not an object, is refused. | `Spec.rejects_header_not_object` | + +The token round trip rests on the proofs in +`Proofs/Token.lean`, where it is +`Jws.Proofs.parseToken_print`: a chain of the three round +trips under it, the JSON text round trip +(`Json.Proofs.parse_print`, carried in with the JSON +code), the UTF-8 round trip +(`Jws.Utf8.Proofs.decode_encode`, in `Proofs/Utf8.lean`), +and the base64url round trip. The base64url layer proves +both directions: `Spec.decode_encode` above, and the +reverse, encoding a decoding gives the text back +(`Jws.Base64url.Proofs.encode_decode`, in +`Proofs/B64.lean`). The single token theorems are single +inputs checked in the kernel with `decide +kernel`, each +one a named fixed case in the test harness, run through +the same `Jws.parseToken` and `Jws.accept` the command +line tool calls. + +The token and UTF-8 round trips check against the +standard three axioms only (`propext`, `Classical.choice`, +`Quot.sound`), and the base64url round trips against +`propext` and `Quot.sound` only, which a reader can +confirm with `#print axioms` on each name. + +The command line tool in `Main.lean` calls +`Jws.parseToken`, `Jws.accept`, and `Jws.printToken` +directly, the same functions the theorems are about. ## What is not proved -- That the checker accepts exactly the tokens `SPEC.md` says it should. The acceptance rules live in one function (`Jws.accept`) and their completeness rests on the tests: the RFC examples, the mutation cases, and the differential corpus against the harness oracle. -- Signature verification, as stated above: nothing about keys, signing inputs, or any algorithm. -- The reverse printing direction at the token level (printing a parsed token is how the round trip is stated; the base64url and JSON layers each prove their own reverse directions). -- Anything about the numeric meaning of claims beyond the exact decimal reading the checker itself uses (whole seconds, comparisons). The reading code is exercised by the tests, including exponent spellings and very large exponents. -- Reading requests and printing answers in `Main.lean`: line splitting, the field format, the decimal code reading. The tests cover them, malformed requests included. -- Speed. The code works on lists, which suits proofs, not large tokens. - -Two readings worth naming, both stated in `SPEC.md` and pinned by tests: - -- An empty signature part is well formed base64url, but the checker turns it away: RFC 7515 never produces an empty signature for a signing algorithm, and the algorithm name `none` is turned away outright, together with any context whose allowlist names `none`, so the none case never reaches acceptance. -- When a JSON object repeats a name, lookup reads the first copy, as the JSON code's lookup does. +- That the checker accepts exactly the tokens `SPEC.md` + says it should, beyond the single inputs the theorems + above pin. The acceptance rules live in one function + (`Jws.accept`), and their completeness rests on the + tests: the RFC examples, the mutation cases, and the + differential corpus against the harness oracle. +- Signature verification, as stated above: nothing about + keys, signing inputs, or any algorithm. A caller that + reads claims from this slice without verifying the + signature has not checked authenticity. +- The reverse printing direction at the token level: + printing a parsed token is how the round trip is + stated. The base64url and JSON layers each prove their + own reverse directions. +- Anything about the numeric meaning of claims beyond + the exact decimal reading the checker itself uses + (whole seconds, comparisons). The reading code is + exercised by the tests, including exponent spellings + and very large exponents. +- Reading requests and printing answers in `Main.lean`: + line splitting, the field format, the decimal code + reading. The tests cover them, malformed requests + included. +- Speed. The code works on lists, which suits proofs, + not large tokens. + +Two readings worth naming, both stated in `SPEC.md` and +pinned by tests: + +- An empty signature part is well formed base64url, but + the checker turns it away: RFC 7515 never produces an + empty signature for a signing algorithm, and the + algorithm name `none` is turned away outright, together + with any context whose allowlist names `none`, so the + none case never reaches acceptance. The theorem + `Spec.rejects_empty_signature` pins the emptied + signature on the RFC's own A.1 token. +- When a JSON object repeats a name, lookup reads the + first copy, as the JSON code's lookup does. ## What you must trust -- The Lean kernel, which checks the proofs. -- The Lean compiler, with the C compiler and linker shipped with it, and the runtime, which turn the proved definitions into the program that runs. -- Lean's core library, including the compiled code it puts in place of some definitions the proofs reason about. -- The operating system and hardware it runs on. -- For the tests: Python's standard library (the oracle's JSON reading and exact decimals), PyJWT and cryptography in the test venv when present (token building and decode cross checks only; verdicts never come from PyJWT), and the RFC 7515 text for the fixed examples. The results file names the versions used. - -This project has no dependencies beyond Lean itself. The test harness's PyJWT corpus is optional and lives in a venv inside the work directory. - -## Run it - -Needs Linux and [elan](https://github.com/leanprover/elan). Build, then feed request lines to the tool: - -``` -lake build -python3 tests/run_tests.py -``` - -A request is one `check` line; `SPEC.md` states the field format in full. The token text, the current time, the allowlist, the required claims, the expected issuer, and the expected audience are the six fields, each written as comma separated decimal character codes, the fields separated by semicolons. The answer is `ok:` and the codes of the canonical reprinted token, `none` when the token is not accepted, and `error` when the request is malformed. +- The Lean kernel (Lean 4.35.0, pinned in + `lean-toolchain`), which checks every proof. +- The Lean compiler, with the C compiler and linker + shipped with it, which turns the proved definitions + into the program that runs. +- The Lean runtime, which runs that program. +- The hardware the program runs on. +- Every dependency in `lake-manifest.json`: the manifest + lists no packages, so there are no library dependencies + to trust beyond the Lean toolchain itself. +- Lean's core library, including the compiled code it + puts in place of some definitions the proofs reason + about. +- The operating system the program runs on. +- That `SPEC.md` states the reading of RFC 7515 you + intend. The proofs are about the parser and checker in + this repo following the statements exactly; the + fidelity of the spec to the RFC is a reading, pinned + in `SPEC.md` where the RFC leaves a choice open. +- The oracle in `tests/run_tests.py`, written from + `SPEC.md`, and PyJWT and cryptography in the test venv + when present. Both are evidence, not proof: PyJWT + builds well formed tokens and cross checks decoding + only, and verdicts never come from PyJWT. The results + file names the versions used. +- The line handling in `Main.lean` (splitting a request + line, reading the six fields and their decimal codes, + and the partial IO loop that reads lines until the + input ends). No statement depends on any of it, and + the tests drive it. +- There are no exceptions to item 4 of the bar: the + project uses none of the features it forbids. ## Re-check it -Needs Linux, elan, and Python 3.11 or later. - -``` -lake build -grep -rn "sorry" --include="*.lean" Json Jws Proofs Main.lean Json.lean Jws.lean Proofs.lean -python3 tests/run_tests.py -``` - -The grep should print nothing: there is no `sorry` anywhere. The test script runs the fixed RFC cases, the mutation cases, the malformed request cases, and the differential corpus (PyJWT built tokens when the venv is present, plus a seeded random corpus), and writes the counts to `tests/TEST-RESULTS.md`. +1. `lake comparator --paranoid`: builds the challenge + file `Spec.lean` and the proofs in a sandbox and + checks that each theorem named in `comparator.json` + proves exactly the statement in the challenge file, + uses no axiom but the three standard ones, and is + accepted by Lean's kernel and every other kernel + shipped with Lean. +2. `python3 tests/run_tests.py`: the fixed RFC cases, + the mutation cases, the malformed request cases, and + the differential corpus, with counts and any failures + written to `tests/TEST-RESULTS.md`. The harness uses + the PyJWT library from the virtual environment in the + work directory (`venv`) when it is there, and says so + in the results file when it is not. +3. `lake build`: the libraries, the proofs, and the tool + build clean. +4. Read `SPEC.md` against RFC 7515 and check the pinned + readings are the ones you want. diff --git a/SPEC.md b/SPEC.md index cdffc50..23ae3e3 100644 --- a/SPEC.md +++ b/SPEC.md @@ -182,3 +182,27 @@ is malformed (wrong field count, a field that is not a code list, a code that is not a Unicode scalar value, a current time field that is not an optional minus sign plus at most 19 digits, an unknown operation). + +## Properties and their theorems + +Each property a reader can check in the page (`README.md`) +names its theorem. The theorems are stated in `Spec.lean` +and proved in `Proofs/SpecProofs.lean`. The single token +theorems are single inputs, one for each named fixed case +in the test harness, run through the same `Jws.parseToken` +and `Jws.accept` the command line tool calls; the tests in +`tests/` cover each rule on many more inputs. + +| Property | Theorem | +|----------|---------| +| Parsing the printed form of a token gives the token back, for well formed JSON parts | `Spec.parseToken_print` | +| Decoding a base64url encoding gives the bytes back | `Spec.decode_encode` | +| The RFC 7515 A.1 token is accepted under its allowlist with no time checks and the issuer checked | `Spec.accepts_rfc_a1` | +| The harness's hand built token is accepted under its base context | `Spec.accepts_hand_built` | +| The RFC 7515 A.5 unsecured token is refused under an HS256 allowlist | `Spec.rejects_unsecured_none` | +| The A.5 token is refused when the allowlist names `none` | `Spec.rejects_unsecured_none_when_allowlist_names_none` | +| The A.5 token is refused when the allowlist names `none` alongside HS256 | `Spec.rejects_unsecured_none_when_allowlist_mixes_none` | +| A token with an empty signature part is refused (rule 2) | `Spec.rejects_empty_signature` | +| A token whose algorithm is outside the allowlist is refused (rule 7) | `Spec.rejects_alg_outside_allowlist` | +| A token with a part that is not strict base64url does not parse | `Spec.rejects_part_not_base64url` | +| A token whose header is not a JSON object is refused (rule 3) | `Spec.rejects_header_not_object` | diff --git a/Spec.lean b/Spec.lean new file mode 100644 index 0000000..487a848 --- /dev/null +++ b/Spec.lean @@ -0,0 +1,159 @@ +/- + The specification as Lean statements: the challenge file. + + A reviewer who did not write this file approves it, and + `bar.toml` records the SHA-256 it had then. The proofs live + in `Proofs` (`Proofs/SpecProofs.lean`); `lake comparator` + checks that each one proves exactly the statement written + here. The `sorry` below is expected in this file only. + + The statements use only the definitions in `Jws/Token.lean`, + `Jws/Base64url.lean`, `Jws/Utf8.lean`, and the JSON code + carried into this repo (`Json/Value.lean` and + `Json/Parse.lean`), the code under proof named in + `bar.toml`. No definition of their own is needed, so this + project has no `Spec/Defs.lean`. +-/ + +import Jws + +open Jws + +/-! ## The round trips + +The statements the slice stands on. Each one is the statement +of the proved theorem of the same shape in `Proofs`. -/ + +/-- Parsing the printed form of a token gives the token back, + for tokens whose JSON parts are well formed in the JSON + slice's sense. So a printer that wrote nothing, or wrote + something shorter, fails this statement. -/ +theorem Spec.parseToken_print (t : Token) (hh : Json.WF t.header) + (hc : Json.WF t.claims) : + parseToken (printToken t) = some t := sorry + +/-- Decoding the base64url encoding of any bytes gives the + bytes back. -/ +theorem Spec.decode_encode (bs : List UInt8) : + Base64url.decode (Base64url.encode bs) = some bs := sorry + +/-! ## Single tokens, accepted and refused + +Single inputs run through the same two entry points the +command line tool calls, `parseToken` and `accept`, each with +the context the test harness gives that case. Each input is +one of the named fixed cases in the test harness. The +differential tests cover these rules on many more inputs; +these statements pin them so a reader of the specification +can check each rule against one concrete case. -/ + +/-- The RFC 7515 A.1 token is accepted when HS256 is allowed + and the issuer must be `joe`, with no current time + supplied, so the time comparisons are skipped and the type + rules still hold. The harness case is "A.1 accept (no time + checks, issuer checked)". -/ +theorem Spec.accepts_rfc_a1 : + (match parseToken + "eyJ0eXAiOiJKV1QiLA0KICJhbGciOiJIUzI1NiJ9.eyJpc3MiOiJqb2UiLA0KICJleHAiOjEzMDA4MTkzODAsDQogImh0dHA6Ly9leGFtcGxlLmNvbS9pc19yb290Ijp0cnVlfQ.dBjftJeZ4CVP-mB92K27uhbUJU1p1r_wW1gFWFOEjXk".toList with + | some t => accept t + { allow := ["HS256".toList], now := none, required := [], + issuer := some "joe".toList, audience := none } + | none => false) = true := sorry + +/-- A hand built token is accepted: header `{"alg":"HS256"}`, + claims `{"iss":"joe","exp":2000000000}`, a 32 byte + signature, HS256 allowed, the current time 1500000000 + before the expiry, and the issuer required to be `joe`. + The harness case is "base accept". -/ +theorem Spec.accepts_hand_built : + (match parseToken + "eyJhbGciOiJIUzI1NiJ9.eyJpc3MiOiJqb2UiLCJleHAiOjIwMDAwMDAwMDB9.AAECAwQFBgcICQoLDA0ODxAREhMUFRYXGBkaGxwdHh8".toList with + | some t => accept t + { allow := ["HS256".toList], now := some 1500000000, + required := [], issuer := some "joe".toList, + audience := none } + | none => false) = true := sorry + +/-- The RFC 7515 A.5 unsecured token (algorithm `none`, empty + signature part) is refused when HS256 is the allowed + algorithm. The harness case is "A.5 reject (alg none, + HS256 allowed)". -/ +theorem Spec.rejects_unsecured_none : + (match parseToken + "eyJhbGciOiJub25lIn0.eyJpc3MiOiJqb2UiLA0KICJleHAiOjEzMDA4MTkzODAsDQogImh0dHA6Ly9leGFtcGxlLmNvbS9pc19yb290Ijp0cnVlfQ.".toList with + | some t => accept t + { allow := ["HS256".toList], now := some 1300819000, + required := [], issuer := none, audience := none } + | none => false) = false := sorry + +/-- The A.5 token is refused when the allowlist itself names + `none`: such a context refuses every token. The harness + case is "A.5 reject (alg none, allowlist names none)". -/ +theorem Spec.rejects_unsecured_none_when_allowlist_names_none : + (match parseToken + "eyJhbGciOiJub25lIn0.eyJpc3MiOiJqb2UiLA0KICJleHAiOjEzMDA4MTkzODAsDQogImh0dHA6Ly9leGFtcGxlLmNvbS9pc19yb290Ijp0cnVlfQ.".toList with + | some t => accept t + { allow := ["none".toList], now := some 1300819000, + required := [], issuer := none, audience := none } + | none => false) = false := sorry + +/-- The A.5 token is refused when the allowlist names `none` + alongside HS256. The harness case is "A.5 reject (alg + none, allowlist names none and HS256)". -/ +theorem Spec.rejects_unsecured_none_when_allowlist_mixes_none : + (match parseToken + "eyJhbGciOiJub25lIn0.eyJpc3MiOiJqb2UiLA0KICJleHAiOjEzMDA4MTkzODAsDQogImh0dHA6Ly9leGFtcGxlLmNvbS9pc19yb290Ijp0cnVlfQ.".toList with + | some t => accept t + { allow := ["none".toList, "HS256".toList], + now := some 1300819000, required := [], issuer := none, + audience := none } + | none => false) = false := sorry + +/-- The A.1 token with its signature part emptied is refused, + under a context that accepts the token as it stands: + HS256 allowed, the current time before the expiry, the + issuer required to be `joe`. The harness case is "A.1 + reject (signature part emptied, otherwise passing + context)", the case the 2026-10-27 review change pinned. -/ +theorem Spec.rejects_empty_signature : + (match parseToken + "eyJ0eXAiOiJKV1QiLA0KICJhbGciOiJIUzI1NiJ9.eyJpc3MiOiJqb2UiLA0KICJleHAiOjEzMDA4MTkzODAsDQogImh0dHA6Ly9leGFtcGxlLmNvbS9pc19yb290Ijp0cnVlfQ.".toList with + | some t => accept t + { allow := ["HS256".toList], now := some 1300819000, + required := [], issuer := some "joe".toList, + audience := none } + | none => false) = false := sorry + +/-- The A.1 token is refused when its algorithm, HS256, is + outside the allowlist, here RS256 alone. The harness case + is "A.1 reject (alg not allowed)". -/ +theorem Spec.rejects_alg_outside_allowlist : + (match parseToken + "eyJ0eXAiOiJKV1QiLA0KICJhbGciOiJIUzI1NiJ9.eyJpc3MiOiJqb2UiLA0KICJleHAiOjEzMDA4MTkzODAsDQogImh0dHA6Ly9leGFtcGxlLmNvbS9pc19yb290Ijp0cnVlfQ.dBjftJeZ4CVP-mB92K27uhbUJU1p1r_wW1gFWFOEjXk".toList with + | some t => accept t + { allow := ["RS256".toList], now := some 1300819000, + required := [], issuer := none, audience := none } + | none => false) = false := sorry + +/-- A token whose first part carries a padding character does + not parse at all: `=` is not in the base64url alphabet, + and padding is not part of the compact form. The harness + case is "mutation: padding on header part", built on its + hand built token. -/ +theorem Spec.rejects_part_not_base64url : + (parseToken + "eyJhbGciOiJIUzI1NiJ9=.eyJpc3MiOiJqb2UiLCJleHAiOjIwMDAwMDAwMDB9.AAECAwQFBgcICQoLDA0ODxAREhMUFRYXGBkaGxwdHh8".toList).isSome + = false := sorry + +/-- A token whose protected (header) part decodes to a JSON + array, not an object, is refused: the header `["HS256"]` + on the harness's hand built payload and signature, under + its base context. The harness case is "mutation: header + is an array". -/ +theorem Spec.rejects_header_not_object : + (match parseToken + "WyJIUzI1NiJd.eyJpc3MiOiJqb2UiLCJleHAiOjIwMDAwMDAwMDB9.AAECAwQFBgcICQoLDA0ODxAREhMUFRYXGBkaGxwdHh8".toList with + | some t => accept t + { allow := ["HS256".toList], now := some 1500000000, + required := [], issuer := none, audience := none } + | none => false) = false := sorry diff --git a/bar.toml b/bar.toml new file mode 100644 index 0000000..612ad77 --- /dev/null +++ b/bar.toml @@ -0,0 +1,62 @@ +# Read by bar/check.py in Proven-Commons/mission. +# See playbook/verified-bar.md there for what each field means. + +[project] +name = "jws" +# "in-progress" until every bar item passes, then "verified". +status = "in-progress" +page = "README.md" +# GitHub handles of everyone who wrote the specification. +spec_authors = ["abu-aska"] +# The program people run. A change to it voids the approval. +entry_points = ["Main.lean"] + +[spec] +files = ["SPEC.md", "Spec.lean"] +# The code under proof: the functions the statements are about. +code = [ + # The token value. + "Jws.Token", + # The framing: split and join at the dots, the printer, the parser. + "Jws.splitSep", "Jws.joinSep", "Jws.printToken", "Jws.parseToken", + # The exact decimal reading of claim numbers, which the check uses. + "Jws.NumVal", "Jws.digitsVal", "Jws.strip", "Jws.mkNumVal", + "Jws.numVal", "Jws.NumVal.isInt", "Jws.NumVal.ofInt", + "Jws.numDigits", "Jws.magCmp", "Jws.NumVal.cmp", + # The check: the context, the claim reading, the accept function. + "Jws.Context", "Jws.ClaimDate", "Jws.ClaimDate.absent", + "Jws.ClaimDate.bad", "Jws.ClaimDate.ok", "Jws.lookup", + "Jws.dateClaim", "Jws.issShapeOk", "Jws.audShapeOk", "Jws.audOk", + "Jws.accept", + # Base64url, strict, no padding. + "Jws.Base64url.char", "Jws.Base64url.encode", "Jws.Base64url.value", + "Jws.Base64url.decode", + # The strict UTF-8 layer the header and payload pass through. + "Jws.Utf8.encodeChar", "Jws.Utf8.encode", "Jws.Utf8.contVal", + "Jws.Utf8.decode", + # The JSON value the token parts hold, its printer, and its + # well formedness, all carried in from the json slice. + "Json.Json", "Json.Json.null", "Json.Json.bool", "Json.Json.num", + "Json.Json.str", "Json.Json.arr", "Json.Json.obj", + "Json.hexDigits", "Json.hexDigit", "Json.escape", "Json.escapeAll", + "Json.printStr", "Json.join", "Json.print", "Json.printPair", + "Json.IsDigit", "Json.FracOk", "Json.ExpOk", "Json.WFNum", "Json.WF", + # The JSON reader the token parser calls. + "Json.isWs", "Json.skipWs", "Json.isDigit", "Json.hexVal", + "Json.simpleEscape", "Json.parseStrBody", "Json.takeDigits", + "Json.parseIntPart", "Json.parseFracOpt", "Json.parseExpOpt", + "Json.parseNumber", "Json.parseValue", "Json.parseEls", + "Json.parseObjEls", "Json.parse", +] + +# One entry per approval, added in a pull request the reviewer approves. +# [[spec.approval]] +# reviewer = "github-handle" +# date = "2026-11-02" +# sha256 = "..." +# record = "https://github.com/Proven-Commons/jws/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..2f9f809 --- /dev/null +++ b/comparator.json @@ -0,0 +1 @@ +{"challenge_module":"Spec","permitted_axioms":["propext","Classical.choice","Quot.sound"],"solution_module":"Proofs","theorem_names":["Spec.parseToken_print","Spec.decode_encode","Spec.accepts_rfc_a1","Spec.accepts_hand_built","Spec.rejects_unsecured_none","Spec.rejects_unsecured_none_when_allowlist_names_none","Spec.rejects_unsecured_none_when_allowlist_mixes_none","Spec.rejects_empty_signature","Spec.rejects_alg_outside_allowlist","Spec.rejects_part_not_base64url","Spec.rejects_header_not_object"]} \ No newline at end of file diff --git a/lakefile.toml b/lakefile.toml index a6ad22a..53e281c 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -11,6 +11,9 @@ name = "Jws" [[lean_lib]] name = "Proofs" +[[lean_lib]] +name = "Spec" + [[lean_exe]] name = "jws" root = "Main"