wip: Lean formalization of Flo / Gyatso / Hydro by shadaj · Pull Request #3190 · hydro-project/hydro

shadaj · 2026-09-05T22:37:29Z

No description provided.

cloudflare-workers-and-pages · 2026-09-05T22:37:30Z

Deploying hydro with Cloudflare Pages

Latest commit:	`bd61d05`
Status:	✅ Deploy successful!
Preview URL:	https://8ea0b930.hydroflow.pages.dev
Branch Preview URL:	https://sandbox-5a878146-15ba-4cec-b.hydroflow.pages.dev

View logs

…of, typed monotonicity framework, and executable bug falsifiers Completes the HydroLean formalization of Hydro programs in Lean 4 (no Mathlib, zero sorries, zero custom axioms): (a) collect_quorum with unbounded correctness proofs. (b) Medium programs: two-phase commit (with open-membership negative results), index_payloads, join_responses, sequence_payload. (c) Paxos (hydro_test/src/cluster/paxos.rs) ported 1:1 (one Lean file per Rust function, Programs/Paxos/) with the headline safety theorem proven over the real program denotation: theorem commit_agreement (hcb : ClientsMono cb) (hstab : LeaderBallotStable f cb nd) (hnA : nA ≤ 2*f+1) : (slot,v) ∈ (paxos_core guarded f cb nd).2 i → (slot,v') ∈ (paxos_core guarded f cb nd).2 i' → v = v' Cross-proposer slot-functionality of p_to_replicas, for all decision traces and all fuels. Rust nondet!/manual_proof! sites are materialized as named proof inputs (LeaderBallotStable = paxos.rs:186–189); the paxos.rs:862 key-nodup obligation and the B1/B2 guard facts are DERIVED. Proof spine: a single Nat-induction on forward_ref unfolding depth (p2a_chosen_agree) using quorum pigeonhole, promise-order internalization (K1), frozen-quorum-bucket pinning (SPChainQ/pinQ), and the scan invariants spKeys_inv/spCovered_inv. Axiom audit (Paxos/AxCheck.lean): propext, Classical.choice, Quot.sound only. Framework: - Hydro/TStream.lean + Hydro/ForwardRef.lean: decisions-as-inputs denotational semantics (ticks×collections, batch regimes = Rust ordering markers, forward_ref = higher-order Kleene fixpoint with fixpoint induction; gas-less bridges). - NEW Hydro/Growth.lean: Growth (⊑) class whose carrier instances mirror Rust ordering markers exactly (prefix / multiset / set, families pointwise) + bundled prefix-monotone maps (α →ₘ β) with one bundled primitive per combinator — prefix-monotonicity is now derived from types; all hand-written per-stage growth lemma stacks deleted. - NEW Hydro/MonoSing.lean: MonoSing = Rust `Monotonic` singleton bound; fold_monotonic pays an inflationary closure obligation at the definition site for a monotonic-singleton output type (mirror of Rust fold + AggFuncAlgebra::monotone + ApplyMonotoneStream). Executable falsification (`lake exe falsify`, ~60ms after build): - B1 (duplicate P1a broadcasts, paxos.rs:311–317): faithful model commits (0, some 20) vs (0, some 10) — real safety violation; guarded model agrees and genuinely commits (non-vacuity witness for the theorem). - B2 (every-tick recommit, paxos.rs:596–672/706–734): faithful emits duplicate (slot,ballot) keys; guarded emits once. - Compiling the falsifier exposed and fixed a vacuous a_log knot in the inherited model (deadlocked fixpoint; a_max_ballot now folds P1a batches productively as in paxos.rs, replies still block on a_log — write-before-ack preserved) and a Lean compiler eta-expansion pitfall that silently destroyed memoization (FINDINGS D14/D15; new standing rule: every headline theorem needs an executable inhabitation witness). Docs: README 1:1 Rust↔Lean table, DESIGN/ACCEPTANCE governance, FINDINGS (B1/B2/B3 Rust bugs with verified falsifier outputs, A1/A2 errata, D1–D15 methodology), SORRIES (zero), docs/00–10 methodology series. Co-authored-by: Infinity 🤖 <infinity@hydro.run> PR: #3190

…s-as-inputs architecture — Paxos safety by pure face composition, updated ACCEPTANCE, executable falsifiers HydroLean formalizes Hydro programs in Lean 4 (no Mathlib, zero sorries, zero custom axioms) under ONE architecture, now ratified in the rewritten ACCEPTANCE.md: decisions-as-inputs denotational semantics with typed monotone wires. All earlier architectures (choreographic/TypedGraphSys, sealed-component/Holds simulation) are retired; deliverables migrated; jj history is the archive. Headline (Programs/Paxos/Safety.lean), over the 1:1 port of paxos.rs: theorem commit_agreement (hstab : LeaderBallotStable f cbM nd) (hnA : nA ≤ 2*f+1) : (slot,v) ∈ (paxos_core guarded f cbM nd).2 i → (slot,v') ∈ (paxos_core guarded f cbM nd).2 i' → v = v' Safety.lean is now PURE FACE COMPOSITION (220 lines): commit_elim, p2a_chosen_agree (the one protocol induction), commit_agreement — zero references to module internals. All K3/K4 invariants live as generic verified faces in their owning modules (AcceptorP1 acceptorP1_ok_elim; PP1b pP1bPv_leader_len/view_promise/leader_providers; SequencePayload sp_emit_elim/sp_keys_face/sp_covered_value/sp_p_to_replicas_elim; JoinResponses joinResponses_zip_elim), instantiated at the run by the wiring layer (PaxosCore GuardedRun section: run views, LeaderBallotStable, pinQ, composed P2a faces, the a_log-knot provenance regress opened once). Framework (Hydro/): TStream (batch regimes = Rust ordering markers; Consumes legality), ForwardRef (Kleene fixpoint + fixpoint induction), Growth (⊑ mirrors the markers; bundled →ₘ maps; reader-lifted wire combinators; MonoMap.fix), MonoSing (Rust `Monotonic` bound via fold_monotonic's inflationary obligation). Proofs-through-types: each dataflow exists once as its typed stage; .f only at boundaries; sidecar growth lemmas forbidden (ACCEPTANCE §3). Program suite: Paxos; 2PC over the SAME shared collect_quorumM stage (twoPC_committed_eq + corollaries); collect_quorum QuorumSpec (a genuine iff — completeness forces emission); index_payloads; join_responses; n-of-n characterization. Open-membership retired to FINDINGS D20. Executable falsification (`lake exe falsify`): B1 duplicate-P1a faithful disagreement at slot 0 vs guarded agreement with genuine commit (non-vacuity witness); B2 recommit duplicate keys. Standing rule (ACCEPTANCE §4): every headline theorem needs an executable inhabitation witness. Docs: ACCEPTANCE.md rewritten (single architecture, deliverables ✅ with exact signatures, binding architecture terms, verification gates, falsification record, governance, explicit out-of-scope); README/DESIGN/ docs-00/01/06/07/09/10/99 synced; docs/02–05, 08, 98 historical; FINDINGS A-errata/B-bugs/C-contracts/D1–D20 methodology; SORRIES zero. Co-authored-by: Infinity 🤖 <infinity@hydro.run> PR: #3190

…ecture — Paxos safety from quorum intersection ALONE, causality derived from the fixpoint, executable falsifiers HydroLean formalizes Hydro programs in Lean 4 (no Mathlib, zero sorries, zero custom axioms) under one ratified architecture (ACCEPTANCE.md): decisions-as-inputs denotational semantics with typed monotone wires. Headline (Programs/Paxos/Safety.lean), over the 1:1 port of paxos.rs: theorem commit_agreement (hnA : nA ≤ 2*f+1) : (slot,v) ∈ (paxos_core guarded f cbM nd).2 i → (slot,v') ∈ (paxos_core guarded f cbM nd).2 i' → v = v' The ONLY input is quorum intersection. Every Rust nondet!/manual_proof! justification is now DERIVED, including leader-ballot stability (paxos.rs:185–188): `leader_ballot_stable` proves fabricated leadership self-destructs — solicitation is fixpoint-staged through the !is_leader trigger gate (paxos.rs:449), flag-false ticks require bucket masking, masking self-poisons, fabrication levels strictly ascend. Constituent faces live at their owning modules (PLeaderHeartbeat trigger gate, LeaderElection p1a elimination, PP1b bucket persistence/masking) and are composed at PaxosCore's wiring layer; Safety.lean is pure face composition (220 lines). Causality findings (FINDINGS D21/D22, docs/11): loops whose triggers route through forward_ref wires inherit tick-causality from the fixpoint — no framework causality machinery needed for Paxos. For gateless loops the shelved compiled design Hydro/CausalAvail.lean provides causalTickLoop (guarded per-tick fixpoint = Hydro atomic tick region; batchC is its constant-environment special case; CausalCuts is its elimination principle), with Programs/CausalToy.lean as the executable boundary witness. `lake exe explore` records the acausal-starvation / causal-healing experiment. Methodology refinement: nondet! comments that CLAIM guarantees are derived, not assumed — deriving them verifies the comment (D22: the paxos.rs comment under-explains its own justification). Framework: TStream (batch regimes = Rust ordering markers), ForwardRef (Kleene fixpoint + the one generic induction), Growth (⊑ mirrors markers; →ₘ bundled maps; wire combinators; MonoMap.fix), MonoSing (Rust `Monotonic` via fold_monotonic), CausalAvail (shelved). Proofs-through- types: dataflow exists once, .f only at boundaries. Programs: Paxos; 2PC over the SAME shared collect_quorumM stage (twoPC_committed_eq, an iff face); collect_quorum QuorumSpec (iff); index_payloads; join_responses. Open membership retired (D20). Executable falsification: `lake exe falsify` — B1 duplicate-P1a faithful double-commit vs guarded agreement with genuine commit; B2 recommit duplicate keys. Standing rule: every headline theorem carries an executable inhabitation witness. Docs: ACCEPTANCE (deliverables ✅, binding architecture terms, verification gates), docs/00–11 (02–05, 08, 98 historical), FINDINGS A-errata/B-bugs (B1/B2/B3 + D22 comment fix recommended upstream)/ C-contracts/D1–D22 methodology, SORRIES zero. Co-authored-by: Infinity 🤖 <infinity@hydro.run> PR: #3190

…intersection alone, module contracts at every signature, executable falsifiers HydroLean formalizes Hydro programs in Lean 4 (no Mathlib, zero sorries, zero custom axioms) under the ratified decisions-as-inputs architecture with typed monotone wires (ACCEPTANCE.md), now with the D23 contract discipline applied all the way down: *if a proof at layer X computes over the internals of a function Y it calls, the fact belongs on Y's signature.* Headline (Programs/Paxos/Safety.lean, 205 lines — one induction + the theorem), over the 1:1 port of paxos.rs: theorem commit_agreement (hnA : nA ≤ 2*f+1) : (slot,v) ∈ (paxos_core guarded f cbM nd).2 i → (slot,v') ∈ (paxos_core guarded f cbM nd).2 i' → v = v' Quorum intersection is the ONLY input. Every Rust nondet!/manual_proof! justification is derived, including leader-ballot stability (le_ballot_stable, LeaderElection's contract): fabricated leadership self-destructs because solicitation is fixpoint-staged through the !is_leader trigger gate (paxos.rs:449). Module contracts (each on its own I/O, hypotheses = named input requirements): AcceptorP1 ap1t_ok_spec/reply_echo/decode_cap; AcceptorP2 ap2t_ok_spec (write-before-ack surfaced on the signature)/log_entry; PP1b fabricated-reign regress over a solicitation oracle; LeaderElection le_ballot_own/le_ballot_stable/le_leader_view_promise/le_leader_providers/ le_view_pinned (promise witnesses = existential acceptor-tick indices into the a_log input and a_max output wires); SequencePayload sp_commit_spec/sp_emission_spec/sp_log_entry_spec/sp_emission_functional over SPWireDiscipline (= exactly LE's contract set). PaxosCore (525 lines) = pcHist + the a_log knot at the signature + contract instantiation + run_promise_covers (the one genuinely cross-module fact, via the shared Monotonic wires). No file references another module's internals — enforced by grep. Framework: TStream (batch regimes = Rust ordering markers), ForwardRef (Kleene fixpoint + the one generic induction), Growth (→ₘ bundled maps, wire combinators, MonoMap.fix), MonoSing (Rust `Monotonic` via fold_monotonic), CausalAvail (shelved causalTickLoop design for gateless loops; batchC = its constant-environment special case; FINDINGS D21 boundary rule). Programs: Paxos; 2PC over the same shared collect_quorumM stage (twoPC_committed_eq); collect_quorum QuorumSpec (iff); index_payloads; join_responses. Open membership retired (D20). Executable falsification: `lake exe falsify` (B1 duplicate-P1a faithful double-commit vs guarded agreement; B2 recommit duplicate keys), `lake exe explore` (acausal starvation / causal healing record). Standing rule: every headline theorem carries an executable inhabitation witness. Docs: ACCEPTANCE (deliverables ✅, binding terms, gates), docs/00–11, FINDINGS A-errata/B-bugs (B1/B2/B3 + D22 comment fix recommended upstream)/C-contracts/D1–D23 methodology, SORRIES zero. Co-authored-by: Infinity 🤖 <infinity@hydro.run> PR: #3190

…axos_core's type, module contracts at every signature, executable falsifiers HydroLean formalizes Hydro programs in Lean 4 (no Mathlib, zero sorries, zero custom axioms) under the ratified decisions-as-inputs architecture with typed monotone wires (ACCEPTANCE.md). The endgame of proofs-through-types (FINDINGS D24): THE PROGRAM'S TYPE IS ITS SPEC. Headline — paxos_core's signature itself (Programs/Paxos/PaxosCore.lean), over the 1:1 port of hydro_test/src/cluster/paxos.rs: def paxos_core (variant : PaxosVariant) (f : Nat) (c_to_proposers : (Fin nP → Stream (Ballot nP)) →ₘ (Fin nP → Stream P)) (nondet : PaxosNondet P nP nA) : (Fin nP → Stream (Ballot nP)) × {out : Fin nP → Stream (Nat × Option P) // variant = .guarded → nA ≤ 2 * f + 1 → SlotFunctional out} Cross-proposer slot agreement is a subtype field: an implication guarded by the bugfix flag (the faithful variant claims nothing), with quorum intersection as the only mathematical input; consumers project `.2.property rfl hnA`. The value components stay definitionally the 1:1 transcription (fold_monotonic pattern — proof attached at the boundary). `#print axioms paxos_core` audits the face: propext, Classical.choice, Quot.sound only. Every Rust nondet!/manual_proof! justification is derived, including leader-ballot stability (le_ballot_stable, LeaderElection's contract: the election trigger routes through the forward_ref cycle, so fabricated reigns cannot bootstrap — FINDINGS D21). Contract discipline (D23: a fact a caller needs about a callee belongs on the callee's signature): AcceptorP1/P2 (promise = a_log input at its tick; ack ⇒ log output covers the key — write-before-ack on the signature), PP1b (fabricated-reign regress over a solicitation oracle), LeaderElection (ballot ownership/stability, leader-view promise witnesses as existential acceptor-tick indices into its I/O wires), SequencePayload (commit/emission/log-entry specs over a wire discipline that is exactly LE's contract set). PaxosCore = wiring + the a_log knot + contract instantiation + K1 (run_promise_covers) + the single Nat-induction (emission_chosen_agree) paying the type's obligation. The Paxos directory is exactly the Rust file map + audit/falsification records — no "final assembly" file. Framework: TStream (batch regimes = Rust ordering markers, Consumes), ForwardRef (Kleene fixpoint + the one generic induction), Growth (→ₘ bundled maps, wire combinators, MonoMap.fix), MonoSing (Rust `Monotonic` via fold_monotonic), CausalAvail (shelved causalTickLoop for gateless loops; batchC = its constant-environment special case). Programs: Paxos; 2PC over the same shared collect_quorumM stage (twoPC_committed_eq); collect_quorum QuorumSpec (iff); index_payloads; join_responses. Open membership retired (D20). Executable falsification: `lake exe falsify` (B1 duplicate-P1a faithful double-commit vs guarded agreement with genuine commit; B2 recommit duplicate keys — outputs recorded in FINDINGS), `lake exe explore` (acausal starvation / causal healing). Standing rule: every headline carries an executable inhabitation witness. Docs: ACCEPTANCE (type-carried face quoted, binding architecture terms, verification gates), docs/00–11, FINDINGS A-errata/B-bugs (B1/B2/B3 + D22 comment fix recommended upstream)/C-contracts/D1–D24 methodology, SORRIES zero. Co-authored-by: Infinity 🤖 <infinity@hydro.run> PR: #3190

…c; HydroV2 tagless-final pilot Two packages on top of the completed Paxos formalization (zero sorries, standard axioms only, executable falsifiers): Package 1 — one `Verified` artifact per Rust function (COMPLETE). Every Paxos module is now a single def bundling `.f` (the 1:1 wire-let transcription, definitionally unchanged — props erase, falsifier output byte-identical), `.mono` (type-derived prefix-monotonicity), and `.ensures` (the module contract as an Ens over the artifact's actual output, variant-guarded where the guarantee needs the bugfix; ghost `have`s over locally-bound values, Verus-style). Composition of proved versions typechecks: the entire manual handoff/instantiation layer (run_discipline, run_* lemmas, proof-view def stacks pP1bPv/leRun/…) is DELETED — the typechecker is the handoff layer. ACCEPTANCE §2(c) quotes the Verified paxos_core signature; consumers project `.ensures cb rfl hnA`. `#print axioms paxos_core`: propext, Classical.choice, Quot.sound. FINDINGS D25 records the design + Lean elaboration lessons; D26 records a new upstream note candidate (paxos.rs:386–390 p_has_largest_ballot is provably identically true under tick atomicity). Package 2 — HydroV2 pilot (IN PROGRESS, separate HydroV2/ lib, v1 untouched). User-directed tagless-final redesign: one SPMD program text over located collections polymorphic in `HydroSem`, carriers mirroring hydro_lang (Stream ordering markers, KeyedStream, Singleton unbounded/monotonic, TickSingleton); nondeterminism = exactly Rust's nondet! sites (assume_ordering selections + snapshot cuts; legality-is-realizability); monotonicity GRADED BY TYPE (prefix / sub-multiset / per-key / value-order / vacuous-at-Unbounded); all properties by gluing instances, no per-program proofs. BallotCalc ported with #guards; FoldPaths acceptance tests green. Follow-on plan in HydroV2/README.md: graded MonoRel, the program-generic soundness/adequacy transfer theorem (compositional automatic correspondence), batch/keyed folds/fix, full V2 Paxos port, machine interpretation + falsifier perf benchmark. Verification: build green (67 jobs incl. HydroV2), zero sorries, all audits standard-axioms-only, `lake exe falsify` ALL PASSED (B1/B2 outputs unchanged), `lake exe explore` green, all V2 #guards pass. Co-authored-by: Infinity 🤖 <infinity@hydro.run> PR: #3190

@values

… port; v1 verified artifacts complete Two generations of the HydroLean formalization now coexist (zero sorries, standard axioms only, all executables green): V1 (HydroLean/, COMPLETE — the proven reference): decisions-as-inputs denotational semantics; every Paxos module a single `Verified` artifact (the 1:1 transcription + type-derived monotonicity + variant-guarded ensures); paxos_core's type carries SlotFunctional (guarded → nA ≤ 2f+1 → agreement) with only quorum intersection as input; every Rust nondet!/manual_proof! justification derived; composition typechecks correctness (no handoff layer); executable falsifiers (B1/B2) and the causality exploration record. V2 (HydroV2/, tagless-final pilot brought through a full Paxos port): - Grades.lean: THE anti-cheating architecture — stream content graded by Rust's (Ordering × Retries) marker pair with QUOTIENT carriers (List / Multiset / StutterSeq / RetryPool); whatever the marker refuses to promise is unobservable BY TYPE; consumers exist only as Quotient.lifts whose respect proofs consume the robustness obligations (commutativity, consecutive idempotence) — a non-idempotent operator under retries is ill-typed. - Sem.lean: one SPMD program text over located collections, polymorphic in the graded signature; ops mirror hydro_lang (broadcast/demux, sample_every introducing TO-ALO by stutter, timing decisions, weaken_retries); nondeterminism = exactly Rust's nondet! sites; fixStream/fixTick = forward_ref/complete_cycle as guarded Kleene iteration with fuel as a decision. - Values (graded denotation), MonoRel (graded relational instance — per-module Flo monotonicity is a two-liner projection), Trace (cut machinery; blocking legality = realizability). - Paxos/ (one file per paxos.rs fn, 11 files): full port incl. leader_election's 3 forward_ref cycles and paxos_core's a_log write-before-ack + seqMax knots; per-module Ensures contracts over @values; composition by contract only; paxos.rs:862's manual_proof! hole made checkable (canonical logView + ValWitness conflict degradation); SlotFunctional face stated and executably observed; `lake exe v2paxos` runs the end-to-end scenario (election → commit (0, some 42), slot-functional true). - M5 perf finding (measured): call-by-name Values evaluation compounds exponentially across knot boundaries (naive paxos_core: hours); boundary materialization (the eager-Machine staging) brings one run to ~105 s — strong empirical motivation for the Machine interpretation, staged in HydroV2/README.md along with the graded Sched/Corr transfer rebuild (pre-quotient incarnation validated the shape; recoverable from jj evolog d5cd22dbf29c), ALO functorial ops, iterate-projection lemmas, and the full V2 agreement derivation. Mathlib adopted (lemma library only; soundness mechanism is core Quotient). Verification: full build green (811 jobs), zero sorries, audits standard-only, `lake exe falsify` ALL PASSED, `lake exe explore` green, `lake exe v2paxos` exit 0. Co-authored-by: Infinity 🤖 <infinity@hydro.run> PR: #3190

@values

…ort (named decision types, transcription-first files); v1 verified artifacts complete Two generations of the HydroLean formalization coexist (zero sorries, standard axioms only, all executables green): V1 (HydroLean/, COMPLETE — the proven reference): decisions-as-inputs denotational semantics; every Paxos module a single `Verified` artifact; paxos_core's type carries SlotFunctional (guarded → nA ≤ 2f+1 → agreement) with only quorum intersection as input; all Rust nondet!/manual_proof! justifications derived; executable falsifiers. V2 (HydroV2/, tagless-final, full Paxos port): quotient carriers graded by Rust's (Ordering × Retries) markers (List/Multiset/StutterSeq/ RetryPool — illegal observation is ill-typed; consumers are Quotient.lifts paying commutativity/idempotence); one SPMD program text over the graded signature; fixStream/fixTick guarded Kleene cycles; graded MonoRel (per-module Flo monotonicity = a two-liner); 11 Paxos files (one per paxos.rs fn) with Ensures contracts over @values, composition by contract only; end-to-end executable scenario (`lake exe v2paxos`: election → commit, slot-functional true). File/type hygiene (this round): - Transcription-first layout: contract-only helpers (aMaxStep, foldEarlyStopBallots, SlotFunctional) moved below their program defs into marked contract sections — a file reads as the Rust mirror first, its verified vocabulary after; impl closure-bodies stay above. - Named decision types (HydroV2/Decisions.lean): BatchCuts / OrderedBatchCuts / SnapshotCuts / OrderSelection / SampleTimes / TimerVerdicts / TimingPulses / UnfoldFuel — every nondet decision parameter reads as a domain concept, docstrings naming the paxos.rs nondet! site each feeds; decisions structurally NESTED by owning module (PaxosCoreDec {le : LEDec {hb : PLHDec, p1b : PP1bDec, …}, sp : SPDec, fuels}) so callers pass callee decision bundles wholesale. Perf finding (measured, staged work): call-by-name Values compounds exponentially across knot boundaries; boundary materialization brings a paxos_core run to ~105 s — motivating the staged eager Machine interpretation. Also staged: graded Sched/Corr transfer rebuild, ALO functorial ops, iterate-projection lemmas, full V2 agreement derivation (HydroV2/README.md has the plan + build workarounds: Mathlib cache needs XDG_CACHE_HOME + LEAN_CC). Verification: build green (804 jobs), zero sorries, audits standard-only, falsify ALL PASSED, explore green, v2paxos exit 0. Co-authored-by: Infinity 🤖 <infinity@hydro.run> PR: #3190

…ontracts, fix HOF package, proved Paxos headline; v1 verified reference intact Two generations, both fully verified (zero sorries, standard-three axioms, all executables green): V1 (HydroLean/): the proven reference — decisions-as-inputs semantics, Verified artifacts, paxos_core type-carried SlotFunctional face, executable falsifiers (B1/B2) and causality exploration. V2 (HydroV2/): graded quotient semantics (markers → List/Multiset/ StutterSeq/RetryPool; illegal observation ill-typed) with the full Paxos port, now in its restructured final form: - Every module is ONE def: the pass/body as a reviewable `let` (Rust text first, reading order), returning its I/O function in a subtype whose colocated dependent-implication clause carries BOTH the unary Ensures contract AND binary Flo-monotonicity (the curried colocated mechanism, FINDINGS D27) — no external contract or mono theorems; composition is `.property rfl` projection; nothing re-spells a body. - paxos_core: single def closing the a_log/seqMax knots via fix_tick/fix_stream; colocated PCEnsures clause = the headline `variant = .guarded → mem acc ≤ 2f+1 → SlotFunctional out.2`, proof = paxos_core_agree (K4 layer in sibling PaxosCoreLemmas.lean: pigeonhole, stage vocabulary, knot-by-rfl, k+1→k provenance regress). - leader_election: single def (3 forward_ref cycles), curried clause with the four-leg mono; B1/B2 bugfix guards variant-gated. - Fixpoint HOF package (Trace.lean): fix_induction, iterate_val_proj (the iterate-projection principle), iterate_stab_of_fixed, fix_stabilizes. Unconsumed leaf mono theorems deleted. - Named nested decision types (Decisions.lean; PaxosCoreDec {le, sp, fuels} — callee bundles passed wholesale). - Staged with recorded designs: 6b fuel-free cycles (stabilization- search fix), proofs-at-the-end layout, graded Sched/Corr transfer, generic agreement theorem, eager Machine interpretation (perf: boundary-materialized v2paxos ≈ 112 s; naive is hours). Gate: build green (808 jobs incl. Mathlib), zero sorries, HydroV2 AxCheck (paxos_core, paxos_core_agree) + all v1 audits standard-three, `lake exe falsify` ALL PASSED, `lake exe explore` green, `lake exe v2paxos` OK (elects tick 1, commits (0, some 42), slot-functional true). Co-authored-by: Infinity 🤖 <infinity@hydro.run> PR: #3190

…emantics, relational coupling, Paxos safety at every schedule; v1 reference intact Two generations, both fully verified (zero sorries, standard-three axioms, executables green): V1 (HydroLean/): the proven reference — decisions-as-inputs semantics, Verified artifacts, type-carried SlotFunctional face, executable falsifiers, causality exploration record. V2 (HydroV2/): graded quotient semantics, full Paxos port, shared verified hydro_std layer (self-contained contracts, generic ScanRun combinators), and now the OPERATIONAL TRANSFER LAYER: - HydroSem signature with 11 instance-declared decision-type families; five instances of one program text: Values (denotation), SchedSem (the erased step machine: plain-list carriers, StepHist prefix-monotone histories on one global step clock, emergent fan-in from delivery timing, tick-skeleton pacing, consume-all-at-tick, fuel-less Kleene-diagonal fix; time model: idle steps unobservable, elastic-above/floored-below — floors exclude exactly the Zeno runs; FINDINGS D31), RelSem (set-valued nondeterminism), CorrSem (per-op couplings, totality = cheat detector over all ~39 ops), SquareSem (six-component relational carriers with lens decisions and δ-realizability — zero per-knot lemmas, type-derived monotonicity). - Theorems: sched_snap_eq + snapshot_tight/batch_tight (every machine run at every horizon couples to a denotational run at DERIVED decisions with EQUALITY at decision-mediated observations); per-wire StabilizesAt end-of-time kit + fix_diag_attains; adequacy (∀d ∃schedule) proven FALSE BY DESIGN with counterexample (the decision space deliberately over-approximates; safety needs only ⊆); adversary-coverage witness suite all #guard-enforced incl. the fixpoint-race overtaking scenario. - THE CLOSING THEOREM paxos_safe_sched (Paxos/SquareSafety.lean): SlotFunctional over the SchedSem instantiation at EVERY schedule and horizon — few-line body, only semantic premises; projection identities are theorems; δ-satisfiability discharged structurally. Zero per-program proof content (ruling: proofs per operator only). - FINDINGS D30 (design evolution incl. three dead drafts), D31 (time model), D32; README architecture + interpretations sections. Queued next (user-approval-gated, in order): (1) eliminate the remaining Paxos-specific proof machinery in SquareSafety(Id) via a per-op projection simp-set (no kernel blowup, no per-program content); (2) δ-witness record; (3) quiescent-completeness ("no more work ⇒ committed IS in output" — quiescence absorbs FLP); (4) fuel-less/lfp Values fix upgrade. Gate: child-verified green on identical tree (823 jobs, zero sorries, AxCheck standard-three, falsify/explore/v2paxos identical, witness suite green); parent re-gate scheduled post-compaction. Co-authored-by: Infinity 🤖 <infinity@hydro.run> PR: #3190

…projection simp set (D33) Replaces the per-program Square-transfer identities with a fully generic, per-operator lemma set, honoring the binding genericity rule (proofs per-operator only, never per-program/per-knot): - NEW HydroV2/SquareProj.lean (~1380 lines): for every HydroSem op, rfl projection lemmas at variable args relating (SquareSem …).op to its Values/SchedSem projections; instance-typed embed/input wrappers; typed decision constructors SqDec.*; Unit-decision normalizers; and the sq_transfer macro (simp only + with_reducible rfl, which fails fast if any lemma misfires instead of silently degenerating into whole-program defeq). - DELETED HydroV2/Paxos/SquareSafetyId.lean (six handwritten body identities; ~41-minute one-time kernel rfl). - HydroV2/Paxos/SquareSafety.lean rewritten: restated loop bodies pcBody/pcALogF/pcSeqMax removed; paxos_sq_rr/paxos_sq_sr are each one sq_transfer call over the program's def names; paxosSqDec spelled via SqDec.*; maxHeartbeats 25.6M → 3.2M; file elaborates in 16 s (was ~42 min). paxos_safe_sched unchanged in meaning (premises now typed at instance projections — definitionally identical carriers). - SquareTheory.lean slimmed (embeds/inputs moved to SquareProj and retyped at instance-projected types). - Attribute-only @[reducible] marks on 5 defs (FoldOkP, ValueOrder.nat, ValueOrder.multiset, Ballot.numVO/obtVO) fixing the reducibility- hygiene root cause: semireducible spellings blinded keyed matching, forcing deep defeq (the old 40-min mode and heartbeat bumps). Paxos program logic itself: zero changes. - AxCheck extended to the closing theorems (paxos_sq_rr/sr, paxos_safe_sched, cq_safe_sched — all standard-three axioms). - FINDINGS.md D33: root-cause writeup (reducibility hygiene, measured cost split, residual-dump + pp.explicit token-diff debugging method). Independently gate-verified after squash: full lake build green (823 jobs, no multi-minute file remains), zero sorries, standard-three axioms only, falsify ALL PASSED, explore green, v2paxos OK (elects tick 1, commits (0, some 42), announcement once, slot-functional true). Co-authored-by: Infinity 🤖 <infinity@hydro.run> PR: #3190

…ORRESPONDENCE.md, 2PC port, V1 retirement Cumulative session changes, each independently gate-verified after squash: 1. SquareProj/D33: deleted per-program transfer identities (SquareSafetyId.lean, ~41-min kernel rfl) in favor of generic per-op projection lemmas + sq_transfer macro; SquareSafety elaborates in 16 s; root cause (reducibility hygiene) recorded as FINDINGS D33. 2. HydroV2/CORRESPONDENCE.md (1037 lines): reader's guided tour of the Values↔Sched correspondence — Rosetta table mapping classic distsys concepts to artifacts, three annotated walkthroughs (cq_safe_sched, corr_values, paxos_safe_sched), batchDerive end-to-end with non-circularity argument, unbounded-commutative-folds section (CutDec chains: "a cut reveals and commits"), Sched trust-boundary audit with 13-row checklist, honest caveats. Pacing per-location gap found, ruled by user, documented (fix in flight). 3. C2 wave / FINDINGS D34: Eager interpretation (Eager.lean, EagerProj.lean + eager_transfer, Paxos/EagerCheck.lean pinning executables to the Values denotation by theorem); falsify (B1/B2, >30min → 5ms), explore, v2paxos (120s → 0ms) rebuilt as thin mains at Eager over V2 vocabulary; 2PC ported (TwoPC.lean + two_pc_unanimous/once/commit_iff + new v2twopc exe); V1 retired: HydroLean/Hydro + Programs deleted, Flo/Gyatso/Collections kept building; README/ACCEPTANCE/SORRIES/FINDINGS updated. Standing gate is now four sub-second exes: falsify, explore, v2paxos, v2twopc. Final gate on merged tree: lake build green (791 jobs), zero sorries, all axiom reports within propext/Classical.choice/Quot.sound, all four exes OK. Co-authored-by: Infinity 🤖 <infinity@hydro.run> PR: #3190

… repair (D35–D37) On top of the earlier consolidation (SquareProj/D33, CORRESPONDENCE.md, Eager execution, 2PC port, V1 retirement — see prior description), this wave hardens the trusted statement itself: 1. Per-member tick pacing (D35): pacing : (ℓ : L) → Fin (mem ℓ) → Nat → Bool across SchedSem/CorrSem/SquareSem; paxos_safe_sched strictly stronger with unchanged body; TransferChecks §9 asymmetric-tick reproducer; CORRESPONDENCE.md updated. 2. Sched red-team audit (D36): HydroV2/SCHED_AUDIT.md — Rust ground-truth summary with citations (dfir_rs, hydro_lang networking, paxos.rs transports), 17-row axis table, findings F1–F6 + 13-item faithful ledger. F1 Stage A: Square knot combinators hoisted, SquareProj _rl family + raw embed twins, SquareKnot.lean generic bridge discharge (knot δ ≡ telescope + fuel). 3. δ-vacuity repair (D37) — THE critical find: the fix ops' left reader bridge made hsat unsatisfiable for nested knots, so paxos_safe_sched was vacuously true for T ≥ 1 in a zero-sorry, gate-green tree. User-ratified repair: bridge replaced by the Values-only Kleene chain condition (exactly what cpl's gluing consumes); statement unchanged, δ now inhabitable. New SchedCausal.lean (~40-op causality family + stabilization roots), SquareDlt.lean (52 δ-projections), chain/ telescope kit in SquareKnot.lean, and ∃d validation theorems for single and nested knots at every schedule and horizon (sq_fix_dlt_exists_batch / _nested). Gate on merged tree: lake build green (794 jobs), zero sorries, standard-three axioms, falsify/explore/v2paxos/v2twopc all OK. In flight: F1 finale (sq_hsat macro → paxos_hsat → premise-free paxos_safe_sched'). Co-authored-by: Infinity 🤖 <infinity@hydro.run> PR: #3190

…hinery files deleted (D44, D45) Completes user queue item #3 ("all/most the files in Paxos that are not proving paxos-specific safety properties should disappear"): 1. Phase 2a (D44): HydroGen engine at program scale — decision-record support (field trees, generated Sched/Values/MonoRel/lower repacks), wire-bundle output legs, bound-directed mono relations, interleaved callee-rewrite ex-scripts; generated stacks validated for all 12 knot-free modules; cq_safe_sched'' proven on generated artifacts. User-ratified heartbeat policy: no engine budgets, call-site set_option only, timeouts treated as script bugs. 2. Phase 2b (D45): user-directed `hydro def`/`hydro_register`/ `hydro_inline` surface — composition specs recorded at definition time (strict body-grammar walker, errors at the definition); generators consume specs. All real Paxos targets green at DEFAULT heartbeats: 3 leader_election knots, leader_election + pcBody glue, pcAlogF (tick) and pcSeqX knots, and hydro_glue paxos_core (whole program). Compositional mono resolver; keyed memoized candidate matching (70s → 3.9s); reducible-only guarded tactics. 3. Deletion wave (~3400 lines of hand-written machinery): CoupleStd, CoupleModules, Paxos/CoupleKnots, Paxos/CoupleDec, HydroGenStage, HydroGenKnotStage, StageA all deleted. CoupleWf: 2722 → 92 lines (paxos_co_wf/cpl + paxos_safe_sched', meaning-identical, budget- free one-liners over generated paxos_core_co_*). CoupleSafety rebuilt at 115 lines. Command tails live in the program files. Paxos/ now contains: program modules + Types + safety-lemma files (PaxosCoreLemmas/PP1bLemmas/SequencePayloadLemmas) + the 92-line headline + scenarios (Falsification/Exploration) + EagerCheck/ EagerKnots (den projection; no generator yet, documented residual). Independently gate-verified after squash: lake build green (800 jobs), zero sorries, standard-three axioms (incl. paxos_safe_sched'), falsify/explore/v2paxos/v2twopc all OK. Co-authored-by: Infinity 🤖 <infinity@hydro.run> PR: #3190

Lands the transferrable-fairness architecture the user requested, correcting rung 1's machine-side framing: - NEW HydroV2/LivenessChain.lean (~490 lines, 1.4s): temporal combinators over decision-chain positions (◇/□/◇□/□◇/⟿ + calculus); fairness vocabulary in pure Values terms (Exhausts = WF(tick) denotationally; ChStabilizes = ◇□ leader-stability premise shape; ChSF for future lossy-retry work); cut chains with ◇=◇□ persistence; Values chain theorems carrying ALL protocol content (cq_complete_mem, cq_chain_live, cq_chain_live_stable); kit 1 (chain-fairness transfer: derived chains are legal+ascending, FairTicks makes them exhaust); kit 2 (tightness: machine observation = Values run at the derived point); headline cq_live_chain — rung 1's conclusion re-derived with few-line glue, quorum crossing consumed only through the Values contract. Theorem transfer restored for liveness. - LIVENESS.md rewritten as design of record: the correction arc (the user's leader-change and lossy-retry challenges → enabledness-based fairness → the chain move), re-anchored TLA+ Rosetta (behaviors → chains), the V∘K1∘K2 architecture, the revised ladder, open forks (rung-b premise style; EmitDec claim-streams recommendation strengthened; NEW skipping-cursor fork for lossy links). - FINDINGS D50; rung 1 (Liveness.lean) kept for comparison. Gate on merged tree: lake build green (807 jobs), zero sorries, standard-three axioms, falsify/explore/v2paxos/v2twopc all OK. In flight: the hydro-def surface-syntax thread (D51). Co-authored-by: Infinity 🤖 <infinity@hydro.run> PR: #3190

…r (D51) Lands the user-requested authoring surface. All term-level elaborators; generators untouched; program semantics byte-identical (all downstream theorems green with meaning-identical statements). 1. `hydro [hints]? (inline)? def` annotation (HydroV2/HydroDef.lean): one declaration elaborates the def, registers the composition spec, and runs the full generation pipeline (route from the spec). ~170 lines of command tails + hand-written knot defs deleted across the 11 program files; heartbeat budgets stay visible as set_option prefixes per the user ruling. 2. Inline `fix` blocks: `fix (w : τ, …) via fuels := body; rest` — mutual knots written in the let chain (the Rust forward_ref reading); the elaborator performs Bekić decomposition and hoists named `M.wire` + folded @[reducible] `M.wire.body` constants (the D40 proof-time law preserved). Hand-written knots (leFails/leIam/leFfx/pcAlogF/pcSeqF/pcSeqX, leCore) deleted. PaxosCore 47s → 23s; LeaderElection unchanged (~6 min). 3. Ghost layer (Verus-translatability shaped per user steer: proof structures decomposed along the program, not relocated): `τ ensures out => P` auto-generates the Values-contract subtype face; `ghost have/let/obtain` = spec-only bindings at program points, stripped from the computational leg, replayed post-subst in the proof leg; `value prove field := proof, …` assembles the contract field-wise. Pilots: both quorum defs; leBody (500-line proof decomposed via shared ghost facts); leader_election restructured (cycle wires as plain inputs; leCore eliminated; binary-mono face conjunct REPLACED by the generated leader_election_param free theorems at the mono instance — Flo monotonicity is now literally a free theorem, consumed as a 4-line corollary). LeaderElection.lean 1235→1107 lines, max width 524→84 chars. 4. FINDINGS D51 incl. the Verus-translatability table (contract face → spec fn, obligations → proof fns, ghost have → assert-by, etc.) and reserved next steps (invariant clauses on fix binders parsed but deferred; ghosts inside fix bodies). Gate on merged tree: lake build green (808 jobs), zero sorries, standard-three axioms, falsify/explore/v2paxos/v2twopc all OK. Co-authored-by: Infinity 🤖 <infinity@hydro.run> PR: #3190

shadaj force-pushed the sandbox-5a878146-15ba-4cec-bc5d-90d176c0d334 branch from 4a86a2a to 81d8cc5 Compare September 8, 2026 19:36

shadaj force-pushed the sandbox-5a878146-15ba-4cec-bc5d-90d176c0d334 branch from 81d8cc5 to 2b9ea00 Compare September 10, 2026 15:45

shadaj force-pushed the sandbox-5a878146-15ba-4cec-bc5d-90d176c0d334 branch from 2b9ea00 to 6b10747 Compare September 11, 2026 02:16

shadaj force-pushed the sandbox-5a878146-15ba-4cec-bc5d-90d176c0d334 branch from 6b10747 to 46915f5 Compare September 11, 2026 13:15

shadaj force-pushed the sandbox-5a878146-15ba-4cec-bc5d-90d176c0d334 branch from 46915f5 to 24267f8 Compare September 15, 2026 20:30

shadaj force-pushed the sandbox-5a878146-15ba-4cec-bc5d-90d176c0d334 branch from 24267f8 to 064a4bb Compare September 16, 2026 23:50

shadaj force-pushed the sandbox-5a878146-15ba-4cec-bc5d-90d176c0d334 branch from 064a4bb to d471e22 Compare September 17, 2026 18:17

shadaj force-pushed the sandbox-5a878146-15ba-4cec-bc5d-90d176c0d334 branch from d471e22 to cd22c55 Compare September 17, 2026 20:18

shadaj force-pushed the sandbox-5a878146-15ba-4cec-bc5d-90d176c0d334 branch from cd22c55 to 8326de8 Compare September 18, 2026 02:50

shadaj force-pushed the sandbox-5a878146-15ba-4cec-bc5d-90d176c0d334 branch from 8326de8 to 39f77aa Compare September 20, 2026 17:33

shadaj force-pushed the sandbox-5a878146-15ba-4cec-bc5d-90d176c0d334 branch from 39f77aa to 4bf0924 Compare September 20, 2026 22:54

shadaj force-pushed the sandbox-5a878146-15ba-4cec-bc5d-90d176c0d334 branch from 4bf0924 to 40cb9b8 Compare September 21, 2026 19:13

shadaj force-pushed the sandbox-5a878146-15ba-4cec-bc5d-90d176c0d334 branch from 40cb9b8 to c644b26 Compare September 21, 2026 20:17

shadaj force-pushed the sandbox-5a878146-15ba-4cec-bc5d-90d176c0d334 branch from c644b26 to 38c76c0 Compare September 21, 2026 22:37

shadaj force-pushed the sandbox-5a878146-15ba-4cec-bc5d-90d176c0d334 branch from 38c76c0 to 944c4fb Compare September 23, 2026 02:02

shadaj force-pushed the sandbox-5a878146-15ba-4cec-bc5d-90d176c0d334 branch from 944c4fb to e93336c Compare September 24, 2026 16:07

shadaj force-pushed the sandbox-5a878146-15ba-4cec-bc5d-90d176c0d334 branch from e93336c to 5d3bce8 Compare September 24, 2026 22:16

shadaj force-pushed the sandbox-5a878146-15ba-4cec-bc5d-90d176c0d334 branch from 5d3bce8 to e74636c Compare September 25, 2026 20:54

shadaj force-pushed the sandbox-5a878146-15ba-4cec-bc5d-90d176c0d334 branch from e74636c to bd61d05 Compare September 26, 2026 00:36

Navigation Menu

wip: Lean formalization of Flo / Gyatso / Hydro - #3190

wip: Lean formalization of Flo / Gyatso / Hydro#3190
shadaj wants to merge 1 commit into
mainfrom
sandbox-5a878146-15ba-4cec-bc5d-90d176c0d334

shadaj commented Sep 5, 2026

Uh oh!

cloudflare-workers-and-pages Bot commented Sep 5, 2026 •

edited

Loading

Uh oh!

This branch has not been deployed

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

shadaj commented Sep 5, 2026

Uh oh!

cloudflare-workers-and-pages Bot commented Sep 5, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Deploying hydro with Cloudflare Pages

Uh oh!

This branch has not been deployed

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

cloudflare-workers-and-pages Bot commented Sep 5, 2026 •

edited

Loading