# Instlang source-language reference

This document specifies the implemented authored-source language. It is a
reference, not an introduction. See the [language primer](./language-primer.md)
for rationale and the [examples](./institution-language-examples.md) for
annotated applications.

The implementation is conforming when `parseInstitutionModule` accepts the
syntax and `parseAndValidateInstitutionModule` admits the resulting definition
against a reviewed `HostSchema`. Unsupported text is rejected. The TypeScript
parser, validator, and tests are the executable specification where this
document is incomplete.

## 1. Lexical classes

```text
Identifier   ::= [A-Za-z_][A-Za-z0-9_]*
DefinitionId ::= [A-Za-z_][A-Za-z0-9_]* ("-" [A-Za-z0-9_]+)*
Version      ::= [1-9][0-9]*
Integer      ::= -?(0|[1-9][0-9]*)
```

`DefinitionId` occurs only in the institution header. It permits plain,
underscore, and well-formed hyphenated external IDs. Leading, trailing, and
repeated hyphens are invalid. All executable names—declarations, processes,
states, signals, fields, locals, bindings, capabilities, operations, rule
sources, reference kinds, and symbols—use `Identifier`.

Whitespace separates tokens and is otherwise insignificant outside JSON string
literals. Commas, semicolons, parentheses, brackets, and braces are structural.
Nested delimiters and escaped characters inside double-quoted JSON strings are
recognized. Comments are not implemented.

## 2. Module

```text
Module ::= "institution" DefinitionId "@" Version
           "capabilities" "(" IdentifierList? ")"
           "inputs" "(" FieldList? ")"
           "{" Declaration* "}"

IdentifierList ::= Identifier ("," Identifier)*
FieldList      ::= Field ("," Field)*
Field          ::= Identifier ":" Type
Declaration    ::= DefaultDecl ";"
                 | ChoiceDecl ";"
                 | EffectDecl ";"
                 | ProcessDecl ";"
```

Capability, input, and body lists may be empty. Names are unique within each
scope. Every declaration has a trailing semicolon; every signal inside a state
block also has a trailing semicolon.

The pair `(DefinitionId, Version)` is the immutable `DefinitionRef`. A process
instance pins the definition reference selected at start. Registration and
activation are kernel operations, not module syntax.

### 2.1 Admission

Parsing attaches host-supplied `ResourceLimits`; source cannot select its own
limits. Admission additionally requires:

- a positive safe-integer definition version;
- definition limits no greater than host limits;
- each requested capability to name a host effect and, when present, belong to
  the host capability ceiling;
- each declared effect to exactly match the reviewed host signature;
- every expression, assignment, output, guard, and effect request to typecheck;
- every type and finite structural product to fit reviewed resource bounds;
- every referenced fact or enumeration to exist in the reviewed schema.

Admission does not grant a mandate, establish an institution, activate a
definition, or execute a process.

## 3. Types

```text
Type ::= "Bool"
       | "Number"
       | "Identifier"
       | "Json"
       | "Int" "[" Integer "," Integer "]"
       | "Text" "[" NonNegativeInteger "]"
       | "Symbol" "{" Identifier ("," Identifier)* "}"
       | "Ref" "(" Identifier ")"
       | "List" "[" NonNegativeInteger "]" Type
       | "Record" "{" FieldList? "}"
```

Constraints:

- `Number` contains finite numbers.
- `Int[min,max]` requires safe integers and `min <= max`.
- `Text[n]` bounds string length.
- `Symbol{...}` is nonempty, duplicate-free, and canonically sorted.
- `Ref(k)` is the exact record `{kind: k, id: string}`.
- `List[n] T` is homogeneous and has at most `n` elements.
- `Record{...}` is exact; fields are duplicate-free and canonically sorted.
- `Json` is any bounded serializable value. It is the explicit dynamic boundary.

### 3.1 Static assignability

Let `A <: E` mean that an expression of actual type `A` is assignable to an
expected type `E`.

```text
T <: T
Int[a,b] <: Int[c,d]       iff c <= a and b <= d
Int[a,b] <: Number
Text[a] <: Text[b]         iff a <= b
Symbol{A} <: Symbol{B}     iff A is a subset of B
Symbol{A} <: Text[n]       iff every symbol length <= n
Symbol{A} <: Identifier
Ref(k) <: Ref(k)
List[a] A <: List[b] B     iff a <= b and A <: B
Record{f:A,...} <: Record{f:B,...} iff fields are identical and each A <: B
T <: Json
Json <: T                  with runtime validation at the typed sink
```

Records do not use width subtyping. References do not cross reference kinds.

## 4. Literals and names

```text
true | false | null
JSONNumber
JSONString
JSONArray
JSONObject
integer(Integer)
symbol(JSONString)
ref(JSONString, JSONString)
list(JSONArray)
record(JSONObject)
record(field=Expression, ...)
```

Unwrapped arrays and objects have type `Json`. `list(...)` and
`record(...)` infer bounded structural types. `integer(n)` produces
`Int[n,n]`. `symbol("x")` requires `x` to match `Identifier`.
`ref("kind","id")` produces `Ref(kind)`.

A bare name resolves in this order: branch binding, signal or definition input,
then process local. At parse time an otherwise unresolved bare `Identifier` is
represented as an identifier-typed input; validation rejects it where the
surrounding typed boundary cannot accept it.

## 5. Expressions

The following forms are implemented:

```text
if Expression then Expression else Expression

Expression and Expression
Expression or Expression
not Expression
equal(Expression, Expression)

less_than(Expression, Expression)
less_than_or_equal(Expression, Expression)
greater_than(Expression, Expression)
greater_than_or_equal(Expression, Expression)

field(Expression, Identifier)
contains(Expression, Expression)
contains_field(Expression, Identifier, Expression)
length(Expression)
append(Expression, Expression)
update(Expression, Identifier=Expression, ...)
record(Identifier=Expression, ...)

HostOperation(Expression, ...)
```

`and` binds more tightly than `or`; `not` applies to its following expression.
Nested `if` expressions are delimited structurally. Function-call arguments are
comma-separated at delimiter depth zero.

Typing constraints include:

- Boolean operators require Boolean operands.
- `equal` requires compatible operand types and returns `Bool`.
- ordered comparisons require bounded integer operands and return `Bool`.
- `field` requires a declared exact-record field.
- `contains` requires a list and an assignable item.
- `contains_field` requires a list of records containing the named field.
- `length(List[n] T)` has type `Int[0,n]`.
- `append` preserves the list type and rejects execution when the list is full.
- `update` may replace only fields of its exact-record operand.
- `record(field=...)` requires at least one unique field.
- a host call must match a reviewed fact signature.

## 6. Finite binders

```text
all Binder in Expression { Expression }
exists Binder in Expression { Expression }
count Binder in Expression { Expression }
unique_by Binder in Expression { Expression }
```

The source expression must be `List[n] T`; the binder has type `T` and may not
shadow an input, local, or enclosing binder. `all`, `exists`, and `count`
require a Boolean body. `unique_by` requires a scalar or exact-record key.

Results are:

```text
all       : Bool
exists    : Bool
count     : Int[0,n]
unique_by : Bool
```

For an empty list, `all` is true, `exists` is false, and `count` is zero.
Nested binder products must fit the host structural bound. These forms do not
provide general iteration, mutation, recursion, or effects.

## 7. Reviewed queries

```text
QueryExpression ::= "query" FactQuery
FactQuery       ::= Predicate
                  | FactQuery "and" FactQuery
                  | "exists" Binder "from" EnumerationCall "." FactQuery
Predicate       ::= HostFact "(" ArgumentList? ")"
EnumerationCall ::= HostEnumeration "(" ArgumentList? ")"
```

A reviewed query has type `TruthResult`, not `Bool`. Predicates and finite
enumerations must be declared by the host. Enumeration arguments and item types
are checked, and enumeration size is bounded.

Conjunctive truth succeeds only with proof-bearing success from both operands.
Existential truth succeeds with a bounded witness and recorded proof. Failure
is an explicit explanation, not Boolean false manufactured by authored code.

## 8. Defaults

```text
DefaultDecl ::= "default" Identifier ":" Type "::=" DefaultRule
                ("|" DefaultRule)*

DefaultRule ::= "base" Guard ("then" Expression)?
              | "except" RuleSource "for" DefaultName
                "when" Guard "then" Expression
                ("overrides" RuleSourceList)?
```

The omitted base value is permitted only for a `Bool` default and means `true`.
An exception without an explicit `overrides` list overrides `base`. Rule-source
names are unique. Override targets must exist and the override graph must be
acyclic. Source order does not establish priority.

Evaluation produces exactly one of:

```text
DefaultResult<T> ::= value(T, source) | absent | conflict(rule_sources)
```

```text
evaluate default DefaultName

match default DefaultName {
  value(binding) -> Expression;
  absent -> Expression;
  conflict(binding) -> Expression
}
```

All three branches are required and unique. `value` and `conflict` bindings may
be omitted when unused; `absent` has no payload.

## 9. Choices

```text
ChoiceDecl ::= "choice" Identifier ":" Type
               "candidates" Binder "from" Expression
               ("where" Expression)?
```

The candidate source must be a bounded list, an assignable value, or a reviewed
`Json` value validated at evaluation. A predicate, when present, is evaluated
with the candidate binder and must have type `Bool` or `TruthResult`.

Evaluation produces exactly one of:

```text
ChoiceResult<T> ::= empty | singleton(T) | finite(Json) | invalid(Text[64])
```

```text
enumerate choice ChoiceName

match choice ChoiceName {
  empty -> Expression;
  singleton(binding) -> Expression;
  finite(binding) -> Expression;
  invalid(binding) -> Expression
}
```

All four branches are required and unique. Only payload-bearing branches may
declare bindings.

## 10. Truth matching

```text
match truth Expression {
  true(binding) -> Expression;
  false(binding) -> Expression
}
```

The matched expression must have type `TruthResult`. Both branches are required
and unique. The success binding contains proof data; the failure binding
contains explanation data. Bindings may be omitted.

## 11. Effects

```text
EffectDecl    ::= "effect" Operation "(" FieldList? ")"
EffectRequest ::= Operation
                | Operation "(" AssignmentList? ")"
AssignmentList ::= Identifier "=" Expression
                   ("," Identifier "=" Expression)*
```

The definition header must request every declared or performed effect as a
capability. The declaration must exactly match the host effect signature. Each
request supplies exactly the declared argument record with assignable values.

Capability admission is not political authorization. Where the host requires
mandates, execution additionally requires an active mandate whose operation and
constraints cover the request and whose authority lineage remains active.

## 12. Processes

```text
ProcessDecl ::= "process" Identifier
                ("outcome" Type)?
                ("locals" "(" FieldList? ")")?
                ("initial" Identifier)?
                "{" State+ "}"

State ::= "state" Identifier ("terminal")?
          ("output" "(" Expression ")")?
          ("{" Signal* "}")?

Signal ::= "on" Identifier ("(" FieldList? ")")? SignalBody ";"
         | "automatic" SignalBody ";"

SignalBody ::= ("require" Guard)?
               ("assign" AssignmentList)?
               Transition?
               ("enact" "amendment" Expression)?
               ("perform" EffectRequestList)?

Transition ::= "->" Identifier | "->" TransitionMatch
```

If a signal declares an input list, that exact record replaces the module-input
environment for the transition. If it omits parentheses, module inputs are the
signal inputs. Locals are a separate environment.

### 12.1 State invariants

- Process, local, state, and signal names are unique in their scopes.
- A process contains at least one state.
- An explicit initial state must exist.
- Every transition target must exist.
- A terminal state has no signals.
- Only a terminal state may declare `output`.
- If an outcome type is declared, every terminal state has an assignable output.
- A state has at most one `automatic` signal.
- An automatic signal has no inputs.

### 12.2 Signal actions

Clauses occur in the order shown by `SignalBody`. Assignments target declared
locals and are evaluated from the pre-transition environment. Guards have type
`Bool` or `TruthResult`. A truth-valued guard contributes proof provenance; a
Boolean guard does not.

`enact amendment` requires a string-like proposal ID, a transition to a terminal
state, and a string-like terminal output. It selects an amendment proposal; the
kernel performs proposal, target, approval, registration, and activation checks.

One accepted signal is atomic. Input validation, guard evaluation, assignments,
outcome selection, requested effects, mandate checks, resource limits, host
composition, and host reduction must all succeed before events are published.

### 12.3 Outcome-driven transitions

```text
TransitionMatch ::= "match" "truth" Expression "{" TruthBranch TruthBranch "}"
                  | "match" "default" Identifier "{" DefaultBranches "}"
                  | "match" "choice" Identifier "{" ChoiceBranches "}"

Branch ::= BranchName ("(" Identifier ")")? "->" Identifier
           ("assign" AssignmentList)?
           ("enact" "amendment" Expression)?
           ("perform" EffectRequestList)? ";"?
```

Each required branch occurs once. The selected branch is the entire transition
action. A signal cannot mix top-level assignment or enactment clauses with an
outcome-driven transition. Unselected branches have no effects.

## 13. Runtime bounds

`ResourceLimits` are reviewed host input. The implemented limits cover event
count, automatic steps, effects per transition, proof items, storage bytes,
list items, record fields, value depth, and structural binder products.

All values, inputs, metadata, provenance, local state, effect requests, and
outputs must be bounded serializable values. Canonical serialization sorts
record keys recursively. Failure to satisfy any bound rejects the candidate
transition without publishing partial state.

## 14. Reported-world records

These standalone parsers are part of the implemented language surface but not
institution-module declarations:

```text
attestation Actor Duty JSON
fulfillment_report Actor Duty JSON
breach_allegation Actor Duty JSON
adjudicated_finding Actor Duty JSON
```

`Actor` and `Duty` use `Identifier`. The payload must be serializable JSON. A
record reports a claim; it is not itself proof of that claim.

## 15. Kernel and host operations outside source syntax

The following are not source keywords:

- definition registration, activation, and amendment enactment;
- fact-snapshot recording and proof replay;
- authority genesis, delegation, revocation, and mandated-effect audit;
- institution chartering, activation maps, dissolution, and lifecycle handling;
- addressed interaction request, delivery, request authorship, and authorization;
- authentication, persistence, networking, polling, and host-world reduction;
- generic fungible-ledger operations.

See [Authority, chartering, and institution interaction](./delegated-authority-and-chartering.md)
and [Semantic kernel and ownership boundary](./semantic-kernel.md).

## 16. Deliberate exclusions

The implemented source language has no comments, imports, macros, inheritance,
definition composition, user-defined functions, arbitrary reducers, host-code
upload, recursion, unbounded collections, general loops, mutable variables,
parallel composition, implicit time, networking, identity, distributed
consensus, or source-defined host schemas.

## Appendix A. Canonical `founding@1` source

These modules are the exact laws parsed and admitted by the Nomurgy Founding
host. The host supplies `member(Text[64]) -> TruthResult`, `hold_asset`, and
`return_asset`; charters and mandates remain kernel artifacts.

### A.1 Bootstrap

```instlang
institution nomurgy-bootstrap @ 1 capabilities() inputs() {
  process RootCharter outcome Json locals(charter: Json) initial pending {
    state pending {
      on complete(actor: Text[64]) require member(actor) -> complete;
    }
    state complete terminal output(charter);
  };
}
```

### A.2 Assembly

```instlang
institution nomurgy-assembly @ 1 capabilities(hold_asset, return_asset) inputs() {
  effect hold_asset(assetId: Text[64]);
  effect return_asset(assetId: Text[64]);
  process ChildCharter outcome Json locals(artifact: Json) initial pending {
    state pending {
      on complete(actor: Text[64]) require member(actor) -> complete;
    }
    state complete terminal output(artifact);
  };
  process InstitutionDissolution outcome Json locals(artifact: Json) initial pending {
    state pending {
      on complete(actor: Text[64]) require member(actor) -> complete;
    }
    state complete terminal output(artifact);
  };
  process InteractionAuthorization outcome Json locals(artifact: Json) initial pending {
    state pending {
      on complete(actor: Text[64]) require member(actor) -> complete;
    }
    state complete terminal output(artifact);
  };
  process Governance locals(artifact: Json, approvals: List[2] Text[64]) initial first_approval {
    state first_approval {
      on approve(actor: Text[64]) require member(actor) assign approvals=append(approvals, actor) -> second_approval;
    }
    state second_approval {
      on approve(actor: Text[64]) require member(actor) assign approvals=append(approvals, actor) -> approved;
    }
    state approved terminal output(artifact);
  };
}
```

### A.3 Custodian

```instlang
institution nomurgy-custodian @ 1 capabilities(hold_asset, return_asset) inputs() {
  effect hold_asset(assetId: Text[64]);
  effect return_asset(assetId: Text[64]);
  process Custody initial waiting {
    state waiting {
      on hold(assetId: Text[64]) -> held perform hold_asset(assetId=assetId);
    }
    state held {
      on return(assetId: Text[64]) -> returned perform return_asset(assetId=assetId);
    }
    state returned terminal;
  };
}
```