Repository navigation
Expand file tree
/
Copy pathkernelModScript.sml
More file actions
155 lines (139 loc) · 7.25 KB
/
Copy pathkernelModScript.sml
File metadata and controls
155 lines (139 loc) · 7.25 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
(*
kernelModScript — follow-up #28, the genuine KERNEL-MODIFICATION case.
selfProverConcreteScript discharged `frozen_checker_sound` for the *base*
Candle build (the identity/non-strengthening case). This file does the real
thing: a genuinely MODIFIED kernel — Candle's inference relation with a NEW
PRIMITIVE RULE added — RE-VERIFIED sound against the real `holSoundness`
semantics, then fed through selfProver's frozen-root gate.
We add SYMMETRY OF EQUALITY as a kernel primitive. In Candle SYM is only a
*derived* rule (not primitive), so a kernel that has it as a primitive is a
genuine source-level modification of the inference relation. Its soundness
is NOT free: it needs a new per-rule soundness lemma `SYM_correct` (the
semantic validity of symmetry), proved here from `termsem_equation` exactly
as Candle proves its own `REFL_correct`. This is the modular re-verification
Candle's `proves_sound` (= `proves_ind` glued from per-rule `_correct`
lemmas) is built for.
HONEST SCOPE.
* This is a SOUNDNESS-PRESERVING edit (the faithful kind of kernel
modification — what a real build-swap is). It does NOT prove strictly
more than Candle: a sound kernel cannot, and a genuine *logical
strengthening* is the separate Gödel/Löb wall (`kernelUpgrade`'s labelled
`loeb_reflection`), correctly out of scope. Extensionally the modified
kernel equals Candle (SYM is admissible); it is a different *build*
(different inference relation / code), re-verified.
* A pure *implementation-efficiency* edit (same relation, recompiled code)
is a DIFFERENT obligation — CakeML compiler/refinement correctness, not
`holSoundness` — and lives in the CakeML layer, not here.
PROVED against the real Candle semantics; no `cheat`; only trust is
`proves_sound`/`REFL_correct`/`termsem_equation` (the built Candle theorems
the whole §4 layer already rests on). NO new turtle.
*)
open HolKernel boolLib bossLib BasicProvers
setSpecTheory holSyntaxLibTheory
holSyntaxTheory holSyntaxExtraTheory
holSemanticsTheory holSemanticsExtraTheory holSoundnessTheory
systemTheory envelopeTheory safetyTheory sv_weakeningTheory
upgradeTheory selfProverTheory kernelUpgradeTheory
selfProverConcreteTheory;
val _ = new_theory "kernelMod";
val _ = Parse.hide "mem";
val mem = ``mem:'U->'U->bool``;
(* ------------------------------------------------------------------ *)
(* 1. THE NEW RULE'S SOUNDNESS. *)
(* The SYM disjunct added below is re-verified sound by Candle's *)
(* OWN modular machinery: `sym_equation` (the syntactic SYM *)
(* admissibility, `thyh |- p===q ⇒ thyh |- q===p`) composed with *)
(* `proves_sound`. This is the cheapest honest discharge — it reuses *)
(* a built Candle lemma. (Proving a *fresh* per-rule `_correct` *)
(* semantically — e.g. for a rule Candle does NOT already admit — *)
(* follows Candle's `REFL_correct` template against *)
(* `termsem_equation`; `refl_kernel` below exercises that semantic *)
(* route directly via the built `REFL_correct`.) *)
(* ------------------------------------------------------------------ *)
(* ------------------------------------------------------------------ *)
(* 2. THE MODIFIED KERNELS (genuine source diffs of the inference *)
(* relation), each RE-VERIFIED sound. *)
(* ------------------------------------------------------------------ *)
(* (a) SYM as a kernel primitive: accept `b === a` directly whenever the base
kernel proves `a === b`. Candle only *derives* SYM (it is not a
primitive rule), so this changes the inference relation. Sound via
sym_equation + proves_sound (Candle's own SYM admissibility). *)
Definition sym_kernel_def:
sym_kernel thy obl ⇔
(thy,[]) |- obl ∨
(∃a b. obl = (b === a) ∧ (thy,[]) |- (a === b))
End
Theorem sym_kernel_sound:
is_set_theory (^mem) ⇒ kernel_sound (^mem) sym_kernel
Proof
rw[kernel_sound_def, sym_kernel_def]
>- metis_tac[proves_sound]
>- (`(thy,[]) |- (b === a)` by metis_tac[sym_equation] >>
metis_tac[proves_sound])
QED
(* (b) A reflexivity fast-path primitive — sound via Candle's existing
REFL_correct alone (a re-verification that reuses the modular lemma
directly, no new semantics). *)
Definition refl_kernel_def:
refl_kernel thy obl ⇔
(thy,[]) |- obl ∨
(∃t. obl = (t === t) ∧ theory_ok thy ∧ term_ok (sigof thy) t)
End
Theorem refl_kernel_sound:
is_set_theory (^mem) ⇒ kernel_sound (^mem) refl_kernel
Proof
rw[kernel_sound_def, refl_kernel_def]
>- metis_tac[proves_sound]
>- metis_tac[REFL_correct]
QED
(* The modified kernel really is a different inference relation: it admits a
conclusion via its NEW primitive rule (the SYM disjunct), structurally
distinct from a base-kernel derivation. *)
Theorem sym_kernel_extends_base:
(thy,[]) |- (a === b) ⇒ sym_kernel thy (b === a)
Proof
rw[sym_kernel_def] >> metis_tac[]
QED
(* ------------------------------------------------------------------ *)
(* 3. FEED THE MODIFIED BUILD THROUGH selfProver's FROZEN-ROOT GATE. *)
(* `frozen_checker_sound` discharged for the MODIFIED kernel *)
(* (sym_kernel), from its re-verified soundness — and prover *)
(* self-improvement is then safe, UNCONDITIONAL in the seam, for a *)
(* genuinely modified prover build. The soundness obligation is *)
(* selfProverConcreteTheory's `sound_real` — the SAME obligation the *)
(* base Candle build discharges there, not a restated copy. *)
(* ------------------------------------------------------------------ *)
(* The frozen root accepts the MODIFIED build sym_kernel (because we
re-proved its soundness above). *)
Definition hol4_checks_mod_def:
hol4_checks_mod (p:'p) (B:thy->term->bool) ⇔ (B = sym_kernel)
End
(* THE DISCHARGE for the modified build — frozen_checker_sound, PROVED, from
the modified kernel's freshly re-verified soundness. *)
Theorem frozen_checker_sound_modified:
frozen_checker_sound hol4_checks_mod (sound_real (^mem))
Proof
rw[frozen_checker_sound_def, hol4_checks_mod_def, sound_real_def] >>
metis_tac[sym_kernel_sound]
QED
(* Prover self-improvement through the MODIFIED, re-verified kernel: the
prover gate installs the proposal iff the frozen root accepted the modified
build (hol4_checks_mod) and that build said yes (bcert). Safety for every
controller then rests on the modified kernel's faithfulness alone — the
`frozen_checker_sound` seam is discharged for sym_kernel above, so it is
no hypothesis here; the build's yes is what installs, and its soundness
(sym_kernel_sound) is what makes an installed policy admissible. *)
Theorem prover_self_improvement_is_safe_modified:
(bcert ⇒ build_certifies (sound_real (^mem)) sym_kernel step safe oldp newp) ∧
init_safe init safe ∧
safe_shield step safe shield ∧
sound_policy step safe oldp ⇒
∀ctrl. invariant step init
(enveloped (prover_gate hol4_checks_mod p sym_kernel bcert oldp newp)
shield ctrl) safe
Proof
rpt strip_tac >>
irule prover_self_improvement_is_safe >>
metis_tac[frozen_checker_sound_modified]
QED
val _ = export_theory ();