CheckTraceJson.lean

1 import ProofPath.TraceWire
2 import Lean.Data.Json.Parser
3 import Lean.Data.Json.Printer
4 
5 /-!
6 IO adapter for canonical NDJSON pairs [problem, certificate]. The proved part
7 is Wire.acceptJson on Json syntax trees. This adapter and the standard text
8 parser/printer are executed and cross-checked, not added as axioms or presented
9 as a proof of arbitrary file-system/byte-level behavior.
10 -/
11 open Lean ProofPath.Trace ProofPath.Trace.Wire
12 
13 def inspectPair (line : String) : String :=
14   match Json.parse line with
15   | .error _ => "REJECT_FORMAT"
16   | .ok j =>
17     match j with
18     | .arr a =>
19       match a.toList with
20       | [jp, jc] =>
21         match decodeProblem jp, decodeCertificate jc with
22         | some p, some c =>
23           if line != (Json.arr #[encodeProblem p, encodeCertificate c]).compress then
24             "REJECT_NONCANONICAL"
25           else if !problemValid p then "REJECT_PROBLEM"
26           else if !certificateValid p c then "REJECT_CERTIFICATE_SHAPE"
27           else if acceptJson jp jc then
28             if c.feasible then "ACCEPT_POSITIVE" else "ACCEPT_NEGATIVE"
29           else "REJECT_CERTIFICATE"
30         | _, _ => "REJECT_FORMAT"
31       | _ => "REJECT_FORMAT"
32     | _ => "REJECT_FORMAT"
33 
34 def main (args : List String) : IO UInt32 := do
35   match args with
36   | [path] =>
37     let text ← IO.FS.readFile path
38     for line in text.splitOn "\n" do
39       if !line.isEmpty then
40         if line.utf8ByteSize > 8388608 then
41           IO.println "RESOURCE_LIMIT"
42         else
43           IO.println (inspectPair line)
44     return 0
45   | _ =>
46     IO.eprintln "Usage: lean --run CheckTraceJson.lean canonical_pairs.ndjson"
47     return 2

Back to source controls