R2 If-Match race probe: the instrument that grounds r2_conditional_put_linearizability

[gunbai-bot]

What this builds. The discriminating run that extdeps.cloudflare.r2 r2_conditional_put_linearizability's read_obligation names. This PR does NOT change that row. A follow-up flips it only on a passing receipt, and only if the receipt shows: curl >= 8.2 observed, declared_rounds=200, rounds=200, verdict=passed, and zero inconclusive rounds.

How a round works (gunbc.cloudflare.r2_conditional_put_race_probe, loop in .dag, run in-process by gunbc run):

1. Seed the probe key (probe/r2-conditional-put-race/head in the workspace bucket, never a head) with an unconditional PUT and read back its ETag.
2. Race two If-Match PUTs on that tag, with bodies distinct from the seed and from each other, in ONE curl invocation (-Z --parallel-immediate). Both transfers read the one netrc placed through gunbc.cloudflare.r2_s3_netrc from fabric_workspace_standing's pinned write credential, which is shredded after.
3. Delete the key and write the receipt.

Overlap is a fact read on one clock (route 3), never inferred from durations. curl's per-transfer %{time_*} values are offsets from each transfer's own start and share no origin, so they cannot show overlap. Instead the same invocation writes --trace-ascii --trace-time --trace-ids into the round's private directory.

• extdeps.tools.curl curl_trace_reading parses it into events stamped by the one process clock.
• Any stamp lower than the line before it refuses the whole trace, which catches a clock stepping backwards or midnight passing.
• Send-header bytes, which include the Authorization header, are dropped and never reach an event. Only the uploaded body is kept, and it is what attributes each transfer to its writer.
• RaceOverlap is Established only if both writers' last body send precedes both first response headers.
• The stated limit, in the module and on the receipt: this is client-side "sent before either was answered", not the order requests arrived at the store.

Verdict, a pure fold (race_probe_verdict):

• Falsifies: two 2xx, whatever the timing.
• Consistent: one 2xx and one 412 with overlap established.
• Inconclusive: everything else, namely both 412, any other status, no answer, an unseeded round, overlap not established, a short run, or zero rounds.
• Pass: every declared round is consistent. Falsified and inconclusive both exit non-zero.

Version gate. A new row, curl_trace_ids_cli_tool (>= 8.2, for --trace-ids), joins the existing curl pin family. The run reads curl --version and compares it to that row's own floor through extdeps.version.semver, which gains semver_core_of_dotted and semver_minimum_of_constraint, the latter admitting only a >= floor. A version below the floor, or one that cannot be read, refuses before any credential or round, and the observed version still goes into the receipt.

Run route. Fleet-converge mode r2_conditional_put_race_probe: shared job, no host scope, its own concurrency group, and its own 30-minute Duration step budget. It is defined in gunbc.fleet.fleet_converge_workflow and gunbc.ci.ci_spec, with fleet-converge.yml regenerated through tools.generated_artifact_gate main_wet_one. The receipt artifact is r2-conditional-put-race-probe-receipt. It names the transport version, the limit, each round's statuses plus its overlap fact and verdict, the cleanup result, and the final verdict.

Evidence.

• test.claim.r2_conditional_put_race_probe: 17/17 PASS (claim_batch on BuildBuddy). Its controls:
  • double-2xx falsifies, with or without overlap;
  • a split without overlap is inconclusive;
  • both-412, 5xx, 403, unreported and unseeded rounds are inconclusive;
  • a short or empty run never passes;
  • the all-consistent positive control passes;
  • the sequential counterexample: durations that look overlapped while the shared clock shows them sequential stay unestablished;
  • a backwards clock step anywhere refuses the trace;
  • TLS data never counts as a body send;
  • a planted Authorization header, key id and signature never reach a parsed event;
  • the argv carries the trace flags once, and the write-out parser reads exactly what the builder emits;
  • the version gate accepts 8.5.0 and 8.2.0, refuses 7.81.0 and refuses garbage;
  • only a >= constraint names a floor.
• extdeps.version.semver: 13/13 PASS.
• CI green at 94ad4e8.

🤖 Generated with Claude Code

[gunbai-bot]

On review 77021:

1. Workflow not regenerated. Agreed, that is the outstanding item. It is being regenerated through tools.generated_artifact_gate main_wet_one --arg path=.github/workflows/fleet-converge.yml on the merged head. The first attempt was OOM-killed under a 16 GiB bound and is rerunning on a larger runner. The regenerated YAML will land in this PR; it will not be hand-edited.

2. Quadratic accumulators. Not changing these, because on this runtime concat(acc, [x]) is not a copied accumulator. v1_rt rc_list_concat does Rc::make_mut(&mut a).extend(b.iter().cloned()): it extends the LEFT operand in place, on the persistent im carrier the interpreter's Value::List shares, and clones only the RIGHT operand. So each step costs |right| (one element here), not |acc|. std.nat nat_range_accumulate records this as the corpus's cost contract. Its annotation says the quadratic form is the opposite one, concat([x], tail), and prescribes exactly the append-to-accumulator shape used here. length(acc) reads the vector's stored length. The curl fold's per-step right operand is one transfer's argument words.

— sent from cool-wren-269

[gunbai-bot]

On review 77083:

1. Timestamps lose their unit. Fixed in db3242d. race_latest and race_earliest now return Microsecond? through race_later / race_earlier, and race_overlap_of_instants takes four Microsecond values. The count is read only inside each comparison.

2. Copied accumulators. The two numbering folds (race_witnesses_of and the receipt lines) now map(enumerate(...)), which also removes length(acc). race_rounds keeps concat(acc, [round]) deliberately, because it is not a copied accumulator on this runtime. v1_rt rc_list_concat is Rc::make_mut(&mut a).extend(b.iter().cloned()) over the persistent im vector the interpreter's Value::List shares: it extends the left operand in place and clones only the right one, so each step costs one element. std.nat nat_range_accumulate records this as the corpus's cost contract and names concat([x], tail) as the quadratic shape. The rounds are effects in sequence, so there is no list to map over without first building one the same way.

— sent from cool-wren-269

[gunbai-bot]

On review 77168: correct, and fixed in 5ec34ab. The merge commit had kept the branch's side of the generated fleet-converge.yml, which predated main's ClaudeCodeOauthHarnessToken option. The file is now regenerated on the merged head through tools.generated_artifact_gate main_wet_one, not hand-merged. Against origin/main its diff is only the r2_conditional_put_race_probe mode option, its concurrency group and its two steps, and the credential choice matches host_custody_credential_options again.

— sent from cool-wren-269

[gunbai-bot]

On review 77176:

• curl_trace_kind_is: agreed, deleted in a31c176. CurlTraceEventKind is four unit variants, so curl_trace_instants now filters on e.kind == kind.
• race_round_falsifies / race_round_inconclusive: kept. RaceRoundVerdict has a payload arm, RaceRoundInconclusive { cause }, so 'is inconclusive' has no == spelling: it is an elimination that ignores the cause. Each is that match, exhaustive over the three arms with no wildcard, consumed by the two filters in race_probe_verdict that pick each witness list. Inlining the same match into both filter lambdas would change the spelling, not the concept.

— sent from cool-wren-269

[gunbai-bot]

On review 77181: correct, fixed in c6867d4. CurlTraceScan.last_at is now Microsecond. It starts at microsecond(count: 0), takes the event's at unchanged, and the monotonicity check compares two microsecond_count reads at the comparison. The backwards-step control exercises it.

— sent from cool-wren-269

[gunbai-bot]

On review 77183: changed in 83b5369. race_rounds is now map(nat_range_inclusive(lo: 1, hi: n), r => race_round(...)), one effectful round per element in order, with no accumulator in the probe. A declared count that is not a natural yields no rounds, and the verdict reads that as a short run: inconclusive. (The earlier reply's runtime point still holds: rc_list_concat extends in place, which is the contract std.nat documents for nat_range_inclusive itself. The range is now the one std authority instead of a second hand-rolled loop.)

— sent from cool-wren-269