-
Notifications
You must be signed in to change notification settings - Fork 0
Development and Operations
BHCP is a Rust-only repository-owned implementation. Rust 1.97.1 is pinned in .mise.toml and in the crate manifest. Runtime dependencies are pinned Rust crates: cddl for RFC 8610 parsing/validation support and RustCrypto sha3 for SHA3-512. The repository has no project-owned Ruby, Python, Node.js, or C toolchain.
Install the pinned toolchain:
mise installRun the same four checks before delivery:
cargo fmt --check
cargo clippy --all-targets -- -D warnings
cargo test --all-targets
cargo build --releaseThe 17-root CDDL fixture gate is part of the Rust test suite and can be run directly with:
cargo test --test schema_fixturesUse cargo run --bin generate-fixtures only when intentionally regenerating checked-in AST/IR fixtures, then review deterministic byte changes.
cargo run -- parse conformance/v0/fixtures/canonical-simple.bhcp > /tmp/canonical-simple.ast.cbor
cargo run -- lower conformance/v0/fixtures/canonical-simple.bhcp > /tmp/canonical-simple.ir.cbor
cargo run -- inspect conformance/v0/fixtures/canonical-simple.bhcp
cargo run -- inspect /tmp/canonical-simple.ir.cbor
cargo run -- hash conformance/v0/fixtures/canonical-simple.bhcp
cargo run -- policy inspect conformance/v0/fixtures/canonical-policy.bhcp
cargo run -- policy compose conformance/v0/fixtures/canonical-policy.bhcp > /tmp/effective-policy.cbor
cargo run -- policy inspect /tmp/effective-policy.cbor
cargo run -- verify <contract.bhcp> <goal-symbol> <candidate.cbor> <subject-file> <produced-at>parse and lower emit CBOR, inspect emits a human-readable outline, and hash emits the algorithm-tagged semantic ID. JSON is not a BHCP repository artifact format.
policy compose consumes explicitly ordered canonical source or source-policy CBOR
inputs and emits deterministic validated effective-policy CBOR only after every
input, layer transition, feature, and monotonicity check succeeds. policy inspect
renders source values or effective layers, rule values, waiver governance,
semantic/artifact identities, and exact source-rule provenance. It never uses JSON
as an intermediate artifact format.
-
Implemented and measured: the
Rust qualityGitHub Actions workflow runs formatting, warnings-as-errors Clippy, a release build, and the exact 17-root CDDL fixture invariant independently. A plan validator requires every root integration target exactly once plus library/binary coverage; six concurrent partitions feed the stable fail-closedRust quality / Testsaggregate. Test-only SHA3/Keccak optimization leaves release semantics unchanged. #97 reduced exact-head protected feedback from 38:01 to about 5:06 (86.6%, 7.5× faster). PR #142 retained the 64 MiB adapter executable ceiling while removing platform debug payloads from test binaries; its complete hosted matrix finished in about three minutes and the formerly failing adapter shards completed in 52–83 seconds. Actions are commit-pinned and Cargo dependency caches are keyed by.mise.tomlandCargo.lock. -
Required on
main: strict branch protection, including for administrators, requiresRust quality / Format,Rust quality / Clippy,Rust quality / Tests,Rust quality / Release build, andRust quality / 17-root CDDL fixtures; force pushes and deletion are disabled and review conversations must be resolved. -
Implemented: the goal-algebra conformance harness regenerates and root-validates exact AST/IR bytes for
all,any,none,chain, andgate; resolves named empty/adversarial and generic proof-check evidence; pins the six generator inputs and 17 schema roots; and derives feature-manifest coverage from the exact identifiers emitted by the implemented obligation and capability graph builders while keeping state/execution/planning/runtime features unclaimed. -
Implemented: the repository-local
AGENTS.mdoperating contract and project-loop profile define authority, issue selection, atomic remote-ref claims, TDD, protected review/merge, fenced release, and completion reconciliation. -
Implemented: the safe-Rust
bhcp::experimentcontroller freezes model/reasoning/sandbox/toolchain pins, exact executables, inputs, run order, limits, and canonical tree identities before launch. It exclusively owns scratch/target trees, clears process environments, enforces combined output/time ceilings and process-group cleanup, withholds oracles until agent completion, gives every judge an ephemeral isolated view, and emits bounded Markdown evidence rather than repository JSON event logs. The focused controller suite includes adversarial tree framing, symlink escape, hiddentargetcontent, output flooding, orphaned descendants, ambient judge variables, judge mutation, and both oracle-order cases. -
Implemented:
bhcp verifydiscovers the nearestbhcp-project.toml, compiles and validates the exact contract/candidate boundary, rejects unregistered or contract-extraneous bindings, dispatches only capability-bounded adapters, binds the exact supplied subject reference and bytes, and emits deterministic evidence with distinct accepted, rejected, unresolved, and faulted results. -
Implemented:
bhcp::proofindependently revalidates complete obligation closures against sealed child observations and evidence, including exact execution-instance binding for claims, items, gaps, expression contexts, and reducer premises. Its protected integration suite covers four-state outcomes, behavior-neutralnone, zero/one/many discharges, repeated-goal substitution, registry and adapter authority, policy minima, and deterministic derivation identity. -
Audited:
cargo test --test phase_two_evidence_audithashes every recorded Phase 2 input, result, and executable evidence source, requires the named Rust test declaration, checks semantic identities, and enforces the exact experiment-to-issue/PR/squash-merge map. The linked replay suites remain the executable outcome evidence. -
Registered:
cargo test --test evidence_generalization_preregistrationchecks the closed future-study manifest, every Git-blob and semantic-ID pin, the four-task registered-use and three-task comparative populations, exact 36-session schedule, six/six order balance, analysis/non-claims, billing preflight, and enforceable resource boundary before any model turn. -
Measured and replayable:
cargo test --test evidence_generalization_positive_runnerchecks every preserved positive-use session and its 0/12 result.cargo test --test evidence_generalization_comparative_resultsrecomputes the 12 paired outcomes, 0/12 acceptance per arm, zero paired risk difference, exact McNemar p=1, and 12/12 calibrated claims per arm from the checked-in comparative record. - Implemented: squash-only auto-merge is matched to the reviewed head SHA, merged topic branches are deleted automatically, and PR bodies use issue-closing links. Disposable probe PR #56 proved that a mismatched expected head and author approval are rejected and that one failed required check keeps queued auto-merge blocked.
Remote CI and branch protection are now authoritative. A local green run remains the required fast feedback loop, but is not a substitute for the protected hosted checks or review.
- Unsupported canonical syntax must return a stable diagnostic; do not silently ignore it.
- Source files are scanned as raw bytes before lexing. Invalid UTF-8, CRLF or non-ASCII preamble whitespace, aliases, duplicate or misplaced directives, and a BOM outside byte zero fail as
BHCP0003without artifact output. Omission and an optional leading BOM selectbhcp/canonical@0; an exact custom profile that has no registered normalizer fails closed asBHCP0004. The scanner retains original byte offsets while treating a leading BOM as logical column 1. - Typed syntax/profile artifact failures use stable
BHCP9001diagnostics. Check unknown fields, malformed or self-referential parents, illegal type modes, invalid formatting records, duplicate local overlays, and mapping coordinates that are duplicated or not in category/canonical order. Mapping entries serialize in deterministic coordinate order, while valid policy overlays retain declared order. The generic 17-root validator deliberately maps these typed failures to its root-levelBHCP5002boundary. - Effective syntax registration fails as
BHCP9002before reading program tokens when inheritance is unresolved or a map has an unknown coordinate, non-NFC/invalid surface, ambiguous spelling, punctuation prefix, alias recursion, core rebinding, or capture of fixed operators and contextual words. The diagnostic names the selected profile, syntax, offendingcategory:canonical=>surfacemapping, stable mapping-list entry, and rule. An unregistered selected profile remainsBHCP0004; using a canonical spelling that the selected map replaced isBHCP0005at the actual program-source point with the same structured context. Unsupported parser callbacks, unrestricted macros, and semantic overrides fail typed artifact decoding asBHCP9001. Every failure is atomic: no artifact or stdout is emitted. Registered custom source lowers through the ordinary parser while diagnostics retain original byte, line, and column points; comments and string contents are never remapped. - Resolved profile topology failures use
BHCP9003: inspect missing or cyclic profile/syntax parents, unrelated child syntax, weakened child type modes, duplicate root-to-leaf overlays, and missing overlay policy parents. Successful inspection prints deterministic profile and syntax chains, overlay order, effective type mode, and effective-policy identity. Overlay weakening still uses the policy composer's category-specificBHCP8101–BHCP8107diagnostics. -
bhcp formataccepts canonical source directly or custom source plus explicit syntax/profile/source-policy CBOR registry artifacts. It retains comments, mapped Unicode spellings, an explicit preamble or BOM, wraps only between tokens, and honors the resolved indentation, width, and final-newline record. A reparse that changes the canonical token stream or AST shape fails atomically asBHCP9004; never redirect a failed invocation into a source replacement. - The checked-in
conformance/v0/profile-layoutmanifest indexes two syntax roots, two profile roots, a shared policy overlay, compact symbolic and spaced narrative sources, and their exact formatter snapshots. The harness validates deterministic syntax/profile/AST/IR CBOR roots, equal semantic IDs with different presentation artifacts, label/comment sensitivity only in artifact identity, a semantic policy-change control, and stable diagnostic code/message with layout-sensitive source points. - The Phase 4 completion audit contains exactly three acceptance claims for every issue #41–#49, binds each claim to a named checked-in test on the correct issue row, resolves every local evidence link, and pins the reviewed #41–#48 delivery ledger. It closes the bounded presentation milestone while retaining the incomplete-v0 and arbitrary executable syntax non-goals.
- Process-backed verifiers run only through the packaged
bhcp-adapter-sandboxhelper. macOS uses/usr/bin/sandbox-exec; Linux requires Landlock ABI 4 with full requested enforcement plus seccomp network denial. A missing helper or unavailable enforcement fails closed before the verifier starts (BHCP7001). - Adapter execution uses the registered project-relative executable and exact argv without a shell or
PATH, clears ambient environment, closes inherited file descriptors above stderr, and enforces declared project read/write scopes. Timeouts and cancellation remain unresolved outcomes; malformed output, nonzero exit, limit violations, and sandbox or launch failures remain operational faults rather than semantic verdicts. - Registered verifier executables must not be mutated concurrently. The runner revalidates stable executable identity through the final pre-launch boundary, but native launch still reopens the canonical path; deployment permissions must prevent replacement during that residual path-open window.
- For policy failures, use the category-specific
BHCP8101–BHCP8107code orBHCP8110for source topology. If a weakening message names the wrong earlier rule after several rules compose, inspect the governing contributor rather than provenance order. An invalid layer must return no effective policy; a partial result is always a composer bug. - If a policy identity mismatch appears, recompute semantic ID from
effectiveonly and artifact ID from the complete document with onlyartifact_idremoved. Source layers or provenance changing semantic ID is a projection bug; observable effective rules changing only artifact ID is also a bug. - If
policy composeemits bytes on a failing invocation, treat it as an atomicity bug. Wrong layer order must beBHCP8110; unsupported policy features or malformed policy forms must remainBHCP8001; category weakening keeps itsBHCP8101–BHCP8107diagnostic. Source and equivalent source-policy CBOR inputs must produce identical effective bytes. - Policy-aware elaboration fails before valid semantic IR with
BHCP8200for an invalid policy boundary,BHCP8201for a type-mode floor violation,BHCP8202for a prohibited effect,BHCP8203for missing or non-provable capability authority, andBHCP8204for an exact dimensioned limit above an applicable maximum. Check goal/effect scope applicability as well as the rule value; deny wins, and a scoped maximum can constrain a matching global goal limit. - If two policies with equal effective restrictions produce different program semantic IDs, inspect the IR policy projection: it must retain the effective semantic ID only. Artifact identity and serialized IR bytes may still differ because source layers, rule provenance, and policy artifact identity are audit material.
- Reducer failures in an unselected branch are still definition failures: the whole expression tree must validate before execution. An unknown call must remain a stable kernel diagnostic, and any primitive value or satisfied conclusion that disagrees with its declared type must be rejected before generic derivation verification.
- If
anychooses a different winner across equivalent source or observation arrival orders, inspect canonical child-tag ordering. Multiple sealed satisfactions must choose the lexicographically least normalized tag; explicit composition must pass the same winner type boundary as the convenience form. - If
noneemits an empty record, accepts a declared output field, or drops counter-evidence from a mixed unresolved result, inspect its inferred goal signature and sealed partial-evidence aggregation. Its output is canonicalUnit; satisfaction requires every child's counter-evidence. - If
chainrequests or accepts a later child before its predecessor is sealed satisfied, inspect both theobserved-outputedge and runtime readiness validation. A later-step refutation must retain prior satisfaction evidence as derivation premises; terminal counter-evidence alone does not prove causal reachability. - If
gateobserves a child while its condition is false, inspect theexcludedprimitive and sealed observation record: a closed gate must reject the execution claim. If two same-signature gates share a reducer despite different conditions, inspect the condition component of reducer specialization identity. Parent-to-child argument tampering must fail at the typedparent-fieldedge, and claimed derivation tampering must still fail through the generic checker. - Unknown hash algorithms fail before parsing; the project manifest is an agility boundary, not arbitrary dynamic loading.
- Missing verifier registrations remain unresolved evidence gaps; contract strings are never executed as shell commands.
- A policy evidence obligation runs only producers explicitly bound by its semantic symbol through the verifier registry. Missing mappings or registrations use
bhcp.reason/policy-verifier-unregistered@0; too few accepted policy-class items usebhcp.reason/policy-evidence-minimum@0. Check the inspected structural target, accepted classes, minimum, and layer/policy/rule provenance. Reordering registrations must not change bytes, and removing the retained effective policy must fail closed before dispatch. - When schema tests fail, compare Rust model encoding, CDDL, examples, and SEMANTICS in the same change.
- Preserve unrelated worktree changes and never regenerate fixtures incidentally.