Repository navigation
icarus_lowerable: reassess asp_solver and ternary_logic witnesses after #10370 (Closes #10450) - #10462
Merged
Conversation
#10370 (Closes #10450) #10370 rewrote specs/ar/asp_solver.t27 and specs/ar/ternary_logic.t27 so they compile (#8980): Program is now fixed arrays with counts, Trit is i8, and the list functions take slices. The pinned source signatures and the Lean witness models were stale. The specs and gen-rust output are correct, so the expected signatures and the Lean models are updated to the real interfaces; ar_asp_solver stays unlowerable (string fields), and a new theorem pins the exact set of slice/usize functions that block ar_ternary_logic. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
This was referenced Oct 18, 2026
Merged
Merged
Contributor
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes #10450
Cause
lowerability_models_keep_real_source_signatures(bootstrap/tests/icarus_lowerable.rs) went red on master at d31bccd. The cause is #10370: it legitimately rewrotespecs/ar/asp_solver.t27andspecs/ar/ternary_logic.t27so they compile (#8980), and the pinned source signatures and their Lean witness models were not reassessed. The spec andgen-rustoutput are correct, so neither is touched, and the test is not added to the ratchet baseline.asp_solver:Programis now{clauses: [Clause; 16], nclauses, constraints: [Clause; 16], nconstraints}instead ofVec<Clause>;Literalcarriesstringfields;solve(prog: Program) -> SolveResult.ternary_logic: a Trit isi8(was an undeclared type);resolve/apply_restrainttake and return slices,backward_chaintakes a slice ofRule. This mismatch was hidden behind the asp panic.What changed
bootstrap/tests/icarus_lowerable.rs: expected signatures and expected Lean model strings updated forProgram,solve,k3_and,backward_chain,resolve,apply_restraint(6 lines in, 6 out).proofs/lean4/Trinity/IcarusLowerable/Completeness.lean:ar_asp_solver_envnow models the real struct graph (Literal, Clause, LitList, Program, AnswerSet, SolveResult) with real array sizes;ar_ternary_logic_envusesi8Trits, a declaredRule, slice types and the real globals.ar_asp_solver_lowerable = falsestill holds, now because of thestringfields. The two stale Trit theorems are replaced byar_ternary_logic_slices_block, which pins the exact set of blocked functions (pool_take,backward_chain,resolve,apply_restraint).Net hand-written foreign lines are negative (foreign-budget gate).
Verification (Railway lab, not the Mac)
cargo test --release -p t27c --test icarus_lowerable -- lowerability_models corpus_classifierpasses.Completeness.lean; the lab disk was too full to fetch Mathlib).🤖 Generated with Claude Code