diff --git a/proofs/README.md b/proofs/README.md index 34d51ffe..0d16031a 100644 --- a/proofs/README.md +++ b/proofs/README.md @@ -133,6 +133,57 @@ state destruction, but whether its ICE condition was transient remains unmeasured; #38's later roster recovery is external and is not credited to the ladder. +The model sweeps transient windows of 0.5, 1, 2, 3, and 5+ rungs against both + fail-fast and preserve-state candidates, with retention boundedness explicit. +It reports their divergence band and requires the separating measurement to +instrument the ICE condition and conntrack state directly, never file arrival. + +The retention precondition is a code question before it is a network question: + +| State a preserve-state rung would hold | Bound status | Cost / open question | +|---|---|---| +| WebRTC peer and ICE/DTLS sockets | BOUNDABLE | Holding a peer/socket for one rung costs roughly 15 seconds of resources; a lifetime policy does not exist today | +| NAT mapping and conntrack state | NOT OURS TO BOUND | Host defaults are `nf_conntrack_udp_timeout=30s` and `nf_conntrack_udp_timeout_stream=120s`; the five-rung ladder is 75s. The #50 dumps showed `[UNREPLIED]` entries, which use the shorter timeout, so the kernel can expire the state before the ladder finishes. The app can send traffic but cannot set the entry's lifetime. | +| QUIC transport file descriptor and UDP port | BOUNDABLE | One descriptor/port per retained transport for at most one rung; count is bounded per link and configured worker count, but the lifetime policy does not exist today | +| `direct_pending` expiry | BOUNDED TODAY | Pending state already has an expiry path | +| `buffered_offers` / `deferred_left` entries | BOUNDABLE | Per-peer entries are small, but a global retention ceiling would need to be designed | +| Active link slot | BOUNDABLE | Count one per peer; lifetime still follows the retained transport | + +The host check also showed live UDP entries in both states: `[UNREPLIED]` and +`[ASSURED]`. That matters because only the latter has the longer stream timeout; +the relevant #50 entries were `[UNREPLIED]`. This is evidence that conntrack is +not ours to bound for the ICE case, not evidence that every NAT flow expires in +30 seconds. The exact arithmetic from this host's operator-configurable kernel +defaults is decisive for the observed case: + +``` +nf_conntrack_udp_timeout 30s (UNREPLIED) +nf_conntrack_udp_timeout_stream 120s (ASSURED) +ladder 5 x 15s = 75s +#50's observed entries [UNREPLIED] +``` + +An `UNREPLIED` entry expires at 30 seconds, so it is gone before rung 3 of a +75-second ladder. An entry only earns the 120-second `ASSURED` timeout by +receiving a reply; #50's defining failure was that no reply arrived. The entry +therefore cannot be promoted and expires mid-ladder by construction. The +failure that prevents the reply is also what prevents the state surviving long +enough for the retries to use it. + +This closes the ICE/conntrack half of #63: bounded preserve-state cannot retain +that kernel-owned state, so fail-fast or a fundamentally different approach is +what remains and the expensive condition measurement is unnecessary there. It +does not close the QUIC fd/port case, where state is ours and a bound is +constructible, nor #31's transport-level data-freeze case, which is not +conntrack. The sysctl values are from this host and an operator can change them; +the arithmetic must be recalculated for a deployment with different defaults. + +If retention cannot be bounded, naive preserve-state without an explicit +lifetime bound is unsafe and fail-fast wins for that design. A bounded +preserve-state variant remains live: the sweep says the candidates diverge +across the full 0.5-5 rung range, so condition instrumentation remains worth +taking. This is an inventory only; it does not implement state preservation. + Gate 0 also reads `MAX_ATTEMPTS` from `cli/src/main.rs` and `WATCHDOG_SECS` from `cli/src/net.rs`; a source change fails the model until its calibration is explicitly redone. diff --git a/proofs/stall_ladder_model.py b/proofs/stall_ladder_model.py index 4343056f..35c92773 100644 --- a/proofs/stall_ladder_model.py +++ b/proofs/stall_ladder_model.py @@ -67,6 +67,37 @@ class Result: terminal: str +WINDOWS = ((0.5, "0.5"), (1.0, "1"), (2.0, "2"), (3.0, "3"), (5.0, "5"), (6.0, "5+")) + + +def candidate_result(window, fix, retention_bounded): + """Evaluate the two candidate fixes without using transfer completion as a clock.""" + if fix == "fail-fast": + return False, "hard-fail" + if not retention_bounded: + return False, "unsafe-unbounded-retention" + return window <= MAX_ATTEMPTS, ("recovered" if window <= MAX_ATTEMPTS else "hard-fail") + + +def candidate_sweep(retention_bounded): + rows = [] + for window, label in WINDOWS: + fail_fast = candidate_result(window, "fail-fast", retention_bounded) + preserve = candidate_result(window, "preserve-state", retention_bounded) + rows.append((label, fail_fast, preserve, fail_fast[0] != preserve[0])) + return rows + + +def sweep_guard(): + bounded = candidate_sweep(True) + divergent = [label for label, _, _, differs in bounded if differs] + expected = ["0.5", "1", "2", "3", "5"] + if divergent != expected: + raise SystemExit(f"SWEEP FAILED: expected bounded-retention divergence {expected}, got {divergent}") + if any(differs for _, _, _, differs in candidate_sweep(False)): + raise SystemExit("SWEEP FAILED: unbounded retention must not recommend preserve-state") + + def run_ladder(environment: Environment, attempts=MAX_ATTEMPTS) -> Result: """Run the ladder; return whether the ladder itself recovered the transfer.""" required = FAILURE_STATE[environment.failure_type] @@ -130,6 +161,7 @@ def explore(): def main(): coherence_guard() gate_0() + sweep_guard() for name, observation in CALIBRATIONS.items(): outcomes = [ run_ladder(Environment(transience, observation.failure_type, observation.discarded_state)) @@ -143,9 +175,17 @@ def main(): ] print(f"TRANSIENT + RETAINED STATE: later-rung recoveries={len(later_rung_successes)}") print("OBSERVED FAILURES: indistinguishable between (a) persistent conditions and (b) transient conditions whose required state the teardown discarded.") - print("SEPARATING MEASUREMENT: measure whether the transient window exceeds one watchdog rung while preserving the candidate's ICE/conntrack state.") + for bounded in (True, False): + rows = candidate_sweep(bounded) + divergent = [label for label, _, _, differs in rows if differs] + retention = "bounded" if bounded else "unbounded" + suffix = "" if bounded else " (preserve-state unsafe)" + print(f"CANDIDATES retention={retention}: divergent windows={divergent or 'none'}{suffix}") + print("RETENTION PRECONDITION: bounded retention is required before the condition measurement is worth taking.") + print("RETENTION DECISION: unbounded retention rules out preserve-state WITHOUT AN EXPLICIT LIFETIME BOUND; a bounded variant remains in the divergent set and still requires condition measurement.") + print("SEPARATING MEASUREMENT: instrument the condition directly (when the ICE pair becomes usable again and when the conntrack entry reappears), not when the file arrives.") print("#50 evidence: each drop destroyed ICE progress, sockets, mapped ports, and conntrack state; whether the underlying ICE condition was transient remains unmeasured.") - print("RECOMMENDATION: do not raise MAX_ATTEMPTS or WATCHDOG_SECS until transience is measured; persistent failure favors fail-fast, transient+discarded state favors preserving state.") + print("RECOMMENDATION: bounded retention diverges for windows 0.5-5 rungs; naive unbounded retention is unsafe. Measure the condition directly before choosing fail-fast versus bounded preserve-state.") if __name__ == "__main__":