Core question: At the moment of action, does every still-possible realization consistent with the current evidence produce the same specified consequence? If two compatible worlds still disagree, Consequence Closure keeps that disagreement as evidence and asks what must be learned or changed to make the consequence determinate.
The question at the moment of action
Consequence Closure starts where several familiar assurances can stop too early. An authorization decision can be correct. A control change can be recorded. A status field can be fresh. None of those facts alone establishes what an already available action path will actually do at the moment of effect.
The Linux commissioning makes the gap concrete. A parent changed a memory-backed file to mode 0444 and verified that mode before a child wrote through a writable descriptor it had already inherited. The administrative state was correct, yet the write still succeeded in all 200 trials. With F_SEAL_WRITE established before the same effect cut, the write was blocked with EPERM in all 200 trials.
The assurance target is therefore not “was the control updated?” It is “is the specified consequence already determined by the evidence and operative state at this action boundary?”
Closure means determinacy, not approval
For one declared Boundary, the verifier considers every admissible realization still compatible with the evidence. A declared consequence function maps each realization to the outcome of the action under study.
- IMPOSSIBLE
- No admissible realization remains compatible with the evidence.
- OPEN
- At least two compatible realizations still produce different specified consequences.
- CLOSED(c)
- Every compatible realization produces the same consequence c.
CLOSED(c) does not mean safe, allowed, or desirable. The fixed consequence can be denial, failure, an adverse result, or any other declared outcome. Closure says that the consequence is determined. A separate policy decides what to do with that consequence.
The action cut is part of the claim. If a consequence-relevant transition can still occur between the evidence cut and the effect but is missing from the Boundary, a clean snapshot cannot be promoted into an action-level guarantee.
If two possible worlds disagree, keep both
An OPEN result is not returned as a bare failure flag. The verifier preserves two compatible realizations that agree on the selected information but disagree on the consequence.
That pair is a materiality witness. It is not merely an explanation attached after the verdict. It is the concrete reason the current evidence cannot yet determine the consequence.
For example, the bundled authority trace records that a deployment grant was revoked and that the decision engine observed the revocation, but an earlier bearer capability has not been tested after revocation. The unresolved operativity of that legacy path is what keeps the consequence open.
Turn the disagreement into semantic obligations
Once a consequence-divergent pair is known, the next question is not “which field looks relevant?” It is which declared semantic distinctions can separate every pair that would otherwise remain indistinguishable while producing different consequences.
Each divergent pair contributes the set of candidate Propositions that distinguish it. Those sets form a materiality hypergraph. A sufficient obligation set must intersect every such edge, and the inclusion-minimal sufficient obligation sets are exactly the inclusion-minimal transversals of that hypergraph.
Inclusion-minimal does not mean unique or smallest by cardinality. Several incomparable minimal obligation sets can exist. Inspector v0.5.0 exposes the exact family it computes within the declared portable budget and chooses one member deterministically only for the compact view.
The reference CEGIS loop discovers only the counterexamples it needs. Within a fixed finite candidate surface and a sound-and-complete fixed-set verifier, it terminates with an inclusion-minimal sufficient obligation set when one exists. If two consequence-divergent realizations agree on every declared Proposition, it returns UNRESOLVABLE UNDER DECLARED EVIDENCE SURFACE. That result identifies a vocabulary boundary rather than disguising it as search failure.
The determinacy and hitting-set ingredients are established formal tools. The project-specific contribution is how they are bound to a declared machine-action consequence, replayable witnesses, realizable Establishments, source-preservation levels, and real-system commissioning without collapsing those claims into one another.
Knowing what matters is different from knowing how to establish it
A semantic obligation answers an information question: which distinctions would be sufficient to determine the consequence? It is deliberately separate from the operations available to obtain that information or change the operative state.
Consequence Closure calls those realizable operations Establishments. The frozen Core distinguishes epistemic observations, state-making acts, operative guards, operative transactions, and action suppression. A Route is a finite strategy over declared Establishments, including branches that depend on observation outcomes.
This means the same unresolved distinction can sometimes be closed in two fundamentally different ways. A probe may observe whether a legacy capability is still effective. An operative guard may instead make that capability unable to produce the consequence. One resolves uncertainty; the other changes the reachable effect. The semantic obligation is the same question, but the mechanism is not.
Declarations are fixed before they justify a result. A witness may motivate a new Proposition or Establishment for a new analysis, but the result that exposed the gap cannot be retroactively repaired by changing the vocabulary or mechanism semantics after the outcome is known.
A correct final decision can still hide a broken abstraction
Carrier-specific systems need a front end that compiles their source semantics into the small Consequence Closure Core. Matching final outcomes on complete worlds is not enough. Two source abstractions can agree on every final ALLOW or DENY while disagreeing on whether a partial-evidence state is OPEN, what semantic obligations are sufficient, or which closure Route is realizable.
The source-preservation hierarchy therefore names the claim that a front end is actually entitled to export:
- P0 · status preservation
- Source and Core agree on IMPOSSIBLE, OPEN, or CLOSED(c) at every declared reachable analysis state.
- P1 · obligation preservation
- P0 holds, and source and Core agree on the paired counterexample predicate for every candidate subset. The sufficient-set family and inclusion-minimal obligation families therefore correspond.
- P2 · route preservation
- P0 and P1 hold, and declared Establishment enabledness plus the complete labeled successor structure are preserved. Only then does successful finite Route transfer follow at the declared level.
The hierarchy is output-relative. A source representation may be compressed aggressively when the stronger distinctions are unnecessary, but a status-preserving abstraction cannot silently claim that it also preserved the reasons for openness or the operative route structure.
The Cedar official-runtime gate
The P0/P1 preservation claim was converted into a preregistered differential against the official Cedar runtime rather than left as a hand-built reference-model exercise. The source oracle was cedar-policy-cli 4.12.0, pinned to its release commit.
- Source / Core worlds
- 64 / 64
- Reachable source / Core analysis states
- 183 / 183
- Complete-world consequence mismatches
- 0
- Proposition interpretation mismatches
- 0
- P0 mismatches
- 0
- P1 surface
- 183 states × all 16 candidate subsets = 2,928 checks
- P1 mismatches
- 0
- Exported witness reifications
- 427 checked · 0 failed
- Post-outcome semantic repair
- 0
The frozen classification is EXACT_P1_CONFIRMED_ON_FROZEN_BOUNDARY. This is stronger than matching Cedar's final decisions on the 64 complete worlds. On the declared reachable surface, source and Core also agreed on the counterexample structure that determines semantic sufficiency and inclusion-minimal obligations.
The result is intentionally narrower than “equivalent to Cedar.” It covers one preregistered bounded front end. P2 was not tested, and no Route-transfer claim follows from this gate.
Then test the semantics at real effect cuts
Source preservation and mechanism behavior are different assurance links. The commissioning sequence tests whether selected declared effects and evidence gates survive contact with concrete systems, while keeping those results separate from P0/P1/P2 claims.
- Linux operative effect
- fchmod 0444 was verified while the inherited write still succeeded 200 / 200. Expert and compiler-selected F_SEAL_WRITE blocked 200 / 200.
- SQLite lost update
- A frozen compiler with no SQLite- or Linux-keyed branches selected compare-and-swap. The naive schedule lost the intervening update 200 / 200; expert and compiler-selected CAS lost 0 / 200.
- Prospective filesystem publication
- RENAME_NOREPLACE_BIND was selected and sealed before the real run. Ordinary rename clobbered 200 / 200; the selected no-replace path clobbered 0 / 200 and returned EEXIST 200 / 200. A profile without that Establishment returned no closure Route before commissioning.
- OAuth paired-control gate
- Across 1,024 well-formed declared gate states, the frozen checker emitted no SAFE_AT_CUT where the declared oracle was non-safe. Missing positive gates remained OPEN, while direct post-revocation acceptance was UNSAFE.
- OAuthLib to Keycloak transfer
- The same frozen checker separated the live SAFE condition from the controlled authority-resource split state on OAuthLib 3.3.1 and pinned Keycloak 26.7.2 with semantic repair 0 and provider-specific semantic checker branches 0.
These tests answer different questions rather than adding up to one vague “system pass.” Linux separates administrative state from operative effect. SQLite and Linux pressure generic Route selection across different mechanism families. The filesystem test removes hindsight by freezing selection before the outcome. OAuth controls alternative explanations for a blocked request. The implementation-transfer runs test whether the frozen checker needs provider-specific semantic repair.
The assurance object stays challengeable
Consequence Closure Inspector v0.5.0 follows the same claim discipline. An OPEN state carries its materiality witness. A selected inclusion-minimal obligation set carries a sufficiency certificate and a concrete removal witness for every selected Proposition, so minimality is replayable rather than asserted by a label.
The Inspector also keeps exact Core analysis, source-preservation status, cut adequacy, Boundary qualification, declared Routes, and source lineage visibly separate. A model-relative Route is not promoted into a source-system Route without the required preservation evidence.
Exactness has a visible computational boundary. The portable implementation accepts at most 20 candidate Propositions and 2,000 worlds, with explicit search budgets for obligation and Route analysis. A budget overrun stops before a semantic result is emitted rather than substituting an approximate closure claim. The release gate matched exact inclusion-minimal obligation families against a brute-force oracle on 300 randomized models.
The v2 inspection export binds the declaration, analysis state, compatible realizations, obligation family and certificate, materiality witness, Route tree, qualifications, and deterministic record digest. The goal is not to make a formal result look polished. It is to make the result easier to challenge without changing what it claims.
Open the Consequence Closure Inspector
Result
Consequence Closure turns uncertainty at a machine action boundary into something a system can inspect, challenge, and resolve. It can show that a consequence is already fixed, preserve a concrete pair showing why it is not, derive the inclusion-minimal semantic distinctions sufficient to determine it, connect those distinctions to declared realizable steps, and keep source and operative qualifications attached to the result.
The project does not depend on one policy language, one control plane, or one carrier to define that target. The frozen record demonstrates the Core on a declared formal surface, exact P1 against one official Cedar boundary, prospective and cross-system Route selection under declared mechanism semantics, and frozen evidence checking across two commissioned OAuth implementations.
Where the result stops
Every positive statement remains relative to its declared Boundary, action cut, consequence, candidate vocabulary, and source or mechanism qualifications. The Core cannot infer that a source model is complete, that the cut is adequate, that evidence is authentic, or that a declared mechanism behaves correctly in an uncommissioned environment.
The Cedar result does not establish general Cedar equivalence and does not establish P2. The Linux, SQLite, filesystem, OAuthLib, and Keycloak runs do not establish general carrier neutrality. A successful commissioning link cannot repair an unproven source-preservation link, and a P1 source result cannot establish the operativity of an unrelated mechanism.
Frozen record and source materials
- Public research baseline
- Consequence Closure v1.0.0
- Core
- Consequence Closure Core v0.1.0
- Inspector
- Consequence Closure Inspector v0.5.0
- Technical Note DOI
- 10.5281/zenodo.22095709
- Software DOI
- 10.5281/zenodo.22095595
- Inspector release ZIP SHA-256
- a379d1dc05e0c7ee90f6370fba3a44fdfdff7dc89cff91d968f9b099d545b26c
- Technical Note PDF SHA-256
- 7de97e497b6703b74afaffcf99cb7532e29e6fe02446f9708b84dca05d875b3d
- Cedar primary evidence archive SHA-256
- 66be1260b0c3917bcae1c9884d0e583ee9a193bca0561c45544803730c6adc0d
- Runtime model
- Browser-local Inspector · no runtime network path