Robert Allan James
346c793ebc
Completes the src/word_source/*.c sweep -- last of the 5 kernel-only files. Five INFER-*@ output accessors fully modelled: they read straight from vm->last_inference_outputs, which is exactly the already-modelled `last_inference :: inference_outputs_state option` field with matching per-field names. Q.VARIANCE/INFER-DECAY-SLOPE/INFER-WINDOW-WIDTH get guard/shape only, capturing a genuine finding: array_ptr sets vm->error AND the caller still pushes a 0 placeholder regardless, unlike the "error or push, never both" shape most guarded words in this sweep follow. L8-UPDATE/L8-TABLE-FORCE get pop-shape only. Second finding: L8-MODE/L8-UPDATE/L8-APPLY/L8-TABLE-FORCE manipulate vm->ssm_l8_state (a legacy 16-mode struct) and, per L8-TABLE-FORCE's own comment, a separate 128-config adaptive table the heartbeat's bandit actually drives -- NEITHER is the `ssm_l8 :: ssm_l8_state` (4-mode C0..C3) field this proof suite has modelled since early in the sweep. Three L8 representations exist in the real system; none of this file's words touch the one the model tracks. Flagged as an open question, not guessed at. WINDOW-DIVERSITY, INFER-RUN, L8-MODE, L8-APPLY, and the six BAYES-* words deferred (unmodelled subsystems: rolling-window diversity algorithm, the whole inference-engine run, legacy L8 state, hot-words cache Bayesian posteriors). Suite now 53 theories, green.
56 lines
1.6 KiB
Plaintext
56 lines
1.6 KiB
Plaintext
session "StarForth" = "HOL-Library" +
|
|
description "Formal proofs of StarForth FORTH-79 primitive correctness and physics-loop invariants"
|
|
theories [document = false]
|
|
StarForth_Base
|
|
StarForth_Q48_16
|
|
StarForth_Stack_Words
|
|
StarForth_Double_Words
|
|
StarForth_Arithmetic_Words
|
|
StarForth_Mixed_Arithmetic_Words
|
|
StarForth_Logical_Words
|
|
StarForth_Return_Stack_Words
|
|
StarForth_Memory_Words
|
|
StarForth_Dictionary_Words
|
|
StarForth_Dictionary_Manipulation_Words
|
|
StarForth_Defining_Words
|
|
StarForth_Control_Words
|
|
StarForth_String_Words
|
|
StarForth_Block_Words
|
|
StarForth_IO_Words
|
|
StarForth_Editor_Words
|
|
StarForth_Format_Words
|
|
StarForth_System_Words
|
|
StarForth_Vocabulary_Words
|
|
StarForth_Mutex
|
|
StarForth_Transition
|
|
StarForth_Dictionary_Heat_Diagnostic_Words
|
|
StarForth_Physics_Freeze_Words
|
|
StarForth_Physics_Diagnostic_Words
|
|
StarForth_Physics_Benchmark_Words
|
|
StarForth_Physics_Pipelining_Diagnostic_Words
|
|
StarForth_StarForth_Words
|
|
StarForth_Framebuffer_Words
|
|
StarForth_Keyboard_Words
|
|
StarForth_Scroll_Words
|
|
StarForth_TTF_Words
|
|
StarForth_Lifecycle_Words_Hosted
|
|
StarForth_Defer_Words
|
|
StarForth_Log_Words
|
|
StarForth_Q48_Words
|
|
StarForth_Inference_Words
|
|
StarForth_Loop1_Heat
|
|
StarForth_Loop2_Window
|
|
StarForth_Loop3_Decay
|
|
StarForth_Loop4_Pipeline
|
|
StarForth_Loop5_WinInf
|
|
StarForth_Loop6_DecayInf
|
|
StarForth_Loop7_Heartrate
|
|
StarForth_Concurrent
|
|
StarForth_Correctness
|
|
ACL_Pin_Monotone
|
|
ACL_Inherit_Clears_Pin
|
|
ACL_TTL_Bounded
|
|
ACL_Emergency_Bypass
|
|
ACL_No_Escalation
|
|
StarForth_ACL_Words
|