Fix Rings paper accuracy and evaluation scope

[RyanKung]

Summary

• tighten the paper's implementation, verification, and evaluation claims so Rings-specific measurements remain explicit obligations
• correct the replica-placement model by separating placement keys from effective live owners
• clarify cryptographic carrier boundaries, signed frame sequencing, and security-control limits
• remove duplicate Chord figure, clean narrow table/layout issues, and rebuild papers/rings.pdf

Validation

• latexmk -xelatex -interaction=nonstopmode -halt-on-error -file-line-error rings.tex
• pdftoppm -png -r 150 papers/rings.pdf tmp/pdfs/rings-rereview-render/rings
• rendered-page visual check for the updated PDF
• git diff --check -- papers/rings.tex papers/rings.pdf

[RyanKung]

Review of this PR. The direction is right, and the repository-facing claims in the new verification table were checked against the code and all hold: Stateright stages 1–4 (predecessor update, star discovery abstraction, storage CRDT, hand-off S2') match crates/core/src/tests/default/dht_stateright.rs, trace replay exists (dht_trace_replay.rs), the E2E replay/final-marker tests exist (crates/core/src/message/e2e.rs), and the byte-to-point adapter exists (crates/core/src/ecc/elgamal/impls/secp256k1.rs). No dangling \refs remain after the figure/table removals, and dropping enumitem is safe (the only bracketed list was removed too).

However, several of the newly introduced formal statements are inconsistent with the implementation or with the paper itself:

1. papers/rings.tex:981 — the new win component contradicts the implementation and breaks the frame's security semantics. The signed encrypted frame is redefined as f=(sid,seq,last,cipher,pk_s,σ_s,win), but the implementation's E2eStreamFrame carries only stream_id/sequence/is_final/ciphertext (crates/core/src/message/e2e.rs:68); reorder_window is receiver-side E2eStreamDecryptor state (e2e.rs:117, with_reorder_window), not a wire field. Moreover m_f = sid‖seq‖last‖cipher does not cover win, so as defined, SeqOK(sid,seq,last,win) depends on an unsigned, sender-controlled field — an attacker could supply an arbitrarily large window. win should be modeled as a receiver policy parameter (e.g. a subscript on SeqOK), not a frame component. This is precisely the accuracy class this PR sets out to fix.

2. papers/rings.tex:899 — the second conjunct of the Placement invariant is a consequence of the first, hence vacuous. Since U = owner_N[K] and O = owner_N[P], K ⊆ P ⇒ U ⊆ O by monotonicity of the image. The live-owner side that motivated the split (realized redundancy may collapse; obligations when |O_k| < ρ) is not captured by this invariant — it is equivalent to its first conjunct alone.

3. papers/rings.tex:1122 — the Replay row drops "nonce", contradicting the Replay rejection obligation immediately below. The new required boundary reads "TTL, stream order, final marker", but the obligation at rings.tex:1144 is nonce deduplication: accept(s,η,t) ⇒ η ∉ Seen_s. Stream order and the final marker only cover in-stream replay; cross-stream message replay still relies on the Seen_s mechanism the same section formalizes.

4. papers/rings.tex:991 — SeqOK is used but never defined. The Methodology (rings.tex:191) states that claims are carried by definitions; the new conjunct in FrameValid references an undefined predicate. The window semantics (strict increase? out-of-order acceptance within the window? rejection after final?) are exactly the content-bearing part of the implementation (e2e.rs pending/consumed idempotence) and deserve a definition.

5. papers/rings.tex:1133 — Base ⊬ Sybil ∧ Anon ∧ DoS treats attack predicates as goals. Read literally, "the base layer does not entail the Sybil attack ∧ anonymity ∧ DoS" is trivially true and the opposite of the intent (the base layer does not provide these resistances). It should use resistance predicates (¬Sybil / SybilResist, etc.).

6. papers/README.md:8 — stale doc and orphaned asset. This PR removes the only \includegraphics of imgs/rings/path.png, but the README still says "image asset referenced by rings.tex", and the PNG remains in the repository with no remaining reference. Given the preceding "prune stale resources" work, both should be cleaned up in this PR.

7. papers/rings.tex:202 vs rings.tex:1175 — two notations for the same object. The contribution set names Explore_Γ; the definition names Explore_{scope} = ModelCheck(→,Γ). Likewise the abstract's stratification uses Evidence_Γ ∪ Obligation while the Methodology uses Ev_Γ ∪ Obl. A paper whose selling point is precision should use one name per object.

8. papers/rings.tex:1292 — Axis(S)=(m,o,q,r) coordinates are never glossed, and q, r collide with symbols already in use. Throughout the paper r is the successor-list length and q is the group order |𝔾|=q (also the ranking-event variable); reusing them as comparison coordinates forces the reader to reverse-engineer the axes from the table. Name the coordinates and pick non-colliding letters.

Findings 1 and 2 run directly against the PR's own stated goals (accuracy; the replica-placement correction), so I'd address those first.

[RyanKung]

Re-review of 660f485 (fresh read of the new material, not just closure of the prior round).

All eight prior findings are addressed, and most fixes were verified against the implementation: the frame tuple now matches E2eStreamFrame, w is correctly receiver policy, the Δ policy's window bound / closed check / final-ordering clauses match E2eStreamDecryptor::validate_frame (the last ⇒ NoFuture clause together with the final-frame-stays-pending invariant entails the implementation's conflicting-final rejection), the Replay row again names the nonce cache, Explore_Γ and the Evidence/Obligation names are unified, and path.png plus the stale README line are gone.

The new material introduces new issues:

1. papers/rings.tex:1014 — Dup_Δ(seq) ⇔ seq ∈ seen ∪ pending accepts a sender equivocation that the implementation rejects. In E2eStreamDecryptor::validate_frame (crates/core/src/message/e2e.rs:367), a frame whose sequence is already pending is a duplicate only if it is equal to the buffered frame; a conflicting frame at the same sequence is an error (E2eFrameSequenceMismatch), i.e. detected stream poisoning. The model's Dup checks sequence membership only, so for a conflicting frame SeqOK_Δ holds and emit = ε — the model silently drops exactly the equivocation the surrounding prose declares "part of the security boundary". It should be Dup_Δ(f) ⇔ seq ∈ seen ∨ (seq ∈ dom(pending) ∧ pending(seq) = f), with a conflicting pending frame rejected rather than absorbed.

2. papers/rings.tex:907 vs papers/rings.tex:290 — two contradictory notions of collapse. The Affine replica set definition keeps collapse_{N,ρ}(k) ⇔ |O_k| < ρ, while the new Replica realization obligation defines Collapse_{ν,x} ⇔ L_{ν,x} < min(ρ,|N|). For |N| < ρ the first is always true while the second is false whenever L = |N| (which the same obligation calls FullRed). Nearly identical names with different truth values and no cross-reference; either use one notion or relate them explicitly (collapse ⇔ Collapse ∨ |N| < ρ).

3. papers/rings.tex:909 — Report_Rings ∋ |{(ν,x) : Collapse_{ν,x}}| contradicts the Benchmark report obligation. Report_Rings is later defined as a fixed tuple (N,ρ,r,transport,runtime,scheduler,T_total,timeoutMean,failrate) that contains no collapse count, and ∋ is not defined on tuples. Either add the field to the report tuple or drop the membership claim.

4. papers/rings.tex:1328 — the fresh Axis coordinates reintroduce symbol collisions. μ is the namespace index used throughout the functoriality and protocol-morphism definitions (rings.tex:551, rings.tex:628: f : X_ν → X_μ, H_μ ∘ σ_X = H_ν), and χ is the cross-domain witness-order operator (rings.tex:1115). The fix for the previous q/r collision picked two more letters already in use.

5. papers/rings.tex:908 — LiveClaim_{ν,x}(ρ) is used once and never defined. Same class as the SeqOK gap fixed in this round: the Methodology states claims are carried by definitions, and the obligation's antecedent is an undefined predicate.

6. papers/rings.tex:999 — e is free in FrameValid_Δ (pre-existing, but this definition was rewritten in this commit): Session(D(pk_s),sid,e) binds e nowhere. It should be existentially quantified with the expiry check (∃e. Session(D(pk_s),sid,e) ∧ now < e) or made a component of Δ.

Finding 1 is the one that matters most: it is the same accuracy class as the previous round's win issue, at the same security boundary.

[RyanKung]

Review of 19cb51f ("Restore formal Chord performance baseline"). Note this commit predates my previous comment, so all six findings from that round still apply to the current head — including the Dup_Δ equivocation gap, which remains the most important open item.

The direction here is right: replacing the removed borrowed tables with a formal, citable baseline object B_C and requiring Cite(B_C) alongside Rings-specific measurement is the correct resolution of the round-1 evaluation-scope issue. New issues in the new material:

1. papers/rings.tex:1295 — B_C(η) is parameterized by η in name only. The right-hand side (𝔼[h_C], timeout(Q_C), fail(Q_C,F_C)) mentions none of η's components; Q_C, F_C, and 𝔼[h_C] are free/global symbols, so the dependence on (|N|, churn, stabilize, loss) — the entire point of introducing η, mirroring Γ for model checking — is never established. They should be Q_C(η), F_C(η), 𝔼[h_C ∣ η]. While rewriting this definition, F ⊆ Q and to(q) also remain unstated/undefined.

2. papers/rings.tex:1323 vs papers/rings.tex:1279/1285 — h_R vs h is a fresh notation drift for the same quantity. The Latency decomposition defines the Rings hop count as h (T_total = T_conn + h·T_hop + …); the report vector calls it h_R. Same class as the Explore_Γ/Explore_scope drift fixed in the previous round. Relatedly, Σ components(vec{T}_R) = T_total holds only if h_R = h, and that intended identity (that vec{T}_R is the decomposition vector of T_total) is never stated; vec{T}_R is also used in the Benchmark report obligation (rings.tex:1309) before the display that defines it (rings.tex:1323).

3. papers/rings.tex:1325 — Overhead_{R/C} is defined and never used. No law, obligation, or prose references it, and the tuple is type-heterogeneous (four latency terms plus the qualitative label runtime). If the intent is "the components of Report_Rings with no counterpart in B_C", state that as the defining law; otherwise drop the orphaned definition.

4. Cross-check with the previous round: this commit rewrites the Report_Rings tuple (rings.tex:1306–1311) and it still does not contain the collapse count that rings.tex:909–910 asserts membership of (Report_Rings ∋ |{(ν,x) : Collapse_{ν,x}}|), so that contradiction now stands against the rewritten tuple.

On the positive side: no stale timeoutMean/failrate references remain, and B_C(η) ≢ Report_Rings correctly keeps the baseline and the measurement as distinct objects.

[RyanKung]

Whole-paper structural review at 19cb51f. Since this PR's mandate is restructuring the paper for accuracy, this pass scans the entire document against the implementation rather than the diff hunks. Findings from the two previous rounds remain open and are not repeated here.

1. The claim stratification is declared but never applied — the paper's central device is unused by its own body. The abstract and the Methodology introduce Claim = Spec ∪ Impl ∪ Evidence_Γ ∪ Obligation and Admit(c), yet no Definition or Invariant in "DID and Resource Algebra" or "Ordering, Ranking, and Security" carries a stratum. Checking the code, the strata are very unevenly populated: implemented — DID/session delegation (crates/core/src/session.rs, the {ts,ttl} contract matches Session(d,s,e)), affine replica keys (Did::rotate_affine, wired into chord.rs storage and chord/storage_repair.rs), subring (dht/subring.rs), storage CRDT (dht/entry.rs), E2E frames, chunk TTL/bounds (chunk.rs), extension runtime with capability interpretation (crates/node/src/extension/); not implemented — Mailbox (zero hits repo-wide), Hidden service descriptor, Sidecar witness and Witness order, Ranking event/Score aggregation (the code has only local, unsigned Measure/BehaviourJudgement counters — no signed q=(subject,rater,…,σ), no RankValid, no robust aggregation), and Shamir secret-sharing placement. Presenting all of these as uniform Definitions is precisely the accuracy failure this PR set out to fix. The restructure should tag every Definition/Invariant/Algorithm with its stratum (e.g. a marginal [Impl]/[Spec]/[Obl] marker or a per-section claims table).

2. papers/rings.tex:288 — |P_k| = ρ still needs ρ ≤ M, and the implementation already states the missing side condition. Did::rotate_affine's documented law (crates/core/src/dht/did.rs:233) reads "for i != j, place(self,n)[i] != place(self,n)[j] while n <= 2^160". The paper asserts the cardinality unconditionally for ρ ∈ ℕ_{>0}. Add the side condition (or note the implementation's u16 domain, which makes it vacuous there).

3. Abstract omits U from the namespace set. papers/rings.tex:89 has {D,V,M,H,Q,W} ⊂ Obj(Set/R) while the Namespace object definition (rings.tex:530) has ν ∈ {D,V,M,H,U,Q,W}. Ironically U (subring) is one of the namespaces that actually has an implementation.

4. Ten of the paper's fourteen floats are never referenced from the text. Only Algorithms 1–3 and the ElGamal algorithm are \ref'd; Figures layers, webrtc-standard-sdp, webrtc-rings-sdp, wasm-boundary, actor-model, lookup-figure and Tables carrier-table, security-table, verification-table, related-table float unanchored. Beyond IEEE style, the Actor Model figure (rings.tex:638) is conceptually orphaned — nothing in "Category and Effects" mentions actors, and its "Mailbox" box collides with the (unimplemented) Mailbox namespace M. Each float should be cited by the claim it witnesses, and actor-model looks like a leftover from the pre-restructure draft that should simply go.

5. papers/rings.tex:674 — E_n ⊆ E is a type error. E = ∏_{v∈VID} E_v is a product, i.e. a set of total assignments; a node's stored entries are a partial section, not a subset of the product. It should be E_n ∈ ∏_{v∈dom(E_n)} E_v (equivalently E_n : VID ⇀ ⋃_v E_v with E_n(v) ∈ E_v).

6. papers/rings.tex:772 — Stabilize tests c ∈ (n.did, s), but the identifier carrier only defines (a,b]_R. The open interval is never introduced, and the endpoint exclusion is exactly the kind of boundary the paper elsewhere treats as semantically loaded. Similarly closest_preceding_node (alg:lookup) is used but never defined — finger state F_n is defined, the selection rule over it is not.

7. papers/rings.tex:944 — the hidden-service descriptor reuses ν and ρ as record fields. In h=(ν,ρ,Intro,Relay,Cap,K,exp,rank), ν is elsewhere the namespace index and ρ the replication factor; Cap collides with cap ⊆ A_X, Relay with the relay frame, rank with the ranking section. Same collision class as the q/r and μ/χ findings in earlier rounds.

8. Pervasive metavariable overloads deserve a symbol table in the restructure. Q is simultaneously a namespace index (ν∈{…,Q,W}), the action queue in the state relation (C=(S,Q), rings.tex:1163), and the query set in fail/timeout (Q_C,Q_R); H is a namespace index, the placement-hash family H_ν, and the bare H(msg) in the sidecar witness (which hash?); r is the successor-list length and the relay frame (rings.tex:1040); e is the session expiry, the mailbox epoch (mbox(d,e)), and free in FrameValid_Δ. For a paper whose thesis is carrier separation, the metalanguage carriers collide everywhere; one symbol table and a pass over binders would fix the class rather than the instances.

One constructive note: crates/core/src/algebra.rs is a direct implementation mirror of the Carrier separation constraint — it models Did as an AbelianGroup and deliberately does not implement CommutativeRing, which is exactly Mult_R ∉ RouteOps_R (rings.tex:233), and its JoinSemilattice backs the replicated-entry algebra. The ImplMap step of the Methodology could cite this module by name; it is the strongest Spec→Impl edge the repository has.