Instlang source-language reference #

This document specifies the implemented authored-source language. It is a reference, not an introduction. See the language primer for rationale and the examples 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 #

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 #

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 #

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.

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 #

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:

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 #

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:

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 #

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 #

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:

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

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 #

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:

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

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 #

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 #

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 #

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 #

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:

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 and Semantic kernel and ownership boundary.

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 #

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 #

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 #

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;
  };
}