You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
combine the exact retained reducer result with parent-local obligation dispositions under the generic Refuted > Faulted > Unresolved > Satisfied precedence
preserve a decisive reducer refutation when an independent parent-local obligation is unresolved
reject a weaker satisfied reducer result when a parent-local obligation remains unresolved
keep child-discharge labels behavior-neutral
align SEMANTICS, README, threat-model, and KRN-08 conformance claims
Red-to-green evidence
Base: 5e29b2c874cba460249010b791f617dd0028d8e8
Before the implementation change, the focused regression decisive_refutation_outweighs_an_unresolved_parent_obligation failed with BHCP7302 claimed execution outcome does not match checked parent obligation dispositions.
After the implementation change:
mise exec -- cargo test --test proof_checker: 24 passed
complementary regression unresolved_parent_obligation_rejects_a_weaker_satisfied_reducer_result confirms the checker still rejects a weaker satisfied result with BHCP7302
affected profile, CI, schema, graph, verification, and policy-evidence targets passed
mise exec -- cargo clippy --all-targets -- -D warnings passed
git diff --check passed
Full validation
The unchanged canonical gate passed from a clean, explicitly bounded experiment-controller scratch directory:
mise exec -- cargo fmt --check
mise exec -- cargo clippy --all-targets -- -D warnings
mise exec -- cargo test --all-targets
mise exec -- cargo build --release
mise exec -- cargo test --test schema_fixtures
Documentation impact
Updated SEMANTICS.md, README.md, THREAT_MODEL.md, and conformance/v0/README.md to publish the same behavior-neutral precedence boundary.
Residual risk
This slice checks proof outcomes at the obligation-graph boundary. Execution-graph construction, runtime enforcement, and final evidence-graph assembly remain separately deferred as already documented.
Independent review evidence from Codex task /root/review_151 (distinct from authoring task /root; shared GitHub account, so this is not represented as a formal GitHub approval).
Reviewed exact immutable head 8eac3b865cd57b0dd514881685a6a2190922a37c against issue #151, the surrounding SEMANTICS.md proof contract, generic checker implementation, obligation-status aggregation, and proof regressions. No actionable findings.
The change preserves the exact retained reducer as child-composition authority, applies only the generic Refuted > Faulted > Unresolved > Satisfied ordering when reconciling parent-local dispositions, rejects weaker incompatible reducer outcomes, and introduces no reducer-, quantifier-, behavior-, or child-discharge-label-specific proof rule.
Independent validation at the reviewed head:
mise exec -- cargo test --test proof_checker: 24 passed
mise exec -- cargo clippy --all-targets -- -D warnings: passed
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
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 #151
Outcome
Refuted > Faulted > Unresolved > SatisfiedprecedenceRed-to-green evidence
Base:
5e29b2c874cba460249010b791f617dd0028d8e8Before the implementation change, the focused regression
decisive_refutation_outweighs_an_unresolved_parent_obligationfailed withBHCP7302 claimed execution outcome does not match checked parent obligation dispositions.After the implementation change:
mise exec -- cargo test --test proof_checker: 24 passedunresolved_parent_obligation_rejects_a_weaker_satisfied_reducer_resultconfirms the checker still rejects a weaker satisfied result withBHCP7302mise exec -- cargo clippy --all-targets -- -D warningspassedgit diff --checkpassedFull validation
The unchanged canonical gate passed from a clean, explicitly bounded experiment-controller scratch directory:
Documentation impact
Updated
SEMANTICS.md,README.md,THREAT_MODEL.md, andconformance/v0/README.mdto publish the same behavior-neutral precedence boundary.Residual risk
This slice checks proof outcomes at the obligation-graph boundary. Execution-graph construction, runtime enforcement, and final evidence-graph assembly remain separately deferred as already documented.
Exact reviewed head
8eac3b865cd57b0dd514881685a6a2190922a37c