-
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 and implemented as a target contract in #99; the pipeline itself remains incomplete. The checked-in completion manifest closes 36 roadmap keys, 99 normative scenario instances, all 17 wire roots, ten delivery stages, and a nontrivial reference-program artifact set. The reference subject crosses typed definitions and goals, ownership and effects, policy plus an exact waiver, custom presentation, a derived extension, planning inputs, execution outcomes, and per-obligation evidence without claiming those deferred stages already execute.
PR #135 tightened the frozen boundary through independent review: exact source definition/fact/clause inventories, per-definition SHA3-512 bindings, whole-file source commitments, typed execution inputs, an S8.1-conforming input-free/predecessor-only chain, exact policy authority and evidence bindings, and source-only adversarial mutations. PR #136 then completed deterministic parsing and AST construction for type, general function, predicate, and refinement definitions; review additionally closed built-in/literal binder-capture paths. PR #137 completed goal headers, clauses, cases, calls, quantification, and nested composition parsing; review closed duplicate structured fields, reserved binders, retained-payload, trailing-comma, literal-routing, unknown-keyword, signed-priority, and delimiter ambiguities. PR #138 completed governance/profile/extension parsing and materialized wire projections; review replaced permissive waiver maps with the typed six-category boundary, aligned complete extension forms with CDDL content references, and preserved arbitrary policy parameters outside closed record ordering. PR #139 completed the value/type/refinement checker; two independent review rounds converted forgeable refinement names into candidate-bound evaluated proofs, made checked Dynamic recursive, enforced exact references and relational canonicality, removed binder names from semantic identity, widened integers to the complete CBOR domain, and then rejected out-of-domain diagnostic values before serialization. PR #140 completed the total pure S5 wire expression and pattern calculus; independent review replaced bounded rational intermediates with exact arithmetic, bound verifier witnesses to the complete quantified claim and domain, canonicalized generic maps, accepted open-record extras, and bounded nonzero Decimal exponent work. PR #141 then completed deterministic function/predicate elaboration for the parsed expression slice. Independent review bound specialization cache identity to the originating template and canonical arguments, rejected source/generated symbol collisions, alpha-normalized local bindings, prohibited verifier-only predicates from pure configuration and retained ordinary calls, and separated callable definitions from eligible reducers. The reference program now reaches the next unsupported source-expression boundary rather than failing on definition resolution. Downstream roadmap work succeeds only when this same frozen subject reaches the full pipeline.
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. The later #39 and #40 work completes waiver evaluation and enforcement over that boundary.
#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.
#40 implements that contract for all six weakening categories. It validates strongly typed waiver roots, exact original provenance targets, complete contributing-source coverage, connected delegation authority, authorization, half-open time validity, and non-waivability before atomically applying any change. Deterministic category/index ordering keeps multi-target removals stable; semantic and artifact identities are rematerialized after application; inspection exposes decision time and exact targets. Maintainer review caught and fixed a multi-hop authority check that initially rejected a valid A → B → C chain. The current rule model cannot encode partial product-scope subtraction, so such non-exact scope requests reject rather than broaden authority.
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.
Decided and implemented in #25. A plan freezes arm order, model/reasoning/sandbox/toolchain pins, exact agent and judge executables, prompts and contract inputs, time/output ceilings, allowed candidate changes, and a typed canonical identity for every fixture-tree path and byte body. The controller creates an absent owned scratch tree, rejects symbolic links and unsupported file types, directs Cargo output outside candidates, clears process environments, stops output floods and surviving process-group members, and rejects incomplete or contaminated result records.
The oracle is absent while an agent runs. Every judge gets its own ephemeral candidate copy; only an explicitly oracle-using judge receives the frozen oracle, and that view plus its build target is removed before the next judge. Review found and closed delimiter-shaped tree-hash collisions, hidden target payloads, preplanted scratch symlinks, closed-descriptor descendants, delayed output-limit enforcement, ambient judge secrets, and both shared-workspace and reverse-order sibling oracle leaks. The boundary does not run a hosted model service: a trusted driver must still enforce the pinned model sandbox and network policy.
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.
Measured. Raw BHCP and prose passed all ten frozen ordered-policy invariants. A compact-skill run used fewer tokens and commands but flattened the resource → subject → action precedence ladder and passed only 8/10; a later run with the same semantic workflow passed 10/10 at substantially higher token cost. The repository preserves both skill outcomes, exact Git blobs, all four candidate patches, and executable replay against the withheld oracle under issue #21. This is evidence of run variance, not a general correctness advantage.
Measured, with invalid attempts retained. Independent review found that runs 001 and 002 had not actually confined same-host oracle reads; run 003 established that boundary but excluded all five fixed arms before model launch because temporary metadata traversal was too narrow. The separately registered run 004 corrected only that infrastructure boundary. Its five model turns completed, returned conservative failure claims, and left the starter unchanged. Visible/static checks passed, but every candidate passed only 4/10 withheld invariants, for 0/5 accepted. The five-session sample supports no population, causal, model-wide, or BHCP-versus-prose claim. See issue #26 and the run-004 report.
Implemented and measured in #27. bhcp verify discovers the nearest project manifest, compiles the exact contract, validates the typed candidate, registers only contract-bounded adapters, binds the supplied subject reference and bytes, and emits canonical evidence while preserving accepted, rejected, unresolved, and faulted distinctions. The focused fixture independently accepts its exact candidate. Forward 001 nevertheless produced no edit, adapter invocation, or success claim, so its preregistered result remains a valid 0/1 negative rather than evidence of a missing runtime path.
Audited in #28. The machine ledger pins source, task/prompt, contract and semantic identity, evaluated skill, model request, oracle, result, executable test, PR, and squash merge for eleven records. Pilot 001 is excluded from model-layer reproduction because its default model was never recorded. Invalid and excluded multi-seed attempts retain those classifications; the hardened 0/5 and 0/1 results remain valid negatives.
Preregistered in #91, executed in #92 and #93. The positive-use study completed its 12 sessions with no exclusions, no replacements, 0/12 registered-adapter use, and 0/12 acceptance. The symmetric comparison completed all 12 pairs with balanced six/six arm order, no exclusions or replacements, 0/12 acceptance in both prose and BHCP arms, paired risk difference 0, no discordant pairs, and exact two-sided McNemar p=1. All 12 claims per arm conservatively declined success and were calibrated. The result means neither representation induced a repair in this frozen single-model setup; it does not establish equivalence, superiority, or a population-wide effect. Both studies observed zero incremental pay-as-you-go spend and remained within every preregistered stop monitor.
- Under what changed, preregistered task or prompting conditions—if any—does a model actually invoke the registered adapter path, given the completed 0/12 result?
- Which larger multi-model design could distinguish representation effects from the all-zero acceptance observed in both completed comparative arms?
- 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?