docs: S0 draft — single 0.5-cell bound, hold steps carry no translational wall velocity

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This commit is contained in:
Claude
2026-10-30 06:22:44 +00:00
co-authored by Claude Opus 5.5
parent 421b90f5d2
commit adbed8ae7e
+12 -8
View File
@@ -101,21 +101,24 @@ fluid pull from a solid slot of a moving body is BFL-written.
### 4a. Applied geometry vs pending target (CANDIDATE, narrow API)
Two distinct facts per moving body, one authority each:
`applied` = offset (and velocity) of the geometry last applied on the device,
changed only by a successful commit; `pending` = an optional requested target
`applied` = offset of the geometry last applied on the device, changed only
by a successful commit; `pending` = an optional requested target
`(offset, velocity)`, changed only by `set_body`. A setter returning proves
nothing about the device. The uploaded motion record is derived each run:
`{c_old = base + applied.offset, c_new = base + (pending or applied).offset,
u = (pending or applied).velocity}`. One moving step consumes one target.
`{c_old = base + applied, c_new = base + (pending.offset or applied),
u = pending.velocity or 0}`. Translational wall velocity exists only on a step
that advances to a pending target; a hold step (`c_old == c_new`) has
translational `u_w = 0` (spin unchanged), so a non-advancing circle never
acts as a sliding wall. One moving step consumes one target.
| situation | contract |
|---|---|
| `set_body` target | validated against `applied` (box, `|Δc|_2 ≤ 0.5` cell, speed bound) before mutation; on success replaces `pending` |
| two setters before a run | last wins; each validated against `applied`, not against the earlier pending target |
| `run(1)` with pending | upload record, step, sync; on success `applied := pending`, `pending := None` |
| `run(1)` without pending | record with `c_old == c_new`: no cover/uncover, links at `applied`, wall velocity `applied.velocity` |
| `run(n > 1)` with pending, or with nonzero `applied.velocity` | `ValueError` before mutation (single-step-only moving API) |
| `run(n > 1)`, no pending, zero velocity | allowed: static geometry, spin only |
| `run(1)` without pending | hold: `c_old == c_new`, no cover/uncover, links at `applied`, translational `u_w = 0` |
| `run(n > 1)` with pending | `ValueError` before mutation (single-step-only moving API) |
| `run(n > 1)`, no pending | allowed: hold for n steps, translational `u_w = 0`, spin only |
| `run(0)` | no motion upload, no commit; `pending` kept |
| validation failure | `ValueError`, nothing mutated, retry allowed |
| upload/launch/sync failure after enqueue | simulation unusable; `applied` and `pending` are not reported as device truth; no re-entry |
@@ -234,7 +237,8 @@ experiment above.
Jets or surface actuation on that body, `sync_bodies`/checkpoint while a
moving body exists; swept band touching domain boundaries, other bodies,
sensors or force regions; `set_body` offset outside the declared box,
per-step move ≥ 1 cell, speed above the declared bound.
per-step move `|c_new - c_old|_2 > 0.5` cell (the single bound of 4a), speed
above the declared bound.
- Host motion state is committed only after the upload *and* the following
synchronization of the step group succeed (section 4); any failure in
between makes the simulation unusable and no host/device match is reported.