Write docs/SPEC-v0.7.md, the Execution boundary contract - #135
Merged
Conversation
A delta over v0.1 to v0.6. It asks whether the kernel's guarantees hold at the edges it does not control: an executor deciding FAILED, a store clock on another host, and a world that moved after a human said yes. Five items: the NotExecuted classifier promoted from gateway/outcome.py into core as ctrlrun.transport; clock-skew detection; a provider idempotency token from (effect_key, attempt); max_attempts, written as an amendment to v0.1 §5.4; and precondition fingerprints, which narrow the decision-to-execution window and do not close it. Written against the code rather than the plan, and §1.4 records the nine places they disagreed: T182 to T208 are taken, so tests start at T209; a renewal of an approved action needs a new approval, so one yes buys one dispatch; the Postgres renewal UPDATE can reuse an attempt number; a receipt schema bump would break every chained 0.6 receipt unless a receipt renders under its own schema; verify's network guard refuses loopback; injected clocks will measure skew; max_attempts needs ctrlrun.policy/v5; the gateway raises NotExecuted unchained; and the byte count must be taken before the send, not after. Documentation only. No src change, no version bump, nothing in ctrlrun-docs.
SPEC-v0.7 §1.4 item 7 pointed at policy.py:115-127, which starts inside the top-level key map; the entry-key gate is 118-127.
|
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info⚙️ Run configurationConfiguration used: defaults Review profile: CHILL Plan: Advanced Run ID: 📒 Files selected for processing (2)
🚧 Files skipped from review as they are similar to previous changes (1)
Included review availability: Your plan provides up to 1 included review per hour; 0 remain after this review. 📝 WalkthroughWalkthroughThe changelog expands the Unreleased Documentation entry for the v0.7 “Execution boundary” contract. It records contract details, approval-dispatch rules, implementation assumptions, and corrections identified during draft review. No code or public declarations change. ChangesExecution boundary documentation
Priority: ⬇️ Low Estimated code review effort: 1 (Trivial) | ~3 minutes Change: Other Merge Risk: ⚪ Minimal · up to The documentation-only change has no identified merge-blocking risk. 🚥 Pre-merge checks | ✅ 5✅ Passed checks (5 passed)
✨ Finishing Touches🧪 Generate unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
Item 3a, a new build item stacked before item 3: the Postgres renewal compare-and-set is conditioned on the planned-from attempt, and a lost COMMIT's re-issue returns the attempt it wrote; every reservation method must return the number it actually wrote (§5.6, T246, T246b). G15 reaches the post-reservation check through a reconcile, so it can no longer pass with that check deleted. G5 and G14 skip an action whose ceiling forbids a renewal, and G12 uses separate keys. The rehash rule renders every schema under its own label, parses only the declared keys, and decides unchained by seq alone. N/A reasons go through unselected(). Verify's network rule is restated as it is actually true, with G12 on a loopback literal and HTTPConnection. Smaller: enforce mode and granted, not human; the adapter exception to the fast path; the policy v5 superset gates; clock_skew as an optional store attribute; the gateway's 401 rule stated plainly; per-Python pin of the write path; cross-deployment tokens; rolling upgrades; the gateway and ACS denial bound; wording in §6.3 and T268's word list.
The rehash rule becomes "hash what was stored": a receipt read from a store keeps its document in a private field and chain_hash() hashes it, so an added key, a relabel and a removed or unknown schema are hash mismatches, from_dict never raises inside receipts(), and no public name is added. Each schema's released key set is stated. T246b opens the insert path's real window, between the re-read and the re-issue's planning read. The G5/G14 ceiling N/A sentence is scoped to drivable actions, with precedence, and T270 runs the mixed document. Smaller: §4.6 leads with different effects sharing a key; T247 claims no window; refusals assert their reason and T245b uses three calls; the fast path refuses only a FAILED record; verify's guard admits only ports the run bound; clock_skew must be ctrlrun.state.ClockSkew and fails the store case otherwise; T229b covers TLS.
The stored document a receipt keeps is not an init parameter and does not survive replace(): the store read path sets it after its own replace, and put_receipt hashes the dict it serializes, so a receipt altered in memory the way G11 alters one is still content_altered, and a read-back receipt written again reads back clean. T265 gains that case, and its mutation sentence now names the one tamper that catches the mutation. The loopback guard records getsockname() after bind and refuses AF_UNIX on purpose. The G5/G14 ceiling sentence says "verify can select", covering the authority axis, and T270 runs the ungranted case.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
docs/SPEC-v0.7.md, the v0.7 "Execution boundary" contract, and a CHANGELOG[Unreleased]entry naming it. Documentation only: nosrc/change, no version bump, nothing inctrlrun-docs, no ROADMAP edit.Summary
v0.7 asks whether the kernel's guarantees hold at the edges it does not control. Five items, each specified against the code rather than against the plan:
ctrlrun.transport: theNotExecutedrule moves fromgateway/outcome.pyinto core (moved, not copied; the gateway calls the same function object).NotExecutedonly from the classifier's ownconnect()on a fresh connection that offered no request byte; everything after the first byte is the original exception. No HTTP status is everNotExecuted; redirects are not followed; no parameter widensFAILED. The httpx variant stays inctrlrun[gateway].clock_timestamp()with half the round trip as the bound, so latency is never reported as skew. Observation only: lease evaluation is unchanged.ctrlrun.idempotency_token(), derived from(effect_key, attempt)throughcanonical_byteswith a domain tag, rendered as a 36-character UUIDv8 (inside the verified limits of Stripe, Adyen, Square and PayPal). Pinned:("refund:txn_1", 1)gives382ee448-97da-8107-b674-8c253650d93f.max_attempts: decided on the attempt number the store assigned, after the reservation and before the executor, with a read-before-the-approval-gate fast path tested separately. The amendment text forSPEC-v0.1.md§5.4 is written out in §5.8.ApprovalMismatchwith three distinct reasons; the approval is left granted; §6.7 states the residual window and T261b opens it on purpose.v0.3 §4.3.1row its answer to "does it recheck preconditions", including the nine that say no. §8 is T209 to T271 plus G12 to G16 inv0.4 §2.1's form. §12 is headings only.Where each settled decision landed
NotExecutedchained, or the original re-raisedNotExecutedInvalidArgumentoutside an executorAPPROVEonly; notALLOW, notresumectrlrun.receipt/v4For the maintainer
Updated after the independent spec review (7 blocking, 9 non-blocking, all fixed in the spec; the review round is summarised below).
Decisions you may overrule:
postgres.py:787-800; fix:AND attempt = <planned-from>), and a lostCOMMIT's re-issue discards its result and returns the originally planned attempt (postgres.py:602-622,660-663,696-699; fix: return what the re-issue wrote). New rule: every reservation method MUST return the attempt number it actually wrote. Tests T246 and T246b open both windows with the test proxy. On SQLite the extraWHEREis an equivalent mutant and the spec says so. Both fixes are changes inside existing methods, not new methods.--store-urlnames and to loopback listeners it bound itself", because the old "nothing leaves the host" was already false under a remote--store-url. G12 drivesctrlrun.transport.HTTPConnection("127.0.0.1", port)directly, noturlopen(which followsHTTP_PROXYand would false-fail). T107's guard admits a connect only to a(127.0.0.1, port)pair the run itself bound through the patched socket class, refuses any other bind (so a0.0.0.0listener fails), matches the literal string rather thanis_loopback, checks the host insideconnectitself, and refuseslocalhostand::1. The tradeoff: an AF_UNIX socket or asocketpairwould keepv0.4 §3.7's words verbatim, but asocketpairis caller-supplied, which §2.3 says never yieldsNotExecuted, so G12 would lose its control; and AF_UNIX needs either a verify-only connect path or a test seam, which §2.6 forbids. It keeps the words and loses the evidence. Item 6 reconcilesREADME.md:258's "with no network".The four open questions:
EventSink(§3.6). The store retains its latest measurement asclock_skew: ClockSkew | None;Controlreads it withgetattrat the start ofexecute/resumeand after anAmbiguousEffectreservation refusal, uses it only if it is actrlrun.state.ClockSkew(a third-party store must use that class; a look-alike is ignored), logs at WARNING once per store per kind of error rather than raising, and appendsCLOCK_SKEW_DETECTEDthrough its normal path. Rejected: a constructor callback and a logger bridge. Please judge one thing: the spec now callsclock_skewwhat it is in effect, an optional member of the store contract (read from any store, invited from third parties, graded by T214), listed in §9.2 as an optional store attribute. It is not on theStateStoreprotocol. Whetherv0.6 §9.2's "no new store method" bar should cover it is your call. A wrapper that does not forward it silently drops skew reporting; decisions are unaffected.PostgresStateStore(clock_skew_threshold=...)within(0, DEFAULT_LEASE]. No value turns detection off.N/Abuilt throughunselected()like G10's, never because of the environment. G14 requires an effect key a renewal can reach, with G5'sN/Aplus a new one where every candidate declaresmax_attempts: 1. Item 4 amends G5's selection the same way, because undermax_attempts: 1G5's control would have failed a correct kernel.ctrlrun.idempotency_token(),max_attempts(withctrlrun.policy/v5),CLOCK_SKEW_DETECTED,approvals.precondition_fingerprintvia migration0005_precondition_fingerprint. §9.2 lists every other name.Where the spec departs from the plan, each argued in it:
SPEC-mcp-operator.mdowns T182 to T193 andSPEC-scan.mdowns T194 to T208.APPROVEaction needs a new granted approval (not necessarily a human one: scripted providers, automatedwait=Trueloops, the operator server and approvals granted ahead of a gateway all grant). Observe mode needs none. The unbounded case is theALLOWaction. The adapter path (needs_approval→Control.evaluate, which cannot see the ceiling) can still put a human in front of an attempt the fast path will refuse; §5.5 records the exception rather than teachingevaluatethe ceiling.v0.6 §6.4), and the round-2 review changed how: hash what was stored. A receipt read from a store keeps the document it came from in a private field, andchain_hash()hashes that document, so an added key, a relabel and a removed or unknownschemaare hash mismatches by construction,from_dictnever raises insidereceipts()(one tampered row cannot blind every reader), and no public name is added. Each schema's key set is its released writers': v1 19 keys, v2 21, v3 26, v4 28.max_attemptsneedsctrlrun.policy/v5, a superset ofv4; item 4 fixes the three equality gates that would refuse av5document using earlier keys (policy.py:912,931,1171). A standalone authority document labelledv5is accepted on purpose.N/Acannot be "no fingerprint", because providers are named in code; G16 is graded with verify's own provider and a printed note.401/challenged-403rule stays inoutcome.pyand is now stated as the product's one status-to-FAILEDpath, resting on the MCP peer's word;ctrlrun.gateway.transport.requestdoes not apply it.http.client's single write path on 3.11 to 3.14.COMMITTED. Decided: an effect key must name its effect uniquely across every store sharing a provider account, including the deployment wherever a placeholder is not unique at the provider; verify prints a note beneath G14 because the kernel cannot check it. Rejected: adding the environment (stable, but does not separate two stores in one environment) and a store id (none exists).preconditions=(§6.11): a 0.6.1 process running when migration0005applies consumes fingerprinted approvals without a recheck, and the kernel cannot detect it.expires_at; fail-closed.Nothing made me stop. No new
StateStoremethod, no new error type, no change to lease evaluation. The nearest are item 3a (inside existing methods) andclock_skew(an optional attribute, flagged above).One convention I did not follow. The pre-push hook refuses AI-tool references in commit metadata and in the tree, and the commit-msg hook strips co-author trailers, so the commits carry none and this description leaves the attribution line off, matching recent PRs.
Review round 1
max_attempts: 1false-fails G5, G14N/Areasonsunselected(); G1's inherited weakness notedv5equality gates, standalone authorityv5clock_skewis an optional store attributeboolrefusal load-bearing; cross-deployment tokens; G14's control rationaleReview round 2
receipts()and let an added key verifyN/Asentence was false for a mixed documentFAILED; whatmax_attempts: 1leaves ungradedclock_skewtype and error handlingChecks
PYTHON=.venv/bin/python ./scripts/check.shwithCTRLRUN_TEST_POSTGRESset: ruff format, ruff check, mypy strict, 2951 passed (rerun after the review fixes, unchanged). Without it: 2900 passed, 45 skipped, the baseline at724ae6eunchanged.capabilities,cli,schemas,api,cookbook,readiness,badgesall report no drift, as expected for a documentation-only change.This needs the separate spec review before it merges, per the build notes.
Summary by CodeRabbit