Move proof modules under Json

Json/Proofs.lean

@@ -0,0 +1,3 @@
+import Json.Proofs.RoundTrip
+import Json.Proofs.NumRoundTrip
+import Json.Proofs.SpecProofs

Proofs/NumRoundTrip.lean → Json/Proofs/NumRoundTrip.lean

@@ -22,7 +22,7 @@
 -/
 
 import Json
-import Proofs.RoundTrip
+import Json.Proofs.RoundTrip
 
 namespace Json.NumProofs
 

Proofs/SpecProofs.lean → 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

Proofs/Verify.lean → 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

Spec.lean → 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,20 +69,20 @@ 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
 
 /-- A number with a leading zero inside a document is refused:
     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

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.

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.