mhpow B4 (R15-07): the composed accepted-proof energy statement, its losses and the encoded-state answer (NOT RUN)
Track B item B4, documents only. docs/analysis/mhpow/b4/README.md: the pROM model and the MTP/DRSample construction exactly as Blocki-Smearsoll TCC 2025 (eprint 2025/1456, full PDF sha256 13c3646e...) states them, its theorems and constants with numbers (Thm 4 to 7, Cor 1 to 3, Lemma 5, Fact 8), the composed three-term statement (hashing, transfers, retention) with the status of each term, what the 2024 bandwidth paper (2018/221, 2a466b97...) and Ren-Devadas (2017/225) give, what is new, the reduction-loss table (generic route at most 0.151 of honest energy at log2 N = 22; red-blue route at least 256/(1-rho) loss), R4's encoded-state question as BLOCKED row B4-B07, the quantum sentence, ten BLOCKED rows and the obligations for B2 and B1 by row. tools/mhpow/b4/params.py (closed-form arithmetic, standard library) ran on build-9; params.txt is its output; RUNS.md the runs; registry-batch-b4.json one NOT RUN cell for the steward, not recorded. Research paths added to tools/ci/export-exclude.txt. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This commit is contained in:
igneum-labs
parent
197a7fe39d
commit
d27064242f
6 changed files with 557 additions and 0 deletions
355
docs/analysis/mhpow/b4/README.md
Normal file
355
docs/analysis/mhpow/b4/README.md
Normal file
|
|
@ -0,0 +1,355 @@
|
|||
# B4 (R15-07): the energy cost of accepted proofs, as a statement first
|
||||
|
||||
Track B item B4 of the 1.5x research programme (plan: docs/plans/igneum-2.0-master/1p5x/, the research plan sha256
|
||||
269ceaa5824d0914..., sections 2, 3.5, 4.2 to 4.5, 6 B4, 8, 9, 10 R15-07). Lane: B4, the theory lane. Written 9 October 2026,
|
||||
10:1x to 12:xx UK. Documents only: no code of Igneum's is changed, nothing activates.
|
||||
|
||||
**Decision: NOT RUN.** This is a statement and an audit of what the published theorems give, not a proof and not a pass. Every
|
||||
NEW line below is a proof obligation until the independent panel reads it. The composed claim is a theorem shape with named holes;
|
||||
where a hole is decision-critical it is a BLOCKED row with its exact question.
|
||||
|
||||
**The result in four lines.**
|
||||
|
||||
1. The 2025 theorem (Blocki and Smearsoll) proves, in the parallel random oracle model, that any prover whose MTP/DRSample
|
||||
certificate is accepted had cumulative memory (bits held, summed over rounds) at least (lambda/4)(e d/2), except with an
|
||||
explicit small probability. Cumulative memory is capacity times time. It is not memory traffic and it is not joules.
|
||||
2. The 2024 bandwidth paper (Blocki, Liu, Ren and Zhou, the corrected JoC version) gives two bridges from that to energy: a
|
||||
generic one (Theorem 4.5, any trace) that loses a square root, and a pebbling one (Theorem 3.3 with Lemma 5.5) that loses a
|
||||
factor of at least 256/(1 - rho) in its published constants and says nothing once the adversary's cache holds about
|
||||
C N / log2 N labels. Neither bridge has been proved for the MTP certificate setting; that composition is the NEW part.
|
||||
3. Through the published constants, the best composed lower bound L is at most about 1/6.6 (generic route, ideal
|
||||
depth-robustness constants c1 c2 = 1, equal transfer and hash costs, log2 N = 22) and 1/341 or less (pebbling route) of an
|
||||
honest specialist's energy. A 1.5x certificate
|
||||
(G_upper / L <= 1.5, plan section 2) is therefore not reachable from the published constants; it needs new theorems with
|
||||
tight constants, and it cannot survive an adversary whose on-die SRAM holds C N / log2 N labels unless the bound prices the
|
||||
SRAM itself (section 8). This is a negative screening result for the Track B route as published, kept as a control.
|
||||
4. R4's encoded-state warning does not break the 2025 cumulative-memory theorem (its model counts the state in bits under any
|
||||
representation, and R4 says itself that its separations do not reach data-independent functions in the parallel model);
|
||||
it does bind every Igneum-specific change that makes the graph data-dependent or the label function structured (row B4-B07).
|
||||
|
||||
## 1. Sources, by sha256
|
||||
|
||||
Fetched on build-9 under the pid file /srv/queue/pids/build-9-b4.pid (mirrors build-9:/srv/builds/b4/run.pid, ended 10:12 UK;
|
||||
SHA256SUMS in build-9:/srv/builds/b4/). Never fetched on the Mac. eprint.iacr.org answers the box with a Cloudflare
|
||||
"Just a moment" page (a 5.4 KB HTML file, which is what build-9:/srv/builds/b2/2025-1456.pdf holds), and the challenge was not
|
||||
bypassed: the full PDFs came from the Internet Archive's copies of the eprint PDF URLs. Two further papers (eprint 2017/443, the
|
||||
DRSample construction, and 2016/875, the cc >= e d bound) returned archived error pages and were not retried (row B4-B01).
|
||||
|
||||
| ref | paper | full PDF | snapshot (UTC) | pages | sha256 |
|
||||
|---|---|---|---|---|---|
|
||||
| R1 | Blocki, Smearsoll, *Provably Memory-Hard Proofs of Work With Memory-Easy Verification*, TCC 2025, eprint 2025/1456 | eprint.iacr.org/2025/1456.pdf | 2025-12-31 15:20:15 | 46 | 13c3646e7d85c1aa58a92914582caab5798d90cf2a3cad33e58d81d49c1d31db |
|
||||
| R2 | Blocki, Liu, Ren, Zhou, *Bandwidth-Hard Functions: Reductions and Lower Bounds*, JoC 2024 version dated 22 January 2024, eprint 2018/221 | eprint.iacr.org/2018/221.pdf | 2026-01-06 14:44:18 | 50 | 2a466b97f536e37169b334c826a9b30caf044e8e11ed0d41252c5fcb58679568 |
|
||||
| R3 | Ren, Devadas, *Bandwidth Hard Functions for ASIC Resistance*, TCC 2017, eprint 2017/225 | eprint.iacr.org/2017/225.pdf | 2026-10-02 01:58:35 | 26 | 29c5a9c0a31044b708b25fdca07413ebff9cd65896aa10544bc4549e8c16e080 |
|
||||
| R4 | de Rezende, Engstrom, Reyzin, *Separating the Pebbling Model from the Random Oracle Model*, dated 21 May 2026, eprint 2026/1024 | eprint.iacr.org/2026/1024.pdf | 2026-05-25 20:25:56 | 26 | aa6caa39cbc70cfd83b0f9689955b4877dcfda41981bf1e52818de9168aa07c4 |
|
||||
| R16 | Bhattacharyya, Mandal, *Bandwidth-Hard Functions from Random Permutations*, arXiv 2207.11519v1 | arxiv.org/pdf/2207.11519 | live, 9 Oct 2026 | 14 | ac2733933e64a3cf27d69e5c8d9371b83bf8c71fee70f6b626988b5c140c34c3 |
|
||||
|
||||
Reading depth, stated exactly: R1 sections 1 to 7 and appendix A line by line (appendix B, the attack proofs, skimmed);
|
||||
R2 sections 1 to 4, section 5.1 and 5.4 and Theorem B.2 (section 6 on scrypt and appendix D on NP-hardness not read); R3
|
||||
abstract and sections 3 to 4 (the model, the energy limit and Table 1), its theorem list only beyond that; R4 sections 1 and 2
|
||||
(the claims, the models, what is and is not separated); R16 abstract and Theorems 1 and 3. No independent proof audit is claimed.
|
||||
|
||||
## 2. The model, exactly as R1 uses it
|
||||
|
||||
**Parallel random oracle model (pROM), R1 section 2.1.** A random oracle H : {0,1}* -> {0,1}^lambda drawn uniformly. The prover
|
||||
A runs in rounds. In round i+1 it receives its state sigma_i = (tau_i, Q_i) and the answers H(Q_i) to the batch of queries it
|
||||
issued, performs arbitrary computation (unbounded, even exponential, R1 footnote 4; only RO queries between rounds are forbidden),
|
||||
and outputs a new state and a new batch Q_{i+1} of any size. The initial state encodes the input chi. Fixing A, H, chi and the
|
||||
coins R fixes the trace sigma_0, ..., sigma_t.
|
||||
|
||||
**Cost measure.** Cumulative memory complexity cmc(trace) = sum over i of |sigma_i| in bits (R1 Definition 4). The state is a bit
|
||||
string with no assumed representation: the pebbling is never assumed of the adversary, it is extracted ex post facto from the RO
|
||||
queries and the state size is bounded by a compression argument (section 9 below).
|
||||
|
||||
**The construction (R1 section 3.2, the MTP framework).** G = G_N a DAG on [N], N = 2^n, constant in-degree delta (delta = 2
|
||||
for DRSample). Labels l_1 = H(chi, 1), l_v = H(chi, v, l_{v_1}, ..., l_{v_delta}). Merkle commitment with chi as salt:
|
||||
tau_v = H(chi, tau_{v||0}, tau_{v||1}), root tau. Challenges c_i = H(chi, i, tau) mod N for i = 1..k (Fiat-Shamir). The
|
||||
certificate opens each challenged label and its parents with their Merkle paths. The verifier recomputes the challenges, checks
|
||||
the openings and checks local consistency of each challenged node. Honest prover: O(N + k log N) sequential time, O(N lambda)
|
||||
space, proof O(k lambda log N) bits, verifier O(k log N) RO calls.
|
||||
|
||||
**The adversary's bounds.** q = total RO queries over the whole trace, t = rounds, n_in = bit length of a query input (the "n"
|
||||
of R1 Lemmas 8 to 10, not log2 N). Hypothesis of R1 Lemma 3: lambda/4 >= 2 log2 q + log2 indeg(G). No bound on time per round,
|
||||
on parallelism, or on non-RO computation. Success = the verifier accepts (R1 Definition 5 item 4 and section 3.2).
|
||||
|
||||
**The energy variant (R2 section 3.1), used for every joule line below.** The state splits into a cache sigma_i of at most m w
|
||||
bits, where RO queries are issued and answered (at most m queries per round), and a memory xi_i of any size. Memory may run
|
||||
arbitrary functions F2, F3 of its own contents and the messages it receives but may not query the RO. Cost of a trace:
|
||||
sum over i of (c_r |Q_i| + c_b NBits_i / w), with NBits_i the bits moved between cache and memory in round i, c_r the cost of
|
||||
one RO call, c_b the cost of moving w bits (R2 Definition 3.2). Every lower bound in R2 is a lower bound for this cost.
|
||||
|
||||
## 3. What R1 proves, restated with its numbers
|
||||
|
||||
Bad events (R1 section 2.1 and appendix A): Collision, Pr <= C(q,2) 2^-lambda (Lemma 7); BadOrder, Pr <= n_in q^2 2^-lambda
|
||||
(Lemma 10); MisColor, Pr <= N 2^-lambda (Lemma 2); implausible extraction IE, Pr <= t 2^(-lambda/2) (Lemma 3); LuckyQuery,
|
||||
Pr <= q (1 - beta)^k (Lemma 4).
|
||||
|
||||
* **Theorem 4.** Without Collision, BadOrder, MisColor, the ex-post-facto pebbling is a legal pebbling of the ex-post-facto graph
|
||||
G' = G - S_red (S_red = the locally inconsistent nodes of the labelling traced from the root the prover output).
|
||||
* **Theorem 5 and Lemma 3.** An extractor given sigma_i and a hint of (2 log2 q + log2 indeg)|P'_i| bits outputs |P'_i| fresh RO
|
||||
input/output pairs, hence |sigma_i| >= |P'_i| lambda/4 for every round except with probability t 2^(-lambda/2).
|
||||
* **Theorem 6.** Without the four bad events, cmc(trace) >= (lambda/4) cc(G').
|
||||
* **Theorem 7 and Corollary 1.** If A succeeds with probability at least alpha after t rounds,
|
||||
Pr_H[cmc < (lambda/4) min over |S| <= beta N of cc(G - S)] <= alpha - (C(q,2) 2^-lambda + n_in q^2 2^-lambda + N 2^-lambda
|
||||
+ t 2^(-lambda/2) + q (1 - beta)^k), read as: with probability at least alpha - eps_bad the prover succeeds AND pays the bound
|
||||
(row B4-B02 records the printed direction of the inequality).
|
||||
* **Lemma 5.** For (e, d)-depth-robust G and e' < e: min over |S| <= e' of cc(G - S) >= (e - e') d (from cc >= e d, [ABP17]).
|
||||
* **Corollary 2.** With beta = e/(2N) and k = 2 N ln2 lambda / e: cmc >= (lambda/4)(e d / 2) except with the error
|
||||
eps_bad = C(q,2) 2^-lambda + n_in q^2 2^-lambda + N 2^-lambda + t 2^(-lambda/2) + q 2^-lambda.
|
||||
* **Fact 8 and Corollary 3 (DRSample).** There exist constants c1, c2 > 0 with indeg(G_N) = 2 and G_N
|
||||
(c1 N/log N, c2 N)-depth-robust; with k = 2 lambda log N / c1: cmc >= (lambda/4)(c1 c2/2) N^2 / log N, error term q e^-lambda
|
||||
for the lucky challenges.
|
||||
* **Section 7 (Theorems 9, 10).** Attacks: for any constant in-degree DAG, k must be omega(log N / log log N); for Argon2i a set
|
||||
of N/k deletions gives cc O(N k^(12/5)). The paper's construction sets k = O(lambda log N).
|
||||
|
||||
## 4. The constants table
|
||||
|
||||
| symbol | meaning | value in the paper | source | Igneum status |
|
||||
|---|---|---|---|---|
|
||||
| lambda | RO output = label width, and the security parameter (the paper uses one symbol for both) | free | R1 sec. 2.1, 3.2 | B2 must split: label width w and soundness lambda_s (row B4-B08) |
|
||||
| delta | in-degree of G | 2 (DRSample) | R1 Fact 8 | fixed by B1 |
|
||||
| N = 2^n | nodes = labels | free | R1 sec. 3.2 | exploratory 32, 128, 512 MiB states (plan B3); params.txt sec. 6 |
|
||||
| e, d | depth-robustness of G | e = c1 N/log N, d = c2 N | R1 Fact 8 (from ABH17, ABP17) | **c1, c2 have no value in R1** (row B4-B03) |
|
||||
| beta | red fraction a lucky root may hide | e/(2N) (Cor. 2); c1/(2 log N) (sec. 6) | R1 Cor. 2, sec. 6 | follows c1 |
|
||||
| 1 - beta | soundness error per challenge | 1 - c1/(2 log N) | R1 Lemma 4 | follows c1 |
|
||||
| k | number of challenges | 2 N ln2 lambda / e (Cor. 2); 2 lambda log N / c1 (Cor. 3) | R1 Cor. 2, 3 | with lambda_s = 128, log2 N = 22, c1 = 0.25: k = 22,528 (params.txt sec. 3) |
|
||||
| cmc bound | cumulative memory of any accepted prover | (lambda/4)(e d/2) = (lambda/4)(c1 c2/2) N^2/log N bit-rounds | R1 Cor. 2, 3 | constant open with c1 c2 |
|
||||
| 1/4 | bits per pebble kept after the hint | lambda/4 | R1 Lemma 3, Thm 6 | general form theta = lambda - 2 log2 q - log2 delta - s (B4 restatement, NOT RUN; params.txt sec. 2) |
|
||||
| q ceiling | queries the cmc theorem covers | lambda/4 >= 2 log2 q + 1, so q <= 2^31.5 at lambda = 256 | R1 Lemma 3 | a network lifetime exceeds 2^31.5 RO calls: 256-bit labels are outside the theorem; >= 520-bit labels cover q = 2^64 (params.txt sec. 1) |
|
||||
| eps_bad | failure probability | C(q,2) 2^-lambda + n_in q^2 2^-lambda + N 2^-lambda + t 2^(-lambda/2) + q 2^-lambda | R1 Cor. 1, 2 | computable once w, lambda_s, q are fixed |
|
||||
| Merkle | binary, salt chi, node = H(chi, left, right), lambda-bit nodes | as stated | R1 sec. 3.2, Def. 15 | B1: explicit domain tags (row B4-B09) |
|
||||
| proof size | k (delta+1) openings, each a label and log N siblings | O(lambda^2 log^2 N) | R1 sec. 6.1 | 11.9 to 278 MiB uncompressed at log2 N = 22 for c1 from 1 to 0.1 (params.txt sec. 3); a B6 cost |
|
||||
| c_b, c_r | energy of moving w bits across the cache boundary; of one RO call | free parameters | R2 Def. 3.2 | technology inputs, BOUND (L) only if each is itself a justified lower bound |
|
||||
| 9m | red pebbles the extracted pebbling may use for a cache of m words | 9 | R2 Thm 3.3 | cache inflation loss |
|
||||
| eps/16 | probability-to-cost factor of the red-blue reduction | 1/16 | R2 Thm 3.3 | loss |
|
||||
| q, w ceiling (R2) | q < 2^(w/20) and 20 log2 n < w | q < 2^12.8 at w = 256 | R2 Thm 3.3, Lemma 3.9 | labels of 1,280 bits or more for q = 2^64 |
|
||||
| DRSample red-blue | per interval of length l >= 16m/(1-rho): min((1-rho) l c_b / 8, ((1-rho) l/16) sqrt(N/(64 l)) c_r) | as stated | R2 Lemma 5.5, Thm 5.2, Thm 1.3 | summed: min((1-rho) N c_b/16, ...) for m = O(N^rho) |
|
||||
| DRSample cache cut-off | above m = C N / log N there is no blue-move bound (a sequential pebbling in space C N/log N, time N) | C not given | R2 sec. 5.4, citing Blocki et al. CRYPTO 2019 | 186 MiB of cache for a 4 GiB, 1 KiB-label state, times C (params.txt sec. 6) |
|
||||
|
||||
## 5. THE COMPOSED THEOREM STATEMENT (draft, NOT RUN)
|
||||
|
||||
**Setting.** The R2 energy variant of the pROM (section 2), with: G = DRSample on N = 2^n nodes, delta = 2; label width w bits,
|
||||
the RO H : {0,1}* -> {0,1}^w; k challenges per certificate; a prover A with cache m w bits, total queries q, rounds t, success
|
||||
probability alpha over H, on an input chi that B2 binds to one lottery trial (network, version, epoch, template, trial id).
|
||||
Physical coefficients, each a LOWER bound over the permitted technology set of plan section 8: c_H = joules per RO evaluation
|
||||
(the hash circuit, excluding operand delivery); e_x = joules per bit moved across the boundary of the hashing cache; p_ret =
|
||||
watts per bit to retain state; tau_H = the minimum wall time of one dependent RO round.
|
||||
|
||||
**Claim (shape).** There is an explicit eps_total such that, with probability at least alpha - eps_total over H, A outputs an
|
||||
accepted certificate and its energy E(A) satisfies
|
||||
|
||||
E(A) >= c_H * (2 (1 - beta) N - 1) [term 1: hashing]
|
||||
+ e_x * L_x(m) [term 2: transfers across the cache boundary]
|
||||
+ p_ret * tau_H * theta * (e/2) * d [term 3: retention over the forced rounds]
|
||||
|
||||
with theta = w - 2 log2 q - log2 delta - s, e = c1 N/log N, d = c2 N, beta = e/(2N), k = 2 N ln2 lambda_s / e, and
|
||||
eps_total = eps_bad (R1 Cor. 2, with w for lambda in the label terms and lambda_s in the challenge term) + t 2^-s + eps_x
|
||||
(the transfer term's own error, open). The three terms count disjoint physical activity (RO evaluation, boundary crossings,
|
||||
holding bits over time), so they add in the additive energy model; no term double-counts another (plan B4: "do not add unrelated
|
||||
lower bounds when they double-count the same work"). Under R2's convention, where c_r already charges an RO call, term 1 IS the
|
||||
c_r q part of R2's ecost and must not be added to it a second time.
|
||||
|
||||
**The status of each term.**
|
||||
|
||||
* **Term 1 is the strongest and is new but short (B4 Lemma A, NOT RUN).** With no Collision and no MisColor, every green node's
|
||||
prelabel (chi, v, parents) was queried (R1 Lemma 2 and the proof of Theorem 5), and every green leaf was traced through the
|
||||
Merkle tree, which needs one distinct query per traced internal node (R1 proof of Theorem 4, the MT procedure). Without
|
||||
LuckyQuery there are more than (1 - beta) N green nodes (R1 Theorem 7 proof). Hence q >= (1 - beta) N + ((1 - beta) N - 1).
|
||||
Because every prelabel and every Merkle node carries chi, queries for distinct trials are distinct: across J accepted
|
||||
certificates with distinct chi the bound is additive, q >= J (2 (1 - beta) N - 1). This term holds at ANY cache size, including
|
||||
the full-SRAM adversary of plan B5, and it is immune to multi-instance amortisation. It prices hashing only: it says nothing
|
||||
about memory, and on its own it is exactly the hashing floor that an ASIC wins on (R3 section 4: the ASIC SHA-256 cost was
|
||||
0.0012 nJ per byte against 30 nJ per byte on a 2016 CPU).
|
||||
* **Term 2 is the memory-energy bridge and is OPEN.** R2 proves a transfer lower bound only for a full evaluation of an iMHF
|
||||
(Theorem 3.3: ecost >= (eps/16 - 2^(-2mw/5) - (q+1)/2^w) rbpeb(G, 9m)) and only for DRSample's complete graph (Lemma 5.5,
|
||||
Theorem 1.3, Theorem B.2). The accepted-certificate version needs (i) the red-blue extension pebbling of R2 section 3.2 built
|
||||
from R1's ex-post-facto pebbling of G' (the ex-post-facto labelling replaces the honest one, as R1 did for the black pebbling),
|
||||
and (ii) a red-blue lower bound for G - S, |S| <= beta N, in place of G: R2's dispersion argument (Lemma 5.5) must survive the
|
||||
deletion of beta N nodes chosen by the adversary after seeing G. Until both are proved, L_x(m) = 0 in any certified number.
|
||||
Even when proved with R2's constants it gives L_x(m) >= (1 - rho) N w / 256 bits for m <= C' N^rho (a loss of 256/(1 - rho)
|
||||
against an honest prover's N w), and nothing for m >= C N / log N.
|
||||
* **Term 3 follows from R1 plus two short steps (B4 Lemma B, NOT RUN).** (a) G - S is (e/2, d)-depth-robust for |S| <= e/2, so G'
|
||||
contains a path of d nodes and the legal ex-post-facto pebbling of G' (R1 Theorem 4) needs t >= d rounds: an accepted prover
|
||||
performed at least d = c2 N dependent RO rounds (this is the "sequential work" of the claim; R1 states no time bound itself).
|
||||
(b) The general extraction count gives cmc >= theta (e/2) d bit-rounds except with probability t 2^-s. Holding sum |sigma_i|
|
||||
bit-rounds for rounds of at least tau_H costs at least p_ret tau_H cmc joules. (c) The memory held: the peak state is at least
|
||||
cmc / t, i.e. at least theta c1 N / (2 log N) bits for a prover finishing in d rounds; R1 gives no sustained-space bound (that is
|
||||
R8's territory and is not used here).
|
||||
Consequence: term 3 is the only joule line that cumulative memory buys by itself, and it prices holding bits, not moving them.
|
||||
Retention power per bit (DRAM refresh, SRAM retention leakage) is small, so term 3 is expected to be small against term 1; its
|
||||
size is a calibration question for the WITNESS rows, not something this lane asserts.
|
||||
|
||||
**What the claim does NOT say.** It is not a bound on the specialist's energy per hash of Igneum's current work; it is per accepted
|
||||
certificate of the published construction under the pROM. It gives no G_upper. It certifies nothing about the GPU side.
|
||||
|
||||
## 6. What each source gives, and what is new
|
||||
|
||||
**R1 (2025) gives:** soundness of the MTP framework for data-independent depth-robust graphs in the pROM; cmc of any accepted prover
|
||||
>= (lambda/4)(e d/2) with an explicit additive error; the DRSample instance with k = O(lambda log N) and polylog proofs; matching
|
||||
attacks showing k = omega(log N / log log N) is necessary. It gives capacity-time, not energy, and no numeric constants for c1, c2.
|
||||
|
||||
**R2 (2024 corrected) gives:** (i) Theorem 3.3, the first pROM reduction from energy to red-blue pebbling for iMHFs, robust to
|
||||
arbitrary encodings of the bits moved between cache and memory; (ii) Theorem 4.5, cost(trace) >= (cmc/(t w) - m) c_b + t c_r for
|
||||
ANY pROM trace, hence cost >= 2 sqrt(cmc c_b c_r / w) - m c_b; (iii) Lemma 5.5 and Theorems 1.3 and B.2, DRSample's red-blue cost
|
||||
min(Omega(N) c_b, Omega(N^(3/2 - rho/2)) c_r) for m = O(N^rho), with the stated constants; (iv) the cut-off: no meaningful bound for
|
||||
m = omega(N / log N). Note: the intro's Theorem 1.3 and the appendix's Theorem B.2 give different DRSample forms for different cache
|
||||
ranges; the composed statement uses the weaker one in each range.
|
||||
|
||||
**R3 (2017) gives:** the red-blue energy model and section 4's limit: whatever the function, an adversary running the honest
|
||||
algorithm on better hardware has advantage at least (c_b,GPU + c_r,GPU R0/B0) / (c_b,ASIC + c_r,ASIC R0/B0); with equal memory
|
||||
energy, the floor is about 1 + c_r,GPU / c_b,GPU. This is the theorem form of the plan's section 3.5 bridge and it binds Track B:
|
||||
a 1.5x certificate needs the GPU's per-label hashing energy at most half its per-label memory-transfer energy AND the specialist's
|
||||
memory energy per bit no lower than the GPU's, before any reduction loss. R3 also flags that a Merkle-Damgard or chunk-absorbing
|
||||
hash breaks the pebbling analogy (section 4.2), an obligation on B1.
|
||||
|
||||
**R16 gives:** a permutation-based instantiation of the RO for bandwidth-hard graph functions, with ecost >= (eps/(40 delta))
|
||||
rbcost(G, 20 delta m) - eps m c_b/2, for q <= 2^(n/(10 delta)) and |V| <= 2^(n/(4 delta)) (Theorem 1), and the wide-label form
|
||||
(Theorem 3). It applies only if B1 builds wide labels from a permutation; its losses then multiply into section 7.
|
||||
|
||||
**NEW in composing them for Igneum (each a proof obligation, none claimed):**
|
||||
|
||||
1. The red-blue reduction for MTP certificates (term 2 (i)).
|
||||
2. Red-blue lower bounds for DRSample minus an adversarial beta N set (term 2 (ii)).
|
||||
3. B4 Lemma A (hash-call floor, additive across trials) and B4 Lemma B (rounds >= d, retention joules), both short, both unreviewed.
|
||||
4. The general-theta restatement of R1 Lemma 3 (q above 2^31.5).
|
||||
5. The physical translation: a lower bound on joules from the three terms with technology coefficients that are themselves lower
|
||||
bounds over the permitted technology set (plan section 8), i.e. BOUND (L), kept apart from X5's chip rows, which are WITNESS (E_D)
|
||||
(section 8 below).
|
||||
6. Multi-instance amortisation for terms 2 and 3 (R1's theorem is per input chi and per trace; only term 1 is additive for free).
|
||||
7. The binding of chi to a lottery trial, the outer target check, grinding of roots against the target, and rejected trials: all B2.
|
||||
|
||||
## 7. Reduction losses, from the paper's theorem to the composed claim
|
||||
|
||||
| # | step | factor lost (published constants) | source | removable? |
|
||||
|---|---|---|---|---|
|
||||
| L1 | state bits per pebble after the extraction hint | lambda -> lambda/4 (4x); general theta = w - 2 log2 q - 1 - s (0.976 of w at w = 8192, q = 2^64, s = 64) | R1 Lemma 3, Thm 6; params.txt sec. 2 | mostly, with wide labels (B4 restatement, NOT RUN) |
|
||||
| L2 | red nodes the prover may hide behind lucky challenges | cc(G) -> min over |S| <= beta N of cc(G - S) >= (e - beta N) d = e d/2 (2x) | R1 Lemma 5, Cor. 2 | trade against k (smaller beta, more challenges) |
|
||||
| L3 | depth-robustness to cumulative pebbling | cc >= e d = c1 c2 N^2 / log N against the N^2 an honest prover holds: c1 c2 / log N | R1 Fact 8, [ABP17] | log N is inherent to DRSample (R2 sec. 5.4); c1 c2 unknown (B4-B03) |
|
||||
| L4 | success probability | alpha -> alpha - eps_bad (additive) | R1 Cor. 1 | negligible at wide labels |
|
||||
| L5 | generic cmc-to-energy | E >= 2 sqrt(cmc c_b c_r / w) - m c_b: share of an honest N (c_b + c_r) <= sqrt(2 c1 c2 / log2 N) x sqrt(c_b c_r)/(c_b + c_r): 0.151 at log2 N = 22 with c1 c2 = 1 and c_b = c_r; 0.030 at c_b/c_r = 100 | R2 Thm 4.5; params.txt sec. 4 | no: the square root is inherent to the route |
|
||||
| L6 | energy-to-red-blue reduction | eps/16, cache m -> 9m, minus 2^(-2mw/5) + (q+1)/2^w; needs q < 2^(w/20), 20 log2 N < w | R2 Thm 3.3, Lemma 3.9 | constants not shown tight |
|
||||
| L7 | DRSample red-blue bound | (1 - rho)/16 of N c_b for m <= C' N^rho; nothing for m >= C N / log N | R2 Lemma 5.5, Thm 5.2, sec. 5.4 | constants not shown tight; the cut-off is a real pebbling |
|
||||
| L8 | combined L6 x L7 | >= 256/(1 - rho): 341x at rho = 0.25, 512x at 0.5 | params.txt sec. 5 | needs new theorems |
|
||||
| L9 | RO instantiated by a permutation (only if used) | eps/(40 delta), cache 20 delta m | R16 Thm 1 | B1's choice |
|
||||
| L10 | MTP certificate instead of full evaluation | unknown | none (open) | B4 obligation O1, O2 |
|
||||
| L11 | amortisation across instances | unknown for terms 2 and 3; none for term 1 | none (open) | B4 obligation O6 |
|
||||
| L12 | technology coefficients | each must be a lower bound over the permitted set; an estimate is not a bound | plan sec. 8 | evidence work, not proof |
|
||||
|
||||
The arithmetic consequence (params.txt sec. 7): if the composed theorem proves only L = E_honest / loss, a 1.5x certificate needs
|
||||
G_upper <= (1.5 / loss) E_honest. At loss 6.6 that is a GPU at 0.23 of the honest specialist's energy; at loss 341, at 0.0044.
|
||||
Neither is credible, so the published constants cannot carry P04 (plan section 11 rule 2: an unknown decision-critical assumption
|
||||
is BLOCKED, not PASS).
|
||||
|
||||
## 8. The memory-energy bridge and the two labels
|
||||
|
||||
Plan section 3.5: r = 1 / (f/s + (1 - f)/c), and the certificate of section 2 needs L <= E*. In this lane's terms:
|
||||
|
||||
* **BOUND (L).** L = c_H q_min + e_x L_x(m) + p_ret tau_H cmc_min, with q_min, L_x(m), cmc_min from section 5 and each coefficient
|
||||
the minimum over the permitted technology set at the node (the cheapest credible hash circuit, the cheapest credible memory per
|
||||
bit moved, the lowest retention power), never a central estimate. Today only the first and third terms have a proof route, the
|
||||
second is 0 in any certified number, and no coefficient has a lower-bound certificate; so L is BLOCKED (row B4-B05), not a number.
|
||||
* **WITNESS (E_D).** X5's opponent-sweep rows (the six designs on build-2, 3, 5, 6, 7, 8) are witnesses: a design D gives E_D >= E*,
|
||||
so G / E_D is a lower bound on the advantage and never a ceiling. They calibrate the coefficients (which term dominates, the real
|
||||
c_b/c_r, the SRAM size where transfers vanish) and they falsify a proposed L if any witness falls below it. A witness row never
|
||||
enters L.
|
||||
* **The full-SRAM confrontation (plan B5) in this language.** "Cheapest credible memory" decides the bridge. If the adversary's
|
||||
hashing cache holds C N / log2 N labels (params.txt sec. 6: 7.5 MiB for a 128 MiB state of 1 KiB labels, 186 MiB for a 4 GiB
|
||||
state, each times the unknown C), then L_x = 0 by a legal pebbling (R2 sec. 5.4), and the bound reduces to hashing plus retention
|
||||
plus the in-cache operand reads, which the pROM prices at zero. A Track B certificate must then price on-die SRAM reads and
|
||||
leakage as part of c_H (a physical lemma outside the pROM), or restrict m by an argument that belongs to P12, not P04. The plan's
|
||||
rule holds: if the energy test fails against the full-SRAM design, P04 stays failed.
|
||||
|
||||
## 9. R4's encoded-state warning
|
||||
|
||||
**What R1's model assumes about the state's representation: nothing.** cmc counts |sigma_i| in bits of an arbitrary string (R1
|
||||
Definition 4), the in-round computation is unrestricted (footnote 4), and the pebbles are extracted from the RO query transcript,
|
||||
not assumed of the adversary. The bound |sigma_i| >= |P'_i| lambda/4 is an incompressibility argument (R1 Lemma 1, Theorem 5,
|
||||
Lemma 3): any encoding, compression or XOR combination of labels that lets A later issue the prelabel queries is itself a hint from
|
||||
which the extractor recovers the labels, so it cannot be shorter than the bound. A prover that stores an encoded state and decodes
|
||||
on demand is inside the model; decoding is free in the model, which only makes the lower bound conservative.
|
||||
|
||||
**What R4 says itself.** Its separations are for sequential-time proofs of space and for DAG-based data-dependent MHFs (R4
|
||||
sections 1.3 and 2.2, Theorems 1.1, 1.2); it states that its results cannot hold in the parallel model, where pebbling and RO models
|
||||
are equivalent for proofs of space [Pie19], and that for data-independent MHFs storing labels in another form does not improve CMC
|
||||
[AS15] (R4 section 2.2). R1's MHPoW is data-independent and analysed in the parallel model; its extraction is the AS15 method.
|
||||
|
||||
**Verdict on survival.** The R1 cumulative-memory theorem survives an encoded state. R2's Theorem 3.3 also handles arbitrary
|
||||
encodings of the bits moved (R2 section 1.2, the encryption remark), and Theorem 4.5 is a pure bit count. What does NOT survive
|
||||
automatically, and so remains as obligations:
|
||||
|
||||
1. any data dependence Igneum adds (addresses or parents chosen from label values, window-dependent reads, challenge-dependent
|
||||
recomputation inside the state construction): R4's dMHF separation then applies and every pebbling bound must be re-proved in
|
||||
the entangled model or directly in the pROM;
|
||||
2. any label function that is not a random oracle on the whole prelabel with w-bit output: a chunk-absorbing (Merkle-Damgard or
|
||||
sponge-streamed) hash (R3 section 4.2), or a function with linear structure, such as the exact reg64 prefix-XOR alternative in the
|
||||
Igneum reviews, can make XOR-combined or partial labels genuinely useful, which is precisely R4's mechanism;
|
||||
3. memory that can compute the RO (processing in memory with hash units, plan section 9): R2's model forbids memory from querying
|
||||
the RO; with hashing in memory the cache/memory split, and term 2, are void (terms 1 and 3 stand).
|
||||
|
||||
**Row B4-B07 (BLOCKED), the exact question:** "For the binding B2 lands and the reference B1 builds, (a) is every label the output of
|
||||
one RO call, modelled as a random oracle with w-bit output, over the complete prelabel (chi, v, all parent labels) with unambiguous
|
||||
encoding, and (b) is the parent set of every node fixed before chi is known (no edge, address or window depending on any label or
|
||||
on chi)? If (a) and (b) hold, R1's cmc bound and R2's transfer reduction apply to an encoded state unchanged. If either fails, which
|
||||
node or step breaks it, and is there a pROM proof (not a pebbling proof) of the cost for that step?"
|
||||
|
||||
## 10. Quantum
|
||||
|
||||
The statement is classical: every bound here is proved in the classical parallel random oracle model, and no quantum random-oracle
|
||||
analysis of this MHPoW exists in the sources (R1 cites quantum results only for proofs of sequential work), so no quantum speedup
|
||||
or quantum resistance is claimed or estimated.
|
||||
|
||||
## 11. Text issues in R1 for the reference lane
|
||||
|
||||
Found while reading; each is a question for B1 to settle against the authors' latest revision, not a claimed error.
|
||||
|
||||
1. Corollaries 2 to 4 print Pr_H[cmc < bound] <= alpha_N - f(...); the informal Theorem 3 and Corollary 1's proof read
|
||||
Pr[Success and cmc < bound] <= f. Section 5 uses the latter.
|
||||
2. Lemma 1 prints the prediction bound as |h| 2^(-lambda |S|); Lemma 3's proof uses 2^|h| 2^(-lambda |S|).
|
||||
3. The n in the BadOrder bound n q^2 2^-lambda is the query bit length (Lemma 8), while n = log2 N elsewhere.
|
||||
4. Fact 8 and Corollary 3 name the depth-robustness constants c1, c2 and c3, c4 interchangeably; Corollary 3 sets k with c1 and
|
||||
then with c3.
|
||||
5. Corollary 2's k = 2 N ln2 lambda / e gives a q 2^-lambda term; Corollary 3's k = 2 lambda log N / c1 gives q e^-lambda.
|
||||
6. Section 3.2 indexes the challenged label as l_{c_i + 1} in the reveal but checks node c_i in the verifier.
|
||||
7. Label queries H(chi, v, ...), Merkle queries H(chi, left, right) and challenge queries H(chi, i, tau) are separated only by
|
||||
their lengths and positions; for a node with one parent the label query and a challenge query have the same shape. B1 adds
|
||||
explicit domain tags and checks the proof's bad-event counts still hold.
|
||||
|
||||
## 12. BLOCKED rows
|
||||
|
||||
| row | question | owner |
|
||||
|---|---|---|
|
||||
| B4-B01 | eprint.iacr.org serves build-9 a Cloudflare challenge; the PDFs are Internet Archive copies. Is each the authors' latest revision (R1 especially: the TCC version vs the eprint)? ABH17 (2017/443) and ABP17 (2016/875) are not fetched (archived error pages). | coordinator: a fetch route the founder approves (not a bypass) |
|
||||
| B4-B02 | The direction of R1 Corollaries 2 to 4 (section 11 item 1). | B1 against the authors' revision |
|
||||
| B4-B03 | The numeric constants c1, c2 of DRSample's depth-robustness (R1 Fact 8 gives none; ABH17 not fetched), and the C, C' of R2's cache cut-off and Lemma 5.5. Without them k, beta and every bound are symbolic. | B4 with B1, from ABH17 and Blocki et al. CRYPTO 2019 |
|
||||
| B4-B04 | Term 2: the red-blue reduction for MTP certificates and the red-blue bound for DRSample minus beta N adversarial nodes (section 5). | B4 (new theorem work; NOT RUN) |
|
||||
| B4-B05 | L as a number: lower-bound certificates for c_H, e_x, p_ret, tau_H over the permitted technology set; until then L is BLOCKED and X5's rows stay WITNESS (E_D). | B4 with the adversary lane's chip model |
|
||||
| B4-B06 | The full-SRAM case: with m >= C N / log N there is no transfer term. Does the programme accept a physical lemma pricing in-cache operand reads and leakage, and on what evidence? | the panel |
|
||||
| B4-B07 | The encoded-state question of section 9. | B2 and B1 |
|
||||
| B4-B08 | Split lambda: label width w (must exceed about 520 bits for the cmc theorem and 1,280 bits for R2's reduction at q = 2^64) and soundness lambda_s for k. | B2 |
|
||||
| B4-B09 | Domain separation of the three query kinds (section 11 item 7). | B1 |
|
||||
| B4-B10 | Proof size: k (delta+1) openings at 128-bit soundness is 11.9 MiB at best (c1 = 1, log2 N = 22, 256-bit labels) and grows as 1/c1. Pool shares carry proofs too. | B6 (plan), via the coordinator |
|
||||
|
||||
## 13. Obligations for the B2 binding lane (a717f5c9730229ea6) and the B1 reference lane (a4490b2dfe9114a55)
|
||||
|
||||
| row | owner | obligation | why it matters to the composed claim |
|
||||
|---|---|---|---|
|
||||
| O-B2-1 | B2 | chi commits to network, version, epoch, template and trial id, and EVERY lottery trial needs a fresh certificate on its own chi (no cheap outer nonce after one expensive commitment) | term 1 is additive across trials only through distinct chi; R1 is per chi |
|
||||
| O-B2-2 | B2 | the parent set of every node is fixed before chi (no data or chi dependence in edges, addresses or windows) | B4-B07 (b); R4's dMHF separation |
|
||||
| O-B2-3 | B2 | label width w >= 520 bits for q up to 2^64 under R1 Lemma 3 (or the general theta), and >= 1,280 bits if term 2 is to use R2 Theorem 3.3; soundness lambda_s separate | B4-B08; the theorems' hypotheses |
|
||||
| O-B2-4 | B2 | grinding: the number of roots a miner can try against the outer target enters q in the LuckyQuery term q (1 - beta)^k; size k for the network's lifetime q, not one proof's | R1 Lemma 4 union bound |
|
||||
| O-B2-5 | B2 | rejected trials and cancellation: the cost per accepted block is the cost per certificate times trials; a certificate that can be reused across trials breaks O-B2-1 | plan B2 |
|
||||
| O-B1-1 | B1 | the exact R1 section 3.2 prover and verifier with explicit domain tags for label, Merkle and challenge queries | B4-B09 |
|
||||
| O-B1-2 | B1 | the label function is one RO call over the complete prelabel (no chunk-absorbing hash, no linear structure); if a wide label is built from a permutation, follow R16 and record its losses | B4-B07 (a); R3 sec. 4.2; L9 |
|
||||
| O-B1-3 | B1 | malicious fixtures for the section 7 attacks: delete an (e, d)-reducing set and pass with probability (1 - e/N)^k; record the cmc of the attack against the R1 bound at the fixture's N | the attack side of the frontier |
|
||||
| O-B1-4 | B1 | settle the text issues of section 11 against the authors' latest revision | B4-B02 |
|
||||
| O-B1-5 | B1 | measure, on a box, q, t and the peak state of the honest prover at small N, and of the streaming prover that keeps C N / log N labels (the R2 sec. 5.4 pebbling), as the first witness of the cache cut-off | B4-B06; the SRAM case |
|
||||
|
||||
## 14. Figures and how they were made
|
||||
|
||||
Every number above that is not quoted from a paper comes from tools/mhpow/b4/params.py (standard library, closed forms only, no
|
||||
measurement), run on build-9: `python3 tools/mhpow/b4/params.py > docs/analysis/mhpow/b4/params.txt`. The script and its output
|
||||
are committed beside this README; their sha256 at the run are recorded in RUNS.md.
|
||||
|
||||
## 15. Registry
|
||||
|
||||
The registry batch is not recorded by this lane: registry-batch-b4.json beside this README holds one cell, status NOT RUN, with the
|
||||
evidence paths, for the steward to record if the coordinator asks. The composed claim stays NOT RUN until the panel reads it.
|
||||
13
docs/analysis/mhpow/b4/RUNS.md
Normal file
13
docs/analysis/mhpow/b4/RUNS.md
Normal file
|
|
@ -0,0 +1,13 @@
|
|||
# B4 runs
|
||||
|
||||
Every run on build-9 (188.40.146.46) under a pid file at build-9:/srv/builds/b4/run.pid, mirrored for the fetch as
|
||||
build-1:/srv/queue/pids/build-9-b4.pid (queue entry B4, ended 10:12 UK). Clocks UTC.
|
||||
|
||||
| when (UTC) | what | command | output | sha256 |
|
||||
|---|---|---|---|---|
|
||||
| 2026-10-09T09:04:54Z | eprint fetch (refused: Cloudflare challenge page, 5.4 KB HTML, not bypassed) | curl -sSL https://eprint.iacr.org/<id>.pdf | 2025-1456.pdf etc. (HTML) | not papers |
|
||||
| 2026-10-09T09:05Z | Internet Archive copies of the eprint PDF URLs, arXiv 2207.11519 | curl -sSL https://web.archive.org/web/2026id_/https://eprint.iacr.org/<id>.pdf | wb-2025-1456.pdf, wb-2018-221.pdf, wb-2017-225.pdf, wb-2026-1024.pdf, arxiv-2207.11519.pdf | SHA256SUMS in build-9:/srv/builds/b4 and README section 1 |
|
||||
| 2026-10-09T09:09Z | 2017/443 and 2016/875 (archived 429 and robots pages; not retried) | as above | removed | none |
|
||||
| 2026-10-09T09:17:30Z | parameter arithmetic | python3 tools/mhpow/b4/params.py > docs/analysis/mhpow/b4/params.txt | params.txt | params.py 7ac7fd48bde3e7962fe01045fa12a2ab1c204d9e34265a78ef9240f4f8433af1, params.txt a98ac460a5f6a16c000d5eda6311444044928f5f899931e0d3afa667d1529eba |
|
||||
|
||||
Text extraction of the five PDFs for reading: pdftotext -layout (poppler), a document conversion, no build, test or benchmark.
|
||||
77
docs/analysis/mhpow/b4/params.txt
Normal file
77
docs/analysis/mhpow/b4/params.txt
Normal file
|
|
@ -0,0 +1,77 @@
|
|||
== 1. query ceilings: the theorems' hypotheses on q (total random-oracle queries of the prover) ==
|
||||
label bits 2025 L3 log2 q max BLRZ T3.3 log2 q max BLRZ max log2 N (20 log2 N < w)
|
||||
256 31.5 12.8 12.8
|
||||
512 63.5 25.6 25.6
|
||||
1024 127.5 51.2 51.2
|
||||
2048 255.5 102.4 102.4
|
||||
8192 1023.5 409.6 409.6
|
||||
|
||||
== 2. bits per pebble theta at q = 2^64 queries, per-round failure 2^-64 (B4 restatement, NOT RUN) ==
|
||||
label 256 bits: theta = 63 bits per pebble (0.246 of the label; the paper's fixed choice is 0.250)
|
||||
label 512 bits: theta = 319 bits per pebble (0.623 of the label; the paper's fixed choice is 0.250)
|
||||
label 1024 bits: theta = 831 bits per pebble (0.812 of the label; the paper's fixed choice is 0.250)
|
||||
label 8192 bits: theta = 7999 bits per pebble (0.976 of the label; the paper's fixed choice is 0.250)
|
||||
|
||||
== 3. challenges k and proof bytes (2025/1456 Corollary 3: k = 2 lambda_s log2 N / c1, error q e^-lambda_s) ==
|
||||
c1 is the DRSample depth-robustness constant of Fact 8; the paper gives no value (BLOCKED row B4-03)
|
||||
log2 N=17 c1=1.0 k= 4352 label 256 bits: proof <= 7.17 MiB (no path sharing)
|
||||
log2 N=17 c1=1.0 k= 4352 label 8192 bits: proof <= 19.52 MiB (no path sharing)
|
||||
log2 N=17 c1=0.25 k= 17408 label 256 bits: proof <= 28.69 MiB (no path sharing)
|
||||
log2 N=17 c1=0.25 k= 17408 label 8192 bits: proof <= 78.09 MiB (no path sharing)
|
||||
log2 N=17 c1=0.1 k= 43520 label 256 bits: proof <= 71.72 MiB (no path sharing)
|
||||
log2 N=17 c1=0.1 k= 43520 label 8192 bits: proof <= 195.23 MiB (no path sharing)
|
||||
log2 N=20 c1=1.0 k= 5120 label 256 bits: proof <= 9.84 MiB (no path sharing)
|
||||
log2 N=20 c1=1.0 k= 5120 label 8192 bits: proof <= 24.38 MiB (no path sharing)
|
||||
log2 N=20 c1=0.25 k= 20480 label 256 bits: proof <= 39.38 MiB (no path sharing)
|
||||
log2 N=20 c1=0.25 k= 20480 label 8192 bits: proof <= 97.50 MiB (no path sharing)
|
||||
log2 N=20 c1=0.1 k= 51200 label 256 bits: proof <= 98.44 MiB (no path sharing)
|
||||
log2 N=20 c1=0.1 k= 51200 label 8192 bits: proof <= 243.75 MiB (no path sharing)
|
||||
log2 N=22 c1=1.0 k= 5632 label 256 bits: proof <= 11.86 MiB (no path sharing)
|
||||
log2 N=22 c1=1.0 k= 5632 label 8192 bits: proof <= 27.84 MiB (no path sharing)
|
||||
log2 N=22 c1=0.25 k= 22528 label 256 bits: proof <= 47.44 MiB (no path sharing)
|
||||
log2 N=22 c1=0.25 k= 22528 label 8192 bits: proof <= 111.38 MiB (no path sharing)
|
||||
log2 N=22 c1=0.1 k= 56320 label 256 bits: proof <= 118.59 MiB (no path sharing)
|
||||
log2 N=22 c1=0.1 k= 56320 label 8192 bits: proof <= 278.44 MiB (no path sharing)
|
||||
log2 N=24 c1=1.0 k= 6144 label 256 bits: proof <= 14.06 MiB (no path sharing)
|
||||
log2 N=24 c1=1.0 k= 6144 label 8192 bits: proof <= 31.50 MiB (no path sharing)
|
||||
log2 N=24 c1=0.25 k= 24576 label 256 bits: proof <= 56.25 MiB (no path sharing)
|
||||
log2 N=24 c1=0.25 k= 24576 label 8192 bits: proof <= 126.00 MiB (no path sharing)
|
||||
log2 N=24 c1=0.1 k= 61440 label 256 bits: proof <= 140.62 MiB (no path sharing)
|
||||
log2 N=24 c1=0.1 k= 61440 label 8192 bits: proof <= 315.00 MiB (no path sharing)
|
||||
|
||||
== 4. the generic CMC-to-energy route (2018/221 Theorem 4.5): ceiling on what it can certify ==
|
||||
E_lb = 2 sqrt(cmc cb cr / w) - m cb with cmc <= w (c1 N/log2 N)(c2 N)/2 gives E_lb <= N sqrt(cb cr) sqrt(2 c1 c2 / log2 N);
|
||||
against an honest prover's energy >= N (cb + cr): share <= sqrt(2 c1 c2 / log2 N) * sqrt(cb cr)/(cb + cr), and sqrt(cb cr)/(cb + cr) <= 1/2
|
||||
log2 N=17 c1*c2=1.0 : certified share of honest energy <= 0.1715 at cb = cr (ratio floor 5.83x)
|
||||
log2 N=17 c1*c2=0.1 : certified share of honest energy <= 0.0542 at cb = cr (ratio floor 18.44x)
|
||||
log2 N=20 c1*c2=1.0 : certified share of honest energy <= 0.1581 at cb = cr (ratio floor 6.32x)
|
||||
log2 N=20 c1*c2=0.1 : certified share of honest energy <= 0.0500 at cb = cr (ratio floor 20.00x)
|
||||
log2 N=22 c1*c2=1.0 : certified share of honest energy <= 0.1508 at cb = cr (ratio floor 6.63x)
|
||||
log2 N=22 c1*c2=0.1 : certified share of honest energy <= 0.0477 at cb = cr (ratio floor 20.98x)
|
||||
log2 N=24 c1*c2=1.0 : certified share of honest energy <= 0.1443 at cb = cr (ratio floor 6.93x)
|
||||
log2 N=24 c1*c2=0.1 : certified share of honest energy <= 0.0456 at cb = cr (ratio floor 21.91x)
|
||||
cb/cr = 1: the factor sqrt(cb cr)/(cb+cr) = 0.5000 (0.5 is its maximum, at cb = cr)
|
||||
cb/cr = 10: the factor sqrt(cb cr)/(cb+cr) = 0.2875 (0.5 is its maximum, at cb = cr)
|
||||
cb/cr = 100: the factor sqrt(cb cr)/(cb+cr) = 0.0990 (0.5 is its maximum, at cb = cr)
|
||||
|
||||
== 5. the red-blue route's published constants (2018/221 Theorem 3.3 x Lemma 5.5 with Theorem 5.2) ==
|
||||
rho=0.25: ecost >= (eps/16) * (1-rho) N cb / 16 -> loss vs an honest N cb >= 341x at eps = 1 (cache 9m <= C' N^rho)
|
||||
rho=0.5: ecost >= (eps/16) * (1-rho) N cb / 16 -> loss vs an honest N cb >= 512x at eps = 1 (cache 9m <= C' N^rho)
|
||||
rho=0.75: ecost >= (eps/16) * (1-rho) N cb / 16 -> loss vs an honest N cb >= 1024x at eps = 1 (cache 9m <= C' N^rho)
|
||||
|
||||
== 6. the cache size at which DRSample has no transfer bound (2018/221 section 5.4: m >= C N / log2 N, C unknown) ==
|
||||
state 32 MiB, label 256 bits: N = 2^20, N/log2 N = 52429 labels = 1.60 MiB of cache (times C)
|
||||
state 32 MiB, label 8192 bits: N = 2^15, N/log2 N = 2185 labels = 2.13 MiB of cache (times C)
|
||||
state 128 MiB, label 256 bits: N = 2^22, N/log2 N = 190650 labels = 5.82 MiB of cache (times C)
|
||||
state 128 MiB, label 8192 bits: N = 2^17, N/log2 N = 7710 labels = 7.53 MiB of cache (times C)
|
||||
state 512 MiB, label 256 bits: N = 2^24, N/log2 N = 699051 labels = 21.33 MiB of cache (times C)
|
||||
state 512 MiB, label 8192 bits: N = 2^19, N/log2 N = 27594 labels = 26.95 MiB of cache (times C)
|
||||
state 4096 MiB, label 256 bits: N = 2^27, N/log2 N = 4971027 labels = 151.70 MiB of cache (times C)
|
||||
state 4096 MiB, label 8192 bits: N = 2^22, N/log2 N = 190650 labels = 186.18 MiB of cache (times C)
|
||||
|
||||
== 7. arithmetic of the 1.5x target against the published losses ==
|
||||
the certificate is G_upper / L <= 1.5 (plan section 2). If the composed theorem only proves L = E_honest_specialist / loss,
|
||||
then G_upper / L = loss * (G_upper / E_honest_specialist), and the certificate needs G_upper / E_honest_specialist <= 1.5 / loss.
|
||||
loss 6.6: a 1.5x certificate needs the GPU at <= 0.2273 of the honest specialist's energy (a GPU at parity certifies only 6.6x)
|
||||
loss 341: a 1.5x certificate needs the GPU at <= 0.0044 of the honest specialist's energy (a GPU at parity certifies only 341.0x)
|
||||
loss 512: a 1.5x certificate needs the GPU at <= 0.0029 of the honest specialist's energy (a GPU at parity certifies only 512.0x)
|
||||
27
docs/analysis/mhpow/b4/registry-batch-b4.json
Normal file
27
docs/analysis/mhpow/b4/registry-batch-b4.json
Normal file
|
|
@ -0,0 +1,27 @@
|
|||
{
|
||||
"run_id": "mhpow-b4-20261009-01",
|
||||
"manifest_sha": "",
|
||||
"method": "model",
|
||||
"evidence_dir": "docs/analysis/mhpow/b4",
|
||||
"release_identity": {
|
||||
"commit": "branch mhpow-b4 (the landing merge names the sha)",
|
||||
"lockfile": "",
|
||||
"binary": "",
|
||||
"network_object": "none: a theorem statement and an audit of published papers, no chain state read or written",
|
||||
"activation": "none (Track B lands documents and tests only)",
|
||||
"profile_hashes": "R1 2025/1456 13c3646e...; R2 2018/221 2a466b97...; R3 2017/225 29c5a9c0...; R4 2026/1024 aa6caa39...; R16 arXiv 2207.11519 ac273393...; params.py 7ac7fd48..., params.txt a98ac460..."
|
||||
},
|
||||
"claim_impact": "none: the composed accepted-proof energy statement is a draft with named proof obligations; the published constants cannot carry a 1.5x certificate (loss at least 6.6x on the generic route, at least 341x on the red-blue route); every row NOT RUN until the panel reads it",
|
||||
"reviewer": "",
|
||||
"note": "NOT RUN by this lane: the steward records it only if the coordinator asks, with the cell added to the map. BLOCKED rows B4-B01 to B4-B10 in README section 12.",
|
||||
"cells": [
|
||||
{
|
||||
"cell": "theory:mhpow-b4",
|
||||
"status": "NOT RUN",
|
||||
"method": "model",
|
||||
"evidence": "docs/analysis/mhpow/b4/README.md; docs/analysis/mhpow/b4/params.txt; docs/analysis/mhpow/b4/RUNS.md; tools/mhpow/b4/params.py",
|
||||
"note": "NOT RUN: statement and losses written; terms 2 (transfers) and the amortisation of terms 2 and 3 are open theorems; L is BLOCKED (no lower-bound certificate for any technology coefficient); X5 rows stay WITNESS (E_D)",
|
||||
"in_progress": true
|
||||
}
|
||||
]
|
||||
}
|
||||
|
|
@ -52,3 +52,6 @@ docs/analysis/class-v6/reference-population.md
|
|||
docs/analysis/class-v6/eco-05-scenarios.md
|
||||
docs/analysis/class-v6/eco-05-results.md
|
||||
docs/analysis/proving-outcome-ledger.md
|
||||
# 9 October 2026: Track B B4 (R15-07), the theory lane: the composed accepted-proof statement, its arithmetic and runs
|
||||
docs/analysis/mhpow/b4
|
||||
tools/mhpow/b4
|
||||
|
|
|
|||
82
tools/mhpow/b4/params.py
Normal file
82
tools/mhpow/b4/params.py
Normal file
|
|
@ -0,0 +1,82 @@
|
|||
#!/usr/bin/env python3
|
||||
"""B4 (R15-07) parameter arithmetic for the composed accepted-proof statement.
|
||||
|
||||
Standard library only. Every number printed here is arithmetic on the closed forms quoted in
|
||||
docs/analysis/mhpow/b4/README.md (theorem numbers there); nothing is measured and nothing here is a chip figure.
|
||||
Run on a build box, never the Mac: python3 tools/mhpow/b4/params.py > docs/analysis/mhpow/b4/params.txt
|
||||
"""
|
||||
import math
|
||||
|
||||
LN2 = math.log(2)
|
||||
DELTA = 2 # DRSample in-degree (2025/1456 Fact 8)
|
||||
|
||||
def lemma3_qmax_log2(lam):
|
||||
# 2025/1456 Lemma 3 hypothesis: lam/4 >= 2 log2 q + log2 indeg -> log2 q <= (lam/4 - log2 indeg)/2
|
||||
return (lam / 4 - math.log2(DELTA)) / 2
|
||||
|
||||
def theta_general(lam, log2q, s):
|
||||
# B4 restatement of the Lemma 3 counting: |sigma_i| >= theta |P_i| except with prob 2^-s per round,
|
||||
# theta = lam - 2 log2 q - log2 indeg - s (the paper's choice is theta = lam/4)
|
||||
return lam - 2 * log2q - math.log2(DELTA) - s
|
||||
|
||||
def blrz_qmax_log2(w):
|
||||
# 2018/221 Theorem 3.3 and Lemma 3.9: q < 2^(w/20) and 20 log2 n < w
|
||||
return w / 20
|
||||
|
||||
print("== 1. query ceilings: the theorems' hypotheses on q (total random-oracle queries of the prover) ==")
|
||||
print(f"{'label bits':>10} {'2025 L3 log2 q max':>20} {'BLRZ T3.3 log2 q max':>22} {'BLRZ max log2 N (20 log2 N < w)':>32}")
|
||||
for lam in (256, 512, 1024, 2048, 8192):
|
||||
print(f"{lam:>10} {lemma3_qmax_log2(lam):>20.1f} {blrz_qmax_log2(lam):>22.1f} {lam/20:>32.1f}")
|
||||
|
||||
print()
|
||||
print("== 2. bits per pebble theta at q = 2^64 queries, per-round failure 2^-64 (B4 restatement, NOT RUN) ==")
|
||||
for lam in (256, 512, 1024, 8192):
|
||||
th = theta_general(lam, 64, 64)
|
||||
print(f"label {lam:>5} bits: theta = {th:>7.0f} bits per pebble ({th/lam:.3f} of the label; the paper's fixed choice is 0.250)")
|
||||
|
||||
print()
|
||||
print("== 3. challenges k and proof bytes (2025/1456 Corollary 3: k = 2 lambda_s log2 N / c1, error q e^-lambda_s) ==")
|
||||
print("c1 is the DRSample depth-robustness constant of Fact 8; the paper gives no value (BLOCKED row B4-03)")
|
||||
lam_s = 128
|
||||
for logN in (17, 20, 22, 24):
|
||||
for c1 in (1.0, 0.25, 0.1):
|
||||
k = math.ceil(2 * lam_s * logN / c1)
|
||||
for w in (256, 8192):
|
||||
# each challenge opens the node and its DELTA parents, each opening = label + logN sibling hashes (256-bit nodes)
|
||||
opening = w / 8 + logN * 32
|
||||
proof = k * (DELTA + 1) * opening
|
||||
print(f"log2 N={logN:>2} c1={c1:<5} k={k:>7} label {w:>5} bits: proof <= {proof/2**20:>9.2f} MiB (no path sharing)")
|
||||
|
||||
print()
|
||||
print("== 4. the generic CMC-to-energy route (2018/221 Theorem 4.5): ceiling on what it can certify ==")
|
||||
print("E_lb = 2 sqrt(cmc cb cr / w) - m cb with cmc <= w (c1 N/log2 N)(c2 N)/2 gives E_lb <= N sqrt(cb cr) sqrt(2 c1 c2 / log2 N);")
|
||||
print("against an honest prover's energy >= N (cb + cr): share <= sqrt(2 c1 c2 / log2 N) * sqrt(cb cr)/(cb + cr), and sqrt(cb cr)/(cb + cr) <= 1/2")
|
||||
for logN in (17, 20, 22, 24):
|
||||
for c1c2 in (1.0, 0.1):
|
||||
f = 0.5 * math.sqrt(2 * c1c2 / logN)
|
||||
print(f"log2 N={logN:>2} c1*c2={c1c2:<4}: certified share of honest energy <= {f:.4f} at cb = cr (ratio floor {1/f:.2f}x)")
|
||||
for r in (1, 10, 100):
|
||||
g = math.sqrt(r) / (r + 1)
|
||||
print(f" cb/cr = {r:>3}: the factor sqrt(cb cr)/(cb+cr) = {g:.4f} (0.5 is its maximum, at cb = cr)")
|
||||
|
||||
print()
|
||||
print("== 5. the red-blue route's published constants (2018/221 Theorem 3.3 x Lemma 5.5 with Theorem 5.2) ==")
|
||||
for rho in (0.25, 0.5, 0.75):
|
||||
loss = 16 * 16 / (1 - rho)
|
||||
print(f"rho={rho}: ecost >= (eps/16) * (1-rho) N cb / 16 -> loss vs an honest N cb >= {loss:.0f}x at eps = 1 (cache 9m <= C' N^rho)")
|
||||
|
||||
print()
|
||||
print("== 6. the cache size at which DRSample has no transfer bound (2018/221 section 5.4: m >= C N / log2 N, C unknown) ==")
|
||||
for state_mib in (32, 128, 512, 4096):
|
||||
for w in (256, 8192):
|
||||
N = state_mib * 2**20 * 8 // w
|
||||
logN = math.log2(N)
|
||||
m = N / logN
|
||||
print(f"state {state_mib:>5} MiB, label {w:>5} bits: N = 2^{logN:.0f}, N/log2 N = {m:>10.0f} labels = {m*w/8/2**20:>8.2f} MiB of cache (times C)")
|
||||
|
||||
print()
|
||||
print("== 7. arithmetic of the 1.5x target against the published losses ==")
|
||||
print("the certificate is G_upper / L <= 1.5 (plan section 2). If the composed theorem only proves L = E_honest_specialist / loss,")
|
||||
print("then G_upper / L = loss * (G_upper / E_honest_specialist), and the certificate needs G_upper / E_honest_specialist <= 1.5 / loss.")
|
||||
for loss in (6.6, 341, 512):
|
||||
print(f"loss {loss:>5}: a 1.5x certificate needs the GPU at <= {1.5/loss:.4f} of the honest specialist's energy (a GPU at parity certifies only {loss:.1f}x)")
|
||||
Loading…
Reference in a new issue