Plan 282fabbb (Filbert) and the six adversarial rounds (Rocko, r6 80cde839). Lead item 15: Gate F first, then A1 and A2 as separate reviewed commits. Co-Authored-By: Claude Opus 5.5 <[email protected]>
411 lines
24 KiB
Markdown
411 lines
24 KiB
Markdown
# Queue as data — adversarial review, round 3
|
||
|
||
VERDICT: revise
|
||
|
||
Rocko for Sage, 2026-09-26. The requested plan hash was verified **before
|
||
reading section 8**:
|
||
`cfdaa3fe4fa3fa6ef339f834a9814eb4a472ceac7c832c19bf955b61351ff21f`.
|
||
This review applies to that section plus Sage's explicit assignment rulings:
|
||
one JSON file with embedded log, complete-record link lock, canonical root in
|
||
genesis, 12-call E budget, 8.15 defaults and explicit per-seat credentials.
|
||
The superseded separate-journal alternative and unresolved-Q4 prose are not
|
||
treated as active choices.
|
||
|
||
During review the shared plan changed to
|
||
`1666f74b615c72a3b1f9f7bc306d3e1baed920d7eb3a19968bfa7727137aca46`.
|
||
Sage was notified. That intermediate revision is not separately reviewed;
|
||
the requested section was already read in full before the change. At Sage's
|
||
subsequent direction, the final revision is reviewed in the delta below.
|
||
|
||
The architecture is substantially simpler and the complete-record lock is
|
||
sound under its cooperative, single-host assumptions. Remaining blockers are
|
||
specific: durability versus visibility, out-of-protocol git rollback, the
|
||
requesting/uncertain lifecycle, the shared git index, and acceptance evidence.
|
||
No separate journal, repair engine, distributed locking or new identity
|
||
service is recommended.
|
||
|
||
## Direct answers to Sage's four questions
|
||
|
||
1. **Rename removes partial in-place JSON updates, not every torn system
|
||
state.** After rename but before directory fsync, the new name is visible
|
||
but not yet durably committed. JSON and Markdown are still two separate
|
||
replacements. Ordinary git ignores the lock and can overwrite the entire
|
||
internally valid log. See T1/T2.
|
||
2. **The link lock plus exclusive unlock gate is a reasonable design.**
|
||
Complete owner publication and manual-only reclaim address the earlier
|
||
races. Same-host boot/start mismatch may authorize unlinking the stale
|
||
record; foreign host or unreadable identity must remain unknown. Apply
|
||
the same rules to cleanup of a stale unlock gate. See T3.
|
||
3. **No resend on uncertain outcome is the right rule, but requesting must
|
||
be unresolved too.** A kill or failed outcome write leaves no uncertain
|
||
record. The human not-posted resolution also cannot be based solely on
|
||
not seeing a comment. See T4.
|
||
4. **The Gate G link is checkable as cooperative evidence.** Pi records
|
||
tool-call IDs, command arguments and corresponding tool results. An op-id
|
||
substring anywhere in a call is insufficient; inspect the actual command,
|
||
result, session branch and matching log transition. See T6.
|
||
|
||
## Findings
|
||
|
||
### T1 — High: visibility is being called durable commitment too early
|
||
|
||
**Where:** 8.0, 8.5 steps 4–6, unlocked reads in 8.4.
|
||
|
||
**Scenario:** the temp file is fsynced and renamed; the process is killed
|
||
before directory fsync, or that fsync returns an I/O error. A reader can
|
||
already observe the new revision. A host crash can then lose the rename's
|
||
durability: the design must not promise which pre-fsync namespace state
|
||
survives. On first creation it cannot even assume a prior queue exists.
|
||
This differs from a mere process kill while the host continues running.
|
||
|
||
The single-file design does avoid a half-appended log **when the complete
|
||
validated temp file is fsynced and only then renamed on the same filesystem**.
|
||
It does not establish the stronger statement “an operation after step 4
|
||
stands” when step 4 was interrupted before its durability barrier. Nor does
|
||
the word rename imply that every invalid file could only have been written
|
||
by an outsider; failed I/O or an implementation fault also need diagnosis.
|
||
|
||
**Required revision:** distinguish the visibility/linearization point
|
||
(rename), durable completion (successful directory fsync), and acknowledgement
|
||
(receipt). On failed fsync, report an uncertain local outcome with op id,
|
||
do not print success and do not undo by overwriting another version. Reads
|
||
may expose visible state, but must not authorize an external POST from an
|
||
intent whose durable write failed. The originating request path proceeds
|
||
to network I/O only after its own successful persistence barrier.
|
||
|
||
Define startup/retry behavior after this uncertainty without automatic
|
||
repair: inspect/verify and, if needed, explicitly establish durability of
|
||
the observed operation before claiming it durable. A plain read or replay
|
||
does not itself perform a durability barrier. State filesystem/platform
|
||
assumptions and handle short writes before rename.
|
||
|
||
**Acceptance:** distinguish process kill from host-crash reasoning; inject
|
||
file-fsync, rename and directory-fsync failures separately. Check that no
|
||
receipt or POST follows failed persistence, and no unsafe rollback occurs.
|
||
Do not claim power-loss behavior was tested merely by SIGKILLing a child.
|
||
|
||
### T2 — High: a valid git rollback erases both data and deduplication evidence
|
||
|
||
**Where:** 8.2 replay, 8.5 manual recovery, 8.12 integration.
|
||
|
||
**Schedule A:** writer A holds the queue lock and has read revision 12.
|
||
Seat B runs checkout/restore/stash on queue.json, installing revision 9.
|
||
A then renames revision 13 computed from 12, silently overwriting B's
|
||
operation. If B runs last, revision 9 silently wins instead. Git does not
|
||
consult `.git/mosaic-queue.lock`.
|
||
|
||
**Schedule B:** after an acknowledged review POST, ordinary checkout or
|
||
stash restores an older JSON and matching Markdown pair. It is perfectly
|
||
canonical and replay-consistent, but the log no longer contains the POST's
|
||
op id. Reissuing the same op can now send again. Internal replay cannot
|
||
detect replacement of its entire trusted history by an earlier valid one.
|
||
|
||
**Required revision:** make preservation of queue history part of the
|
||
cooperative git protocol: no checkout/stash/restore/reset/branch switch
|
||
touching queue paths while they carry unintegrated operations or active
|
||
review requests; lead coordinates and verifies any exceptional restoration.
|
||
Check baseline file identity/hash immediately before replacement to catch
|
||
ordinary accidental interference, while stating that this cannot atomically
|
||
exclude uncooperative git. Pin the branch as well as canonical path.
|
||
|
||
Withdraw the generic instruction “restore with git” for invalid JSON. First
|
||
preserve the failed bytes and reconcile all acknowledged and outstanding
|
||
ops against receipts; restoring HEAD may delete work performed since the
|
||
last commit. A deliberate history reset requires explicit disposition of
|
||
external side effects and cannot retain the normal deduplication guarantee.
|
||
No same-user file format can make arbitrary rollback impossible. This is
|
||
a necessary trust-model limit, not a demand for a second authoritative log.
|
||
|
||
**Acceptance:** checkout/stash interleavings and a restored older valid pair
|
||
must be either refused by the cooperating workflow or explicitly diagnosed
|
||
as outside the guarantee. Do not label a passing replay as proof that no
|
||
history was lost. Preserve append-only *logical* history across normal writes.
|
||
|
||
### T3 — Medium: stale-gate cleanup needs the same identity rules as unlock
|
||
|
||
**What is fine:** the lock record is complete before `link()` publishes it.
|
||
EEXIST preserves exclusivity. The exclusive unlock gate prevents two
|
||
unlockers acting on old observations. A writer publishing after the gate
|
||
appears either sees it and releases or is classified live and retained.
|
||
I find no two-cooperating-writers schedule violating that argument, given
|
||
the specified post-publication gate check and identity validation.
|
||
|
||
**Remaining scenario:** the lock/gate was created on host A; it is later
|
||
seen on host B where the numeric PID is absent. The Discord helper's
|
||
`ownerState` checks PID death before other identity fields and knows no
|
||
host. Blindly adopting that order would classify the foreign record dead.
|
||
The queue specification correctly says foreign host is unknown: that test
|
||
must take precedence over local PID liveness. A stale gate's current hint,
|
||
“remove it by hand once that pid is gone,” omits host, boot and reuse.
|
||
|
||
**Required revision:** define queue classification explicitly: validate the
|
||
record, establish supported host/namespace scope, then evaluate boot/start
|
||
and PID evidence. Same-host known previous boot is a mismatch; foreign-host
|
||
record or missing evidence refuses, even if no such local PID exists.
|
||
Apply this to the unlock gate's manual cleanup too. A reused local PID may
|
||
be alive but cannot be the old owner if known start/boot differs; never
|
||
signal that unrelated process. Unknown remains unknown.
|
||
|
||
The release check should compare the full acquisition identity (and ideally
|
||
the acquired inode), not merely op+PID. This is a small defensive improvement,
|
||
not a replacement for the gate. `unlock` must use the gate protocol directly,
|
||
not first try to acquire the very lock it is supposed to remove. Validate
|
||
temp writes and use exclusive temp creation; other link errors must refuse.
|
||
|
||
**Acceptance:** PID reuse within a boot; same PID/start on a different boot;
|
||
foreign host with locally absent PID; unknown /proc; stale gate with reused
|
||
PID; both writer/unlocker orderings. No age-based reclaim. A renamed host
|
||
may require manual diagnosis: safe unavailability is acceptable here.
|
||
|
||
### T4 — High: requesting is an unresolved outcome, not permission to request again
|
||
|
||
**Where:** 8.9; op uniqueness in 8.2 and retry order in 8.5/8.6.
|
||
|
||
**Scenario:** durable intent is recorded, the lock is released, POST is
|
||
accepted, and the CLI dies before reacquiring the lock. The row remains
|
||
`requesting`, not `uncertain`. The current prohibition on further requests
|
||
only explicitly covers uncertain. A new op could open another request.
|
||
Failure to reacquire after the 30-second network call has the same result.
|
||
A timeout of the shell helper may also leave its curl child running; the
|
||
server outcome remains unknown regardless of client cleanup.
|
||
|
||
**Required revision:** requesting-without-terminal-outcome and uncertain
|
||
must both block a new request for that logical review. An explicit manual
|
||
resolve handles both. Keep the original op and candidate frozen through
|
||
all phases. No retransmission on replay, read, retry or a new op while the
|
||
prior attempt is unresolved. Define outcome finalization as a separate
|
||
logged event referencing the original op: log op IDs are unique, so intent
|
||
and outcome cannot both append entries with the same ID. State who may
|
||
resolve and how conflicting/late resolutions are rejected.
|
||
|
||
**Manual not-posted:** a human merely checking that a comment is absent
|
||
does not prove a timed-out request will never complete. Require positive
|
||
non-delivery evidence or leave it unresolved. If the lead explicitly
|
||
overrides uncertainty to permit a fresh attempt, record the accepted
|
||
duplicate risk; do not still claim at-most-one delivery for that case.
|
||
`posted:<id>` must refer to the expected issue, marker, round and candidate.
|
||
This is operational reconciliation, not a blind state setter.
|
||
|
||
The 4xx rule should be limited to actual trusted endpoint responses known
|
||
to mean non-acceptance; an arbitrary transport/proxy failure is uncertain.
|
||
The existing helper provides HTTP status in stderr and response JSON in
|
||
stdout: the wrapper must preserve that distinction without exposing tokens.
|
||
There is no timeout inside the helper; D must bound the process tree and
|
||
treat interrupted transport conservatively.
|
||
|
||
**Related gap:** 8.7 allows `move in-review` separately from `review request`,
|
||
but Piece D's brief requires the move itself to post the request. Define
|
||
that move as the request workflow (or explicitly change the brief); otherwise
|
||
a seat can enter review without a request/round. Also, 8.5 runs stale-view
|
||
checks before retry lookup: a recorded op followed by a view-write crash
|
||
does not get 8.6's promised recorded receipt until someone renders. Define
|
||
read-only lookup/receipt behavior before view freshness blocks new mutations.
|
||
|
||
**Acceptance:** kill before POST, after server acceptance, before outcome
|
||
write and during lock reacquisition; new-op request while requesting;
|
||
same-op retry after stale view; delayed first POST after attempted resolution;
|
||
late outcome after manual resolution; no second POST in any uncertain path.
|
||
|
||
### T5 — High: the shared-index commit procedure can sweep unreviewed files
|
||
|
||
**Where:** 8.12.
|
||
|
||
**Scenario:** another seat already staged source. Step 1 adds the queue pair,
|
||
step 2 checks it, and step 3's plain `git commit` commits the other seat's
|
||
source too. Or another seat changes the index after staged verification;
|
||
the commit is no longer the tested staged snapshot. Even reading
|
||
`git show :queue.json` and then `git show :QUEUE.md` can observe different
|
||
index generations. Neither is solved by keeping the queue write lock out
|
||
of the test path.
|
||
|
||
**Required revision:** Sage should choose an isolated index for the intended
|
||
commit, or an explicit cooperative exclusive staging/commit interval with
|
||
a clean/approved index. Freeze a prospective tree id once, verify the queue
|
||
pair from that tree, verify the complete intended path set and compare HEAD
|
||
before committing exactly that tree. Preserve others' index and working
|
||
changes. Do not use path commit as a substitute: it can select current
|
||
working bytes instead of the tested staged pair.
|
||
|
||
The sequence says `verify-commit ID COMMIT` runs before the source is
|
||
committed. Define a prospective-tree verification target or verify the
|
||
resulting local commit before treating it as approved integration. Also
|
||
ensure package tests exercise the proposed queue code, not unrelated dirty
|
||
working versions while claiming the staged code passed.
|
||
|
||
**Acceptance:** unrelated staged file; two-stage reads across an index
|
||
mutation; index mutation after verification; working queue changes during
|
||
integration; changed HEAD; manifest compared with the actual prospective
|
||
source tree. Commit authorization remains separate from this procedure.
|
||
|
||
### T6 — Medium: Gate G's evidence exists, but the checklist must follow execution
|
||
|
||
**Observed in the installed pinned Pi code:** session entries have `id` and
|
||
`parentId`; the header may carry `parentSession`. Assistant `toolCall`
|
||
blocks have `id`, `name` and `arguments`; a `toolResult` has `toolCallId`,
|
||
`toolName`, content and `isError`. Thus a direct bash command and its result
|
||
can be linked without inventing an incarnation variable.
|
||
|
||
**False pass:** a failed command, a dry-run/echo containing the op ID, or a
|
||
command on an abandoned session branch satisfies “op id appears in a tool
|
||
call.” Meanwhile a helper has moved the row. The checklist already concedes
|
||
helper spoofing is outside the cooperative proof, which is honest; it
|
||
should still reject these observable non-execution cases.
|
||
|
||
**Required revision:** pin session id/file hash at the evidence cutoff,
|
||
freshness/no-parent evidence, active entry ancestry and the test interval.
|
||
Inspect the actual `scripts/mosaic queue` invocation in canonical cwd,
|
||
its op/row/actor/arguments, the corresponding tool-result ID and receipt,
|
||
and the matching log entry/revision. A successful recorded retry is evidence
|
||
of lookup, not proof this session originated the move: check the original
|
||
timing and pre-test revision. If output was lost or truncated, preserve the
|
||
actual recoverable evidence or declare the link inconclusive.
|
||
|
||
Require the trace `next output → named brief read → successful start
|
||
transition → concrete work`, with normal prerequisite reads allowed. The
|
||
work action needs its own successful result/effect, not merely a proposed
|
||
tool call. Define when input counting stops so later verdict/housekeeping
|
||
messages cannot retroactively fail the completed interval.
|
||
|
||
The literal “any row-specific text” context rule needs an exception for
|
||
the authorized brief/task data discovered during the test; otherwise the
|
||
task itself fails the audit. `git status` at two endpoints does not detect
|
||
an edit made and reverted between them. Record content hashes and bound
|
||
the no-coaching claim to the observed interval under the cooperative
|
||
no-external-edits rule. Jason's observation remains the final gate.
|
||
|
||
**Negative controls:** echo-only op id; nonzero command result; helper's
|
||
earlier op reused by the seat; resumed/forked session; wrong branch of the
|
||
session tree; brief never read; work command failed. Manual review suffices;
|
||
no checker package is required.
|
||
|
||
### T7 — Medium: unverified PIDs still qualify as a full liveness pass
|
||
|
||
**Where:** 8.10.
|
||
|
||
The display correctly says pid-present is unverified, but the full-pass
|
||
predicate allows every owner to be pid-present without any verified process
|
||
identity. A reused PID can therefore produce “full pass” although the
|
||
brief required a live owner registration. This recreates the acceptance
|
||
gap in more honest display wording.
|
||
|
||
**Required revision:** either call this a reduced registration/PID-presence
|
||
check and obtain the designated reduced-gate acceptance, or retain
|
||
incomplete liveness and do not issue a full pass. No start-time producer
|
||
or schema expansion is needed. Null/unknown PID needs a category and cannot
|
||
be converted to verified liveness. Keep the approved 12-call Gitea budget;
|
||
it is unrelated to this finding.
|
||
|
||
The age-unknown legacy case similarly needs incomplete coverage reporting
|
||
if it prevents deciding whether a required row is overdue. A report can
|
||
truthfully have zero known violations without meeting every full-pass gate.
|
||
|
||
### T8 — Medium: a few executable rules are still internally inconsistent
|
||
|
||
These are lead-level specification fixes, not new owner questions:
|
||
|
||
- **Ordinary add:** every add requires brief, but brief is privileged-only
|
||
“on add as well as afterwards.” Define the allowed initial fields/defaults
|
||
for an ordinary owner's add, or state that only privileged actors add.
|
||
- **Claim lifecycle:** specify claim creation/clearing for
|
||
in-review→in-progress, blocked→previousState and reassignment. Otherwise
|
||
“claimant” permissions can refer to the wrong owner or stale op.
|
||
- **Current briefs:** add validates a HEAD blob, but the fresh seat opens
|
||
a working path. `next`/start should refuse or visibly flag a working brief
|
||
that differs from the pinned blob; an optional verify --current against
|
||
HEAD alone does not establish what the seat reads.
|
||
- **Genesis bootstrap:** canonicalRoot exists only inside the file genesis
|
||
creates. Define the reviewed root input and special absence check for
|
||
first creation, without guessing a root or allowing a second genesis.
|
||
Resolve git-dir paths relative to the cwd actually used for the git call;
|
||
simplest is to run those queries explicitly from the discovered toplevel.
|
||
- **B scope:** 8.1 now lists only AGENTS.md, whereas Piece B also requires
|
||
seat context files that direct work to CURRENT.md to change. Keep those
|
||
named context edits and their snapshot verification in the active scope.
|
||
|
||
## What is now closed or honestly limited
|
||
|
||
| Earlier concern | Round-3 disposition |
|
||
|---|---|
|
||
| S1 owner-publication/reclaim race | Complete-record hard link and manual gated unlock address the core race. T3 specifies remaining classification/cleanup details. |
|
||
| S2 partial journal append | Removed by one validated fsynced temp JSON file. T1 is the narrower durability distinction; no journal repair verb requested. |
|
||
| S3 unexplained table drift | Genuine old-render hash versus unknown body and manual-only render is a sound boundary. JSON/Markdown mismatch remains detectable and intentional. |
|
||
| S4 tuple retry matching | Explicit persistent op IDs close the core ABA/tuple problem. T4 addresses receipt lookup ordering and multi-phase request events. |
|
||
| S5 shared git integration | Still open; T5 gives an exact prospective-tree procedure. |
|
||
| S6 multiple histories/replay | Canonical-root genesis, linked-worktree refusal and versioned replay are suitable for this scope. External git rollback remains a cooperative boundary (T2). |
|
||
| S7 impossible required dependency | Fixed by owner-approved prerequisites of either required status. Remaining field/claim details are T8. |
|
||
| S8 unsupported identity | Same-seat sessions deliberately share a claimant: an honest bounded limitation under Sage's ruling. T6 makes Gate G checkable; T7 prevents unsupported liveness acceptance. |
|
||
| S9 uncertain POST | No automatic retry is correct. Requesting, outcome events and manual negative resolution remain open (T4). |
|
||
| S10 candidate/brief evidence | Embedded manifest plus exact integration digest check is useful. It explicitly does not preserve uncommitted source bytes: review can become unrecoverable if those bytes vanish; that must block integration, not silently downgrade to a fresh candidate. T5/T8 bind verification to the actual source/brief. |
|
||
| S11 conflicting active sections | Section 8's precedence banner resolves the old-section conflict. This review does not relitigate superseded alternatives or accepted defaults. |
|
||
|
||
## Recommendation and evidence limits
|
||
|
||
Keep the ruled architecture. Before coding, close T1/T2/T4/T5 and make the
|
||
bounded checklist/matrix corrections in T3/T6/T7/T8. These are operational
|
||
and specification changes; they do not require Jason to choose a locking
|
||
algorithm or a new service. At the third review round, Sage should record
|
||
this remaining disposition explicitly rather than infer approval from the
|
||
absence of rejected earlier findings.
|
||
|
||
Investigation was read-only except this report. Failure schedules are
|
||
design analyses, not executed power-loss, git-interference or transport
|
||
tests against queue code (which does not exist yet). I inspected existing
|
||
process-identity helpers, API transport and local Pi transcript types; no
|
||
live session transcripts or credentials were read for this round.
|
||
|
||
Source pins: `packages/discord/src/journal.mjs`
|
||
`db33880f88dc2c7708015efecd0c6db604bc40387ea0dd6259d91f621a5b022c`;
|
||
`scripts/gitea-api.sh`
|
||
`033e6d5fdd4626fb0ca1c981b6d85eba961a4618a303faf2bb7b30ae024ed9a6`;
|
||
`scripts/agent-host-dev.sh`
|
||
`706f8e02fe0d8c18887d2e030f64f447a7db05badb3df3a20800c68ed5313687`.
|
||
Pi evidence: local `pi-coding-agent/dist/core/session-manager.d.ts` and
|
||
`pi-ai/dist/types.d.ts` under `node_modules/@earendil-works/`; bash tool
|
||
implementation under `pi-coding-agent/dist/core/tools/bash.js`.
|
||
|
||
## Delta: final specification 124b6f9e
|
||
|
||
Verified **before reading** the final section 8:
|
||
`124b6f9e250985d48654c6068ddfb0d82be6984f16da8700969281c4e06b0d26`.
|
||
Main review target remains
|
||
`cfdaa3fe4fa3fa6ef339f834a9814eb4a472ceac7c832c19bf955b61351ff21f`.
|
||
|
||
**Delta verdict: revise, for the same remaining technical findings.** The
|
||
recorded rulings are taken as authoritative for this review; no Q/J approval
|
||
is requested again. The only outstanding external input identified by the
|
||
final plan is seat tokens for D's live posting test.
|
||
|
||
- **J4:** Jason-only unpark to queued is explicit and appropriate: it
|
||
requires renewed briefing before work can start. Refusing required=true
|
||
on parked rows closes that conflicting state combination. Test unpark
|
||
actor refusal, queued re-entry and claim/review state cleanup. No new
|
||
authority finding against this ruling.
|
||
- **J5:** the new edge correctly refuses gateOwner=jason and requires
|
||
logged approval evidence for the allowed gate-owner/privileged path.
|
||
Define permission precedence against 8.8's blanket refusal for another
|
||
seat moving a claimed row; otherwise a legitimate non-owner gateOwner
|
||
could be rejected. Evidence must identify this candidate/round's approval,
|
||
and completion must settle the claim. These are the existing T8 lifecycle
|
||
details, not objections to delegated completion.
|
||
- **D:** fake-transport construction/testing reads no token; the live round
|
||
waits for explicit per-seat credentials. This is a clean build/live split.
|
||
It does not close T4: requesting can still outlive the CLI, and manual
|
||
not-posted resolution still needs a defined uncertainty disposition.
|
||
- **No repair/journal:** the final removal matches Sage's accepted design.
|
||
“Reviewed hand restore” improves recovery governance, but T1/T2 still
|
||
require reconciliation of uncommitted/externally effective operations
|
||
before a git restore discards their log. No repair verb is proposed here.
|
||
- **Other rulings:** accept the 12-call budget, root in genesis, link lock,
|
||
cooperative claims, narrowed closes with a logged reason, and E-before-D.
|
||
The reduced liveness gate is now explicitly accepted. T7 consequently
|
||
needs **no further approval**: label unverified PID-only coverage reduced
|
||
too, rather than full merely because no exempt seat exists. The accepted
|
||
reduced gate resolves permission to report limited coverage, not evidence
|
||
of verified liveness.
|
||
|
||
The final delta does not change the write/fsync sequence, shared-index
|
||
procedure or Gate G op-id test; T1/T2/T5/T6 remain applicable. T3's lock
|
||
classification and T8's ordinary-add, current-brief, genesis and B-context
|
||
details likewise remain. The core architecture is accepted as the target;
|
||
the revise verdict concerns these bounded implementation contracts.
|