Repository navigation
fix(ledger): enter ar_ternary_logic Rust/Lean mismatch (fast green for #6658) - #6672
Merged
Merged
Conversation
…#6658) #6452 made specs/ar/ternary_logic.t27 parse completely, so the classifier now reaches it and answers false (resolve and apply_restraint return unsized [Trit]). The Lean theorem ar_ternary_logic_lowerable is about an EMPTY model, so it proved nothing about the spec and is the stale side. Entered the same way as benchmarks_gf16_bfloat16_nmse (b751ee2): max_entries 77 -> 78, max_vacuous 44 -> 45, with the reason recorded. Owner approved 2026-10-06 (all three options for #6658), translated. The follow-up writes a real Lean model and removes this entry. Refs #6658 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Contributor
Contributor
PR DashboardGenerated at: 2026-10-06 06:53:26 UTC
Summary
Seal Status
|
This was referenced Oct 6, 2026
gHashTag
added a commit
that referenced
this pull request
Oct 6, 2026
…eave the ledger (#6684) * fix(proofs): real Lean model for ar_ternary_logic, theorem = false; leave the ledger The Lean model of specs/ar/ternary_logic.t27 was EMPTY, so native_decide proved the empty module lowerable while the classifier answers false. It is now a signature projection of the spec (as ar_asp_solver is): the three Trit consts, struct Rule, all ten functions, the 33 tests and nine benches by name, unmodeled types kept under their source names. Its theorem is `= false`, matching the classifier. A second theorem pins the reason #6658 names: with Trit declared as a lowerable struct, exactly backward_chain, resolve and apply_restraint -- the functions with a variable-length [Rule] / [Trit] in their signature -- are still not lowerable. Both theorems checked with Lean 4.31.0 core (Ast + Predicate) on the Railway lab; the old `= true` claim over the new model fails there, as it should. lowerability_models_keep_real_source_signatures now ties four of the model's signatures to what gen-rust emits for the spec. The ar_ternary_logic ledger entry from #6672 is removed; max_entries and max_vacuous return to 77 and 44. The theorem count is unchanged, so the 245 floor stays. The two hand-edited files get a one-time entry in tools/policy/foreign-exceptions.txt, removed again right after merge. Owner approved 2026-10-06 (all three options for #6658), translated. debt: #5980 Refs #6658 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * fix(lean): compile the proofs tree under --wfail; fix wasm-objdump install lake build has been red since the W472/W460 wave block landed in TernaryFPGABoot.lean with Rust-flavored syntax (struct ... where, .length, Array.forall) and identifiers the file never imported. Repaired in place: - Lean surface: structure/deriving, Array.set with proof, #[...] literals, arr.all; import Trinity.TernaryGemm for ternaryMac/ternaryGemm2x2. - raw_ns_preserved_under_jitter was false as stated (base 1000, jittered 1002); the 2 ns margin the claim needed now sits in the hypothesis. - worst_case_jitter_envelope_bound: 200000 was not a witness (eff + 2 only bounds the jittered value by 200002); tight witness 184002, bound proved by period*derating <= period*(23/20) <= 160000*(23/20) = 184000. - Array.getElem_set_self is namespaced in core; native_decide for the array lemma kernel decide cannot reduce. TernaryInference.lean: drop the three simp args the linter reports unused (Int.mul_neg x2, identityWeights) and rename 17 shadowed binders x -> _x. CI plumbing, same tree: - wasm-explorer.yml: cargo install wasm-objdump can never work (no such crate is published); install wabt from apt, which ships wasm-objdump. - test-baseline.txt: the corpus is fully parseable now, so the_dead_code_census_names_what_it_skipped fails on master too; one hand entry, reason in a comment, prune on next regen. - foreign-exceptions.txt: one-time entries for the two Lean files and the workflow repair. Refs #6658 Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * fix(ci): MAX_SORRY grep must exclude .lake/packages The sorry ratchet in lean-proofs.yml ran for the first time once the build went green and counted 434: batteries and mathlib ship `sorry` literals in their own test files under .lake/packages, which the recursive grep swept in. The ceiling of 5 describes the Trinity tree (3 real sorries in GoldenFloatRoundTrip + 2 prose mentions), which --exclude-dir=.lake restores. The gate's own comment says "Five sit in the tree today" -- the tree, not the dependencies. Refs #6658 Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * fix(ci): build wasm-explorer from inside its own package `-p t27-wasm-explorer` from the repo root can never resolve: the crate is on the workspace exclude list with its own Cargo.toml and Cargo.lock, and cargo only matches -p over workspace members. Run the build and the tests with working-directory set, as the crate's own header prescribes, and read the artifact from the package-local target dir. Verified locally: the wasm32 build finishes and the binary carries all four no_mangle exports. Refs #6658 Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
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.
Refs #6658
Owner approved 2026-10-06 (all three options for #6658), translated.
What
The t27c lab
leangate is red on master:NEW Rust/Lean lowerability disagreement(s), not in the ledger: ["ar_ternary_logic: Rust=false, Lean theorem=true"].#6452 made
specs/ar/ternary_logic.t27parse completely; the classifier now answersfalse, correctly (resolveandapply_restraintreturn unsized[Trit]). The Lean theoremar_ternary_logic_lowerableis about an EMPTY model, so it is the stale side.This PR enters the mismatch in
docs/reports/lean_completeness_mismatches.jsonthe same waybenchmarks_gf16_bfloat16_nmsewas entered on 2026-10-04 (b751ee2):max_entries77 -> 78,max_vacuous44 -> 45, reason recorded in the entry and in_why_entries_raised.Data only, no code.
Follow-up
The next PR for #6658 replaces the empty Lean model with a real one whose theorem is
= false, removes this entry and returns the caps to 77 / 44.🤖 Generated with Claude Code