Add non-trivial-proof: stateful HTTP echo lifecycle study (scenario #1, measure-first) - #3
Open
verivus-open wants to merge 13 commits into
Open
Add non-trivial-proof: stateful HTTP echo lifecycle study (scenario #1, measure-first)#3verivus-open wants to merge 13 commits into
verivus-open wants to merge 13 commits into
Conversation
…2 fixes Design for the stateful I/O proof: a multi-language HTTP echo server lifecycle governed by the same DAG-TOML machinery as hello-world. Includes the §7 leaf-count correction (three leaf nodes U08/U09/U10, matching the validator-computed set in §4) and the §12 gate-status fix (Grok no longer counted as an equal third approval), plus the §12.1 round-2 cross-model re-review record (Codex 7a7ad1e1 evidence-backed approval; Gemini noted non-evidential), recorded under the retrieved-by-job-id discipline. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…; add FUTURE-STUDIES DESIGN.md: - Retract the false "Java HttpServer carries the same SO_REUSEADDR guarantee" claim. Empirical spike (OpenJDK 25.0.3/Linux) shows com.sun HttpServer sets no SO_REUSEADDR and exposes no API to set it, so it cannot re-bind a port holding a ~60s TIME_WAIT (a <=2s retry is useless); ServerSocket(reuse=true) can. Mitigation propagated to §1 C04, §3, §4 (U08 runs Java first), §5.1 step 1 (Java no-reuse pre-flight; foreign TIME_WAIT => SKIP). - Lead the title/framing with "eight languages" (the firm number); define "runtime" explicitly and own the C/Rust-both-native soft edge (§2/§11.1). - Require validators run with --check-paths-exist --repo-root so on-disk path existence is actually enforced, not just structure/links (§7, §10 step 3). FUTURE-STUDIES.md: record the four-scenario arc — #1 HTTP echo (in progress), #2 concurrent sort, #3 third-party deps, #4 Semgrep/CodeQL SAST — each with contract, what it stresses, and artifacts needed. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…ate (§12.2) Cross-LLM gate on commit 3437e30 caught a defect Gemini missed: §5.1 step 7 still said the re-bind probe "pairs with the mandatory SO_REUSEADDR on every server," contradicting the §3 Java exception (Java cannot set it). Rewrote the paragraph: the port-release check is valid for all seven runtimes including Java because the PROBE socket sets SO_REUSEADDR, independent of the server; Java is handled by run-ordering. §12.2 records the round: Codex 376fb179 (BLOCKER) -> 3b9f0b44 (evidence-backed unconditional approval after fix); Gemini f980ef49 approved but missed the blocker. Also retracts round-1 finding #2's now-false resolution (setReuseAddress before bind is unreachable via the HttpServer API). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Eight echo servers (Go, Node/JS, TypeScript, Python, C raw-sockets, Rust std+FFI no-crates, Java source-launch, gawk /inet) + two negative controls; three witnesses (run_service_contract.sh C01..C05 serialized Java-first; detect_graceful_shutdown.sh; detect_awk_boundary.sh); five DAG-TOML files that validate with --check-paths-exist --repo-root; README with the real Observed Execution table (7 PASS / 1 SKIP / 0 FAIL on this runner). Cross-LLM gate (§12.3): Codex (f3cde9d8) raised three real witness-vs-contract vacuity blockers — C03 Content-Length never checked, C04 port-release polled ss instead of a real SO_REUSEADDR re-bind probe, traceability overclaimed AWK as held to C01..C05 — all fixed and re-confirmed (bc430543, validators re-run). Gemini (32739d3d) approved but missed all three; the gate rests on Codex. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…ound-5)
manuscript/{main.tex,references.bib,README.md}: the paper for the stateful HTTP
echo-service proof, adapting the hello-world paper structure. Leads with eight
languages; reports the real Observed Execution (7 PASS / 1 SKIP / 0 FAIL), the
first real use of the MEASURED result word, the graceful-vs-kill negative
control, and the Java SO_REUSEADDR spike as a measured runtime correction. 11
cited references (drops the clone-detection set; adds twelvefactor disposability
and Nygard's Release It!). No TeX on this runner: cite keys resolve, all 17
bundle paths exist, LaTeX environments balance.
§12.4 logs round-5: Codex (fe3612ce -> 0ab94e38 -> 5efa2a44) caught the same
real defect in three places -- the paper swept AWK into the full C01..C05
lifecycle though the bundle holds only seven PASS-candidates to it -- abstract,
intro, then conclusion; all fixed, then unconditional approval. Gemini
(99d2b738) raised a "30 entities" blocker that was an arithmetic miscount
(code section = 11, total = 29 per the validator); rejected with evidence.
This completes §10 (bundle + manuscript).
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
A pinned podman image (Containerfile, opensuse/tumbleweed base pinned by digest) reproduces the whole Stateful I/O proof and compiles the paper, closing the honest "ran on this runner" gap. go 1.26.3 / node 24.15.0 / rust 1.90.0 pinned by version + sha256; java-25-openjdk matches the host's SUSE OpenJDK 25.0.3 build; gcc/gawk/python/TeX from the pinned base (one documented delta: gcc 15.2.1 vs host 15.2.0). reproduce.sh runs the 3 witnesses + 5 validators + pdflatex/bibtex; build-and-run.sh stages a minimal context (proof tree + the sibling-repo validators) and bind-mounts the manuscript dir for main.pdf output. In-container run: witnesses 7 PASS / 1 SKIP / 0 FAIL, both negative controls caught, AWK C06 boundary confirmed, all five validators pass, main.pdf built (10 pages) — so the proof holds in a second, version-pinned environment. The container also surfaced and fixed one undeclared dependency the host happened to have (validate_implementation_dag.py imports networkx; added python3-networkx). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The podman reproduction builds+runs green, but its prose overclaimed: it called itself "hermetic" with "pinned toolchains" while every zypper package (gcc, gawk, python3, java, TeX, networkx) tracks live Tumbleweed repos and drifts on rebuild; it documented only the gcc 15.2.1-vs-15.2.0 delta and omitted the larger gawk 5.4.0-vs-5.3.2 one; it claimed the JDK "matches exactly"; and the validators are an unpinned sibling checkout. Containerfile/reproduce.sh/build-and-run.sh/README now separate PINNED (base digest + go/node/rust sha256) from NOT PINNED, disclose both deltas as a snapshot, scope the JDK match to this build, and stamp the validators' git rev (PROVENANCE.txt). Prose/disclosure only — no functional build/run/install/TeX command changed; the three sha256 pins are unchanged. §12.5 logs the round: Codex (b67e985d -> 4a6e9007 -> 271ee865) raised 6 main + 2 residual honesty/reproducibility blockers, all fixed, then confirmed all four files OK with sha256 pins intact. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…eader
The research-quality rubric lived under chardet-relicense/ (untracked) and was
written for one genre (falsifiable measurement/detection harnesses). Promote it to
the papers-repo root so it applies across all artifacts, and add §0.1 "Two genres
in this repo" distinguishing:
- Genre A — measurement/detection harness (chardet, CDA): every dimension at full
weight; D (controls/calibration) and E (statistics) are core.
- Genre B — executable assurance proof / engineering artifact (hello-world,
non-trivial-proof): E1-E6 and D3-D5 are N/A-with-reason (no null distribution or
statistics), but D1/D2 STILL APPLY as a deliberately-broken control the gate must
catch; A/B1-B3/C2/C4/C5/F/G/H and §6.2 hold at full weight.
The header explicitly warns against the failure mode a panel review just exhibited:
forcing D3-D5 to "pass" for a categorical proof by relabelling a design fact as a
"null" (mark N/A instead). The chardet copy is now a pointer stub to the root.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…DDR finding
The prior stateful-I/O proof asserted a FALSE Java finding — that
com.sun.net.httpserver.HttpServer "sets no SO_REUSEADDR and cannot re-bind a
TIME_WAIT'd port" — and built a load-bearing Java-first run order on it, plus a
§12 review record with documented fabrications. Direct measurement
(MEASUREMENTS.md M1; committed ReuseSpike.java, 6/6) overturned it: a started
HttpServer (NIO ServerSocketChannel, SO_REUSEADDR on by default) tolerates a
prior TIME_WAIT and releases its port immediately on stop(0). The real,
deterministic footgun is a never-start()ed stop() leaking its listener — an
in-process quirk that does not affect the cross-process proof.
This rebuild (old set safe on branch pre-rewrite-nontrivial-2026-06-01):
- DESIGN.md rewritten from measured facts; §3.1 "Measured Runtime Correction"
retracts the false finding; all Java special-casing removed (Java now runs
last in plain build order). §12 reset to an honesty-trail of this rebuild.
- run_service_contract.sh: dropped Java-first ordering + no-reuse pre-flight;
uniform independent SO_REUSEADDR re-bind probe for all seven PASS-candidates.
- ReuseSpike.java + detect_java_reuseaddr.sh re-pointed to the TRUE finding;
SKIPs honestly (exit 2) when the kernel cannot hold a TIME_WAIT.
- Differential behavioural-equivalence witness added as a first-class DAG leaf
(U11 + traceability chain 4 + evidence E06/EV08/M09) with a committed broken
calibration control (src/controls/broken_echo.py); 0 divergences across the 7
servers, control caught 6/10 (non-vacuous). differential_echo.py now returns
a real exit code.
- manuscript/main.tex rewritten to match the correction (retraction section,
plain build order, differential channel, updated counts/tables). Container
reproduce.sh now runs all five witnesses and gates on each. Stale committed
main.pdf removed (it is a container build product; no TeX on the runner).
Verified green: 5/5 DAG-TOMLs validate with --check-paths-exist (11 units,
layers {0:10,1:1}, critical-path LOC 327, 36 traceability entities); witnesses
7 PASS / 1 SKIP (awk C06) / 0 FAIL; both graceful controls caught; differential
non-vacuous; Java reproducer CONFIRMED.
Cross-model gate SATISFIED in two rounds (DESIGN §12.1 design+bundle, §12.2
manuscript+container), each on Codex's blocker(s)->fix->evidence-backed
unconditional approval with Gemini corroborating; only retrieved-by-job-id
output recorded.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
| if delay > 0 { | ||
| time.Sleep(time.Duration(delay) * time.Millisecond) | ||
| } | ||
| _, _ = w.Write(body) |
| if delay > 0 { | ||
| time.Sleep(time.Duration(delay) * time.Millisecond) | ||
| } | ||
| _, _ = w.Write(body) |
…l pre-merge gate The final holistic pre-merge cross-model review (DESIGN §12.3) caught a real cross-document contradiction: DESIGN §5.4 still described the differential calibration control as "materialized by the harness itself (embedded + written to a temp path)" — the original approach, abandoned mid-build for a committed src/controls/broken_echo.py that the harness loads by fixed bundle-relative path. The harness, traceability, evidence matrix, and manuscript already used the committed-control model; only §5.4 was stale. Reworded §5.4 to match. Records the round-3 gate in §12.3: Codex (49a4a78f -> 9c318530) blocker -> fix -> evidence-backed unconditional approval; Gemini (02eaadeb) evidence-backed approval. Only retrieved-by-job-id output recorded. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…ot + chardet copies Prior-session commit 650fa4e had promoted the guide to the repo root (with a chardet-relicense stub pointer), putting two files outside non-trivial-proof/ into this PR. Move the canonical guide to non-trivial-proof/RESEARCH-QUALITY-GUIDE.md and remove the repo-root and chardet-relicense copies, so this PR's net diff is confined to non-trivial-proof/. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…al-review sections
Add two sections that surface contributions previously confined to the design
docs (paper 11 -> 13 pages):
- "Differential Behavioural Equivalence Across Implementations" with a results
table: seven implementations byte-exact-equivalent on a 10-input adversarial
corpus; committed calibration control caught on the 6 bodies > 16 B (non-vacuous).
- "Keeping the Proof Honest: Measure-First and Adversarial Cross-Model Review":
the self-falsification of the Java SO_REUSEADDR claim, the per-round adversarial
gate and the defects it caught, and the finding that an approval verdict is not
evidence (one model approved while missing what another blocked on).
Gated as DESIGN §12.4: Codex (610175e4 -> c7fd3345) raised a real review-scope
overclaim ("all four artifacts before each milestone" vs the per-round scopes in
§12.1-12.3) -> fixed -> evidence-backed unconditional approval; Gemini (01e67988)
evidence-backed approval. An accuracy slip in the new honesty section (example
blockers drawn from the voided pre-rebuild review log) was self-caught and
corrected before dispatch. Container reproduction stays green; main.pdf compiles
to 13 pages (build product, not committed).
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…M1b)
A pre-submission referee report found two un-measured Java runtime claims — the
very sin the measure-first discipline exists to prevent. Measuring them was
significant:
M1a: the manuscript footnote "Java shuts down in 27ms because stop(2) interrupts
the sleep" was false. com.sun HttpServer (default null executor) does NOT transmit
response headers until body bytes flow, so the witness's header-flush sync point
silently failed for Java: SIGTERM landed on an already-complete request and C04's
in-flight clause was VACUOUS for Java (body 0ms after SIGTERM vs ~1001ms for Go;
the sleep completed normally). Fix: src/java/Server.java's test-only delay path now
flushes the first body byte before sleeping, forcing headers onto the wire so the
remainder is genuinely in flight; Java's measured shutdown is now ~1000ms like the
others. New permanent guard detect_inflight_window.py (DAG leaf U12, traceability
chain 5, evidence E07) asserts each PASS-candidate's in-flight body completes
strictly after SIGTERM by >= half the delay — non-vacuous by construction.
M1b: the SO_REUSEADDR "channel defaults reuse on by default" causal claim is demoted
to a measured inference about this JDK build (DESIGN §3.1, manuscript §9).
Also per the referee: M3 (define "proof" narrowly in §1), M2 (the DAG is depth-1;
"critical path" is not a scheduling claim; state what the declarative layer adds),
M5 (report the podman container reproduction as a second mostly-pinned environment),
and minors (JEP 330 clause, softened Rust/libc phrasing). Counts updated everywhere
(12 units, layers {0:11,1:1}, 43 traceability entities, 26 evidence entries, six
witnesses); container reproduce.sh gates on all six; FUTURE-STUDIES marks #1 complete.
Gated as DESIGN §12.5: both Codex (c122fe8c->3a4dcdda) and Gemini (8088a07e)
independently re-ran the witnesses and confirmed the fix (all 7 in-flight genuine,
Java ~1000ms, differential 0 divergences); Codex ran the full podman reproduction
(6 witnesses + 5 validators + 14-page PDF). Both flagged a stale §2 artifact-count
list -> fixed; Codex blocker->fix->unconditional approval. main.pdf is a container
build product (not committed).
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
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
2 participants
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.
Summary
Introduces scenario #1 of the four-scenario "escape the triviality trap" arc:
a stateful, multi-language HTTP echo service-lifecycle proof — the follow-up to
the
hello-world/stdout proof. It points the same DAG-TOML machinery (contract →implementation DAG → traceability → readiness gate → evidence matrix → executable
witnesses) at a contract that cannot be checked by run-to-completion + stdout
diff: each server must bind a port, stay alive, echo a
POSTbody byte-for-byte,answer repeated requests, and shut down gracefully on
SIGTERM.The branch's earlier CDA/lineage commits already merged via #1; the net delta here
is the
non-trivial-proof/tree (plus one repo-root change from a prior session,the RESEARCH-QUALITY-GUIDE promotion in
650fa4e).What's in it
Rust, Java as PASS-candidates; AWK as the declared C06 signal boundary.
run_service_contract.sh(C01–C05), the graceful-vs-kill negative control (two non-graceful controls), the
AWK C06 boundary witness, a cross-implementation differential-equivalence witness
(
differential_echo.py, with a committed broken calibration control), and there-pointed Java reproducer.
--check-paths-exist(11 units, layers{0:10,1:1}, critical-path LOC 327, 36traceability entities).
manuscript/main.tex) and a podman reproduction with honest partial-pinning disclosure.
Measure-first correction (the honesty trail in this history)
An earlier commit on this branch asserted a false Java finding — that
com.sun.net.httpserver.HttpServercannot setSO_REUSEADDR/ re-bind aTIME_WAIT'd port — and built a Java-first run order on it. Direct measurement(
MEASUREMENTS.md; committedReuseSpike.java, 6/6) overturned it: a startedHttpServertolerates a priorTIME_WAITand releases its port immediately onstop(0). The real footgun is a never-start()edstop()leaking its listener.The final commit (
2b694a9) retracts the false claim, removes all Javaspecial-casing, and re-points the reproducer; the intermediate commits are kept as
the honesty trail. The net diff to
mainis the corrected state.Verification (on the authoring runner)
--check-paths-existrun_service_contract.sh: 7 PASS / 1 SKIP (AWK) / 0 FAIL(non-vacuous)
Cross-model review
Both gate rounds SATISFIED (DESIGN §12.1 design+bundle, §12.2 manuscript+container),
each on Codex's blocker(s)→fix→evidence-backed unconditional approval with Gemini
corroborating; only retrieved-by-job-id output recorded.
🤖 Generated with Claude Code