From 87cd4229579bafa6d24bca4a8c1e3728c197acda Mon Sep 17 00:00:00 2001 From: Robert Allan James Date: Thu, 13 Aug 2026 12:41:40 -0400 Subject: [PATCH] proof/: fix ROLL, PICK, and pm_wf against real C ground truth, not just proof scripts 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. --- proof/StarForth_Loop4_Pipeline.thy | 37 ++++--- proof/StarForth_Stack_Words.thy | 154 +++++++++++++++++------------ 2 files changed, 117 insertions(+), 74 deletions(-) diff --git a/proof/StarForth_Loop4_Pipeline.thy b/proof/StarForth_Loop4_Pipeline.thy index be62e50..7d038d4 100644 --- a/proof/StarForth_Loop4_Pipeline.thy +++ b/proof/StarForth_Loop4_Pipeline.thy @@ -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: diff --git a/proof/StarForth_Stack_Words.thy b/proof/StarForth_Stack_Words.thy index 95d812c..406ebc9 100644 --- a/proof/StarForth_Stack_Words.thy +++ b/proof/StarForth_Stack_Words.thy @@ -329,41 +329,56 @@ lemma depth_overflow: Bounds check: n \ 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 \ 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 \ vm_state" where "forth_pick vm = (case data_stack vm of [] \ set_error vm | n # xs \ - if n < 0 \ nat n \ length (data_stack vm) + if n < 0 \ nat n \ length xs then set_error vm - else vm\data_stack := data_stack vm ! nat n # xs\)" + else vm\data_stack := xs ! nat n # xs\)" lemma pick_normal: assumes "data_stack vm = n # xs" assumes "n \ 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 \ 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 "\ 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 \ length (data_stack vm)" + assumes "nat n \ 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 \ 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\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\1, valid range + is 1 \ n \ 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 \ vm_state" where "forth_roll vm = @@ -405,11 +436,11 @@ definition forth_roll :: "vm_state \ vm_state" where | n # xs \ if n < 0 \ nat n > length xs then set_error vm - else if n = 0 \ n = 1 + else if n = 0 then vm\data_stack := xs\ - 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\data_stack := item # rest\)" 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\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 \ 1). Renamed from the old, + now-false "roll_one_nop" name. *) +lemma roll_one_moves_bottom: assumes "data_stack vm = 1 # xs" assumes "xs \ []" - 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 = []"