Docs / Specification

A-assurance — Assurance decisions

Status: accepted

consumer-compatibility-binds — Consumer compatibility binds execution evidence to artifact bytes

Cited byassurance.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 manifest parse establishes neither replay behavior nor receiver durability, and a release version does not establish source correspondence. A consumer reproduces the verdict outside the checkout with no inherited provider account.

assurance-claims-carry — Assurance claims carry their qualifiers, and the proof gate audits assumptions

Cited byassurance.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 hand-maintained inventory checks each constant’s transitive assumption footprint against a two-entry allowlist. The package holds no dependency, so two machines reach one verdict offline.

Revisit: a mathematics library elaborates inside the per-change budget.

evaluation-data-follows — Evaluation data follows store policy

Cited byassurance.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.

An evaluation that bypasses enforcement never shows an over-restrictive policy as a recall regression. A zero in a report is then a retrieval fact.

model-specifies-profile — The model specifies the profile-to-effective-authority mapping, each target bound to one query path

Cited byassurance.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.

Proving a self-owned wire protocol re-opens every proof on each protocol correction. The delegation library, its cryptography and its parser are trusted dependencies the claim names.

Revisit: the profile’s maintainer changes the mapping’s domain; a defect surfaces in the trusted remainder.

mediation-ranges-over — Mediation ranges over statement execution, and restriction preservation is a proof target

Cited byassurance.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 run step reaches stored rows only through a read-path statement, so statement execution is the object the induction ranges over. Run-step effects answer to the protocol model’s fences.

Revisit: the read path releases a row outside a statement; the model gains SQL semantics.

differentially-tested-reference — A differentially tested reference model is the standing link between proofs and binary

Cited byassurance.differential-test.discarded-counterexampleassurance.differential-test.discarded-counterexampleA run reporting a disagreement and writing no corpus entry raises CounterexampleDiscarded.

A refinement proof through a broken translator passes about the wrong object and leaves nothing to inspect. A differential leaves a minimized case.

Revisit: a pinned, reproducible translation toolchain exists; a production divergence falls outside the malformed, boundary and well-formed classes.

executed-reference-proved — The executed reference model is the proved definitions

Cited byassurance.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 disagreement implicates the proved definitions directly, and every theorem over Authority.Grant speaks about the function the harness executes.

Revisit: a misreading of a clause reaches a release through a definition both proofs and differential accepted.

store-protocol-modelled — The store protocol is modelled in Lean 4

Cited byassurance.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 commit between a successor’s grant and raise lands below the highest grant and loses nothing. A theorem proves each invariant for every lease generation, where a model checker bounds it.

Revisit: the bounded check exceeds the formal stage’s wall clock; a maintained Rust bridge to a model checker reaches the protocol’s step vocabulary.

columnar-read-statement — The columnar-read and statement-serialization functions link into every engine-linked build

Cited byassurance.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.

An autoloaded extension brings a second copy of the engine’s type information. A cast between copies aborts, and on Apple platforms corrupts reads.

Revisit: the engine resolves extensions against the host binary’s type tables; a profile’s footprint budget cannot absorb 55 MiB.

source-change-carries — A source change carries a test that fails first, and a milestone carries its acceptance test before it progresses

Cited bycorpus.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 test written after its code is textually identical to one written first, so only a run against the base commit tells them apart.

Revisit: the base-commit build exceeds the stage wall clock; the refactor trailer appears on changes that alter a public surface.

tracked-targets-gate — Tracked targets gate on counts and record per commit in notes

Cited byassurance.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.

Status: proposed

Wall-clock and resident-memory figures move on shared containers, so they annotate and gate nothing. Gate-tier targets measure counts, within-run ratios or locked-resolve sizes.

Revisit: a dedicated runner class holds p95 within 5 percent across runs.

version-tag-names — A version tag names a gated revision and counts closed milestones

Cited byassurance.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 consumer pinning a bare commit reads no promise. Derivability from computed state decided the scheme, so no mislabelled tag can be cut. Below v1 no surface promises compatibility.

Revisit: an external consumer needs a compatibility promise on a public surface, which opens v1.

store-format-major — A store format major moves the release minor

Cited byassurance.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 consumer pinning ~0.16 takes every v0.16.* tag as a patch, yet a build reading format 1.x refuses a table format 2.0 writes. The commit counter marker declares the same format_version, so it counts with the manifest major. The bucket manifest’s MANIFEST_FORMAT counts the same way, since a build parsing manifest format 1 refuses format 2.

Consequences: 16 closed milestones under format 2.0 compute v0.17.0; the tag message names the reader-first upgrade order. Revisit: the store format promises compatibility across majors, or v1 opens.

workspace-fits-stage — The workspace fits the stage wall clock through parts

Cited byassurance.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.

The feature-unified workspace suite exceeds the 1800 s sandbox cap on a cold build. Tests sharing one costly nested build stay on one shard.

feature-runs-formal — Feature runs, formal checks and profile budgets run in a nightly tier

Cited byassurance.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.

The features, formal and budget parts each need a cold build of their own feature set or profile. P7 keeps a nightly cadence for a check too costly per change, naming the change range.

Revisit: pull-request parts share builds, so the nightly parts fit a 30 min verdict.

decision-module-compiles — One decision module compiles native and to WebAssembly

Cited byassurance.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.

One verdict computed from two sources drifts. The gateway needs verification, admission and placement, never SQL, under a host with no JavaScript. The module imports only the credential library’s evaluator clock.

profile-graphs-answer — Profile graphs answer to cargo-deny bans, one run per profile feature

Cited byassurance.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.

One walk over workspace-unified metadata cannot tell which profile pulled a crate. A red check follows a change, not the calendar, so advisories stay out.

edge-profile-ships — The edge profile ships no WASI release, and a scheduled probe measures it

Cited byassurance.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.

The SQL engine relies on threads, file locks and a statically linked extension set that wasm32-wasip2 does not provide. A target’s viability is a measured figure.

gate-repair-evidence — Gate repair evidence binds one checkout and one comparison

Cited byassurance.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.

Workspace artifacts retain checkout paths, and a timeout without phase evidence hides whether compilation or tests exhausted the budget. Each verdict identifies its source, comparison and failure class.

Revisit: representative timings show checkout isolation or partitioning exceeds the declared resource budget.

windows-release-support — Windows release support is deferred independently of Linux and macOS delivery

Cited byassurance.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.

Native Windows execution adds MSVC toolchains, executor registration and descendant-lifetime verification to the release boundary.

Revisit: a Windows support decision carries passing MSVC lifetime, filesystem and read-engine evidence for each admitted architecture within the gate budget.

stage-subset-runs — A stage subset runs in sequence order and refuses a missing predecessor

Cited byassurance.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 part in a fresh checkout holds no earlier stage’s output, and a gate fails rather than skips (P7). A predecessor’s output already on disk satisfies its reader.

generated-artifacts-prove — Generated artifacts prove currency by regeneration and diff

Cited bycorpus.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 generated file can keep a plausible header after its source changes. Neither a hand-maintained hash nor a generator’s exit status shows a stale committed byte.

duplicated-capabilities-match — Duplicated capabilities match registered symbols and home constants by folded name

Cited byassurance.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 second implementation can sit in a TypeScript gateway or a Python script, where no compiler sees both. Folding singleStatement to single_statement needs no parser beyond Rust.

Revisit: a copy under another name escapes to production.

backtests-estimate-leakage — Backtests estimate leakage against a reference, and their tracks never pool

Cited byassurance.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.

Recency alone lifts accuracy near a cutoff, so a reported leak survives a model that cannot have seen the outcome. Consumer-selected profiles own return scoring, price fills and decoding corrections.

case-s-judge — The case’s judge scores leakage against a pre-horizon reference

Cited byassurance.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.

The score feeds the Brier-per-tier report and the zero threshold a late snapshot capture answers under.

pull-request-runs — A pull request runs the parts its diff reaches

Cited byassurance.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.

Running every part makes a prose change wait hours behind binary feature suites. No change skips a part its diff can reach.

protocol-package-holds — The protocol package holds the journal, merge and fold machines

Cited byassurance.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.

run.journalrun.journalThe journal records step values, returns those values on replay and deletes records after execution retirement. and store.mergestore.mergeMerging bucket manifests across writers, verifying tombstones and retrying conditional manifest commits. carry the engine’s concurrency risk. One toolchain and one audit cover them, beside five policy modules.

Consequences: no_dangling_blob holds under the grace hypothesis; --no-grace reproduces BlobMissingrun.journal.missing-blobIf a row references a missing blob, the journal raises BlobMissing carrying the reference. The journal returns no empty replacement value. on every adapter.