Assurance — card

Operation	Covers	Clauses	Proved
model	The Lean policy package and the Lean protocol state machine, their pins, and the definitions theorems and checks range over.	27	0
prove	The theorem inventory: layer composition, placement, the evidence floor, the proof targets over the authority mapping, and the mediation relation over statement execution.	21	1
audit-assumptions	The assumption allowlist, the transitive footprint audit over the elaborated environment, the inventory and the report.	14	0
recheck	Rebuilding and re-auditing from pinned source in a credential-free environment.	4	0
scope-claim	The sentence the assurance claim is allowed to be: named decisions, named specifications and trusted dependencies.	4	0
differential-test	The executable reference models, the case generators, the minimized counterexample corpus and the command running them.	27	0
structure-tree	One home per capability, the one enforcement decision module, adapters, mirror annotations and derived-artifact checks.	10	0
test	Assertion construction, guard validation, suite placement, test-first and acceptance tests, and the connector test kit.	16	0
build	Target directories, the engine-linked invocation, linked query functions, build targets, release artifacts and the dependency allowlist.	22	0
evaluate	The read-path quality harness: case format, deterministic metrics and floors, judged dimensions, the reader and the judge.	40	0
baseline	Holding a run against committed baselines and absolute floors, intervals, golden custody and case generation.	27	0
backtest	Historical evaluations, called backtests: bounded cases, model-knowledge controls, label intervals and splits, execution metadata, planted leaks and replayable trajectories. Financial return-series and execution profiles are consumer-selected applications of this flow (domain-neutraltopology.bound-application.domain-neutralThe engine processes declared data, schemas, policies, time bounds and capabilities. Consumer configuration, connectors, components or explicitly selected evaluation profiles supply domain meanings, business rules and sector-specific metrics.).	21	0
forecast	Probability forecasts over consumer-declared outcomes: freeze instant, settlement, lead time, imputation, coverage, reference baselines and separate scoring tracks. Reference baselines belong to an explicitly selected profile (domain-neutraltopology.bound-application.domain-neutralThe engine processes declared data, schemas, policies, time bounds and capabilities. Consumer configuration, connectors, components or explicitly selected evaluation profiles supply domain meanings, business rules and sector-specific metrics.).	9	0
consumer	Artifact compatibility: source-independent execution, required capabilities, scenario evidence, storage profiles and release distribution.	19	0
automate	Typed subcommands over compiled binaries, and the boundary shell keeps.	6	0
gate	Stage order, secrets of record, the crate-graph, row-token, egress and dependency rules, the formal stage, build jobs, free disk, footprint budgets and surface checks.	44	0
measure	The target ledger: each tracked target, the clause it serves, how it is measured and its record per commit.	20	0
release	The release tag’s version, the refusals guarding it, the signed annotated tag contextful-ci tag creates, and the local packaging the operator runs from it.	12	0
deploy-apps	The one GitHub Actions workflow, its trigger, permission and credential shape, and contextful-ci deploy cloudflare, the command it and an operator run to ship one Cloudflare app.	15	0

Error	When	Clause
FormalPackageDependencyassurance.model.declared-dependencyA require stanza in the policy package's lakefile.toml reaching any external library raises FormalPackageDependency, naming the library.	The Lean package manifest declares an external library.	assurance.model.declared-dependencyassurance.model.declared-dependencyA require stanza in the policy package's lakefile.toml reaching any external library raises FormalPackageDependency, naming the library.
ProofToolchainDriftassurance.model.toolchain-driftA build whose resolved toolchain string differs from the pinned one raises ProofToolchainDrift, printing both strings.	The resolved toolchain release string differs from the pinned one.	assurance.model.toolchain-driftassurance.model.toolchain-driftA build whose resolved toolchain string differs from the pinned one raises ProofToolchainDrift, printing both strings.
UnmodelledConstructorassurance.model.unmodelled-constructorA category the manifest admits with no case in the placement inductive raises UnmodelledConstructor at elaboration, naming the category.	A placement category the manifest admits has no case in the model’s inductive.	assurance.model.unmodelled-constructorassurance.model.unmodelled-constructorA category the manifest admits with no case in the placement inductive raises UnmodelledConstructor at elaboration, naming the category.
ProtocolInvariantViolatedassurance.model.protocol-checkThe gate evaluates every invariant on each state reached by every step sequence over three nodes and four lease generations; a breaking state raises ProtocolInvariantViolated, printing the shortest sequence reaching it.	A state the bounded check reaches breaks a protocol invariant.	assurance.model.protocol-checkassurance.model.protocol-checkThe gate evaluates every invariant on each state reached by every step sequence over three nodes and four lease generations; a breaking state raises ProtocolInvariantViolated, printing the shortest sequence reaching it.
JournalInvariantViolatedassurance.model.journal-checkprotocol journal check evaluates every journal property on each state three callers reach on one key; a breaking state raises JournalInvariantViolated, printing the shortest sequence reaching it.	A state the journal check reaches breaks a journal property.	assurance.model.journal-checkassurance.model.journal-checkprotocol journal check evaluates every journal property on each state three callers reach on one key; a breaking state raises JournalInvariantViolated, printing the shortest sequence reaching it.
CommutationClaimedassurance.prove.commutation-claimA claim that the enforcement stages commute raises CommutationClaimed.	Order-independence asserted over stages whose order the composition theorem fixes.	assurance.prove.commutation-claimassurance.prove.commutation-claimA claim that the enforcement stages commute raises CommutationClaimed.
ZoneInclusionSampledassurance.prove.sampled-inclusionInclusion decided by evaluating a fixed set of example values raises ZoneInclusionSampled.	Inclusion decided by evaluating a fixed set of example values.	assurance.prove.sampled-inclusionassurance.prove.sampled-inclusionInclusion decided by evaluating a fixed set of example values raises ZoneInclusionSampled.
ProofTargetUnboundassurance.prove.unbound-targetA target the claim names with no binding raises ProofTargetUnbound, naming the target.	A proof target named in the claim with no authenticated query path bound to it.	assurance.prove.unbound-targetassurance.prove.unbound-targetA target the claim names with no binding raises ProofTargetUnbound, naming the target.
TheoremWithoutNegativeSpaceassurance.prove.no-negative-spaceA theorem published without its negative space raises TheoremWithoutNegativeSpace, naming the constant.	A theorem published with no statement of what it leaves open.	assurance.prove.no-negative-spaceassurance.prove.no-negative-spaceA theorem published without its negative space raises TheoremWithoutNegativeSpace, naming the constant.
MediationClaimedFromCompositionassurance.prove.mediation-from-compositionA filter-composition theorem offered as a mediation theorem raises MediationClaimedFromComposition.	A filter-composition theorem offered as a mediation theorem.	assurance.prove.mediation-from-compositionassurance.prove.mediation-from-compositionA filter-composition theorem offered as a mediation theorem raises MediationClaimedFromComposition.
AssumptionOutsideAllowlistassurance.audit-assumptions.assumption-outside-allowlistAn assumption in a footprint and absent from the allowlist raises AssumptionOutsideAllowlist, printing the constant and the assumption.	A constant’s footprint reaches an assumption absent from the allowlist.	assurance.audit-assumptions.assumption-outside-allowlistassurance.audit-assumptions.assumption-outside-allowlistAn assumption in a footprint and absent from the allowlist raises AssumptionOutsideAllowlist, printing the constant and the assumption.
ProofHoleAssumptionassurance.audit-assumptions.hole-assumptionA footprint containing the hole assumption raises ProofHoleAssumption, naming the declaration, whatever its syntax spells.	A footprint contains the hole assumption.	assurance.audit-assumptions.hole-assumptionassurance.audit-assumptions.hole-assumptionA footprint containing the hole assumption raises ProofHoleAssumption, naming the declaration, whatever its syntax spells.
NativeEvaluationAssumptionassurance.audit-assumptions.native-evaluation-assumptionA footprint containing a per-declaration native-evaluation assumption raises NativeEvaluationAssumption, naming the declaration that minted it.	A footprint contains a per-declaration native-evaluation assumption.	assurance.audit-assumptions.native-evaluation-assumptionassurance.audit-assumptions.native-evaluation-assumptionA footprint containing a per-declaration native-evaluation assumption raises NativeEvaluationAssumption, naming the declaration that minted it.
TheoremConstantMissingassurance.audit-assumptions.missing-constantA required constant absent from the elaborated environment raises TheoremConstantMissing.	A required constant is absent from the elaborated environment.	assurance.audit-assumptions.missing-constantassurance.audit-assumptions.missing-constantA required constant absent from the elaborated environment raises TheoremConstantMissing.
TheoremStatementDriftassurance.audit-assumptions.statement-driftA required constant whose elaborated statement differs from its expected text raises TheoremStatementDrift, printing both.	A required constant’s elaborated statement differs from its expected text.	assurance.audit-assumptions.statement-driftassurance.audit-assumptions.statement-driftA required constant whose elaborated statement differs from its expected text raises TheoremStatementDrift, printing both.
RecheckEnvironmentCredentialedassurance.recheck.credential-freeA recheck environment exposing a token, a signing key or a registry login raises RecheckEnvironmentCredentialed, naming the variable or file carrying it.	The recheck environment exposes a credential.	assurance.recheck.credential-freeassurance.recheck.credential-freeA recheck environment exposing a token, a signing key or a registry login raises RecheckEnvironmentCredentialed, naming the variable or file carrying it.
RecheckReportMismatchassurance.recheck.report-mismatchA recheck whose per-constant statement text or assumption set differs from the first phase's raises RecheckReportMismatch, naming the constant.	The recheck’s per-constant statement or assumption set differs from the first phase’s.	assurance.recheck.report-mismatchassurance.recheck.report-mismatchA recheck whose per-constant statement text or assumption set differs from the first phase's raises RecheckReportMismatch, naming the constant.
ClaimBeyondNamedDecisionsassurance.scope-claim.beyond-named-decisionsA claim that the enforcement engine, or any object wider than the named decisions, is verified raises ClaimBeyondNamedDecisions.	The assurance claim asserts an object wider than its named decisions.	assurance.scope-claim.beyond-named-decisionsassurance.scope-claim.beyond-named-decisionsA claim that the enforcement engine, or any object wider than the named decisions, is verified raises ClaimBeyondNamedDecisions.
TrustedDependencyUnnamedassurance.scope-claim.unnamed-dependencyA claim resting on a component absent from its trusted-dependency list raises TrustedDependencyUnnamed, naming the component.	The claim rests on a component absent from its trusted-dependency list.	assurance.scope-claim.unnamed-dependencyassurance.scope-claim.unnamed-dependencyA claim resting on a component absent from its trusted-dependency list raises TrustedDependencyUnnamed, naming the component.
ReferenceVocabularyDriftassurance.differential-test.reference-vocabularyBefore any case, the harness reads the reference binary's operation listing; an operation one of the reference and the harness lists and the other lacks raises ReferenceVocabularyDrift, printing both lists.	The reference binary and the harness list different operations.	assurance.differential-test.reference-vocabularyassurance.differential-test.reference-vocabularyBefore any case, the harness reads the reference binary's operation listing; an operation one of the reference and the harness lists and the other lacks raises ReferenceVocabularyDrift, printing both lists.
ReferenceModelDriftassurance.differential-test.disagreementA case on which any two of the three decisions differ raises ReferenceModelDrift, printing the minimized case and every decision.	The reference model and the engine’s decision function disagree on a case.	assurance.differential-test.disagreementassurance.differential-test.disagreementA case on which any two of the three decisions differ raises ReferenceModelDrift, printing the minimized case and every decision.
CounterexampleDiscardedassurance.differential-test.discarded-counterexampleA run reporting a disagreement and writing no corpus entry raises CounterexampleDiscarded.	A run reported a disagreement and wrote no corpus entry.	assurance.differential-test.discarded-counterexampleassurance.differential-test.discarded-counterexampleA run reporting a disagreement and writing no corpus entry raises CounterexampleDiscarded.
ProtocolConformanceDriftassurance.differential-test.protocol-driftA step after which the model's state and the store's projected state differ raises ProtocolConformanceDrift, printing the minimized operation sequence and both states.	The protocol model and the Rust store disagree on the state after a step.	assurance.differential-test.protocol-driftassurance.differential-test.protocol-driftA step after which the model's state and the store's projected state differ raises ProtocolConformanceDrift, printing the minimized operation sequence and both states.
ProtocolVocabularyDriftassurance.differential-test.protocol-vocabularyBefore any case, the harness reads the protocol executable's step listing; a step kind one of the model and the harness lists and the other lacks raises ProtocolVocabularyDrift, printing both lists.	The protocol model and the harness list different step kinds.	assurance.differential-test.protocol-vocabularyassurance.differential-test.protocol-vocabularyBefore any case, the harness reads the protocol executable's step listing; a step kind one of the model and the harness lists and the other lacks raises ProtocolVocabularyDrift, printing both lists.
JournalConformanceDriftassurance.differential-test.journal-driftA step after which the journal model and an adapter differ raises JournalConformanceDrift, printing the adapter, the minimized sequence and both states.	The journal model and a journal adapter disagree on the state after a step.	assurance.differential-test.journal-driftassurance.differential-test.journal-driftA step after which the journal model and an adapter differ raises JournalConformanceDrift, printing the adapter, the minimized sequence and both states.
MergeConformanceDriftassurance.differential-test.merge-driftA case on which the merge model and merge_verified differ raises MergeConformanceDrift, printing the minimized case and both merges.	The merge model and the store’s merge disagree on a key’s outcome.	assurance.differential-test.merge-driftassurance.differential-test.merge-driftA case on which the merge model and merge_verified differ raises MergeConformanceDrift, printing the minimized case and both merges.
CapabilityDuplicatedassurance.structure-tree.duplicated-capabilityA surface or crate carrying a second implementation of an engine capability, in any language, or a hand-written copy of an engine constant, raises CapabilityDuplicated, naming both sites.	A second implementation of an engine capability, or a hand-written copy of an engine constant.	assurance.structure-tree.duplicated-capabilityassurance.structure-tree.duplicated-capabilityA surface or crate carrying a second implementation of an engine capability, in any language, or a hand-written copy of an engine constant, raises CapabilityDuplicated, naming both sites.
CapabilityHomeUnresolvedassurance.structure-tree.capability-registryspec/capabilities.toml names each capability of one-home with one home path and one or more defining symbols; an absent registry, a missing or doubled capability, an absent home or an undefined symbol raises CapabilityHomeUnresolved.	A capability registry entry resolving to no home or symbol in the tree.	assurance.structure-tree.capability-registryassurance.structure-tree.capability-registryspec/capabilities.toml names each capability of one-home with one home path and one or more defining symbols; an absent registry, a missing or doubled capability, an absent home or an undefined symbol raises CapabilityHomeUnresolved.
BoundConstantDriftassurance.structure-tree.bound-constantA [limit] entry whose limit-const names <file>::<NAME> holds a constant that file defines outside tests at the bound, in its unit or another unit of its kind; a mismatch or an absent constant raises BoundConstantDrift.	A bound constant whose value differs from its registry entry, or that its named file does not define.	assurance.structure-tree.bound-constantassurance.structure-tree.bound-constantA [limit] entry whose limit-const names <file>::<NAME> holds a constant that file defines outside tests at the bound, in its unit or another unit of its kind; a mismatch or an absent constant raises BoundConstantDrift.
MirrorUnresolvedassurance.structure-tree.mirror-unresolvedA mirrors: comment in a tracked file under crates/, tools/ or apps/ naming no clause of spec/spec.lock.json raises MirrorUnresolved in the schema stage, naming the file and line.	A mirrors annotation naming no clause of the lock file.	assurance.structure-tree.mirror-unresolvedassurance.structure-tree.mirror-unresolvedA mirrors: comment in a tracked file under crates/, tools/ or apps/ naming no clause of spec/spec.lock.json raises MirrorUnresolved in the schema stage, naming the file and line.
VacuousAssertionassurance.test.vacuous-exclusionAn exclusion assertion — all, or a negated any — in a tracked test file under crates/ or tools/, over a collection no earlier statement of its function shows non-empty, raises VacuousAssertion in the test-first stage.	An exclusion assertion evaluated over an empty collection.	assurance.test.vacuous-exclusionassurance.test.vacuous-exclusionAn exclusion assertion — all, or a negated any — in a tracked test file under crates/ or tools/, over a collection no earlier statement of its function shows non-empty, raises VacuousAssertion in the test-first stage.
TestNotFirstassurance.test.test-firstA change altering Rust source under crates/ or tools/ adds or alters a test under a package's tests/ that fails against the base commit's source; a change without one raises TestNotFirst.	A source change carrying no test that fails against the base commit’s source.	assurance.test.test-firstassurance.test.test-firstA change altering Rust source under crates/ or tools/ adds or alters a test under a package's tests/ that fails against the base commit's source; a change without one raises TestNotFirst.
TestFirstBaseUnrunnableassurance.test.base-unrunnableA base invocation whose output reports a full disk, an unloadable manifest or an unfetchable dependency raises TestFirstBaseUnrunnable instead of a verdict.	A test-first run at base stopped by the machine or the base workspace, not by the tests.	assurance.test.base-unrunnableassurance.test.base-unrunnableA base invocation whose output reports a full disk, an unloadable manifest or an unfetchable dependency raises TestFirstBaseUnrunnable instead of a verdict.
AcceptanceLinksEngineassurance.test.acceptance-surfaceAn acceptance test drives a built binary through its command line, MCP or HTTP surface; a workspace package among the acceptance package's dependencies raises AcceptanceLinksEngine.	The acceptance package depending on a workspace package.	assurance.test.acceptance-surfaceassurance.test.acceptance-surfaceAn acceptance test drives a built binary through its command line, MCP or HTTP surface; a workspace package among the acceptance package's dependencies raises AcceptanceLinksEngine.
ExtensionAutoloadRefusedassurance.build.runtime-extension-loadA read path loading an extension into a binary that statically links the SQL engine raises ExtensionAutoloadRefused.	A read path loading a query-engine extension into a statically linked binary.	assurance.build.runtime-extension-loadassurance.build.runtime-extension-loadA read path loading an extension into a binary that statically links the SQL engine raises ExtensionAutoloadRefused.
ImageBinaryMismatchassurance.build.image-binary-mismatchA binary whose ELF machine differs from its target's, or whose program headers name a dynamic interpreter, raises ImageBinaryMismatch, naming the target.	A release image binary of another ELF machine than its target, or naming a dynamic interpreter.	assurance.build.image-binary-mismatchassurance.build.image-binary-mismatchA binary whose ELF machine differs from its target's, or whose program headers name a dynamic interpreter, raises ImageBinaryMismatch, naming the target.
PackageLicenceMissingassurance.build.licence-fieldEvery workspace package under crates/ or tools/ declares license = "Apache-2.0", inherited from [workspace.package]; a package declaring another value or none raises PackageLicenceMissing, naming its manifest.	A workspace package whose manifest declares no licence, or one other than Apache-2.0.	assurance.build.licence-fieldassurance.build.licence-fieldEvery workspace package under crates/ or tools/ declares license = "Apache-2.0", inherited from [workspace.package]; a package declaring another value or none raises PackageLicenceMissing, naming its manifest.
DependencyAllowlistViolationassurance.build.dependency-allowlistThe connector authoring dependency allowlist carries regex and serde_json at its depth limit; a profile graph reaching fancy-regex, pcre2, onig or serde_json's unbounded_depth feature raises DependencyAllowlistViolation, naming the profile and path.	A profile graph reaching a backtracking regular-expression engine or a parser with its depth limit off.	assurance.build.dependency-allowlistassurance.build.dependency-allowlistThe connector authoring dependency allowlist carries regex and serde_json at its depth limit; a profile graph reaching fancy-regex, pcre2, onig or serde_json's unbounded_depth feature raises DependencyAllowlistViolation, naming the profile and path.
EvalCorpusUnlabeledassurance.evaluate.unlabeled-corpusA run over a corpus whose tables declare no zone or row policy, with no local: zone passed as --zone, raises EvalCorpusUnlabeled before any row lands.	An evaluation corpus with no policy labels and no explicit local zone.	assurance.evaluate.unlabeled-corpusassurance.evaluate.unlabeled-corpusA run over a corpus whose tables declare no zone or row policy, with no local: zone passed as --zone, raises EvalCorpusUnlabeled before any row lands.
EvalSemanticCacheUnverifiedassurance.evaluate.semantic-cache--semantic-manifest hashes corpus, held-out labels, development queries, configuration, and the model's license, embedding configuration and artifacts at an immutable revision; a changed, unhashed or symbolically linked input or a second table raises EvalSemanticCacheUnverified before through-the-store.	A semantic cache input changed, unhashed, symbolically linked, or a second table.	assurance.evaluate.semantic-cacheassurance.evaluate.semantic-cache--semantic-manifest hashes corpus, held-out labels, development queries, configuration, and the model's license, embedding configuration and artifacts at an immutable revision; a changed, unhashed or symbolically linked input or a second table raises EvalSemanticCacheUnverified before through-the-store.
EvalSemanticInputRejectedassurance.evaluate.semantic-inputsA missing, non-finite, zero-norm or mismatched vector, a relocated held-out file, an overlapping development query or a configuration difference raises EvalSemanticInputRejected before retrieval; every leg consumes the same verified cases and corpus.	A semantic vector, held-out file, development split or configuration that fails verification.	assurance.evaluate.semantic-inputsassurance.evaluate.semantic-inputsA missing, non-finite, zero-norm or mismatched vector, a relocated held-out file, an overlapping development query or a configuration difference raises EvalSemanticInputRejected before retrieval; every leg consumes the same verified cases and corpus.
BaselinePathUnresolvedassurance.baseline.unresolvable-pathA path resolving to nothing, a mean over fewer than 30 cases, a malformed entry or a non-finite band raises BaselinePathUnresolved before the suite runs.	A baseline entry naming no report field, under-sampled, or malformed.	assurance.baseline.unresolvable-pathassurance.baseline.unresolvable-pathA path resolving to nothing, a mean over fewer than 30 cases, a malformed entry or a non-finite band raises BaselinePathUnresolved before the suite runs.
BaselineRunStampMismatchassurance.baseline.run-stamp-driftA run block differing from the run's own configuration raises BaselineRunStampMismatch before the suite runs.	A baseline run block differing from the run’s configuration.	assurance.baseline.run-stamp-driftassurance.baseline.run-stamp-driftA run block differing from the run's own configuration raises BaselineRunStampMismatch before the suite runs.
GoldenSetIngestedassurance.baseline.answer-key-in-the-storeAn artifact path normalizing under the evaluation directory, reached by a manifest lint or a connector, raises GoldenSetIngested.	A golden set reaching the store it measures.	assurance.baseline.answer-key-in-the-storeassurance.baseline.answer-key-in-the-storeAn artifact path normalizing under the evaluation directory, reached by a manifest lint or a connector, raises GoldenSetIngested.
GoldenRedactionFailedassurance.baseline.generated-redactionA golden mined from a live query or promoted from a labeled outcome passes write-time before commit; a case it cannot redact raises GoldenRedactionFailed.	A generated golden the write-time redaction pass cannot clear.	assurance.baseline.generated-redactionassurance.baseline.generated-redactionA golden mined from a live query or promoted from a labeled outcome passes write-time before commit; a case it cannot redact raises GoldenRedactionFailed.
PublicCorpusDigestMismatchassurance.baseline.public-corporaA public benchmark corpus enters through a fetch-manifest entry naming its URL, its dataset's terms and a SHA-256 digest, and is never committed; fetched bytes under another digest raise PublicCorpusDigestMismatch.	Fetched public benchmark bytes whose SHA-256 digest differs from the fetch manifest’s.	assurance.baseline.public-corporaassurance.baseline.public-corporaA public benchmark corpus enters through a fetch-manifest entry naming its URL, its dataset's terms and a SHA-256 digest, and is never committed; fetched bytes under another digest raise PublicCorpusDigestMismatch.
TraceExportOutOfPerimeterassurance.baseline.trace-exportA run touching a deployed store with a hosted trace endpoint configured raises TraceExportOutOfPerimeter; hosted collection serves runs over public or synthetic fixtures alone.	A hosted trace endpoint configured for a run touching a deployed store.	assurance.baseline.trace-exportassurance.baseline.trace-exportA run touching a deployed store with a hosted trace endpoint configured raises TraceExportOutOfPerimeter; hosted collection serves runs over public or synthetic fixtures alone.
EvalLabelIntervalMissingassurance.backtest.label-intervalEvery bounded case declares its label interval [t0, t1], the span its outcome is observed over; a bounded case without one raises EvalLabelIntervalMissing before any of its reads.	A bounded case declaring no label interval.	assurance.backtest.label-intervalassurance.backtest.label-intervalEvery bounded case declares its label interval [t0, t1], the span its outcome is observed over; a bounded case without one raises EvalLabelIntervalMissing before any of its reads.
EvalExecutionUndeclaredassurance.backtest.execution-componentA backtest report stamps its declared execution component's digest and parameters under domain-neutral; a report without one raises EvalExecutionUndeclared.	A backtest report stamping no declared execution component.	assurance.backtest.execution-componentassurance.backtest.execution-componentA backtest report stamps its declared execution component's digest and parameters under domain-neutral; a report without one raises EvalExecutionUndeclared.
EvalCaseResolvedBeforeFreezeassurance.forecast.resolved-before-freezeA backtest forecast case whose resolution instant precedes its freeze instant raises EvalCaseResolvedBeforeFreeze.	A backtest forecast case resolved before its freeze instant.	assurance.forecast.resolved-before-freezeassurance.forecast.resolved-before-freezeA backtest forecast case whose resolution instant precedes its freeze instant raises EvalCaseResolvedBeforeFreeze.
ConformanceAlreadyRunningassurance.consumer.d1-admissionA cloudflare-d1 suite holds a lease row in the bound D1 from before its first reset until it ends, lapsing 120 s after its last renewal; a suite meeting a live lease refuses each required scenario with ConformanceAlreadyRunning.	Another suite holds a live admission lease on the bound D1 database.	assurance.consumer.d1-admissionassurance.consumer.d1-admissionA cloudflare-d1 suite holds a lease row in the bound D1 from before its first reset until it ends, lapsing 120 s after its last renewal; a suite meeting a live lease refuses each required scenario with ConformanceAlreadyRunning.
ConformanceBindingAbsentassurance.consumer.d1-absentA native contextful-full release cell without CONTEXTFUL_CONFORMANCE_D1_ENDPOINT runs no cloudflare-d1 pass; its report records binding origin absent and every required scenario skipped with ConformanceBindingAbsent.	A native full release cell holds no D1 binding, so its cloudflare-d1 pass does not run.	assurance.consumer.d1-absentassurance.consumer.d1-absentA native contextful-full release cell without CONTEXTFUL_CONFORMANCE_D1_ENDPOINT runs no cloudflare-d1 pass; its report records binding origin absent and every required scenario skipped with ConformanceBindingAbsent.
ShellCheckFailedassurance.automate.unchecked-shellA shell file in the tree that shellcheck rejects raises ShellCheckFailed in the toolchain stage.	A shell file in the tree that the shell linter rejects.	assurance.automate.unchecked-shellassurance.automate.unchecked-shellA shell file in the tree that shellcheck rejects raises ShellCheckFailed in the toolchain stage.
StagePredecessorMissingassurance.gate.stage-subsetA selected subset runs in the sequence's order; a stage reading an unselected predecessor's output, with that output absent, raises StagePredecessorMissing, naming both stages, before any stage runs.	A selected stage reading an unselected predecessor’s absent output.	assurance.gate.stage-subsetassurance.gate.stage-subsetA selected subset runs in the sequence's order; a stage reading an unselected predecessor's output, with that output absent, raises StagePredecessorMissing, naming both stages, before any stage runs.
SecretPlaintextassurance.gate.secret-ciphertextIn the schema stage, a key other than DOTENV_PUBLIC_KEY in a git-tracked .env file other than .env.example holding a value without the encrypted: prefix, or a tracked .env.keys, raises SecretPlaintext, naming file and key.	A tracked dotenv key holding a value other than dotenvx ciphertext, or a tracked private-key file.	assurance.gate.secret-ciphertextassurance.gate.secret-ciphertextIn the schema stage, a key other than DOTENV_PUBLIC_KEY in a git-tracked .env file other than .env.example holding a value without the encrypted: prefix, or a tracked .env.keys, raises SecretPlaintext, naming file and key.
SecretScopeMissingassurance.gate.secret-scopeIn the schema stage, a key other than DOTENV_PUBLIC_KEY in a git-tracked .env file whose block — the assignments above it, up to the first blank line — opens with no comment carrying text raises SecretScopeMissing, naming file and key.	A tracked dotenv key with no comment above it stating what it grants.	assurance.gate.secret-scopeassurance.gate.secret-scopeIn the schema stage, a key other than DOTENV_PUBLIC_KEY in a git-tracked .env file whose block — the assignments above it, up to the first blank line — opens with no comment carrying text raises SecretScopeMissing, naming file and key.
SurfaceCheckFailedassurance.gate.surface-check-failedA surface whose typecheck, unit tests or framework build fails raises SurfaceCheckFailed, naming the surface and the script.	A TypeScript surface whose typecheck, unit tests or framework build failed.	assurance.gate.surface-check-failedassurance.gate.surface-check-failedA surface whose typecheck, unit tests or framework build fails raises SurfaceCheckFailed, naming the surface and the script.
CrateGraphViolationassurance.gate.crate-graphThe crate-graph stage holds run-path crates to reaching read-path crates through the three crossing crates alone; another edge raises CrateGraphViolation, naming both crates.	A run-path crate reaching a read-path crate outside the three crossing crates.	assurance.gate.crate-graphassurance.gate.crate-graphThe crate-graph stage holds run-path crates to reaching read-path crates through the three crossing crates alone; another edge raises CrateGraphViolation, naming both crates.
EnforceUnmediatedPathassurance.gate.row-tokenEvery row-returning function of the store crate takes the enforcement token type, whose constructor is private to the enforcement module; a row path outside a registered relation raises EnforceUnmediatedPath, naming the function.	A row-returning path reaching stored rows outside a registered relation.	assurance.gate.row-tokenassurance.gate.row-tokenEvery row-returning function of the store crate takes the enforcement token type, whose constructor is private to the enforcement module; a row path outside a registered relation raises EnforceUnmediatedPath, naming the function.
DenyListDriftassurance.gate.deny-listdeny.toml holds one [bans] entry per crate or feature a profile-wide dependency refusal names, its reason that refusal's clause id; an entry missing or extra raises DenyListDrift, naming it.	A deny.toml entry missing for, or absent from, the profile-wide dependency refusals.	assurance.gate.deny-listassurance.gate.deny-listdeny.toml holds one [bans] entry per crate or feature a profile-wide dependency refusal names, its reason that refusal's clause id; an entry missing or extra raises DenyListDrift, naming it.
UnconfiguredEgressassurance.gate.unconfigured-egressAn outbound call reachable under the default configuration — usage ping, license check, update probe — raises UnconfiguredEgress in the crate-graph stage, naming the call site.	An outbound call a default configuration reaches without operator configuration.	assurance.gate.unconfigured-egressassurance.gate.unconfigured-egressAn outbound call reachable under the default configuration — usage ping, license check, update probe — raises UnconfiguredEgress in the crate-graph stage, naming the call site.
EnforceInterpolatedSubjectClaimassurance.gate.interpolated-claimA source lint over the runtime crates finding a subject claim formatted into SQL text raises EnforceInterpolatedSubjectClaim, naming the file and line.	A subject claim formatted into SQL text in a runtime crate.	assurance.gate.interpolated-claimassurance.gate.interpolated-claimA source lint over the runtime crates finding a subject claim formatted into SQL text raises EnforceInterpolatedSubjectClaim, naming the file and line.
BuildDiskPreconditionassurance.gate.free-diskA stage starting with less than 2 GiB of free disk raises BuildDiskPrecondition and exits 28 before doing work.	A gate stage beginning below the free-disk floor.	assurance.gate.free-diskassurance.gate.free-diskA stage starting with less than 2 GiB of free disk raises BuildDiskPrecondition and exits 28 before doing work.
FootprintBudgetExceededassurance.gate.footprint-exceededAn artifact over its profile's budget, or carrying a dynamic dependency beyond the platform C library, raises FootprintBudgetExceeded, naming the profile.	A profile artifact over its budget, or carrying an extra dynamic dependency.	assurance.gate.footprint-exceededassurance.gate.footprint-exceededAn artifact over its profile's budget, or carrying a dynamic dependency beyond the platform C library, raises FootprintBudgetExceeded, naming the profile.
MeasureEntryUnresolvedassurance.measure.unresolved-entryAn entry whose owning clause, method or metric path resolves to nothing raises MeasureEntryUnresolved before any measure runs.	A ledger entry naming no clause, method or metric path.	assurance.measure.unresolved-entryassurance.measure.unresolved-entryAn entry whose owning clause, method or metric path resolves to nothing raises MeasureEntryUnresolved before any measure runs.
MeasureRecordMissingassurance.measure.recordA measure writes one JSON record carrying its entry id, value, sample count, seed and run stamp; a gate-tier method finishing without one raises MeasureRecordMissing.	A gate-tier method finishing without writing its record.	assurance.measure.recordassurance.measure.recordA measure writes one JSON record carrying its entry id, value, sample count, seed and run stamp; a gate-tier method finishing without one raises MeasureRecordMissing.
MeasureSeedMismatchassurance.measure.seed-mismatchA gate or scheduled record whose seed differs from its entry's declared seed raises MeasureSeedMismatch and counts as red; a trend mismatch leaves no comparable record.	A record carrying another seed than its ledger entry declares.	assurance.measure.seed-mismatchassurance.measure.seed-mismatchA gate or scheduled record whose seed differs from its entry's declared seed raises MeasureSeedMismatch and counts as red; a trend mismatch leaves no comparable record.
MeasureThresholdLoosenedassurance.measure.threshold-costA gate-tier target that rises under <=, falls under >= or moves under == carries a # cost: comment above its entry that its entry at <rev> lacks, or contextful-ci measure --since <rev> raises MeasureThresholdLoosened.	A gate-tier target loosened since the base revision without a new cost note.	assurance.measure.threshold-costassurance.measure.threshold-costA gate-tier target that rises under <=, falls under >= or moves under == carries a # cost: comment above its entry that its entry at <rev> lacks, or contextful-ci measure --since <rev> raises MeasureThresholdLoosened.
TagStoreFormatUnreadassurance.release.store-formatA commit's store format is the FormatVersion::CURRENT constant in its crates/contextful-core/src/store/lay_out.rs, and 1.0 where that constant is absent; a constant that does not parse raises TagStoreFormatUnread.	A store format constant whose major or minor does not parse as an integer.	assurance.release.store-formatassurance.release.store-formatA commit's store format is the FormatVersion::CURRENT constant in its crates/contextful-core/src/store/lay_out.rs, and 1.0 where that constant is absent; a constant that does not parse raises TagStoreFormatUnread.
TagManifestFormatUnreadassurance.release.manifest-formatA commit's manifest format is the MANIFEST_FORMAT constant in its crates/contextful-core/src/store/sync.rs, and 1 where that constant is absent; a constant that does not parse as an integer raises TagManifestFormatUnread.	A bucket manifest format constant that does not parse as an integer.	assurance.release.manifest-formatassurance.release.manifest-formatA commit's manifest format is the MANIFEST_FORMAT constant in its crates/contextful-core/src/store/sync.rs, and 1 where that constant is absent; a constant that does not parse as an integer raises TagManifestFormatUnread.
TagTreeDirtyassurance.release.dirty-treeA working tree or index differing from HEAD raises TagTreeDirty.	A tag requested over a working tree or index differing from HEAD.	assurance.release.dirty-treeassurance.release.dirty-treeA working tree or index differing from HEAD raises TagTreeDirty.
TagOffDefaultBranchassurance.release.off-branchA HEAD unreachable from the default branch, origin/HEAD unless --branch names another, raises TagOffDefaultBranch.	A tag requested on a commit the default branch does not reach.	assurance.release.off-branchassurance.release.off-branchA HEAD unreachable from the default branch, origin/HEAD unless --branch names another, raises TagOffDefaultBranch.
TagVersionRegressedassurance.release.version-regressedA computed version below the highest existing v<major>.<minor>.<patch> tag raises TagVersionRegressed, naming both.	A computed version below the highest existing version tag.	assurance.release.version-regressedassurance.release.version-regressedA computed version below the highest existing v<major>.<minor>.<patch> tag raises TagVersionRegressed, naming both.
TagFormatBreakPatchassurance.release.format-break-patchA computed <minor> equal to the highest existing tag's, while HEAD's store format major or manifest format differs from that tag's, raises TagFormatBreakPatch, naming both formats.	A store format major change under the highest existing tag’s minor version.	assurance.release.format-break-patchassurance.release.format-break-patchA computed <minor> equal to the highest existing tag's, while HEAD's store format major or manifest format differs from that tag's, raises TagFormatBreakPatch, naming both formats.
TagWorkspaceVersionMismatchassurance.release.workspace-versionA [workspace.package] version in HEAD's Cargo.toml that is absent or differs from the computed version raises TagWorkspaceVersionMismatch, naming both.	A workspace package version absent or differing from the computed tag version.	assurance.release.workspace-versionassurance.release.workspace-versionA [workspace.package] version in HEAD's Cargo.toml that is absent or differs from the computed version raises TagWorkspaceVersionMismatch, naming both.
TagGateFailedassurance.release.gate-failedOnce the other refusals clear, every gate stage runs against HEAD with HEAD~1 as base; a failing stage raises TagGateFailed, naming the stage's refusal, and no tag is created.	A gate stage failing on the commit a tag names.	assurance.release.gate-failedassurance.release.gate-failedOnce the other refusals clear, every gate stage runs against HEAD with HEAD~1 as base; a failing stage raises TagGateFailed, naming the stage's refusal, and no tag is created.
ReleaseTagVersionMismatchassurance.release.release-tag-versioncontextful-ci release over a HEAD carrying a v tag, none of which equals v plus the [workspace.package] version, raises ReleaseTagVersionMismatch, naming both, before any build.	A release build over a version tag that differs from the workspace package version.	assurance.release.release-tag-versionassurance.release.release-tag-versioncontextful-ci release over a HEAD carrying a v tag, none of which equals v plus the [workspace.package] version, raises ReleaseTagVersionMismatch, naming both, before any build.
DeployWorkflowRefusedassurance.deploy-apps.workflow-refusedAnother file under .github/workflows, or a deploy workflow breaching workflow-trigger, workflow-permissions, workflow-credentials, job-timeout or one-command, raises DeployWorkflowRefused in the schema stage, naming the file and the breach.	A workflow file other than the deploy workflow, or a deploy workflow outside its fixed shape.	assurance.deploy-apps.workflow-refusedassurance.deploy-apps.workflow-refusedAnother file under .github/workflows, or a deploy workflow breaching workflow-trigger, workflow-permissions, workflow-credentials, job-timeout or one-command, raises DeployWorkflowRefused in the schema stage, naming the file and the breach.
DeployCredentialsAbsentassurance.deploy-apps.credentials-absentcontextful-ci deploy cloudflare with CLOUDFLARE_API_TOKEN or CLOUDFLARE_ACCOUNT_ID unset or empty raises DeployCredentialsAbsent, naming the variable, before any command runs.	A deploy started without the Cloudflare API token or account identifier in its environment.	assurance.deploy-apps.credentials-absentassurance.deploy-apps.credentials-absentcontextful-ci deploy cloudflare with CLOUDFLARE_API_TOKEN or CLOUDFLARE_ACCOUNT_ID unset or empty raises DeployCredentialsAbsent, naming the variable, before any command runs.
DeployUnhealthyassurance.deploy-apps.healthAfter wrangler deploy, the command repeats an anonymous GET / to the URL wrangler reports until a status in the app's expected set arrives or --health-wait elapses, printing each status alone; the wait elapsing raises DeployUnhealthy, naming the last status.	A deployed app answering outside its expected status set, or not at all.	assurance.deploy-apps.healthassurance.deploy-apps.healthAfter wrangler deploy, the command repeats an anonymous GET / to the URL wrangler reports until a status in the app's expected set arrives or --health-wait elapses, printing each status alone; the wait elapsing raises DeployUnhealthy, naming the last status.

Bound	Value	Basis	Clause
assurance-formal-build-artifacts	2048 KiB	chosen	assurance.model.build-costassurance.model.build-costA cold elaboration of the package completes within 60 s and writes at most 2048 KiB of artifacts.
assurance-formal-build-time	60 s	chosen	assurance.model.build-costassurance.model.build-costA cold elaboration of the package completes within 60 s and writes at most 2048 KiB of artifacts.
assurance-assumption-allowlist	2 entries	chosen	assurance.audit-assumptions.allowlistassurance.audit-assumptions.allowlistThe assumption allowlist holds 2 entries, propext and Quot.sound, and every theorem's footprint is a subset of it.
assurance-recheck-wall-time	600 s	chosen	assurance.recheck.wall-timeassurance.recheck.wall-timeA recheck completes within 600 s.
assurance-counterexample-corpus	256 entries	chosen	assurance.differential-test.corpus-entriesassurance.differential-test.corpus-entriesThe counterexample corpus retains at most 256 entries, evicting the oldest case a fresh seed reproduces.
assurance-differential-budget	300 s	chosen	assurance.differential-test.run-budgetassurance.differential-test.run-budgetOne invocation, corpus replay included, completes within 300 s.
assurance-test-first-base-run	300 s	chosen	assurance.test.base-run-boundassurance.test.base-run-boundOne test-first execution against the base, its build excluded, runs for at most 300 s; a run past the bound is killed with its process group and counts as failing.
assurance-precision-floor	60 percent	chosen	assurance.evaluate.precision-floorassurance.evaluate.precision-floorPrecision at rank min(k, R), R being the relevant-set size, holds at or above 60 percent.
assurance-forbidden-row-rate	0 percent	chosen	assurance.evaluate.forbidden-row-rateassurance.evaluate.forbidden-row-rateA row named in a must-not-retrieve set holds at 0 percent of a regression case's returned rows.
assurance-duplicate-row-rate	0 percent	chosen	assurance.evaluate.duplicate-row-rateassurance.evaluate.duplicate-row-rateA repeated table-and-row-key pair holds at 0 percent of the ranking.
assurance-in-window-rate	95 percent	chosen	assurance.evaluate.in-window-rateassurance.evaluate.in-window-rateA case declaring a recency bound holds its in-window rate at or above 95 percent.
assurance-default-dead-band	2 percent	chosen	assurance.baseline.default-dead-bandassurance.baseline.default-dead-bandA rate-valued entry with no override gates at a 2 percent dead band.
assurance-rank-dead-band	3 percent	chosen	assurance.baseline.rank-quality-dead-bandassurance.baseline.rank-quality-dead-bandThe ranked-quality entry gates at a 3 percent dead band.
assurance-gated-mean-cases	30 cases	chosen	assurance.baseline.unresolvable-pathassurance.baseline.unresolvable-pathA path resolving to nothing, a mean over fewer than 30 cases, a malformed entry or a non-finite band raises BaselinePathUnresolved before the suite runs.
assurance-bootstrap-resamples	1000 resamples	chosen	assurance.baseline.intervalassurance.baseline.intervalEach judged figure reports a 95 percent percentile-bootstrap interval over cases from 1000 resamples.
assurance-interval-level	95 percent	chosen	assurance.baseline.intervalassurance.baseline.intervalEach judged figure reports a 95 percent percentile-bootstrap interval over cases from 1000 resamples.
assurance-forecast-coverage	95 percent	chosen	assurance.forecast.coverage-floorassurance.forecast.coverage-floorA forecaster answering below 95 percent of a round's cases is reported unranked.
assurance-d1-admission-lease	120 s	chosen	assurance.consumer.d1-admissionassurance.consumer.d1-admissionA cloudflare-d1 suite holds a lease row in the bound D1 from before its first reset until it ends, lapsing 120 s after its last renewal; a suite meeting a live lease refuses each required scenario with ConformanceAlreadyRunning.
assurance-shell-lines	5 lines	chosen	assurance.automate.typed-subcommandassurance.automate.typed-subcommandAn automation step carrying a branch, a loop or a retry, or running past 5 lines, is a typed subcommand shelling out to compiled binaries.
assurance-cli-shard-wall-clock	9 min	chosen	assurance.gate.cli-shard-mapassurance.gate.cli-shard-maptools/ci/cli-shards.toml assigns each remaining CLI test, a nested-build group whole, one shard by recorded duration within 9 min per shard; an unmapped test, reported as drift, joins its group or the least-loaded shard, which adds unit tests and doctests.
assurance-job-memory	3 GiB	chosen	assurance.gate.parallel-jobsassurance.gate.parallel-jobsA footprint build's parallel job count is its build memory — the cgroup memory ceiling, else the physical or container-engine memory — divided by 3 GiB, at least one and at most the processor count.
assurance-stage-free-disk	2 GiB	chosen	assurance.gate.free-diskassurance.gate.free-diskA stage starting with less than 2 GiB of free disk raises BuildDiskPrecondition and exits 28 before doing work.
assurance-edge-compressed	50 MiB	chosen	assurance.gate.edge-budgetassurance.gate.edge-budgetThe edge profile compresses to at most 50 MiB.
assurance-full-compressed	150 MiB	chosen	assurance.gate.full-budgetassurance.gate.full-budgetThe full profile compresses to at most 150 MiB.
assurance-control-compressed	60 MiB	chosen	assurance.gate.control-budgetassurance.gate.control-budgetThe control profile compresses to at most 60 MiB.
assurance-timing-iterations	200 repeats	chosen	assurance.measure.timing-iterationsassurance.measure.timing-iterationsA timed batch reports p50 and p95 over 200 repeats of its operation, each after warm-up.
assurance-timing-batches	5 repeats	chosen	assurance.measure.timing-batchesassurance.measure.timing-batchesA timed figure is the median of 5 repeats of its timed batch.
assurance-trend-band	25 percent	chosen	assurance.measure.trend-bandassurance.measure.trend-bandA trend figure more than 25 percent worse than its baseline annotates the run report and fails no stage.
assurance-deploy-job-timeout	90 min	chosen	assurance.deploy-apps.job-timeoutassurance.deploy-apps.job-timeoutThe deploy job's timeout-minutes is at most 90 min.
assurance-deploy-builder-job-memory	1536 MiB	chosen	assurance.deploy-apps.builder-jobsassurance.deploy-apps.builder-jobsThe builder compiles with the caller's CARGO_BUILD_JOBS when set, and otherwise with one job per 1536 MiB of the memory docker info reports, at least one.

Section	Cited by
A-assurance#assurance-claims-carry	assurance.prove.commutation-claimassurance.prove.commutation-claimA claim that the enforcement stages commute raises CommutationClaimed., assurance.prove.sampled-inclusionassurance.prove.sampled-inclusionInclusion decided by evaluating a fixed set of example values raises ZoneInclusionSampled., assurance.prove.unbound-targetassurance.prove.unbound-targetA target the claim names with no binding raises ProofTargetUnbound, naming the target., assurance.prove.no-negative-spaceassurance.prove.no-negative-spaceA theorem published without its negative space raises TheoremWithoutNegativeSpace, naming the constant., assurance.audit-assumptions.assumption-outside-allowlistassurance.audit-assumptions.assumption-outside-allowlistAn assumption in a footprint and absent from the allowlist raises AssumptionOutsideAllowlist, printing the constant and the assumption., assurance.audit-assumptions.hole-assumptionassurance.audit-assumptions.hole-assumptionA footprint containing the hole assumption raises ProofHoleAssumption, naming the declaration, whatever its syntax spells., assurance.audit-assumptions.native-evaluation-assumptionassurance.audit-assumptions.native-evaluation-assumptionA footprint containing a per-declaration native-evaluation assumption raises NativeEvaluationAssumption, naming the declaration that minted it., assurance.audit-assumptions.missing-constantassurance.audit-assumptions.missing-constantA required constant absent from the elaborated environment raises TheoremConstantMissing., assurance.audit-assumptions.statement-driftassurance.audit-assumptions.statement-driftA required constant whose elaborated statement differs from its expected text raises TheoremStatementDrift, printing both., assurance.audit-assumptions.allowlist-admissionassurance.audit-assumptions.allowlist-admissionAn assumption joins the allowlist through an A-assurance section naming it, and each inventory row admitting it cites that section in a record field., assurance.recheck.credential-freeassurance.recheck.credential-freeA recheck environment exposing a token, a signing key or a registry login raises RecheckEnvironmentCredentialed, naming the variable or file carrying it., assurance.scope-claim.beyond-named-decisionsassurance.scope-claim.beyond-named-decisionsA claim that the enforcement engine, or any object wider than the named decisions, is verified raises ClaimBeyondNamedDecisions., assurance.scope-claim.unnamed-dependencyassurance.scope-claim.unnamed-dependencyA claim resting on a component absent from its trusted-dependency list raises TrustedDependencyUnnamed, naming the component.
A-assurance#backtests-estimate-leakage	assurance.backtest.cutoff-sliceassurance.backtest.cutoff-sliceA backtest report places each case by its resolution instant minus the reader's post-training cutoff and states leakage against a declared reference, a cutoff discontinuity or a clean control model, never a bare pre/post gap., assurance.backtest.fill-instantassurance.backtest.fill-instantA financial execution profile fills each decision at the first price available strictly after the decision's recorded instant., assurance.backtest.execution-componentassurance.backtest.execution-componentA backtest report stamps its declared execution component's digest and parameters under domain-neutral; a report without one raises EvalExecutionUndeclared., assurance.forecast.tracks-separateassurance.forecast.tracks-separateBacktest, prospective, tool-free and tool-using scores never pool into one figure.
A-assurance#case-s-judge	assurance.backtest.cutoff-sliceassurance.backtest.cutoff-sliceA backtest report places each case by its resolution instant minus the reader's post-training cutoff and states leakage against a declared reference, a cutoff discontinuity or a clean control model, never a bare pre/post gap., assurance.backtest.leak-scoreassurance.backtest.leak-scoreThe case's judge model scores each retrieved document 0 to 4 against a reference answer from rows available before the horizon, landing one row per document and case horizon; the report gives Brier per leak tier.
A-assurance#columnar-read-statement	assurance.build.linked-query-functionsassurance.build.linked-query-functionsColumnar file reading and statement serialization link into every build linking the SQL engine, and the read path loads no extension while serving., assurance.build.runtime-extension-loadassurance.build.runtime-extension-loadA read path loading an extension into a binary that statically links the SQL engine raises ExtensionAutoloadRefused.
A-assurance#consumer-compatibility-binds	assurance.consumer.suiteassurance.consumer.suitecontextful-conformance --binary <path> --output <report> executes its versioned scenarios through the supplied artifact's public CLI and HTTP surfaces outside a source checkout., assurance.consumer.requirementsassurance.consumer.requirementsEvery required scenario executes its declared capabilities; a missing capability or unsupported storage profile records unsupported, names its requirement and refuses consumer activation., assurance.consumer.d1-profileassurance.consumer.d1-profileA cloudflare-d1 verdict runs the supplied contextful-full artifact against D1 and R2 bindings, replaces its local disk, and records every required outcome independently of the local and PostgreSQL profiles., assurance.consumer.d1-releaseassurance.consumer.d1-releaseRelease evidence binds a cloudflare-d1 report to the artifact digest, source revision, suite revision and storage profile; a required failure, unsupported case, skip or unverified binding supplies no compatibility verdict.
A-assurance#decision-module-compiles	assurance.differential-test.harnessassurance.differential-test.harnessThe harness drives the reference binary and the decision module's native and WebAssembly builds over each generated case and compares their decisions field by field., assurance.differential-test.buildsassurance.differential-test.buildsThe native build decides in process and the wasm32-unknown-unknown build under the decision-module host; absent --wasm, the command compiles the module from the working tree, and the report names the builds compared., assurance.differential-test.disagreementassurance.differential-test.disagreementA case on which any two of the three decisions differ raises ReferenceModelDrift, printing the minimized case and every decision., assurance.structure-tree.decision-moduleassurance.structure-tree.decision-moduleOne module owns the enforcement decision; a gateway and the engine reaching the same verdict execute it, compiled native and to WebAssembly from one pinned source.
A-assurance#differentially-tested-reference	assurance.differential-test.discarded-counterexampleassurance.differential-test.discarded-counterexampleA run reporting a disagreement and writing no corpus entry raises CounterexampleDiscarded.
A-assurance#duplicated-capabilities-match	assurance.structure-tree.capability-registryassurance.structure-tree.capability-registryspec/capabilities.toml names each capability of one-home with one home path and one or more defining symbols; an absent registry, a missing or doubled capability, an absent home or an undefined symbol raises CapabilityHomeUnresolved., assurance.structure-tree.cross-languageassurance.structure-tree.cross-languageThe crate-graph stage matches Rust, TypeScript, JavaScript and Python functions, types and constants outside a home by name folded to lowercase without separators, against its symbols and its literal constants' names and values.
A-assurance#edge-profile-ships	assurance.build.wasi-probeassurance.build.wasi-probeNo profile ships a wasm32-wasip2 release; a scheduled-tier ledger entry builds the edge profile for it and holds the compressed artifact to edge-budget., assurance.build.release-artifactassurance.build.release-artifactEach profile ships a release archive with a SHA-256 checksum and an SBOM, a package-manager formula and an independently tagged container image; the bare formula name and the install script resolve to the full profile.
A-assurance#evaluation-data-follows	assurance.evaluate.policy-labelsassurance.evaluate.policy-labelsAn evaluation corpus carries zone and row-policy labels in its table declarations, and a run reads it through the access-control path under one admitted credential., assurance.evaluate.unlabeled-corpusassurance.evaluate.unlabeled-corpusA run over a corpus whose tables declare no zone or row policy, with no local: zone passed as --zone, raises EvalCorpusUnlabeled before any row lands., assurance.baseline.golden-custodyassurance.baseline.golden-custodyVersion-controlled JSONL under evals/cases/ is the canonical golden set, one loader is its only ingestion door, and a reviewer's edit reaches the gate as a change to the tree., assurance.baseline.answer-key-in-the-storeassurance.baseline.answer-key-in-the-storeAn artifact path normalizing under the evaluation directory, reached by a manifest lint or a connector, raises GoldenSetIngested., assurance.baseline.generated-redactionassurance.baseline.generated-redactionA golden mined from a live query or promoted from a labeled outcome passes write-time before commit; a case it cannot redact raises GoldenRedactionFailed., assurance.baseline.trace-exportassurance.baseline.trace-exportA run touching a deployed store with a hosted trace endpoint configured raises TraceExportOutOfPerimeter; hosted collection serves runs over public or synthetic fixtures alone.
A-assurance#executed-reference-proved	assurance.differential-test.reference-modelassurance.differential-test.reference-modelThe reference model is the policy package's proved decision definitions, compiled with JSON case decoding and decision rendering into a binary that reads one case on standard input and prints one decision.
A-assurance#feature-runs-formal	assurance.gate.nightly-tierassurance.gate.nightly-tiercontextful-ci stages --parts --tier nightly prints the features, formal, unwired and budget parts in run order; stages --parts prints the remaining parts, those a change runs before merge, and gate --stage runs a part of either tier.
A-assurance#gate-repair-evidence	assurance.test.base-evidenceassurance.test.base-evidenceTest-first reports assertion failures, compilation failures and bounded test executions separately; infrastructure faults follow base-unrunnable and supply no failing-test evidence., assurance.build.checkout-artifactsassurance.build.checkout-artifacts.cargo/config.toml names the checkout root, and every workspace package's build script folds its canonical path into the package fingerprint, so a shared target directory recompiles workspace packages per checkout while unchanged dependencies stay fresh., assurance.build.runtime-checkoutassurance.build.runtime-checkoutReusable test helpers resolve the workspace root and tested binary from explicit runtime inputs bound to the invocation; cached helpers carry no compile-time checkout path deciding which source or binary runs.
A-assurance#generated-artifacts-prove	corpus.render.generatedcorpus.render.generatedcontextful-spec state regenerates spec/status.md, spec/targets.md, spec/cards/ and spec/spec.lock.json, and contextful-spec extract the lock file alone. A committed copy differing from regeneration raises SpecStaleRender., assurance.structure-tree.derivation-checkassurance.structure-tree.derivation-checkA generated artifact declares the check that fails once its source moves, and the gate's schema stage runs that check.
A-assurance#mediation-ranges-over	assurance.prove.restriction-preservationassurance.prove.restriction-preservationattenuateAll_permits_every_parent_block: every block of a credential admits each request that any chain of attenuations of that credential permits, under one trusted environment., assurance.prove.mediation-relationassurance.prove.mediation-relationstatement_reach_released_rows_pass_session_layers: the mediation induction ranges over the read path's statement execution, and every row a reachable state has released passed every layer of the session.
A-assurance#model-specifies-profile	assurance.model.declared-dependencyassurance.model.declared-dependencyA require stanza in the policy package's lakefile.toml reaching any external library raises FormalPackageDependency, naming the library., assurance.model.unmodelled-constructorassurance.model.unmodelled-constructorA category the manifest admits with no case in the placement inductive raises UnmodelledConstructor at elaboration, naming the category.
A-assurance#profile-graphs-answer	assurance.gate.dependency-denyassurance.gate.dependency-denyThe crate-graph stage runs pinned cargo-deny check bans over each profile's resolved graph, denying every crate a profile-wide dependency refusal names; a hit raises that refusal's error, naming the profile and the path., assurance.gate.deny-profile-graphassurance.gate.deny-profile-graphA profile's graph is the binary resolved with default features off and the profile's feature on, across every target, excluding development dependencies; the stage prints each profile the binary declares no feature for.
A-assurance#protocol-package-holds	assurance.model.journal-modelassurance.model.journal-modelThe journal model is a total, computable step function over three callers and two keys; each journal-store and blob-store port call, effect, lapse, crash, sweep and retirement is one step., assurance.model.merge-modelassurance.model.merge-modelThe merge model decides each key from its local entry, remote entry, remote tombstone, held flag and verification flag; one differing commit-log copy refuses the whole merge., assurance.model.fold-modelassurance.model.fold-modelThe fold model is a total, computable step function over two passes staging, committing and dying, lease acquisition, collection and two readers; a pass commits only while its fence is the highest granted., assurance.differential-test.journal-harnessassurance.differential-test.journal-harnessThe journal harness runs each caller's Journal::step on a thread over gated memory, file and SQLite adapters, one port call per step, comparing rows, blobs and caller phases with the model., assurance.differential-test.journal-driftassurance.differential-test.journal-driftA step after which the journal model and an adapter differ raises JournalConformanceDrift, printing the adapter, the minimized sequence and both states., assurance.differential-test.merge-driftassurance.differential-test.merge-driftA case on which the merge model and merge_verified differ raises MergeConformanceDrift, printing the minimized case and both merges., assurance.differential-test.fold-harnessassurance.differential-test.fold-harnessThe fold differential replays seeded step sequences through prepare_under, commit and collect over a file-backed store, comparing pointer, chain, directories and readers with protocol fold run after every step.
A-assurance#pull-request-runs	assurance.gate.affected-partsassurance.gate.affected-partscontextful-ci stages --parts --base <rev> --affected lists, in run order, the parts of the selected tier the diff from the merge base of <rev> and HEAD reaches, the required tier always including preflight., assurance.gate.affected-everyassurance.gate.affected-everyA change to Cargo.toml, Cargo.lock, a toolchain file, anything under crates/, tools/ or .github/, or any path no other affected clause maps reaches every part of either tier., assurance.gate.affected-specassurance.gate.affected-specA change under spec/ or references/ reaches test-first validation, one under spec/ the foundation workspace part, and each clause whose statement or spec/pins.toml entry changed the parts running its pinned test or theorem., assurance.gate.affected-surfacesassurance.gate.affected-surfacesA change under apps/ or packages/ reaches the TypeScript surfaces, acceptance and crate-graph parts., assurance.gate.affected-formalassurance.gate.affected-formalA change under formal/ other than a lean-toolchain file reaches the formal and evaluate stages, the foundation, CLI and CLI differential workspace parts, and every feature part.
A-assurance#source-change-carries	corpus.state.theorem-beside-testcorpus.state.theorem-beside-testA clause carries at most one theorem pin beside its test pins. A theorem pin alone states a property of a model, and performs once its proof holds no sorry., corpus.state.acceptancecorpus.state.acceptanceA milestone's Acceptance: line names one test under crates/acceptance/; that test computes absent when undefined, open when ignored or holding a body line that opens with todo!, and passing otherwise., corpus.state.acceptance-firstcorpus.state.acceptance-firstA milestone holding a pinned clause while its acceptance test computes absent raises SpecAcceptanceMissing., assurance.test.test-firstassurance.test.test-firstA change altering Rust source under crates/ or tools/ adds or alters a test under a package's tests/ that fails against the base commit's source; a change without one raises TestNotFirst., assurance.test.acceptance-surfaceassurance.test.acceptance-surfaceAn acceptance test drives a built binary through its command line, MCP or HTTP surface; a workspace package among the acceptance package's dependencies raises AcceptanceLinksEngine.
A-assurance#stage-subset-runs	assurance.gate.stage-sequenceassurance.gate.stage-sequenceThe gate runs its stages in order — pins, toolchain, schema, test-first, workspace, acceptance, evaluate, features, crate graph, connectors, TypeScript surfaces, formal, unwired, budget — all of both tiers when none is named, else the named subset, which --plan prints., assurance.gate.stage-subsetassurance.gate.stage-subsetA selected subset runs in the sequence's order; a stage reading an unselected predecessor's output, with that output absent, raises StagePredecessorMissing, naming both stages, before any stage runs.
A-assurance#store-format-major	assurance.release.versionassurance.release.versionA release tag is v0.<minor>.<patch>: <minor> counts the milestones computing closed in the tagged commit's spec/status.md plus each store format major and each manifest format past 1, and <patch> counts the existing tags v0.<minor>.., assurance.release.store-formatassurance.release.store-formatA commit's store format is the FormatVersion::CURRENT constant in its crates/contextful-core/src/store/lay_out.rs, and 1.0 where that constant is absent; a constant that does not parse raises TagStoreFormatUnread., assurance.release.manifest-formatassurance.release.manifest-formatA commit's manifest format is the MANIFEST_FORMAT constant in its crates/contextful-core/src/store/sync.rs, and 1 where that constant is absent; a constant that does not parse as an integer raises TagManifestFormatUnread., assurance.release.version-regressedassurance.release.version-regressedA computed version below the highest existing v<major>.<minor>.<patch> tag raises TagVersionRegressed, naming both., assurance.release.format-break-patchassurance.release.format-break-patchA computed <minor> equal to the highest existing tag's, while HEAD's store format major or manifest format differs from that tag's, raises TagFormatBreakPatch, naming both formats.
A-assurance#store-protocol-modelled	assurance.model.packageassurance.model.packageThe policy model is a Lean package rooted at formal/: lakefile.toml declares one lean_lib target and no require stanza, and lean-toolchain names one exact release string., assurance.model.toolchain-driftassurance.model.toolchain-driftA build whose resolved toolchain string differs from the pinned one raises ProofToolchainDrift, printing both strings., assurance.model.protocol-packageassurance.model.protocol-packageThe protocol model is a second Lean 4 package rooted at formal/protocol/, beside the policy package, pinned to the same lean-toolchain string, with one lean_lib target, one lean_exe target and no require stanza., assurance.model.protocol-modelassurance.model.protocol-modelThe protocol model is a total, computable step function over two lease paths, the compaction lease guarding a table pointer and the run lease guarding a commit log: grant, raise, renewal, expiry, release, fenced commit, pause, message delay and crash., assurance.model.protocol-safetyassurance.model.protocol-safetyFive invariants are Lean theorems over every reachable state of both paths: one lease holder per fence, fences only increase, no commit after a successor's acquisition, no lost update, and release keeps the lease object and its fence., assurance.differential-test.protocol-harnessassurance.differential-test.protocol-harnessThe harness drives the protocol executable and the store's own lease calls, Syncer over a scripted bucket and the local catalog with the commit log, through each case, comparing lease, fence, head, write count and node views after every step., assurance.differential-test.protocol-driftassurance.differential-test.protocol-driftA step after which the model's state and the store's projected state differ raises ProtocolConformanceDrift, printing the minimized operation sequence and both states.
A-assurance#tracked-targets-gate	assurance.measure.trend-directionassurance.measure.trend-directionEach trend-tier ledger entry declares higher_is_better or lower_is_better for its metric., assurance.measure.trend-baselineassurance.measure.trend-baselineA trend figure compares with the newest earlier successful default-branch report for the same entry and seed under runner-stamp; absent matching history yields no annotation., assurance.measure.historyassurance.measure.historyA run on the default branch attaches its run report to the measured commit under refs/notes/measures, and no verdict reads a note.
A-assurance#version-tag-names	assurance.release.annotatedassurance.release.annotatedcontextful-ci tag creates a signed annotated tag on HEAD naming the closed milestones once every refusal of this operation clears, and never moves or replaces an existing tag., assurance.release.off-branchassurance.release.off-branchA HEAD unreachable from the default branch, origin/HEAD unless --branch names another, raises TagOffDefaultBranch., assurance.release.workspace-versionassurance.release.workspace-versionA [workspace.package] version in HEAD's Cargo.toml that is absent or differs from the computed version raises TagWorkspaceVersionMismatch, naming both., assurance.release.gate-failedassurance.release.gate-failedOnce the other refusals clear, every gate stage runs against HEAD with HEAD~1 as base; a failing stage raises TagGateFailed, naming the stage's refusal, and no tag is created.
A-assurance#windows-release-support	assurance.build.targetsassurance.build.targetsAll three profiles cross-compile to x86_64-unknown-linux-musl and aarch64-unknown-linux-musl; edge and full also build for aarch64-apple-darwin and x86_64-apple-darwin., assurance.build.windows-targetassurance.build.windows-targetWindows targets are excluded from the release matrix; no profile publishes Windows artifacts.
A-assurance#workspace-fits-stage	assurance.gate.workspace-partsassurance.gate.workspace-partsThe workspace parts compile the feature-unified workspace untested, run differential CLI tests apart and remaining CLI tests in eight shards under cli-shard-map, and each other non-acceptance package suite in one of four groups., assurance.gate.cli-shard-mapassurance.gate.cli-shard-maptools/ci/cli-shards.toml assigns each remaining CLI test, a nested-build group whole, one shard by recorded duration within 9 min per shard; an unmapped test, reported as drift, joins its group or the least-loaded shard, which adds unit tests and doctests.