cert: read the type section only through its cut in the acceptance proofs - #1446
Merged
Merged
Conversation
…oofs The package's roles_ok and plans_ok unfolded carrierState, carrierConfirmed and typeSectionMatches with simp. Each is a match on the decoded type section, and simp reduced that match before the cut could rewrite the decode, evaluating the whole type-section decode in the elaborator. After the Vector version structs changed the type section, btc-listener's Artifact.lean ran past the 9000-second phase limit. Unfold these definitions by their unconditional equations with matcher reduction off, so the decode is replaced by the cut and read only in the kernel: roles_ok 13 s and plans_ok 68 s on that package, where each ran for over 10 minutes. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
jasisz
force-pushed
the
cert/acceptance-cuts
branch
from
September 26, 2026 06:00
81033a0 to
4efea8b
Compare
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.
The acceptance proofs a package writes read the type section through its declared cut (
types_cut), but two of them unfoldedCertDecode.carrierState,TypeTable.carrierConfirmedandWasmSlice.typeSectionMatcheswithsimp. Each of those is amatchon the decoded type section, andsimptried to reduce thatmatchbefore the cut could rewrite the decode, so it evaluated the whole type-section decode in the elaborator.On btc-listener (commit 5698c8e) compiled after #1444, this made
aver-cert checkfail:Artifact.leanran past the 9000-second phase limit, where it took 266 s before #1444. Split into single theorems on the same built package:roles_okplans_okThe other theorems of
Artifact.lean(axes_ok13 s,envelope_okunder 1 s) were not affected. #1444 added the version and diff structs of everyVector<T>, which is what changed the type section. The fix is the same for both theorems: unfold these definitions by their unconditional equations (eq_def) with matcher reduction off (simp -iota), so the decode is replaced by the cut and read only in the kernel'sdecide.This changes only the proof scripts the producer writes into
Artifact.lean. The statements, the wall and the checker are unchanged, so the wall id stays the same and nothing moves in the ratchet.With this change the full
aver-cert checkof that btc-listener package passes in 1331 s (measured on #1445 merged with main). It failed at the limit without the change.Tests: the certificate snapshots,
cert_certify_spec cert_projects_andcert_hardening_spec(34).