ECS for Control: Review Guide

The review of an ECS program, check-point by check-point: every module before its kind, each module against its kind, the pairs of kinds, and the program as a whole; what each check reads, what must hold, and what a program without it is.

Overview

A review reads a program against the architecture's definitions and the discipline's constructs, and decides compliance. Every check-point here states a property of a program, says where it is read and what must hold, and says what a program without the property is. No check-point decides whether the program runs; the compiler and the kernel hold that.

The review is a walk in five parts:

Part A, every module before its kind: the program is built, its module list is the linker's map, every module declares its kind. These are the tools' preconditions; a review by hand can pass over them.
Part B, each module against its kind: one section per kind, self-contained, with the kind's declaration, its placement, its imports and its check-points.
Part C, pairs of kinds: the interactions, one section per pair, read once both kinds are done.
Part D, the program as a whole: check-points over all modules of one kind, or over the program.
Part E, read by a person only: the facts not in the code or not decidable from it.

Part B is walked per partition: the program's skeleton and vocabulary first, then one partition at a time through its kinds in the order of the sections, then the kinds that gather over all partitions, then Parts C, D and E once. The order of the sections is the order of reading: each section presumes the ones before it.

Two files are open during the review: this guide, and the allow-lists file that applies to the program, the library's or the project's own copy. The allow-lists file holds every kind's import list in the notation of the ECS file and defines its own reading rules in its header; the import check-point of every kind reads against it, and the guide does not restate the lists.

Preparation

The sources at a named state. A commit or a tag; the review's subject is the sources as of that state.
The allow-lists file. The library's file for its version, or the project's copy. When the tools have run, the ECS file's allow-lists line names the file used.
The ECS file and the map file, when the tools have run. The ECS file records the facts the review looks at and the tools do not judge: every module's library imports, the constants a System takes from its VALUES module, the deployment calls. The ECS map file states the evaluated values. Neither is required: every fact is in the sources, and the guide says where.
The example program. A current example program of this document set is the worked instance of every construct, which can complement the guide where a construct's listing is not enough.

Terminology

Kinds. Every module of a program is of one kind, declared in a comment before its MODULE line, (* ECSKIND: SYSTEM Manifest Name Run *). The kind names are the vocabulary of this guide; a module name is the programmer's choice.

Roles and slots. A kind's roles are the exported items a module of the kind provides, written as slots in angle brackets: <storevar>, <buildproc>. The identifier that fills a slot is the module's own, declared as a parameter of the kind declaration in the order the kind section gives. A slot's suffix is its sort: var a variable, proc a procedure.

The import lists. The allow-lists file lists, per kind, the kinds a module may import and the framework modules it may import by name, each entry with a qualifier where the kind's placement restricts it: own partition, any partition, schedule 0 only, same level. The file's header defines the qualifiers and the inheritance between its groups. A program module of any other kind is a finding; a library module is never a finding and is recorded in the ECS file for the reviewer. One library module is checked: the transport an ADAPTER declares, read for its kind declaration, counts as a module of that kind for every importer, with no qualifier, since it lies in no directory of the program.

Check-points and readings. A check-point is named by its kind and a number, SYSTEM.7; a pair of kinds by both, SCHEDULE/PARTITION.1; a check-point over the program PROGRAM.1; a check-point on the build MODULE.2, on the kind declaration ECSKIND.1. A letter in place of the number names a check-point every kind has: SYSTEM.R for the roles, .X for the exports, .I for the imports, .P for the placement. A check-point's readings are lettered, and a reading is cited with its letter: SYSTEM.7-a.

Severity. Each check-point says what a program without its property is:

violation: not compliant in any case; the property is one of the architecture's fundamentals, or a form the discipline makes mandatory;
observation: not compliant by the constructs alone, but possibly compliant with sufficient understanding of the architecture; the fact is pointed out and the programmer assesses, or a stated reason is called for;
fact: nothing is decided; the reading records what the reviewer wants to look at;
unread: the construct may achieve what the architecture requires, but the tools cannot read it; the reviewer reads the source, and the ECS file carries the gap;
precondition: a condition of the tools' reading, not of the program's compliance; the tools refuse a program without it.

A violation the kernel also stops at start-up carries stops, and names the station: the static finding and the run-time stop are one fact seen twice.

Tool-checked, tool-recorded. A check-point's status line says Tool-checked when the tools decide it, and Tool-recorded when the tools write its fact into the ECS file, by reading letter where they hold a part; no mention means the check-point is read by the reviewer alone. The tools are described at the end.

Status line. Under every check-point heading, in italics: the severity, by reading where the readings differ, then the tool mark. Violation (a, b), fact (c). Tool-checked (a), tool-recorded (c). reads: readings a and b are violations, c is a fact, the tools check a and record c, and b is the reviewer's reading.

Admitted. The last line of every check-point names what a program may do against the property and still pass, with the reason stated; "none" means the property holds without exception.

Part A. Every Module, Before Its Kind

These check-points read the program's files without knowing any kind. The first five read the linker's map file and the build products, and hold for any Astrobe program: the program is linked, its module list is the map, every module is compiled as it stands and against current interfaces, the link products are built from everything. The last two read the kind declaration's syntax and vocabulary, before the kind it declares is known. All are preconditions of the tools; a review by hand, which reads the sources and knows each module's kind without a declaration, passes over them.

MODULE.1 The program is linked

Precondition. Tool-checked.

a the program directory: exactly one linker map file lies in it

Admitted: none.

MODULE.2 The module list is the map

Observation. Tool-checked.

The map's file table is the program. A linked module whose code file lies inside the program directory and has its source is a program module, read for its declaration. A linked module without source is a library module by its mode of existence: it declares no kind, it is recorded by name, and every role demanded of it is checked at the use site against a declaration it does not have. A source in the tree the map does not list is not part of the built program: pointed out, then ignored.

a the map's file table against the tree: every source in the tree is listed in the map
b the map's file table: every linked module whose code file lies inside the program directory has its source

Admitted: a module parked in the tree for a later build; the reason is stated.

MODULE.3 Every module is compiled as it stands

Precondition. Tool-checked.

a the source and code file timestamps: each module's code file is newer than its source; a module without source has nothing to compare

Admitted: none.

MODULE.4 Every module is compiled against current interfaces

Precondition. Tool-checked.

a the code file and the imports' symbol file timestamps: an importer's code file is newer than the symbol files of the program modules it imports

Admitted: none.

MODULE.5 The link products are built from everything

Precondition. Tool-checked.

a the binary against all build products: the binary is newer than every source, code and symbol file of the program
b the map against all code files: the map is newer than every code file

Admitted: none.

ECSKIND.1 Exactly one kind declaration

Precondition. Tool-checked.

The declaration is a comment before the MODULE line whose text, with whitespace and asterisks stripped from both ends, starts with ECSKIND; its formatting inside the comment is free. Nothing after the MODULE line is read.

a the comments before the MODULE line: exactly one is a declaration
b that comment: it is the tag, an optional space, the colon, the kind and the parameters, separated by whitespace, newlines admitted, and nothing else

Admitted: none.

ECSKIND.2 The kind is in the vocabulary

Precondition. Tool-checked.

a the declaration: the declared kind is one of the reference's kinds, spelt exactly

Admitted: none.

Part B. Each Module Against Its Kind

One section per kind, in the order of reading. Each section opens with the kind's purpose, its declaration with the roles, its placement, its import group and its construct in the Implementation, and then lists its check-points: the four every kind has, roles, exports, imports and placement, instantiated for the kind, and the kind's own. Where a kind restricts nothing on exports or placement, the check-point says so: the export list is read without a rule, the level is read from the directory.

SCHEDULE

Purpose: a schedule's module: creates its partitions, sets the boundary, registers their Systems, plans, commits and runs; schedule 0's module is the program's main module, its <gateproc> called from the module body; every other schedule's <gateproc> is started by a deployment call.

Declaration: <gateproc>, the gate

(* ECSKIND: SCHEDULE Run *)

Placement: the program directory.

Imports: the SCHEDULE group of the allow-lists file.

Construct: Implementation, § Schedules and the Boundary, The Schedule Modules.

SCHEDULE.R The declaration's parameter is `<gateproc>`, and it exists as a procedure

Precondition (a, b), violation (c). Tool-checked.

a the declaration: one parameter
b the parameter: an Oberon identifier
c the module against the declaration: the parameter names a procedure of the module; exported in every started schedule's module, local in schedule 0's module

Admitted: none.

SCHEDULE.X Nothing beyond `<gateproc>` is exported

Violation. Tool-checked.

a the export list: a started schedule's module exports <gateproc> and nothing else; schedule 0's module exports nothing

Admitted: none.

SCHEDULE.I Imports are within the allow-list

Violation (a), fact (b). Tool-checked (a), tool-recorded (b).

a the import list against the declared kinds and the SCHEDULE group of the allow-lists file: every imported program module is of a kind the group names, with the group's qualifier, and every imported framework module is named there
b the import list: every other imported library module, recorded in the ECS file with the module

For the reviewer, reading b: the bring-up modules, the start-up anchor, the cores module, the error console, the clocks, and the diagnostic modules are expected here and in no other kind. Check that <gateproc>'s deployment stations configure this core's infrastructure only.

Admitted: none.

SCHEDULE.P The module lies in the program directory

Violation. Tool-checked.

a the module's directory: the program directory itself

Admitted: none.

SCHEDULE.1 Every `<gateproc>` is parameterless; schedule 0's is local and called from the module body, every other schedule's is exported and started by its deployment call alone

Violation (a), observation (b, c). Tool-checked.

A core starts at a code address and takes nothing with it: a <gateproc> with parameters is no schedule's gate. Schedule 0's module brings the whole program up, and nothing calls into it; the local procedure guarantees that. For a started schedule the deployment call pins the gate as parameterless and exported.

a the procedure heading, every schedule's module: <gateproc> takes no parameters
b the procedure heading and the module body, schedule 0's module: <gateproc> is a local procedure and is called from the module body
c the module body, every other schedule's module: <gateproc> is not called from the module body

Admitted: none.

SCHEDULE.2 `<gateproc>` runs the station sequence in order

Violation.

The kernel's stations are Install, the partitions' <createproc> calls, Begin, the partitions' <addsystemsproc> calls, Plan, Commit, Run, each once and in this order; SetBoundary stands between Begin and Plan, once. Relax is optional and belongs between Begin and Plan; Begin clears the relaxed set, so a Relax before it is void, and a second Relax replaces the first. The kernel asserts a part of this at start-up and voids the rest silently, so the reviewer reads the whole sequence.

a <gateproc>'s statements: Kernel.Run is called, last
b <gateproc>'s statements: the stations in order, each kernel station once; SetBoundary after Begin and before Plan
c <gateproc>'s statements: Kernel.Relax, when called, stands after Begin and before Plan, at most once

Admitted: none.

SCHEDULE.3 A deployment call starts a `<gateproc>`

Violation.

A deployment is read as the passing of a program procedure as a procedure actual. The deployment procedure itself comes from a library or from a module of the programmer's own, and the reviewer knows which it is.

a the deployment calls in the module body and in <gateproc>, every call that passes a program procedure as an actual: the actual is a SCHEDULE's <gateproc>

Admitted: none.

SCHEDULE.4 No waiver is in force

Observation.

A Kernel.Relax call is legitimate; whether the program is meant to ship with it is the reviewer's question. The plan check-points of Part D report their gaps whatever the waiver, and the reviewer matches them to the relaxed set.

a <gateproc>: no Kernel.Relax call

Admitted: a development build with a stated waiver.

PERIODS

Purpose: the periods: one tick period per schedule, and the Systems' periods in ticks of their schedule.

Declaration: no roles

(* ECSKIND: PERIODS *)

Placement: the program directory.

Imports: the PERIODS group of the allow-lists file, which is empty.

Construct: Implementation, § The Definition Modules, Constructs.

PERIODS.R The declaration has no parameters

Precondition. Tool-checked.

a the declaration: no parameter

Admitted: none.

PERIODS.X Nothing beyond constants and the variables the module body assigns is exported

Violation. Tool-checked.

A value the language cannot write as a constant, a record, is exported as a variable, and the module body assigns it; the body does nothing else, which is read by hand. A private variable, type or procedure reaches no constant and is nobody's concern. A private constant, the intermediate of a computed one, is the author's choice.

a the export list: constants, and variables the module body assigns

Admitted: none.

PERIODS.I Nothing is imported

Violation. Tool-checked.

a the import list: empty; a PERIODS module declares constants and needs no module

Admitted: none.

PERIODS.P The module lies in the program directory

Violation. Tool-checked.

a the module's directory: the program directory itself

Admitted: none.

A schedule's tick period is a millisecond count and a System's period a count of its schedule's ticks; that the denominations are right is read by the reviewer, Part E.

RESOURCES

Purpose: the resource choices: library handles, chip units and pins, exception priorities, each an authored choice in the owning module's vocabulary.

Declaration: no roles

(* ECSKIND: RESOURCES *)

Placement: the program directory.

Imports: the RESOURCES group of the allow-lists file, which names no kind.

Construct: Implementation, § The Definition Modules, Constructs.

RESOURCES.R The declaration has no parameters

Precondition. Tool-checked.

a the declaration: no parameter

Admitted: none.

RESOURCES.X Nothing beyond constants is exported

Violation. Tool-checked.

a the export list: constants only

Admitted: none.

RESOURCES.I Imports are within the allow-list

Violation (a), fact (b). Tool-checked (a), tool-recorded (b).

a the import list against the declared kinds: no program module of any kind
b the import list: every imported library module, recorded in the ECS file with the module

For the reviewer, reading b: the owning modules, imported for their vocabulary, a driver's unit, pin or priority constants. Check that each import serves a constant's vocabulary and that nothing is called.

Admitted: none.

RESOURCES.P The module lies in the program directory

Violation. Tool-checked.

a the module's directory: the program directory itself

Admitted: none.

PARTITION

Purpose: the partition module: creates the partition's world and registers its Systems.

Declaration: <createproc> <addsystemsproc>

(* ECSKIND: PARTITION Create AddSystems *)

Placement: its own partition directory, named as the module by convention.

Imports: the PARTITION group of the allow-lists file.

Construct: Implementation, § The Main Program and the Partitions, Constructs.

PARTITION.R The declaration's parameters are `<createproc>` and `<addsystemsproc>`, and both exist as exported procedures

Precondition (a, b), violation (c). Tool-checked.

a the declaration: two parameters
b each parameter: an Oberon identifier
c the export list against the declaration: each parameter names an exported procedure of the module

Admitted: none.

PARTITION.X Nothing beyond the two procedures is exported

Violation. Tool-checked.

a the export list: <createproc> and <addsystemsproc>, nothing else

Admitted: none.

PARTITION.I Imports are within the allow-list

Violation (a), fact (b). Tool-checked (a), tool-recorded (b).

a the import list against the declared kinds and the PARTITION group of the allow-lists file: every imported program module is of a kind the group names, with the group's qualifier, and every imported framework module is named there
b the import list: every other imported library module, recorded in the ECS file with the module

For the reviewer, reading b: device modules and the error code catalogue are expected at creation, for handles and pins. Check that each is used at creation and not after.

Admitted: none.

PARTITION.P The module lies in its own partition directory

Violation (a, b), observation (c). Tool-checked.

A partition directory is a first-level directory of the program directory holding exactly one PARTITION module. Its name equals the module's by convention, and the generator writes it so.

a the module's directory: a first-level directory of the program directory
b that directory: it holds no second PARTITION module
c that directory's name: it equals the module's

Admitted: none.

PARTITION.1 Both procedures are parameterless

Observation. Tool-checked.

A parameter would let a fact into the creation that the architecture does not control. One may be a deliberate choice, a world-creation fact passed down from the schedule; the reason is stated.

a the procedure headings: <createproc> and <addsystemsproc> take no parameters

Admitted: a stated reason for the parameter.

PARTITION.2 The registration procedure registers each System once, with its declared roles

Violation (a, b), observation (b, registered nowhere). Tool-checked.

Each Kernel.AddSystem call names a System's run procedure, manifest and name; the SYSTEM module's declaration is the authority for the names. A System registered twice produces its tokens twice and stops at Plan; a System registered nowhere may be parked for a build, and the reason is stated.

a each Kernel.AddSystem call in <addsystemsproc> against the SYSTEM modules' declarations: run, manifest and name are one module's declared <runproc>, <manifestvar> and <namevar>, and the module is a SYSTEM of this partition's directory
b the calls against the directory listing: every SYSTEM of the directory is registered exactly once

Admitted: a System present and unregistered, with the reason stated.

<createproc> creates the partition's world in phases of its own organisation and allocates the devices and writers the partition owns. What it must show is read as pairs: the call of its STATE's <buildproc> and an initialisation site for every store leaf, Part C. Which leaf is a handle, and whether the right device lands in it, is read by the reviewer, Part E. VALUES.1 is read here: no VALUES constant is an array dimension in the module.

WIRING

Purpose: the partition's structure: cardinalities and role-binding indices.

Declaration: no roles

(* ECSKIND: WIRING *)

Placement: its partition's directory.

Imports: the WIRING group of the allow-lists file.

Construct: Implementation, § The Definition Modules, Constructs.

WIRING.R The declaration has no parameters

Precondition. Tool-checked.

a the declaration: no parameter

Admitted: none.

WIRING.X Nothing beyond constants is exported

Violation. Tool-checked.

A private variable, type or procedure reaches no constant and is nobody's concern; a module body here is the one line a reviewer cannot miss in a screen of constants. A private constant, the intermediate of a computed one, is the author's choice.

a the export list: constants only

Admitted: none.

WIRING.I Imports are within the allow-list

Violation (a), fact (b). Tool-checked (a), tool-recorded (b).

a the import list against the declared kinds and the WIRING group of the allow-lists file: every imported program module is of a kind the group names, with the group's qualifier, and every imported framework module is named there
b the import list: every other imported library module, recorded in the ECS file with the module

For the reviewer, reading b: PERIODS serves the tick conversion; a module imported for a type and the error code catalogue are expected; anything else, check what it serves.

Admitted: none.

WIRING.P The module lies in its partition's directory

Violation. Tool-checked.

a the module's directory: a partition directory, flat

Admitted: none.

The store's array lengths name these constants, STATE.4. A structural fact two partitions share, a size or a protocol value across a crossing or a transport, is declared in each partition's WIRING and held equal by CONS.

VALUES

Purpose: the partition's tuning values: rates, thresholds, baudrates, anything changeable without touching structure.

Declaration: no roles

(* ECSKIND: VALUES *)

Placement: its partition's directory.

Imports: the VALUES group of the allow-lists file.

Construct: Implementation, § The Definition Modules, Constructs.

VALUES.R The declaration has no parameters

Precondition. Tool-checked.

a the declaration: no parameter

Admitted: none.

VALUES.X Nothing beyond constants and the variables the module body assigns is exported

Violation. Tool-checked.

a the export list: constants, and variables the module body assigns

Admitted: none.

VALUES.I Imports are within the allow-list

Violation (a), fact (b). Tool-checked (a), tool-recorded (b).

a the import list against the declared kinds and the VALUES group of the allow-lists file: every imported program module is of a kind the group names, with the group's qualifier, and every imported framework module is named there
b the import list: every other imported library module, recorded in the ECS file with the module

For the reviewer, reading b: PERIODS serves the tick conversion; a module imported for a type and the error code catalogue are expected; anything else, check what it serves.

Admitted: none.

VALUES.P The module lies in its partition's directory

Violation. Tool-checked.

a the module's directory: a partition directory, flat

Admitted: none.

VALUES.1 A VALUES constant is never an array dimension

Violation. Tool-checked.

This check-point is read in every module whose import group names VALUES: CONS, PARTITION, SYSTEM and LOCKED. A count is what a structure is: how many of something exists is consulted where the world is created and lives with the partition's WIRING, apart from the tuning values it parameterises, so that structure changes loudly. A size behind a module whose definition is "changeable without touching structure" is the silent extension the architecture holds hazardous. A VALUES constant may index an array: a protocol code is a position in a table by its nature, a System must be able to name it, and a code outside the table is caught where the table is filled. STATE never imports VALUES, so the store's dimensions are STATE.I's reading.

a every array type declared in the importing module: no dimension names a VALUES constant

Admitted: none.

What a VALUES constant is, how it is written and who reads it is the programmer's decision. A System may read VALUES; what it reads is recorded, SYSTEM.9.

STATE

Purpose: the partition's variable Component state: the store record and its build procedure.

Declaration: <storevar> <buildproc>

(* ECSKIND: STATE S Build *)

Placement: its partition's directory.

Imports: the STATE group of the allow-lists file.

Construct: Implementation, § Components State, Constructs.

STATE.R The declaration's parameters are `<storevar>` and `<buildproc>`, and each exists with its sort

Precondition (a, b), violation (c). Tool-checked.

a the declaration: two parameters
b each parameter: an Oberon identifier
c the export list against the declaration: <storevar> names an exported variable, <buildproc> an exported procedure

Admitted: none.

STATE.X Nothing beyond the two roles and the module's types is exported

Violation. Tool-checked.

The store types and the named array types are exported for the System signatures, which bind to them.

a the export list: <storevar>, <buildproc> and the module's types; no constant, no other variable or procedure

Admitted: none.

STATE.I Imports are within the allow-list

Violation (a), fact (b). Tool-checked (a), tool-recorded (b).

a the import list against the declared kinds and the STATE group of the allow-lists file: every imported program module is of a kind the group names, with the group's qualifier, and every imported framework module is named there
b the import list: every other imported library module, recorded in the ECS file with the module

For the reviewer, reading b: a module imported for a type, the port and buffer protocol modules, and the error code catalogue are expected. A STATE module calls nothing; check that each import serves a type.

Admitted: none.

STATE.P The module lies in its partition's directory

Violation. Tool-checked.

a the module's directory: a partition directory, flat

Admitted: none.

STATE.1 The store variable points to a store record declared here; the build procedure is parameterless

Violation (a), observation (b). Tool-checked.

A parameter on <buildproc> would let a fact into the build that the architecture does not control; one may have its reason, which is stated.

a the TYPE and VAR sections: <storevar> is an exported variable of a pointer type declared in the module, pointing to a record declared in the module
b the procedure heading: <buildproc> takes no parameters

Admitted: a stated reason for the parameter.

STATE.2 The store holds values and handles only

Violation. Tool-checked (a).

A device handle and an address are the same INTEGER to the compiler; the declaration tells them apart from nothing, the initialisation site does. The framework uses addresses everywhere, never through address arithmetic, each looked up in its device module, so no construct marks one.

a the leaves' declared types: no pointer type, no procedure type
b the leaves' initialisation sites in <createproc>, which PARTITION/STATE.2 lists: no INTEGER leaf receives an address

Admitted: none.

STATE.3 The build procedure allocates the store and nothing else

Violation. Tool-checked.

The values are given by the partition in <createproc>, PARTITION/STATE.2. An allocation after creation is the run-time heap lock's stop, not a static reading.

a <buildproc>: it contains the NEW of <storevar> and its assertion
b <buildproc>: it assigns no leaf of <storevar>

Admitted: none.

STATE.4 The store's array lengths are WIRING constants

Observation. Tool-checked.

A literal length is a judgement call like a parameter on a role procedure; the reason is stated. A VALUES constant cannot reach a store dimension, since STATE never imports VALUES, STATE.I.

a the record against the partition's WIRING: every array's cardinality is a WIRING constant

Admitted: a stated reason for the literal.

STATE.5 Nothing runs or is declared beside the store type, the store variable and the build procedure

Violation. Tool-checked.

With <buildproc> the only exported procedure and the module body empty, nothing else runs at load, and no NEW has a caller but <buildproc>.

a the module body: empty
b the procedures: <buildproc> alone

Admitted: none.

The leaves' initialisation is read as a pair, PARTITION/STATE.2; the tokens that mirror the leaves, STATE/TOKENS.1.

LOCKED

Purpose: the partition's locked Component state: written once at load, read-only thereafter, with its interface record for other partitions.

Declaration: <lockedvar> <interfacevar>, both optional: the declaration names both, and a module may declare one or neither

(* ECSKIND: LOCKED L I *)

Placement: its partition's directory.

Imports: the LOCKED group of the allow-lists file.

Construct: Implementation, § Components Locked, Constructs.

LOCKED.R The declaration's parameters are `<lockedvar>` and `<interfacevar>`, and each present one is an exported variable

Precondition (a, b), violation (c). Tool-checked.

a the declaration: two parameters, the optional roles included
b each parameter: an Oberon identifier
c the export list against the declaration: each parameter that names an item of the module names an exported variable; an optional role may be absent from the module

Admitted: none.

LOCKED.X Nothing beyond the two variables and the module's types is exported

Violation. Tool-checked.

The roles are variables; an exported procedure plays no declared role. The named types are exported for the System signatures, which bind to them.

a the export list: <lockedvar> and <interfacevar>, when present, and the module's types; no procedure, no other variable, no constant

Admitted: none.

LOCKED.I Imports are within the allow-list

Violation (a), fact (b). Tool-checked (a), tool-recorded (b).

a the import list against the declared kinds and the LOCKED group of the allow-lists file: every imported program module is of a kind the group names, with the group's qualifier, and every imported framework module is named there
b the import list: every other imported library module, recorded in the ECS file with the module

For the reviewer, reading b: device modules for device handles and types, and the error code catalogue, are expected; check that each serves a locked value or a type. VALUES.1 is read here: no VALUES constant is an array dimension in the module.

Admitted: none.

LOCKED.P The module lies in its partition's directory

Violation. Tool-checked.

a the module's directory: a partition directory, flat

Admitted: none.

LOCKED.1 Both are record variables, not pointers

Violation. Tool-checked.

An exported variable is read-only for every importer by the language, and a record variable keeps it so; an exported pointer would let an importer write through a local alias, the store's own idiom, and defeat LOCKED.2.

a the VAR section: <lockedvar> and <interfacevar>, when declared, are each an exported variable of a record type

Admitted: none.

LOCKED.2 Written in the module body only

Violation. Tool-checked.

a the module: every assignment to <lockedvar> or <interfacevar> is in the module body or in a local procedure the module body reaches

Admitted: none.

LOCKED.3 Every locked leaf has an initialisation site

Violation. Tool-checked.

A necessary condition: nothing is zeroed at load, so a leaf without a site is uninitialised. A leaf with a site may still miss its value at run time, the loop that stops short, the branch around the assignment, the VAR parameter the callee never writes; that is read by the reviewer, Part E. The parameter mode is read from the callee's procedure heading, through the import alias; for a library procedure without source the mode is unknowable and the actual counts as a site, a miss rather than a false finding. A local procedure that takes the record or a part of it as a VAR parameter is followed with the actual's path in place of the formal's path.

a the record types against the module body and the local procedures it reaches: every leaf of <lockedvar> and <interfacevar>, through nested records and arrays, appears at least once in a position that can write it: the left side of :=, the actual of a VAR parameter, or the operand of CLEAR, the leaf itself or an enclosing record or array; array indices are abstracted, L.a[i].x covers the path a[].x

Admitted: none.

TOKENS

Purpose: the partition's tokens, one per store variable; its surfaces; its token names.

Declaration: <tokensvar> <surfacesvar> <namesvar>, the latter two optional: the declaration names all three, and a module may lack the surfaces or the names

(* ECSKIND: TOKENS L I Names *)

Placement: its partition's directory.

Imports: the TOKENS group of the allow-lists file.

Construct: Implementation, § Tokens, Constructs.

TOKENS.R The declaration's parameters are the three roles, and each present one is an exported variable

Precondition (a, b), violation (c). Tool-checked.

a the declaration: three parameters, the optional roles included
b each parameter: an Oberon identifier
c the export list against the declaration: <tokensvar> names an exported variable; <surfacesvar> and <namesvar>, when present in the module, name exported variables

Admitted: none.

TOKENS.X Nothing beyond the three variables is exported

Violation. Tool-checked.

a the export list: <tokensvar>, <surfacesvar> and <namesvar>, when present, nothing else

Admitted: none.

TOKENS.I Imports are within the allow-list

Violation (a), fact (b). Tool-checked (a), tool-recorded (b).

a the import list against the declared kinds and the TOKENS group of the allow-lists file: every imported program module is of a kind the group names, with the group's qualifier, and every imported framework module is named there
b the import list: every other imported library module, recorded in the ECS file with the module

For the reviewer, reading b: the error code catalogue is expected and nothing else.

Admitted: none.

TOKENS.P The module lies in its partition's directory

Violation. Tool-checked.

a the module's directory: a partition directory, flat

Admitted: none.

TOKENS.1 The tokens variable is a record of INTEGER leaves

Violation. Tool-checked.

a the type: <tokensvar> is an exported record variable
b the type: every leaf, through nested records, is an INTEGER; no arrays

Admitted: none.

TOKENS.2 Every token is assigned once, a constant expression

Violation. Tool-checked.

a the module body: each leaf of <tokensvar> is assigned exactly once
b the module body: each right side is an expression over the program's constants and literals; no loop, no procedure, no variable

Admitted: none.

TOKENS.3 The ordinals are dense from the base

Violation. Tool-checked.

The base is the one TOKENBASES constant the expressions reach, TOKENBASES/TOKENS.1.

a the evaluated leaves: the values minus the base are exactly 0 to n-1, no repeat

Admitted: none.

TOKENS.4 A surface is a braced set of the module's own tokens

Violation. Tool-checked.

a the module body: every leaf of <surfacesvar> is a SET assigned once from a braced set
b the module body: the braced set's members are leaves of <tokensvar>

Admitted: none.

TOKENS.5 Every token has a name

Violation. Tool-checked.

a the module body: <namesvar> has one entry per token, at the token's ordinal, and no more

Admitted: none.

TOKENS.6 The back-assert holds

Observation (a), violation (b). Tool-checked.

The back-assert is the module's own check that its count agrees with TOKENBASES, the program's own start-up assertion run early. The invariant behind it, one authority for the allocation, is proven on the evaluated ranges whether or not the module asserts, PROGRAM.3; a module without the assertion departs from the proposed form and loses nothing structural, and the programmer assesses.

a the module body: an assertion referencing a TOKENBASES constant is present
b the module body and TOKENBASES: both sides of that assertion are constant expressions, and the assertion, evaluated as written, is true

Admitted: the absence of the assertion, with the reason stated.

The tokens are read against the store, STATE/TOKENS.1; against their base, TOKENBASES/TOKENS.1; against the names table, TOKENNAMES/TOKENS.1; and against the manifests, SYSTEM/TOKENS.1.

SYSTEM

Purpose: one System: its manifest, its name, its run procedure.

Declaration: <manifestvar> <namevar> <runproc>

(* ECSKIND: SYSTEM Manifest Name Run *)

Placement: a partition directory.

Imports: the SYSTEM group of the allow-lists file.

Construct: Implementation, § System Modules, The Module.

SYSTEM.R The declaration's parameters are the three roles, and each exists with its sort

Precondition (a, b), violation (c). Tool-checked.

a the declaration: three parameters
b each parameter: an Oberon identifier
c the export list against the declaration: <manifestvar> and <namevar> name exported variables, <runproc> an exported procedure

Admitted: none.

SYSTEM.X Nothing beyond the roles is exported

Violation. Tool-checked.

a the export list: <manifestvar>, <namevar> and <runproc>, nothing else

Admitted: none.

SYSTEM.I Imports are within the allow-list

Violation (a), fact (b). Tool-checked (a), tool-recorded (b).

a the import list against the declared kinds and the SYSTEM group of the allow-lists file: every imported program module is of a kind the group names, with the group's qualifier, and every imported framework module is named there
b the import list: every other imported library module, recorded in the ECS file with the module

For the reviewer, reading b: device modules read by the System and the error code catalogue are expected; the kernel beyond its access procedures, the plan report or a bring-up module among them means a System or a bring-up module in disguise. No System configures the infrastructure.

Admitted: none.

SYSTEM.P The module lies in a partition directory

Violation. Tool-checked.

a the module's directory: a partition directory, flat

Admitted: none.

SYSTEM.1 The name is assigned

Observation. Tool-checked.

The name serves the plan report alone; nothing is zeroed at load, so a System without a name prints garbage there, bounded by the name's length. A corrupt review instrument, not a wrong program.

a the module body: <namevar> is assigned at least once, in the module body itself

Admitted: none.

SYSTEM.2 The module body assigns the name and the manifest, and nothing else

Violation. Tool-checked.

A System's module body declares, it does not run: a System runs over its state in <runproc>, whose helpers are its own. Nothing is zeroed at load, so a set of the manifest that is neither assigned nor cleared is garbage, and the ECS file would record it empty.

a the module body's statements: each is the <namevar> assignment, CLEAR(<manifestvar>), or an assignment to one of the six sets of <manifestvar>
b each set assignment's right side: a set expression of braced tokens and bare surfaces, nothing computed
c every set of <manifestvar>: assigned in the module body, or CLEAR(<manifestvar>) precedes the first set assignment

Admitted: none.

SYSTEM.3 A System holds no state

Violation (a), observation (b). Tool-checked.

A module-level type is neither state nor a fact with an authority: it carries no value and fixes nothing program-wide. Three readings of one: the shape of a scratch record <runproc> uses, which concerns no check-point; a shape that mirrors part of the store, which belongs to STATE; a pointer type, which points at an allocation in <runproc>, the run-time heap lock's stop.

a the VAR section: no variable beyond <manifestvar> and <namevar>
b the TYPE section: every module-level type, pointed out

Admitted: none.

SYSTEM.4 No local constants beyond the name string

Violation. Tool-checked.

A constant in a System is a fact without an authority module: a tuning value belongs to VALUES, a structural fact to LOCKED or TOKENS, a name to TOKENNAMES. Every fact has one authority.

a the CONST section: no constant beyond the name string

Admitted: none.

SYSTEM.5 The run procedure runs to completion

Violation.

a <runproc>'s control flow and the procedures it reaches: no waiting loop on a store value or a transport predicate; no call that yields

Admitted: none.

SYSTEM.6 The kernel's station procedures are off limits

Violation. Tool-checked.

A System reaches the kernel for its types and its run-time access procedures. The check-point names the forbidden procedures, not the permitted ones: the access procedures grow with the kernel, the stations do not.

a a search for Kernel. in the module: no call of a station procedure, Install, Begin, Relax, AddSystem, SetBoundary, Plan, Commit, Run, nor of the run-context procedure GetRunCtx

Admitted: none.

SYSTEM.7 A foreign TOKENS or LOCKED module is used through its interface record only

Violation. Tool-checked.

The import of a foreign partition's TOKENS or LOCKED module is admitted by the SYSTEM group; this check-point is the usage side. What a partition publishes for others is its surfaces and its interface record, never its tokens or its locked values one by one.

a the references into other partitions' modules, the <manifestvar> assignment included: into a TOKENS module, its <surfacesvar> only; into a LOCKED module, its <interfacevar> only

Admitted: none.

SYSTEM.8 No self-loop: no token is in C or Cx and also in O, P or Px; Cp is free

Violation, stops at Plan. Tool-checked.

The kernel's self-loop check at Plan evaluates the same set per System. Cp is excluded by design: a System may consume its own previous-pass value, since the consumer runs before the producer.

a <manifestvar>: the set (C + Cx) * (O + P + Px) is empty

Admitted: none.

SYSTEM.9 The VALUES constants a System names are recorded

Fact. Tool-recorded.

What a System reads from its VALUES module is the programmer's decision; the list is recorded for the reviewer to look at.

a the import list and a search for the VALUES module's name: every VALUES constant the System names, recorded in the ECS file with the System

Admitted: none.

VALUES.1 is read here: no VALUES constant is an array dimension in the module. A System is read against its store and its tokens as pairs, SYSTEM/STATE.1 to 4 and SYSTEM/TOKENS.1.

ADAPTER

Purpose: the store access procedures over one transport, store-handle-indexed where the store path is an array, and the procedure types that carry their direction.

Declaration: <transport>, the module name of its transport; no role

(* ECSKIND: ADAPTER PeriodPort *)

Placement: its partition's directory.

Imports: the ADAPTER group of the allow-lists file.

Construct: Implementation, § Ports and Adapters, Adapters.

ADAPTER.R The declaration's parameter names its transport

Precondition. Tool-checked.

That the named module exists and is a transport is the pair's reading, TRANSPORT/ADAPTER.1.

a the declaration: one parameter
b the parameter: an identifier of a module name's form

Admitted: none.

ADAPTER.X Procedure types, procedures and the transport's value type only are exported

Violation. Tool-checked.

The transport's value type is re-exported so that a System imports the adapter and nothing of the transport.

a the export list: procedure types, procedures and the transport's value type; nothing else

Admitted: none.

ADAPTER.I Imports are within the allow-list

Violation (a), fact (b). Tool-checked (a), tool-recorded (b).

a the import list against the declared kinds and the ADAPTER group of the allow-lists file: every imported program module is of a kind the group names, with the group's qualifier, and every imported framework module is named there
b the import list: every other imported library module, recorded in the ECS file with the module

For the reviewer, reading b: service modules and the error code catalogue are expected; a device module is not. An adapter moves values and a BINDING operates hardware; check the source.

Admitted: none.

ADAPTER.P The module lies in its partition's directory

Violation. Tool-checked.

a the module's directory: a partition directory, flat

Admitted: none.

ADAPTER.1 One STATE import, the store reached through it

Violation. Tool-checked.

a the import list: exactly one STATE module
b the exported procedures: every store reference is <storevar>.<path> or a local assigned from <storevar>, and <path> is a store variable

Admitted: none.

ADAPTER.2 The store handle is taken iff a reached store path is an array, uniformly

Violation. Tool-checked.

A Component of one instance is addressed by the procedure alone, the module having selected the transport and the path; an index into a one-element array selects nothing. Several array paths under one handle are co-indexed; a module with an array path and a single path takes the handle, and one path selects by it. An array is one leaf and one token, as a single instance is.

a the procedure headings against the STATE declarations: the exported procedures take the store handle as their first parameter iff a store path the module reaches is an array; all of them or none
b the procedure bodies: every array path reached is indexed by the store handle; one argument per Component

Admitted: none.

ADAPTER.3 The procedure type carries the direction

Fact. Tool-recorded.

That a procedure type's modes are the modes of its procedure is checked by the compiler: wherever a System's procedure-typed formal receives the adapter's procedure, procedure-type compatibility includes the parameter modes, which are the direction.

a the procedures: the direction, read from the parameter modes: a VAR parameter beyond the store handle is a get, a result a read, else a put; recorded in the ECS file

Admitted: none.

ADAPTER.4 The adapter's policy is intended

Violation.

a each procedure: what it does when the transport's precondition fails, and what it records; a recorded observation goes to a store variable the calling System's manifest covers

Admitted: none.

ADAPTER.5 Nothing is declared beside the procedures and their types

Violation. Tool-checked.

An adapter is a route, not a party: stateless.

a the module: no module variable; no constant, no type beyond the procedure types and the transport's value type
b the module body: empty

Admitted: none.

What an adapter exports over its transport is the programmer's decision, within ADAPTER.X and ADAPTER.1 to 3. Its transport and the agreement of their modes are read as the pair, TRANSPORT/ADAPTER.1 and 2; its paths against the store and the tokens, STATE/ADAPTER.1 and TOKENS/ADAPTER.1.

The Transports: SPORT, QPORT, RBUFFER, BUFFER

Purpose: a transport: SPORT the sampling port, QPORT the queueing port, RBUFFER the ring buffer, each identical in interface to the framework's reference implementation of its kind; BUFFER a transport of unstated organisation with a hand-written adapter.

Declaration: no roles; the canonical interface is the kind

(* ECSKIND: SPORT *)

Placement: a partition's directory or a sub-directory of it when one partition's store holds its instances; the program directory or a helper directory when several do; or a library. Either level is admitted; the directory decides which partition, if any, the module belongs to.

Imports: the group of the declared kind in the allow-lists file, which names no kind.

Construct: Implementation, § Ports and Adapters, Per-Seam Port Modules.

The four kinds share the check-points of this section, identified TRANSPORT.

TRANSPORT.R The declaration has no parameters

Precondition. Tool-checked.

a the declaration: no parameter

Admitted: none.

TRANSPORT.X The export list is the canonical interface

Observation.

The kinds restrict nothing on exports of their own: a canonical kind's export list is read against the reference implementation, TRANSPORT.1; a BUFFER exports what its adapter needs.

a the export list: for SPORT, QPORT and RBUFFER, read by TRANSPORT.1; for BUFFER, the module's own, each item serving its adapter

Admitted: any export of a BUFFER.

TRANSPORT.I Imports are within the allow-list

Violation (a), fact (b). Tool-checked (a), tool-recorded (b).

a the import list against the declared kinds: no program module of any kind
b the import list: every imported library module, recorded in the ECS file with the module

For the reviewer, reading b: the protocol module of the kind and the error code catalogue are expected; anything else, check what it serves.

Admitted: none.

TRANSPORT.P The module's directory decides its partition

Fact. Tool-recorded.

a the module's directory: a partition directory or a sub-directory of one places the module in that partition, the program directory or a helper directory at the program level; recorded in the ECS file with the module

Admitted: either level.

TRANSPORT.1 A canonical kind has the canonical interface

Observation. Tool-checked.

A port extended for a purpose may have its reason, which is stated. BUFFER has no canonical interface. By hand: the module against the reference implementation of its kind in the library's ref/ directory for the library version.

a the export list against the reference implementation of the declared kind: SPORT and QPORT export exactly its procedures with its signatures, the value or message type aside; RBUFFER exports a subset of its access procedures, element and multiple put and get, Empty, Full, Free and Count, each with its signature

Admitted: an extension with its reason stated.

TRANSPORT.2 A canonical transport's procedure bodies follow the reference implementation

Violation.

Each algorithm module's protocol is one correct order: the sampling port's index, write and publish; the ring buffer's precondition assertion, index with write or read, publish or release with the count. A statement that differs is a correctness fault, not a style choice, so the comparison is exact. The adjust region is the reference implementation's own: for SPORT the value type; for QPORT the message type and the message count; for RBUFFER the value type and the chosen access subset. By hand: a diff of the module against its reference implementation, with every difference inside the adjust region.

a every exported procedure's body against its body in the reference implementation, outside the adjust region: the statement sequences are identical, the algorithm module's calls in the reference implementation's order

Admitted: none.

BINDING

Purpose: a partition's device seam: a module that operates interface hardware for the partition's Systems, configured at the partition's creation and called by its Systems at run time.

Declaration: no roles

(* ECSKIND: BINDING *)

Placement: its partition's directory or a sub-directory of it.

Imports: the BINDING group of the allow-lists file.

Construct: Implementation, § Bindings and Handles, Constructs.

A BINDING module is configured, never informed by import: a fact it needs from the definition arrives as a parameter, at the partition's <createproc> or at the System's call. It is imported by its own partition's PARTITION and SYSTEM modules alone; a foreign System importing it is cross-partition device sharing. Neither an ADAPTER nor a transport imports one, both being software-to-software bridges with no business with a device. No tool verifies that the module operates hardware, a device module being a library module like any other; the declaration asserts it.

BINDING.R The declaration has no parameters

Precondition. Tool-checked.

a the declaration: no parameter

Admitted: none.

BINDING.X The export list is the module's own

Observation.

The kind restricts nothing on exports: the interface is what the partition's <createproc> configures and its Systems call.

a the export list: procedures that operate the partition's device, with the handles and types they take; what each serves is read with BINDING.I-b, against the device modules imported

Admitted: any export.

BINDING.I Imports are within the allow-list

Violation (a), fact (b). Tool-checked (a), tool-recorded (b).

a the import list against the declared kinds and the BINDING group of the allow-lists file: every imported program module is of a kind the group names, with the group's qualifier, and every imported framework module is named there
b the import list: every other imported library module, recorded in the ECS file with the module

For the reviewer, reading b: the device modules are what the kind is for; check that the hardware operated is the partition's own, RESOURCES naming the owner.

Admitted: none.

BINDING.P The module lies in its partition's directory or below it

Violation. Tool-checked.

a the module's directory: a partition directory, or a sub-directory of one

Admitted: none.

BINDING.1 A module variable is pointed out

Observation. Tool-checked.

What the variable holds is read by the reviewer, Part E, "No caching below the store": on the synchronous control path nothing is held between calls beyond a device's technical state behind its handle; an asynchronous binding holds transfer state only.

a the VAR section: every module variable, pointed out

Admitted: a device's technical state; the transfer state of an asynchronous binding.

OTHER

Purpose: a module the definition places but says nothing about, tracked by existence only; the kind of every module that is of no other kind.

Declaration: no roles

(* ECSKIND: OTHER *)

Placement: the program level, in the program directory or a helper directory, or a partition's directory or a sub-directory of it. Either level is admitted; the directory decides the module's level.

Imports: the OTHER group of the allow-lists file.

Construct: Implementation, § Bindings and Handles, Constructs.

An OTHER module is configured, never informed by import: a fact it needs from the definition arrives as a parameter, at the partition's <createproc> or at the System's call. This is the library module's stance applied inside the tree, and it makes the helper portable between programs. A parameter carries a value, a handle or a procedure at run time, never an array length or a type; a helper that would need a WIRING cardinality for a declaration is playing a role that belongs in STATE or LOCKED.

OTHER.R The declaration has no parameters

Precondition. Tool-checked.

a the declaration: no parameter

Admitted: none.

OTHER.X The export list is the module's own

Observation.

The kind restricts nothing on exports.

a the export list: what each item serves is read with OTHER.I-b; an exported variable is read by OTHER.1

Admitted: any export.

OTHER.I Imports are within the allow-list

Violation (a), fact (b). Tool-checked (a), tool-recorded (b).

a the import list against the declared kinds and the OTHER group of the allow-lists file: every imported program module is an OTHER module of the importer's level, a partition's helper importing its partition's helpers, a program-level helper importing program-level helpers
b the import list: every imported library module, recorded in the ECS file with the module

For the reviewer, reading b: the kernel, the plan report or a bring-up module among them means a System or a bring-up module in disguise; check what each import serves.

Admitted: none.

OTHER.P The module's directory decides its level

Fact. Tool-recorded.

a the module's directory: the program directory or a helper directory places the module at the program level, a partition directory or a sub-directory of one in that partition; recorded in the ECS file with the module

Admitted: either level.

OTHER.1 A module variable is pointed out

Observation. Tool-checked.

What the variable is for is read by the reviewer, Part E, "No caching below the store": a synchronous helper holds nothing between calls beyond a device's technical state; a stateful helper imported by two Systems is a channel beside the store.

a the VAR section: every module variable, pointed out

Admitted: a device's technical state.

TOKENBASES

Purpose: the program-wide token allocation: each partition's count, its base, the total against the kernel's capacity.

Declaration: no roles

(* ECSKIND: TOKENBASES *)

Placement: the program directory.

Imports: the TOKENBASES group of the allow-lists file.

Construct: Implementation, § Tokens, Constructs.

TOKENBASES.R The declaration has no parameters

Precondition. Tool-checked.

a the declaration: no parameter

Admitted: none.

TOKENBASES.X Nothing beyond constants and the token name type is exported

Violation. Tool-checked.

The token name type lives here because a TOKENS module imports nothing but TOKENBASES, so the plan report module stays out of its reach and free of any kind dependency.

a the export list: constants, and at most one type, the token name type

Admitted: none.

TOKENBASES.I Imports are within the allow-list

Violation (a), fact (b). Tool-checked (a), tool-recorded (b).

a the import list against the declared kinds and the TOKENBASES group of the allow-lists file: no program module of any kind; the kernel, for its capacity constant, is the one framework module named there
b the import list: every other imported library module, recorded in the ECS file with the module

For the reviewer, reading b: the error code catalogue is expected and nothing else.

Admitted: none.

TOKENBASES.P The module lies in the program directory

Violation. Tool-checked.

a the module's directory: the program directory itself

Admitted: none.

TOKENBASES.1 Constants, the token name type, an asserting body

Violation.

Which constant is a partition's count, which its base and which the total is not readable without a naming rule the architecture does not impose; the allocation is checked on the evaluated token values instead, TOKENS.3, TOKENS.6 and PROGRAM.3. That the constants are the counts and the running sum they read as, and that the body asserts the total against the kernel's capacity, is read by the reviewer, Part E.

a the declarations: exported constants; at most one exported type, the token name type; no variable, no procedure
b the module body: every statement is an assertion over the module's own constants and the kernel's

Admitted: none.

TOKENNAMES

Purpose: the program-wide token name table, gathered from the partitions' TOKENS modules, for the plan report.

Declaration: <namesvar>

(* ECSKIND: TOKENNAMES Names *)

Placement: the program directory.

Imports: the TOKENNAMES group of the allow-lists file.

Construct: Implementation, § Tokens, Constructs.

TOKENNAMES.R The declaration's parameter is `<namesvar>`, and it exists as an exported variable

Precondition (a, b), violation (c). Tool-checked.

a the declaration: one parameter
b the parameter: an Oberon identifier
c the export list against the declaration: the parameter names an exported variable of the module

Admitted: none.

TOKENNAMES.X Nothing beyond `<namesvar>` is exported

Violation. Tool-checked.

a the export list: <namesvar>, nothing else

Admitted: none.

TOKENNAMES.I Imports are within the allow-list

Violation (a), fact (b). Tool-checked (a), tool-recorded (b).

a the import list against the declared kinds and the TOKENNAMES group of the allow-lists file: every imported program module is of a kind the group names, and every imported framework module is named there
b the import list: every other imported library module, recorded in the ECS file with the module

For the reviewer, reading b: the plan report module is expected, the table being for it; anything else, check what it serves.

Admitted: none.

TOKENNAMES.P The module lies in the program directory

Violation. Tool-checked.

a the module's directory: the program directory itself

Admitted: none.

TOKENNAMES.1 Every partition's names are collected

Observation.

The gathering is form-free, loops, a local procedure, index arithmetic, so it can copy a table over incompletely and leave a valid token without a name. The table serves the plan report alone: a corrupt review instrument, not a wrong program. The plan report prints a cleared entry as the token's number and an undefined one as garbage, so a clearing of the table before the gathering makes a missed token visible at the first run; the clearing is a programming choice. The decidable part is the pair, TOKENNAMES/TOKENS.1.

a the module body and the local procedures it reaches, against the TOKENS modules and TOKENBASES: each partition's whole names table lands at that partition's base, entry by entry; by hand, the gathering statements against each <namesvar>'s length and each base constant

Admitted: none.

CONS

Purpose: the consistency module: the assertions that hold across partitions' definitions, one station of schedule 0's sequence, run before any partition is created in any schedule, so that a failed assertion halts the program before anything exists. One per program.

Declaration: <assertproc>

(* ECSKIND: CONS Assert *)

Placement: the program directory.

Imports: the CONS group of the allow-lists file.

Construct: Implementation, § The Main Program and the Partitions, The Consistency Module.

Assertions between partitions of different schedules are the normal case: two partitions that share a size or a protocol value each declare it, neither importing the other's WIRING or VALUES, and the shared values are those a crossing or a transport connects. With WIRING and VALUES the only program imports and both exporting definition values alone, constants and the variables their bodies assign, every imported operand is a definition value; an assertion over literals or private constants is the programmer's business.

CONS.R The declaration's parameter is `<assertproc>`, and it exists as an exported procedure

Precondition (a, b), violation (c). Tool-checked.

a the declaration: one parameter
b the parameter: an Oberon identifier
c the export list against the declaration: the parameter names an exported procedure of the module

Admitted: none.

CONS.X Nothing beyond `<assertproc>` is exported

Violation. Tool-checked.

a the export list: <assertproc>, nothing else

Admitted: none.

CONS.I Imports are within the allow-list

Violation (a), fact (b). Tool-checked (a), tool-recorded (b).

a the import list against the declared kinds and the CONS group of the allow-lists file: every imported program module is of a kind the group names, from any partition, and every imported framework module is named there
b the import list: every other imported library module, recorded in the ECS file with the module

For the reviewer, reading b: the error code catalogue is expected and nothing else. VALUES.1 is read here: no VALUES constant is an array dimension in the module.

Admitted: none.

CONS.P The module lies in the program directory

Violation. Tool-checked.

a the module's directory: the program directory itself

Admitted: none.

CONS.1 The assert procedure is parameterless

Observation. Tool-checked.

A parameter would let a fact into the consistency check from outside the definitions; one may have its reason, which is stated.

a the procedure heading: <assertproc> takes no parameters

Admitted: a stated reason for the parameter.

That <assertproc> runs at schedule 0's gate, and in no other module, is the pair, SCHEDULE/CONS.1.

BOUNDARY

Purpose: the schedule boundary: the crossings between schedules, declared once for the program.

Declaration: <crossingsvar>

(* ECSKIND: BOUNDARY Crossings *)

Placement: the program directory.

Imports: the BOUNDARY group of the allow-lists file.

Construct: Implementation, § Schedules and the Boundary, The Boundary Module.

BOUNDARY.R The declaration's parameter is `<crossingsvar>`, and it exists as an exported variable

Precondition (a, b), violation (c). Tool-checked.

a the declaration: one parameter
b the parameter: an Oberon identifier
c the export list against the declaration: the parameter names an exported variable of the module

Admitted: none.

BOUNDARY.X Nothing beyond `<crossingsvar>` is exported

Violation. Tool-checked.

a the export list: <crossingsvar>, nothing else

Admitted: none.

BOUNDARY.I Imports are within the allow-list

Violation (a), fact (b). Tool-checked (a), tool-recorded (b).

a the import list against the declared kinds and the BOUNDARY group of the allow-lists file: every imported program module is of a kind the group names, from any partition, and every imported framework module is named there
b the import list: every other imported library module, recorded in the ECS file with the module

For the reviewer, reading b: none is expected; check what it serves.

Admitted: none.

BOUNDARY.P The module lies in the program directory

Violation. Tool-checked.

a the module's directory: the program directory itself

Admitted: none.

BOUNDARY.1 The module body assigns the crossings with constant indices, and every entry is determinate

Violation (a, c), observation (b). Tool-checked.

A loop or a variable index leaves the entry outside the ECS file. The kernel reads every entry of both arrays at SetBoundary and asserts the calling core's diagonal empty; nothing is zeroed at load, so an entry never assigned is a phantom crossing or a failed assertion. The ECS file records the assigned entries and writes the rest empty, so without determinacy the file states a boundary the program does not have. No CLEAR is mandated: every entry assigned satisfies c.

a the module body: every assignment to <crossingsvar> is <crossingsvar>.flow[i, j] := ... or <crossingsvar>.deposit[i, j] := ... with constant i, j
b the module body: every other statement, pointed out
c every entry of both arrays: assigned in the module body, or CLEAR(<crossingsvar>) precedes the first assignment

Admitted: a CLEAR or an assertion among the statements b points out.

BOUNDARY.2 A crossing names surfaces only

Violation. Tool-checked.

a the right sides: every term is a bare surface, a leaf of a TOKENS module's <surfacesvar>; no token in braces

Admitted: none.

BOUNDARY.3 No schedule crosses to itself

Violation, stops at SetBoundary. Tool-checked.

a the indices: i differs from j in every entry

Admitted: none.

Which index is which schedule is the programmer's statement, read by the reviewer against the deployment calls, SCHEDULE/BOUNDARY.1; that each surface exists is the pair, BOUNDARY/TOKENS.1.

Part C. Pairs of Kinds

One section per pair, named by both kinds, the one whose declaration is taken as given first. A pair is read once both kinds are done; the sections stand in the order of the later kind.

SCHEDULE/PERIODS

SCHEDULE/PERIODS.1 The tick is a PERIODS constant

Observation. Tool-checked.

PERIODS is the proposed construct; a tick named otherwise undermines no invariant, and the reason is stated.

a each <gateproc>'s Kernel.Install: the tick argument is a PERIODS constant, one tick constant per schedule

Admitted: a stated reason for the tick's place.

SCHEDULE/PARTITION

SCHEDULE/PARTITION.1 Each partition is created by one schedule and registered by the same

Violation. Tool-checked.

a every <gateproc>: PARTITION.<createproc> is called by exactly one of them, before its Kernel.Begin
b every <gateproc>: <addsystemsproc> is called by the same one, between its Kernel.Begin and Kernel.Plan, once

Admitted: none.

SCHEDULE/PARTITION.2 Only PARTITION modules are created

Violation. Tool-checked.

a every <gateproc> against the declarations: every <createproc> and <addsystemsproc> call targets a module declared PARTITION whose declaration names those procedures

Admitted: none.

PERIODS/PARTITION

PERIODS/PARTITION.1 A registration's period is a PERIODS constant

Observation. Tool-checked.

a PARTITION.<addsystemsproc>: the period argument of every Kernel.AddSystem is a PERIODS constant

Admitted: a stated reason for the period's place.

PARTITION/STATE

PARTITION/STATE.1 The build procedure is called from its own partition's create procedure only

Violation. Tool-checked.

a all call sites of STATE.<buildproc>: exactly one in the program, in its PARTITION's <createproc>

Admitted: none.

PARTITION/STATE.2 Every store leaf has an initialisation site in the create procedure

Violation. Tool-checked.

The STATE module assigns nothing, STATE.3; the sites lie in the partition's <createproc>. A necessary condition, as LOCKED.3: a leaf without a site is uninitialised, since nothing is zeroed at load; a leaf with a site is read by the reviewer, Part E. The parameter mode is read from the callee's procedure heading, through the import alias; for a library procedure without source the mode is unknowable and the actual counts as a site, a miss rather than a false finding. A local procedure that takes the record or a part of it as a VAR parameter is followed with the actual's path in place of the formal's path.

a the record types against <createproc> and the local procedures it reaches: every leaf of the store record, through nested records and arrays, appears at least once in a position that can write it, through <storevar> or a local assigned from it: the left side of :=, the actual of a VAR parameter, a device's read into the store included, or the operand of CLEAR, the leaf itself or an enclosing record or array; array indices are abstracted, S.a[i].x covers the path a[].x

Admitted: none.

STATE/TOKENS

STATE/TOKENS.1 The tokens mirror the store

Violation. Tool-checked.

a both leaf lists: the leaves of TOKENS.<tokensvar> and the leaves of STATE.<storevar>'s record correspond one to one, names verbatim, structure verbatim

Admitted: none.

PARTITION/SYSTEM

PARTITION/SYSTEM.1 The registration names the declared roles

Violation. Tool-checked.

The pair side of PARTITION.2-a: the SYSTEM module's declaration is the authority for the names the registration passes.

a each Kernel.AddSystem call against the named module's declaration: run, manifest and name are its declared <runproc>, <manifestvar> and <namevar>

Admitted: none.

SYSTEM/TOKENS

SYSTEM/TOKENS.1 Manifest references resolve

Violation. Tool-checked.

That a foreign module's tokens appear through its surfaces only is SYSTEM.7, which reads the manifest assignment with every other reference.

a the manifests against the TOKENS modules: every braced token is a declared token of a TOKENS module; every bare surface a declared surface

Admitted: none.

SYSTEM/STATE

SYSTEM/STATE.1 Every store variable the code touches is in the manifest

Violation. Tool-checked.

a <runproc>, the procedures it reaches and the adapter procedures it calls, against the manifest: each <storevar>.<path> reference maps to a token of the manifest, through the mirror, STATE/TOKENS.1

Admitted: none.

SYSTEM/STATE.2 Access direction matches the manifest set

Violation. Tool-checked.

a <runproc> against the manifest: a written store variable is in O, P or Px; a read one in C, Cp or Cx
b <runproc> against the manifest: a Cp token is never written

Admitted: none.

SYSTEM/STATE.3 Every manifest token is touched

Observation. Tool-checked.

a <runproc> against the manifest: each token of the manifest is reached in the code, directly or through an adapter, or through a declared library callback

Admitted: a token reached through a library callback, the callback named.

SYSTEM/STATE.4 Transport access flows through the adapter

Violation. Tool-checked.

a <runproc>: a store variable of a transport's type is reached through the adapter procedure of its direction, never by direct store access, in whatever manifest set it is declared

Admitted: none.

The storage kind decides the route, not the manifest set: a transport is reached through its adapter under produced and consumed as under deposited and collected, and a plain Component is reached directly under either. The tally an adapter records beside a transport access is a plain Component: the adapter's write is a direct write on the calling System's behalf, ADAPTER.4, and the collector's read is a direct read. A store variable is of a transport's type when its type, resolved through the STATE module's own type declarations, names a type of a transport module, a declared library transport included.

A procedure-typed formal that receives an adapter's procedure of the wrong direction does not compile: procedure-type compatibility includes the parameter modes, which are the direction, ADAPTER.3. The pair SYSTEM/ADAPTER has no check-point.

STATE/ADAPTER

STATE/ADAPTER.1 The adapter's store paths are store variables

Violation. Tool-checked.

The pair side of ADAPTER.1-b: the STATE's record is the authority for the paths.

a the adapter's store references against the store record: every <path> reached is a store variable

Admitted: none.

TOKENS/ADAPTER

TOKENS/ADAPTER.1 Every reached store path has a token

Violation. Tool-checked.

a the adapter's procedures against TOKENS: each store variable an adapter procedure reaches translates to a token of the partition's TOKENS module

Admitted: none.

TRANSPORT/ADAPTER

TRANSPORT/ADAPTER.1 The adapter's transport is declared and imported

Violation. Tool-checked.

a the ADAPTER's declaration against the named module's declaration: the parameter names a module declared under a transport kind, in the tree or the library
b the import list: the adapter imports it

Admitted: none.

TRANSPORT/ADAPTER.2 Procedure modes agree with the transport's

Violation. Tool-checked.

a both modules, for a transport in the tree: the adapter's put calls the transport's put with the same modes, and so on for every procedure

Admitted: none.

TOKENBASES/TOKENS

TOKENBASES/TOKENS.1 The partition's tokens are allocated from its base

Violation. Tool-checked.

Which constant is the partition's count is not readable without a naming rule; the count is asserted by the TOKENS body, TOKENS.6, and proven by the ranges, PROGRAM.3.

a the leaves' expressions against TOKENBASES: each reaches exactly one TOKENBASES constant, the same for all leaves

Admitted: none.

TOKENNAMES/TOKENS

TOKENNAMES/TOKENS.1 Every partition's names are referenced

Violation. Tool-checked.

A necessary condition: a table referenced nowhere is not gathered. How the body gathers is its own, and where each name lands is TOKENNAMES.1.

a TOKENNAMES' body and the local procedures it reaches, against the TOKENS declarations: every declared <namesvar> is referenced

Admitted: none.

SCHEDULE/CONS

SCHEDULE/CONS.1 `<assertproc>` runs at schedule 0's `<gateproc>`

Violation. Tool-checked.

The consistency station comes first: a program whose definitions disagree has no business starting another core or creating anything. That no other module imports CONS is the schedule 0 only qualifier of the SCHEDULE group, SCHEDULE.I.

a schedule 0's <gateproc>: it calls CONS.<assertproc> once, as its first statement, before the deployment calls and before Kernel.Install

Admitted: none.

SCHEDULE/BOUNDARY

SCHEDULE/BOUNDARY.1 The boundary is set and its indices are schedules

Violation. Tool-checked.

Which index is which schedule is the programmer's statement, read by the reviewer against the deployment calls.

a every <gateproc> of a program of two or more schedules: it passes BOUNDARY.<crossingsvar> to Kernel.SetBoundary; a program of one schedule crosses nothing and sets no boundary, PROGRAM.2-a
b BOUNDARY's indices against the program's schedule count: every crossing index lies in 0 to n-1, n the number of schedules, PROGRAM.1-c

Admitted: none.

BOUNDARY/TOKENS

BOUNDARY/TOKENS.1 Every crossing surface exists

Violation. Tool-checked.

a BOUNDARY's body against the TOKENS modules: each surface term of a crossing resolves to a leaf of a TOKENS module's <surfacesvar>

Admitted: none.

Part D. The Program as a Whole

Check-points over all modules of one kind, or over the program, read once after Parts B and C. Several are the kernel's own plan checks seen statically; each of these carries its stop.

PROGRAM.1 Schedules are dense, one per core, started once

Violation (a, b), fact (c). Tool-checked (a), tool-recorded (c).

A deployment is read as the passing of a SCHEDULE's exported <gateproc> as a procedure actual, without knowing the callee. The core lives in the deployment procedure's name or arguments, which the reviewer knows and the tools do not; the kernel equates schedule and core.

a all SCHEDULE modules: schedule 0 is the main module; every other SCHEDULE module's <gateproc> is passed as a procedure actual exactly once, in another SCHEDULE module
b the deployment calls: the cores so used are distinct
c the schedules: the main module and the started ones, n in all, listed in the ECS file, schedule 0 numbered, the others by module with their deployment call as written; the crossing indices range over 0 to n-1, SCHEDULE/BOUNDARY.1-b

Admitted: none.

PROGRAM.2 The singletons are single

Violation. Tool-checked.

The PARTITION module's count is PARTITION.P-b: a directory is a partition directory because it holds exactly one, so counting it here would be circular.

a the declared kinds by directory: at most one PERIODS, RESOURCES, TOKENBASES, TOKENNAMES and CONS module in the program, and exactly one BOUNDARY module in a program of two or more schedules; a program of one schedule crosses nothing and declares none
b the declared kinds by directory: exactly one STATE and TOKENS module per partition directory; at most one LOCKED, WIRING and VALUES

Admitted: none.

PROGRAM.3 Token ranges are disjoint and gapless over the program, and the total fits the kernel

Violation. Tool-checked.

a all TOKENS modules' evaluated ranges, base to base plus count less one: they do not overlap and leave no gap from 0 to the total
b the total against the kernel's constant: not above Kernel.MaxTokens

Admitted: none.

PROGRAM.4 Single writer

Violation, stops at Plan. Tool-checked.

a all manifests: no token is in O or P of two Systems

Admitted: none.

PROGRAM.5 A token is dataflow or deposit, never both

Violation, stops at Plan. Tool-checked.

a all manifests: a token is a dataflow token, in O, P, C or Cp, or a deposit token, in Px or Cx, never both

Admitted: none.

PROGRAM.6 Owned is private

Violation, stops at Plan. Tool-checked.

a all manifests: no token in a System's O appears in any other System's C or Cp

Admitted: none.

PROGRAM.7 Produced is consumed, consumed is produced

Violation, stops at Plan. Tool-checked.

The kernel's check is relaxable; the tools report each gap whatever the waiver, and the reviewer matches the gaps to the relaxed set read from <gateproc>, SCHEDULE.4.

a all manifests: every P token is in some C or Cp
b all manifests: every C or Cp token is in some P

Admitted: a gap covered by a waiver, SCHEDULE.4.

PROGRAM.8 Deposits are collected

Violation, stops at Plan. Tool-checked.

Relaxable, as PROGRAM.7.

a all manifests: every Px token is in some Cx

Admitted: a gap covered by a waiver, SCHEDULE.4.

PROGRAM.9 Acyclic

Violation, stops at Plan. Tool-checked.

a the dependency graph over P and C edges, with Cp edges reversed: no cycle

Admitted: none.

PROGRAM.10 No token written in two schedules

Violation, a stops at Commit. Tool-checked.

a all manifests with their schedules: no O or P token in Systems of two schedules
b all manifests with their schedules: no Px token deposited from two schedules

Admitted: none.

PROGRAM.11 Every crossing is real and oriented

Violation, b stops at Commit. Tool-checked.

a BOUNDARY against the manifests and the registrations: for every crossing [i, j] surface, its producers' Systems run in schedule i and its consumers' in schedule j
b every crossing token: a counterpart System exists in another schedule
c every crossing token: it is reached through an adapter

Admitted: none.

PROGRAM.12 Every token appears in a manifest

Observation.

A token in no manifest is a store variable no System reads or writes.

a each token of each TOKENS module against all manifests: in at least one manifest of the program

Admitted: a store variable kept for a System not yet written, with the reason stated.

The role names are not a check-point: the ECS file's role names section shows the majority name of each role and the overrides, and a module with its own line is visible there.

Part E. Read by a Person Only

Facts not in the code or not decidable from it. The review reads them; no tool does.

Previous-value consumption. A Cp declaration says the System reads the last pass's value and runs before the producer. Whether the logic is correct under a one-pass-old value, and what the value is at the first pass, is the control question.
Initial values. PARTITION/STATE.2 and LOCKED.3 see an assignment site per leaf, not that it executes nor what it writes. The loop that stops one short, the branch around the assignment, the device procedure that leaves a field untouched, and the value itself are read here, with the first-pass question above.
The periods and the rate test. Every System period is counted in the ticks of the schedule it runs on; every tick-denominated value crossing the boundary is denominated in the consumer's tick. The rate test: change one schedule's tick and nothing else; every period re-derives to the same milliseconds, and the plant behaviour does not change.
The adapter's policy. What an adapter does when the precondition fails, and what it records, ADAPTER.4.
The boundary's preflight. That the crossings are the whole set, and that a value crossing by sampling tolerates the delay, is read from the manifests before the boundary is written.
The authored facts against reality. Units, pins, priorities, the memory map, the console unit: against the reference manual and the schematic.
The token allocation's arithmetic. That the TOKENBASES constants are the counts and the running sum they read as, and that the module body asserts the total against the kernel's capacity. The tools prove the allocation on the values, TOKENS.3, TOKENS.6 and PROGRAM.3, not on the constants' meaning.
The names table. TOKENNAMES.1: the plan report prints the names beside the token numbers, so a misplacement shows at the first run, and a missed name shows as the bare number where the table is cleared first.
Run to completion. SYSTEM.5.
No caching below the store. OTHER and BINDING modules, over the variables OTHER.1 and BINDING.1 point out: a synchronous helper or binding holds nothing between calls beyond a device's technical state behind its device handle; an asynchronous binding holds transfer state only, a single-producer single-consumer queue, the interrupt one side and the System's call the other, each item consumed once, the protocol's indices beside it, no lock. The one test: can a second call obtain what a first one already obtained? A queue says no, a cache says yes. A stateful helper imported by two Systems is a channel beside the store. A violation.
The module body rule. A body initialises the module's own memory, never hardware; the bring-up is the exception, and which modules are the bring-up is a role the tools cannot know. The kinds' check-points pin the module bodies the ECS file reads; a transport, OTHER, BINDING or PARTITION body is read by eye against the rule.
Content. Names, header text, the logic inside <runproc>, the order of registration: authored freedom. The run order is derived; registration order means nothing.

Legitimate gaps are recorded as such, never as findings: a coverage gap the reviewer matches to a waiver read from <gateproc>, SCHEDULE.4, and a generated skeleton, the kind shapes present and the content not yet written, which is built before it is checked like any program. A tree without build products is not a gap for the tools: they refuse it, and the rebuild is the check. For the review by hand a deep-cleaned tree is reviewed from its sources, and the precondition check-points do not apply.

Tool Support

The tools hold the check-points marked Tool-checked or Tool-recorded: extract-ecs reads the build, the declarations and the facts and writes the ECS file; check-ecs prints the findings. Each prints a finding with the check-point's identifier as its first field and the position in the sources, so a finding is read against this guide by its identifier. The tools are described in their own pages, extract-ecs and check-ecs.

ECS for Control: Review Guide

Overview

Preparation

Terminology

Part A. Every Module, Before Its Kind

MODULE.1 The program is linked

MODULE.2 The module list is the map

MODULE.3 Every module is compiled as it stands

MODULE.4 Every module is compiled against current interfaces

MODULE.5 The link products are built from everything

ECSKIND.1 Exactly one kind declaration

ECSKIND.2 The kind is in the vocabulary

Part B. Each Module Against Its Kind

SCHEDULE

SCHEDULE.R The declaration's parameter is <gateproc>, and it exists as a procedure

SCHEDULE.X Nothing beyond <gateproc> is exported

SCHEDULE.I Imports are within the allow-list

SCHEDULE.P The module lies in the program directory

SCHEDULE.1 Every <gateproc> is parameterless; schedule 0's is local and called from the module body, every other schedule's is exported and started by its deployment call alone

SCHEDULE.2 <gateproc> runs the station sequence in order

SCHEDULE.3 A deployment call starts a <gateproc>

SCHEDULE.4 No waiver is in force

PERIODS

PERIODS.R The declaration has no parameters

PERIODS.X Nothing beyond constants and the variables the module body assigns is exported

PERIODS.I Nothing is imported

PERIODS.P The module lies in the program directory

RESOURCES

RESOURCES.R The declaration has no parameters

RESOURCES.X Nothing beyond constants is exported

RESOURCES.I Imports are within the allow-list

RESOURCES.P The module lies in the program directory

PARTITION

PARTITION.R The declaration's parameters are <createproc> and <addsystemsproc>, and both exist as exported procedures

PARTITION.X Nothing beyond the two procedures is exported

PARTITION.I Imports are within the allow-list

PARTITION.P The module lies in its own partition directory

PARTITION.1 Both procedures are parameterless

PARTITION.2 The registration procedure registers each System once, with its declared roles

WIRING

WIRING.R The declaration has no parameters

WIRING.X Nothing beyond constants is exported

WIRING.I Imports are within the allow-list

WIRING.P The module lies in its partition's directory

VALUES

VALUES.R The declaration has no parameters

VALUES.X Nothing beyond constants and the variables the module body assigns is exported

VALUES.I Imports are within the allow-list

VALUES.P The module lies in its partition's directory

VALUES.1 A VALUES constant is never an array dimension

STATE

STATE.R The declaration's parameters are <storevar> and <buildproc>, and each exists with its sort

STATE.X Nothing beyond the two roles and the module's types is exported

STATE.I Imports are within the allow-list

STATE.P The module lies in its partition's directory

STATE.1 The store variable points to a store record declared here; the build procedure is parameterless

STATE.2 The store holds values and handles only

STATE.3 The build procedure allocates the store and nothing else

STATE.4 The store's array lengths are WIRING constants

STATE.5 Nothing runs or is declared beside the store type, the store variable and the build procedure

LOCKED

LOCKED.R The declaration's parameters are <lockedvar> and <interfacevar>, and each present one is an exported variable

LOCKED.X Nothing beyond the two variables and the module's types is exported

LOCKED.I Imports are within the allow-list

LOCKED.P The module lies in its partition's directory

LOCKED.1 Both are record variables, not pointers

LOCKED.2 Written in the module body only

LOCKED.3 Every locked leaf has an initialisation site

TOKENS

TOKENS.R The declaration's parameters are the three roles, and each present one is an exported variable

TOKENS.X Nothing beyond the three variables is exported

TOKENS.I Imports are within the allow-list

TOKENS.P The module lies in its partition's directory

TOKENS.1 The tokens variable is a record of INTEGER leaves

TOKENS.2 Every token is assigned once, a constant expression

TOKENS.3 The ordinals are dense from the base

TOKENS.4 A surface is a braced set of the module's own tokens

TOKENS.5 Every token has a name

TOKENS.6 The back-assert holds

SYSTEM

SCHEDULE.R The declaration's parameter is `<gateproc>`, and it exists as a procedure

SCHEDULE.X Nothing beyond `<gateproc>` is exported

SCHEDULE.1 Every `<gateproc>` is parameterless; schedule 0's is local and called from the module body, every other schedule's is exported and started by its deployment call alone

SCHEDULE.2 `<gateproc>` runs the station sequence in order

SCHEDULE.3 A deployment call starts a `<gateproc>`

PARTITION.R The declaration's parameters are `<createproc>` and `<addsystemsproc>`, and both exist as exported procedures

STATE.R The declaration's parameters are `<storevar>` and `<buildproc>`, and each exists with its sort

LOCKED.R The declaration's parameters are `<lockedvar>` and `<interfacevar>`, and each present one is an exported variable

TOKENNAMES.R The declaration's parameter is `<namesvar>`, and it exists as an exported variable

TOKENNAMES.X Nothing beyond `<namesvar>` is exported

CONS.R The declaration's parameter is `<assertproc>`, and it exists as an exported procedure

CONS.X Nothing beyond `<assertproc>` is exported

BOUNDARY.R The declaration's parameter is `<crossingsvar>`, and it exists as an exported variable

BOUNDARY.X Nothing beyond `<crossingsvar>` is exported