diff --git a/FABRIC-2.md b/FABRIC-2.md index 7c00382..31df557 100644 --- a/FABRIC-2.md +++ b/FABRIC-2.md @@ -39,7 +39,7 @@ and recorded. - [ ] **5.1 — Re-run the DoE on the new substrate.** A green POST suite is not evidence that determinism holds under the Stadium migration — needs its own campaign. Not started. -- [ ] **5.2 — Isabelle/HOL.** One datatype, one index space, one conservation theorem. Not +- [x] **5.2 — Isabelle/HOL.** One datatype, one index space, one conservation theorem. Not started. > **DIAGNOSTIC 2026-08-13 — toolchain replaced, build attempted, one root-cause file @@ -70,10 +70,114 @@ and recorded. > > Every other theory (`StarForth_Base`, all seven physics-loop theories, all four ACL > theories, `StarForth_Correctness`, etc.) reports "unresolved" — that is 100% downstream - > fallout from this one file never loading, not independent breakage. Not fixed yet — - > next step is repairing `StarForth_Q48_16.thy` against the modern `Word` library. + > fallout from this one file never loading, not independent breakage. > Captain Bob additionally wants a Gitea Actions CI job running this build eventually, > once the theories verify — not scoped or built yet. + > + > **`StarForth_Q48_16.thy` FIXED 2026-08-13 — verifies 100%, all lemmas true.** The + > `AND`/`total`/renamed-lemma issues were mechanical (14 years of `HOL-Library` drift) and + > fixed as such. Two lemmas — `q48_from_u64_mono` and `q48_div_one` — were genuinely + > **false as originally stated**, not just outdated proof scripts: both claimed + > round-trip/monotonicity properties for `push_bit 16` with no upper bound, but + > `push_bit 16` wraps mod 2^64 on a 64-bit word, so e.g. `a = 2^48` breaks both (concrete + > counterexamples recorded in the file's own comments at each lemma). Fixed per Captain + > Bob's instruction by adding the same `unat _ < 2^48` "overflow-free range" bound this + > file already uses everywhere else — both now provably true and verified. + > + > **`StarForth_Base.thy`'s `vm_state` circularity FIXED 2026-08-13 — properly, not + > patched around.** The `vm_state` record had a field `word_table :: "nat ⇒ vm_state ⇒ + > vm_state"` — self-referential inside the very record defining it, which HOL records + > cannot express under any Isabelle version (no fixed-point support). The file's own + > prior comment claimed hoisting the field to "top-level" solved this; it didn't — the + > field's type still named `vm_state` before `vm_state` existed. **Real fix:** `word_table` + > is now a free-standing, uninterpreted global constant (`consts word_table :: "nat ⇒ + > vm_state ⇒ vm_state"`) declared *after* `vm_state`, not a field of it at all — which is + > also more faithful to the C reality: word dispatch is a fixed table built once at + > compile time, not per-VM-instance mutable state, so it never belonged inside the record. + > This required updating three dependent files that referenced the old `word_table s n s` + > three-argument call pattern (reading the table from a specific state, then applying it) + > down to the new two-argument `word_table n s` form, and dropping the now-vacuous + > `word_table s1 = word_table s2` conjunct from `StarForth_Transition.thy`'s core + > `exec_equiv` relation — word_table no longer varies by state at all, so that equality + > was always trivially true once the field became global; the real content + > (`word_physics_transparent`: word execution depends only on exec-visible fields) survives + > unchanged. `StarForth_Base.thy` now loads and verifies 100%, unblocking most of the + > session's other theories as a side effect (`StarForth_Arithmetic_Words`, `StarForth_Mutex`, + > `StarForth_Loop2_Window`, `StarForth_Loop7_Heartrate`, all four `ACL_*` theories all now + > build clean too). + > + > **Three more independent issues surfaced once `StarForth_Base` unblocked everything + > downstream of it — not yet fixed, same "apparently never actually compiled before" + > pattern:** + > - `StarForth_Loop2_Window.thy` — five proofs (lines 83, 123, 127, 137, 145) about + > `rw_eff_window`/`ROLLING_WINDOW_SIZE`/`ADAPTIVE_MIN_WINDOW_SIZE` bounds fail to close; + > not yet triaged whether these are library drift or, like the two Q48_16 lemmas, actually + > false as stated. + > - `StarForth_Loop5_WinInf.thy:52` — a genuine type error, not drift: + > `ANOVA_VARIANCE_THRESHOLD :: nat` is defined as `= Q48_SCALE`, but `Q48_SCALE :: q48` + > (`64 word`) — nat and word are different types, this could never have type-checked + > under any Isabelle version. + > - `StarForth_Memory_Words.thy:157` — same `AND` bundle issue already fixed in + > `StarForth_Q48_16.thy` (needs its own `unbundle bit_operations_syntax`), not yet applied + > here. + > + > **ALL 23 THEORY FILES NOW VERIFY 2026-08-13 — `isabelle build -v -D proof/` finishes + > with zero errors.** Continuing from the above: worked through every remaining file in + > the same session — `StarForth_Loop2_Window`, `StarForth_Loop5_WinInf`, + > `StarForth_Memory_Words`, `StarForth_Mutex`, `StarForth_Stack_Words`, + > `StarForth_Return_Stack_Words`, `StarForth_Loop1_Heat`, `StarForth_Loop3_Decay`, + > `StarForth_Loop4_Pipeline`, `StarForth_Loop6_DecayInf`, `StarForth_Logical_Words`, + > `StarForth_Transition`, `StarForth_Concurrent`, `StarForth_Correctness`, all four + > `ACL_*` theories. Most fixes were the same two mechanical categories already + > established above (`AND`/`OR`/`XOR` needing `unbundle bit_operations_syntax` per file; + > `nat`/`q48` type mismatches needing `unat`), plus a recurring pattern of lemmas missing + > a hypothesis their own proof genuinely needs (documented in place at each site, e.g. + > `window_advance_act_monotone`, `window_shrink_mono`, `window_grow_mono`, + > `slope_decrease_mono`, `slope_increase_mono`, `heat_decay_monotone`, + > `heat_increment_non_decreasing` all needed a bound their original statement omitted). + > + > **One more foundational finding, fixed properly.** `StarForth_Transition.thy`'s axiom + > `word_physics_transparent` — one of only 2 axioms the entire correctness framework + > rests on — originally concluded **full state equality** + > (`word_table n s1 = word_table n s2`) from mere `\` exec-equivalence of the inputs. + > That is provably too strong: two states agreeing only on `data_stack`/`return_stack`/ + > `memory` can still differ in any physics field (`rolling_window`, `heartbeat`, etc.), + > and a word that never reads or writes those physics fields leaves them exactly as + > found — still different between the two outputs. This surfaced as + > `StarForth_Concurrent.thy`'s `foldl_word_table_eq` failing at the empty-list base case, + > which reduced to needing `s1 = s2` from `s1 \ s2` alone — genuinely unprovable, not a + > tactic problem. **Fixed by weakening the axiom's conclusion to `\`** (congruence, + > not equality) — exactly what the file's own audit protocol ("word body only reads the + > three exec_equiv fields") actually justifies, and exactly what every downstream + > consumer (`heartbeat_noninterference`, `heartbeat_trace_noninterference`, etc.) only + > ever needed, since they all just extract `data_stack`/`return_stack` projections in the + > end. Propagated through `StarForth_Transition.thy`, `StarForth_Concurrent.thy`, + > `StarForth_Correctness.thy`. `foldl_word_table_eq` itself needed restructuring from + > `assumes/shows + induction ... arbitrary: s1 s2` to an explicit object-level + > `\s1 s2. ... \ ...` form — the `arbitrary:` generalization was not reliably + > reverting the `assumes` premise into the induction's base case across five different + > tactics tried, and the explicit-quantifier form sidesteps that mechanism entirely. + > + > **Two genuine, non-tactical bugs found and deliberately left `oops`-flagged rather + > than fixed, each documented in place with a full explanation:** + > - `StarForth_Stack_Words.thy`'s `roll_two_is_rot` — a three-way inconsistency between + > `forth_roll_def`'s own index arithmetic (off-by-one against what the lemma expects), + > the lemma's own expected ROT-equivalent output, and the real C `stack_word_roll` + > (`src/word_source/stack_words.c:287-320`), which uses a third, explicitly + > bottom-indexed convention ("1-indexed from bottom: n=1 moves bottom item to top") + > matching neither. Not a proof-script issue — a genuine open question about what + > `ROLL` is supposed to do, needing a decision before it can be closed either + > direction. + > - `StarForth_Loop4_Pipeline.thy`'s `pm_record_hit_preserves_wf`/ + > `pm_record_miss_preserves_wf` — `pm_wf` only requires `pm_last_accuracy_den > 0` + > when `pm_prefetch_attempts > 0`; both operations increment `attempts` from 0 to 1 + > without ever having required `den > 0` beforehand, so the postcondition needs + > something the precondition never guaranteed. A genuine invariant-maintenance gap in + > `pm_wf`'s own definition, not fixed here. + > + > Toolchain: `/home/rajames/CLionProjects/Isabelle2011-1` now genuinely runs + > Isabelle2025-2 (old 2011 install preserved as `Isabelle2011-1.old`). Gitea Actions CI + > for this build remains wanted but unscoped (Captain Bob, see above) — not built yet. - [ ] **5.3 — Shrink the subsystem documents.** `ARTEMIS.md`, `HERMES.md`, `CONSOLE.md`, `TRIPOD.md` need trimming now that `FABRIC-2.md` (via `FABRIC.md`) is the design-of-record. diff --git a/proof/ACL_Emergency_Bypass.thy b/proof/ACL_Emergency_Bypass.thy index aa1553a..e1f933b 100644 --- a/proof/ACL_Emergency_Bypass.thy +++ b/proof/ACL_Emergency_Bypass.thy @@ -91,7 +91,7 @@ lemma denied_word_permitted_under_zuse: lemma either_bypass_sufficient: "(emergency_console vm = True \ zuse_session vm = True) \ acl_check_permits vm e = True" - by (simp add: acl_check_permits_def) + by (auto simp: acl_check_permits_def) (* Without either bypass, the word's own acl_allow is definitive. *) lemma no_bypass_check_follows_allow: diff --git a/proof/ACL_TTL_Bounded.thy b/proof/ACL_TTL_Bounded.thy index 1a53832..23f4820 100644 --- a/proof/ACL_TTL_Bounded.thy +++ b/proof/ACL_TTL_Bounded.thy @@ -57,7 +57,7 @@ definition acl_ttl_compute :: "nat \ nat" where (* Lower bound: result is always ≥ ACL_BASE_TTL. *) lemma acl_ttl_compute_ge_base: "acl_ttl_compute heat \ ACL_BASE_TTL" - by (simp add: acl_ttl_compute_def ACL_BASE_TTL_def) + by (simp add: acl_ttl_compute_def ACL_BASE_TTL_def ACL_MAX_TTL_def) (* Upper bound: result is always ≤ ACL_MAX_TTL. *) lemma acl_ttl_compute_le_max: diff --git a/proof/StarForth_Base.thy b/proof/StarForth_Base.thy index 546e5a2..35a534f 100644 --- a/proof/StarForth_Base.thy +++ b/proof/StarForth_Base.thy @@ -135,8 +135,9 @@ record dict_physics = (* ── Dictionary entry ────────────────────────────────────────────────────── *) (* ○ CODE-MUST-MATCH: struct DictEntry in include/vm.h ⚠ HUMAN-REVIEW: The C DictEntry stores a function pointer (word_func_t func). - This has been moved to word_table (a top-level vm_state field) to avoid the - type circularity vm_state → vm_state inside dict_entry. + This has been moved to word_table, a free-standing global constant declared + after vm_state (see "Word semantics table" section below) -- not a + vm_state field at all, which is what actually avoids the type circularity. Implementors: the C code must maintain a SEPARATE lookup table indexed by word_id that maps to word_func_t pointers — this is what word_table models. The dict_entry record here has no func field; look it up via word_table. *) @@ -301,7 +302,9 @@ record inference_outputs_state = □ dictionary / latest_id / here / dict_fence — dictionary state □ dict_lock / word_id_next — dict management □ vm_mode / vm_ip / state_var / vm_base / vm_error / vm_halted - □ word_table — function pointer table (C: per-DictEntry func ptr) + □ word_table — NOT a field of this record; see the + free-standing "consts word_table" declaration after this record, + function pointer table (C: per-DictEntry func ptr) □ heat_threshold_25th/50th/75th / last_bucket_reorg_ns / lookup_strategy □ rolling_window — all sub-fields including rw_act_window □ decay_slope_q48 / last_decay_check_ns / total_heat_at_check / ... @@ -358,20 +361,6 @@ record vm_state = vm_error :: bool vm_halted :: bool - (* ── Word semantics table ───────────────────────────────────────────── *) - (* ⚠ CRITICAL DESIGN NOTE: The C DictEntry stores word_func_t func, a function - pointer per word. Putting (vm_state ⇒ vm_state) inside dict_entry inside - vm_state creates a circular type in HOL. SOLUTION: the word function table - is a TOP-LEVEL field of vm_state, indexed by word_id. - - ○ CODE-MUST-MATCH: C implementors must maintain a PARALLEL array (or map) - from word_id → word_func_t that is logically equivalent to this field. - The dict_entry.func pointer in C can remain, but the proof framework - treats word_table as the authoritative semantic specification. - ⚠ HUMAN-REVIEW: Verify that for every word_id i, word_table i matches - exactly the behavior of the corresponding word_func_t function. *) - word_table :: "nat \ vm_state \ vm_state" - (* ── Physics Loop #1: Execution heat tracking ───────────────────────── *) (* ○ CODE-MUST-MATCH: heat_threshold_{25th,50th,75th} in C VM struct. ⚠ HUMAN-REVIEW: Thresholds are recomputed periodically by the heat bucket @@ -439,6 +428,32 @@ record vm_state = non-interference proof breaks. Verify in the SSM implementation. *) ssm_l8 :: ssm_l8_state +(* ========================================================================= + Word semantics table — deliberately NOT a vm_state field. + + CORRECTED 2026-08-13: the original design put word_table inside vm_state + with type "nat \ vm_state \ vm_state" -- self-referential (vm_state + naming itself in its own field's type) and rejected by every Isabelle + version, not just this one; HOL records have no fixed-point support. The + file's own prior comment claimed hoisting it to a "top-level field of + vm_state" solved the circularity -- it does not: the field's type still + names vm_state before vm_state exists. + + Fix: word_table is a free-standing, uninterpreted global constant, + declared here AFTER vm_state so there is no forward reference. This is + also more faithful to the C reality it models -- word_func_t dispatch is + a fixed table built once at compile time, not per-VM-instance mutable + state, so it never belonged inside vm_state's record in the first place. + Individual word_id entries are characterised by axioms in the per-word + theories (StarForth_Arithmetic_Words.thy etc.), not defined here. + + ○ CODE-MUST-MATCH: C implementors maintain the word_id \ word_func_t + dispatch table this constant models. See StarForth_Transition.thy's + word_physics_transparent axiom for the one property assumed of it: word + execution depends only on the exec-visible fields (data_stack, + return_stack, memory), never on physics state. *) +consts word_table :: "nat \ vm_state \ vm_state" + (* ========================================================================= Section 5: Well-formedness, error signalling, capacity predicates ======================================================================== *) @@ -515,7 +530,10 @@ definition rs_full :: "vm_state \ bool" where (* ⚠ CENTRAL CORRECTNESS MECHANISM: HOL record-update syntax vm⦇data_stack := xs⦈ proves that EVERY field not mentioned in the update (rolling_window, heartbeat, decay_slope_q48, - pipeline_metrics, dictionary, word_table, etc.) is EXACTLY unchanged. + pipeline_metrics, dictionary, etc.) is EXACTLY unchanged. word_table is + not in this list since 2026-08-13 -- it is no longer a vm_state field at + all (see above), so its independence from any vm_state update is true by + construction, stronger than a per-update lemma could state. This is how we mechanise "proof of correctness in totality with no assumptions" — no field is silently assumed unchanged; HOL record algebra guarantees it. @@ -555,8 +573,11 @@ lemma ds_update_preserves_dict: "dictionary (vm\data_stack := xs\) = dictionary vm" by simp -lemma ds_update_preserves_word_table: - "word_table (vm\data_stack := xs\) = word_table vm" - by simp +(* ds_update_preserves_word_table removed 2026-08-13: word_table is no + longer a vm_state field (see the "Word semantics table" section above), + so "word_table (vm\...\)" no longer type-checks -- there is nothing + left to state. word_table's independence from data_stack updates is now + true by construction (it is a fixed global, not read from vm at all), + not something requiring its own lemma. *) end diff --git a/proof/StarForth_Concurrent.thy b/proof/StarForth_Concurrent.thy index 0db5d36..502feea 100644 --- a/proof/StarForth_Concurrent.thy +++ b/proof/StarForth_Concurrent.thy @@ -21,53 +21,72 @@ begin theorem heartbeat_noninterference: "\n k vm. - data_stack (word_table (heartbeat_step ^^ k $ vm) n (heartbeat_step ^^ k $ vm)) - = data_stack (word_table vm n vm)" - by (simp add: exec_after_n_heartbeats_eq) + data_stack (word_table n ((heartbeat_step ^^ k) vm)) + = data_stack (word_table n vm)" + using exec_after_n_heartbeats_eq exec_equiv_ds by blast theorem heartbeat_noninterference_rs: "\n k vm. - return_stack (word_table (heartbeat_step ^^ k $ vm) n (heartbeat_step ^^ k $ vm)) - = return_stack (word_table vm n vm)" - by (simp add: exec_after_n_heartbeats_eq) + return_stack (word_table n ((heartbeat_step ^^ k) vm)) + = return_stack (word_table n vm)" + using exec_after_n_heartbeats_eq exec_equiv_rs by blast (* ========================================================================= Section 2: Trace-level non-interference (proved by induction over ≃) foldl_word_table_eq: if two initial states are exec-equivalent (≃), then - running any word sequence on each produces identical states. The proof is - structural: at each step word_physics_transparent (A4') gives FULL state - equality of the successors (not just exec-field agreement), so the remaining - foldl is trivially identical — no propagation of equivalence is needed. + running any word sequence on each produces exec-equivalent (not + identical -- CORRECTED 2026-08-13, see StarForth_Transition.thy's note + at word_physics_transparent for why full equality was never provable) + states. The proof is structural: at each step word_physics_transparent + (A4') gives ≃ of the successors, which is exactly what arbitrary: s1 s2 + needs to carry the induction through. heartbeat_trace_noninterference follows immediately by instantiating with - s1 = heartbeat_step ^^ k $ vm, s2 = vm, using heartbeat_n_exec_neutral. + s1 = (heartbeat_step ^^ k) vm, s2 = vm, using heartbeat_n_exec_neutral. ○ CODE-MUST-MATCH: the inductive argument holds only if word_physics_transparent holds for every word — see the audit protocol in StarForth_Transition.thy. ======================================================================== *) +(* Restated 2026-08-13 with explicit object-level \/\ instead of + assumes/shows + arbitrary: s1 s2 -- the assumes/arbitrary combination + was not reliably carrying "s1 \ s2" into the Nil case as Nil.prems + despite multiple tactics (simp, rule, metis with the fact named + explicitly all failed identically); this form sidesteps the whole + revert-and-generalize mechanism by quantifying s1/s2 in the goal from + the start. *) lemma foldl_word_table_eq: - assumes "s1 \ s2" - shows "foldl (\s n. word_table s n s) s1 ws - = foldl (\s n. word_table s n s) s2 ws" -proof (induction ws arbitrary: s1 s2) - case Nil thus ?case by simp + "\s1 s2. s1 \ s2 \ + foldl (\s n. word_table n s) s1 ws \ foldl (\s n. word_table n s) s2 ws" +proof (induction ws) + case Nil + show ?case by simp next case (Cons w ws) - (* A4' gives full state equality of the one-step successors *) - have heq: "word_table s1 w s1 = word_table s2 w s2" - by (rule word_physics_transparent [OF Cons.prems]) - show ?case by (simp add: heq) + show ?case + proof (intro allI impI) + fix s1 s2 :: vm_state + assume h: "s1 \ s2" + have heq: "word_table w s1 \ word_table w s2" + using h word_physics_transparent by blast + have "foldl (\s n. word_table n s) (word_table w s1) ws + \ foldl (\s n. word_table n s) (word_table w s2) ws" + using Cons.IH heq by blast + thus "foldl (\s n. word_table n s) s1 (w # ws) + \ foldl (\s n. word_table n s) s2 (w # ws)" + by simp + qed qed theorem heartbeat_trace_noninterference: "\ words vm k. data_stack - (foldl (\s n. word_table s n s) (heartbeat_step ^^ k $ vm) words) + (foldl (\s n. word_table n s) ((heartbeat_step ^^ k) vm) words) = data_stack - (foldl (\s n. word_table s n s) vm words)" - using foldl_word_table_eq [OF heartbeat_n_exec_neutral] by simp + (foldl (\s n. word_table n s) vm words)" + using foldl_word_table_eq [rule_format, OF heartbeat_n_exec_neutral] exec_equiv_ds + by blast (* ========================================================================= Section 3: Mutex safety (proved from lock_state algebra) @@ -97,12 +116,12 @@ lemma vm_step_preserves_lock_safety: lemma word_exec_deterministic: assumes "s1 \ s2" - shows "data_stack (word_table s1 n s1) = data_stack (word_table s2 n s2)" - using word_physics_transparent [OF assms] by simp + shows "data_stack (word_table n s1) = data_stack (word_table n s2)" + using word_physics_transparent [OF assms] exec_equiv_ds by blast lemma word_exec_rs_deterministic: assumes "s1 \ s2" - shows "return_stack (word_table s1 n s1) = return_stack (word_table s2 n s2)" - using word_physics_transparent [OF assms] by simp + shows "return_stack (word_table n s1) = return_stack (word_table n s2)" + using word_physics_transparent [OF assms] exec_equiv_rs by blast end diff --git a/proof/StarForth_Correctness.thy b/proof/StarForth_Correctness.thy index b9ba2a0..80ee997 100644 --- a/proof/StarForth_Correctness.thy +++ b/proof/StarForth_Correctness.thy @@ -28,15 +28,20 @@ begin heartbeat_step vm ≃ vm The heartbeat is the identity in vm_state/≃ (exec_equiv). C audit: src/vm_time.c vm_tick() must NOT write to - data_stack, return_stack, memory, or word_table. + data_stack, return_stack, or memory. (word_table dropped + from this list 2026-08-13: it is a free-standing global + constant now, not a vm_state field, so vm_tick() cannot + write to it at all.) The physics substate is unconstrained — the heartbeat may evolve it freely and non-monotonically. The former 8 field axioms are now proved lemmas from A1. A4'×1. word_physics_transparent (StarForth_Transition) - s1 ≃ s2 ⟹ word_table s1 n s1 = word_table s2 n s2 + s1 ≃ s2 ⟹ word_table n s1 ≃ word_table n s2 + (corrected 2026-08-13: conclusion is ≃, not literal + equality -- see the note at its declaration) Word execution is a congruence law for ≃. - Word audit: every Level 1 word body must read ONLY the four + Word audit: every Level 1 word body must read ONLY the three fields in exec_equiv — never any physics field. Physics invariants (A2/A3) remain removed — clamping suffices. @@ -59,14 +64,14 @@ thm swap_normal \ \✓ SWAP exchanges top two\ thm over_normal \ \✓ OVER copies second to top\ thm rot_normal \ \✓ ROT cycles top 3\ thm swap_involutive \ \✓ SWAP ∘ SWAP = identity\ -thm rot_neg_rot_identity \ \✓ ROT ∘ -ROT = identity\ +thm rot_nrot_inverse \ \✓ ROT ∘ -ROT = identity (corrected name, 2026-08-13)\ thm add_normal \ \✓ + pops 2, pushes sum\ -thm mul_comm \ \✓ * is commutative\ +thm mul_commutative \ \✓ * is commutative (corrected name, 2026-08-13)\ thm negate_involutive \ \✓ NEGATE ∘ NEGATE = identity\ -thm abs_non_negative \ \✓ ABS result ≥ 0\ +thm abs_nonneg \ \✓ ABS result ≥ 0 (corrected name, 2026-08-13)\ thm and_normal \ \✓ AND bitwise\ -thm zero_eq_true \ \✓ 0= of 0 is FORTH_TRUE\ -thm zero_lt_exhaustion \ \✓ {0=, 0<, 0>} partition ℤ\ +thm zero_eq_zero \ \✓ 0= of 0 is FORTH_TRUE (corrected name, 2026-08-13)\ +thm zero_tests_exhaustive \ \✓ {0=, 0<, 0>} partition ℤ (corrected name, 2026-08-13)\ thm to_r_then_from_r \ \✓ >R then R> round-trip\ thm store_then_fetch \ \✓ ! then @ identity\ thm cstore_then_cfetch \ \✓ C! then C@ round-trip\ @@ -83,8 +88,10 @@ lemma pure_ds_word_preserves_physics: "last_inference (vm\data_stack := xs\) = last_inference vm" "ssm_l8 (vm\data_stack := xs\) = ssm_l8 vm" "dictionary (vm\data_stack := xs\) = dictionary vm" - "word_table (vm\data_stack := xs\) = word_table vm" by simp_all +(* The word_table conjunct here was removed 2026-08-13: word_table is a + free-standing global constant now, not a vm_state field, so + "word_table (vm\...\)" no longer type-checks -- true by construction. *) (* ========================================================================= Section 3: Level 2 — Physics invariants (all ✓ or ○) @@ -125,11 +132,14 @@ theorem starforth_correctness_totality: fixes vm :: vm_state assumes wf: "wf_vm vm" shows - (* Level 1: key wf_vm invariants hold *) + (* Level 1: key wf_vm invariants hold. Level 2: physics invariants + from wf_vm (comment moved out here 2026-08-13 -- it was previously + embedded mid-string at the "rw_eff_window" line, which is inside a + quoted prop and does not parse as a comment there; genuine syntax + error, not a version issue). *) "length (data_stack vm) \ STACK_SIZE \ length (return_stack vm) \ STACK_SIZE \ \ vm_error vm \ - (* Level 2: physics invariants from wf_vm *) rw_eff_window (rolling_window vm) \ ADAPTIVE_MIN_WINDOW_SIZE \ rw_eff_window (rolling_window vm) \ ROLLING_WINDOW_SIZE \ rw_act_window (rolling_window vm) \ ROLLING_WINDOW_SIZE \ @@ -142,15 +152,15 @@ theorem starforth_correctness_totality: (* Corollary: non-interference for a word executed after k heartbeat ticks. *) corollary word_result_heartbeat_independent: "\ n k vm. - data_stack (word_table (heartbeat_step ^^ k $ vm) n (heartbeat_step ^^ k $ vm)) - = data_stack (word_table vm n vm)" + data_stack (word_table n ((heartbeat_step ^^ k) vm)) + = data_stack (word_table n vm)" using heartbeat_noninterference by blast (* Corollary: trace-level non-interference (proved theorem). *) corollary trace_result_heartbeat_independent: "\ words vm k. - data_stack (foldl (\s n. word_table s n s) (heartbeat_step ^^ k $ vm) words) - = data_stack (foldl (\s n. word_table s n s) vm words)" + data_stack (foldl (\s n. word_table n s) ((heartbeat_step ^^ k) vm) words) + = data_stack (foldl (\s n. word_table n s) vm words)" using heartbeat_trace_noninterference by blast end diff --git a/proof/StarForth_Logical_Words.thy b/proof/StarForth_Logical_Words.thy index 4be844c..076820f 100644 --- a/proof/StarForth_Logical_Words.thy +++ b/proof/StarForth_Logical_Words.thy @@ -2,6 +2,10 @@ theory StarForth_Logical_Words imports StarForth_Base begin +(* AND/OR/XOR infix notation moved behind an opt-in bundle at some point + after 2011 -- unbundled by default now. Same fix as StarForth_Q48_16.thy. *) +unbundle bit_operations_syntax + (* ========================================================================= POST-03: Logical and Comparison Words Mirrors: src/word_source/logical_words.c @@ -194,13 +198,13 @@ lemma zero_lt_negative: assumes "data_stack vm = n # xs" assumes "n < 0" shows "data_stack (forth_zero_lt vm) = (-1) # xs" - by (simp add: forth_zero_lt_def to_forth_bool_def forth_true_def assms) + using assms by (auto simp: forth_zero_lt_def to_forth_bool_def forth_true_def) lemma zero_lt_nonneg: assumes "data_stack vm = n # xs" assumes "n \ 0" shows "data_stack (forth_zero_lt vm) = 0 # xs" - by (simp add: forth_zero_lt_def to_forth_bool_def forth_false_def assms) + using assms by (auto simp: forth_zero_lt_def to_forth_bool_def forth_false_def) lemma zero_lt_underflow: assumes "data_stack vm = []" @@ -220,13 +224,13 @@ lemma zero_gt_positive: assumes "data_stack vm = n # xs" assumes "n > 0" shows "data_stack (forth_zero_gt vm) = (-1) # xs" - by (simp add: forth_zero_gt_def to_forth_bool_def forth_true_def assms) + using assms by (auto simp: forth_zero_gt_def to_forth_bool_def forth_true_def) lemma zero_gt_nonpos: assumes "data_stack vm = n # xs" assumes "n \ 0" shows "data_stack (forth_zero_gt vm) = 0 # xs" - by (simp add: forth_zero_gt_def to_forth_bool_def forth_false_def assms) + using assms by (auto simp: forth_zero_gt_def to_forth_bool_def forth_false_def) lemma zero_gt_underflow: assumes "data_stack vm = []" @@ -270,7 +274,7 @@ lemma eq_symmetric: assumes "data_stack vm = n2 # n1 # rest" assumes "data_stack vm' = n1 # n2 # rest" shows "data_stack (forth_eq vm) = data_stack (forth_eq vm')" - by (simp add: forth_eq_def assms) + by (simp add: forth_eq_def assms eq_commute) lemma eq_underflow_nil: assumes "data_stack vm = []" diff --git a/proof/StarForth_Loop1_Heat.thy b/proof/StarForth_Loop1_Heat.thy index a4590cb..b660494 100644 --- a/proof/StarForth_Loop1_Heat.thy +++ b/proof/StarForth_Loop1_Heat.thy @@ -2,6 +2,10 @@ theory StarForth_Loop1_Heat imports StarForth_Base begin +(* AND/OR/XOR infix notation moved behind an opt-in bundle at some point + after 2011 -- unbundled by default now. Same fix as StarForth_Q48_16.thy. *) +unbundle bit_operations_syntax + (* ========================================================================= StarForth_Loop1_Heat — Execution Heat Tracking (Physics Loop #1) @@ -60,25 +64,33 @@ definition heat_increment :: "dict_entry \ dict_entry" where lemma heat_increment_correct: assumes "de_heat e < HEAT_MAX" shows "de_heat (heat_increment e) = de_heat e + 1" - by (simp add: heat_increment_def assms) + using assms by (simp add: heat_increment_def min_def) lemma heat_increment_saturates: assumes "de_heat e = HEAT_MAX" shows "de_heat (heat_increment e) = HEAT_MAX" by (simp add: heat_increment_def assms) +(* CORRECTED 2026-08-13: added the missing upper-bound hypothesis. Without + it, if de_heat e already exceeds HEAT_MAX, the min-clamp in + heat_increment could pull the result back down below de_heat e, + breaking monotonicity. *) lemma heat_increment_non_decreasing: - "de_heat (heat_increment e) \ de_heat e" - by (simp add: heat_increment_def) + assumes "de_heat e \ HEAT_MAX" + shows "de_heat (heat_increment e) \ de_heat e" + using assms by (simp add: heat_increment_def) lemma heat_increment_preserves_validity: assumes "heat_valid e" shows "heat_valid (heat_increment e)" proof - - have "de_heat e \ 0" and "de_heat e \ HEAT_MAX" + have h0: "de_heat e \ 0" and hmax: "de_heat e \ HEAT_MAX" using assms by (simp_all add: heat_valid_def) - thus ?thesis - by (simp add: heat_valid_def heat_increment_def HEAT_MAX_def) + have le: "de_heat (heat_increment e) \ HEAT_MAX" + unfolding heat_increment_def by (simp add: min.cobounded2) + have ge: "de_heat (heat_increment e) \ 0" + unfolding heat_increment_def using h0 by (simp add: HEAT_MAX_def) + from le ge show ?thesis by (simp add: heat_valid_def) qed lemma heat_increment_preserves_flags: @@ -112,10 +124,18 @@ lemma heat_decay_frozen: shows "heat_decay amount e = e" by (simp add: heat_decay_def assms) +(* CORRECTED 2026-08-13: added the missing lower-bound hypothesis. In the + PINNED branch, heat_decay floors at max 1 (de_heat e - amount) -- if + de_heat e was already below 1 (e.g. 0), the floor raises it, breaking + monotonicity. de_heat e \ 1 is the standing invariant a pinned word is + supposed to maintain (see heat_decay_pinned_positive's own \ 1 + conclusion below), just never stated here as a precondition before. *) lemma heat_decay_monotone: assumes "\ heat_frozen e" + assumes "de_heat e \ 1" + assumes "amount \ 0" shows "de_heat (heat_decay amount e) \ de_heat e" - by (simp add: heat_decay_def assms) + using assms by (simp add: heat_decay_def) lemma heat_decay_non_negative: assumes "\ heat_frozen e" @@ -155,7 +175,7 @@ lemma heat_decay_preserves_flags: (* All dict entries reachable via the dictionary have valid heat. *) definition dict_heat_wf :: "vm_state \ bool" where "dict_heat_wf vm \ - \i e. dictionary vm i = Some e \ heat_valid e" + (\i e. dictionary vm i = Some e \ heat_valid e)" (* ========================================================================= Section 6: Heat thresholds diff --git a/proof/StarForth_Loop2_Window.thy b/proof/StarForth_Loop2_Window.thy index 5abecb0..65f5580 100644 --- a/proof/StarForth_Loop2_Window.thy +++ b/proof/StarForth_Loop2_Window.thy @@ -78,9 +78,17 @@ lemma window_advance_act_window: "rw_act_window (window_advance w rw) = min (rw_total_exec rw + 1) ROLLING_WINDOW_SIZE" by (simp add: window_advance_def) +(* CORRECTED 2026-08-13: added the missing window_invariant hypothesis. + Without it, rw_act_window rw is an unconstrained field unrelated to + rw_total_exec rw, so the claim is not provable -- nothing stops a + caller from handing in a state where rw_act_window is already larger + than the post-advance value. window_invariant is exactly what ties + rw_act_window to rw_total_exec (its defining formula), which is what + the proof actually needs. *) lemma window_advance_act_monotone: - "rw_act_window (window_advance w rw) \ rw_act_window rw" - by (simp add: window_advance_def min_def) + assumes "window_invariant rw" + shows "rw_act_window (window_advance w rw) \ rw_act_window rw" + using assms by (simp add: window_advance_def window_invariant_def min_def) lemma window_advance_act_bounded: "rw_act_window (window_advance w rw) \ ROLLING_WINDOW_SIZE" @@ -120,29 +128,50 @@ lemma window_shrink_lb: lemma window_shrink_ub: assumes "rw_eff_window rw \ ROLLING_WINDOW_SIZE" shows "rw_eff_window (window_shrink rw) \ ROLLING_WINDOW_SIZE" - using assms by (simp add: window_shrink_def) + using assms + by (simp add: window_shrink_def ROLLING_WINDOW_SIZE_def ADAPTIVE_MIN_WINDOW_SIZE_def) +(* CORRECTED 2026-08-13: added the missing lower-bound hypothesis. Without + it, rw_eff_window rw could be below ADAPTIVE_MIN_WINDOW_SIZE, in which + case window_shrink's max-clamp raises it back up to the floor -- the + result would then be \ the input, not \. window_invariant's own lower + bound is exactly what rules this out. *) lemma window_shrink_mono: - "rw_eff_window (window_shrink rw) \ rw_eff_window rw" - by (simp add: window_shrink_def) + assumes "rw_eff_window rw \ ADAPTIVE_MIN_WINDOW_SIZE" + shows "rw_eff_window (window_shrink rw) \ rw_eff_window rw" + using assms by (simp add: window_shrink_def) lemma window_shrink_preserves_invariant: assumes "window_invariant rw" shows "window_invariant (window_shrink rw)" - using assms by (simp add: window_invariant_def window_shrink_def) + using assms + by (auto simp: window_invariant_def window_shrink_def diff_le_self + intro: le_trans[OF diff_le_self]) lemma window_grow_lb: assumes "rw_eff_window rw \ ADAPTIVE_MIN_WINDOW_SIZE" shows "rw_eff_window (window_grow rw) \ ADAPTIVE_MIN_WINDOW_SIZE" - using assms by (simp add: window_grow_def) + using assms + by (simp add: window_grow_def ROLLING_WINDOW_SIZE_def ADAPTIVE_MIN_WINDOW_SIZE_def) lemma window_grow_ub: "rw_eff_window (window_grow rw) \ ROLLING_WINDOW_SIZE" - by (simp add: window_grow_def) +proof - + have "rw_eff_window (window_grow rw) + = min ROLLING_WINDOW_SIZE (rw_eff_window rw + ADAPTIVE_GROWTH_THRESHOLD)" + by (simp add: window_grow_def) + also have "\ \ ROLLING_WINDOW_SIZE" by (rule min.cobounded1) + finally show ?thesis . +qed +(* CORRECTED 2026-08-13: added the missing upper-bound hypothesis. Without + it, rw_eff_window rw could already exceed ROLLING_WINDOW_SIZE, in which + case window_grow's min-clamp would lower it -- the result would then be + \ the input, not \. *) lemma window_grow_mono: - "rw_eff_window (window_grow rw) \ rw_eff_window rw" - by (simp add: window_grow_def) + assumes "rw_eff_window rw \ ROLLING_WINDOW_SIZE" + shows "rw_eff_window (window_grow rw) \ rw_eff_window rw" + using assms by (simp add: window_grow_def) lemma window_grow_preserves_invariant: assumes "window_invariant rw" diff --git a/proof/StarForth_Loop3_Decay.thy b/proof/StarForth_Loop3_Decay.thy index 4a2e3db..c39c4fe 100644 --- a/proof/StarForth_Loop3_Decay.thy +++ b/proof/StarForth_Loop3_Decay.thy @@ -21,9 +21,11 @@ begin ======================================================================== *) (* ○ CODE-MUST-MATCH: Initial slope = 2 × Q48_SCALE = 131072. - Matches DECAY_RATE_PER_US_Q16 × 2 in include/vm.h. *) + Matches DECAY_RATE_PER_US_Q16 × 2 in include/vm.h. + CORRECTED 2026-08-13: was "2 * Q48_SCALE" directly -- Q48_SCALE :: q48 + (64 word), this constant is nat. Same unat fix as elsewhere. *) definition DECAY_SLOPE_INIT :: nat where - "DECAY_SLOPE_INIT = 2 * Q48_SCALE" + "DECAY_SLOPE_INIT = 2 * unat Q48_SCALE" (* ○ CODE-MUST-MATCH: Never let slope reach zero. ⚠ HUMAN-REVIEW: Every C code path that reduces decay_slope_q48 must clamp @@ -33,7 +35,7 @@ definition DECAY_SLOPE_MIN :: nat where "DECAY_SLOPE_MIN = 1" definition DECAY_SLOPE_MAX :: nat where - "DECAY_SLOPE_MAX = Q48_SCALE * 1000" + "DECAY_SLOPE_MAX = unat Q48_SCALE * 1000" (* ========================================================================= Section 2: Slope well-formedness @@ -69,7 +71,8 @@ lemma slope_decrease_lb: lemma slope_decrease_preserves_wf: assumes "slope_wf s" shows "slope_wf (slope_decrease step s)" - using assms by (simp add: slope_wf_def slope_decrease_def DECAY_SLOPE_MIN_def) + using assms + by (auto simp: slope_wf_def slope_decrease_def intro: le_trans[OF diff_le_self]) lemma slope_increase_ub: "slope_increase step s \ DECAY_SLOPE_MAX" @@ -80,11 +83,20 @@ lemma slope_increase_preserves_wf: shows "slope_wf (slope_increase step s)" using assms by (simp add: slope_wf_def slope_increase_def DECAY_SLOPE_MIN_def DECAY_SLOPE_MAX_def) -lemma slope_decrease_mono: "slope_decrease step s \ s" - by (simp add: slope_decrease_def) +(* CORRECTED 2026-08-13: added the missing slope_wf hypothesis. Without + "s \ DECAY_SLOPE_MIN", slope_decrease's max-clamp can raise a too-small + s back up above its own input (e.g. s=0, step=0 gives + max DECAY_SLOPE_MIN 0 = 1 > 0 = s), breaking the claim. Symmetric + argument for slope_increase_mono below. *) +lemma slope_decrease_mono: + assumes "s \ DECAY_SLOPE_MIN" + shows "slope_decrease step s \ s" + using assms by (simp add: slope_decrease_def) -lemma slope_increase_mono: "slope_increase step s \ s" - by (simp add: slope_increase_def) +lemma slope_increase_mono: + assumes "s \ DECAY_SLOPE_MAX" + shows "slope_increase step s \ s" + using assms by (simp add: slope_increase_def) (* ========================================================================= Section 4: VM decay step @@ -134,8 +146,8 @@ lemma vm_decay_step_dict [simp]: definition total_dict_heat :: "vm_state \ int" where "total_dict_heat vm = - \i \ {i. dictionary vm i \ None}. - de_heat (the (dictionary vm i))" + (\i \ {i. dictionary vm i \ None}. + de_heat (the (dictionary vm i)))" (* PROOF (no sorry): vm_decay_step only changes decay_slope_q48, so dictionary is identical @@ -149,7 +161,7 @@ lemma decay_step_dict_unchanged: lemma decay_total_heat_non_increasing: assumes "\i. dictionary vm i \ None \ de_heat (the (dictionary vm i)) \ 0" shows "total_dict_heat (vm_decay_step step vm) \ total_dict_heat vm" - using decay_step_dict_unchanged by linarith + by (simp add: decay_step_dict_unchanged) (* ========================================================================= Section 6: Well-formedness: slope is positive in wf_vm diff --git a/proof/StarForth_Loop4_Pipeline.thy b/proof/StarForth_Loop4_Pipeline.thy index 440f400..be62e50 100644 --- a/proof/StarForth_Loop4_Pipeline.thy +++ b/proof/StarForth_Loop4_Pipeline.thy @@ -23,28 +23,40 @@ begin Section 1: Pipeline accuracy ======================================================================== *) +(* CORRECTED 2026-08-13: was "* Q48_SCALE" directly -- Q48_SCALE :: q48 + (64 word), this function is nat. Same fix as StarForth_Loop5_WinInf.thy's + ANOVA_VARIANCE_THRESHOLD: unat Q48_SCALE converts to the equivalent nat. *) definition pm_accuracy_q48 :: "pipeline_metrics_state \ nat" where "pm_accuracy_q48 pm = (if pm_prefetch_attempts pm = 0 then 0 - else (pm_prefetch_hits pm * Q48_SCALE) div pm_prefetch_attempts pm)" + else (pm_prefetch_hits pm * unat Q48_SCALE) div pm_prefetch_attempts pm)" lemma pm_accuracy_zero_attempts [simp]: "pm_accuracy_q48 (pm\pm_prefetch_attempts := 0\) = 0" by (simp add: pm_accuracy_q48_def) +(* CORRECTED 2026-08-13: "\ Q48_ONE" was comparing nat to q48 (64 word) -- + a type error, could not have type-checked under any Isabelle version. + Fixed via unat Q48_ONE, same pattern as pm_accuracy_q48_def above. + Internal proof also fixed: Q48_SCALE needs unat for the same reason, and + div_le_iff_le_mult doesn't exist under this name any more (same finding + as StarForth_Q48_16.thy's q48_accuracy_upper_bound) -- replaced with the + same div_le_mono-based argument used there. *) lemma pm_accuracy_upper_bound: assumes "pm_prefetch_hits pm \ pm_prefetch_attempts pm" - shows "pm_accuracy_q48 pm \ Q48_ONE" + shows "pm_accuracy_q48 pm \ unat Q48_ONE" proof (cases "pm_prefetch_attempts pm = 0") case True thus ?thesis by (simp add: pm_accuracy_q48_def Q48_ONE_def) next case False - have "pm_prefetch_hits pm * Q48_SCALE \ pm_prefetch_attempts pm * Q48_SCALE" - using assms by (simp add: mult_le_mono1) - hence "(pm_prefetch_hits pm * Q48_SCALE) div pm_prefetch_attempts pm \ Q48_SCALE" - using False by (simp add: div_le_iff_le_mult) - thus ?thesis by (simp add: pm_accuracy_q48_def Q48_ONE_def False) + have "(pm_prefetch_hits pm * unat Q48_SCALE) div pm_prefetch_attempts pm + \ (pm_prefetch_attempts pm * unat Q48_SCALE) div pm_prefetch_attempts pm" + using assms by (intro div_le_mono mult_le_mono1) + also have "\ = unat Q48_SCALE" + using False by simp + finally show ?thesis + by (simp add: pm_accuracy_q48_def Q48_ONE_def False) qed lemma pm_accuracy_non_negative: @@ -65,8 +77,12 @@ definition pm_wf :: "pipeline_metrics_state \ bool" where lemma pm_wf_accuracy_range: assumes "pm_wf pm" - shows "pm_accuracy_q48 pm \ Q48_ONE" - using assms by (simp add: pm_accuracy_upper_bound pm_wf_def) + shows "pm_accuracy_q48 pm \ unat Q48_ONE" +proof - + have "pm_prefetch_hits pm \ pm_prefetch_attempts pm" + using assms by (simp add: pm_wf_def) + thus ?thesis by (rule pm_accuracy_upper_bound) +qed (* ========================================================================= Section 3: Recording a prefetch hit or miss @@ -97,15 +113,26 @@ lemma pm_record_miss_hits_unchanged: "pm_prefetch_hits (pm_record_miss pm) = pm_prefetch_hits pm" by (simp add: pm_record_miss_def) +(* FLAGGED, NOT FIXED 2026-08-13: pm_wf is not actually closed under + pm_record_hit/pm_record_miss as currently defined. pm_wf only requires + "pm_last_accuracy_den pm > 0" when pm_prefetch_attempts pm > 0 -- when + attempts = 0, den is completely unconstrained (could be 0). Both + pm_record_hit and pm_record_miss increment attempts from 0 to 1 without + touching pm_last_accuracy_den, so pm_wf's postcondition needs den > 0 + in a state where nothing in the precondition ever guaranteed it. Not a + proof-script issue -- a genuine gap in what pm_wf requires versus what + these two operations can establish. Left failing rather than silently + strengthening pm_wf's own definition (a design decision, not a + mechanical fix) or weakening these lemmas' claim. *) lemma pm_record_hit_preserves_wf: assumes "pm_wf pm" shows "pm_wf (pm_record_hit pm)" - using assms by (simp add: pm_wf_def pm_record_hit_def) + oops lemma pm_record_miss_preserves_wf: assumes "pm_wf pm" shows "pm_wf (pm_record_miss pm)" - using assms by (simp add: pm_wf_def pm_record_miss_def) + oops (* After a hit, hits ≤ attempts still holds. *) lemma pm_record_hit_hits_le_attempts: diff --git a/proof/StarForth_Loop5_WinInf.thy b/proof/StarForth_Loop5_WinInf.thy index b208c46..67fe78a 100644 --- a/proof/StarForth_Loop5_WinInf.thy +++ b/proof/StarForth_Loop5_WinInf.thy @@ -49,8 +49,14 @@ lemma inf_window_wf_ub: Section 2: ANOVA early-exit threshold ======================================================================== *) +(* CORRECTED 2026-08-13: was "= Q48_SCALE" directly -- Q48_SCALE :: q48 + (64 word) but this constant is nat (matching io_window_variance_q48's + type). A genuine type error, not library drift; this could not have + type-checked under any Isabelle version. Fixed via unat to convert the + word's value (65536) to the equivalent nat while keeping the same + intended numeric meaning (1.0 in Q48.16). *) definition ANOVA_VARIANCE_THRESHOLD :: nat where - "ANOVA_VARIANCE_THRESHOLD = Q48_SCALE" \ \1.0 in Q48.16 — matches C default\ + "ANOVA_VARIANCE_THRESHOLD = unat Q48_SCALE" \ \1.0 in Q48.16 — matches C default\ definition anova_early_exit :: "inference_outputs_state \ bool" where "anova_early_exit io \ diff --git a/proof/StarForth_Loop6_DecayInf.thy b/proof/StarForth_Loop6_DecayInf.thy index a19a383..221e754 100644 --- a/proof/StarForth_Loop6_DecayInf.thy +++ b/proof/StarForth_Loop6_DecayInf.thy @@ -29,7 +29,8 @@ definition clamp_slope_suggestion :: "nat \ nat" where lemma clamp_slope_wf: "slope_wf (clamp_slope_suggestion s)" - by (simp add: slope_wf_def clamp_slope_suggestion_def) + by (simp add: slope_wf_def clamp_slope_suggestion_def + DECAY_SLOPE_MIN_def DECAY_SLOPE_MAX_def Q48_SCALE_def) lemma clamp_slope_pos: "clamp_slope_suggestion s \ DECAY_SLOPE_MIN" diff --git a/proof/StarForth_Loop7_Heartrate.thy b/proof/StarForth_Loop7_Heartrate.thy index 0066902..f31e6ab 100644 --- a/proof/StarForth_Loop7_Heartrate.thy +++ b/proof/StarForth_Loop7_Heartrate.thy @@ -86,7 +86,9 @@ lemma hb_shorten_pos: lemma hb_shorten_preserves_wf: assumes "hb_state_wf hb" shows "hb_state_wf (hb_shorten_period delta hb)" - using assms by (simp add: hb_state_wf_def hb_shorten_period_def TICK_MAX_NS_def TICK_MIN_NS_def) + using assms + by (auto simp: hb_state_wf_def hb_shorten_period_def TICK_MAX_NS_def TICK_MIN_NS_def + intro: le_trans[OF diff_le_self]) lemma hb_lengthen_ub: "hb_tick_target_ns (hb_lengthen_period delta hb) \ TICK_MAX_NS" @@ -95,7 +97,7 @@ lemma hb_lengthen_ub: lemma hb_lengthen_preserves_pos: assumes "hb_tick_target_ns hb > 0" shows "hb_tick_target_ns (hb_lengthen_period delta hb) > 0" - using assms by (simp add: hb_lengthen_period_def) + using assms by (simp add: hb_lengthen_period_def TICK_MAX_NS_def) lemma hb_lengthen_preserves_wf: assumes "hb_state_wf hb" diff --git a/proof/StarForth_Memory_Words.thy b/proof/StarForth_Memory_Words.thy index 7e55622..144e6af 100644 --- a/proof/StarForth_Memory_Words.thy +++ b/proof/StarForth_Memory_Words.thy @@ -2,6 +2,10 @@ theory StarForth_Memory_Words imports StarForth_Base begin +(* AND/OR/XOR infix notation moved behind an opt-in bundle at some point + after 2011 -- unbundled by default now. Same fix as StarForth_Q48_16.thy. *) +unbundle bit_operations_syntax + (* ========================================================================= POST-05: Memory Access Words Mirrors: src/word_source/memory_words.c @@ -38,7 +42,7 @@ lemma mem_write_read_same: lemma mem_write_read_other: assumes "a \ b" shows "mem_read (mem_write mem a v) b = mem_read mem b" - by (simp add: mem_read_def mem_write_def assms) + using assms by (auto simp: mem_read_def mem_write_def) (* ── @ ( addr -- n ) ───────────────────────────────────────────────────── *) (* Pops addr from data stack, reads cell from memory at addr, pushes value. @@ -57,7 +61,7 @@ lemma fetch_normal: assumes "data_stack vm = addr # xs" assumes "addr \ 0" shows "data_stack (forth_fetch vm) = mem_read (memory vm) (nat addr) # xs" - by (simp add: forth_fetch_def assms) + using assms by (auto simp: forth_fetch_def) lemma fetch_reads_stored_value: assumes "memory vm = mem_write m a v" @@ -101,26 +105,26 @@ lemma store_normal: assumes "addr \ 0" shows "data_stack (forth_store vm) = xs" and "memory (forth_store vm) = mem_write (memory vm) (nat addr) n" - by (simp add: forth_store_def assms)+ + using assms by (auto simp: forth_store_def) lemma store_writes_value: assumes "data_stack vm = addr # n # xs" assumes "addr \ 0" shows "mem_read (memory (forth_store vm)) (nat addr) = n" - by (simp add: forth_store_def mem_write_def mem_read_def assms) + using assms by (auto simp: forth_store_def mem_write_def mem_read_def) lemma store_depth_decreases: assumes "data_stack vm = addr # n # xs" assumes "addr \ 0" shows "length (data_stack (forth_store vm)) = length (data_stack vm) - 2" - by (simp add: forth_store_def assms) + using assms by (auto simp: forth_store_def) lemma store_other_unchanged: assumes "data_stack vm = addr # n # xs" assumes "addr \ 0" assumes "nat addr \ b" shows "mem_read (memory (forth_store vm)) b = mem_read (memory vm) b" - by (simp add: forth_store_def mem_write_def mem_read_def assms) + using assms by (auto simp: forth_store_def mem_write_def mem_read_def) lemma store_underflow_nil: assumes "data_stack vm = []" @@ -147,7 +151,7 @@ lemma store_then_fetch: assumes "memory vm' = memory (forth_store vm)" assumes "addr \ 0" shows "hd (data_stack (forth_fetch vm')) = n" - by (simp add: forth_fetch_def forth_store_def mem_write_def mem_read_def assms) + using assms by (auto simp: forth_fetch_def forth_store_def mem_write_def mem_read_def) (* ── C@ ( addr -- c ) ──────────────────────────────────────────────────── *) (* Reads a single byte (0..255) from memory, zero-extended to cell width. @@ -169,14 +173,14 @@ lemma cfetch_normal: assumes "addr \ 0" shows "data_stack (forth_cfetch vm) = (mem_read (memory vm) (nat addr) AND 0xFF) # xs" - by (simp add: forth_cfetch_def assms) + using assms by (auto simp: forth_cfetch_def) lemma cfetch_byte_range: assumes "data_stack vm = addr # xs" assumes "addr \ 0" shows "0 \ hd (data_stack (forth_cfetch vm))" and "hd (data_stack (forth_cfetch vm)) \ 255" - by (simp add: forth_cfetch_def assms)+ + using assms by (auto simp: forth_cfetch_def) lemma cfetch_underflow: assumes "data_stack vm = []" @@ -208,19 +212,19 @@ lemma cstore_normal: assumes "addr \ 0" shows "data_stack (forth_cstore vm) = xs" and "memory (forth_cstore vm) = mem_write (memory vm) (nat addr) (c AND 0xFF)" - by (simp add: forth_cstore_def assms)+ + using assms by (auto simp: forth_cstore_def) lemma cstore_writes_byte: assumes "data_stack vm = addr # c # xs" assumes "addr \ 0" shows "mem_read (memory (forth_cstore vm)) (nat addr) = c AND 0xFF" - by (simp add: forth_cstore_def mem_write_def mem_read_def assms) + using assms by (auto simp: forth_cstore_def mem_write_def mem_read_def) lemma cstore_depth_decreases: assumes "data_stack vm = addr # c # xs" assumes "addr \ 0" shows "length (data_stack (forth_cstore vm)) = length (data_stack vm) - 2" - by (simp add: forth_cstore_def assms) + using assms by (auto simp: forth_cstore_def) lemma cstore_underflow_nil: assumes "data_stack vm = []" @@ -245,6 +249,6 @@ lemma cstore_then_cfetch: assumes "data_stack vm' = addr # xs" assumes "memory vm' = memory (forth_cstore vm)" shows "hd (data_stack (forth_cfetch vm')) = c AND 0xFF" - by (simp add: forth_cfetch_def forth_cstore_def mem_write_def mem_read_def assms) + using assms by (auto simp: forth_cfetch_def forth_cstore_def mem_write_def mem_read_def) end diff --git a/proof/StarForth_Mutex.thy b/proof/StarForth_Mutex.thy index 2e82305..a2a3fa7 100644 --- a/proof/StarForth_Mutex.thy +++ b/proof/StarForth_Mutex.thy @@ -104,18 +104,18 @@ lemma lock_wf_held: lemma acquire_preserves_wf: assumes "lock_wf s" "valid_thread t" shows "lock_wf (acquire_lock t s)" - by (cases s; simp add: acquire_lock_def lock_wf_def assms) + using assms by (cases s; simp add: acquire_lock_def lock_wf_def) lemma release_preserves_wf: assumes "lock_wf s" shows "lock_wf (release_lock t s)" - by (cases s; simp add: release_lock_def lock_wf_def assms) + using assms by (cases s; simp add: release_lock_def lock_wf_def) (* Two distinct threads cannot both hold the same lock. *) lemma mutex_exclusive: assumes "lock_held_by t s" "lock_held_by u s" shows "t = u" - by (cases s; simp add: lock_held_by_def assms; blast) + using assms by (cases s; simp add: lock_held_by_def) (* ========================================================================= Section 5: VM-level lock accessors diff --git a/proof/StarForth_Q48_16.thy b/proof/StarForth_Q48_16.thy index 91a4337..46a5f50 100644 --- a/proof/StarForth_Q48_16.thy +++ b/proof/StarForth_Q48_16.thy @@ -2,6 +2,11 @@ theory StarForth_Q48_16 imports "HOL-Library.Word" begin +(* AND/OR/XOR infix notation moved behind an opt-in bundle at some point after + 2011 -- unbundled by default now to avoid clashing with other uses of the + same tokens. q48_frac_part below needs it. *) +unbundle bit_operations_syntax + (* ========================================================================= StarForth_Q48_16 — Q48.16 Fixed-Point Arithmetic (HOL-Word model) @@ -58,9 +63,15 @@ definition q48_to_u64 :: "q48 \ 64 word" where lemma q48_round_trip: assumes "unat n < 2 ^ 48" shows "q48_to_u64 (q48_from_u64 n) = n" - unfolding q48_to_u64_def q48_from_u64_def - using assms - by (simp add: drop_bit_push_bit word_size) +proof - + have "unat n * 65536 < 2 ^ 64" using assms by simp + hence h: "unat (n * 65536) = unat n * 65536" + using unat_mult_lem[of n "65536::q48"] by simp + show ?thesis + unfolding q48_to_u64_def q48_from_u64_def + by (simp add: word_unat_eq_iff push_bit_eq_mult drop_bit_eq_div + unat_div_distrib h) +qed lemma q48_from_u64_zero [simp]: "q48_from_u64 0 = 0" by (simp add: q48_from_u64_def) @@ -68,11 +79,26 @@ lemma q48_from_u64_zero [simp]: "q48_from_u64 0 = 0" lemma q48_to_u64_zero [simp]: "q48_to_u64 0 = 0" by (simp add: q48_to_u64_def) +(* CORRECTED 2026-08-13: the original statement had no upper bound and is + false as such -- push_bit 16 wraps mod 2^64, so e.g. a=1, b=2^48 satisfies + unat a \ unat b (1 \ 2^48) while push_bit 16 a = 65536 and push_bit 16 b + wraps to 0, breaking the conclusion. Added the same "unat _ < 2^48 + overflow-free range" bound this file already uses everywhere else. *) lemma q48_from_u64_mono: - assumes "unat a \ unat b" + assumes "unat a \ unat b" and "unat b < 2 ^ 48" shows "unat (q48_from_u64 a) \ unat (q48_from_u64 b)" - unfolding q48_from_u64_def - using assms by (simp add: unat_push_bit) +proof - + have ha: "unat a < 2 ^ 48" using assms by simp + have hb64: "unat b * 65536 < 2 ^ 64" using assms(2) by simp + have ha64: "unat a * 65536 < 2 ^ 64" using ha by simp + have eb: "unat (b * 65536) = unat b * 65536" + using unat_mult_lem[of b "65536::q48"] hb64 by simp + have ea: "unat (a * 65536) = unat a * 65536" + using unat_mult_lem[of a "65536::q48"] ha64 by simp + show ?thesis + unfolding q48_from_u64_def + by (simp add: push_bit_eq_mult ea eb assms(1)) +qed (* ========================================================================= Section 3: Arithmetic operations @@ -117,9 +143,14 @@ lemma q48_mul_zero_left [simp]: "q48_mul 0 a = 0" lemma q48_mul_one_right: assumes "unat a < 2 ^ 48" shows "q48_mul a Q48_ONE = a" - unfolding q48_mul_def Q48_ONE_def Q48_SCALE_def - using assms - by (simp add: drop_bit_push_bit word_size) +proof - + have "unat a * 65536 < 2 ^ 64" using assms by simp + hence h: "unat (a * 65536) = unat a * 65536" + using unat_mult_lem[of a "65536::q48"] by simp + show ?thesis + unfolding q48_mul_def Q48_ONE_def Q48_SCALE_def + by (simp add: word_unat_eq_iff drop_bit_eq_div unat_div_distrib h) +qed (* q48_div: (a << 16) / b C: return ((__uint128_t)a << 16) / b; @@ -130,10 +161,21 @@ definition q48_div :: "q48 \ q48 \ q48" where lemma q48_div_zero_denom [simp]: "q48_div a 0 = 0" by (simp add: q48_div_def) +(* CORRECTED 2026-08-13: the original statement had no bound and is false + as such -- push_bit 16 wraps mod 2^64, so e.g. a=2^48 gives push_bit 16 a + = 0, so q48_div a Q48_ONE = 0 \ a. Added the same overflow-free bound + used throughout this file. *) lemma q48_div_one: - "q48_div a Q48_ONE = a" - unfolding q48_div_def Q48_ONE_def Q48_SCALE_def - by simp + assumes "unat a < 2 ^ 48" + shows "q48_div a Q48_ONE = a" +proof - + have "unat a * 65536 < 2 ^ 64" using assms by simp + hence h: "unat (a * 65536) = unat a * 65536" + using unat_mult_lem[of a "65536::q48"] by simp + show ?thesis + unfolding q48_div_def Q48_ONE_def Q48_SCALE_def + by (simp add: word_unat_eq_iff push_bit_eq_mult unat_div_distrib h) +qed (* ========================================================================= Section 4: Accuracy ratio in Q48.16 (used by Loop #4 / Loop #5) @@ -142,24 +184,27 @@ lemma q48_div_one: (* Prefetch accuracy: hits / total, represented in Q48.16. Arguments are natural numbers (counters); result is a 64 word. *) definition q48_accuracy :: "nat \ nat \ q48" where - "q48_accuracy hits total = - (if total = 0 then 0 - else word_of_nat ((hits * 65536) div total))" + "q48_accuracy hits tot = + (if tot = 0 then 0 + else word_of_nat ((hits * 65536) div tot))" lemma q48_accuracy_zero_total [simp]: "q48_accuracy hits 0 = 0" by (simp add: q48_accuracy_def) lemma q48_accuracy_upper_bound: - assumes "hits \ total" - shows "unat (q48_accuracy hits total) \ 65536" -proof (cases "total = 0") + assumes "hits \ tot" + shows "unat (q48_accuracy hits tot) \ 65536" +proof (cases "tot = 0") case True thus ?thesis by simp next case False - have "(hits * 65536) div total \ 65536" - using assms False by (simp add: div_le_iff_le_mult) + have "(hits * 65536) div tot \ (tot * 65536) div tot" + using assms by (intro div_le_mono) simp + also have "\ = 65536" + using False by simp + finally have "(hits * 65536) div tot \ 65536" . thus ?thesis - by (simp add: q48_accuracy_def False unat_word_of_nat) + by (simp add: q48_accuracy_def False unat_of_nat) qed (* ========================================================================= @@ -177,7 +222,15 @@ definition q48_frac_part :: "q48 \ 64 word" where lemma q48_decompose: "push_bit 16 (q48_int_part q) + q48_frac_part q = q" unfolding q48_int_part_def q48_frac_part_def - by (simp add: push_bit_drop_bit_and_not_mask_eq and_mask_eq_iff_shiftr_0 - bit_push_bit drop_bit_eq_div push_bit_eq_mult) +proof - + have disj: "push_bit 16 (drop_bit 16 q) AND (q AND mask 16) = 0" + by (rule bit_word_eqI) (auto simp: bit_simps) + have "push_bit 16 (drop_bit 16 q) + (q AND mask 16) + = push_bit 16 (drop_bit 16 q) OR (q AND mask 16)" + by (rule disjunctive_add_eq_or) (rule disj) + also have "\ = q" + by (rule bit_word_eqI) (auto simp: bit_simps) + finally show "push_bit 16 (drop_bit 16 q) + (q AND mask 16) = q" . +qed end diff --git a/proof/StarForth_Return_Stack_Words.thy b/proof/StarForth_Return_Stack_Words.thy index fdd7c6b..81e5d2d 100644 --- a/proof/StarForth_Return_Stack_Words.thy +++ b/proof/StarForth_Return_Stack_Words.thy @@ -152,9 +152,9 @@ proof - have no_ds_full: "\ ds_full (forth_to_r vm)" using assms(3) by simp show "data_stack (forth_from_r (forth_to_r vm)) = data_stack vm" - by (simp add: forth_from_r_def forth_to_r_def rs ds no_ds_full assms) + using rs ds no_ds_full assms by (simp add: forth_from_r_def) show "return_stack (forth_from_r (forth_to_r vm)) = return_stack vm" - by (simp add: forth_from_r_def forth_to_r_def rs ds no_ds_full assms) + using rs ds no_ds_full assms by (simp add: forth_from_r_def) qed (* >R then R@ preserves the return stack and pushes a copy to data stack. *) @@ -168,9 +168,9 @@ proof - have rs: "return_stack (forth_to_r vm) = x # return_stack vm" by (simp add: forth_to_r_def assms) show "hd (data_stack (forth_r_fetch (forth_to_r vm))) = x" - by (simp add: forth_r_fetch_def forth_to_r_def rs assms) + using rs assms by (simp add: forth_r_fetch_def) show "return_stack (forth_r_fetch (forth_to_r vm)) = x # return_stack vm" - by (simp add: forth_r_fetch_def forth_to_r_def rs assms) + using rs assms by (simp add: forth_r_fetch_def) qed end diff --git a/proof/StarForth_Stack_Words.thy b/proof/StarForth_Stack_Words.thy index 1f024b0..95d812c 100644 --- a/proof/StarForth_Stack_Words.thy +++ b/proof/StarForth_Stack_Words.thy @@ -343,7 +343,7 @@ lemma pick_normal: assumes "n \ 0" assumes "nat n < length (data_stack vm)" shows "data_stack (forth_pick vm) = data_stack vm ! nat n # xs" - by (simp add: forth_pick_def assms) + using assms by (auto simp: forth_pick_def) lemma pick_depth_unchanged: assumes "data_stack vm = n # xs" @@ -380,7 +380,7 @@ lemma pick_bounds_high: assumes "data_stack vm = n # xs" assumes "nat n \ length (data_stack vm)" shows "vm_error (forth_pick vm)" - by (simp add: forth_pick_def set_error_def assms) + using assms by (auto simp: forth_pick_def set_error_def) (* ── ROLL ( +n -- ) ─────────────────────────────────────────────────────── *) (* Pops n, then rotates items. @@ -407,8 +407,8 @@ definition forth_roll :: "vm_state \ vm_state" where then set_error vm else if n = 0 \ n = 1 then vm\data_stack := xs\ - else let i = nat n - item = xs ! (i - 1) + else let i = nat n; + item = xs ! (i - 1); rest = take (i - 1) xs @ drop i xs in vm\data_stack := item # rest\)" @@ -417,16 +417,37 @@ lemma roll_zero_nop: shows "data_stack (forth_roll vm) = xs" by (simp add: forth_roll_def assms) +(* CORRECTED 2026-08-13: added the missing "xs non-empty" hypothesis. For + n=1 with xs=[], forth_roll_def's own guard (nat n > length xs, i.e. + 1 > 0) fires BEFORE the n=0\n=1 shortcut is reached, giving set_error + instead of the identity -- so the claim is false for xs=[]. *) lemma roll_one_nop: assumes "data_stack vm = 1 # xs" + assumes "xs \ []" shows "data_stack (forth_roll vm) = xs" - by (simp add: forth_roll_def assms) + using assms by (auto simp: forth_roll_def) -(* 2 ROLL is equivalent to ROT (bring third item to top). *) +(* FLAGGED, NOT FIXED 2026-08-13: this lemma does not hold against + forth_roll_def as currently written. Tracing the definition by hand for + this exact instantiation (xs = n3#n2#n1#rest after popping the leading + 2) gives item = xs!(i-1) = xs!1 = n2, rest' = take 1 xs @ drop 2 xs = + n3#n1#rest, so forth_roll actually produces n2#n3#n1#rest -- not + n1#n3#n2#rest as this lemma (and its own "2 ROLL is equivalent to ROT" + comment) claims. Separately, the real C stack_word_roll + (src/word_source/stack_words.c:287-320) uses yet a THIRD convention of + its own, explicitly commented "1-indexed from bottom: n=1 moves bottom + item to top" -- neither this definition nor this lemma's expectation + matches it. Three mutually inconsistent conventions (this definition, + this lemma, and the C code) -- not a proof-script issue, a genuine + unresolved semantic question about what ROLL is supposed to do. This + theory's own header asserts the theory is ground truth and the C code + must match it, but the theory does not even agree with itself here, so + that framing does not resolve which side (if either) is correct. + Left failing rather than silently reconciled either direction. *) lemma roll_two_is_rot: assumes "data_stack vm = 2 # n3 # n2 # n1 # rest" shows "data_stack (forth_roll vm) = n1 # n3 # n2 # rest" - by (simp add: forth_roll_def assms) + oops lemma roll_underflow: assumes "data_stack vm = []" diff --git a/proof/StarForth_Transition.thy b/proof/StarForth_Transition.thy index 69d1d2a..24b2074 100644 --- a/proof/StarForth_Transition.thy +++ b/proof/StarForth_Transition.thy @@ -49,12 +49,16 @@ type_synonym event = "thread \ action" well-defined endomorphism. ======================================================================== *) +(* word_table dropped from exec_equiv 2026-08-13: it is no longer a + vm_state field (StarForth_Base.thy fixed the vm_state self-reference by + making word_table a free-standing global constant), so "word_table s1 = + word_table s2" no longer type-checks -- and would have been vacuously + true anyway, since a global constant cannot differ between s1 and s2. *) definition exec_equiv :: "vm_state \ vm_state \ bool" (infix "\" 50) where "s1 \ s2 \ data_stack s1 = data_stack s2 \ return_stack s1 = return_stack s2 \ - memory s1 = memory s2 \ - word_table s1 = word_table s2" + memory s1 = memory s2" lemma exec_equiv_refl [simp, intro]: "vm \ vm" by (simp add: exec_equiv_def) @@ -68,7 +72,8 @@ lemma exec_equiv_trans: "s1 \ s2 \ s2 \ s3 \ s2 \ data_stack s1 = data_stack s2" by (simp add: exec_equiv_def) lemma exec_equiv_rs: "s1 \ s2 \ return_stack s1 = return_stack s2" by (simp add: exec_equiv_def) lemma exec_equiv_mem:"s1 \ s2 \ memory s1 = memory s2" by (simp add: exec_equiv_def) -lemma exec_equiv_wt: "s1 \ s2 \ word_table s1 = word_table s2" by (simp add: exec_equiv_def) +(* exec_equiv_wt removed 2026-08-13: word_table is global now, not read + from state, so this fact no longer type-checks and is not needed. *) (* ========================================================================= Section 3: Heartbeat axiom — A1 ×1 (collapsed from ×8) @@ -87,12 +92,14 @@ lemma exec_equiv_wt: "s1 \ s2 \ word_table s1 = word_ta Read every code path reachable from vm_tick() — including vm_tick_window_tuner, vm_tick_slope_validator, and all inference_engine.c callees — and verify that NONE of those paths write - to the following four fields: + to the following three fields: data_stack (vm->data_stack / vm->ds_top) return_stack (vm->return_stack / vm->rs_top) memory (vm->memory[]) - word_table (vm->word_table) - Those four fields are exactly exec_equiv. Everything else is free. + Those three fields are exactly exec_equiv. word_table is no longer + among them (2026-08-13: it is a free-standing global constant, not a + vm_state field, so it cannot be written by any vm_tick() path at all). + Everything else is free. ○ CODE-MUST-MATCH: if a future refactor moves any of those four fields into the heartbeat's write set, exec_equiv must be updated and a new audit @@ -118,77 +125,100 @@ lemma heartbeat_rs [simp]: "return_stack (heartbeat_step vm) = return_stack vm" lemma heartbeat_mem [simp]: "memory (heartbeat_step vm) = memory vm" using heartbeat_exec_neutral by (simp add: exec_equiv_def) -lemma heartbeat_wt [simp]: "word_table (heartbeat_step vm) = word_table vm" - using heartbeat_exec_neutral by (simp add: exec_equiv_def) +(* heartbeat_wt removed 2026-08-13: word_table no longer varies by state. *) (* ========================================================================= Section 5: n-fold heartbeat exec-neutrality and field preservation ======================================================================== *) -lemma heartbeat_n_exec_neutral: "heartbeat_step ^^ n $ vm \ vm" +lemma heartbeat_n_exec_neutral: "(heartbeat_step ^^ n) vm \ vm" proof (induction n) case 0 show ?case by simp next case (Suc k) - show "heartbeat_step ^^ Suc k $ vm \ vm" + show "(heartbeat_step ^^ Suc k) vm \ vm" using exec_equiv_trans [OF heartbeat_exec_neutral Suc.IH] by simp qed -lemma heartbeat_n_steps_ds [simp]: "data_stack (heartbeat_step ^^ n $ vm) = data_stack vm" +lemma heartbeat_n_steps_ds [simp]: "data_stack ((heartbeat_step ^^ n) vm) = data_stack vm" using heartbeat_n_exec_neutral by (simp add: exec_equiv_def) -lemma heartbeat_n_steps_rs [simp]: "return_stack (heartbeat_step ^^ n $ vm) = return_stack vm" +lemma heartbeat_n_steps_rs [simp]: "return_stack ((heartbeat_step ^^ n) vm) = return_stack vm" using heartbeat_n_exec_neutral by (simp add: exec_equiv_def) -lemma heartbeat_n_steps_mem [simp]: "memory (heartbeat_step ^^ n $ vm) = memory vm" +lemma heartbeat_n_steps_mem [simp]: "memory ((heartbeat_step ^^ n) vm) = memory vm" using heartbeat_n_exec_neutral by (simp add: exec_equiv_def) -lemma heartbeat_n_steps_wt [simp]: "word_table (heartbeat_step ^^ n $ vm) = word_table vm" - using heartbeat_n_exec_neutral by (simp add: exec_equiv_def) +(* heartbeat_n_steps_wt removed 2026-08-13: word_table no longer varies by + state -- see the note at heartbeat_wt above. *) (* ========================================================================= Section 6: Word physics transparency — A4' ×1 (congruence form) Word execution is a well-defined endomorphism on the exec quotient: if two - states are exec-equivalent, executing any word on each produces identical - results. This is the congruence law that makes word sequences independent - of interleaved heartbeat ticks. + states are exec-equivalent, executing any word on each produces + exec-equivalent results. This is the congruence law that makes word + sequences independent of interleaved heartbeat ticks. + + CORRECTED 2026-08-13: the conclusion was full state equality + ("word_table n s1 = word_table n s2"), not \-equivalence. That is + provably too strong and was never true: two states agreeing only on the + three exec_equiv fields can differ in any physics field (rolling_window, + heartbeat, etc.), and a word that never reads or writes those physics + fields leaves them exactly as it found them -- still different between + the two output states. Concretely, this broke + StarForth_Concurrent.thy's foldl_word_table_eq at the empty-list base + case, which reduced to needing s1 = s2 from s1 \ s2 alone -- genuinely + unprovable. The audit protocol below only ever justified the \ form: + "the word body only reads the three exec_equiv fields" gives identical + NEW data_stack/return_stack/memory (since those three inputs agree by + \), but says nothing about physics fields the word doesn't touch, + which simply carry through from s1/s2 respectively and so can still + differ. \ is exactly the right conclusion strength -- it is silent + about physics fields, which is what the design has always wanted. ⚠ AUDIT PROTOCOL: for each word registered in word_table, verify its body - only reads data_stack, return_stack, memory, word_table — the four fields - of exec_equiv. These are exactly the fields a FORTH word may observe. + only reads data_stack, return_stack, memory — the three fields of + exec_equiv (word_table itself is no longer one of them since 2026-08-13; + it is a fixed global, not part of state to read). These are exactly the + fields a FORTH word may observe. ○ CODE-MUST-MATCH: no word in src/word_source/ may read rolling_window, heartbeat, decay_slope_q48, pipeline_metrics, last_inference, ssm_l8, tuning_lock, dict_lock, heat thresholds, or any other physics field. ======================================================================== *) +(* word_table's arity dropped from 3 to 2 call-site arguments 2026-08-13: + it used to be read from a specific state first (word_table s n s -- get + s's own copy of the table, apply entry n to s), now it is one fixed + global table (word_table n s -- apply entry n directly to s). The + mathematical content of this axiom (word execution depends only on the + exec-visible fields, not physics state) is unchanged. *) axiomatization where word_physics_transparent: "\ (s1 :: vm_state) (s2 :: vm_state) n. - s1 \ s2 \ word_table s1 n s1 = word_table s2 n s2" + s1 \ s2 \ word_table n s1 \ word_table n s2" (* ========================================================================= Section 7: Consequences — all proved from A1 + A4' ======================================================================== *) lemma exec_after_heartbeat_eq: - "word_table (heartbeat_step vm) n (heartbeat_step vm) = word_table vm n vm" + "word_table n (heartbeat_step vm) \ word_table n vm" by (rule word_physics_transparent [OF heartbeat_exec_neutral]) lemma exec_after_heartbeat_ds: - "data_stack (word_table (heartbeat_step vm) n (heartbeat_step vm)) - = data_stack (word_table vm n vm)" - using exec_after_heartbeat_eq by simp + "data_stack (word_table n (heartbeat_step vm)) + = data_stack (word_table n vm)" + using exec_after_heartbeat_eq exec_equiv_ds by blast lemma exec_after_heartbeat_rs: - "return_stack (word_table (heartbeat_step vm) n (heartbeat_step vm)) - = return_stack (word_table vm n vm)" - using exec_after_heartbeat_eq by simp + "return_stack (word_table n (heartbeat_step vm)) + = return_stack (word_table n vm)" + using exec_after_heartbeat_eq exec_equiv_rs by blast lemma exec_after_n_heartbeats_eq: - "word_table (heartbeat_step ^^ k $ vm) n (heartbeat_step ^^ k $ vm) - = word_table vm n vm" + "word_table n ((heartbeat_step ^^ k) vm) \ word_table n vm" by (rule word_physics_transparent [OF heartbeat_n_exec_neutral]) (* ========================================================================= @@ -200,7 +230,7 @@ inductive vm_step :: "vm_state \ event \ vm_state \ vm_error vm \ \ vm_halted vm \ - vm' = word_table vm n vm \ + vm' = word_table n vm \ vm \[(ExecThread, ExecWord n)] vm'" | StepHeartTick: