Repository navigation
chore(dr-math): land the stranded D-DRMC stack (#1701-#1704 + charter amendment) - #1708
Merged
Merged
Conversation
Coresearch D-DRMC items X1, X2, X3 (operator-chosen).
- The 5-field caller-built BindingWitness is gone. The frame (source,
relationship map, coordinates) is a Frame issued by a FrameStore and
compared by identity of the issue, mirroring dir-rmap-probe's Witness
(Weak + ptr_eq; that type is tied to dir-sim's VersionStore, so it is
not reused). Two stores at equal revisions do not alias; a re-seal at
equal numbers is FrameResealed.
- Focus (motion) and Scope (policy) are separate types and separate
guards; moving either leaves the frame valid.
- Validity is a carrier of R: Operand { rows, validity }. A three-valued
method needs it, a two-valued one refuses it, so no validity plane can
be bound to a foreign method.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg
…xtures
Coresearch D-DRMC items X4 and X17 (operator-chosen), on the stage 1
frame/focus/scope split.
- universal_on_focus checks Counterexamples before Unknown. A refuted
focus used to report Unknown(n) and hide the counterexample; under
certain-answer semantics one observed FALSE refutes the claim.
refuted_beats_unknown pins Gamma 0b111, R 0b001, validity 0b011 and
its two twins.
- The fixtures no longer bind Gamma and R to the same bits ("Gamma
subset of R" was Gamma subset of Gamma). R holds pairs outside Gamma,
with anti-vacuity asserts; the scalar-enumeration test now also calls
universal_on_focus.
- observe_focus reads validity from R, requires a two-valued Gamma, and
refuses a different frame issue, a stale frame or a different focus.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg
Coresearch D-DRMC item X15 (operator-chosen) and X17 for the recipe fixtures. - ProofDisposition (a caller-set "checked" flag) and the caller-supplied proof digest are gone. ProofReference has private fields and one constructor, rechecked(law, ReplayCapsule), which requires the capsule to prove law.statement (Stage B's SemanticKey) and re-runs ReplayCapsule::recheck. A forged nonzero digest used to pass; it can no longer be written (compile_fail doctest), and a real proof of a different statement is ProofOfOtherStatement. - CompiledReference carries Stage B's TargetAbi instead of a bare u32. - Recipe fixtures bind non-zero registers. - dr-math-binding-probe now depends on egglog-r2il-probe (egglog and ogar-loco by git, ndarray through the sibling patch). Limit: Stage B proves exact-integer substitution statements only. No statement language or checker exists for Boolean-DR64 laws, so the tests pair a DR64 shape with E1's statement to exercise the plumbing; that is not a claim that E1 says anything about DR64 (RECIPE_ADMISSION.md). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg
Disabling ReplayCapsule::recheck in ProofReference::rechecked leaves every test green: a capsule can only come from certify in-process. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg
The merge carries stage 3's Stage B proof identity, and in the same commit the stage 4 files that had to change with it (the handoff test does not compile against the new API otherwise). Conflict in Cargo.toml: keep both the egglog-r2il-probe dependency and the lance-graph-act-r dev-dependency. Coresearch D-DRMC items X17 and X20 (operator-chosen), plus the cheap X19 tightening: - contract_handoff bound Gamma and R to the same array, so "Gamma subset of R" could not fail. R now holds the selected pair and one more; the census is (1, 1, 0, 0). The proof is Stage B's re-checked E1 capsule, the target Stage B's TargetAbi. - The ACT-R snapshot version is read from the bound frame instead of a literal that matched the source revision by coincidence. - The effect refusal asserts EffectRequiresSeparateAuthorization, not any error. - The workflow was red at Format and installed `stable` while the repo pins 1.99. It now mirrors egglog-r2il-probe.yml: rustup show on the pinned toolchain, the ndarray sibling checkout the new egglog-r2il-probe dependency needs, native rustflags, cache, release tests, and triggers on the crates the probe now depends on. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg
…t the authority 55f88ef made ReplayCapsule::recheck the proof authority for DR64 recipes and paired a DR64 law shape with Stage B's scalar E1 statement in the tests. That conflated two things: egglog derives and checks proofs; ReplayCapsule only retains and replays one E1 compilation. It also treated E1's scalar substitution language as if it covered relational DR64 laws. Corrected: - RecipeCertificate is opaque (no public constructor, no status field), issued only by a certified-compiler boundary after egglog's proof check, law admission and a lowering check. The caller-set CheckedByExternalAuthority flag and the caller-supplied digest stay removed. - No such boundary exists for Boolean-DR64 laws, so admit_recipe runs every metadata check and then refuses with NoCertifiedCompiler. - The egglog-r2il-probe dependency and the ndarray patch are gone; E1 stays Stage B's own replay artifact. - Law identity no longer carries Stage B's SemanticKey; target ABI is back to this probe's own u32. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg
Stage 3 no longer uses Stage B's ReplayCapsule as proof authority (see ca88fea). Follow-through in this stage, in the merge because the handoff test does not compile against the new API otherwise: - Cargo.toml: egglog-r2il-probe dependency and patches dropped; the lance-graph-act-r dev-dependency stays. - contract_handoff: the recipe admission ends in NoCertifiedCompiler; ACT-R arbitrates on census eligibility alone, never on a proof. - Workflow: the pinned toolchain stays; the ndarray sibling checkout and the egglog/r2il/mask-risc triggers are gone with the dependency. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg
…-20261022 probe(dr-math): typed DR64 class/method operand binding [1/5]
…lational law Documentation only, operator-approved. Three amendments: 1. Certificate and rebinding. A recipe needs a certificate from a certified-compiler boundary (proof verified by egglog, typed law admission, lowering validated); caller-asserted status is never enough, and until the boundary exists admission refuses (NoCertifiedCompiler). Rebinding across two store-issued frames is an open probe (coresearch X8); a fallback to baseline does not count. 2. Witness model. Binding is under three independent guards: frame (identity, store-issued, compared by issue), focus (motion), scope (policy). Validity travels with the relation data. A new section keeps apart what mathematics permits, what the compiler certified, and what one execution may bind. 3. First candidate law: associativity of Boolean relation composition over OR/AND across compatible ClassView domains. The identity is established algebra; its representation, proof route, lowering, certificate and selection are open hypotheses. GF(2)/M4RI methods need an explicit semantics-preserving reduction. E1's stated limits (line 58) are unchanged. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg
…-20261022 test(dr-math): ClassView→DR→math offer→ACT-R handoff and isolated CI [4/5]
|
Important
This repository does not receive automatic reviews because it has fewer than 10 stars. ⚙️ Run configuration
Warning Billing warning: we have not been able to collect payment for this subscription for more than 72 hours. Please update the payment method or pay any pending invoices in Billing to avoid service interruption. Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
AdaWorldAPI
marked this pull request as ready for review
October 22, 2026 17:12
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
AdaWorldAPI
pushed a commit
that referenced
this pull request
Oct 22, 2026
AdaWorldAPI
pushed a commit
that referenced
this pull request
Oct 23, 2026
…stranded stacked PRs) BC-2026-10-23-13: the thought-git receipt is sealed before landing, its CommitWitness is issued only by commit_cycle, and replay -> proof is a refused promotion. A seventh independent source for trail T-ADMISSION. G-2026-10-23-5: a stacked PR is finished only when its commits are on main. Receipts #1696 and #1708 (both re-landed stranded stacks), plus lance-graph-java ISS-LGJ-STACK-TAIL-STRANDED-MINOR-8. IDs follow draft #1730 (BC-5..12, G-4); expect a trivial prepend conflict. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019fbZ92dFKQ5BJHrA3YcH9A
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
2 participants
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 D-DRMC stack merged base-first, so only #1700's first commit reached
main. Each later PR merged into its parent branch after that parent had already been merged:mainat 16:45:23 with27cddb7conly.4a04344b: certificate boundary, three guards, first relational law) was pushed to the charter branch at 16:46.mainhas none of thedr-math-binding-probecrate, and the plan onmainlacks the "Three boundaries" section.This branch is
mainplus two merge commits, with no new content:origin/lab/dr-math-0-charter-20261022: the charter amendment and probe(dr-math): typed DR64 class/method operand binding [1/5] #1701.origin/lab/dr-math-3-law-recipe-20261022: probe(dr-math): finite-population evidence and counterexample refusal [2/5] #1702, probe(dr-math): guarded theorem/compiled-recipe identities across DR classes [3/5] #1703 and test(dr-math): ClassView→DR→math offer→ACT-R handoff and isolated CI [4/5] #1704 (it also carries probe(dr-math): typed DR64 class/method operand binding [1/5] #1701's stage-1 commits).Both merges were clean.
Checks (on this branch)
crates/dr-math-binding-probe: fmt clean, clippy--release --all-targets -D warningsclean.SUPERSESSION-INDEX.mdregenerates byte-identical.#1707 (stage 5, associativity probe) will be retargeted onto this branch so its diff stays stage 5 only.
Generated by Claude Code