Robert Allan JamesandClaude Sonnet 5
d59a913e13
Adds de_df :: cell to dict_entry (StarForth_Base.thy) -- the DF cell modelled as a plain value, closing gap (b) for every word that only reads/writes it through its OWNING entry. Confirmed by grep this record has exactly one construction site in the whole 52-theory suite (dict_insert_entry), so the field addition's blast radius is contained to StarForth_Defining_Words.thy alone -- full suite still verifies unchanged elsewhere. dict_write_df writes an existing entry's DF by word_id. forth_create_full/ forth_variable_full/forth_constant_full now compose the DF write in, making CREATE/VARIABLE/CONSTANT the first three FULLY modelled words in this file (guard through parse through insertion through the DF write -- nothing left unmodelled per word except the pin-shadow name-scan guard, sidestepped the same way as everywhere else in this suite). Their runtime companions (defining_runtime_create/_variable/_constant -- confirmed byte-identical C bodies) share one new definition, forth_runtime_read_df, gated on ds_full matching vm_push's real internal check. Required adding current_executing_word_id to vm_state (mirrors vm->current_executing_entry, word-id-indexed like latest_id). DEFER and : remain at their previous closure level: DEFER's DF write was already implicitly closed (de_df=0 at creation matches its explicit *df=0), but its own runtime is a fundamentally different DF usage (dispatch reassignment via a stored pointer, gap c, not a plain value); : has no vm_state field for vm->compiling_word tracking. Full suite (54 theories) verifies green. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
proof/
Isabelle/HOL theory files providing machine-checkable proofs of determinism and correctness for StarForth. 24 theory files covering all 7 feedback loops, core word categories, and the word-level ACL system.
Running proofs
isabelle build -D proof/
Requires an Isabelle installation. See docs/01-getting-started/DEVELOPER.md.
Theory files
Foundations
| File | Covers |
|---|---|
StarForth_Base.thy |
Base definitions and type system |
StarForth_Correctness.thy |
Overall correctness |
StarForth_Transition.thy |
State transitions |
StarForth_Concurrent.thy |
Concurrency properties |
StarForth_Mutex.thy |
Mutual exclusion |
Physics loops (1–7)
| File | Loop |
|---|---|
StarForth_Loop1_Heat.thy |
Execution heat tracking |
StarForth_Loop2_Window.thy |
Rolling window of truth |
StarForth_Loop3_Decay.thy |
Linear decay |
StarForth_Loop4_Pipeline.thy |
Word transition prediction |
StarForth_Loop5_WinInf.thy |
Window width inference |
StarForth_Loop6_DecayInf.thy |
Decay slope inference |
StarForth_Loop7_Heartrate.thy |
Adaptive heartrate |
Word categories
StarForth_Arithmetic_Words.thy, StarForth_Stack_Words.thy,
StarForth_Logical_Words.thy, StarForth_Memory_Words.thy,
StarForth_Return_Stack_Words.thy, StarForth_Q48_16.thy
ACL system (Phase 6)
| File | Property |
|---|---|
ACL_Pin_Monotone.thy |
Pin is one-way |
ACL_Inherit_Clears_Pin.thy |
Inheritance clears pin |
ACL_TTL_Bounded.thy |
TTL stays within bounds |
ACL_Emergency_Bypass.thy |
Emergency console bypass |
ACL_No_Escalation.thy |
No privilege escalation |
See also
ROOT— Isabelle project manifest- Project root