Repository navigation
Conversation
curl_transfer_argv set no HTTP version, so curl negotiated HTTP/2 with the download hosts. Over HTTP/2, macOS /usr/bin/curl 8.7.1 exits 56 for a size-limit breach, which run_curl_transfer does not classify as the enforced limit (63), and it does not retry a 503. Qualification only exercised HTTP/1.1, because its http.server fixture offers no ALPN protocol. Pass --http1.1 in the shared argv. The fixture now offers h2 before http/1.1 through ALPN, as the download hosts do, so a client that accepted h2 fails the real-curl tests.
The participant-opacity proof manifest binds each source that acquires the prover by digest, tools/maintained_client_acquisition.py included. Record the digest of the file with the --http1.1 argv. The proof lane, the participant-opacity proof tests and the dev-container smoke failed on the old digest.
9 of 11 tasks
The Cambridge Isabelle mirror (www.cl.cam.ac.uk) negotiates only http/1.1; the other download hosts in the tooling artifact lock offer h2.
doublewhy
marked this pull request as ready for review
October 10, 2026 14:09
3 tasks
doublewhy
added a commit
that referenced
this pull request
Oct 12, 2026
…ter entry Each open entry in the divergence register now names its issue: #1525 to #1557 for the production changes, and #1521 for the smaller corrections. The entries that open pull requests now address move to "Addressed by pull requests" with their issues: GH-7 (#1491, #1490), NS-1 (#1476, #1475), NS-2 (#1480, #1479), MF-2 (#1483, #1482), CL-2 (#1474, #1473), ST-2 (#1472, #1559) and NS-7 and NS-8 (#1488, #1560 and #1561). ST-1 names #1558, GH-3 records that #1415 merged, and "What remains" names #1522 for the unverified and unexamined boundaries.
10 tasks done
This branch has not been deployed
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
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
curl_transfer_argv(tools/maintained_client_acquisition.py) builds the one argv that qualification and every real acquisition share. It set no HTTP version, so curl negotiates HTTP/2 with the download hosts. #1475 reproduces this on dev 3512210 with macOS/usr/bin/curl8.7.1:run_curl_transferthen reportscurl-transfer-failedinstead ofcurl-size-limit-enforced.With
--http1.1, the same transfers exit 63 and, for the 503, 22 after three requests. Qualification never saw the difference: itshttp.serverfixture offers no ALPN protocol, so curl always used HTTP/1.1 there. The #1344 fixture-provenance audit recorded the same exit codes (finding NS-1 in the record #1461 proposes).This PR adds
--http1.1to the shared argv, inside the design #1246 introduced. No outcome classification, budget, retry or redirect setting changes. The real-curl fixture now offersh2beforehttp/1.1through ALPN, as most download hosts do (the Cambridge Isabelle mirror,www.cl.cam.ac.uk, offers onlyhttp/1.1).http.serverspeaks only HTTP/1.x, so a client that acceptedh2fails the real-curl tests. That makes those tests, and the large-object ones intest_issue_1220_isabelle_acquisition.pythat reuse the fixture, fail without the pin.The participant-opacity proof evidence binds each prover-acquisition source by digest, so the second commit records the new digest of
tools/maintained_client_acquisition.pythere.Requirement UIDs
Related Issues
Closes #1475
ADR Impact
curl("Repository adapters own selection, local integrity checks and installation, never HTTP behavior").--http1.1is native curl configuration, like the--proto,--max-redirsand--retryflags already in the argv. No repository HTTP code is added.Changes
tools/maintained_client_acquisition.py:curl_transfer_argvadds--http1.1after the--protoand--proto-redirrestrictions, with a comment giving the reason.implementations/python/tests/test_issue_1217_bootstrap_profiles.py:test_curl_qualification_uses_fixed_hardened_argvasserts that--http1.1is the argv's only--http*flag._https_fixtureoffersh2andhttp/1.1through ALPN (ssl.SSLContext.set_alpn_protocols), so the real-curl tests see a client that negotiates HTTP/2. Its comment says most download hosts offerh2first (third commit,578c6fec): every host probed below negotiatedh2except the Cambridge Isabelle mirror.specs/formal/participant-semantics/participant-opacity-proof-evidence.json(second commit,7d2f81d6): thetoolchain.tool_sourcesdigest oftools/maintained_client_acquisition.py. The proof checker binds that file by digest (PROOF_TOOL_SOURCE_PATHSintools/check_participant_opacity_proof.py). On the first head,76cbe186, the old digest failed three CI jobs.canonical / proofand sixtest_issue_963_participant_opacity_proof.pytests incanonical / integrationreportedproof tool source digest does not match its repository source(CI run 38046775269). The Bootstrap dev-container smoke expects the proof session to stop at its bubblewrap check, and it did not find that line (Bootstrap qualification run 38046775103). Locally the checker validates this digest before its platform and sandbox checks. Only that digest changes. refactor(tooling): simplify connected developer and release workflows #1317 re-pinned other tool sources in this manifest the same way.Test Plan
All runs were on macOS, where
/usr/bin/curl --versionreportscurl 8.7.1 (x86_64-apple-darwin26.0) libcurl/8.7.1 (SecureTransport) LibreSSL/3.3.6 zlib/1.2.12 nghttp2/1.69.0. Commands ran fromimplementations/python.Real-curl tests on
578c6fec, with the selection the Bootstrap qualification workflow uses:uv run --frozen --all-extras python -m pytest tests/test_issue_1217_bootstrap_profiles.py tests/test_issue_1220_isabelle_acquisition.py -q -p no:cacheprovider -m integration -k real_curlpassed (8 passed).The same run fails without the pin. With
tools/maintained_client_acquisition.pyrestored to dev's version and the new tests kept, 7 failed and 1 passed:curl-transfer-failed, for example{'reason_code': 'curl-transfer-failed'} != {'reason_code': 'curl-size-limit-enforced'}./disconnectcase, which expects that reason.test_curl_qualification_uses_fixed_hardened_argvfailed withassert [] == ['--http1.1'].A scratch
http.serverTLS fixture checked the fixture change before it was written:h2offer, the server sawh2from dev's argv and every transfer failed. From the pinned argv it sawhttp/1.1, and the transfers passed.Download hosts, for the fixture's ALPN offer: for the first
source_urlsentry of each of the 12 hosts inimplementations/tooling/artifacts.lock.json,/usr/bin/curl -sS -o /dev/null -I -w '%{http_version}', which offersh2, negotiated HTTP/2 with 11 hosts and HTTP/1.1 withwww.cl.cam.ac.uk, the Isabelle archive's second URL. Against that host,openssl s_client -alpn h2,http/1.1selectshttp/1.1, and anh2-only offer negotiates no ALPN protocol.The #1475 reproduction against real hosts, rerun on this branch, uses the argv from
curl_transfer_argvplus--verbose:http/1.1after 2 requests (redirect and asset).https://httpbin.org/status/503andhttps://postman-echo.com/status/503exit 22 after 3 requests.Through the production entry points,
run_curl_transferreturnscurl-size-limit-enforcedfor the oversize transfer (dev:curl-transfer-failed), andrun_curl_qualificationreturnspassedfor it. The exact-limit transfer returnscurl-transfer-qualified.Module runs on
578c6fec:test_issue_1217_bootstrap_profiles.py,test_issue_1137_maintained_client_acquisition.py,test_issue_1221_vocabulary_maintained_client_acquisition.py,test_tooling_artifact_policy.pyandtest_issue_1313_workflow_policy.py: 238 passed.test_issue_1220_isabelle_acquisition.py: 93 passed, 11 failed. The same 11 fail on this host with dev's code (macOS temporary-directoryPermissionErrors, and Isabelle checks that support only Linux x86_64; tracked in Lock qualification and Isabelle acquisition tests fail on macOS #1536). CI runs them on Linux.-m integration, all six modules: 18 passed.-m fuzzselects no test in the 1217 module.Proof manifest checks on
578c6fec:uv run --project implementations/python --frozen python tools/check_participant_opacity_proof.pygets past manifest validation and stops atthe pinned Isabelle proof tool supports Linux x86_64 onlyon this Mac. With dev's manifest it stops atproof tool source digest does not match its repository source.tests/test_issue_963_participant_opacity_proof.py -m integration: 35 passed, including the six that failed in CI.tools/check_specification_coverage.pyexits 0, andtools/check_formal_semantic_validation.pyreportsFormal semantic-validation evidence bundle passed integrity and replay checks.nox -s contracts -- --base-rev origin/devpassed 14 stages.On
578c6fec,nox -s verify-fast-feedback -- --base-rev origin/devpassed: every stage PASS or SKIP, its ruff format and check stages passed on the tool file and the test, and the changed test module ran (45 passed).nox -s lintpassed. The pinned toolingruff formatandruff check, run fromimplementations/python, pass on the test.make policypassed 15 stages. Requirement governance was skipped: the branch has no requirement UID, and no scope file has ever existed for #1475.The changed source line is an argv element that every transfer test builds, so coverage does not change. The Bootstrap qualification workflow reruns the real-curl tests on Ubuntu x86_64, Ubuntu arm64 and macOS 15.
On
578c6fec, CI run 38056743267 passed and all 14 required checks pass (32 checks pass, deploy skipped), includingcanonical / proofandcanonical / integration. Bootstrap qualification run 38056743136 passed: the real-curl selection passed on Ubuntu x86_64, Ubuntu arm64 and macOS 15 (8 passed each), and the dev-container smoke passed. SonarCloud's quality gate is OK with no new issues.Ground Control Checks
make policyand the test runs are recorded in the Test Plan.Traceability
implementations/python/tests/test_issue_1217_bootstrap_profiles.py; also exercised:implementations/python/tests/test_issue_1220_isabelle_acquisition.py, which reuses_https_fixture, andimplementations/python/tests/test_issue_963_participant_opacity_proof.py, which validates the proof manifest.Checklist
builddoes not cut a release.