TraceWire.lean

1 import ProofPath.Trace
2 import Lean.Data.Json.Basic
3 import Mathlib.Data.List.Nodup
4 
5 /-!
6 A strict, versioned JSON value codec. Positional arrays have exact lengths and
7 natural numbers use nonnegative, exponent-zero JSON number nodes. Round trips
8 are proved at the Json syntax-tree boundary, not assumed from sample tests.
9 The JSON text parser/printer and file I/O remain separately stated trust layers.
10 -/
11 namespace ProofPath.Trace.Wire
12 open Lean
13 
14 -- Small structural decoders make the accepted syntax explicit.
15 def encodeNat (n : Nat) : Json := .num ⟨Int.ofNat n, 0⟩
16 def decodeNat : Json → Option Nat
17   | .num ⟨Int.ofNat n, 0⟩ => some n
18   | _ => none
19 
20 def encodeBool (b : Bool) : Json := .bool b
21 def decodeBool : Json → Option Bool
22   | .bool b => some b
23   | _ => none
24 
25 def decodeItems {α : Type*} (d : Json → Option α) : List Json → Option (List α)
26   | [] => some []
27   | j :: js => do
28     let x ← d j
29     let xs ← decodeItems d js
30     pure (x :: xs)
31 
32 def encodeArray {α : Type*} (e : α → Json) (xs : List α) : Json :=
33   .arr ((xs.map e).toArray)
34 
35 def decodeArray {α : Type*} (d : Json → Option α) : Json → Option (List α)
36   | .arr a => decodeItems d a.toList
37   | _ => none
38 
39 @[simp] theorem nat_roundtrip (n : Nat) : decodeNat (encodeNat n) = some n := rfl
40 @[simp] theorem bool_roundtrip (b : Bool) : decodeBool (encodeBool b) = some b := rfl
41 
42 theorem items_roundtrip {α : Type*} (e : α → Json) (d : Json → Option α)
43     (hd : ∀ x, d (e x) = some x) (xs : List α) :
44     decodeItems d (xs.map e) = some xs := by
45   induction xs with
46   | nil => rfl
47   | cons x xs ih => simp [decodeItems, hd, ih]
48 
49 theorem array_roundtrip {α : Type*} (e : α → Json) (d : Json → Option α)
50     (hd : ∀ x, d (e x) = some x) (xs : List α) :
51     decodeArray d (encodeArray e xs) = some xs := by
52   simpa [decodeArray, encodeArray] using items_roundtrip e d hd xs
53 
54 @[simp] theorem natArray_roundtrip (xs : List Nat) :
55     decodeArray decodeNat (encodeArray encodeNat xs) = some xs :=
56   array_roundtrip encodeNat decodeNat nat_roundtrip xs
57 
58 def encodeRule (r : Rule) : Json :=
59   .arr #[encodeArray encodeNat r.premises, encodeNat r.conclusion]
60 
61 def decodeRule : Json → Option Rule
62   | .arr a =>
63     match a.toList with
64     | [ps, co] => do
65       let premises ← decodeArray decodeNat ps
66       let conclusion ← decodeNat co
67       pure ⟨premises, conclusion⟩
68     | _ => none
69   | _ => none
70 
71 @[simp] theorem rule_roundtrip (r : Rule) : decodeRule (encodeRule r) = some r := by
72   cases r
73   simp [decodeRule, encodeRule]
74 
75 @[simp] theorem ruleArray_roundtrip (xs : List Rule) :
76     decodeArray decodeRule (encodeArray encodeRule xs) = some xs :=
77   array_roundtrip encodeRule decodeRule rule_roundtrip xs
78 
79 def encodeProblem (p : Problem) : Json :=
80   .arr #[.str "proof-path/problem/1", encodeNat p.nodeCount,
81     encodeArray encodeNat p.leaves, encodeArray encodeRule p.rules,
82     encodeArray encodeNat p.positive, encodeArray encodeNat p.negative]
83 
84 def decodeProblem : Json → Option Problem
85   | .arr a =>
86     match a.toList with
87     | [.str "proof-path/problem/1", n, l, r, s, f] => do
88       let nodeCount ← decodeNat n
89       let leaves ← decodeArray decodeNat l
90       let rules ← decodeArray decodeRule r
91       let positive ← decodeArray decodeNat s
92       let negative ← decodeArray decodeNat f
93       pure ⟨nodeCount, leaves, rules, positive, negative⟩
94     | _ => none
95   | _ => none
96 
97 @[simp] theorem problem_roundtrip (p : Problem) :
98     decodeProblem (encodeProblem p) = some p := by
99   cases p
100   simp [decodeProblem, encodeProblem]
101 
102 def encodeWitness (w : Witness) : Json :=
103   .arr #[encodeNat w.target, encodeArray encodeNat w.trace]
104 
105 def decodeWitness : Json → Option Witness
106   | .arr a =>
107     match a.toList with
108     | [t, tr] => do
109       let target ← decodeNat t
110       let trace ← decodeArray decodeNat tr
111       pure ⟨target, trace⟩
112     | _ => none
113   | _ => none
114 
115 @[simp] theorem witness_roundtrip (w : Witness) :
116     decodeWitness (encodeWitness w) = some w := by
117   cases w
118   simp [decodeWitness, encodeWitness]
119 
120 def encodeObstruction : Option Witness → Json
121   | none => .null
122   | some w => encodeWitness w
123 
124 def decodeObstruction : Json → Option (Option Witness)
125   | .null => some none
126   | j => (decodeWitness j).map some
127 
128 @[simp] theorem obstruction_roundtrip (w : Option Witness) :
129     decodeObstruction (encodeObstruction w) = some w := by
130   cases w with
131   | none => rfl
132   | some w => simp [decodeObstruction, encodeObstruction, encodeWitness,
133       decodeWitness]
134 
135 def encodeCertificate (c : Certificate) : Json :=
136   .arr #[.str "proof-path/certificate/1", encodeBool c.feasible,
137     encodeArray encodeNat c.closure, encodeArray encodeNat c.trace,
138     encodeObstruction c.obstruction]
139 
140 def decodeCertificate : Json → Option Certificate
141   | .arr a =>
142     match a.toList with
143     | [.str "proof-path/certificate/1", f, cl, tr, ob] => do
144       let feasible ← decodeBool f
145       let closure ← decodeArray decodeNat cl
146       let trace ← decodeArray decodeNat tr
147       let obstruction ← decodeObstruction ob
148       pure ⟨feasible, closure, trace, obstruction⟩
149     | _ => none
150   | _ => none
151 
152 @[simp] theorem certificate_roundtrip (c : Certificate) :
153     decodeCertificate (encodeCertificate c) = some c := by
154   cases c
155   simp [decodeCertificate, encodeCertificate]
156 
157 theorem encodeProblem_injective : Function.Injective encodeProblem := by
158   intro a b h
159   have he := congrArg decodeProblem h
160   simpa using he
161 
162 theorem encodeCertificate_injective : Function.Injective encodeCertificate := by
163   intro a b h
164   have he := congrArg decodeCertificate h
165   simpa using he
166 
167 def nodeListValid (n : Nat) (xs : List Nat) : Bool :=
168   xs.all (fun v => decide (v < n)) && decide xs.Nodup
169 
170 def problemValid (p : Problem) : Bool :=
171   nodeListValid p.nodeCount p.leaves &&
172   nodeListValid p.nodeCount p.positive &&
173   nodeListValid p.nodeCount p.negative &&
174   p.rules.all (fun r => nodeListValid p.nodeCount r.premises &&
175     decide (r.conclusion < p.nodeCount))
176 
177 def traceValid (p : Problem) (tr : List Nat) : Bool :=
178   tr.all (fun j => decide (j < p.rules.length))
179 
180 def certificateValid (p : Problem) (c : Certificate) : Bool :=
181   nodeListValid p.nodeCount c.closure && traceValid p c.trace &&
182   match c.obstruction with
183   | none => true
184   | some w => decide (w.target < p.nodeCount) && traceValid p w.trace
185 
186 /-- The input problem is a separate argument; certificates cannot silently
187 replace it. Invalid data is rejected before mathematical replay. -/
188 def accept (p : Problem) (c : Certificate) : Bool :=
189   problemValid p && certificateValid p c && checkCertificate p c
190 
191 def acceptJson (problemJson certificateJson : Json) : Bool :=
192   match decodeProblem problemJson, decodeCertificate certificateJson with
193   | some p, some c => accept p c
194   | _, _ => false
195 
196 /-- The codec neither changes nor fabricates the executable verdict. -/
197 theorem encoded_acceptance (p : Problem) (c : Certificate) :
198     acceptJson (encodeProblem p) (encodeCertificate c) = accept p c := by
199   simp [acceptJson]
200 
201 def CertifiedAnswer (p : Problem) (c : Certificate) : Prop :=
202   (∀ v, v ∈ c.closure ↔ v ∈ p.exactClosure) ∧
203   (c.feasible = true ↔ ∃ x, p.field.Extends p.seeds p.forbidden x)
204 
205 theorem acceptance_sound (p : Problem) (c : Certificate)
206     (h : accept p c = true) : CertifiedAnswer p c := by
207   have hc : checkCertificate p c = true := (Bool.and_eq_true_iff.mp h).2
208   exact ⟨certificate_closure p c hc, certificate_decides_feasibility p c hc⟩
209 
210 /-- Soundness is about the actual decoded records, not a claimed external identity. -/
211 theorem json_acceptance_sound (jp jc : Json) (h : acceptJson jp jc = true) :
212     ∃ p c, decodeProblem jp = some p ∧ decodeCertificate jc = some c ∧
213       CertifiedAnswer p c := by
214   cases hp : decodeProblem jp with
215   | none => simp [acceptJson, hp] at h
216   | some p =>
217     cases hc : decodeCertificate jc with
218     | none => simp [acceptJson, hp, hc] at h
219     | some c =>
220       exact ⟨p, c, rfl, rfl, acceptance_sound p c (by simpa [acceptJson, hp, hc] using h)⟩
221 
222 /-- A valid finite address table cannot derive an unnamed node slot. -/
223 theorem valid_closure_bounded (p : Problem) (h : problemValid p = true) :
224     ∀ v, v ∈ p.exactClosure → v < p.nodeCount := by
225   have hall := Bool.and_eq_true_iff.mp h
226   have hleft := Bool.and_eq_true_iff.mp hall.1
227   have hfirst := Bool.and_eq_true_iff.mp hleft.1
228   have hl := (Bool.and_eq_true_iff.mp hfirst.1).1
229   have hs := (Bool.and_eq_true_iff.mp hfirst.2).1
230   have hm : p.field.Model (fun v => v < p.nodeCount) := by
231     constructor
232     · intro v hv
233       have hh := List.all_eq_true.mp hl v hv
234       simpa using hh
235     · intro j hj _
236       cases he : lookup p.rules j with
237       | none => simp [Problem.field, he] at hj
238       | some r =>
239         have hh := List.all_eq_true.mp hall.2 r (lookup_mem he)
240         have hc := (Bool.and_eq_true_iff.mp hh).2
241         simpa [Problem.field, he] using hc
242   apply p.field.closure_le_model p.seeds hm
243   intro v hv
244   have hh := List.all_eq_true.mp hs v hv
245   simpa using hh
246 
247 end ProofPath.Trace.Wire

Back to source controls