Snapshot-view contract

The snapshot-view contract is an operational runtime monitor. It reports selected hazards at AMBER’s instrumented read/write seams, such as a borrow after a same-step commit. It does not prove that arbitrary NumPy/CuPy code or a private GPU kernel preserves every intended activation schedule. Run with a contract mode and inspect the per-step records:

results = model.run(steps=100, contract="check")   # "off" | "check" | "warn" | "raise"
for cert in results["contract"]:
    if not cert.ok:
        print(cert.step, cert.violations)

check records a ContractCertificate per step; warn also emits a warning per violation; raise stops on the first one. Mode off (the default) adds no monitor bookkeeping. Contract modes apply under both model.cpu(...) and model.gpu() on the instrumented general runner. An optional private GPU fast loop is selected only with contract="off" and an explicit per-instance deployment declaration such as model.approve_fast_path("smoke-report-2026-07"). The string is a caller-supplied provenance label, not evidence AMBER verifies. Without that declaration the general native runner is used. The private loop is not monitored. cert.clean means no monitored error or warning was observed; it is not a completeness or confluence claim.

Write paths the monitor sees

• Buffered (OOP) – agent.col = value / Model._queue_write (per-cell duplicate detection).

• Lane / view – agents.col = ..., agents.set(...), agents.commit(...), and TensorLane commits (per-column commit counting + borrow-after-commit).

• Mutable raw arrays – agents.array(...) records uncertified_mutable_borrow because later indexing and in-place mutations cannot be reconstructed reliably.

• Cross-path – the same column written via both OOP and lane/view in one step (cross_path_write).

scatter_add is the sanctioned multi-write reducer and is not counted as an ordinary lane/view commit.

Prefer those APIs over assigning population.data directly: direct frame replacement is deprecated and remains outside the write-conflict seam, although endpoint schema/id changes can still be reported.

Runtime bookkeeping lives in ContractMonitor; Model only owns the thin write seams (_queue_write, _set_frame(..., written_columns=...), run_step).

Runtime conformance checking for AMBER’s snapshot-view contract.

This module turns simultaneous-update discipline into a falsifiable per-step artifact. A ContractCertificate reports conflicts observed at AMBER’s read/write seams; it is a runtime diagnostic, not a proof that arbitrary user array code is schedule-independent.

It witnesses violations on two write paths:

• the buffered (OOP) path – per-agent Agent.__setattr__ writes routed through Model._queue_write; and

• the vectorized lane/view path – whole-column writes via agents.col = ... / agents.commit(...) / TensorLane, which bypass _queue_write but report commits to ContractMonitor.

The checks:

• duplicate unreduced write – the same (column, agent_id) cell received more than one ordinary (non-scatter) write within a step (buffered path), or the same column was committed more than once within a step (lane/view path). Under simultaneous activation the later write silently clobbers the earlier one (a “partial map” conflict). The sanctioned fix is a commutative reducer (agents.at[ids].scatter_add(col=delta)) or committing each column once.

• cross-path write – the same column received both a buffered (OOP) write and a whole-column lane/view commit within one step. The flush order makes the later path win; under simultaneous activation that is still a partial-map conflict.

• read-after-write (lane path) – a column borrowed after it was committed in the same step; a snapshot rule must read step-entry state.

• uncertified mutable borrow – agents.array(...) exposed a mutable NumPy/CuPy buffer. AMBER observes the borrow, but cannot infer whether or how user code subsequently mutates or indexes that raw array.

• schema / population mutation – the column set, a column’s dtype, or the agent id-set changed between step entry and exit, so reads issued during the step no longer see a stable snapshot. Column/population additions and births/deaths are reported as warnings; column removal and dtype change are errors.

This is a conformance monitor, not a prover, with two known limits: (1) the schema/population diff is endpoint-only – a mutation that is introduced and reverted within a single step is not caught; (2) raw population.data = ... writes that bypass both _queue_write and the reported lane/view seams are invisible to the conflict check (Population.data = ... is deprecated and warns; prefer agents.col = ... / agents.set / agents.commit). Cell-level dependency and commutativity reasoning remains the job of model analysis or tests; a clean certificate is evidence only for the operations the runtime seams can observe.

ambr.contract.CONTRACT_MODES = ('off', 'check', 'warn', 'raise')

Valid values for Model.run(contract=...).

class ambr.contract.ContractCertificate(step: int)

Bases: object

Per-step record of contract conformance.

ok is True when no error-severity violations were found (warnings do not flip it). clean is True only when there are no violations of any severity.

add(violation: ContractViolation) → None

property clean: bool

errors() → List[ContractViolation]

property ok: bool

violations: List[ContractViolation]

warnings() → List[ContractViolation]

class ambr.contract.ContractMonitor

Bases: object

Per-model runtime monitor for the snapshot-view contract.

Owns per-step bookkeeping and certificate construction so Model only needs a thin seam (_queue_write, view/lane commits, run_step).

active: bool

begin_step(snapshot: Tuple[Dict[str, str], Set[Any]]) → None

Arm tracking for a step body; snapshot is step-entry state.

certificates: List[ContractCertificate]

end_step(step: int, snapshot: Tuple[Dict[str, str], Set[Any]]) → ContractCertificate

Disarm tracking and return the certificate for step.

mode: str

record_borrow(column: str) → None

Record a lane borrow of column; flag if already committed.

record_buffered_write(column: str, agent_id: Any) → None

Count an ordinary OOP-path write; second write to a cell is a conflict.

record_commit(columns: Iterable[str]) → None

Record a whole-column lane/view commit of columns this step.

record_mutable_borrow(column: str) → None

Record raw mutable array access that cannot be fully traced.

record_reduction(columns: Iterable[str]) → None

Record a sanctioned commutative reduction write.

Repeated reductions are not duplicate-write errors, but mixing a reduction with an ordinary write to the same column remains ambiguous and is reported as a cross-path conflict.

reset_run(mode: str) → None

Configure mode for a new Model.run and clear prior certificates.

class ambr.contract.ContractViolation(kind: str, detail: str, severity: str = 'error', columns: Iterable[str] | None = None, ids: Iterable[Any] | None = None)

Bases: object

A single admissibility violation observed during one step.

columns: List[str]

ids: List[Any]

exception ambr.contract.ContractViolationError(certificate: ContractCertificate)

Bases: RuntimeError

Raised by Model.run(contract='raise') on the first non-conforming step.