-
Notifications
You must be signed in to change notification settings - Fork 0
Decisions and Interesting Bits
This page summarizes durable decisions and measured findings. SEMANTICS remains normative; experiment reports remain the evidence source.
Decided and implemented. The compiler, deterministic CBOR codec, CLI, schema harness, kernel, verification foundation, and tests are safe Rust. Ruby schema tooling and mixed-format event artifacts were removed. CDDL remains the artifact contract and is parsed through the pinned Rust cddl crate.
Decided and implemented for the current slice. Canonical artifacts use deterministic CBOR and validate against the v0 CDDL bundle. Human inspection is a Rust-rendered view; checked-in experiment reports are Markdown. JSON is not a competing BHCP exchange format.
Decided and implemented. bhcp.hash/sha3-512@0 is the default and only registered algorithm. The project manifest is an agility point for future registered algorithms, not a license for untrusted dynamic hash plugins.
Decided, implemented, and audited: evaluator plus all, any, none, chain, and gate. The runtime knows generic sealed observations, checked construction, child tags, typed data edges, and derivation sealing. #15 provides the closed total-pure evaluator. #16 adds stable homogeneous any; #17 adds genuine-Unit none; #18 adds causal chain; and #19 adds unary typed gate. Chain edges are ordinary typed child arguments reading an earlier sealed output, while gate child inputs use typed parent-field edges; neither is scheduler metadata. Review tightened four proof boundaries: premature later-child observations are rejected, a later chain refutation retains the predecessor satisfaction premises that made it reachable, chain derivation tampering is checked through generic re-evaluation, and gate-specific derivation tampering is checked through the generic verifier. A closed gate rejects an observation instead of treating it as an invisible execution claim. No behavior kind or guard field was added. #20 publishes the complete five-form source/artifact/feature/proof conformance inventory.
Normatively decided and executable through composition and identity. Organization, team, repository, and user layers are checked in that order and combine as a restriction lattice rather than an override stack. Requirements, evidence demands, and prohibitions accumulate; capability scopes intersect; exact limits take the minimum applicable maximum; and type mode strengthens from dynamic through strict. Deny wins. Source rules use (policy-symbol, local-rule-id) identity, non-waivable restrictions remain absolute, and only exact authorized waivers may weaken a source rule.
Source and effective policy documents remain alternatives under the existing policy root. Effective semantic identity commits to normalized restrictions and governance constraints; content-addressed source layers, canonical rule provenance, waiver audit material, and authoring decomposition remain artifact identity. The finite executable model establishes reflexivity, antisymmetry, transitivity, and associative restrictive composition for the claimed coordinates. #30 implements strongly typed Rust source/effective documents, deterministic CBOR normalization, closed-field validation, and identity checks for the effective form. During implementation the effective document's per-rule provenance key was separated as rule_provenance, avoiding a collision with generic header provenance. Waiver evaluation and enforcement remain later Phase 3 work.
#31 makes the canonical authored boundary explicit: one layer clause followed by sorted stable-ID rule clauses, each with an optional diagnostic-only label, a closed category/operation/value, and exact waivability. The parser lowers directly through the typed model and retains policy/rule spans. §waiver, profile attachment shorthand, and expression-valued policy clauses are rejected until their dedicated implementations. Waiver grammar uses its own block rather than inheriting the policy layer shape.
#32 implements the restrictive join rather than an override stack. Crucially, every later capability, limit, and type-mode statement is checked before its layer is joined, so a forbidden weakening cannot be hidden by a more restrictive sibling. Empty scope maps canonicalize to the omitted universe; mathematically equal exact-number representations choose a deterministic encoding; exact duplicate governance combines by waivability conjunction and issuer intersection; and deny rules survive later capability declarations. Source decomposition stays in artifact identity, not effective semantic identity.
#33 assigns stable, category-specific conflict codes and treats rejection as a first-class boundary for the later waiver evaluator. During maintainer review, multi-source attribution was tightened: when earlier rules compose, diagnostics name a contributor that actually governs the failed comparison, not merely the lexicographically first provenance entry. This preserves audit truth for intersected capabilities, minimum limits, and strongest type modes.
#34 makes policy identity projections explicit and reusable. The semantic ID is the deterministic hash of effective only. The artifact ID hashes the full effective-policy document after removing only its own field, so it includes the materialized semantic ID and retained audit structure. Composition and received-artifact validation call the same recomputation methods, preventing the two paths from drifting.
#35 exposes that boundary without adding a JSON artifact layer. bhcp policy compose accepts explicitly ordered source or canonical source-policy CBOR inputs, validates the complete operation before writing deterministic effective-policy bytes, and preserves category-specific weakening diagnostics. bhcp policy inspect renders authored and effective rule values, waiver governance, semantic/artifact identities, source layers, and exact tightening provenance. Maintainer review caught and corrected an initial auditability gap where values were visible but governing waivability and authorized issuers were omitted.
#36 makes effective policy an elaboration input rather than passive metadata. Policy-aware compilation validates the document and identity algorithm, enforces the type-mode floor, deny rules, scoped capabilities, and exact dimensioned maxima, and emits no valid semantic IR when authority is absent or unresolved. The IR records both effective-policy identities and normalized per-goal decisions. Its semantic projection includes only the effective semantic ID, so changed restrictions change program meaning while a source-only decomposition change alters audit bytes without inventing different program semantics. Maintainer review closed a subtle scope gap: a global source limit must still obey every applicable scoped policy maximum, not just unscoped maxima.
#37 routes policy-added evidence through explicit host registry mappings rather than treating an obligation symbol as a command. Each applicable effective rule gets a deterministic structural target; bound producers are sorted, must still cross the ordinary in-process or capability-bounded adapter registration, and count only accepted policy-approved classes toward the positive minimum. The evidence bundle retains effective-rule and layer/policy/rule provenance directly. Duplicate restrictions collapse with all sources, distinct same-symbol demands remain independent, and producer insertion order cannot change bytes. Maintainer review closed a fail-open typed-boundary gap: removing the retained policy document while leaving IR evidence indices now fails instead of silently dropping obligations.
#38 closes the no-waiver slice with canonical four-layer inputs, deterministic effective-policy artifacts, every weakening diagnostic, equivalent and meaningful-change identity controls, source/CBOR CLI parity, schema round trips, and per-goal enforcement evidence.
#39 defines the only conforming escape from monotonic policy. A waiver targets exact source rules with one of six closed weakening shapes, cannot exceed the source restriction or typed change scope, and requires direct or finite acyclic delegated authority plus authorization and audit material. One injected decision time governs the entire atomic application over [not_before, expires_at); invalid, expired, overbroad, unauthorized, or non-waivable targets reject the whole operation. The waiver is artifact-only, while the normalized post-waiver restriction determines semantic identity. Effective-policy audit records retain the waiver reference, exact targets, and decision time; executable waiver application remains #40.
Normatively decided; fixed selection, typed artifacts, token lowering, inheritance, and overlays implemented. #41 closes the profile design boundary without adding a grammar-plugin system. A syntax mapping replaces exactly one registered keyword, punctuation, or symbol-alias coordinate with one unambiguous surface token. Omitted coordinates keep canonical spellings, so those defaults still participate in collision checks. Effective punctuation spellings must be prefix-safe; aliases expand once, cannot chain, and cannot rebind the reserved bhcp/ namespace. Formatting is a separate bounded whitespace-only record and cannot alter tokens.
Syntax and profile artifacts each have at most one exact parent and resolve root to leaf; missing parents and cycles reject the whole attachment. A child profile may keep or descend from its inherited syntax and may keep or strengthen type mode, never switch to an unrelated syntax or relax checking. Policy overlays concatenate root to leaf with duplicates rejected, then enter the existing organization → team → repository → user restrictive composer. Mapping, profile, and formatting provenance belong to the AST artifact; only normalized canonical tokens and the explicitly resolved policy/type boundary enter semantic identity. The finite decision model includes equivalent-profile normalization plus adversarial collision, inheritance, alias, core-rebinding, type-mode, and overlay vectors. #42 implements the profile-independent byte scanner; #43 adds deterministic typed Rust/CBOR artifacts; #44 validates one explicitly registered effective map and lowers it span-aware into the existing parser; #45 deterministically resolves exact profile/syntax ancestry, inherited features and mappings, policy-parent closures, effective type mode, and auditable resolution output; #46 formats validated canonical/custom source idempotently while retaining comments, mapped spellings, preamble/BOM choice, and exact canonical-token meaning; #47 implements the adversarial model as checked-in diagnostics and integration tests; #48 proves two substantially different checked-in layouts retain distinct presentation and artifact identity while one shared policy-governed semantic projection remains identical; and #49 closes the milestone with an executable 27-claim evidence audit. Invalid maps and unsupported executable extensions fail before parsing, identify the selected profile and exact offending rule, and produce no partial artifact.
Decided and implemented through the process boundary. Canonical BHCP owns verifier symbols, typed input/output evidence, trust restrictions, and structural obligation targets. A local bhcp-project.toml binding owns only a project-relative executable, an argv vector, project working scope, media types, a bounded timeout, a closed non-network effect ceiling, and expected evidence kind. The parser rejects unknown or duplicate fields and symbols, shells and command strings, path escapes, invalid media types, ambient network, and unsupported effects; local bindings do not change semantic identity or add a CDDL root.
#23 adds the capability-bounded runner: exact argv with no shell or PATH, cleared environment and inherited descriptors, canonical project scopes, request/output/time limits, deterministic audit records, process-group cleanup, and distinct accepted, rejected, unresolved, and faulted results. macOS execution is wrapped by the system sandbox; Linux requires Landlock ABI 4 enforcement and seccomp network denial. Maintainer review tightened three boundaries before merge: declared-write coverage on both platforms, inherited-descriptor closure, and stable executable identity checks through the final pre-launch boundary. Native launch still reopens the canonical executable path, so deployments must prevent concurrent replacement.
#24 maps those results through the generic verifier registry into the existing evidence-bundle root. The host encodes the closed typed candidate, forwards only normalized structural targets under an explicit effective effect ceiling, injects timestamps, retains process audit records, and records the declaration and captured executable as evidence provenance. Registry insertion order is unobservable in bundle bytes. Missing registration, accepted refutation, unresolved response, adapter fault, malformed output, and pre-launch boundary failure remain distinct in validated CBOR and human inspection. Review added an exact no-process proof for effect-ceiling violations before the unchanged head merged.
Measured. Both prose and BHCP arms passed the same independent Rust oracles on the minimal batch-transfer repair. BHCP added traceability but did not improve correctness and used more input tokens. See Pilot 001 and Pilot 002.
Measured. All policy-resolution arms passed. The interpretation skill correctly withheld a success claim while its bound oracle was unavailable, but front-loaded too much artifact context. See Pilot 003.
Measured, narrowly. A plausible prose-only implementation prioritized numeric priority before specificity and failed one withheld invariant; raw BHCP and skill arms preserved the canonical order and passed all seven. The experiment is intentionally information-asymmetric and does not establish general language superiority. See Pilot 004.
Measured. On the frozen Pilot 004 challenge, the optimized skill reduced input tokens by 26.6% versus the previous skill and brought its premium over raw BHCP to 9.6%, while retaining 7/7 correctness and fail-closed evidence claims. Wall time did not improve. See Pilot 005.
In progress. The fixture records a compact-skill run that lost part of an ordered obligation and a later-skill run that retained it at higher token cost. It is being landed without hiding the unfavorable arm under issue #21.
- Can registered adapters give agents accepted evidence in-session without increasing trusted authority?
- Do BHCP’s correctness and calibration effects persist across seeds, models, and symmetric-information tasks?
- Can the complete standard goal algebra remain self-hosted without smuggling behavior decisions into generic Rust primitives?
- Are typed policy restriction lattices expressive enough for real organization/user layering while remaining deterministic and auditable?