Instlang language reference #

This is the canonical language guide for the implemented InstLang core. Part I is a first-principles explanation of the semantic model and the reasoning behind its boundaries. Part II is the normative implemented source-language subset. In both parts, the parser, validator, and tests remain the executable reference; this document is the maintained human-readable specification.

The presentation is deliberately bottom-up. It defines notation, source text, and data structures before using terms such as definition, version, admission, or replay.

Part I: Conceptual model #

1. Purpose and scope #

Instlang is a small language for defining an institution: a bounded rule system that receives explicitly shaped requests, evaluates named reviewed facts, changes its own recorded process state, and requests narrowly specified effects from a surrounding application or game.

An institution may describe a ballot procedure, an appeal, an escrow, a guild rule, a licensing decision, or the procedure by which a game changes some of its own rules. Its design objective is not universal computation. It is to make the following objects finite and inspectable:

1. the rules currently in force;
2. the input and reviewed facts used to reach a decision;
3. the resulting institutional state change;
4. the limited external effects requested by that change; and
5. the procedure by which rules can later be replaced.

Instlang therefore has aspects of a rule engine (defaults, exceptions, and facts), a workflow engine (states and transitions), and an event-sourced system (immutable history and reconstruction). Its characteristic extra feature is that the rules are themselves versioned data, and a bounded constitutional procedure can authorize replacing the active rule version. That is the basis for the project’s qualified “computerized Nomic” claim.

The qualification matters. The language neither executes arbitrary prose nor allows institutions to upload arbitrary host code. Hosts still determine the meaning of facts and effects, and an immutable constitutional kernel limits the scope of self-amendment.

2. Notation and representations #

We use standard notation from programming-language semantics.

• x : T reads “x has type T.”
• { f : T, ... } is a record type: a finite mapping from named fields to values of the given types.
• Set<T> is a meta-level finite unordered collection of T; List<T> is a finite ordered collection of T. Set is notation here, not a source language value type.
• A × B → C is a total function from a pair of values to a value.
• A ⇀ B is a partial function: some A values have no valid B result.
• Γ ⊢ e : T is a typing judgment: in type environment Γ, expression e has type T. A type environment is a finite map such as Γ = { member : Identifier, approve : Bool }.
• ε denotes the empty sequence in a grammar.

One rule appears in three representations:

source text  --parse-->  abstract syntax tree  --serialize-->  event-safe data

Source text is the string an author writes. An abstract syntax tree (AST) is the structured data produced by parsing; it retains meaning-relevant structure and discards cosmetic whitespace. A serialized value is a finite JSON-compatible representation that may be included in an immutable event.

Parsing answers whether a string has a permitted grammatical form. Validation answers whether the parsed AST is meaningful under a reviewed host schema. Neither parsing nor validation changes which rules are active.

3. Source grammar, definitions, and versions #

3.1 Lexical categories #

The outer source grammar uses these categories:

<Identifier>      ::= [A-Za-z_][A-Za-z0-9_]*
<PositiveInteger> ::= [1-9][0-9]*

An identifier is initially only a restricted string. The position in which it appears gives it meaning: voting may be a definition identifier, record_vote an effect/capability name, and member a field name.

3.2 Outer module grammar #

The simplified outer grammar is:

<module> ::= "institution" <definition-id> "@" <version>
             "capabilities" "(" <capability-list> ")"
             "inputs" "(" <field-list> ")"
             "{" <declaration>* "}"

<definition-id> ::= <Identifier>
<version> ::= <PositiveInteger>
<capability-list> ::= ε | <Identifier> ("," <Identifier>)*
<field-list> ::= ε | <field> ("," <field>)*
<field> ::= <Identifier> ":" <value-type>

For example:

institution voting @ 1 capabilities(record_vote) inputs(member: Identifier) {
  ...
}

parses at its header as follows:

Source text	AST field	Meaning
voting	definitionId: "voting"	The name of a family of rule versions.
1	version: 1	The positive version number in that family.
record_vote	capability name	A requested host-effect authority, subject to host approval.
member: Identifier	input field	An external input named member with type Identifier.
{ ... }	declarations	The rules and processes belonging to this definition.

The @ 1 is therefore the version field. It is neither a player id nor a comment. The source header is the first line of the source text from which a candidate rule definition is parsed.

3.3 Definition identity #

The stable identity of a definition is represented by:

type DefinitionRef = {
  readonly definitionId: string;
  readonly version: number; // positive safe integer
};

If Id is the set of valid definition identifiers and Nat+ is the set of positive safe integers, then:

DefinitionRef = Id × Nat+

The pair is needed because voting alone identifies a family, not a specific artifact. ("voting", 1) identifies the rules written in version 1; ("voting", 2) identifies a later replacement. The parser maps voting @ 1 directly to {definitionId: "voting", version: 1}. It does not infer versions from file names, timestamps, commits, or registration order.

A simplified definition type is:

type AuthoredDefinition = {
  readonly reference: DefinitionRef;
  readonly capabilities: ReadonlySet<string>;
  readonly limits: ResourceLimits;
  readonly inputs?: readonly Field[];
  readonly declarations?: readonly Declaration[];
};

type Field = { readonly name: string; readonly type: DataType };

Thus the parser has the conceptual signature:

parseModule : SourceText × ResourceLimits × EnumerationSchema
            ⇀ AuthoredDefinition

3.4 Why the version is semantically necessary #

Suppose an instance of a voting procedure starts under ("voting", 1). The institution later adopts ("voting", 2), perhaps changing its quorum. The old instance must not silently acquire the new quorum. Instead it is pinned to the definition reference under which it started.

Without a version, replaying a historical event involving voting is ambiguous: should the runtime interpret the event using the old rules that accepted it, or the rules active today? Definition references eliminate this ambiguity.

The registry stores definitions and named active slots:

type DefinitionRegistry = {
  readonly definitions: readonly AuthoredDefinition[];
  readonly active: Readonly<Record<string, DefinitionRef>>;
};

An activation is a named slot whose value is a definition reference. For example, active["constitution"] = {definitionId: "voting", version: 2} says that new work started at the constitution activation uses version 2. Older versions remain registered so past events can still be replayed.

3.5 Five distinct operations #

The following words name different operations, not synonyms:

source text
  --parse-->       candidate AST
  --validate-->    admitted candidate or error list
  --register-->    catalogue event and stored definition
  --activate-->    active[name] = DefinitionRef
  --execute-->     process work under the chosen definition

• Parse: recognize the grammar and produce an AST.
• Validate: check semantic constraints, including types, bounds, names, process graphs, and compatibility with a host schema.
• Admit: accept a definition because validation succeeded. Admission alone does not mutate the registry.
• Register: append an event that stores an admitted serializable definition in the catalogue.
• Activate: change a named activation slot to point to one registered definition reference.
• Execute: evaluate requests against a running process pinned to a particular definition reference.

The combined convenience entry point is conceptually:

parseAndValidate : SourceText × HostSchema
                 → Accepted(AuthoredDefinition) | Rejected(Reason)

4. Resource limits and serializable values #

Every definition contains reviewed non-negative safe-integer limits:

type ResourceLimits = {
  maxCandidates: number;
  maxValueDepth: number;
  maxListItems: number;
  maxRecordFields: number;
  maxProofItems: number;
  maxAutomaticTransitions: number;
  maxEffects: number;
  maxEvents: number;
  maxStorageBytes: number;
};

These are semantic bounds, not hints for optimizing an implementation. If maxCandidates = 10, an eleven-candidate result is invalid; the interpreter must reject it rather than silently discard one candidate. Similarly, maxAutomaticTransitions prohibits an unbounded automatic loop, and maxValueDepth limits nested input data. A definition may choose tighter bounds than the host schema but cannot exceed reviewed host bounds.

Values crossing an interpreter, host, or event boundary must be serializable:

Serializable ::= null | boolean | finite-number | string
               | List<Serializable>
               | Record<String, Serializable>

Arrays have no holes; records have string keys and ordinary enumerable data properties; cycles, functions, class instances, symbols, NaN, and infinity are rejected. Record keys are sorted in canonical serialization, so {"a":1,"b":2} and {"b":2,"a":1} have the same serialized identity.

5. Source value types #

InstLang values are finite and serializable. A source type is not merely a runtime tag: it declares the bounds, equality shape, nested structure, and replay representation that an authored value may have. Primitive dynamic boundaries such as Json are explicit and remain subject to resource limits; they do not make the rest of the language dynamically typed.

Parameterized descriptors make institutional state inspectable. Integer and text ranges, finite symbols, reference kinds, list maxima, homogeneous item types, and exact record fields all participate in admission and runtime validation. Descriptor order is canonicalized, so cosmetic source ordering cannot change definition identity.

The exact descriptor grammar and membership rules appear once in Part II, under “Parameterized value types.” The conceptual distinction is important: known institutional state should use a bounded descriptor, while unstructured host or evidence payloads should use Json explicitly. Typed literals and record/list constructors preserve structural information when an expression would otherwise be inferred as dynamic JSON.

6. The host boundary: schemas, capabilities, facts, and effects #

The host is the surrounding game or application. It owns databases, networking, identity, user interfaces, scheduling, and physical/world effects. Instlang does not allow an authored definition to upload arbitrary code into the host. Instead, the host supplies a reviewed schema of the external names that definitions may use:

type HostSchema = {
  readonly limits: ResourceLimits;
  readonly effects: ReadonlyMap<string, EffectDeclaration>;
  readonly facts?: ReadonlyMap<string, HostFactDeclaration>;
  readonly enumerations?: ReadonlyMap<string, HostEnumerationDeclaration>;
  readonly grantedCapabilities?: ReadonlySet<string>;
};

An effect is a typed request for a host-side action, not an immediate uncontrolled mutation. For example:

effect record_vote(member: Identifier, approve: Bool)

declares that an institutional transition may request an operation named record_vote with exactly fields member and approve. The schema determines whether that operation exists, which capabilities may use it, and how compatible requests are composed into a host effect plan.

A capability is a named authority to request one effect. A definition must declare the capability; the host schema must define the effect; and the host may additionally restrict the granted-capability set. Therefore merely writing an operation name in source never grants filesystem, network, or arbitrary database authority.

A fact is a named reviewed host predicate or value source. The definition may query eligible(member) only if the schema declares it with compatible argument types. The host implements that fact: for example, it may inspect its current membership records and return either evidence that the member is eligible or an explanation that they are not. The institution decides what that answer means for its own process; it does not supply arbitrary fact implementation.

An enumeration is a named finite, typed host source used by bounded existential queries. The source definition supplies neither arbitrary fact implementation nor arbitrary effect reducer.

7. Expressions and reviewed-claim outcomes #

An expression is a finite AST node evaluated by the interpreter without directly mutating the host. Current expressions include literals, inputs, process locals, case bindings, host calls, equality, field access, Boolean operators, conditionals, typed list and record operations, bounded collection binders, bounded integer comparisons, defaults, choices, and explicit outcome matches.

For example, in the type environment

Γ = { member : Identifier, approve : Bool }

we have these typing judgments:

Γ ⊢ member : Identifier
Γ ⊢ approve : Bool
Γ ⊢ integer(2) : Int[2,2]

The most important distinction in the language is between a Boolean data value and a reviewed-claim outcome. TruthResult is the implementation and grammar name for that outcome:

Bool        ::= true | false
TruthResult ::= true(proof) | false(reason)

Bool is ordinary data: a ballot field, a local flag, or the condition of an if expression. A TruthResult is a transient result produced when the interpreter evaluates a query against a host fact (or combines such queries). It is not ordinary source data that an author creates, stores in a field, or returns as a process result. Its true case carries a finite proof (provenance showing the reviewed facts used to establish the claim); its false case carries an explicit explanation.

This distinction matters at the point where a process needs an answer from the surrounding game or application. Suppose a player asks the institution to decide an admission. The process receives the decide signal, the interpreter asks the host's reviewed eligible(member) fact, and the source rule chooses the institutional consequence. The host answers the factual question; the authored rule chooses the next state, local data, and permitted effects.

A reviewed-claim outcome must be consumed explicitly. match truth is most often written inside a process transition (processes are introduced in section 9). A Boolean expression such as a binder result or integer comparison is ordinary data and may instead be used directly as a requirement or branch condition; it does not carry reviewed proof provenance.

on decide -> match truth(query eligible(member)) {
  true(proof) -> admitted assign decision=proof;
  false(reason) -> rejected assign decision=reason;
}

Here admitted and rejected are states of the surrounding process. proof and reason are bindings available only in their respective branches; an author may copy them into a Json local or use them in a declared effect. The runtime records which branch the transition took. A successful require query ... additionally records its proof as provenance for the accepted event.

There is no implicit coercion from TruthResult to Bool. Allowing if eligible(member) then ... would erase whether a claim succeeded with a proof or failed with a reason exactly where institutional authority was decided.

8. Bounded fact queries, defaults, and choices #

The reviewed fact-query fragment is:

query predicate(arguments)
query left and right
query exists item from source(arguments). query body

It is positive because it includes conjunction but no general negation. It is bounded because enumeration queries range only over a host-declared source with a finite maximum item count. Every query produces a reviewed-claim outcome: a successful conjunction retains the evidence for each constituent claim, while a failed query supplies its explanation. Besides match truth, these outcomes are used as process requirements and as the applicability checks of default rules and choice predicates.

The language also has pure generic binders over typed local lists. They answer bounded Boolean or counting questions without producing reviewed fact proof:

all ballot in field(state, ballots) {
  contains(field(state, voters), field(ballot, voter))
}

exists claimant in field(case, claimants) {
  equal(claimant, actor)
}

count ballot in field(state, ballots) {
  equal(field(ballot, approve), true)
}

unique_by transfer in field(case, transfers) {
  record(first=field(transfer, from), second=field(transfer, to))
}

For a source of type List[n] T, the item binding has type T, all and exists return Bool, and count returns Int[0,n]. Empty-list semantics are fixed: all is true, exists is false, and count is zero. unique_by rejects repeated finite keys; its key may be a scalar or an exact record. Nested binders are admitted only when their finite product bound fits the reviewed structural limit.

Bounded integer comparisons connect these results to typed thresholds:

greater_than_or_equal(
  count ballot in field(state, ballots) {
    equal(field(ballot, approve), true)
  },
  field(field(state, quorum), minimumApproval)
)

The operands must have compatible bounded integer ranges. These constructs do not add general loops, unconstrained lambdas, mutation, or a general fold.

The remaining collection primitives stay separate from quantification: contains tests membership, contains_field tests a field in a typed record list, length maps List[n] T to Int[0,n], append constructs a successor list only when its bound permits another item, and update immutably replaces existing fields of an exact typed record. These operations are pure and do not create reviewed proof or host authority.

A default declaration has a base rule and optional exception rules. An exception has a stable source name and an explicit overrides relation; its textual position is not priority. Default evaluation produces:

DefaultResult<T> ::= value(T, provenance) | absent | conflict(sources)

Authors must match these cases when a concrete value is required. This avoids silently choosing the last rule or treating legal/institutional ambiguity as a Boolean falsehood.

A choice declaration computes a bounded canonical candidate set:

ChoiceResult<T> ::= empty | singleton(T) | finite(List<T>) | invalid(reason)

One candidate, many candidates, no candidates, and an invalid bounded result are intentionally different cases. A game can require a vote when there are many candidates instead of accidentally treating a candidate list as a priority order.

9. Processes and transitions #

A process is the authored workflow for one in-progress institutional matter: one admission, ballot, appeal, escrow, or amendment. "Authored" only means that its states and rules come from the institution's source definition; the host still starts instances and submits their signal requests. A process is a request-driven extended finite-state machine (EFSM).

• A finite-state machine has finitely many named control states and transitions between them.
• “Extended” means the process also has a finite typed local record.
• “Request-driven” means it advances only for an explicit signal request, except for bounded automatic transitions.

The source shape is:

process P outcome Type locals(field: Type, ...) initial state_name {
  state state_name {
    on signal_name(request_field: Type, ...)
      require query ...
      assign local=expression, ...
      -> next_state
      perform effect_name(field=expression, ...);
  }
  state finished terminal output(expression)
}

A transition is one on signal ... rule within a state. It says: while this process instance is in this state, if this signal arrives with valid request data and any reviewed requirement succeeds, make these assignments, request these effects, and move to this next state. Thus the on decide -> match truth ... example above is one transition; the process is the larger container holding its states and transitions.

For the admission scenario from section 7, the complete process skeleton is:

process Admission locals(decision: Json) {
  state pending {
    on decide -> match truth(query eligible(member)) {
      true(proof) -> admitted assign decision=proof;
      false(reason) -> rejected assign decision=reason;
    };
  }

  state admitted terminal;
  state rejected terminal;
}

When the host submits decide for a pending instance, this code evaluates the reviewed fact and records exactly one transition: either pending → admitted or pending → rejected. It does not run by itself merely because the host's membership data changes.

A running process instance includes its pinned DefinitionRef, a process name, instance identifier, current state, and local record. Signal handling has the conceptual partial transition relation:

(definition, instance, signal, request, reviewed-fact-runtime)
  ⇀ (new-instance, effect-plans, accepted-event)

To handle a signal, the interpreter:

1. finds the pinned definition and current state;
2. checks the signal name and exact request fields;
3. evaluates its proof-bearing requirement, if any;
4. evaluates assignments, selected outcome branches, and effect arguments;
5. validates types, capabilities, effect fields, and resource limits; and
6. records one accepted transition event if every preceding step succeeds.

This is atomic at the institutional boundary: a rejected transition does not leave half-updated locals or a partially accepted effect plan. Automatic transitions are bounded by maxAutomaticTransitions, preventing an unbounded internal loop. A process may still wait indefinitely for a player request; there are no implicit timers, callbacks, or background threads.

Current processes are sequential within one instance. Multiple instances may exist, but there is no intra-instance fork/join construct. A future bounded workflow-net semantics is appropriate only if a concrete institution needs parallel work, such as two independent reviews that must both complete.

10. Events, replay, and lifecycle #

An event is an immutable record of an accepted institutional operation. An event log is an ordered finite sequence:

H = [e₁, e₂, ..., eₙ]

Let S be runtime state. The implementation has a deterministic partial reduction function:

reduce : S × Event ⇀ S
replay(H, S₀) = foldl(reduce, S₀, H)

Here foldl means: apply reduce to initial state S₀ and e₁, then to the result and e₂, continuing through eₙ. The function is partial because an invalid event is not allowed to transform a state. Replay reconstructs state from the log rather than trusting an in-memory snapshot.

The current runtime is single writer: accepted events have one global total order. This is not distributed-consensus semantics. The host chooses which request is offered next; Instlang determines whether that request can produce the next valid event.

Lifecycle events include definition registration, activation, deactivation, replacement, process start, transition, and cancellation. If a definition is replaced while instances are live, the policy is explicit: pin old instances, reject the replacement, or cancel instances through recorded cancellation events. The runtime derives live work from the event history rather than trusting a caller-provided claim that nothing is running.

Replay establishes a limited but important property: with the same admitted definition, requests, ordered events, and relevant fact snapshot, the runtime reconstructs the same institutional state. It does not prove that an external host observation was physically true.

11. Constitutional amendment and bounded computerized Nomic #

Versioning alone is not self-government: an administrator could simply activate another version. The constitutional layer constrains rule replacement through recorded institutional data and a proof-bearing authored process.

The implemented amendment path has these parts:

1. A proposed definition is recorded as a complete serializable and pre-admitted artifact.
2. An immutable constitutional kernel fixes the activation and definition family that may be changed. It is a small fixed trust root.
3. A bounded electorate, one-time ballots, and quorum thresholds are recorded as typed institutional events. AmendmentQuorumState is reconstructed from those validated events rather than accepted from an arbitrary caller.
4. An authored amendment-vote process uses generic all and count binders, inclusive bounded integer comparisons, and the reviewed amendment_quorum_state_reviewed(state) fact. That fact succeeds only when the supplied snapshot exactly matches replayed electorate and ballot state, and its proof names the event-derived provenance.
5. The process may end with enact amendment field(state, proposalId) only on the proof-bearing true branch. Its terminal approval, proof, branch, output, effects, and amendment target are recorded and checked during replay and audit.
6. A fact snapshot may record finite reviewed fact answers and enumeration results, so that this audit need not invoke a live host callback. Host-side ballot authentication, typed validation, event identity, and replay remain authoritative boundaries.

The active constitutional definition may revise its own amendment procedure, but only within the immutable kernel’s target scope. There is real mutability: future active rules can differ because a procedure defined by current rules authorized their replacement. There is also a deliberate limit: that procedure cannot enlarge its own authority into arbitrary host code or unrelated activations.

The accurate claim is therefore a bounded computerized-Nomic substrate, not unrestricted philosophical Nomic. Natural-language interpretation, arbitrary self-modifying code, distributed consensus, general evidence/trust logic, and migration of live processes are not part of the current language.

12. Worked typed artifact #

The constitutional amendment path is a useful application of the type model. At the meta-level, its state is an exact record containing a bounded ballot list, a bounded voter list, a proposal identifier, and bounded participation and approval thresholds. The source representation expands those fields into the descriptors defined in Part II; the runtime and event log use the same canonical structure.

This is more than a schema example. The reviewed resolver reconstructs the state from validated electorate and ballot events, rejects malformed or altered snapshots, and returns event-derived provenance only for an exact match. Authored law then uses the typed lists and thresholds to perform the quorum decision. This demonstrates how finite descriptors, generic binders, reviewed facts, proof retention, and replay fit together without turning institutional state into arbitrary host-shaped JSON.

13. Future concurrency and verification #

The current process language is an EFSM. It does not require Petri nets or distributed execution. If a later example needs independent work followed by a join, the language could add a human-readable workflow construct and give it a bounded typed workflow-net semantics internally.

This would be logical concurrency, not CPU threads or distributed consensus. The event log could remain single writer and totally ordered. The benefit would be explicit fork/join behavior and stronger eventual analysis of reachability, deadlock, boundedness, and conditional completion.

No formal proof is presently claimed. A credible route to stronger assurance is: first give parsing, validation, and transition execution a precise semantics; then establish that serialization and replay preserve it; then build finite abstractions of bounded values and reviewed facts; and finally model check or prove properties of particular procedures. A Petri/workflow-net model may help at the last stage if a concrete parallel-work example warrants it.

The repository already has a bounded reachable-state analyzer for the Economancy Scarcity Case. It explores a declared finite proposal domain and action horizon through the authenticated adapter and authored automatic transitions, retaining shortest legal traces and counterexamples. A complete analysis means only that its declared finite bounds were exhausted; it is not an unbounded proof of the institution or of external host facts.

14. Summary #

Instlang is a finite, typed, event-replayed language for institutions with reviewed host seams and a bounded constitutional amendment path. An authored process is its workflow for one in-progress matter; each on signal rule is a transition within that process. Reviewed host queries produce transient TruthResult values, whose proof-bearing and explanatory cases must be handled explicitly where a transition needs an institutional decision. In the header

institution voting @ 1 capabilities(record_vote) inputs(member: Identifier) { ... }

voting is the definition-family identifier and 1 is its version. Together they create the stable reference {definitionId: "voting", version: 1}, which lets historical replay distinguish the rules that governed an old transition from later versions of the same institution.

Parameterized structural types and generic bounded collection binders are now implemented. The first concrete host example is the Economancy Scarcity Case: a SHA-256 simultaneous buy commitment/reveal boundary, a verified post-reveal opening bridge, then a sequential public proposal and final-ratification ledger carried by authored EFSM processes and exact nested record descriptors. It has not required a bounded workflow-net extension or a host-owned Json schema escape hatch. Its agreed/default effects apply to a small immutable host-world reducer that validates purchase and transfer balances atomically.

The constitutional amendment example now exercises the same typed collection machinery: replay reconstructs the electorate and ballots, authored law counts participation and approvals, inclusive bounded comparisons decide the quorum, and a reviewed snapshot fact supplies event-derived proof before enactment.

Part II: Implemented source language #

This part is the normative source-language reference for the current parser and admission boundary. Unsupported or ambiguous text is rejected; the language does not infer missing declarations, coerce values implicitly, or use declaration order as priority.

15. Lexical and module grammar #

Whitespace is normalized outside quoted JSON strings. Identifiers match [A-Za-z_][A-Za-z0-9_]*. Positive versions and all numeric bounds are safe integers.

institution name @ version capabilities(effect_a, effect_b) inputs(field: Type) {
  declaration;
  ...
}

Capabilities, inputs, and the module body may be empty. Every declaration ends in a semicolon. Module inputs, capabilities, declaration names, and effect argument names are duplicate-free. Admission checks the complete definition against the reviewed host schema, including referenced facts, effects, capabilities, types, and resource limits.

Definitions are immutable versioned artifacts. Registration stores an admitted definition; activation changes a named slot to a registered reference; process instances retain the resolved reference under which they started.

16. Parameterized value types #

Type ::= Bool
       | Number
       | Identifier
       | Json
       | Int[min, max]
       | Text[maxLength]
       | Symbol{name_a, name_b, ...}
       | Ref(kind)
       | List[maxItems] Type
       | Record{field_a: Type, field_b: Type, ...}

Number is finite; Identifier is an identifier-shaped string; Json is a bounded serializable value. Integer ranges are safe signed integers with min <= max; text and list bounds are non-negative. Symbols and record fields are identifier-shaped, unique, and canonicalized by name. Lists are homogeneous. Records are exact: values contain every declared field and no other own fields. Ref(kind) accepts only {kind, id} with the declared kind and a non-empty string id.

Static assignment permits safe widening of bounded integers, text, and lists; records remain exact and references remain kind-specific. Json can flow to a specific type only through a runtime boundary check, while specific descriptors can flow to Json. Typed sinks include inputs, locals, effects, fact results, fact snapshots, and terminal outputs.

The shared type operations are conceptually:

isDataType(value)                 descriptor shape and canonicality
sameDataType(left, right)         structural equality
isAssignable(actual, expected)    bounded static compatibility
valueMatchesDataType(type, value) exact runtime validation
parseDataType(source)             recursive source parser
formatDataType(type)              canonical diagnostics

Use explicit constructors when a literal needs structural type information: integer(2), symbol("member_a"), ref("proposal", "raise-quorum"), list(["a", "b"]), and record({"approve":true}). Typed record construction uses named expressions such as record(approve=true, proposalId=proposal).

17. Declarations #

effect operation(argument: Type, ...)

default name : Type ::= base fact_call(arguments) then expression
  | except rule_source for name when fact_call(arguments)
      then expression overrides source, ...

choice name : Type candidates item from expression
  where expression

The then value is optional only for a Bool base rule, where it means true. Exception order is not priority: overrides declares precedence explicitly, and the precedence graph must be acyclic. Every exception has an explicit stable source name. The former unlabelled except name when ... spelling is rejected.

Effects declare exact, duplicate-free argument records. A capability only requests authority; the reviewed host schema still decides whether the effect exists, is granted, and how accepted requests compose.

18. Expressions, facts, and outcomes #

Ordinary expressions may contain JSON literals, inputs, locals, case bindings, reviewed host calls, equality, fields, Boolean operators, conditionals, typed collection operations, generic binders, bounded integer comparisons, and named outcome producers.

Fact queries have this form:

query predicate(arguments)
query left and right
query exists item from source(arguments). query_body

Enumeration sources are host-declared finite relations with reviewed maximum sizes. A query produces a proof-bearing TruthResult, not an ordinary Boolean:

match truth outcome {
  true(proof) -> expression;
  false(reason) -> expression
}

match truth, match default, and match choice cases are exhaustive and each case appears exactly once. Bindings are scoped to their own branch. A proof-bearing requirement contributes recorded provenance; a Boolean requirement does not invent proof.

The pure collection and record primitives are:

contains(list, item)
contains_field(list, field, value)
length(list)
append(list, item)
update(record, field=expression, ...)
record(field=expression, ...)

contains and append require typed bounded lists. length returns Int[0,maxItems]. append rejects a full list. update replaces only existing fields of an exact record and never mutates its input. These operations are pure and do not invoke host code.

19. Generic bounded collection quantification #

The generic binder forms are the sole collection quantification and keyed uniqueness forms in the source language:

all item in list-expression {
  Boolean-expression
}

exists item in list-expression {
  Boolean-expression
}

count item in list-expression {
  Boolean-expression
}

unique_by item in list-expression {
  key-expression
}

The source must have static type List[maxItems] Item; the binder introduces item with exactly Item. all and exists return Bool. count returns Int[0,maxItems] and counts matching items. For an empty source, all is true, exists is false, and count is zero. unique_by rejects repeated evaluated keys; its key may be a scalar or an exact finite record.

Bounded integer comparisons are ordinary Boolean expressions:

greater_than_or_equal(
  count ballot in field(amendment, ballots) {
    equal(field(ballot, approve), true)
  },
  field(field(amendment, quorum), minimumApproval)
)

The comparison operators are less_than, less_than_or_equal, greater_than, and greater_than_or_equal. Operands must have compatible bounded integer ranges. Binder predicates must be Boolean, field projections must name exact declared fields, and nested binders are admitted only when their finite product bound fits the reviewed structural limit. Binders do not add loops, lambdas, mutation, general fold, effects, fact provenance, or authority.

20. Processes and transitions #

process Name outcome Type locals(field: Type, ...) initial state_name {
  state state_name {
    on signal_name(request_field: Type, ...) require guard_expression
      assign local=expression, ...
      -> next_state
      perform operation(argument=expression, ...);

    automatic -> next_state;
  }

  state terminal_name terminal output(expression)
}

outcome, locals, initial, terminal output, signal inputs, require, assign, and perform are optional where meaningful. Automatic signals have no request inputs. A terminal state has no signal block. State and signal names are unique, transition targets must exist, and there is at most one automatic signal per state.

A signal may instead select an exhaustive outcome-driven transition:

on decide -> match truth(query authorized(actor)) {
  true(proof) -> accepted assign status=proof perform record(proof=proof);
  false(reason) -> rejected assign status=reason;
};

Branch actions are the sole selected action for an outcome match. They may use the branch payload and exact signal inputs. A process transition is atomic: request validation, requirements, assignments, outcome selection, effects, capabilities, and resource limits all succeed before one accepted event is recorded. Automatic transitions are bounded by maxAutomaticTransitions.

21. Reported-world inputs #

Reported responses are separate tagged records:

attestation actor duty JSON_payload
fulfillment_report actor duty JSON_claim
breach_allegation actor duty JSON_claim
adjudicated_finding actor duty JSON_claim

The parser accepts only these tags with identifier-shaped actors and duties and finite JSON payloads. Recording a report creates an institutional event; it does not assert that an external claim is independently true. An attestation becomes an obligation only when a reviewed host fact supplies an explicit true proof.

22. Deliberate limits and coverage #

The implemented subset excludes recursive or negative fact programs, unbounded collections, general process parallelism, persistence protocols, user-defined host code, arbitrary reducers, implicit time, networking, identity, and distributed consensus. The reviewed HostSchema remains programmatic: authored definitions cannot upload host declarations or reducers.

Registration, activation, replacement, fact snapshots, constitutional enactment, persistence, identity, networking, and game hosting remain runtime or integration boundaries rather than source constructs. Authored amendment procedures may invoke the approved enactment bridge but do not directly mutate the definition catalogue.

Coverage includes typed descriptors, exact records and lists, generic binders, bounded comparisons, defaults, choices, outcome matches, process transitions, reported responses, amendment quorum, replay, provenance, persistence, and the bounded Scarcity analyzer. The analyzer explores only declared finite domains and horizons; its complete result is not an unbounded proof.