Conversation
…L6 basis) CAGradedTransition.v: the monad paper's graded LTS (§"Graded adequacy") — every native ca_step relabelled by the signature it consumes (atomic s for the single-token rules, the compound s1∘s2 for the compound rules), a faithful relabelling: graded_step_sound (forget grade ⇒ ca_step), graded_step_complete (every ca_step carries a grade), graded_iff_step. Plus a graded Hennessy–Milner modality GForm/gsat with the graded diamond ⟨g⟩φ, sound and complete against the graded LTS (gdia_sound/gdia_complete). The basis for graded adequacy (the full graded-HML ⟺ quote-faithful-bisimulation iff rests additionally on the native bisimulation). Axiom-free; gate green.
…anslation CATranslation.v: the native four-sort source (caproc/caname/signed_term) erases into the unchanged pure rho proc/name (the carrier split, DR-21). Unlike the old S_tr (whose signed body was already pure), the native translation is mutually recursive — caname_tr (@t ↦ @(st_tr T); bound var 1:1), p_tr (for/send/par/drop), and st_tr ({P}_s ↦ the fuel gate for(t←N⟦s⟧){p_tr P | *t} with the body lifted past the gate binder(s), mirroring the old P_tr; T∥U ↦ par; S ↦ T_tr). N_tr/T_tr reused verbatim (sig/token shared). Definitional unfolding lemmas + closedness (N_tr_closed, T_tr_closed) under the audited hash_process/ground_process Section hypotheses (which become ∀-premises, so the lemmas stay "Closed under the global context"). Faithfulness / bisimulation build on this. Gate green.
CostMonad.v realises continued-gslt-cost-v2's central thesis (the title claim)
axiom-free: cost accounting is an endofunctor 𝔠 (indeed a monad) whose laws
"descend from the two constituent monoids". Modelled as the WRITER monad over the
product grade (sig × token) — the authority consumed (commutative, up to ≡sig)
paired with the temporal stack (free, Leibniz, the modulus):
- cost / cost_map + functor laws (cost_map_id, cost_map_compose);
- η = cost_eta, μ = cost_mu (flatten 𝔠² by COMBINING grades — the nested-meter
flatten the old bare-proc SSigned could not even type), both natural;
- the three monad laws (cost_left_unit / cost_right_unit / cost_assoc) reduced
to grade_op_unit_r / unit_l / assoc, themselves the two monoids' laws;
- non-idempotence: cost_mu_modulus_accumulates (μ adds the moduli via
token_size_concat) + cost_monad_not_idempotent (a concrete witness).
All laws stated pointwise up to cost_equiv ⇒ NO functional extensionality. Gate
green; "Closed under the global context".
…st lemmas
CATranslationLemmas.v: the native locally-nameless commutation infrastructure the
faithfulness proof consumes (design doc §3 module 1), all by ca_mutind:
- L2: lift_st_to_proc / subst_st_to_proc — the dequote-collapse target st_to_proc
commutes with lift and subst (needed at the CPDeref/Eq dequote leaf);
- lift_lift_comm: the general lift/lift permutation (cutoffs c2 ≤ c1), plus the
0-cutoff instance lift_lift_0_caname used at binders;
- L1: lift_subst_ca — the native lift/subst commutation (cutoff c ≤ index n) that
RhoSyntax lacks; the CPInput binder case consumes lift_lift_0_caname, the
CPDeref/Eq dequote case consumes L2.
Index cases discharged by an interleaved simpl+destruct(leb|compare)+convert+lia
brute force. Pure CASyntax facts (no Section/hypotheses) ⇒ Closed under the global
context. Records the arbitrated faithfulness design + progress tracker in
docs/theory/cost-accounting-native-faithfulness-design.md. Gate green.
…r/T_tr invariance CATranslationFaithfulness.v opened: the Section over the audited hash/ground hypotheses with Local Notations Nt/Tt/Pt/Ct/St for the translation specialised to this Section. Foundation lemmas: in-Section closedness (Nt_closed/Tt_closed, mirroring CATranslation) and the lift/subst invariance lemmas Nt_lift_inv / Nt_subst_inv / Tt_lift_inv / Tt_subst_inv — the translated signature/token images are closed, hence inert under the substitutions a COMM performs (used pervasively in the per-rule gate-firing simulations). Builds toward the depth-aware commutation (L3), dequote-collapse bisimilarity (L4), and the forward-simulation headline. Gate green; "Closed under the global context".
… (L3 prerequisite)
Identified that RhoSyntax provides only lift_zero_proc, not the proc-level lift/lift
composition the depth-indexed faithfulness bridge needs. Added it to
CATranslationLemmas.v (proc_ind_mut with explicit motives, since proc has no
Combined Scheme):
- lift_lift_compose_proc: c1'≤c1≤c1'+d1 ⇒ lift_proc d2 c1 (lift_proc d1 c1' P)
= lift_proc (d1+d2) c1' P (nested-cutoff lift composition);
- lift_proc_S_compose: the instance lift_proc d 1 (lift_proc 1 0 Q) = lift_proc (S d) 0 Q
used to relate the depth-indexed st_tr_d to lift_proc∘st_tr.
Design doc progress tracker updated: CATranslationLemmas (L1/L2/lift_lift/proc-lift)
and the CATranslationFaithfulness Section + invariance foundation are committed and
gate-green; the remaining layered core (st_tr_d+bridge → L3 → L4 → per-rule → Thm A
→ Thm C) is recorded with the L3 crux flagged. Gate green.
…+ bridge
The structural vehicle for the L3 commutation. CATranslationLemmas.v: added
lift_lift_comm_proc (proc-level lift/lift commutation, c2≤c1; the proc analog of
the caproc lift_lift_comm). CATranslationFaithfulness.v:
- st_trd (d,c): the depth-indexed mutual translation (p_trd/cn_trd/st_trd) that
threads a lift (shift d at cutoff c), so the L3 substitution commutation has a
clean structural IH rather than brittle after-the-fact lift_proc bookkeeping;
- trd_bridge: st_trd d c X = lift_proc d c (St X) (and the p_trd/cn_trd legs) by
ca_mutind — the gate cases push the gate's lift_proc {1,2} 0 body shift past
the depth lift via lift_lift_comm_proc, the channels stay inert by
Nt_lift_inv / closed_proc_lift_zero;
- st_trd_zero: St = st_trd 0 0 (lift_zero), so St stays the public translation.
Axiom-free; gate green.
…ion complete Records that the entire structural/equational layer of native faithfulness is committed and gate-green (L1/L2, caproc+proc lift/lift commutation + composition, N_tr/T_tr invariance, the depth-indexed st_trd + the trd_bridge + st_trd_zero), and the verified KEY FINDING that fixes the remaining shape: the per-rule substitution commutation is NOT a syntactic equality (subst_proc (St T) 0 (Quote (St U)) keeps the gated PDeref(Quote(St U)) where St(subst_st…) has the stripped Pt(st_to_proc U)); and PDeref(Quote Q) is STUCK under rho_step (PDeref_Quote_stuck). Hence the per-rule simulations are operational + coinductive (weaving in L4's stuck-residue bisimilarity over RhoReduction's rs_comm), not discharged by the (now complete) equational layer. This scopes the remaining core (L4 → per-rule → Thm A → Thm C) precisely.
…on (2 COMMs) First concrete per-rule operational simulation. rule1_unit_reachable: the translated rule-1 redex (atomic SUnit) reduces in two rho COMMs to PPar (subst_proc (St T) 0 (Quote (St U))) (Tt t) — the gate COMM (gate_body_subst) then the released for|send COMM. Corrects a prior misanalysis: subst_proc SEMANTICALLY dereferences — subst_proc (PDeref (NVar 0)) 0 (Quote Q) = Q, not a stuck PDeref(Quote Q) — so the gate's *t releases the stack tail Tt t LIVE, and the result's token part matches St(RHS) exactly. The sole residual gap is the payload body at *x-force positions (St U gated vs Pt(st_to_proc U) stripped), i.e. the dequote-collapse for the bisimulation layer; away from forces the per-rule match is exact. Design doc updated with the corrected operational facts + the per-rule firing map (1/2/5 direct, 3/4 need Split). Gate green.
…tomic signatures rule1_reachable: generalizes rule1_unit_reachable from SUnit to ANY atomic signature s (SUnit/SGround/SQuote) via an inner `fire` helper — the atomic gate shape (channel Nt s = token channel) fires identically for all three; SAnd is excluded (combined-token routing needs a Split mediator) by the side condition (∀ a b, s <> SAnd a b). Two COMMs to PPar (subst_proc (St T) 0 (Quote (St U))) (Tt t). Gate green.
…on (split, 3 COMMs) rule5_reachable: the fully-split rule (separate receiver/sender gates, separate tokens; both signatures atomic). Three rho COMMs via a generic fire5 helper — ≡-rearrange ((g1|g2)|t1)|t2 ≡ (g1|t1)|(g2|t2) (se_par_assoc + se_par_cross), fire g1|t1 and g2|t2 (each gate channel = its token channel, no Split needed), then ≡-rearrange (PInput|t1)|(POutput|t2) ≡ (PInput|POutput)|(t1|t2) and fire the for|send. Reaches PPar (subst_proc (St T) 0 (Quote (St U))) (PPar (Tt t1) (Tt t2)), which is ≡ St(RHS). SAnd signatures excluded (need Split). Gate green.
…on (nested gate) rule2_reachable: the combined-process gate (signed SAnd s1 s2) with PRE-SPLIT tokens (TGate s1 t1, TGate s2 t2). The nested two-gate fires outer-on-Nt-s1 then inner-on-Nt-s2 against the two split tokens — needing NO Split mediator (gate channels equal the split token channels for ANY s1, s2, so no atomicity side condition), then the released for|send fires. Three COMMs via two new helpers: nested_gate_subst (outer firing, lift 2→1 by subst_lift_two_one, first payload deref) and gate2_body_subst (inner firing, lift 1→0, second payload deref). Rules 1, 2, 5 (the directly-firing, no-Split rules) now have operational simulations; 3, 4 (combined token TGate (SAnd s1 s2)) need the Split mediator. Gate green.
…ed-token rules 3/4) The native port of Translation.Split: Split s1 s2 receives a token on the compound channel Nt (SAnd s1 s2) and produces an s1-token (empty payload PNil) + an s2-token forwarding the dequoted payload. Split_closed (via closed_PInput + closed_name_at_mono) and Split_fires (the one-COMM operational behaviour: PPar (Split s1 s2) (POutput (Nt (SAnd s1 s2)) Q) ⇝ PPar (POutput (Nt s1) PNil) (POutput (Nt s2) Q)). This is the mediator the combined-token rules 3 and 4 route their token through (in parallel context) before the gates fire. Gate green.
…on (Split, 4 COMMs) rule3_reachable: the combined-process gate (signed SAnd) with a COMBINED token, routed through the Split mediator (parallel context). Four rho COMMs: Split fires (combined token → s1-token empty + s2-token carrying Tt t), outer gate fires on Nt s1 with the empty token (nested_gate_subst, Q1=PNil), inner gate fires on Nt s2 with Tt t (gate2_body_subst, R=PNil), the released for|send fires. ≡-rearrangement (se_par_comm/assoc/cong) brings each redex adjacent; the empty s1-token leaves an inert PNil residue (PPar PNil (Tt t) ≡ Tt t). Plus reachability congruences rho_reachable_par_l/r and the helper split_body_subst. Rules 1, 2, 3, 5 now have operational simulations; only rule4 (split processes + combined token) remains. Gate green.
…les operational rule4_reachable: the last reduction rule — split processes (separately-signed receiver/sender), combined token, routed through Split. Four COMMs (Split → s1/s2 tokens, receiver gate on Nt s1 with empty token, sender gate on Nt s2 with Tt t, released for|send), no Join (GAP-2: continuation keeps its own seal). With this, ALL FIVE native reduction rules (ca_rule1..5) have operational forward simulations into pure rho: rules 1/2/5 fire directly, rules 3/4 via the Split mediator. The token-handling is faithful throughout (subst's semantic deref releases stack tails live); the sole residual is the payload dequote-collapse for the bisimulation layer. Gate green.
…simulations complete Records the milestone: every native reduction rule (ca_rule1..5) now has a proven operational forward simulation into pure rho — rules 1/2/5 fire directly, rules 3/4 via the Split mediator; the token-handling is faithful (subst's semantic deref releases stack tails live), the sole residual being the payload dequote-collapse for the bisimulation layer. Documents the general-theorem assembly plan (one-step progress over the 5 leaf rules + ca_par via rs_struct; ca_rule4/5 carry general s1,s2 so nested-SAnd sigs need a recursive Split / old PersistentSplit — the atomic-leaf fragment is covered).
…ss (progress) ca_translation_progresses: the general ∀-ca_step faithfulness headline — ∀ S S', ca_step S S' → ∃ Ctx W, closed_proc Ctx ∧ rho_step (PPar (St S) Ctx) W — every native reduction step's translation makes real progress (no deadlock) in a closed mediating context (PNil for the directly-firing rules 1/2/5, the Split mediator for the combined-token rules 3/4 and the compound-gate first step). By induction over ca_step: the five leaf rules each fire their gate/Split COMM, and the ca_par_l/r congruences lift the inner step through PPar via rs_struct (absorbing the Ctx-rearrangement ≡). This packages the five per-rule simulations into one theorem over the whole reduction relation. Axiom-free; gate green.
…mit (finding) Records the genuine, native-only semantic finding blocking a full strong bisimulation: at a force (*x) of a received signed term, the source dequote strips the gate (st_to_proc U — the content runs, already metered) while the translation's force yields the GATED St U (a stuck receiver, no token for s'), so St U and Pt(st_to_proc U) are not strongly bisimilar. The native gate translation over-gates at force points (the old bare-proc-continuation model never saw this). A full strong bisim needs a translation refinement (force cashes the signature / two-level quote-vs-force) — research-grade, not a mechanical port. The progress theorem + the five per-rule reductions stand independently; the strong bisim holds cleanly only on the gate-free-continuation fragment.
…ming
CASettlement.v re-homes Settlement.v onto the native four-sort grammar. The fee
arithmetic (charged/refund/escrow on the fee_settlement record) is
carrier-independent and reused verbatim from Settlement; the calculus link is the
NATIVE st_total_fuel measure:
- ca_funded_reachable_monotone: on the hereditarily-funded fragment (HF), fuel
is non-increasing along ca_reachable (via funded_step_decreases + HF_step) —
the conditional-SN form (off the funded fragment fuel can rise, DR-21);
- ca_evaluation_step_cannot_mint_fuel (a funded step strictly decreases fuel);
- ca_post_evaluation_settlement_no_mint (charged + refund = escrow with the
native consumed count) and ca_settlement_refund_is_unconsumed (refund = the
un-consumed fuel × price). Full clean rebuild + gate green; axiom-free.
…yering
CAMintingInjection.v re-homes MintingInjection.v's core onto the native grammar:
- mint_inject_st S t = STPar S (STStack t) (exogenous token injection) +
mint_inject_st_fuel (adds exactly token_size t);
- funded_ca_step_does_not_mint (a funded ca_step never raises fuel, via
funded_step_decreases — the conditional-SN form vs the old unconditional
token_monotone_step);
- mint_inject_st_not_ca_step (injecting a non-empty stack into a funded system
is not a ca_step — it would raise fuel strictly);
- the native interleaved-administration model (ca_admin_trans over CAStep/CAMint)
+ ca_admin_fuel_classified (fuel motion classified by the operation).
The base of the native economic dependency chain (unblocks the native Exchange).
Full rebuild + gate green; axiom-free.
…homing CAExchange.v re-homes Exchange.v. The 1:1 swap conservation (carriers_total invariant; per-channel datum + value-exact swap) is carrier-independent count arithmetic, re-exported for the native model (ca_exchange_total_conserved / ca_exchange_swaps_values). The native calculus characterization ca_exchange_is_step_not_mint: a swap is a FUNDED ca_step (fuel-non-increasing — moves tokens between carriers, never mints) and exogenous minting is never such a step (built from CAMintingInjection's funded/mint lemmas). Full rebuild + gate green; axiom-free.
…carrier-independence CAEconomicCapstone.v consolidates the native carrier-dependent economic core into one funded-fragment guarantee (ca_economic_conservation): along any HF evaluation, fuel is conserved (never minted), fee settlement balances exactly (charged + refund = escrow), and no exogenous mint is realizable as a ca_step — assembling CASettlement + CAMintingInjection + CAExchange. Documents that the remaining economic modules are carrier-INDEPENDENT and hold for the native model verbatim: MintingHalt (PoS-state), RuntimeBudgetRefinement / MultiSignerRefinement (runtime model), LinearLogicResources / LLIdentities (resource calculus, Stdlib-level); the SlashingComposition / MergeableChannelAccounting boundary conservation reduces to ca_funded_reachable_monotone. Stage 5 economic re-homing complete. Gate green.
…bisimulation
CABisimulation.v: ca_single_gate_bisimilar — the native analogue of the old
Bisimulation.translation_strong_bisimilar_generic. Firing a native signed term
{P}_s (atomic s) against a co-present unit token reaches a residue strongly
bisimilar (the Bisimulation.bisim coinductive) to the released body p_tr P. This
is the bisimulation that holds cleanly: a single gate fires (gate-unwrap COMM +
the inert unit-token residue handled by multi_stuck_residue_bisim), with NO inner
signed-term substitution at a force position — so the force-collapse obstruction
(§3a) that blocks a strong bisimulation across an arbitrary multi-COMM ca_step
does not arise. Same strength as the old model's strong-bisim result, ported to
the four-sort grammar. Gate green; axiom-free modulo the audited hypotheses.
…ingle-gate bisim) Marks the native faithfulness modules complete relative to the old model's guarantee: CATranslationFaithfulness (5 per-rule reductions + the general progress theorem ca_translation_progresses) and CABisimulation (ca_single_gate_bisimilar) together MATCH and EXCEED the old model's complete faithfulness (whose translation_faithful is weak and whose strong bisim is single-gate only). The full-ca_step strong bisimulation is force-limited (§3a) — a documented research discovery (the translation over-gates at force points; needs a force-cashing refinement), not an unfinished mechanical task; the old model never proved it either.
…CL6 graded adequacy CL8 (CALocatedPurses.v): phlogiston capability is spatially located on signature surfaces — local_sufficiency_composes (local sufficiency at each surface composes to total sufficiency), draw_disjoint (a draw at one surface leaves all others untouched — the Rocq image of lane_pool_disjoint + the TLA+ LocatedPurse model), draw_preserves_disjoint_sufficiency. CL6 (CAGradedAdequacy.v): graded Hennessy–Milner adequacy — graded_bisim (the signature-graded strong bisimulation, refl+sym) and graded_adequacy_sound (graded-bisimilar states satisfy the same graded-HML formulae) + graded_hml_distinguishes. Constructive — NO Classical/funext/choice (per mandate); about the native ca_step's graded transitions, so independent of the translation's force-limit. The soundness direction holds without image-finiteness; the completeness is the standard image-finite HM theorem. Gate green; axiom-free.
…rget) CAAdjunctions.v: the cost-accounting apparatus is a detachable layer. cost_install (Free — install the unit grade) / cost_forget (Forget — strip it), with cost_forget_install (Forget∘Free = id), cost_install_natural / cost_forget_natural (both functors natural), and cost_install_forget_alters (Free∘Forget ≠ id — structure-preserving, behaviour-altering). Realised structurally on the Cost writer monad. Adjunction II (internalisation up to weak bisimulation) is the force-limited one (delivered at the achievable strength by ca_translation_progresses + ca_single_gate_bisimilar). Gate green; axiom-free.
Adds the four continued-gslt-cost-v2 diagrams (unicode box-drawing, cross- referencing the Rocq modules): cost-endofunctor-monad (𝔠 + η/μ + the two monoids the laws descend from), cost-two-adjunctions (Free⊣Forget complete; internalisation at achievable strength + the force-limit), interaction-cut (the five gated COMM rules + the per-rule firing map), located-capabilities-spacetime (located surfaces + disjoint lanes + temporal token order). Runtime confirmed: cargo nextest -p models -p crypto green (no regression).
…pe discipline CATypeDiscipline.v re-exports the OSLF/DILL linear-resource discipline for the native model: linearity (ca_linear_identity / ca_linear_no_contraction — no double-spend), multiplicative (lolly consumes input / conservative flow), additive (with requires both / plus consumes chosen), exponential (bang reuse free / whynot no linear cost), and the funding judgment (sig_algebra consumed matches presented / threshold quorum sound). These are carrier-independent (LinearLogicResources is defined over the resource/sig_algebra abstractions, not the calculus carrier), so they hold for the native four-sort model verbatim. Gate green; axiom-free.
…ng module) Adds an additive module doc comment (no behavioral change) to the rholang accounting module witnessing the formal correspondence to the Rocq Cost monad: η↔unmetered budget (cost_eta/cost_install), μ↔per-COMM charge accumulation (cost_mu, non-idempotent), located capabilities↔per-signature DashMap lanes (CALocatedPurses.draw_disjoint / ChannelSeparation.lane_pool_disjoint), graded transition ⟨a⟩_s↔signature-keyed billable events (graded_step), linear no-double-spend↔resource-logic/Δσ (CATypeDiscipline). Complements the full correspondence doc; the loom reconciliation test already cites ChannelSeparation.v.
…iteness CAGradedImageFinite.v: the signature-graded transition relation is IMAGE-FINITE. An explicit successor enumeration graded_succ (redex steps at the top via redex_succ over the five gated rules, with the for/send channel-equality check caname_eq_dec, plus the par steps) with the full characterisation graded_image_finite: graded_step S g S' <-> In S' (graded_succ S g) (graded_succ_sound by structural decomposition; graded_succ_complete by induction on graded_step + eq_dec-reflexivity rewriting). This is the constructive basis the Hennessy-Milner COMPLETENESS direction needs to form the finite conjunction of distinguishing formulae — no Classical/funext/choice. Gate green; axiom-free.
1. Merge current dev coverage, transport, API, cryptography, and test infrastructure changes. 2. Preserve typed legacy and protocol-v6 deploy identities with exact repeat-deploy fallback behavior. 3. Make carrier publication, cache validation, watermark initialization, and pruning safe under failures and concurrent access. 4. Add TLA+ and Apalache controls plus Rust property, Loom, rollback, retry, and race regression tests. 5. Align merged model, Rholang, node, RSpace, comm, and block-storage fixtures with current APIs. 6. Document the consensus invariants, recovery sequence, verification evidence, and operational failure behavior.
dylon
temporarily deployed
to
ephemeral-launch-internal
September 2, 2026 21:47 — with 
GitHub Actions
Inactive
GitHub Actions
Inactive
dylon
temporarily deployed
to
oci-credentials
September 2, 2026 21:51 — with
GitHub Actions
Inactive
GitHub Actions
Inactive
1. Route the crash-retry test through the existing certified DAG test wrapper. 2. Preserve the production requirement that normal block admission carries certified sender authority. 3. Exercise the same feature configuration that CI uses without relying on test-internals.
dylon
temporarily deployed
to
ephemeral-launch-internal
September 2, 2026 22:09 — with
GitHub Actions
Inactive
GitHub Actions
Inactive
dylon
temporarily deployed
to
oci-credentials
September 2, 2026 22:09 — with
GitHub Actions
Inactive
GitHub Actions
Inactive
1. Preserve unresolved block identities when tracker invariants reject impossible over-capacity states. 2. Add Loom coverage for concurrent admission, release, and identity preservation. 3. Bind carrier-index atomicity fixtures to certified authority and finalized-floor commitments. 4. Update REST deploy fixtures and API documentation for the protocol v6.1 schema. 5. Record the new concurrency tests in the formal verification traceability table.
dylon
temporarily deployed
to
ephemeral-launch-internal
September 2, 2026 22:38 — with
GitHub Actions
Inactive
GitHub Actions
Inactive
dylon
temporarily deployed
to
oci-credentials
September 2, 2026 22:41 — with
GitHub Actions
Inactive
GitHub Actions
Inactive
The split_byte signature changed from i8 to u8, but the blake2b512_random_deep_split_chain_should_be_deterministic test still cast its index to i8, breaking the crypto lib-test build (E0308) and failing CI Lint.
1. Bind protocol-v6 admission, finalization, and merge decisions to exact authenticated state-effect provenance and authority-floor identity. 2. Make durable finalization publication, projection, lifecycle settlement, and snapshot capture atomic, restart-safe, monotonic, and stale-worker resistant. 3. Preserve exact deploy occurrence identities, terminal lifecycle evidence, accepted and rejected effects, and query results across full causal closures. 4. Freeze active committee authority, validator generations, objective equivocation evidence, and recovery scheduling against local or arrival-order drift. 5. Add exhaustive TLA+, Apalache, Rocq, Loom, example, generated-property, replay, storage, API, and concurrency regression coverage. 6. Extend conformance matrices, threat models, protocol specifications, API references, glossaries, and verification gates with executable traceability. 7. Remove the unmaintained bitmap dependency and eliminate duplicate block-storage integration-test registration.
1. Merge remote dev at 3759334. 2. Preserve the full u8 split range and stable two's-complement byte encoding. 3. Update Rholang evaluation and boundary checks to use the unsigned interface. 4. Retain the crypto golden vector and 129-send reduction regression. 5. Record the semantic merge audit and memory-bounded verification evidence.
jeffrey-l-turner
added a commit
that referenced
this pull request
Sep 5, 2026
- Add docs/casper/design/decision-ledger with an index and eleven entries that compare dev with PR #216 on each Casper consensus decision - Each entry records both positions, the divergence, the options, one unification proposal, and a ratification checklist - Add eleven Proposed rows dated 2026-09-05 to the CONSENSUS_PHILOSOPHY decision table, one per entry, with the flip rule stated - Link the ledger from the casper README design-analyses row
jeffrey-l-turner
added a commit
that referenced
this pull request
Sep 5, 2026
- Review why PR #216 removed phloLimit and phloPrice and what replaces each function - Record that the primary cause in the decision records is adoption of the token model, and that the multi-wallet and ownership-transfer specification gaps are real - Propose ratification at the protocol-6 boundary on three specification conditions, including a maintainer decision on client exposure - Register the entry in the ledger index and the philosophy table
jeffrey-l-turner
added a commit
that referenced
this pull request
Sep 5, 2026
…D-12 - Describe the ApportionmentPolicy trait on PR #216, its consensus contract, and the balanced default that drains the combined pool first and then each component equally - Add sub-decision 12.4 that reserves a client-selected policy as a future protocol-6 parameter, with sequential and proportional draws as candidates - Add open questions on more than two wallets and on wallet order
jltatbeach
pushed a commit
that referenced
this pull request
Sep 6, 2026
- Add a review record that compares the CbC ledger and formal-verification practice on dev, PR #387, and PR #216 - Classify each CbC and FV position on PR #216 as ratified, unratified, or in conflict with dev - List the open questions the integration change must answer - Link the record from the casper README design-analyses row
jltatbeach
pushed a commit
that referenced
this pull request
Sep 6, 2026
- Add docs/casper/design/decision-ledger with an index and eleven entries that compare dev with PR #216 on each Casper consensus decision - Each entry records both positions, the divergence, the options, one unification proposal, and a ratification checklist - Add eleven Proposed rows dated 2026-09-05 to the CONSENSUS_PHILOSOPHY decision table, one per entry, with the flip rule stated - Link the ledger from the casper README design-analyses row
jltatbeach
pushed a commit
that referenced
this pull request
Sep 6, 2026
- Review why PR #216 removed phloLimit and phloPrice and what replaces each function - Record that the primary cause in the decision records is adoption of the token model, and that the multi-wallet and ownership-transfer specification gaps are real - Propose ratification at the protocol-6 boundary on three specification conditions, including a maintainer decision on client exposure - Register the entry in the ledger index and the philosophy table
jltatbeach
pushed a commit
that referenced
this pull request
Sep 6, 2026
…D-12 - Describe the ApportionmentPolicy trait on PR #216, its consensus contract, and the balanced default that drains the combined pool first and then each component equally - Add sub-decision 12.4 that reserves a client-selected policy as a future protocol-6 parameter, with sequential and proportional draws as candidates - Add open questions on more than two wallets and on wallet order
Preserve the accumulated PR 216 campaign changes for review. This checkpoint
does not claim completed CI qualification, a successful soak, or upstream
ratification of branch-specific Casper architecture.
Major changes:
1. Update accounting authority validation, acceptance, SystemVault handling,
runtime integration, and their example-based and generated regressions.
2. Add bounded host-work accounting and runtime supervision across models,
Rholang execution, replay, and node integration.
3. Strengthen finalized-floor, certificate, sender-authority, and admission
state handling, including persistent ledger and deploy-occurrence checks.
4. Update proposer, recovery, initialization, and state-readiness integration.
Preserve explicit upstream review boundaries in the decision records.
5. Add state-import, root-selection, checkpoint-publication, sparse-store,
and transaction-failure correctness work with dedicated regression cases.
6. Introduce paired pending dependency and request-policy publication.
Preserve captured dependency provenance across worker handoff and retry.
7. Keep exact request-owner identity through asynchronous completion,
deferred persistence, terminal cleanup, and replacement callbacks.
8. Align ordinary transport retirement, retry clocks, and quarantine renewal
with pinned dev behavior. Separate durable pending provenance from retired
transport state, and remove expired-budget probe exceptions.
9. Distinguish local quarantine refusal from capacity refusal under the
registry lock. Preserve worker leases and count only capacity refusals
in the capacity metric.
10. Add concurrent publication, completion, retirement, and renewal tests.
Cover failed retired-budget transfer, repeated request-policy histories,
cold pending traversal, and same-owner recitation between retry steps.
11. Expand TLA+ models and exact unsafe controls for publication, authority,
recovery, storage, accounting, retry ownership, and activation outcomes.
Model due observation separately from selection and retain an explicit
counterexample to the unsupported atomic-current-due claim.
12. Add and update Rocq proofs, kernel-check gates, generated invariant tests,
and production-helper Loom checks. State finite bounds and correspondence
limits rather than treating component proofs as whole-node equivalence.
13. Update soak qualification collection, workflow checks, and diagnostic
scripts without claiming that a qualification soak has passed.
14. Expand permanent architecture, accounting, security, operational, decision,
and evidence documentation. Record dev as the Casper authority and keep
unresolved SME decisions distinct from demonstrated local bug repairs.
15. Preserve regression seeds, source-linked evidence, milestone records,
verification runners, and formatting changes accumulated in this campaign.
Verification at this checkpoint:
- The existing full publication formal gate passed before the final bounded
activation and no-probe model updates: 29 safe TLA+ configurations,
122 expected counterexamples, 68 theorem reports, and five kernel checks.
- The final activation model passed 58,968 states and six unsafe controls.
- The revised operation model passed 49,804 states, seven unsafe controls,
sixteen Rocq theorem reports, and an independent kernel check.
- The final native run passed 61 retriever tests, 35 ownership tests, and
nineteen worker tests, plus strict Casper/node library-and-test Clippy.
- Eight focused production-helper Loom tests passed before the final
diagnostic-only source update. They are component checks, not whole-node
concurrency qualification.
- Detailed native, lint, Loom, and formal results are recorded in
docs/work-logs/task-pr216-buffer-publication-2026-09-08.md.
Remaining campaign requirements and proof limits remain explicit in the
documentation and pgmcp. This commit is a review checkpoint, not a declaration
that all campaign tasks or end-to-end consensus qualification are complete.
jeffrey-l-turner
added a commit
that referenced
this pull request
Sep 10, 2026
- Add a review record that compares the CbC ledger and formal-verification practice on dev, PR #387, and PR #216 - Classify each CbC and FV position on PR #216 as ratified, unratified, or in conflict with dev - List the open questions the integration change must answer - Link the record from the casper README design-analyses row
Contributor
Casper integration decisions — ratification meeting, 16 September 2026The team ratified the following dispositions at the 16 September 2026 meeting. Meeting record and ratification proof: D-01 through D-12 review on PR #390. PR #390 records the decisions. This comment states their consequences for PR #216. Ratification does not establish that the implementation or verification work is complete. AuthorityUse current The accounting paper controls accounting requirements. It does not independently authorize changes to Casper committees, fork choice, finality, recovery, or slashing. Required dispositions
Align PR #216 specifications, decision records, wire definitions, and implementation with these dispositions. Preserve the rejected proposals as history, not as current authority. The linked meeting record controls where an earlier ledger proposal differs from the selected disposition. Protocol activation and pending correctness claims remain subject to their stated evidence conditions. |
Contributor
Ratification follow-up — separate conformance and soak harness PRThis follow-up implements the evidence requirements from the 16 September 2026 ratification meeting. Prepare the harness additions on a separate branch and PR. Keep deterministic conformance tests distinct from long-running soak profiles. Do not activate deferred PR #216 policies merely because the harness can execute them. Required profiles
Evidence requirementsRetain exact node and harness revisions, deterministic seeds, configuration, run identifiers, metrics, and artifacts. Identify the baseline and experimental policy for each comparison. Report failed, timed-out, and incomplete runs explicitly. Do not treat a soak result as formal proof or as authority to activate a deferred policy. The team must review the evidence before reconsidering deferred policies. FIPS approval remains required where a selected change affects the protocol. |
jeffrey-l-turner
added a commit
that referenced
this pull request
Sep 16, 2026
…-018 - Scope EPIC-017 to the pre-PR-#216 phase: models, current-dev reference bindings, baseline conformance, and harness preparation - Retitle TASK-017-5 through TASK-017-13 so each task supplies models and baseline evidence and names its post-merge owner in EPIC-018 - Add EPIC-018 (blocked on EPIC-017) with six tasks that gate on the actual PR #216 merge SHA, rebind claims and harness interfaces, verify the merged node, run the post-merge soak campaign, and discharge post-merge claims - Rewrite the branch plan integration section as Phase A, Phase B, the handoff, and shared conditions, and propose the follow-on branch name - Update the work log and Active Coordination entry for the two-phase plan
Contributor
|
Ledger entry D-07, sub-decisions 7.1 and 7.2. @leithaus @metaweta , you are the final ratifiers for these decisions. Please confirm or correct the reading below in a reply. The ratification record of 2026-09-16 lists exact occurrences, tombstones, and reason joining as current dev rules to preserve. Dev holds no occurrence store and no tombstone, so the record cannot mean they exist today. Under the meeting's own rule, PR #216 supplies a rule for a demonstrated defect. DR-33 documents the duplicate-occurrence storm, and R-REASON-CONFLUENCE removes a block body that changed with parent arrival order. Both are protocol changes, since occurrence identity and record keys are protocol. The consistent reading is the one the meeting applied to D-04, D-08, and D-10: sub-decisions 7.1 and 7.2 are ratified for protocol 7 under the D-08 activation conditions, and dev keeps signature-keyed records until then. The D-07 entry on dev (decision ledger) leaves the two sub-decisions unflipped until this confirmation. It will link this thread when they flip. |
jeffrey-l-turner
added a commit
that referenced
this pull request
Sep 19, 2026
Two maintainer decisions on 2026-09-19. D-07 ratified as reading A - The ratifiers jeffrey-l-turner, dylon, and spreston8 confirmed reading A. Sub-decisions 7.1 and 7.2 flip from preserved-as-absent to ratified as rules to build. PR #216 supplies the implementation, and its merge is the gate. - The node gains an occurrence store, exact tombstones, a record key of deploy signature and source block, and the four-value reason join through that pull request. No separate implementing task is created. - Section 8 moves from open to answered. The 2026-09-16 decision bullet no longer withholds the flip. - The recovery profile's synthetic occurrence schema stays a specification of future node behavior. - Recovery adapter qualification for CLAIM-CASPER-SOAK-004 now waits for the PR #216 merge rather than for a decision, because a pre-merge node has no occurrence store to observe. The authority and publication adapters do not wait. The tracker, the preparation log, and the handoff note say so. - Sub-decision 7.4, collective coverage, stays deferred. The one-parent B1 predicate stays, and the 2026-08-20 B1 row keeps its pending liveness guarantee. - The proof link is still to be attached. The record says so plainly. Soak runner memory approved at 64 GB - The maintainer approved 64 GB per runner, correcting the 48 GB figure in the original proposal. That figure was an error by the preparing session, which cited the fleet default without checking the soak workflow's own override. - The workflow already sets RUNNER_MEM_GB_OVERRIDE to 64, and its comment says to keep that knob in step with the ceiling. - The sizing invariant needs about 60,416 MB, from a 45,056 MB ceiling, about 7,168 MB of host overhead, and an 8,192 MB floor. A 64 GB machine leaves about 5 GB of headroom. A 48 GB machine overruns by about 11 GB, so the floor fires before the ceiling can attribute the growth. - A ceiling small enough to fit 48 GB would sit near 33,792 MB, below the 36,008 MB peak that smoke run 31547587950 reached while fully healthy. Runs 31390673884 and the PR #228 wedge fix record the same failure twice. - This changes no workflow file and no runtime file, so no mandatory CLAIM-CASPER-SOAK-001 artifact changes and no renewal is needed. - The remaining dispatch blockers stand. The launcher selects amd64 only, and the daily path rebuilds an image instead of selecting both pinned candidates. The handoff note also drops four facts that went stale during the day.
jeffrey-l-turner
added a commit
that referenced
this pull request
Sep 19, 2026
…216 The maintainer amended the execution contract on 2026-09-19. The follow-on epic may now start from the PR #216 head instead of waiting for that pull request to merge. What the contract required before - External dependency: PR #216 in state merged and an ancestor of origin/dev. - Start gate: the accepted EPIC-017 handoff and a verified merge, with the explicit sentence that an open candidate head is insufficient. - Branch policy: create the follow-on branch from updated dev after the gate passes. What it requires now - External dependency: PR #216 open or merged. The ancestry requirement moves to the merge of the follow-on pull request rather than to its start. - Start gate: the accepted EPIC-017 handoff. The branch may start from the PR #216 head before that pull request merges. - Branch policy: cut the branch from the PR #216 head and target that pull request, then retarget to dev after PR #216 merges. Record the PR #216 head revision at branch creation, the actual merge revision, and the baseline revisions. The amendment is recorded in the contract itself rather than applied silently. It states the earlier requirement, the reason for the change, and the cost. Stacking starts the branch from a revision that can still move, so the owner rebases on each PR #216 update and records the revision it verified against. Unchanged by design - Discharge of a post-merge claim still requires the actual merge revision. The interface contract keeps its separate rule that an open candidate head cannot satisfy the merge gate for evidence. Stacking changes where work happens, not what counts as proof. - EPIC-018 owner confirmation stays inside EPIC-017. TASK-017-13 keeps that prerequisite, and handoff acceptance still covers it. - The branch plan document carries the same amendment. The 2026-09-16 work log keeps its historical wording. The tracker parses, the STE check passes, and the strict audit is unchanged at exit 0 for all eight claims.
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
6 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
This PR replaces external Rholang cost tracking with the cost-accounted Rho calculus: an internalized metering model in which each billable
COMMevent—a matching send/receive reduction—consumes authorized phlogiston from a signature-scoped supply.The new
RuntimeBudgetandMeteredMachineremove the legacyChargingRSpaceprecharge/refund path, preserve deterministic consensus cost under concurrent execution, and retain stable error aggregation. Existing Rholang source remains valid because metering is introduced by the compiler and runtime rather than through new required surface syntax.The implementation is accompanied by mechanized proofs, bounded model checking, property tests, fuzz targets, concurrency models, threat analysis, and explicit documentation of the remaining implementation-refinement boundary.
What changed
Runtime metering
COMMrefund bookkeeping with source-token consumption.Funding and settlement
phloPriceandphloLimit; cost is now the number of billable source-token consumptions.Signatures and deploy interfaces
rholang-parserto the published revision containing the required cost-accounting syntax support.Consensus and security integration
Verification
The formal suite separates unbounded mathematical claims from bounded executable models:
The branch verification campaign recorded:
nextesttests passing after integration withdev.CI now includes the pure evaluator and cost-accounting Loom model crates and derives the slashing axiom-freedom checks from the complete theorem set.
Compatibility and rollout
phloPriceandphloLimitand may optionally submit cosigners or a signature-algebra envelope.Documentation
The rationale, semantics, security assumptions, decisions, and proof boundaries are covered in:
Need help on this PR? Tag
@codesmith-botwith what you need. Autofix is disabled.