Fix WP timeout in okj_measure_container#67
Conversation
The prover timed out on the loop-progress assert because the '"' branch contains a nested inner loop, making the proof obligation too complex for a single step. Adding an intermediate assert after the string-skip branch splits the proof so Alt-Ergo can discharge each branch independently. https://claude.ai/code/session_01LFxTXPy7Ut9JhJVnkTbYqM
|
Still have a timeout: [kernel] Parsing src/ok_json.c (with preprocessing) |
…ainer assert Add `p >= p_entry + 1` invariant to the inner string-skipping loop and an assertion before the loop establishing the initial value. This gives Alt-Ergo a direct proof path for the `p > p_entry` assertion after the string-skip branch, avoiding the timeout on typed_okj_measure_container_assert. https://claude.ai/code/session_01LFxTXPy7Ut9JhJVnkTbYqM
2 participants
Summary
typed_okj_measure_container_assert— the loop-progress assertionp > p_entryat the end of the outer loop body'"'branch contains a nested inner loop (string skipping), making the combined proof obligation too complex for a single solver step//@ assert p > p_entry;after the string-skip branch so the prover can discharge each branch independentlyTest plan
https://claude.ai/code/session_01LFxTXPy7Ut9JhJVnkTbYqM