admin/LithosAnanake
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

proof/: fix ROLL, PICK, and pm_wf against real C ground truth, not just proof scripts

Browse Source 
ROLL: forth_roll_def implemented a third, invented convention matching
neither the theory's own test lemma nor the real C stack_word_roll(). Traced
the actual C source (src/word_source/stack_words.c:287-320) and its passing
tests (stack_words_test.c roll_1/roll_2) to the real semantics -- ROLL is
1-indexed from the BOTTOM of the stack, not top-indexed as the old
definition assumed. Rewrote forth_roll_def to match, replaced the false
roll_one_nop/roll_two_is_rot with lemmas verified against the actual test
vectors.

PICK: forth_pick_def indexed into the pre-pop stack (still containing the
count n as its own head) instead of the post-pop stack, off by one position,
plus a bound check one too permissive. Fixed against src/word_source/
stack_words.c:265-282 and its pick_0/pick_1/pick_2 test vectors.

pm_wf: pm_record_hit_preserves_wf/pm_record_miss_preserves_wf were
oops-flagged as a genuine invariant gap. Fixed with the minimal added
hypothesis (pm_last_accuracy_den pm > 0), matching this session's established
discipline. Also documents a deeper finding: pm_last_accuracy_num/den don't
correspond to any field in the real PipelineGlobalMetrics C struct (which has
a single "double last_checked_accuracy", not a fraction) -- flagged for a
separate field-level audit, not attempted here.

All 23 theory files verify with zero errors.
This commit is contained in:
Robert Allan James
2026-08-13 12:41:40 -04:00
parent 422ef2fa29
commit 87cd422957
2 changed files with 117 additions and 74 deletions
Download Patch File Download Diff File Expand all files Collapse all files
proof/StarForth_Loop4_Pipeline.thy
+25 -12
View File
@@ -113,26 +113,39 @@ 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
(* CORRECTED 2026-08-13, in two parts.
(1) The narrower gap first flagged: 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. *)
attempts = 0, den is 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 the precondition never guaranteed it. Fixed with the minimal,
honest addition: assume "pm_last_accuracy_den pm > 0" directly, same
discipline as every other missing-hypothesis fix this session (added,
not silently invented into pm_wf's own definition, which is a design
decision for Captain Bob, not a mechanical fix).
(2) A deeper finding surfaced while chasing this: pm_last_accuracy_num
and pm_last_accuracy_den do not correspond to anything in the real C
struct. include/vm.h's PipelineGlobalMetrics has a single
"double last_checked_accuracy" field (confirmed via
src/vm_bootstrap.c:290-295 and src/vm_time.c:412-413,627-628) -- there
is no num/den fraction pair anywhere in the real struct. This theory's
pipeline_metrics_state record (StarForth_Base.thy) modeled accuracy as
a fraction that was never audited against the actual C fields it
claims to mirror. Not re-audited or corrected here -- a full field-level
pass over pipeline_metrics_state is its own separate task, flagged for
later, not attempted as a side effect of this fix. *)
lemma pm_record_hit_preserves_wf:
assumes "pm_wf pm"
assumes "pm_last_accuracy_den pm > 0"
shows "pm_wf (pm_record_hit pm)"
oops
using assms by (simp add: pm_wf_def pm_record_hit_def)
lemma pm_record_miss_preserves_wf:
assumes "pm_wf pm"
assumes "pm_last_accuracy_den pm > 0"
shows "pm_wf (pm_record_miss pm)"
oops
using assms by (simp add: pm_wf_def pm_record_miss_def)
(* After a hit, hits ≤ attempts still holds. *)
lemma pm_record_hit_hits_le_attempts:
proof/StarForth_Stack_Words.thy
+92 -62
View File
@@ -329,41 +329,56 @@ lemma depth_overflow:
Bounds check: n \<ge> 0 and n < length (data_stack vm) *)
(* CORRECTED 2026-08-13, against src/word_source/stack_words.c:265-282 and
its passing tests (test_runner/modules/stack_words_test.c: pick_0,
pick_1, pick_2). The C code pops n FIRST (vm_pop), THEN indexes into
the REMAINING stack: "cell_t value = vm->data_stack[vm->dsp - n]" where
vm->dsp is already the post-pop top-of-stack index -- i.e. value = the
post-pop stack's n'th-from-top item, xs!n in this list's head=TOS
convention. The theory's original definition indexed into
"data_stack vm" (the PRE-pop stack, still containing n as its own head)
instead of "xs" (post-pop) -- off by one position, and its bound check
"nat n \<ge> length (data_stack vm)" used the pre-pop length too, one too
permissive (C's own bound is against post-pop depth, vm->dsp+1 = length
xs). Confirmed against the real test vectors: "1 2 3 0 PICK" expects
TOS=3 (xs!0), "1 2 3 1 PICK" expects 2 (xs!1), "1 2 3 2 PICK" expects 1
(xs!2) -- all match xs!n, none match the old (data_stack vm)!n. *)
definition forth_pick :: "vm_state \<Rightarrow> vm_state" where
"forth_pick vm =
(case data_stack vm of
[] \<Rightarrow> set_error vm
| n # xs \<Rightarrow>
if n < 0 \<or> nat n \<ge> length (data_stack vm)
if n < 0 \<or> nat n \<ge> length xs
then set_error vm
else vm\<lparr>data_stack := data_stack vm ! nat n # xs\<rparr>)"
else vm\<lparr>data_stack := xs ! nat n # xs\<rparr>)"
lemma pick_normal:
assumes "data_stack vm = n # xs"
assumes "n \<ge> 0"
assumes "nat n < length (data_stack vm)"
shows "data_stack (forth_pick vm) = data_stack vm ! nat n # xs"
assumes "nat n < length xs"
shows "data_stack (forth_pick vm) = xs ! nat n # xs"
using assms by (auto simp: forth_pick_def)
lemma pick_depth_unchanged:
assumes "data_stack vm = n # xs"
assumes "n \<ge> 0"
assumes "nat n < length (data_stack vm)"
assumes "nat n < length xs"
shows "length (data_stack (forth_pick vm)) = length (data_stack vm)"
by (simp add: forth_pick_def assms)
using assms by (auto simp: forth_pick_def)
(* 0 PICK: replaces TOS (which is 0) with data_stack[0] = 0 — identity. *)
lemma pick_zero_self:
assumes "data_stack vm = 0 # xs"
assumes "\<not> ds_full vm"
shows "data_stack (forth_pick vm) = 0 # xs"
by (simp add: forth_pick_def assms)
(* 1 PICK: replaces TOS (1) with the element at index 1 = hd xs. *)
lemma pick_one:
assumes "data_stack vm = 1 # x # xs"
(* 0 PICK: pushes a copy of the post-pop TOS (xs!0) -- equivalent to DUP.
Matches the real test vector "1 2 3 0 PICK" => prints 3. *)
lemma pick_zero_dup:
assumes "data_stack vm = 0 # x # xs"
shows "data_stack (forth_pick vm) = x # x # xs"
by (simp add: forth_pick_def assms)
using assms by (auto simp: forth_pick_def)
(* 1 PICK: pushes a copy of the item one below TOS (xs!1).
Matches the real test vector "1 2 3 1 PICK" => prints 2. *)
lemma pick_one:
assumes "data_stack vm = 1 # x # y # xs"
shows "data_stack (forth_pick vm) = y # x # y # xs"
using assms by (auto simp: forth_pick_def)
lemma pick_underflow:
assumes "data_stack vm = []"
@@ -378,25 +393,41 @@ lemma pick_bounds_neg:
lemma pick_bounds_high:
assumes "data_stack vm = n # xs"
assumes "nat n \<ge> length (data_stack vm)"
assumes "nat n \<ge> length xs"
shows "vm_error (forth_pick vm)"
using assms by (auto simp: forth_pick_def set_error_def)
(* ── ROLL ( +n -- ) ─────────────────────────────────────────────────────── *)
(* Pops n, then rotates items.
Special cases in C implementation:
n = 0: pop n, return (stack depth decreases by 1, TOS unchanged)
n = 1: pop n, return ("top item already at top")
n \<ge> 2: save item at index (depth - n) from bottom (= dsp+1-n after pop),
shift items down to fill gap, place saved item on top.
(* REWRITTEN 2026-08-13 to match real, ground-truth semantics -- the
previous version implemented a THIRD convention that matched neither
the real C code nor its own test lemma (see git history for the
original oops-flagged finding). Resolved by tracing the actual C
source and its passing tests:
Net effect on depth: decreases by 1 (n is consumed, one item moved).
src/word_source/stack_words.c:291-320 (stack_word_roll): n is popped
FIRST. n=0 is a no-op. For n\<ge>1, the comment is explicit and the code
matches it exactly: "1-indexed from bottom: n=1 moves bottom item to
top" -- target = bottom + (n-1) (C array index, bottom=0); the item at
that index is removed, everything above it shifts down one slot, and
the removed item is placed on top. This is NOT the standard/gforth
"count from top" ROLL (which would make "2 ROLL" a ROT) -- it is a
different, deliberately bottom-indexed operation in this codebase.
Index convention after popping n (dsp' = dsp - 1):
value = data_stack[dsp'+1-n] = data_stack[dsp-n]
Items at indices (dsp-n)..(dsp-1) shift down by 1.
Saved value placed at data_stack[dsp].
Final dsp unchanged (= dsp-1 after pop, but top slot reused). *)
Verified against the real passing tests (stack_words_test.c):
"1 2 3 1 ROLL . . . CR" => prints "1 3 2"
"1 2 3 2 ROLL . . . CR" => prints "2 3 1"
In this list's head=TOS convention, after popping n the remaining xs
has xs!0 = TOS ... xs!(length xs - 1) = bottom. "n=1 moves bottom to
top" means: target index = length xs - n (n=1 -> last index = bottom,
n=length xs -> index 0 = TOS itself, a full-depth roll). Hand-checked
both test vectors against this formula -- both match exactly (worked
in the discovering session's transcript, not reproduced in-line here).
Bound: n=0 is a no-op (checked first, no shift). For n\<ge>1, valid range
is 1 \<le> n \<le> length xs (C: "n >= vm->dsp + 1" is the error condition,
vm->dsp+1 = length xs after the pop) -- n = length xs is a valid
full-depth roll (brings the very bottom item to top when the whole
remaining stack is rolled), not an error. *)
definition forth_roll :: "vm_state \<Rightarrow> vm_state" where
"forth_roll vm =
@@ -405,11 +436,11 @@ definition forth_roll :: "vm_state \<Rightarrow> vm_state" where
| n # xs \<Rightarrow>
if n < 0 \<or> nat n > length xs
then set_error vm
else if n = 0 \<or> n = 1
else if n = 0
then vm\<lparr>data_stack := xs\<rparr>
else let i = nat n;
item = xs ! (i - 1);
rest = take (i - 1) xs @ drop i xs
else let i = length xs - nat n;
item = xs ! i;
rest = take i xs @ drop (i + 1) xs
in vm\<lparr>data_stack := item # rest\<rparr>)"
lemma roll_zero_nop:
@@ -417,37 +448,36 @@ 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\<or>n=1 shortcut is reached, giving set_error
instead of the identity -- so the claim is false for xs=[]. *)
lemma roll_one_nop:
(* n=1 moves the BOTTOM item to the top -- NOT a no-op in general (only
coincidentally a no-op when xs has length \<le> 1). Renamed from the old,
now-false "roll_one_nop" name. *)
lemma roll_one_moves_bottom:
assumes "data_stack vm = 1 # xs"
assumes "xs \<noteq> []"
shows "data_stack (forth_roll vm) = xs"
using assms by (auto simp: forth_roll_def)
shows "data_stack (forth_roll vm) = last xs # butlast xs"
proof -
have i: "length xs - nat (1::int) = length xs - 1" by simp
show ?thesis
using assms
by (simp add: forth_roll_def Let_def i last_conv_nth butlast_conv_take)
qed
(* 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"
oops
(* Ground-truth test vectors, proved symbolically (no need to construct a
concrete vm_state -- data_stack alone determines forth_roll's result).
"1 2 3 1 ROLL . . . CR" => prints "1 3 2": push 1,2,3 gives
data_stack=[3,2,1] (head=TOS), push count 1 gives [1,3,2,1]; xs=[3,2,1]
after popping the count; 1 ROLL moves the bottom item (1) to top. *)
lemma roll_test_vector_1:
assumes "data_stack vm = [1, 3, 2, 1]"
shows "data_stack (forth_roll vm) = [1, 3, 2]"
using assms by (simp add: forth_roll_def)
(* "1 2 3 2 ROLL . . . CR" => prints "2 3 1": xs=[3,2,1] after popping the
count 2; 2 ROLL moves the 2nd-from-bottom item (2) to top. *)
lemma roll_test_vector_2:
assumes "data_stack vm = [2, 3, 2, 1]"
shows "data_stack (forth_roll vm) = [2, 3, 1]"
using assms by (simp add: forth_roll_def)
lemma roll_underflow:
assumes "data_stack vm = []"