# Semantic kernel and ownership boundary This document is the working architecture specification for the reference interpreter. It is an ownership and trust-boundary document first, not a complete formal semantics. Its purpose is to make every immutable rule answer why it is not authored institutional law, and every host seam answer why it is not being delegated to authored code. ## The boundary model The interpreter is parameterized by a fixed semantic environment: ```text Xi = (K, H) ``` where: - `K` is the trusted kernel: typed evaluation, canonical values, bounded execution, event construction, definition references, and replay rules; - `H` is the reviewed host envelope: value schemas, fact and enumeration declarations, effect schemas, capability ceilings, composition rules, and resource limits. The institutional event log and external host world are separate concerns: ```text I = replay_Xi(E) Xi |- -> reject(reason) | -> ``` Here: - `E` is the ordered institutional event log; - `I` is replay-derived institutional state, including the definition catalogue, activation pointers, and live process instances; - `W` is the host/world state, such as balances, cards, or authenticated sessions; - `q` is one submitted request or automatic transition; - `F` is the reviewed fact snapshot or bounded evidence used for this transition; and - `effect-plan` is a typed request for reviewed host effects. The notation describes the boundary rather than replacing the existing event and process specifications. In particular, institutional state should remain reconstructible from events wherever the current implementation promises replay. Host-world changes are applied by a reviewed adapter and may produce their own declared world events; they are not silently authored code. An accepted transition is therefore conceptually two coupled operations: 1. derive and validate the institutional event from one pre-request snapshot; 2. apply its reviewed effect plan atomically to the host world. Neither operation may partially commit. A rejected request appends no institutional event and applies no effect plan. ## Active and pinned law The active definition is not one mutable AST. For an activation name `x`, its current definition is resolved as: ```text R_x = D[A[x]] ``` where `D` is the immutable definition catalogue and `A` is the replayable activation mapping. A new process instance resolves and pins one definition reference. Later activation changes affect future instances only; they do not reinterpret historical signals or mutate an existing process in place. An amendment is consequently a constitutionally authorized lifecycle transition: authored law decides whether a candidate should become authoritative, while the kernel performs the bounded registration, activation, pinning, and event-history checks. This is logical self-amendment without retroactive mutation of history. ## Ownership matrix “Mutable through Instlang” means that an institution can change the behavior by admitting and authorizing a new definition. It does not mean that the definition can bypass the host's capability ceiling or world integrity rules. | Concern | Owner | Mutable through Instlang? | Why this owner? | | --- | --- | ---: | --- | | AST meaning, typing, canonical serialization | kernel | no | Changing these would change the meaning of existing definitions and events. | | Evaluation and automatic-transition bounds | kernel and reviewed limits | no | The sandbox must remain terminating and replayable. | | Event identity, atomic append, and replay interpretation | kernel | no | Partial or retroactive history would invalidate the execution model. | | Definition registration, activation, and pinning mechanics | kernel/control plane | no as mechanism | The mechanism protects history; authored law chooses whether to request an amendment. | | Which definition family an amendment may replace | constitutional kernel policy | intentionally bounded | The current v1 seam prevents an amendment from escaping its declared authority envelope. | | Existence and argument types of a host effect | reviewed host ontology | no | Authored code cannot invent a new external operation or reinterpret its arguments. | | Static effect capability ceiling | reviewed admission and host schema | no | Gameplay cannot grant filesystem, network, or other unadmitted authority. | | World integrity of an individual effect | host ontology/reducer | no | A transfer cannot debit a nonexistent balance, and a card cannot occupy an impossible world state. | | Whether an admitted effect is politically authorized | authored law plus dynamic authorization | yes | Institutions decide who may exercise an available power and under what procedure. | | Membership, quorum, deadlines, offices, proposal slots, and endorsements | authored law | yes | These are institutional procedures, not interpreter safety properties. | | Currency issuance, taxation, and other normative permissions | authored law within the host effect envelope | yes, when modeled | The host may represent minting or transfer safely; law decides when it is authorized. | | Reviewed external facts and their provenance | host/evidence provider | no guarantee of truth | The interpreter records and consumes reviewed evidence; it does not manufacture observations. | | Dynamic mandates or political authority | authored institutional state/host integration | yes, when modeled | These are mutable game or institutional records, distinct from static effect capabilities. | “Conservation” is therefore not a sufficient ownership category by itself. The host may enforce that a particular world transition is well-formed, while authored law determines whether minting, destruction, taxation, or transfer is permitted at all. ## Capabilities, mandates, and evidence Three concepts must not be collapsed into one word: ### Effect capability An admission-time ceiling saying that a definition may request a named, reviewed host effect with a particular schema. It cannot be acquired through gameplay. ### Mandate or political authority Mutable institutional state saying that an actor, office, or institution may exercise some already-admitted power under specified conditions. This is a future host/game modeling concept, not a new kernel escape hatch. ### Evidence or proof Provenance attached to a reviewed fact or derived result. Evidence explains why a transition was accepted; it is not itself an authority grant. An actual effect requires both the static effect capability and the dynamic authorization selected by authored law: ```text requested effect requires static capability ceiling and requires current authored authorization ``` ## Core semantic seams These are the shared operational rules underneath every language fragment. ### Explicit outcomes and exhaustive matching ```text TruthResult ::= true(proof) | false(explanation) DefaultResult ::= value(T) | absent | conflict(nonempty sources) ChoiceResult ::= empty | singleton(T) | finite(canonical nonempty set) | invalid(reason) ``` Proofs, explanations, sources, reasons, and set elements are finite, serializable values subject to declaration bounds. Candidate sets are canonicalized before storage or comparison; iteration order is never an institutional priority. `match` consumes exactly one constructor of its statically known outcome type. Every constructor must appear exactly once, with no catch-all case hiding a missing constructor. Cases may bind typed payloads. A `TruthResult` is never a `Bool`; ordinary Boolean operators accept only `Bool`. ### Bounds and deterministic rejection | Resource | Declared by | On exceedance | | --- | --- | --- | | Source cardinality | host enumeration | reject before derivation | | Candidate cardinality | choice expression | `invalid(bound_exceeded)` | | Collection/string size | value schema | reject validation | | Proof/provenance size | definition or host declaration | reject transaction | | Automatic transitions/requests | process | fail with bound reason | | Requested effects/events | definition/host policy | reject before append | | Process local/storage size | process schema | reject lifecycle operation | Implementations may not truncate, sample, or use iteration order to satisfy a bound. Operational CPU or memory quotas are runtime protection, not semantics, unless they are deterministic and replay-visible. ### Provenance, lifecycle, and transaction atomicity An accepted request is evaluated against one pre-request snapshot. Events carry the resolved definition references, input values, relevant proofs or provenance, outcome handling, requested effects, and composition result. Definitions are immutable and referenced as `definition-id @ version`. Activation names resolve when a new record or process is created; existing instances retain their resolved reference. Version-one lifecycle operations are explicit events using only `pin_existing`, `cancel_existing(reason)`, or `reject_change_if_running`. The execution outline is: ```text validate(snapshot, request) -> reject(reason) | admitted(context) derive(snapshot, context, outcomes) -> explicit results with provenance advance(snapshot, context, outcomes) -> waiting | completed | failed | unresolved plan(snapshot, requested effects) -> events | reject(reason) ``` Validation, derivation, advancement, composition, and limits must all succeed before effect events are appended. Waiting is valid and does not imply wall-clock progress. A rejected request appends no institutional event and applies no effect plan. ## The policy-leakage test For each host predicate or reducer, ask: > Is this a structural fact about the world and execution boundary, or is it a > normative/procedural rule that an institution might reasonably amend? If it is structural, retain it in the reviewed host boundary and document the guarantee. If it is normative, authored law should own it when the language can express it. If it is mixed, split it into: - primitive typed facts and effect reducers supplied by the host; and - authored conditions, state construction, and procedure selecting when those primitives apply. The sharper litmus test is: > Could a participant change this rule by submitting a new admitted > definition, or must a TypeScript programmer change the host? The second answer is acceptable only when the rule is deliberately part of the kernel/ontology boundary or when the current language limitation is recorded as an explicit next exercise. ## Completed vertical slice: deliberation pass The first migration target was the simplest part of the Scarcity Case successor state oracle: `valid_deliberation_pass_update`. Before migration, the public signal supplied a complete `next: Case`, and a host predicate checked that it: - preserves the frozen case fields; - preserves proposals, ratifiers, and endorsements; - contains the actor in the claimant set; and - appends the actor exactly once to `deliberators`. The authored process should instead receive the actor and construct the next local record itself. Conceptually: ```text require actor is a claimant require actor is not already in case.deliberators assign case = case with { deliberators = append(case.deliberators, actor) } ``` The exact source syntax is deliberately left for the implementation exercise. The minimum language surface should be derived from this example, not generalized in advance. It is expected to require typed list membership, bounded append, and immutable typed record update. This slice is implemented in the reference source. The Economancy definition is versioned as `@ 2` for that change; `pass_deliberation` accepts only its actor, and the authored Boolean guard plus record update constructs the successor. The host-side successor predicate was deleted. The first slice is successful only if all of the following hold: 1. the public action no longer supplies a complete successor ledger; 2. the authored definition owns the one-action-per-claimant rule; 3. the host retains only generic type, bound, event, capability, and world integrity checks for this transition; 4. accepted and rejected behavior is covered by focused tests; 5. replay reconstructs the same local record; and 6. the old host validator can be deleted or reduced to genuinely structural checks. ## Completed vertical slice: proposal append The next migration was proposal append. The Economancy definition is now versioned as `@ 3`; `propose` accepts a typed proposal record and authored law constructs both the new `deliberators` and `proposals` lists. Its guard owns claimant membership, actor/action uniqueness, proposer identity, and proposal ID uniqueness through bounded `contains_field` expressions. The subsequent proposal-domain slice also moves claimant membership, refund uniqueness, and non-reflexive transfer-pair uniqueness into authored generic binders. The reviewed host now retains only structural parsing, numeric/resource bounds, and external settlement/effect checks; the former `valid_scarcity_proposal` policy oracle is gone. The ratification `pass` action is the second small migration: it accepts only the actor and authored law appends that actor to `ratifiers`. The final endorsement migration adds a small exact typed-record constructor, `record(field=value, ...)`; `endorse(actor, proposal)` uses it to append the authored `{ claimant, proposal }` record alongside the ratifier. The old complete-successor endorsement oracle is gone. ## Completed vertical slice: phase closure The next migration moved the Scarcity Case's automatic phase-closure policy. The source is now versioned as `@ 6` and compares the bounded lengths of `claimants` with `deliberators`, then with `ratifiers`, using the pure authored expression `length(list)`. The active host facts `deliberation_complete` and `ratification_complete` were removed from the reviewed schema. ## Completed vertical slice: settlement proposal membership The Scarcity source is now versioned as `@ 7`. Its authored judgment query computes endorsement completeness, claimant membership, claimant uniqueness, and proposal-ID membership with bounded generic binders. It passes that result to the narrowed `settlement_selection_valid` fact, which checks only that endorsements agree on one proposal. The settlement reducer retains an independent proposal, case, balance, escrow, and effect-integrity check before applying effects. The host does not decide proposal-domain eligibility, proposal-ID membership, or phase closure. ## Completed vertical slice: buy scheduling, buying, and investment bids The current Economancy source is versioned as `@ 8`. `BuyScheduleGate` owns the exact eligible participant set, one-slot allowance transition, and closed phase snapshot. `BuyValidationGate` owns current-slot eligibility, `pass` or available-card choice, and bounded affordability. `InvestmentBidGate` owns active-player/balance coverage, bid affordability, and the unique-highest versus tied-bid branch. Accepted transitions retain gate snapshots and proof provenance in public event metadata, so persistence replay detects altered authored inputs, proofs, or definition references. The host continues to own commitment/reveal authentication, typed parsing, duplicate protocol identifiers, stock and escrow integrity, payment, awards, balance conservation, and world mutation. Left-to-right income arithmetic and coin mutation remain host-owned accounting mechanics, and combat behavior and combat resolution are unchanged. The constitutional amendment seam now applies the same discipline to its institutional records. Amendment targets, proposal envelopes, electorates, quorums, and ballots have exact bounded descriptors and replay decoders; raw electorate and ballot values cannot become events without crossing those descriptors. The complete next definition and tagged lifecycle policy remain explicit dynamic payloads at the amendment code boundary, rather than being silently treated as arbitrary host state. The language additions are deliberately narrow: `length` accepts a typed bounded list and returns a bounded integer whose range is derived from the list type, while generic binders express bounded cross-list field membership. Neither introduces general iteration or arithmetic. ## Collection-language checkpoint This deliberately small, generic language checkpoint is implemented. It gives the reference language one typed model for quantifying over local bounded lists. It also supplies the generic binders and bounded integer comparisons used by the authored amendment-quorum exercise below. The implemented syntax is a typed binder whose item type is derived from the statically bounded source list: ```text all endorsement in field(case, endorsements) { contains_field(field(case, proposals), id, field(endorsement, proposal)) } ``` The model includes `all` and `exists` over `List[maxItems] Item` values, and a `count` expression that returns the number of items whose predicate is true. For a source with maximum length `n`, `count` has the bounded type `Int[0, n]`. Empty-list semantics are fixed: `all` is true, `exists` is false, and `count` is zero. Bounded integer comparison expressions may compare count results with declared quorum thresholds; they accept only compatible integer ranges and return `Bool`. Keyed uniqueness is an optional generic operation over the same binder. Its key expression may be a scalar or an exact finite record. That makes ordinary uniqueness and pair uniqueness generic rather than field-specific: a pair key can be formed from two projections, while non-reflexivity remains an explicit universal predicate. Scalar equality, record projection, membership, bounded `append`, and immutable `update` remain separate operations; collection quantification does not absorb construction or mutation primitives. The static and operational rules are: - a binder source must be a statically bounded homogeneous list, and its item binding has exactly that list's item type; - field access is checked against the exact declared record type, with no dynamic or missing-field access; - predicates and comparison operands have their declared Boolean or bounded integer types, with no implicit conversion; - evaluation is pure, deterministic, and based only on the pre-request snapshot and reviewed fact results; it does not invoke effects or host mutation; - structural cost is bounded by the source maxima. Nested binders are admitted only when their statically finite product bound is itself within the reviewed limit; and - the phase provides no general-purpose loops, unconstrained lambdas, arbitrary mutation, or general `fold`. The amendment-quorum exercise is implemented. Authored law expresses voter membership, proposal matching, participation and approval counts, and bounded inclusive integer threshold comparisons. The host continues to own authenticated ballot ingestion, typed artifact validation, event recording, replay mechanics, and external fact provenance. A binder does not turn an unreviewed report into a fact or grant authority; it only derives a bounded result from admitted institutional values and reviewed evidence. The collection cleanup is complete: generic binders are the sole source and AST forms, while former specialized spellings are rejected. The resulting model can now be used to reassess whether income, buying, bidding, or combat procedure needs further collection features. The generic model does not introduce `sum`, `max`, or `fold` in this phase. A concrete non-combat policy exercise must demonstrate that need first. Parser and static-validation coverage includes binder scope and item types, exact fields, count ranges, comparison types, nested bounds, and malformed syntax. Runtime coverage includes empty and full lists, false predicates, duplicate keys, threshold edges, and deterministic proofs. The Scarcity suite must preserve acceptance, rejection, replay, persistence, and analyzer behavior, with generic-binder coverage for every former specialized predicate. Amendment-quorum coverage includes insufficient participation, insufficient approval, exact thresholds, duplicate and ineligible ballots, replay, and fact provenance. These tests must continue to distinguish authored normative rules from host enforcement and external facts. ## Completed vertical slice: bounded reachable-state analysis The Scarcity Case now has a small breadth-first analyzer in `packages/instlang/src/economancy-analyzer.ts`. It explores a finite proposal domain and action horizon by sending every candidate action through the real authenticated Scarcity Case adapter, including authored automatic settlement. Each reachable state retains a shortest legal action trace, and an invariant result may include the first counterexample state and its trace. The analyzer's `complete` result means only that its declared finite bounds were exhausted without truncation. It is not a proof of an unbounded institution, a different definition, or host facts outside the supplied domain. The initial checks cover phase closure, one claimant slot per stage, unanimous settled cases, and settled endorsement proposal membership; tests also demonstrate a deliberately false property producing a legal defaulted-case trace. ## Host-policy audit: remaining extraction candidates The collection checkpoint pauses further extraction and narrows the remaining migrations to the following inventory. Amendment quorum and the collection cleanup are implemented; the remaining items are later domain exercises. 1. **Scarcity collection migration — implemented.** The Scarcity source and documentation use generic universal membership, keyed uniqueness, and explicit non-reflexive-relation predicates. This was an equivalence- preserving source migration, not a change to Scarcity policy. 2. **Amendment quorum — implemented.** `AmendmentQuorumState` is reconstructed from validated electorate and ballot events. The authored amendment-vote fixture owns voter membership, proposal matching, participation and approval counts, and inclusive bounded integer threshold comparisons. The host retains authenticated ballot ingestion, event recording and replay, ballot/event identity checks, typed artifact validation, and reviewed fact provenance. `amendment_quorum_state_reviewed` proves that the authored snapshot is the replayed state; a successful proof-bearing `match truth` gate is retained in terminal approval metadata. The authored fixture is now the sole quorum decision path. 3. **Buy scheduling — implemented.** Authored law verifies the exact positive- allowance participant set, one slot per participant, complete post-wave allowances, and closure. Commitment/reveal verification, supply, escrow, payment, awards, and world reducers remain host responsibilities. 4. **Income, buying, and bidding — selected slices implemented.** Authored law verifies current-slot buying eligibility, available-card or `pass` choices, affordability, active-player bid coverage, bid affordability, and unique-highest investment selection. Income arithmetic and coin mutation remain host-owned accounting mechanics; no aggregate arithmetic primitive was added. 5. **Combat procedure only.** Authored law may eventually own authorization, challenge/defense procedure, sequencing, surrender, forfeiture, and sanctions. These rules are normative and violable. Combat resolution is not an extraction target: the host or external world owns attack resolution, strength and defense effects, fainting, randomness, card integrity, and persistent-world mutation. External observations and host-enforced world integrity remain outside these authored migrations. In particular, “combat procedure” does not authorize authored code to resolve attacks or mutate the persistent game world. ## Explicit non-goals This boundary does not currently commit the project to: - a general-purpose or Turing-complete authored language; - first-class kernel `Institution` objects; - equating political mandates with effect capabilities; - theorem-carrying amendments; - a Maude, Lean, or SMT backend; or - implicit parallel process semantics. Those may become later research or game-design exercises. They do not need to be prerequisites for this vertical slice.