Core Draft 0: arguments and evidence

Update, 7 September 2026: the accepted best-effort service model adds C-SERVICE-01 with documentation-only coverage. A fresh Rust adapter check passed 12 primitive/ preimage vectors, 14 signed-envelope vectors and six transition traces. Results are under docs/results/service-contract-v1/. The abstract model was also rerun. conformance/IMPLEMENTER_HANDOFF.md is prepared for an actual external implementer; preparing it does not establish independent implementation or review. Earlier arguments and their limitations are preserved below.

Informative companion. These are explicit proof obligations and sketches, not a security proof of the Rust implementation or the deployed network. The Core Draft is authoritative about proposed requirements; evidence may reveal that they need revision. Experimental slot policy is analyzed without making it mandatory Core.

1. Local safety argument

For one node and epoch, let S map credential slots to claim IDs. A successful allocation inserts S(slot)=claim only when the slot is empty or already maps to that same claim. Retention changes do not modify S. Acknowledgement follows durable commit, and restart restores the committed mapping under A-LOCAL.

Lemma L-SLOT (sketch): a sequence of these transitions cannot acknowledge different claims for the same slot in that epoch. Base case: S is empty. Inductive step: insertion into an empty slot establishes one binding; exact replay preserves it; conflicting input is rejected; restart preserves committed bindings. Epoch changes end the scope of the statement. This discharges P-LOCAL for the abstract rules, assuming signatures/bindings and storage behave as specified. It does not prove that a particular parser, filesystem, or implementation refines those rules.

Counterexample to the stronger GLOBAL claim: during partition, node A's empty S accepts X while node B's empty S accepts Y for the same slot. Both satisfy L-SLOT. No quorum intersection, majority threshold, or global exclusivity follows.

2. Quarantine and convergence argument

Let Q be the set of quarantined slots. Within an epoch, verified evidence only adds to Q. Permission use checks both S and Q. Restart restores committed Q.

Lemma L-QUARANTINE (sketch): after a quarantine commit, subsequent guarded uses of that slot fail until epoch transition. This requires every serving/retention path to consult current state, including previously issued receipts. The network paths are not yet wired to this guard; library tests alone do not satisfy that obligation.

Conditional P-CONVERGE (sketch): under A-DELIVERY, compatible policy, eventual successful durable processing, and the same valid evidence, each honest replica adds the slot to Q and thereafter rejects its use. This is convergence of a refusal predicate, not of all retained data or previous actions. At capacity the experiment suspends all sponsored service; its availability cost is not justified by this lemma.

Withheld evidence, permanent isolation, persistent storage failure, or incompatible policy breaks the progress assumptions. Those conditions do not imply that local cryptographic checks failed. Attention already given cannot be retracted.

3. Executable finite model

model/admission.py is written independently of Rust. It exhaustively explores two slots, three claims (two conflicting), two epochs, pending appends, acknowledged commits, crashes with incomplete or complete unacknowledged appends, and exact replay. Epoch guards, signature validity, and storage guarantees are abstract assumptions. It checks all reachable states rather than randomly sampling traces.

The retained run examines 122 states, 462 transitions, and 900 pairs of stable replica states for conditional quarantine convergence. It also constructs the partition counterexample. These counts describe this model only. They are neither millions-of-agents scale evidence nor a formal refinement proof of the runtime. Clock drift, saturation, key compromise, and scheduling fairness remain outside it.

4. Adversarial model and uncovered cases

Identity creation: unbounded keys; no assumed honest fraction. Required future experiment: fix honest traffic and vary attacker cost/volume, including valid proofs. Measure useful honest/newcomer retrieval, not just accepted identity counts.

Scheduling: adversary delays, duplicates, drops, reorders, or permanently withholds messages. Current evidence: abstract partition counterexample and separate ledger tests. Missing: deterministic transport simulation with evidence retry and queue load.

Resource pressure: valid equivocation can fill Q and suspend innocent sponsored traffic. The library has a saturation regression; an adversarial utility experiment must assess whether that failure policy is acceptable before promotion.

Storage/time: tests cover restart, partial tails, complete corruption, failed writes, ENOSPC, epoch pinning, and limited clock rollback. Missing: injected power-loss schedules, malicious backup rollback detection, and a network clock/skew contract.

Topology/keys: eclipse, malicious bootstrap, colluding operators, compromise, revocation, and membership churn are explicit threats without a completed network mechanism or proof. Their absence must remain visible in deployment claims.

5. Conformance coverage and evidence status

conformance/requirements.json links every Core requirement to existing evidence or an explicit gap. The initial executable suite tests only the candidate open-cost signing-preimage codec and Ed25519 primitive vectors. It includes malformed inputs. It does not test full message framing, admission transitions through a node API, network negotiation, durability of arbitrary implementations, or Core conformance.

The Python runner accepts a caller-supplied executable adapter. The included Rust adapter uses the actual claim codec and ring verification. A second independently written adapter would test this small surface, not establish two independent Skein implementations. No such second implementation or independent team review exists yet.

A second suite now checks 14 signed-claim envelopes independently generated with Python hashlib and cryptography, including distinct issuer/beneficiary signatures. Rust tests reject all 5,216 single-bit changes to the two normal envelopes and all truncations of three valid fixtures. This authenticates bytes, not permission or state transitions. See spec/core/CLAIM_PROFILE.md and the retained docs/results/core-claims-v1-conformance.json.

Property generation and fuzzing are separate pending work. The finite model is exhaustive within its abstraction, not a fuzzing campaign. Unit tests, model results, codec vectors, and performance reports must never be presented interchangeably.

6. Review gate

The review in spec/core/DECISIONS.md retains X-SLOTS and X-CONFLICT as an experimental profile and rejects blanket saturation suspension as a default. Before feature expansion, compare isolated capacity and define a complete wire/transition profile. Extend conformance to signed claim verification and state-transition traces, then parser/state-machine fuzzing and deterministic network fault schedules. Record changes to requirement IDs and rerun their linked evidence. Existing Rust behavior may need to change.

7. Local transition evidence

Six independently specified traces now execute 34 operations against the actual Rust ledger, using Python-signed fixture objects. They cover authorization, replay, clean reopen, quarantine, and the saturation-control failure. This is fixed-corpus coverage; clean reopen does not inject a crash. See spec/core/TRANSITIONS.md and docs/results/core-transitions-v1.json. The reserved-capacity comparison is specified in spec/core/CAPACITY_EXPERIMENT.md and now has an opt-in implementation with 24 matched cases. It is not promoted; see docs/RESERVED_CAPACITY_V1.md for the measured availability/storage tradeoff.

8. Preverification and issuer diversity

An experimental bounded preverification queue and eight multi-issuer cases now exist. Their limits are documented in docs/ADMISSION_QUEUE_V1.md. Queue outputs are not durable permission. Per-session round-robin does not establish Sybil fairness, and invocation credits do not impose a wall-clock CPU rate. No public network driver or protected local-evidence lane has been implemented.

9. Sync errors and bounded-driver proposal

Forty local fsync-failure scenarios now pass: 36 before/after-error combinations at nine sync sites and four modeled losses of unacknowledged tails. See docs/ADMISSION_FSYNC_V1.md for exact limits. Test hooks are absent from production builds; device failure and power-loss behavior are not proven by injected errors. spec/core/INGRESS_PIPELINE.md specifies the next driver experiment's resource budgets and acknowledgement rules. Its transport and commit scheduler are not yet implemented. Reserved commit service cannot guarantee passage through hostile input.

10. Driver model evidence

An independent Python model passes 13 targeted schedules and 128,000 seeded events, plus five observer/scheduling tests. It retains the attack-first session starvation case and reports both commit-lane refusal rates. Validity and successful recovery are oracles, not cryptographic/filesystem implementations. This is not exhaustive exploration or a proof that Rust refines the model. See docs/DRIVER_MODEL_V1.md and docs/results/driver-model-v1.json.

11. Synchronous Rust/model comparison

Thirteen shared fixed-corpus traces now match a Rust scheduler harness that uses the actual queue and durable ledger. This compares per-step observations, not just final states. Whole-second timestamps, pre-established sessions, and synchronous commits are deliberate restrictions. The broader model's asynchronous cases and 128,000 generated events have not been replayed through Rust. See docs/DRIVER_RUST_V1.md and docs/results/driver-rust-v1.json.

12. Controlled worker completion

Eleven additional shared traces use one real ledger-owner thread and a gate after its durable operation, or skip the operation entirely. They verify timeout fencing, withheld acknowledgements, retry, and exclusive OS locking. This is completion notification control, not a suspended fsync or physical failure. See docs/DRIVER_COMPLETION_V1.md and docs/results/driver-async-v1.json.

13. Real loopback framing

Sixteen TCP loopback cases now exercise fixed-size framing, total read deadlines, truncation, oversized declarations, signature preverification, and worker cleanup. Recorded buffer capacities and byte counts are not process-RAM measurements. This harness handles one frame per session and issues no durable acknowledgement. See docs/ADMISSION_LOOPBACK_V1.md and docs/results/admission-loopback-v1.json.

14. Serial receiver-to-ledger integration

Ten loopback cases connect framing, preverification and serial ledger ownership. They check a precommit no-response gate, suppressed responses after durable writes, clean reopen/replay without journal growth, and persistent quarantine. This uses fixed policy time and unsigned local responses; it does not establish concurrent server bounds, authenticated acknowledgements or crash/power-loss recovery. See docs/ADMISSION_INTEGRATION_V1.md and docs/results/admission-integration-v1.json.

15. Session and output components

Seven real loopback checks cover a four-slot session pool, overflow refusal, response bounds and cleanup. Nine injected writer checks cover nonblocking yields, partial writes, fixed output deadlines and errors. A tiny unread TCP response does not establish socket saturation; expiry uses injected scheduling time. These components are not yet integrated with the concurrent ledger driver. See docs/ADMISSION_SESSIONS_V1.md and docs/results/admission-sessions-v1.json.

16. Concurrent pipeline and real socket backpressure

Eleven checks connect four concurrent sessions to framing, preverification, serial ledger calls and bounded responses. Three reader tests cover fragmentation, nonblocking yields and invalid/truncated frames. A separate real TCP experiment observes WouldBlock, progress on another socket and bounded output completion or expiry. Synchronous fsync can still block the network pump; this is not the proposed isolated-writer production driver. See docs/ADMISSION_CONCURRENT_V1.md, docs/results/admission-concurrent-v1.json and docs/results/admission-saturation-v1.json.

17. Isolated writer integration

Twelve loopback checks move ledger ownership to one persistent thread with one outstanding request. Network cleanup continues during gated completion; deadline fencing clears queued sessions, refuses new work and suppresses late success. Clean reopen/replay preserves the unacknowledged commit. The gate holds notification after the operation, not OS fsync; shutdown may wait indefinitely on a real stuck call. See docs/ADMISSION_ISOLATED_V1.md and docs/results/admission-isolated-v1.json.

18. Finite pipeline resource baseline

Separate normal and allocation-profile release builds pass the same twelve checks. The normal harness is 718,560 bytes with 2.20 MiB observed peak RSS on this Mac. Diagnostic requested heap peaks at 45,617 bytes through the sampled phases, including fixtures and clients. These are single-run finite-workload observations, not full capacity, container requirements or throughput. See docs/ADMISSION_MEMORY_V1.md and docs/results/admission-memory-v1.json.

19. Rejection versus journal uncertainty

The isolated owner now uses the ledger recovery flag rather than fencing every rejection. Fourteen loopback checks preserve valid service after insufficient-work refusal. Completion-routing tests distinguish refusal, uncertainty and timeout; write/sync tests assert the underlying health boundary. This adds no public wire error taxonomy. See docs/ADMISSION_ERRORS_V1.md and docs/results/admission-error-boundary-v1.json.

20. Refusal/recovery model projection

Eight new shared traces match the Python model and gated Rust adapter; all 24 prior driver traces still pass. This compares accounting, successful acknowledgements, recovery state and bounds, not negative response bytes or the persistent network owner's complete trace. Rejected calls can be internal steps hidden by the projection. See docs/DRIVER_ERRORS_V1.md, conformance/driver-errors-v1.json and docs/results/driver-errors-v1.json.

21. Persistent network-owner observations

Five stable checkpoints from the actual loopback owner match a narrow independent owner model, including prepared negative responses and queue cleanup on fencing. This is one finite schedule; it is not equivalence with the larger two-lane driver model or all network interleavings. See docs/NETWORK_OWNER_V1.md and docs/results/network-owner-v1-comparison.json.

22. Queue pressure and source reuse

Seven loopback checks and four model checkpoints cover partial EOF, a two-job queue, explicit source closure and completion after session-slot reuse. Source closure reclaims queued work without cancelling the owner or erasing an admission. Complete TCP write-half-close remains valid. This is one controlled schedule; see docs/NETWORK_PRESSURE_V1.md and docs/results/network-pressure-v1-comparison.json.

23. Network service after clean recovery

Ten checks resume service through a new owner/listener after joining the fenced owner. Replay preserves accounting, fresh admission and quarantine append exactly one record each, and policy rejection preserves service for another slot. Six stable checkpoints match the narrow owner model. Successful recovery is an explicit model input; this is not process-crash or stuck-filesystem testing. See docs/NETWORK_RECOVERY_V1.md and docs/results/network-recovery-v1-comparison.json.

24. Real private Fly admission

Ten fixed-corpus admission requests pass on the existing private Fly pair, including wrong credentials and replay/quarantine after a source-Machine restart. The first round appends 663 bytes; the second appends zero. Both Machines are stopped with no public services. This serial pilot uses fixture time and preloaded descriptors, not general public admission. See docs/FLY_ADMISSION_PILOT_V1.md and docs/results/fly-admission-pilot-v1-audit.json.

25. Bounded descriptor submissions

docs/ADMISSION_DESCRIPTOR_V1.md specifies an experimental bounded claim-plus-Beacon envelope implemented by src/admission_descriptor.rs. Six tests in tests/admission_descriptor.rs exercise newly signed inputs, malformed envelopes, lease boundaries, durable replay, and rollback below committed time. No fixture lookup is needed. This library is not connected to the deployed Fly transport. The descriptor path now persists receiver time before lease decisions using a 40-byte sidecar. Additional tests cover restart after expiry refusal, a separate process reopening the floor, forward jumps, epoch rollover and corruption; four injected sync-boundary failures check fencing and recovery. The guarantee is relative to successfully persisted observations and assumes preserved storage and a trusted receiver clock. It does not cover disk rollback, power cuts, stalled storage, idle ticks, or callers bypassing observe_time. Aggregate ingress budgets and independent object encoding remain unresolved. This evidence does not establish public admission readiness.

26. Private descriptor transport integration

The bounded Submission now reaches a persistent ledger worker through a separately domain-separated private HMAC transport. The worker samples receiver time at execution. tests/admission_descriptor.rs runs five separate client/server exchanges covering admission, restart/replay, forgery refusal, old-domain refusal, and durable clock-floor enforcement. The existing ten-case fixture smoke remains passing. Details and commands are in docs/ADMISSION_DESCRIPTOR_V1.md.

This is serial loopback evidence, not a new Fly deployment. Concurrent scheduling, aggregate verification budgets, hostile network load, public encryption, real filesystem stalls and descriptor retention remain outside this integration.

27. Finite concurrent descriptor ingress

src/admission_ingress.rs adds an opt-in four-session scheduler with two pending packets, one ledger handoff, and 32 shared parsing/admission attempts per run. The socket test in tests/admission_descriptor.rs checks saturation and reuse, progress beside a stalled client, and budget exhaustion across 39 connections. It is not evidence of fairness, sustained rates, authenticated queue-pressure behavior, power-loss safety, or Fly/container memory. See the concurrent ingress section of docs/ADMISSION_DESCRIPTOR_V1.md for resource and shutdown limits.

28. Authenticated descriptor queue pressure

The unit test authenticated_queue_pressure_fences_and_discards_pending_work uses four authenticated socket clients and distinct signed descriptors. A test-only gate holds notification after the first real ledger operation. Two packets queue; one receives a full-queue refusal. Timeout fencing discards pending work and suppresses late success. Reopen retains one claim and replay adds no journal bytes. The scheduler joins sessions before publishing its queue-refusal counter.

This supports one controlled notification-delay schedule. It does not establish behavior under a genuinely stuck filesystem, broad schedule exploration, power loss, or public-network adversaries. No new Fly deployment was performed.

29. Linux descriptor container gate

docs/DESCRIPTOR_CONTAINER_V1.md records 44 passing release tests under one CPU and a 256 MiB cgroup limit. The sampled server high-water mark was 6,872 KiB; the whole test container peaked at 64,897,024 bytes. The 981,808-byte binary matches the non-root runtime image. The harness ran as root, on an amd64 image translated by an arm64 Docker host. These are small-workload measurements, not steady-state/full-capacity bounds or fresh Fly evidence. Raw output is preserved.

30. Finite public-test readiness

docs/FLY_DESCRIPTOR_PILOT_V1.md records 39 real private-Fly connections and a Machine restart. docs/PUBLIC_TEST_RUNBOOK_V1.md limits the next step to a finite, invitation-only Internet admission smoke test. The final explicit TLS-proxy build passed 45 Linux tests and a 1,000-connection local real-TLS run. The Python client verifies certificate trust and hostname and independently authenticates the application response. Private defaults still reject wildcard bind and public peers.

The source-pinned offline audit is scripts/audit_public_test_readiness.py. The final public-proxy binary has not been deployed; actual public-edge behavior must be checked before inviting testers. Independent security/transition review, full Object interoperability, fair sustained service, independent retention, real disk-stall recovery and unrestricted public admission remain unclaimed.

31. Real public TLS edge smoke

docs/results/public-fly-smoke-v3.json records the final binary on a separate Fly app. External TLS trust/hostname validation and application authentication passed for fresh admission, replay, expired/forged refusal, and wrong-invitation rejection. This was a five-request operator-only smoke, not a public load cohort. The Machine was stopped, services removed, invitation revoked and originals unchanged. Two staging failures were preserved. See the public-test runbook for retained resources and the limits of this evidence.

32. Three-client public TLS cohort

docs/PUBLIC_FLY_COHORT_V1.md records three temporary Fly clients concurrently using the real public TLS endpoint. Twelve checks passed with no retry, and three unique admissions added exactly 663 journal bytes. Median/max client request times were 22.23/273.35 ms, including transport setup. All clients were in one Fly region; this is functional evidence, not geographic/adversarial scale evidence. The clients were removed, the invitation revoked and the server stopped without public services. The runner now checks explicit reuse and preserves earlier ledgers.

33. Regional authenticated malformed traffic

docs/results/public-fly-mixed-regions-v1.json extends the cohort to lax, iad and ams with unsupported versions and truncated envelopes interleaved with valid admissions, replay, expired claims and forged signatures. All 18 client checks and five operator checks passed without retries; the three unique client admissions added 663 journal bytes. The compact audit verifies cleanup and unchanged original Machines. This is bounded functional evidence: refusal status does not identify its internal cause, and no sustained fairness or unrestricted public-admission guarantee follows. The runtime and frozen semantic control are unchanged.

34. Connection pressure and variable honest progress

Two bounded Fly partial-handshake experiments are preserved as docs/results/public-fly-pressure-v1.json and public-fly-pressure-v2.json. Honest acceptances varied from 1/8 to 7/8. The first recovery command failed without retained command diagnostics; its cause remains unknown. The repeat passed 12 recovery and five operator checks, with 663 journal bytes for three unique client admissions across pressure and recovery. Both runs cleaned up. These observations establish neither sustained fairness nor reliable progress under pressure. Better backend/proxy attribution is required before such claims.

35. Backend diagnostics without ingress log blocking

The local reference runtime now has opt-in aggregate diagnostic counters sampled outside ingress threads. Partial-handshake timeout/reconnect and queue/fencing assertions pass; 16 real TLS checks cover normal logging and a full diagnostic pipe without preventing process exit. See docs/PUBLIC_FLY_COHORT_V1.md for commands, schema and limits. Sampling is approximate and does not establish proxy attribution or fairness. This build is not yet Linux/Fly-certified; prior public results remain tied to their recorded binary, not the changed source.

36. Linux diagnostic build validation

docs/results/public-diagnostics-build-manifest-v1.json records a 1,000,808-byte Linux admission binary. Its build passed 45 release tests in a 256 MiB/one-CPU container, 1,000 local TLS backend connections, and eight checks with diagnostics enabled. This advances Linux validation only: registry upload was rejected pending approval of the new image digest, and no new cloud pressure evidence exists. Prior cloud failures and the absence of a sustained fairness guarantee remain.

37. Diagnostic cloud pressure and recovery

The user approved and the controller deployed the digest recorded in docs/results/diagnostic-image-upload-v1.json. The first diagnostic Fly run accepted 0/8 honest pressure requests and failed immediate recovery. Its backend recorded four partial sessions timing out and releasing within approximately two seconds, with no authentication, admission or fencing. Recovery connections did not appear in the captured backend counters. This narrows investigation to the path before application admission without proving a proxy defect.

The repeat waited five seconds before recovery, accepted 6/8 pressure requests, and passed 12 recovery plus five operator checks. It recorded 22 authenticated attempts/responses, no owner fencing, and 663 bytes for three unique client admissions across both phases. Both runs passed cleanup audits. Their differing pressure outcomes prevent attributing recovery success to the delay alone. See docs/PUBLIC_FLY_COHORT_V1.md; sustained fairness remains unproven.

38. Verified deployment mitigation for post-burst recovery

The reference deployment now separates proxy routing thresholds (soft/hard 8/16) from the application's unchanged four-session resource cap. Three preserved regional runs passed all 36 immediate recovery and 15 operator checks without retries or a recovery delay. Overload drops occurred at the backend, sessions released, and the owner did not fence. The controller, template and offline readiness gate agree on this verified profile; all cloud test resources were cleaned up except the stopped server and retained storage/IP.

This resolves the reproduced recovery issue for the tested finite deployment. Burst acceptances still varied from 2/8 to 8/8; the mitigation establishes neither fair service under sustained saturation nor a protocol-wide availability theorem. Proxy configuration is implementation/deployment guidance, not a normative wire requirement. docs/results/proxy-recovery-mitigation-v1.json binds the evidence; prior failures remain preserved.

39. Repeated handshake pressure without budget exhaustion

Three consecutive eight-connection waves exercised the same deployed runtime and proxy 8/16 profile. Seven of eight spaced honest requests succeeded, followed by 12 immediate recovery and five operator checks passing. The backend recorded 23 admission attempts, below its limit of 32; it shed 15 connections, timed out ten receives, returned to zero sessions and did not fence the owner. Cleanup passed. docs/results/public-fly-pressure-waves-v1.json preserves the raw result. This is approximately 9.39 seconds of bounded pressure, not a sustained-fairness claim or per-client service guarantee. The readiness gate now checks this result and its source/evidence manifest in addition to the prior recovery regressions.