proof: side-build laws can import earlier ones; name clashes degrade honestly#501
Merged
Conversation
…honestly Three pieces of plumbing for proofs that build on previously-proven conditional laws: - a side-build module can import source-earlier law modules; the lane index records the dependency edges, and an imported helper's content folds into the consumer's module hash — editing a helper renames every consumer, so a stale compiled artifact can never satisfy the credit probe (machinery only; nothing emits imports yet outside the test hook); - sabotage propagates: a failing helper takes every consumer's credit down in the same run (two-module chain test), while sabotaging only a consumer leaves the helper credited; - name-collision guard: a sibling law whose name collides with an emitted universal-proof theorem (the <law>_universal and <law>_prop hazards, both measured) is now honestly omitted with a note in the proof detail artifact, instead of failing the side build and silently stripping a NEIGHBOR's credit. json crediting byte-identical (universal credit, counted summaries across normal/sabotage/revert); full corpus counted builds unchanged. Co-Authored-By: Claude Fable 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.
Second increment of conditional helper lemmas (plan:
prompts/conditional-helper-lemmas-probe.md§8): the plumbing that lets a later law's universal proof build on earlier ones — consumption itself comes next.<law>_universal/<law>_propused to fail the side build and silently strip a neighbor's credit (measured during the previous increment's review, both hazards). Now the colliding law is honestly omitted with a plain-language note in the detail artifact; the neighbor keeps its credit. New fixture + live test.Gates: json crediting byte-identical (
when_universal5, summaries identical across normal/sabotage/revert); workspace tests green (live proof_spec incl. 3 new lane tests + 4 unit tests); fmt/clippy clean.Review notes carried to the next increment: the guard parser should also strip
@[...]attribute prefixes (not exploitable today), and aux-lemma names join the guarded set when consumers start importing helper namespaces.🤖 Generated with Claude Code