Repository navigation
fix(gate): re-prove authority at the commit point (gauntlet revoke-during-spend) #18
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
base: main
Are you sure you want to change the base?
Changes from all commits
ee4c5f5
72e0bc1
5853f51
f2742a9
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -11,8 +11,10 @@ | |
| facade and live, no gating fault on the lease's resource. | ||
| """ | ||
|
|
||
| import inspect | ||
| from collections.abc import Callable, Iterator | ||
| from contextlib import contextmanager | ||
| from typing import TypeVar | ||
|
|
||
| from interlock._errors import ( | ||
| EStopEngaged, | ||
|
|
@@ -23,12 +25,14 @@ | |
| LeaseRevoked, | ||
| ) | ||
| from interlock.claims import Claim | ||
| from interlock.estop import EStop | ||
| from interlock.estop import EStop, InFlightGate | ||
| from interlock.faults import FaultBus | ||
| from interlock.interfaces import REGISTRY, InterfaceRecord, declare | ||
| from interlock.leases import Lease, LeaseManager | ||
| from interlock.ledger import Ledger | ||
|
|
||
| T = TypeVar("T") | ||
|
|
||
| __version__ = "0.1.0" | ||
|
|
||
| __all__ = [ | ||
|
|
@@ -60,9 +64,10 @@ def __init__( | |
| clock: Callable[[], float] | None = None, | ||
| ledger: Ledger | None = None, | ||
| ) -> None: | ||
| self.leases = LeaseManager(clock) | ||
| self.estop = EStop() | ||
| self.faults = FaultBus() | ||
| self._gate = InFlightGate() | ||
| self.leases = LeaseManager(clock, gate=self._gate) | ||
| self.estop = EStop(self._gate) | ||
| self.faults = FaultBus(gate=self._gate) | ||
| self.ledger = ledger if ledger is not None else Ledger() | ||
|
|
||
| def grant( | ||
|
|
@@ -92,24 +97,15 @@ def grant( | |
| ) | ||
| return lease | ||
|
|
||
| @contextmanager | ||
| def permit(self, lease: Lease, action: str, target: str) -> Iterator[Lease]: | ||
| """Permit exactly one action on one target, checking in order: | ||
|
|
||
| 1. e-stop clear → else :exc:`EStopEngaged` | ||
| 2. lease issued by this facade's manager and unaltered → else | ||
| :exc:`LeaseNotIssued`; then live (unrevoked, unexpired) → else | ||
| :exc:`LeaseRevoked` or :exc:`LeaseExpired` | ||
| 3. no gating fault on the lease's resource → else :exc:`FaultActive` | ||
|
|
||
| Permits and denials are appended to the ledger. | ||
| """ | ||
| def _check(self, lease: Lease, action: str, target: str, phase: str) -> dict: | ||
| """Run the gate in order; log and raise on the first failure.""" | ||
| base = { | ||
| "lease_id": lease.id, | ||
| "holder": lease.holder, | ||
| "resource": lease.resource, | ||
| "action": action, | ||
| "target": target, | ||
| "phase": phase, | ||
| } | ||
| try: | ||
| self.estop.assert_clear() | ||
|
|
@@ -130,8 +126,93 @@ def permit(self, lease: Lease, action: str, target: str) -> Iterator[Lease]: | |
| if self.faults.gating(lease.resource): | ||
| self.ledger.append("denials", {**base, "reason": "fault"}) | ||
| raise FaultActive(f"gating fault active on {lease.resource}") | ||
| return base | ||
|
|
||
| @contextmanager | ||
| def permit(self, lease: Lease, action: str, target: str) -> Iterator[Lease]: | ||
| """Permit exactly one action on one target, checking in order: | ||
|
|
||
| 1. e-stop clear → else :exc:`EStopEngaged` | ||
| 2. lease issued by this facade's manager and unaltered → else | ||
| :exc:`LeaseNotIssued`; then live (unrevoked, unexpired) → else | ||
| :exc:`LeaseRevoked` or :exc:`LeaseExpired` | ||
| 3. no gating fault on the lease's resource → else :exc:`FaultActive` | ||
|
|
||
| Permits and denials are appended to the ledger. | ||
|
|
||
| ``permit()`` checks at block entry only: it cannot stop an effect the | ||
| caller performs later inside the block. For irreversible effects use | ||
| :meth:`execute`, which re-proves the gate at the commit point. If the | ||
| e-stop engages or the lease is revoked while the block runs, a | ||
| ``violations`` record is appended on exit so the gap is never silent. | ||
| An engagement counts even if the e-stop was released again before | ||
| the block exited — the exit check compares engagement counts, not | ||
| the final state. | ||
| """ | ||
| base = self._check(lease, action, target, phase="entry") | ||
| self.ledger.append("permits", base) | ||
| yield lease | ||
| engagements = self.estop.engagements | ||
| try: | ||
| yield lease | ||
| finally: | ||
| reason = None | ||
| if self.estop.engagements != engagements: | ||
| reason = "estop" | ||
|
Comment on lines
+158
to
+160
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
If an e-stop is engaged and then deliberately released before the Useful? React with 👍 / 👎. |
||
| elif self.leases.is_revoked(lease): | ||
| reason = "lease_revoked" | ||
| if reason: | ||
| self.ledger.append("violations", {**base, "reason": reason}) | ||
|
|
||
| def execute(self, lease: Lease, action: str, target: str, effect: Callable[[], T]) -> T: | ||
|
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
The new safe API is absent from the README and quickstart, which still instruct users to perform effects inside Useful? React with 👍 / 👎. |
||
| """Run ``effect`` only if the gate is clear at the commit point. | ||
|
|
||
| Fail-closed: the gate (e-stop, lease issued/live/unrevoked, faults) is | ||
| checked and the effect registered as in flight atomically, under the | ||
| same lock :meth:`EStop.engage` and :meth:`LeaseManager.revoke` take. | ||
| Either the halt lands first and the effect never starts, or the effect | ||
| started first and the halt call waits for it to finish. Any error in | ||
| the check refuses the effect. | ||
|
|
||
| ``effect`` must run to completion synchronously. A coroutine, | ||
| generator, or async generator is deferred work: calling it starts | ||
| nothing, so the gate cannot hold it in flight. Deferred callables | ||
| are refused with :exc:`TypeError` before the gate runs, and a | ||
| deferred result returned by a plain callable is closed unstarted | ||
| and refused the same way — never left to run after a halt returns. | ||
| """ | ||
| if ( | ||
| inspect.iscoroutinefunction(effect) | ||
| or inspect.isgeneratorfunction(effect) | ||
| or inspect.isasyncgenfunction(effect) | ||
| ): | ||
| raise TypeError( | ||
| "execute() effect must be a plain synchronous callable; " | ||
| "async and generator effects are refused" | ||
| ) | ||
| registered = False | ||
| try: | ||
| with self._gate.cond: | ||
| base = self._check(lease, action, target, phase="commit") | ||
| self._gate.enter(lease.id) | ||
| registered = True | ||
| self.ledger.append("permits", base) | ||
| result = effect() | ||
| if ( | ||
| inspect.iscoroutine(result) | ||
| or inspect.isgenerator(result) | ||
| or inspect.isasyncgen(result) | ||
|
Comment on lines
+201
to
+203
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
When a plain effect returns a custom object implementing Useful? React with 👍 / 👎. |
||
| ): | ||
| close = getattr(result, "close", None) | ||
| if close is not None: | ||
| close() | ||
| raise TypeError( | ||
| "execute() effect returned deferred work (coroutine or generator); " | ||
| "it was closed unstarted and refused" | ||
| ) | ||
| return result | ||
| finally: | ||
| if registered: | ||
| self._gate.leave(lease.id) | ||
|
|
||
| def claim( | ||
| self, | ||
|
|
||
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Running the README example as shown raises
NameErrorbecauseeffectis never defined, so the newly documented commit-point path cannot reach the gate. Define a concrete function or use a self-contained lambda as the detailed quickstart does.Useful? React with 👍 / 👎.