HEGEMON
What verification establishes
A passing result means the listed checks completed on the identified block bytes. Hidden amounts stay private. The proof system’s assumptions still apply.
An additional check on public data
The explorer checks public data separately from the node and runs a configured released Hegemon verifier on private-spend proofs. This can reveal skipped checks, inconsistent data and some implementation failures.
It uses the released cryptographic implementation. A forged proof that passes that verifier, or a missing constraint in the shared relation, can also pass the explorer. Rechecking enforces existing rules; it does not increase the proof system’s soundness.
The checks behind a passing status
“Public checks passed” covers the contiguous indexed history from genesis to the displayed checked block. This is the configured node’s reported canonical view. The observer does not independently choose the winning chain.
| Check | What is tested |
|---|---|
| Action encoding and identity | Supported action framing and the selected network and proof identity. |
| Private-spend reference | The reference block hash and permitted age of 0–12 blocks. The note root is not reconstructed. |
| Nullifiers | No repeated public nullifiers across the complete indexed prefix. |
| Reward accounting | Public reward amounts and allocation follow the permitted subsidy-plus-fees rules. |
| Private-spend proof | The SHA-pinned released binary verifies the exact 688-byte statement and proof, with ciphertext binding checked. |
These checks do not independently reconstruct the note root, header hash, proof of work, difficulty adjustment or supply_digest. A per-block result covers that block; the global result also requires a complete checked prefix. Unknown or incomplete coverage never means passed.
What a passing result relies on
1. The executable implements the intended rules
The verifier must match the intended release and relation. Its parser, arithmetic, compiler and platform must behave correctly. Source review, checksums and fixture tests provide evidence, but are not a proof about every possible native execution.
The explorer adds a separate execution of public checks. It does not supply an independently implemented proof system or a complete proof that native bytes and execution match the Lean model.
2. The cryptographic assumptions hold
The proof model treats SHA-512 as an ideal oracle that can also receive quantum queries. Real SHA-512 is a fixed algorithm. The model also assumes bounds on the exact primitive attacks used in the native authorization argument, including attacks on commitments and their domains.
BLAKE2b implementation and commitment binding remain separate assumptions. A verifier cannot reliably diagnose a successful attack on the assumptions it uses to accept proofs.
The seven primitive attacks, in plain language
- Change a note without changing its commitment. Find different canonical 18-word note payloads with the same NOTE hash. Note-collision predicate ↗
- Change a tree node’s children without changing its hash. Find different ordered child-digest pairs with the same COMPFF node hash. Merkle-collision predicate ↗
- Make an ordinary output look like approval state. Match an ordinary recipient’s owner digest to an accumulator owner. The recipient can be an arbitrary canonical digest; the game does not assume a known secret-key preimage. Ordinary-recipient / accumulator predicate ↗
- Make locked value look like approval state. Match a value-note owner digest to an accumulator owner. Value / accumulator predicate ↗
- Substitute different approval state. Find different accumulator credentials, signer policy, intent or approval bits with the same owner digest. Accumulator-collision predicate ↗
- Confuse approval state with a hash/time lock. Match an accumulator owner to an HTLC owner. Accumulator / HTLC predicate ↗
- Make the known-empty placeholder look like approval state. Match an accumulator owner to the exact public SINGLE hash of
[1,0,0,0,0,0,0]. This is a fixed known target, not a zero digest or secret. Known-empty-target predicate ↗
3. The resource bounds include offline work
One oracle query is a modeled request for a hash result, including quantum queries. A single proof needs many queries. The budget covers the whole modeled history: other hash work, proof generation, verification and diagnostic traces, including failed and unused attempts.
For example, generating one proof and checking it on five nodes charges one generation and five verifications. Discarding a failed proof still uses the budget. An adversary’s offline work is not visible in a block explorer.
Transaction counts, chain height and restarts do not establish those bounds. The ongoing HGN route has no automatic chain expiry or accepted-proof quota; its security statements remain conditional on finite resources.
Exact resource class and source
4. Native data must match the formal model
The engineering assumption is that real note tables, append positions, historical roots and serialized inputs have their stated formal interpretation. The native-data interface supplies chronological data; it does not assume that a spender is authorized.
Inside the model, matching the proof producer, decoded assignment and history is derived, or the corresponding failure is accounted for. The same-source witness is a proved conclusion under the theorem’s hypotheses. It is not an extra assumption that “everything is valid,” and does not give the explorer a practical way to extract private amounts.
5. Privacy has its own conditions
The privacy argument assumes honest proofs from valid private inputs, the prescribed independent randomness, and the same well-formed initial state chosen before the oracle. Earlier oracle work must be included and charged.
It also uses an external mathematical bound on how much an observer can notice the public simulator changing selected oracle answers as requests evolve. This is the adaptive-reprogramming premise. Continuation queries, failed requests and errors remain part of the comparison.
The explorer does not test these conditions. Privacy and soundness are separate mathematical games; their individual bounds do not automatically form a combined security guarantee.
6. The observer has the right chain data
Results depend on the configured RPC source, local index and verifier executable. The observer can lag behind the chain. A reorganization changes which blocks are canonical and invalidates affected results.
An RPC source can withhold a competing chain. This service does not independently establish global chain selection or audit every consensus rule. An accounting or proof check does not imply that proof of work, difficulty adjustment and every state root were independently recomputed. The displayed coverage defines the claim.
Proved facts and supplied hypotheses
Lean checks that the conclusion follows from the stated inputs. It does not make every input a fact about deployed software or an adversary.
- Proved within the model: matching-source witness and failure bounds, coverage of unauthorized Finals by the listed games, the conditional privacy comparison, and resource-accounting arithmetic.
- Explicit hypotheses: primitive-attack probability bounds, their total allowance, query/read bounds, initialization, and the privacy argument’s valid requests and external adaptive-reprogramming premise.
- Model choices: ideal oracle behavior and independent randomness. Their real-world interpretation is not a cryptanalytic theorem.
- Engineering trust: the current source binding, native data interpretation, compiled parser/verifier and platform. The observer also relies on its RPC history and accurate coverage reporting.
Logical axioms are different from security hypotheses. Even an axiom audit with no extra project axioms would not remove a theorem’s explicit cryptographic inputs. This explorer performs no new Lean kernel or axiom audit.
Supply accounting is not a public balance total
The subsidy schedule limits authorized issuance. Hidden note conservation additionally relies on proof soundness, correct admission and the history assumptions above. Fees move existing value; they do not create new HGN.
The chain’s supply_digest is fee-inclusive gross accounting. It is not hidden circulating supply. The explorer can recompute public accounting; it cannot add up amounts concealed inside note commitments.
Exact release and theorem scope
The current software release is v0.11.4. These existing explorer checks remain pinned to public source tag v0.11.2. Its private-spend route is the 86-word BoundedPolicy.CompFF01.Packed.v4 relation, circuit 12, with HGPSLC02 carriers and compact SMZL/q38 proofs.
The linked 77-word SMZD/q58 and RP05 results are inherited evidence with their own identities. They do not independently certify the current 86-word bytes. The current source binding and qualification must also hold.
Named theorem entry points
NativePrivateSpendQ58CurrentAcceptedSourceInitialized128.initialized_accepted_no_source_witness_mass_below_128NativePrivateSpendQ58CurrentTotalNativeSourceOutcome.Collector.initialized_actual_native_global_failure_below_128NativePrivateSpendCurrentNativeHistoryJoin.current_native_final_authorization_or_failureNativePrivateSpendOngoingSecurity.current_initialized_history_below_149
Reproduce a proof check
The packaged node can verify a public statement and proof offline, without opening chain state or connecting to peers. Use the exact extracted bytes and record which binary you ran.
hegemon-node verify-private-spend --statement statement.bin --proof proof.bin
That command checks the cryptographic backend. Inclusion, reference freshness, nullifier uniqueness and public reward accounting need separate chain-context checks.