Crate bvisor

Expand description

bvisor-core — platform-agnostic boundary contract.

ZERO OS code, ZERO BatPak writes in the Backend trait.

bvisor is a sync-first boundary supervisor. The Boundary Adapter Layer (BAL, prose only) lowers admitted Capabilitys + HostControls from a BoundaryPlan into honest platform Backends; the BoundaryRunner SEALS a BoundaryReport and the host PERSISTS it into BatPak.

The loop (sealing ownership made precise):

BoundarySpec     asks      (Capabilities + HostControls + workload)
BoundaryPlanner  admits    → BoundaryPlan   (inert IR, bound to backend + machine profile; fail-closed)
Backend          OBSERVES  → BoundaryReportBody (unsealed facts; no hashing, no BatPak)
BoundaryRunner   SEALS     → BoundaryReport (canonicalize + body_hash)  [SEALED ≠ persisted]
Host             PERSISTS  → appends 0xE event into BatPak              [now durable; replay reconstructs]

C0 scope: the pure contract + a fail-closed planner + the honest InertBackend. No real OS backends, no SimBackend, no host wiring yet.

Modules§

linux: Linux backend — landlock + cgroup-v2 + launcher-process confinement.
macos: macOS backend — Seatbelt (sandbox_init) confinement (scaffolding).
wasm: Wasm backend — wasmi + WASI-preopen confinement.
windows: Windows backend — AppContainer + Job Object confinement (scaffolding).

Structs§

AdmissionInputs: The normalized, immutable admission inputs — (S,P,V,L,Q,B) reduced to the membrane-relevant encoded form. Probed and normalized ONCE; fed to both paths.
AdmissionProgram: A bounded, canonical admission decision circuit. Constructing one proves the canonical-topological invariant (operands reference strictly-earlier nodes, arity matches the op); deeper acceptance — vocabulary closure, width/arity typing, structural limits, canonical re-encoding — is the independent validator’s contract (step 3).
AdmissionProgramHash: Canonical content hash of an crate::contract::admission::AdmissionProgram (H_A) — the digest of the bounded, validated admission circuit.
AdmissionShape: The shape of a full admission instance — how many requirements / budget dimensions and the per-aspect lane widths the compiled circuit reads.
AdmittedBudget: One dimension’s ADMITTED contract.
AdmittedBudgets: The complete admitted budget B_A bound into a BoundaryPlan.
AdmittedRequirement: One admitted requirement with its verdict and the ACTUAL mechanism chosen.
ArtifactFix: An interrupted disposition the host must finish idempotently before the boundary is settled (re-promote / re-discard the artifact, then record the Applied phase).
ArtifactId: Lifecycle identity of one artifact OCCURRENCE.
ArtifactReality: What the host INDEPENDENTLY observes about one artifact’s bytes on open().
AttemptId: Opaque identity of ONE attempt to run a plan.
BackendId: Stable identity of a backend FAMILY ("inert", "linux", "wasm", …).
BackendProfile: TYPED planning view, derived DETERMINISTICALLY from a raw snapshot. The planner consults THIS, never the map.
BackendProfileHash: Canonical hash of a crate::BackendProfileSnapshot.
BackendProfileSnapshot: RAW probe facts — portable, string-ish, persisted in the plan + report for AUDIT/REPLAY ONLY. NEVER consulted directly at admission.
BackendRegistry: Holds the registered backends, keyed by BackendId.
Boundary: A boundary in lifecycle state S. NOT Clone/Copy: transitions move self, so a consumed state cannot be reused (a retry mints a new attempt).
BoundaryDispositionEvent: 0xE/0x004 — a post-report artifact disposition decision/result, appended by the host.
BoundaryPlan: Admitted authority + controls. INERT typed data — not bytecode/executable. Bound to ONE backend AND the machine profile it was admitted against.
BoundaryPlanHash: Canonical content hash of a crate::BoundaryPlan (its plan_id).
BoundaryPlanner: Admits a BoundarySpec against a chosen backend, FAIL-CLOSED.
BoundaryRecoveryEvent: 0xE/0x003 — a typed, replayable startup-reconciliation verdict.
BoundaryReport: SEALED = canonicalized + body_hash. NOT persisted; the host appends it (0xE).
BoundaryReportBody: OBSERVED facts, unsealed. Returned by crate::Backend::execute.
BoundaryReportEvent: 0xE/0x002 — a sealed BoundaryReport, appended by the host.
BoundaryReportHash: Canonical body_hash over a crate::BoundaryReportBody.
BoundaryRun: A driven boundary run: pumped one RunStep at a time.
BoundaryRunner: Executes a plan via its bound backend, then SEALS the observed body.
BoundarySpec: The caller’s request: authority + controls + workload + budgets + evidence.
BoundaryStartedEvent: 0xE/0x001 — a sealed BoundaryPlan, durably appended by the host AT RUN-START (gated to Durable before the backend executes).
BudgetAvailability: One dimension’s PROFILE: P_d = (available, actual-guarantee, available-evidence, mechanism). Probed and declared by the backend.
BudgetInputs: One budget dimension’s full admission inputs (the per-dimension B slice): the request (limit, derived-minimum, guarantee, evidence) vs the backend’s availability (available, guarantee, evidence). The membrane passes the dimension iff D ≤ L ∧ L ≤ A ∧ G_req ≤ G_avail ∧ E_req ⊆ E_avail (the two-phase admission of crate::contract::budget, flattened to a single pass bit here — the per-dimension reason selector is a later step).
BudgetProfile: The complete profile B_P — seven dimensions of host capability.
BudgetRefusal: A budget refusal: the first failing dimension and its reason.
BudgetRequest: One dimension’s REQUEST: R_d = (limit, min-guarantee, required-evidence).
BudgetRequirements: The complete request B_R — seven branded, fixed-unit dimensions. ProcessCount and HandleCount carry u32-valued counts in their limit; the rest carry the u64 unit named on the field.
BudgetWitness: One dimension’s execution witness: W_d = (L, G, E, M, O, R, F).
BudgetWitnesses: The seven execution witnesses the report carries — one per fixed budget dimension, in canonical order, with FIXED observed-usage semantics (per field).
CanonicalPolicy: The canonical normal form of one capability POLICY: a family tag, a variant discriminant, and the normalized (sorted + deduplicated) payload. Two values are == iff the policies they were normalized from are SEMANTICALLY IDENTICAL (modulo syntactic list ordering). The wrapped bytes ARE the canonical form; equality is byte equality, so the §2 law reduces to a byte comparison.
CaptureRefs: References to captured standard streams (not the bytes themselves).
CertNode: One node’s entry in a ProgramCertificate.
CircuitBuilder: Builds an AdmissionProgram by appending nodes in canonical order. Every constructor returns the NodeId of the node just appended; because nodes are only ever appended, operands always reference strictly-earlier nodes — the canonical-topological invariant holds by construction.
ContentHash: blake3 content hash of an artifact’s bytes — its BYTE identity.
Decision: The decision E produces: the admission bit, the first-failed-membrane refusal code (meaningful when admit is false), and the per-membrane pass/fail bits.
DeniedAttempt: An attempt the boundary blocked.
DerivedMinimums: The cross-dimensional derived structural minimums DerivedMinimum_d(S,L) — the floor each dimension’s limit must meet (e.g. a native launch ⇒ process ≥ 1).
DispositionState: The folded disposition state of one artifact (from its 0x004 phases).
EnvEntry: One admitted environment binding: a variable name and where its value comes from (EnvSource). The value is NEVER ambient — it is a literal or a lease ref.
EvidenceRequirements: What evidence the caller requires the report to carry. Minimal in C0.
EvidenceSet: A set of EvidenceClaims — the evidence a backend can produce (the “available” set) or a caller requires (the “required” set).
InertBackend: The honest no-confinement reference backend.
InputDecl: A declared input lane.
InputSlot: Index of a declared input lane, referenced by NodeOp::Input.
Lane: A value lane: a sequence of bits, least-significant bit first. Its length is the lane’s bit width.
LookupTable: A frozen lookup table for NodeOp::BoundedLookup: the index operand selects one entry. Bounded — entries.len() and each entry’s length are structurally limited.
LoweringSchedule: A validated, ordered, canonical schedule of primitives to lower.
MapSecretResolver: An explicit in-memory SecretResolver for tests + simple host wiring: a fixed ref-id → value table. An unknown ref fails closed with SecretResolveError::Unknown. NOT a production secret store (it holds values in process memory); it exercises the JIT-resolve + fail-closed contract.
MechanismDigest: A blake3 digest of a backend’s MECHANISM string for a requirement key (§1’s H_M). The coupling law binds a production Enforced claim to a Proven ledger row ONLY when the row’s digest matches the digest of the mechanism the backend would actually use — so a backend cannot satisfy the gate by swapping in a different (unproven) mechanism under the same key.
NetDest: A single allow-listed network destination (host + port), inert evidence.
Node: One circuit node: an op, its operand edges, and its declared output width.
NodeId: Index of a node within an AdmissionProgram’s canonical node array.
ObservedFact: A fact the backend OBSERVED about what actually happened.
Outputs: The program’s declared outputs (plan §2): the admission bit, a refusal-code lane (the first-failed membrane index), and one pass/fail bit per membrane.
PathSet: A declared set of filesystem roots a Capability::Filesystem is scoped to.
Planned: An admitted, machine-bound plan. The next legal move is Boundary::start.
PlannerInputs: The normalized inputs for the current planner contract — produced by a single probe/classify pass and fed byte-for-byte to both the imperative reference and the shadow circuit.
PrimitiveDeclInputs: One declared primitive in the membrane’s bounded universe (its position in ScheduleInputs::declarations is its index p ∈ 0..N). This is the TRUSTED declaration the schedule is checked against — the planner authenticated it, and a slot’s claimed digest must reproduce decl_digest / param_digest exactly.
PrimitiveId: Stable identity of a ConfinePrimitive within a backend’s primitive set.
PrimitiveVersion: A primitive declaration’s revision, paired with PrimitiveId to bind a schedule entry to the EXACT declaration it was compiled from.
Privilege: A privilege a primitive requires in order to lower.
ProfileFacts: The concrete, TYPED machine facts a ProfileFloor is checked against — the probe truths a backend derives once at construction (the live landlock ABI, and whether the kernel exposes atomic cgroup.kill / the pids.peak witness).
ProfileFloor: The MINIMUM machine facts a qualification covers (§3 PROFILE-CLASS): the floor predicate a production profile must DOMINATE (p_prod ⊒ floor) for a Proven receipt earned at the floor to transfer to it.
ProgramCertificate: The frozen proof certificate the compiler C emits and the independent validator re-checks (plan §3): the canonical per-node levels/widths/edges, the counts, the total bit-depth, and the digest. The validator recomputes every field rather than trusting it.
ProgramLimits: The structural bounds: a widest-lane cap, a polynomial node bound, and a logarithmic depth bound.
ProofReceipt: Archived evidence that the QF_BV qualification gate ran and PASSED for a specific circuit (identified by the canonical SMT input digest). Retained as gate evidence; a release that treats the circuit as authority must carry a receipt whose smt_digest matches the current circuit and whose verdicts are all correct.
QualificationRow: One committed row of the qualification LEDGER (§1 Qualification(p,k) joined to its profile-class + mechanism digest + proof receipt). The ledger is the REPOSITORY’s independent record; a backend never authors it.
QuarantineRecord: One orphan (proc / fd / dir) swept during a RolledBack reconciliation.
RecoveryProbe: INDEPENDENTLY observed host reality at open() — NOT a backend self-report.
Reported: A reported attempt: the sealed terminal evidence is in hand. The next legal move is Boundary::into_report_event (the host persists 0x002).
RequirementInputs: One requirement’s admission inputs (the per-requirement slice of V/Q).
RunView: A PURE projection of one attempt, folded from its durable 0xE events.
ScaffoldingBackend: A scaffolding backend: honest family support, empty machine ceiling.
ScheduleEntry: One entry of a canonical LoweringSchedule.
ScheduleInputs: The normalized, immutable schedule-membrane inputs — the trusted declaration universe D, the supplied order L, and the spec’s required coverage R(S). Probed and normalized ONCE; fed identically to the imperative reference and (next) the shadow circuit.
ScheduleShape: The fixed shape + derived lane widths a compiled schedule circuit reads.
ScheduleSlotInputs: One slot of the supplied schedule L: which declared primitive it places, plus the digests it CLAIMS for that slot (authenticated against the trusted declaration).
SeccompEvidence: The D6 evidence binding for ONE compiled launcher seccomp filter.
SecretRef: An OPAQUE, typed reference to a leased secret. NEVER carries a value — only an identifier a crate::SecretResolver dereferences in the parent at launch time. Serializing this (in a plan or report) leaks only the ref string, never a secret.
Spec: A proposed boundary, not yet admitted. Carries the request and the chosen backend; the next legal move is Boundary::plan.
StagedArtifact: A record of an artifact the boundary STAGED (produced + quarantined).
Started: A started attempt (one AttemptId). The next legal move is Boundary::into_reported once the runner seals a BoundaryReport.
StdStreams: Which standard streams the host captures around the boundary.
SupportMatrix: What a backend FAMILY can THEORETICALLY do. Static, per-backend-kind, TYPED.
SupportVerdict: The full support answer for one requirement: a PRODUCT of the two orthogonal axes — Enforcement (how strongly held) and EvidenceSet (what can be witnessed). The matrix grades both; planning floors both via Self::meet.
TranslatedCircuit: A circuit translated to SMT-LIB2: the input declarations + node definitions, and the SMT name of the admit output (a 1-bit lane).
Width: The bit width of a value lane. A node’s declared output width; also the width of an input lane. Always 1 ..= MAX_WIDTH.

Enums§

AdmissionDivergence: A typed shadow disagreement — a hard gauntlet finding, never silently ignored.
AdmissionOutcome: The canonical admission decision both paths must agree on.
BoundaryFinding: A deterministic structural finding, sorted before the body is hashed.
BoundaryRequirement: The unit the matrix/profile classifies: a guest Capability OR a host-provisioned HostControl. One classify, one path through plan().
BudgetDimension: The fixed seven budget dimensions, in canonical order.
BudgetFailure: Why one budget dimension was refused. The canonical reason ORDER is fixed (and must match the circuit + shadow + JSON projection + solver model): the intrinsic derived-minimum check comes FIRST (the request is internally incoherent, independent of any backend), THEN backend adjudication — capacity, then guarantee, then evidence — so the first-failing reason is deterministic.
BudgetFinding: The terminal budget finding for a dimension (F_d).
Capability: Guest-invokable admitted authority policy (grants AND restrictions).
CommitDurability: GUARANTEE: how durable a committed artifact is.
CompareRel: A fixed-width unsigned comparison relation carried by NodeOp::Compare.
DispositionAction: What the host decided to do with a produced (staged) artifact.
DispositionPhase: The lifecycle phase a BoundaryDispositionEvent records for one artifact.
Enforcement: The enforcement-strength axis of a support verdict.
EnvLowerError: Why an EnvPolicy::Exact could not be LOWERED to a concrete envp: either the table is contract-invalid (EnvPolicyError) or a lease failed to resolve (SecretResolveError). Both fail the launch closed — the target never runs.
EnvPolicy: Environment-variable policy (proof-spine §5 D2 — Environment::Exact).
EnvPolicyError: Why an EnvPolicy::Exact table is contract-invalid. The contract fails CLOSED on the FIRST violation (admission refuses before any execution). Every variant names a malformed class the §4 oracle’s fail-closed branch plants.
EnvSource: Where an EnvEntry’s value comes from. A Literal carries the value inline (durable); a SecretLease carries only an opaque REF — the value is resolved in the parent immediately before launch and NEVER persisted (proof-spine §5 D2 + §8 Vault-style JIT secrets).
EvalError: Why a program could not be evaluated over a given input vector. Every variant is a fail-closed typed refusal; E never panics.
EvidenceClaim: One kind of evidence a backend can produce for a requirement.
ExitStatus: Process exit status, portably encoded (no OS ExitStatus type).
FdPolicy: Host-fd inheritance policy: none by default, explicit fds only.
FsAccess: Filesystem access grant.
FsConfinement: GUARANTEE: “reads/writes confined to the declared scope” — not a mechanism.
GuaranteeProfile: The quantitative enforcement semantics actually supplied for a dimension (E_d). “Enforced” without overshoot numbers is too vague for timers, sampled memory, CPU accounting, and network mediation — so a mediated guarantee carries them.
HostControl: Host-provisioned lifecycle controls applied around the boundary.
KillGuarantee: GUARANTEE: how complete a kill is.
KillTarget: GUARANTEE: what a kill targets.
LifecycleError: Why a lifecycle transition refused. Distinct from PlanError (admission) and crate::RecoveryClassification (reconciliation): this is the typestate validating a semantic relation the substrate cannot prove on its own.
LimitViolation: Why a program exceeds the structural limits.
LoweringError: Why a set of primitives could not be compiled into a LoweringSchedule. The compiler fails closed: any inconsistency aborts rather than emitting a partial or out-of-order schedule.
LoweringPhase: The ordered setup phase a primitive lowers in.
MinGuarantee: The minimum acceptable guarantee a requirement may demand. A caller may demand Mediated or Enforced — never Unsupported (that is only a backend answer).
NetPolicy: GUARANTEE: deny vs scoped-allow (a policy, not a mechanism).
NodeOp: The FROZEN, CLOSED node vocabulary. This is the entire instruction set an AdmissionProgram may use; the validator rejects anything else. Adding an op is a schema bump (see ADMISSION_PROGRAM_SCHEMA_VERSION) — deliberately NOT #[non_exhaustive], because “frozen” and “open for extension” contradict.
Outcome: Run-time terminal outcome. DISTINCT from crate::RecoveryClassification, which is a startup-reconciliation verdict.
PathView: GUARANTEE: a path view private to this boundary (not a mechanism).
PlanError: Why a boundary could not be planned. The planner fails closed: any unsupported REQUIRED requirement aborts admission rather than degrading.
ProgramError: Why a node array could not form a well-formed canonical AdmissionProgram. Constructor-level structural faults only; full vocabulary/width/limit validation is the step-3 validator’s job.
ProofGateError: Why a proof receipt does NOT qualify the circuit as authority.
ProofStatus: Whether the compiled admission circuit has passed its full-width equivalence proof and may be treated as authoritative, or is still a candidate behind the authoritative imperative reference.
QfBvError: Why an admission circuit could not be translated to SMT-LIB2.
QualificationStatus: What the repository has INDEPENDENTLY qualified about a capability claim. Distinct from Enforcement (the runtime claim a backend makes).
RecoveryAction: The PURE decision reconcile reaches for one in-flight attempt. The host APPLIES it (sweep / finish / refuse), then appends the 0x003 verdict from RecoveryAction::classification.
RecoveryClassification: A reconciliation verdict for one in-flight boundary on open().
RequirementKind: The classification key: a requirement’s CANONICAL POLICY identity (proof-spine §2), one key per semantically-distinct policy.
RunStep: One discrete step of a driven boundary run.
ScheduleDivergence: A typed schedule-membrane shadow disagreement — a hard gauntlet finding.
ScheduleOutcome: The canonical schedule-membrane decision the imperative reference and the shadow circuit must agree on.
ScheduleRefusal: Why the schedule membrane refused, in canonical priority order. The numeric ScheduleRefusal::code is the stable selector the circuit and shadow trace agree on (0 = admitted).
SeccompActionKind: One seccomp ACTION a policy may resolve to (proof-spine §5 D6: the “kernel-supported action profile”). A stable, assembler-independent mirror of the actions our policy model uses, so the evidence records WHAT the kernel must honor without leaking seccompiler’s type into the pure contract. Errno carries the returned errno so two policies that deny via different errnos stay distinct.
SeccompArch: The LITTLE-ENDIAN architectures a launcher seccomp filter targets (proof-spine §5 D6: “seccompiler supports LE x86_64/aarch64/riscv64”). The BPF arch-audit preamble is arch-specific, so the same policy compiles to DIFFERENT bytes per arch — the digest binds the exact target.
SeccompObservedMode: The kernel-observed seccomp mode of a confined child, read at S10 install time from /proc/<pid>/status (Seccomp: / Seccomp_filters:). Defined here so the evidence type is complete now; S7 never constructs one (the field stays None).
SecretResolveError: Why a SecretRef could not be resolved to a value. Carried back so the backend fails closed (refuses the launch) rather than running with a missing secret.
SpawnPolicy: The admitted CHILD-TASK policy — what new tasks (threads / processes) the confined workload may itself create. The three variants are FROZEN SEMANTICS (proof-spine §2/§6/S6): they are an object-capability ATTENUATION ladder (§8 seL4/Capsicum), strictest first. The VARIANT is the policy (no payload).
ValidationError: Why a program failed validation. The validator fails closed on the FIRST fault; each variant names a malformed class its red fixtures prove it catches.
Workload: What the boundary runs. Wasm is always present in the type; a real wasm backend is gated later, but the contract stays uniform.

Constants§

ADMISSION_CIRCUIT_PROOF: The admission circuit’s source-declared proof status. It STAYS PromotionCandidate: promoting the circuit to authority (binding H_A) requires the QF_BV qualification gate, and a release that treats the circuit as authority is blocked until a valid ProofReceipt covering the current circuit exists. The dual path stays fail-closed meanwhile — the imperative reference decides.
ADMISSION_PROGRAM_SCHEMA_VERSION: Wire schema version of the frozen IR. The vocabulary, encoding, limits, depth model, and certificate shape are FROZEN at this version; any change to them is a schema bump, not an in-place edit.
BOUNDARY_PLAN_SCHEMA_VERSION: Schema version for BoundaryPlan bodies.
BOUNDARY_REPORT_SCHEMA_VERSION: Schema version for BoundaryReportBody bodies.
FROZEN_LIMITS: The frozen limit constants. Provisional values, pinned until a schema bump: generous enough for a 12-membrane admission circuit over capped requirement / evidence / budget inputs, while keeping |V| polynomial and D(A) = O(log W).
LINUX_QUALIFICATION_LEDGER: The COMMITTED Linux qualification ledger (S1): the CURRENTLY-PROVEN cells, each citing its real passing oracle(s), plus the explicitly-stated non-proven cells.
MAX_ENV_ENTRIES: The maximum number of entries an EnvPolicy::Exact table may declare. A defensible cap (kernel ARG_MAX admits far more, but a confined workload that genuinely needs hundreds of explicit env vars is pathological — the cap bounds the admitted table and the canonical-key payload). 256 covers every realistic declared environment with headroom.
MAX_ENV_TOTAL_BYTES: The maximum total byte budget of an EnvPolicy::Exact table, summed over every name and every inline Literal value (a SecretLease ref counts its ref bytes, not a resolved value — the value is unknown at admission). 128 KiB is a defensible fraction of a typical 2 MiB ARG_MAX/env budget, leaving ample room for argv.
MAX_LOOKUP_ENTRIES: The frozen upper bound on a LookupTable’s entry count — keeps a bounded lookup actually bounded regardless of key width.
MAX_PRIMITIVES: The bounded universe size the u64 bitset encoding supports. A lowering schedule names a handful of primitives; this ceiling is far above any real plan and exists only so the index → bit mapping is total without a wider word.
MAX_WIDTH: The widest single lane the frozen limits admit. Sized to cover a 64-bit budget word and a 64-element capability/evidence bitset with headroom; the 7-dimension budget vector is seven separate lanes, never one wide lane.
WASM_QUALIFICATION_LEDGER: The committed Wasm qualification ledger. Every production Enforced Wasm ceiling cell has a Proven row backed by the live grid oracle; structurally unsupported native cells are stated explicitly and stay absent from the ceiling.

Traits§

Backend: A platform boundary backend. OBSERVES only; never seals or writes BatPak.
BoundaryState: Sealed marker bound for the Boundary typestate parameter.
PrimitiveDecl: One composable confinement mechanism. The planning + evidence surface; see the module-level layering note for why lower/rollback arrive with the executor.
SecretResolver: Resolves an opaque SecretRef to its concrete value, JIT, in the parent. A resolver is the host hook the backend calls immediately before launch; the returned value is written ONLY into the child’s envp and never persisted.

Functions§

adjudicate_dimension: Adjudicate ONE dimension’s coherent request against the backend’s available capacity, FAIL-CLOSED in canonical reason order (capacity → guarantee → evidence). The intrinsic derived-minimum check (L_d ≥ D_d) is a SEPARATE, EARLIER phase in budget_admit; a dimension reaching here has already passed it, so this never returns BudgetFailure::BelowDerivedMinimum.
budget_admit: Admit all seven dimensions in two phases, returning the admitted contract or the FIRST failing dimension + reason in canonical order.
budget_membrane_equivalence_smt: Emit the full SMT-LIB2 script proving the compiled budget membrane equivalent to the imperative reference over the WHOLE input space, plus non-vacuity. The three (check-sat) results a conforming solver must return, in order, are: unsat (equivalence), sat (admit reachable), sat (refusal reachable).
budget_planted_disagreement_smt: Emit the PLANTED-DISAGREEMENT script: the same compiled circuit against a reference with a deliberately weakened dimension-0 capacity check (< not ≤). A conforming solver MUST return sat — a model where they differ. This is the negative control: it proves the equivalence query can DETECT a real disagreement, so the genuine unsat is not vacuously true over an always-equal encoding.
classify_via_primitives: Classify a requirement against a set of primitives, FAIL-CLOSED.
compile_admission: Compile the FULL admission circuit: the six membranes composed in the fixed canonical order with the ordered priority-encoder refusal (kernel plan §6 + the lowering-schedule membrane of track A).
compile_budget_detail: Compile the budget DETAIL selector circuit: its refusal_code is the packed (first-failing dimension, that dimension's first-failing reason) — 0 if every dimension passes. Reads the same 7·dims budget lanes as compile_budget_membrane. A bounded priority encoder: within a dimension the reasons are ordered (intrinsic highest), and across dimensions the lowest index wins — matching the imperative reference’s first-failure semantics exactly.
compile_budget_membrane: Compile the budget membrane: admit iff every dimension passes the two-phase check D_d ≤ L_d ∧ L_d ≤ A_d ∧ G_d ≤ E_d ∧ Q_d ⊆ C_d. Reads 7·dims input lanes in canonical order: limit, available, derived-min (each budget_width), guarantee-required, guarantee-available (each 2-bit), evidence-required, evidence-available (each evidence_width).
compile_conflict_membrane: Compile the conflict-freedom membrane: admit iff no present set intersects its forbidden set. Reads 2·reqs bitset lanes of width.
compile_evidence_membrane: Compile the evidence membrane: admit iff each requirement’s required evidence ⊆ the backend’s available evidence. Reads 2·reqs bitset lanes of evidence_width.
compile_profile_drift_membrane: Compile the profile-drift membrane: admit iff the planned profile hash equals the live re-probed one — fails closed if the machine changed.
compile_schedule: Compile selected primitives into a canonical, validated LoweringSchedule — the deterministic backend-side compiler K:(S,P,D)→L, FAIL-CLOSED.
compile_schedule_membrane: Compile the standalone schedule membrane: admit iff the supplied schedule passes all nine checks; the refusal code is the first-failing check’s ScheduleRefusal::code. This is the circuit the shadow evaluates for the per-schedule reason detail.
compile_support_membrane: Compile the support membrane: admit iff every requirement’s enforcement is at least Mediated (2-bit codes 0 Unsupported, 1 Mediated, 2 Enforced).
compose_membranes: Compose ordered membrane bits into (admit, refusal_code): admit is their conjunction (a balanced AND tree); refusal_code is the 1-based index of the FIRST failing membrane (0 when all pass) — a bounded priority encoder built right-to-left so an earlier failure overrides a later one.
decode_validated: The untrusted-bytes wall: decode a program, validate it, and require the bytes to be its canonical encoding (so a valid-but-non-canonical encoding is rejected).
derive_minimums: Compute the cross-dimensional derived structural minimums DerivedMinimum_d(S) — the floor each budget dimension’s requested limit must meet, from what the spec structurally implies (kernel plan §7). The values are SYMBOLIC structural floors (a nonzero 1, the 3 standard descriptors), not precise resource sizing: they encode coherence, e.g. a launched workload needs ≥1 process and nonzero time/cpu/memory; requested network access cannot be 0 bytes.
enforced_claim_is_qualified: The coupling-law check at a single (key, profile, claim) point: a runtime Enforcement claim is admissible against a qualification only when either the claim is not Enforced, or the qualification is Proven. (The full gate also matches the profile floor and mechanism digest — those live in the ledger + the integrity gate; this is the pointwise core, kept here so it is unit-testable and shared by the runtime if it ever consults a qualification.)
evaluate: Evaluate program over the input vector inputs (indexed by input slot).
linux_ledger_row: Look up the committed Linux ledger row for a requirement key (the lookup the coupling gate uses). None ⇒ the key is not in the ledger at all (which, for an Enforced production cell, is itself a coupling violation).
linux_mechanism: Derive the MechanismDigest for a Linux mechanism string built the way backend_impl::mechanism builds it: "{id}:{primitive}:{enforcement:?}". The ledger is committed const, but a digest is a runtime blake3, so the ledger stores the SOURCE mechanism string and the coupling test re-derives the digest; this helper keeps the two spellings (ledger vs. backend) in one place.
lower_env: LOWER an admitted EnvPolicy::Exact to the concrete name → value envp the launcher serves to fexecve (proof-spine §5 D2 lowering). Re-validates the table (defense in depth — admission already validated it, but lowering is the last gate before the value materializes), then resolves every EnvSource::SecretLease in the PARENT via resolver. Entry ORDER is preserved (the table is already a validated function name → value); the result is exactly the child’s environment, nothing inherited.
planner_reference: The authoritative imperative decision for the current planner contract.
planner_shadow_check: Run both paths over the same normalized planner inputs and return the authoritative outcome, or a typed AdmissionDivergence on disagreement.
reconcile: Reconcile one in-flight attempt: PURE decision over what the events SAY (RunView) vs what the world IS (RecoveryProbe). Walks the §13 crash windows in order of severity, fail-closed.
reference_admission: The authoritative imperative admission decision over normalized inputs.
reference_schedule_admission: The authoritative imperative schedule decision over normalized inputs: the first-failing check in canonical priority order, or ScheduleOutcome::Admitted. Total and fail-closed — never panics on adversarial input.
run_confined: Plan spec against backend, execute it, and return the sealed BoundaryReport — the one-call form of the registry → plan → run pipeline.
schedule_refusal: The first-failing ScheduleRefusal in canonical priority order, or None when the schedule is admitted. Factored so the circuit-equivalence proof can drive the reference directly. The structural checks (1)–(2) run first and build the verified present/pos view; the order-sensitive checks (3)–(9) are then one short-circuit chain over that view (each is its own bounded predicate).
schedule_shadow_check: Run both paths over the identical normalized inputs and return the authoritative outcome — or a typed ScheduleDivergence if the shadow circuit disagrees.
shadow_check: Run both paths over the identical normalized inputs and return the authoritative outcome — or a typed AdmissionDivergence if the shadow circuit disagrees.
shape_of: Derive the lossless ScheduleShape for inputs: every lane is wide enough to hold the largest value it carries, so circuit and reference agree on the exact u64 domain (no truncation modeling).
smt_digest: The canonical digest of an SMT input — the circuit’s proof identity. A receipt must carry this exact digest (over the genuine equivalence script) to qualify the circuit.
translate: Translate a validated AdmissionProgram into SMT-LIB2 declarations + node definitions. Every input lane becomes a free BitVec; every node becomes a define-fun over earlier nodes; the admit output is named for assertion.
validate: Validate a program against the structural limits, FAIL-CLOSED on the first fault, returning the independently re-derived ProgramCertificate on success.
verify_certificate: Verify a claimed certificate by independently re-deriving it.
verify_receipt: Verify a receipt qualifies the circuit identified by expected_digest as authority: matching digest, primary [unsat, sat, sat], independent unsat, planted sat. Any failure leaves the circuit a ProofStatus::PromotionCandidate.
wasm_ledger_row: Look up the committed Wasm ledger row for a requirement key.
wasm_mechanism: Derive the MechanismDigest source string for a Wasm mechanism.

Type Aliases§

Digest32: 32-byte blake3 digest, matching BatPak’s evidence-report identity width.

Crate bvisor

Crate bvisor Copy item path

Modules§

Structs§

Enums§

Constants§

Traits§

Functions§

Type Aliases§

Crate bvisor