TraceExamples.lean

1 import ProofPath.TraceWire
2 import ProofPath.TraceCompleteness
3 
4 namespace ProofPath.Trace.Examples
5 open Wire
6 
7 def chain : Problem := ⟨4, [0], [⟨[0], 1⟩, ⟨[1], 2⟩], [], [3]⟩
8 def chainCertificate : Certificate := ⟨true, [0, 1, 2], [0, 1], none⟩
9 def blocked : Problem := { chain with negative := [2] }
10 def blockedCertificate : Certificate :=
11   ⟨false, [0, 1, 2], [0, 1], some ⟨2, [0, 1]⟩⟩
12 
13 theorem chain_accepted : accept chain chainCertificate = true := by decide
14 
15 theorem chain_has_protected_model :
16     chain.field.Extends chain.seeds chain.forbidden (fun v => v ∈ chainCertificate.closure) :=
17   certificate_positive _ _ (by decide) rfl
18 
19 theorem blocked_accepted : accept blocked blockedCertificate = true := by decide
20 
21 theorem blocked_has_no_model :
22     ¬ ∃ x, blocked.field.Extends blocked.seeds blocked.forbidden x :=
23   certificate_negative blocked blockedCertificate (by decide) rfl
24 
25 theorem accepted_json_has_checked_answer :
26     acceptJson (encodeProblem chain) (encodeCertificate chainCertificate) = true := by
27   rw [encoded_acceptance]
28   exact chain_accepted
29 
30 /-- Closedness by itself is not a least-model certificate. -/
31 theorem forged_closed_superset_is_rejected :
32     closed chain [0, 1, 2, 3] = true ∧
33       checkClosure chain [] [0, 1, 2, 3] = false := by decide
34 
35 /-- Derivability of every listed node does not establish saturation. -/
36 theorem partial_replay_is_not_complete :
37     replay chain true chain.initial [0] = some [1, 0] ∧
38       checkClosure chain [0] [0, 1] = false := by decide
39 
40 theorem wrong_order_rejected :
41     replay chain false chain.initial [1, 0] = none := by decide
42 
43 theorem unknown_rule_rejected :
44     replay chain false chain.initial [9] = none := by decide
45 
46 theorem repeated_rule_causal_not_strict :
47     checkWitness blocked ⟨2, [0, 0, 1]⟩ = true ∧
48       replay blocked true blocked.initial [0, 0, 1] = none := by decide
49 
50 theorem context_substitution_rejected :
51     accept blocked chainCertificate = false := by decide
52 
53 theorem witness_target_must_be_forbidden :
54     checkWitness chain ⟨2, [0, 1]⟩ = false := by decide
55 
56 theorem direct_observation_conflict :
57     checkWitness ({ chain with positive := [3] } : Problem) ⟨3, []⟩ = true := by decide
58 
59 def cycle : Problem := ⟨2, [], [⟨[0], 1⟩, ⟨[1], 0⟩], [], [1]⟩
60 
61 theorem unseeded_cycle_is_not_self_justifying :
62     accept cycle ⟨true, [], [], none⟩ = true ∧
63       checkWitness cycle ⟨1, [0, 1]⟩ = false := by decide
64 
65 theorem seeded_cycle_saturates :
66     accept { cycle with positive := [0] }
67       ⟨false, [0, 1], [0], some ⟨1, [0]⟩⟩ = true := by decide
68 
69 theorem empty_problem_accepted :
70     accept ⟨0, [], [], [], []⟩ ⟨true, [], [], none⟩ = true := by decide
71 
72 theorem empty_address_space_rejects_rule :
73     problemValid ⟨0, [], [⟨[], 0⟩], [], []⟩ = false := by decide
74 
75 theorem duplicate_rows_retain_distinct_addresses :
76     let p : Problem := ⟨2, [0], [⟨[0], 1⟩, ⟨[0], 1⟩], [], []⟩
77     accept p ⟨true, [0, 1], [0], none⟩ = true ∧
78     accept p ⟨true, [0, 1], [1], none⟩ = true := by decide
79 
80 theorem booleans_are_not_node_indices : decodeNat (.bool true) = none := rfl
81 
82 theorem strings_are_not_verdicts : decodeBool (.str "false") = none := rfl
83 
84 theorem extra_certificate_fields_rejected :
85     decodeCertificate (.arr #[.str "proof-path/certificate/1", .bool true,
86       .arr #[], .arr #[], .null, .null]) = none := rfl
87 
88 theorem wrong_version_rejected :
89     decodeCertificate (.arr #[.str "proof-path/certificate/2", .bool true,
90       .arr #[], .arr #[], .null]) = none := by decide
91 
92 end ProofPath.Trace.Examples

Back to source controls