From f56278b8f0997ac9c65e23b0156b2ee721c21687 Mon Sep 17 00:00:00 2001 From: orda-aska Date: Thu, 29 Oct 2026 20:05:45 +0000 Subject: [PATCH] Move the spec and proof modules and spec names under Json Spec becomes Json.Spec and Proofs becomes Json.Proofs, with the files moved under Json/. The statement names in comparator.json, Json/Spec.lean and Json/Proofs/SpecProofs.lean take the Json. prefix, and bar.toml, lakefile.toml, the README, SPEC.md and the test harness follow the new paths. Part of Proven-Commons/mission#22. This redoes the earlier move on top of main, which since gained the statement file, comparator.json and bar.toml from json#3. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01QwrvNdsMA6RtgKxXn1Pmhf --- Json/Proofs.lean | 3 ++ {Proofs => Json/Proofs}/NumRoundTrip.lean | 2 +- {Proofs => Json/Proofs}/RoundTrip.lean | 0 {Proofs => Json/Proofs}/SpecProofs.lean | 40 ++++++++++----------- {Proofs => Json/Proofs}/Verify.lean | 4 +-- Spec.lean => Json/Spec.lean | 42 +++++++++++------------ Json/Value.lean | 2 +- Proofs.lean | 3 -- README.md | 42 +++++++++++------------ SPEC.md | 36 +++++++++---------- bar.toml | 2 +- comparator.json | 2 +- lakefile.toml | 8 +++-- tests/TEST-RESULTS.md | 2 +- tests/run_tests.py | 10 +++--- 15 files changed, 100 insertions(+), 98 deletions(-) create mode 100644 Json/Proofs.lean rename {Proofs => Json/Proofs}/NumRoundTrip.lean (99%) rename {Proofs => Json/Proofs}/RoundTrip.lean (100%) rename {Proofs => Json/Proofs}/SpecProofs.lean (61%) rename {Proofs => Json/Proofs}/Verify.lean (89%) rename Spec.lean => Json/Spec.lean (77%) delete mode 100644 Proofs.lean diff --git a/Json/Proofs.lean b/Json/Proofs.lean new file mode 100644 index 0000000..78db15b --- /dev/null +++ b/Json/Proofs.lean @@ -0,0 +1,3 @@ +import Json.Proofs.RoundTrip +import Json.Proofs.NumRoundTrip +import Json.Proofs.SpecProofs diff --git a/Proofs/NumRoundTrip.lean b/Json/Proofs/NumRoundTrip.lean similarity index 99% rename from Proofs/NumRoundTrip.lean rename to Json/Proofs/NumRoundTrip.lean index ab9df7e..5325684 100644 --- a/Proofs/NumRoundTrip.lean +++ b/Json/Proofs/NumRoundTrip.lean @@ -22,7 +22,7 @@ -/ import Json -import Proofs.RoundTrip +import Json.Proofs.RoundTrip namespace Json.NumProofs diff --git a/Proofs/RoundTrip.lean b/Json/Proofs/RoundTrip.lean similarity index 100% rename from Proofs/RoundTrip.lean rename to Json/Proofs/RoundTrip.lean diff --git a/Proofs/SpecProofs.lean b/Json/Proofs/SpecProofs.lean similarity index 61% rename from Proofs/SpecProofs.lean rename to Json/Proofs/SpecProofs.lean index c741053..7f2afe1 100644 --- a/Proofs/SpecProofs.lean +++ b/Json/Proofs/SpecProofs.lean @@ -1,94 +1,94 @@ /- - Proofs of the statements in `Spec.lean`, under the same names. + Proofs of the statements in `Json/Spec.lean`, under the same names. The five claims are the theorems proved in - `Proofs/RoundTrip.lean` and `Proofs/NumRoundTrip.lean`. The + `Json/Proofs/RoundTrip.lean` and `Json/Proofs/NumRoundTrip.lean`. The refusals are single inputs, checked in the kernel with `decide +kernel`: no native evaluation, which the bar forbids. -/ import Json -import Proofs.RoundTrip -import Proofs.NumRoundTrip +import Json.Proofs.RoundTrip +import Json.Proofs.NumRoundTrip open Json -theorem Spec.parse_print {v : Json} (hv : WF v) : +theorem Json.Spec.parse_print {v : Json} (hv : WF v) : parse (print v) = some v := Json.Proofs.parse_print hv -theorem Spec.read_print {v : DecVal} (hv : WFVal v) : +theorem Json.Spec.read_print {v : DecVal} (hv : WFVal v) : readNumber (printVal v) = some v := Json.NumProofs.read_print hv -theorem Spec.readNumber_wf {cs : List Char} {v : DecVal} +theorem Json.Spec.readNumber_wf {cs : List Char} {v : DecVal} (h : readNumber cs = some v) : WFVal v := Json.NumProofs.readNumber_wf h -theorem Spec.read_print_of_read {cs : List Char} {v : DecVal} +theorem Json.Spec.read_print_of_read {cs : List Char} {v : DecVal} (h : readNumber cs = some v) : readNumber (printVal v) = some v := Json.NumProofs.read_print_of_read h -theorem Spec.canonical_eq_of_value_eq {t1 t2 : List Char} +theorem Json.Spec.canonical_eq_of_value_eq {t1 t2 : List Char} {v : DecVal} (h1 : readNumber t1 = some v) (h2 : readNumber t2 = some v) : canonicalText t1 = canonicalText t2 := Json.NumProofs.canonical_eq_of_value_eq h1 h2 -theorem Spec.rejects_trailing_after_value : +theorem Json.Spec.rejects_trailing_after_value : (parse (['1', ' ', 'x'] : List Char)).isSome = false := by decide +kernel -theorem Spec.rejects_bad_literal : +theorem Json.Spec.rejects_bad_literal : (parse (['t', 'r', 'u', 'x'] : List Char)).isSome = false := by decide +kernel -theorem Spec.rejects_leading_zero_in_document : +theorem Json.Spec.rejects_leading_zero_in_document : (parse (['0', '1'] : List Char)).isSome = false := by decide +kernel -theorem Spec.rejects_num_lone_minus : +theorem Json.Spec.rejects_num_lone_minus : (readNumber (['-'] : List Char)).isSome = false := by decide +kernel -theorem Spec.rejects_num_leading_zero : +theorem Json.Spec.rejects_num_leading_zero : (readNumber (['0', '1'] : List Char)).isSome = false := by decide +kernel -theorem Spec.rejects_num_trailing_point : +theorem Json.Spec.rejects_num_trailing_point : (readNumber (['1', '.'] : List Char)).isSome = false := by decide +kernel -theorem Spec.rejects_num_leading_point : +theorem Json.Spec.rejects_num_leading_point : (readNumber (['.', '5'] : List Char)).isSome = false := by decide +kernel -theorem Spec.rejects_num_bare_exponent : +theorem Json.Spec.rejects_num_bare_exponent : (readNumber (['1', 'e'] : List Char)).isSome = false := by decide +kernel -theorem Spec.rejects_num_exponent_sign_only : +theorem Json.Spec.rejects_num_exponent_sign_only : (readNumber (['1', 'e', '+'] : List Char)).isSome = false := by decide +kernel -theorem Spec.rejects_num_leading_plus : +theorem Json.Spec.rejects_num_leading_plus : (readNumber (['+', '1'] : List Char)).isSome = false := by decide +kernel -theorem Spec.rejects_num_nondigit : +theorem Json.Spec.rejects_num_nondigit : (readNumber (['1', 'a'] : List Char)).isSome = false := by decide +kernel diff --git a/Proofs/Verify.lean b/Json/Proofs/Verify.lean similarity index 89% rename from Proofs/Verify.lean rename to Json/Proofs/Verify.lean index 15e5b06..edc8e40 100644 --- a/Proofs/Verify.lean +++ b/Json/Proofs/Verify.lean @@ -6,8 +6,8 @@ other name here breaks the verified bar. -/ -import Proofs.RoundTrip -import Proofs.NumRoundTrip +import Json.Proofs.RoundTrip +import Json.Proofs.NumRoundTrip #print axioms Json.Proofs.parse_print #print axioms Json.NumProofs.read_print diff --git a/Spec.lean b/Json/Spec.lean similarity index 77% rename from Spec.lean rename to Json/Spec.lean index 05870d0..fc71480 100644 --- a/Spec.lean +++ b/Json/Spec.lean @@ -2,15 +2,15 @@ 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 + records the SHA-256 it had then. The proofs live in `Json.Proofs` + (`Json/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 `Json/Value.lean`, `Json/Parse.lean`, and `Json/Number.lean`, the code under proof named in `bar.toml`. No definition of their own is needed, so - this project has no `Spec/Defs.lean`. + this project has no `Json/Spec/Defs.lean`. -/ import Json @@ -20,40 +20,40 @@ open Json /-! ## The document round trip The headline claim of the first slice, the statement of -`Json.Proofs.parse_print` in `Proofs/RoundTrip.lean`, over the +`Json.Proofs.parse_print` in `Json/Proofs/RoundTrip.lean`, over the same well formedness predicate, `Json.WF`. -/ /-- Parsing the printed form of a well formed value gives the value back. So a printer that wrote nothing, or wrote something shorter, fails this statement. -/ -theorem Spec.parse_print {v : Json} (hv : WF v) : +theorem Json.Spec.parse_print {v : Json} (hv : WF v) : parse (print v) = some v := sorry /-! ## The number value layer The claims of the second slice, the statements of the theorems -of the same names in `Proofs/NumRoundTrip.lean`, over the +of the same names in `Json/Proofs/NumRoundTrip.lean`, over the canonical form predicate, `Json.WFVal`. -/ /-- Reading the canonical text of a well formed decimal value gives the value back. -/ -theorem Spec.read_print {v : DecVal} (hv : WFVal v) : +theorem Json.Spec.read_print {v : DecVal} (hv : WFVal v) : readNumber (printVal v) = some v := sorry /-- Every value the number reader returns is well formed: canonical zero, or a significand with no trailing zero. -/ -theorem Spec.readNumber_wf {cs : List Char} {v : DecVal} +theorem Json.Spec.readNumber_wf {cs : List Char} {v : DecVal} (h : readNumber cs = some v) : WFVal v := sorry /-- The canonical text of a text's value re-reads to that value. -/ -theorem Spec.read_print_of_read {cs : List Char} {v : DecVal} +theorem Json.Spec.read_print_of_read {cs : List Char} {v : DecVal} (h : readNumber cs = some v) : readNumber (printVal v) = some v := sorry /-- Two texts with the same value have the same canonical text. -/ -theorem Spec.canonical_eq_of_value_eq {t1 t2 : List Char} +theorem Json.Spec.canonical_eq_of_value_eq {t1 t2 : List Char} {v : DecVal} (h1 : readNumber t1 = some v) (h2 : readNumber t2 = some v) : canonicalText t1 = canonicalText t2 := sorry @@ -69,12 +69,12 @@ each rule against one concrete case. -/ /-- Characters standing after a complete value, past the whitespace the grammar allows, are refused: here `1 x`. -/ -theorem Spec.rejects_trailing_after_value : +theorem Json.Spec.rejects_trailing_after_value : (parse (['1', ' ', 'x'] : List Char)).isSome = false := sorry /-- A literal that is none of `true`, `false`, and `null` is refused: here `trux`. -/ -theorem Spec.rejects_bad_literal : +theorem Json.Spec.rejects_bad_literal : (parse (['t', 'r', 'u', 'x'] : List Char)).isSome = false := sorry @@ -82,7 +82,7 @@ theorem Spec.rejects_bad_literal : here `01`, where the zero alone is the whole integer part the grammar allows, and the `1` is left standing after the value. -/ -theorem Spec.rejects_leading_zero_in_document : +theorem Json.Spec.rejects_leading_zero_in_document : (parse (['0', '1'] : List Char)).isSome = false := sorry /-! ## Refused inputs: number texts @@ -93,39 +93,39 @@ rejection set in the test harness (`NUM_REJECTIONS` in /-- A bare minus sign is refused: a sign with no digits is not a number. -/ -theorem Spec.rejects_num_lone_minus : +theorem Json.Spec.rejects_num_lone_minus : (readNumber (['-'] : List Char)).isSome = false := sorry /-- A leading zero is refused: here `01`. -/ -theorem Spec.rejects_num_leading_zero : +theorem Json.Spec.rejects_num_leading_zero : (readNumber (['0', '1'] : List Char)).isSome = false := sorry /-- A point with no digit after it is refused: here `1.`. -/ -theorem Spec.rejects_num_trailing_point : +theorem Json.Spec.rejects_num_trailing_point : (readNumber (['1', '.'] : List Char)).isSome = false := sorry /-- A point with no integer part before it is refused: here `.5`. -/ -theorem Spec.rejects_num_leading_point : +theorem Json.Spec.rejects_num_leading_point : (readNumber (['.', '5'] : List Char)).isSome = false := sorry /-- An exponent letter with no digits after it is refused: here `1e`. -/ -theorem Spec.rejects_num_bare_exponent : +theorem Json.Spec.rejects_num_bare_exponent : (readNumber (['1', 'e'] : List Char)).isSome = false := sorry /-- An exponent sign with no digits after it is refused: here `1e+`. -/ -theorem Spec.rejects_num_exponent_sign_only : +theorem Json.Spec.rejects_num_exponent_sign_only : (readNumber (['1', 'e', '+'] : List Char)).isSome = false := sorry /-- A leading plus sign is refused: the grammar allows a minus only. Here `+1`. -/ -theorem Spec.rejects_num_leading_plus : +theorem Json.Spec.rejects_num_leading_plus : (readNumber (['+', '1'] : List Char)).isSome = false := sorry /-- A letter standing where a digit must be is refused: here `1a`, where the `a` is left over after the number part. -/ -theorem Spec.rejects_num_nondigit : +theorem Json.Spec.rejects_num_nondigit : (readNumber (['1', 'a'] : List Char)).isSome = false := sorry diff --git a/Json/Value.lean b/Json/Value.lean index 01711c0..754782e 100644 --- a/Json/Value.lean +++ b/Json/Value.lean @@ -1,6 +1,6 @@ /- The JSON value type, the canonical printer, and the well formed - predicate that the round trip proof in `Proofs` uses. + predicate that the round trip proof in `Json.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. diff --git a/Proofs.lean b/Proofs.lean deleted file mode 100644 index 70be0e6..0000000 --- a/Proofs.lean +++ /dev/null @@ -1,3 +0,0 @@ -import Proofs.RoundTrip -import Proofs.NumRoundTrip -import Proofs.SpecProofs diff --git a/README.md b/README.md index 6a54929..f04826f 100644 --- a/README.md +++ b/README.md @@ -4,7 +4,7 @@ Status: in-progress A JSON parser and printer in Lean, following RFC 8259. The parser reads a JSON text into a value; the printer writes a value back in one fixed canonical form, with no spaces, object keys in the order held, and strings escaped by fixed rules. The main claim is proved: parsing what the printer wrote returns the same value. Slice 2 adds a number value layer: a single number text can be read as an exact decimal value, held in a canonical normalized form, and printed back as one canonical text in plain notation. Its round trip is proved too. The definitions are in `Json/Value.lean` (the value type, the printer, and the well-formedness rules), `Json/Parse.lean` (the parser), and `Json/Number.lean` (the decimal value, its reader, and its canonical printer). 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. +The statements a reviewer approves are in `Json/Spec.lean`, with their proofs in `Json/Proofs/SpecProofs.lean`. No reviewer has approved them yet, so this project is not called verified. ## How to run it @@ -21,30 +21,30 @@ That request is the text `["a"]` as character codes, and the answer is `ok:91,34 ## 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. +Each claim below names the theorem behind it. The theorems are stated in `Json/Spec.lean` (the challenge file, where they end in `sorry`) and proved in `Json/Proofs/SpecProofs.lean`, under the same names. `comparator.json` lists all of them. | Claim | Theorem | |-------|---------| -| Parsing the printed form of a well formed value gives the value back. | `Spec.parse_print` | -| Reading the canonical text of a well formed decimal value gives the value back. | `Spec.read_print` | -| Every value the number reader returns is well formed (canonical zero, or a significand with no trailing zero). | `Spec.readNumber_wf` | -| The canonical text of a text's value re-reads to that value. | `Spec.read_print_of_read` | -| Two texts with the same value have the same canonical text. | `Spec.canonical_eq_of_value_eq` | -| Characters standing after a complete value, past the whitespace the grammar allows, are refused: the text `1 x`. | `Spec.rejects_trailing_after_value` | -| A literal that is none of `true`, `false`, and `null` is refused: the text `trux`. | `Spec.rejects_bad_literal` | -| A number with a leading zero inside a document is refused: the text `01`. | `Spec.rejects_leading_zero_in_document` | -| A bare minus sign is refused as a number text: the text `-`. | `Spec.rejects_num_lone_minus` | -| A number text with a leading zero is refused: the text `01`. | `Spec.rejects_num_leading_zero` | -| A number text ending in a point with no digit after it is refused: the text `1.`. | `Spec.rejects_num_trailing_point` | -| A number text with a point and no integer part before it is refused: the text `.5`. | `Spec.rejects_num_leading_point` | -| A number text whose exponent letter has no digits after it is refused: the text `1e`. | `Spec.rejects_num_bare_exponent` | -| A number text whose exponent sign has no digits after it is refused: the text `1e+`. | `Spec.rejects_num_exponent_sign_only` | -| A number text with a leading plus sign is refused: the text `+1`. | `Spec.rejects_num_leading_plus` | -| A number text with a letter where a digit must stand is refused: the text `1a`. | `Spec.rejects_num_nondigit` | +| Parsing the printed form of a well formed value gives the value back. | `Json.Spec.parse_print` | +| Reading the canonical text of a well formed decimal value gives the value back. | `Json.Spec.read_print` | +| Every value the number reader returns is well formed (canonical zero, or a significand with no trailing zero). | `Json.Spec.readNumber_wf` | +| The canonical text of a text's value re-reads to that value. | `Json.Spec.read_print_of_read` | +| Two texts with the same value have the same canonical text. | `Json.Spec.canonical_eq_of_value_eq` | +| Characters standing after a complete value, past the whitespace the grammar allows, are refused: the text `1 x`. | `Json.Spec.rejects_trailing_after_value` | +| A literal that is none of `true`, `false`, and `null` is refused: the text `trux`. | `Json.Spec.rejects_bad_literal` | +| A number with a leading zero inside a document is refused: the text `01`. | `Json.Spec.rejects_leading_zero_in_document` | +| A bare minus sign is refused as a number text: the text `-`. | `Json.Spec.rejects_num_lone_minus` | +| A number text with a leading zero is refused: the text `01`. | `Json.Spec.rejects_num_leading_zero` | +| A number text ending in a point with no digit after it is refused: the text `1.`. | `Json.Spec.rejects_num_trailing_point` | +| A number text with a point and no integer part before it is refused: the text `.5`. | `Json.Spec.rejects_num_leading_point` | +| A number text whose exponent letter has no digits after it is refused: the text `1e`. | `Json.Spec.rejects_num_bare_exponent` | +| A number text whose exponent sign has no digits after it is refused: the text `1e+`. | `Json.Spec.rejects_num_exponent_sign_only` | +| A number text with a leading plus sign is refused: the text `+1`. | `Json.Spec.rejects_num_leading_plus` | +| A number text with a letter where a digit must stand is refused: the text `1a`. | `Json.Spec.rejects_num_nondigit` | A document value is well formed when a number's text matches the RFC 8259 number grammar and every value inside an array or object is well formed too. Strings and keys need no further condition. A decimal value is well formed when it is held in the canonical form: the zero value as sign positive, significand `0`, exponent `0`, and a nonzero value with no trailing zero in its significand. The value round trip needs no bound on the value: the canonical text is finite for every held value. -The five claims rest on the proofs in `Proofs/RoundTrip.lean` and `Proofs/NumRoundTrip.lean`, where they are `Json.Proofs.parse_print`, `Json.NumProofs.read_print`, `Json.NumProofs.readNumber_wf`, `Json.NumProofs.read_print_of_read`, and `Json.NumProofs.canonical_eq_of_value_eq`. `Spec.parse_print` checks against the standard axioms only (`propext`, `Classical.choice`, `Quot.sound`); `Spec.read_print`, `Spec.readNumber_wf`, and `Spec.read_print_of_read` against `propext` and `Quot.sound` only; and `Spec.canonical_eq_of_value_eq` against `propext` only. A reader can confirm this with `#print axioms`, or by running `lake env lean Proofs/Verify.lean`. The test harness writes that output into the Axiom check section of `tests/TEST-RESULTS.md` on every run. The refusal theorems are single inputs checked in the kernel with `decide +kernel`. +The five claims rest on the proofs in `Json/Proofs/RoundTrip.lean` and `Json/Proofs/NumRoundTrip.lean`, where they are `Json.Proofs.parse_print`, `Json.NumProofs.read_print`, `Json.NumProofs.readNumber_wf`, `Json.NumProofs.read_print_of_read`, and `Json.NumProofs.canonical_eq_of_value_eq`. `Json.Spec.parse_print` checks against the standard axioms only (`propext`, `Classical.choice`, `Quot.sound`); `Json.Spec.read_print`, `Json.Spec.readNumber_wf`, and `Json.Spec.read_print_of_read` against `propext` and `Quot.sound` only; and `Json.Spec.canonical_eq_of_value_eq` against `propext` only. A reader can confirm this with `#print axioms`, or by running `lake env lean Json/Proofs/Verify.lean`. The test harness writes that output into the Axiom check section of `tests/TEST-RESULTS.md` on every run. The refusal theorems are single inputs checked in the kernel with `decide +kernel`. The command line tool in `Main.lean` calls `Json.parse`, `Json.print`, `Json.readNumber`, and `Json.printVal` directly, the same functions the theorems are about. @@ -76,7 +76,7 @@ The command line tool in `Main.lean` calls `Json.parse`, `Json.print`, `Json.rea ## Re-check it -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. +1. `lake comparator --paranoid`: builds the challenge file `Json/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`: JSONTestSuite if a clone is found, the differential against Python's `json` module, the number layer against Python's `decimal` module, and the axiom check, with counts and any failures written to `tests/TEST-RESULTS.md`. -3. `lake build`: the library, the proofs, and the tool build clean, and `lake env lean Proofs/Verify.lean` prints the axiom list for the five headline theorems. +3. `lake build`: the library, the proofs, and the tool build clean, and `lake env lean Json/Proofs/Verify.lean` prints the axiom list for the five headline theorems. 4. Read `SPEC.md` against RFC 8259 and check the pinned readings are the ones you want. diff --git a/SPEC.md b/SPEC.md index ce54e18..aee6f97 100644 --- a/SPEC.md +++ b/SPEC.md @@ -1,6 +1,6 @@ # Specification: json -A JSON parser and printer in Lean, following RFC 8259. A reviewer who did not write this specification approves it, together with the statement file. The statements are in `Spec.lean` and their proofs are in `Proofs/SpecProofs.lean`; no reviewer has approved them yet, so nothing here counts toward the verified bar yet. +A JSON parser and printer in Lean, following RFC 8259. A reviewer who did not write this specification approves it, together with the statement file. The statements are in `Json/Spec.lean` and their proofs are in `Json/Proofs/SpecProofs.lean`; no reviewer has approved them yet, so nothing here counts toward the verified bar yet. Text is `List Char`. A Lean `Char` is one Unicode scalar value, so a string in this library can never hold half of a surrogate pair. That fact shapes two choices below. @@ -100,23 +100,23 @@ No claim is made that the parser accepts every text the RFC grammar allows, or r ## Properties and their theorems -Each property a reader can check in the page (`README.md`) names its theorem. The theorems are stated in `Spec.lean` and proved in `Proofs/SpecProofs.lean`. The refusal theorems are single inputs, one for each named rejection shape in the test harness; the tests in `tests/` cover each rule on many more inputs. +Each property a reader can check in the page (`README.md`) names its theorem. The theorems are stated in `Json/Spec.lean` and proved in `Json/Proofs/SpecProofs.lean`. The refusal theorems are single inputs, one for each named rejection shape in the test harness; the tests in `tests/` cover each rule on many more inputs. | Property | Theorem | |----------|---------| -| Parsing the printed form of a well formed value gives the value back | `Spec.parse_print` | -| Reading the canonical text of a well formed decimal value gives the value back | `Spec.read_print` | -| Every value the number reader returns is well formed | `Spec.readNumber_wf` | -| The canonical text of a text's value re-reads to that value | `Spec.read_print_of_read` | -| Two texts with the same value have the same canonical text | `Spec.canonical_eq_of_value_eq` | -| Characters after a complete value, past the allowed whitespace, are refused | `Spec.rejects_trailing_after_value` | -| A literal outside `true`, `false`, and `null` is refused | `Spec.rejects_bad_literal` | -| A leading zero in a number inside a document is refused | `Spec.rejects_leading_zero_in_document` | -| A bare minus sign is refused as a number text | `Spec.rejects_num_lone_minus` | -| A leading zero in a number text is refused | `Spec.rejects_num_leading_zero` | -| A point with no digit after it ends no number text | `Spec.rejects_num_trailing_point` | -| A point with no integer part before it starts no number text | `Spec.rejects_num_leading_point` | -| An exponent letter with no digits after it is refused | `Spec.rejects_num_bare_exponent` | -| An exponent sign with no digits after it is refused | `Spec.rejects_num_exponent_sign_only` | -| A leading plus sign is refused | `Spec.rejects_num_leading_plus` | -| A letter where a digit must stand is refused | `Spec.rejects_num_nondigit` | +| Parsing the printed form of a well formed value gives the value back | `Json.Spec.parse_print` | +| Reading the canonical text of a well formed decimal value gives the value back | `Json.Spec.read_print` | +| Every value the number reader returns is well formed | `Json.Spec.readNumber_wf` | +| The canonical text of a text's value re-reads to that value | `Json.Spec.read_print_of_read` | +| Two texts with the same value have the same canonical text | `Json.Spec.canonical_eq_of_value_eq` | +| Characters after a complete value, past the allowed whitespace, are refused | `Json.Spec.rejects_trailing_after_value` | +| A literal outside `true`, `false`, and `null` is refused | `Json.Spec.rejects_bad_literal` | +| A leading zero in a number inside a document is refused | `Json.Spec.rejects_leading_zero_in_document` | +| A bare minus sign is refused as a number text | `Json.Spec.rejects_num_lone_minus` | +| A leading zero in a number text is refused | `Json.Spec.rejects_num_leading_zero` | +| A point with no digit after it ends no number text | `Json.Spec.rejects_num_trailing_point` | +| A point with no integer part before it starts no number text | `Json.Spec.rejects_num_leading_point` | +| An exponent letter with no digits after it is refused | `Json.Spec.rejects_num_bare_exponent` | +| An exponent sign with no digits after it is refused | `Json.Spec.rejects_num_exponent_sign_only` | +| A leading plus sign is refused | `Json.Spec.rejects_num_leading_plus` | +| A letter where a digit must stand is refused | `Json.Spec.rejects_num_nondigit` | diff --git a/bar.toml b/bar.toml index 22c12df..806670d 100644 --- a/bar.toml +++ b/bar.toml @@ -12,7 +12,7 @@ spec_authors = ["abu-aska"] entry_points = ["Main.lean"] [spec] -files = ["SPEC.md", "Spec.lean"] +files = ["SPEC.md", "Json/Spec.lean"] # The code under proof: the functions the statements are about. code = [ # The data types the statements are about, and their constructors. diff --git a/comparator.json b/comparator.json index a05140b..f9c7b1e 100644 --- a/comparator.json +++ b/comparator.json @@ -1 +1 @@ -{"challenge_module":"Spec","permitted_axioms":["propext","Classical.choice","Quot.sound"],"solution_module":"Proofs","theorem_names":["Spec.parse_print","Spec.read_print","Spec.readNumber_wf","Spec.read_print_of_read","Spec.canonical_eq_of_value_eq","Spec.rejects_trailing_after_value","Spec.rejects_bad_literal","Spec.rejects_leading_zero_in_document","Spec.rejects_num_lone_minus","Spec.rejects_num_leading_zero","Spec.rejects_num_trailing_point","Spec.rejects_num_leading_point","Spec.rejects_num_bare_exponent","Spec.rejects_num_exponent_sign_only","Spec.rejects_num_leading_plus","Spec.rejects_num_nondigit"]} \ No newline at end of file +{"challenge_module":"Json.Spec","permitted_axioms":["propext","Classical.choice","Quot.sound"],"solution_module":"Json.Proofs","theorem_names":["Json.Spec.parse_print","Json.Spec.read_print","Json.Spec.readNumber_wf","Json.Spec.read_print_of_read","Json.Spec.canonical_eq_of_value_eq","Json.Spec.rejects_trailing_after_value","Json.Spec.rejects_bad_literal","Json.Spec.rejects_leading_zero_in_document","Json.Spec.rejects_num_lone_minus","Json.Spec.rejects_num_leading_zero","Json.Spec.rejects_num_trailing_point","Json.Spec.rejects_num_leading_point","Json.Spec.rejects_num_bare_exponent","Json.Spec.rejects_num_exponent_sign_only","Json.Spec.rejects_num_leading_plus","Json.Spec.rejects_num_nondigit"]} \ No newline at end of file diff --git a/lakefile.toml b/lakefile.toml index a39cc35..5d260ac 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -1,16 +1,18 @@ name = "json" version = "0.1.0" license = "Apache-2.0" -defaultTargets = ["Json", "Proofs", "json"] +defaultTargets = ["Json", "JsonSpec", "JsonProofs", "json"] [[lean_lib]] name = "Json" [[lean_lib]] -name = "Proofs" +name = "JsonSpec" +roots = ["Json.Spec"] [[lean_lib]] -name = "Spec" +name = "JsonProofs" +roots = ["Json.Proofs"] [[lean_exe]] name = "json" diff --git a/tests/TEST-RESULTS.md b/tests/TEST-RESULTS.md index 4875283..f31f7fc 100644 --- a/tests/TEST-RESULTS.md +++ b/tests/TEST-RESULTS.md @@ -28,7 +28,7 @@ Written by `tests/run_tests.py`. Rerun it to check these numbers. ## Axiom check -The output of `#print axioms` for the five named theorems, from `lake env lean Proofs/Verify.lean`: +The output of `#print axioms` for the five named theorems, from `lake env lean Json/Proofs/Verify.lean`: - 'Json.Proofs.parse_print' depends on axioms: [propext, Classical.choice, Quot.sound] - 'Json.NumProofs.read_print' depends on axioms: [propext, Quot.sound] diff --git a/tests/run_tests.py b/tests/run_tests.py index 497c3b9..8f6b514 100644 --- a/tests/run_tests.py +++ b/tests/run_tests.py @@ -59,7 +59,7 @@ must answer `none`, and a text at the limit must print. The results file also carries an Axiom check section. The - harness runs `lake env lean Proofs/Verify.lean`, which + harness runs `lake env lean Json/Proofs/Verify.lean`, which prints the axioms of the headline theorems with `#print axioms`, and writes that output into the section. If the run fails or a named theorem is missing from the @@ -1035,7 +1035,7 @@ def main(): timeout=120, ).stdout.strip() - # The axiom check: Proofs/Verify.lean prints the axioms of + # The axiom check: Json/Proofs/Verify.lean prints the axioms of # the five named theorems with `#print axioms`. Its output # goes into the results file, in the Axiom check section. # A failed run, a missing line, or a line that does not name @@ -1048,7 +1048,7 @@ def main(): "Json.NumProofs.canonical_eq_of_value_eq", ] axiom_run = subprocess.run( - ["lake", "env", "lean", "Proofs/Verify.lean"], + ["lake", "env", "lean", "Json/Proofs/Verify.lean"], cwd=ROOT, capture_output=True, text=True, @@ -1066,7 +1066,7 @@ def main(): ) ): all_failures.append( - "axiom check: running Proofs/Verify.lean gave " + "axiom check: running Json/Proofs/Verify.lean gave " f"status {axiom_run.returncode} and lines {axiom_lines!r}" ) @@ -1086,7 +1086,7 @@ def main(): out.append("") out.append( "The output of `#print axioms` for the five named theorems, " - "from `lake env lean Proofs/Verify.lean`:" + "from `lake env lean Json/Proofs/Verify.lean`:" ) out.append("") for line in axiom_lines: