Laws and objects
A law is a predicate the kernel checks on every change to a resource, whoever proposed it. Objects, activities and seats build on that rule. All of what follows is compiled and proved in Lean; none of it is reachable from a Host operation yet unless a row says so.
Three things called law
- A cell law is a decidable predicate over a write's old and new state and its request. It is the judge of admission.
- A
lawin.obendis a property of a specification's methods, kept as a closure in its metadata. Nothing discharges it and it never reaches admission. requiresnames a member a specification needs from its final self. It is not a precondition, and it is recorded, not checked.
Rules for admission written in .obend (invariant, guard,
permit, forbid) are a design, not built: a program cannot yet state the
law of its own object.
Which code wrote
Every law state begins with the slot objective/artifact. For a command with an
Objective claim it holds the claimed method's identity; for any other command it holds
-1. A clause objectivePin accepts only steps whose slot names a pinned
artifact, so an ordinary command is refused whatever its writes. No turn installs that clause at
object birth yet.
Objects
A cell is an object to the kernel only if it has a record: its package pin, its law, an upgrade policy and a payer. A birth on a cell without a record is refused, and so is a birth of any package but the pinned one. Every write to an object's declared state, from a birth, a resume or a direct write, is judged by the object's law over the old and new state. A resumed activity's write is judged as its birth subject, never as whoever delivered the response. A refusal names the failing clause and commits nothing.
Activities
An activity is a persisted checkpoint plus one await. Its reply slot has one decider and one deadline, decided once. A resume delivers the settled outcome together with the object's state and version read in the same turn, so no write is computed from a stale read. An await that exhausts its declared envelope is a paid turn; an ended activity leaves an empty tombstone; anyone may abandon an await after its deadline plus a grace, which returns the purse minus the timeout fee. One public tariff prices every declared envelope, for native admission and for activities.
Seats
A seat holds one side of a contract in its own Book account. Its law is offer safety: every want is met, or every give is refunded. The law is judged on every reallocation, and the offerer's exit is a kernel action no contract clause is consulted for.
Where each stands
| Part | Evidence | Landed | Journey row |
|---|---|---|---|
| Native Objective admission (signed invocation, receipt, refusals) | integrated on scratch worlds | 6df4602f, 73223088, a2454432 | objective PASS, 17 rows at main 4795b657 |
| Law slot and the pin clause | compiled, proved | 2a7c372b | none |
| Object record, law on every state write | compiled, proved; no Host operation | eac4b18c, de9c84f7 | none (a row is queued) |
| Activities: records, slots, resume with view, paid exhaustion, abandonment | compiled, proved; no Host operation | 8194e09d, 67362781, d1ce7b0c | activity ABSENT: no driver |
| One public tariff | compiled, proved; in the Host | bf28dd19 | objective (prices the claim) |
| Seats and invitations | compiled, proved; no Host operation | 6347dcb4 | seats ABSENT: no driver |
In flight, by lane: the signed route for activities, seats on the native route, a storage charge for packages and checkpoints, record upgrades, the turn gate, and the receiver that pins an object's law to its package.
Objects, activities and seats in the language guide, the kernel activity and seats: each theorem and its line.