SPEC/RUN-A-NODE: reference point aere.pq.checkpoint documented, rewrite bound of 2026-10-07 in the formal table, 3.1 corrected by dated note; nothing removed

RUN-A-NODE.md

@@ -248,6 +248,10 @@ fleet runs (see the patch message). `run-node.sh` applies it, passes the four st
 `SHA256SUMS`. **If you built a node before, `run-node.sh` now rebuilds it**: the patch set is
 fingerprinted, and a binary built from another patch set is no longer reused.
 
+Note added 2026-10-07: one option that patch carries is of use to a follower today without activating
+any stage, the reference point `aere.pq.checkpoint`; it is documented below, after the configuration
+section.
+
 Measured 2026-10-01: patches 0001 and 0003 to 0008 applied with plain `git apply` on a pristine
 `d2032017` checkout reproduce the patch generator's tree with zero differences; the build has the
 same 3,554 classes as the fleet distribution, none only on one side, and **no class with different
@@ -416,6 +420,60 @@ IMPORT path reads: the registries (`aere.falcon.manifest` loads only together wi
 `aere.falcon.registry.history` carries every earlier registry the chain was signed against), the
 anchor-validation schedule (`aere.pq.*`), and the 1 Gwei base-fee floor live from block 10,141,734.
 
+### A reference point for a node that syncs from genesis: `aere.pq.checkpoint` (note added 2026-10-07)
+
+The configuration above gives a from-genesis node no knowledge of the chain beyond `genesis.json`.
+That is enough to verify every certificate it is served, and not enough to know that it was served
+the whole chain: a neighbour that controls what you see can hand you a history that stops before the
+first enforced anchor, or a tail of up to 32 blocks above the latest anchor's parent (33 counting
+the parent itself, in the case of the AIP-22 erratum of 2026-10-01), and nothing in the headers
+tells you that the honest chain is longer. That is the weak subjectivity every finality gadget has,
+and the answer is the one every such chain gives: give the node one recent anchor from outside the
+sync, and it refuses any chain that does not run through it. The argument, with the machine-checked
+model (every history that diverges at or below the reference is refused; without a reference a short
+divergence below an anchor is accepted, shown as a negative control), is
+`research/rewrite-bound-round-free-seal-2026-10-07.md` in the aere-research repository
+(https://git.aere.network/aere-network/aere-research/src/branch/main/research/rewrite-bound-round-free-seal-2026-10-07.md).
+
+The option is in patch 0008 (`PqCheckpointRule`, AIP-22 stage 4 code, inert unless set; the form below
+is the one the patch defines). Append it to `BESU_OPTS`:
+
+```
+-Daere.pq.checkpoint=<height>:<block hash>[,<height>:<block hash>...]
+```
+
+for example `-Daere.pq.checkpoint=20966864:0x<64 hex characters>`, the height and the 32-byte hash of
+an anchor block. What it does: a header at a named height whose hash is not the named one is refused
+at import (`AERE-PQC-CHECKPOINT-02` in the log, "a chain that does not run through the checkpoint is
+never adopted"), and every other height is not judged by it. Unset or blank: inert, every header
+passes; `run-node.sh` does not set it, and this document did not name it before today. A value the
+parser cannot read (no `:`, a height below 1, a hash that is not 32 bytes, the same height named twice)
+refuses at startup with `AERE-PQC-CHECKPOINT-01`; it never degrades to "no checkpoint". It is a
+separate rule from the anchor configuration, so naming it alone does not arm the anchor loader.
+
+When to use it: a node that syncs from genesis with no other knowledge of the chain, or any node whose
+peers you do not choose. A node already at the tip has its own head to compare against and gains less.
+
+How to choose the value, and the one thing not to do:
+
+- pick a recent ANCHOR height (on chain 2800 every 32nd block since block 20,746,736, that is
+  `h mod 32 == 16`; the dated interval schedule is in `SPEC.md` 3.1), so that the reference also
+  pins a certificate; the parser accepts any height, and a non-anchor height pins only a hash;
+- take the hash from somewhere the adversary of the argument does not control: the public verifier
+  (`tools/verify-anchor.mjs`, run from an empty directory as the documentation page "Verify an anchor"
+  gives it) names the anchor heights it verified, and `eth_getBlockByNumber` on a node you trust, or on
+  the two public endpoints compared against each other (the call is in "Check that you are on the right
+  chain" below), gives the block hash at such a height; a hash handed to you by the same peer that
+  serves you the blocks is no reference at all;
+- never guess or copy a stale value: a wrong hash at a named height makes the node refuse the honest
+  chain at that height and stop there, which is the rule doing exactly what it is for.
+
+What is and is not measured: the rule's own tests in the patch (`PqCheckpointRuleTest`) cover the
+refusal at the named height, the pass at every other height, the inert unset form and five malformed
+values; the model named above proves the reference-point property and runs its negative control.
+Refusing a served fork at a checkpoint height on a running node has not been exercised on any network,
+and the option is not part of the follower configuration above [NOT MEASURED].
+
 ---
 
 ## Start it

SPEC.md

@@ -5,6 +5,11 @@ that follows chain 2800 from block 0 to the live head and validates what the net
 without reading Aere source code. It specifies the follower (validation) protocol completely; it
 describes seal production only where a follower must understand it to validate.
 
+Amended 2026-10-07 (sections 3.1, 3.2, 6.4 and 7: the rewrite bound under the round-free seal model,
+machine-checked that day, enters the table of formal results; the sentence "protected by ECDSA alone,
+permanently" of section 3.1 is corrected to the reference-point form; the reference-point option
+`aere.pq.checkpoint` of patch 0008 is documented; nothing removed).
+
 ## 0. Conventions, and how every statement here is grounded
 
 Every normative statement in this document carries one of three markers:
@@ -476,6 +481,35 @@ certificate, only its grandparent, the block both siblings share.
 History below H remains protected by ECDSA alone, permanently (source:
 `anchor/consensus/common/.../PqAnchorConfig.java`, interval javadoc; `anchor/README.md`).
 
+Correction added 2026-10-07: the sentence above ("protected by ECDSA alone, permanently") is weaker
+than what holds for a node with a reference point and, for a node without one, an overstatement:
+ECDSA is exactly what this adversary holds. History below block 13,014,000 carries no certificates
+of its own and the anchor cannot reach backwards; what covers it is the hash chain. Every block hash
+covers its parent's hash, and an anchor's hash covers its certificate, whose seals sign the parent's
+hash, so a rewrite at ANY height changes every hash above it. A node that holds, from outside the
+sync, the height and block hash of one recent honest anchor (a reference point) therefore refuses
+every history that diverges at or below that anchor, since no such history reaches the reference
+with the same hash; above the reference the bound of this section applies (at most 32 blocks, the
+latest anchor and the 31 after it; 33 with the sealed-sibling exception above, which keeps the
+latest anchor's grandparent and everything below it; 128 and 129 in the dated 128-interval window).
+A node with no reference point, syncing from genesis, can be served a history that stops before the
+first enforced anchor, or a 32-block (33-block) tail with no honest head to compare against, and
+cannot tell that the honest chain is longer: the weak subjectivity of every finality gadget, and
+below the first enforced anchor such a node has no post-quantum cover at all. The published patch
+set carries the reference-point option, `aere.pq.checkpoint=<height>:<block hash>`
+(`PqCheckpointRule`, patch 0008, AIP-22 stage 4 code; inert unless set; semantics in section 3.2,
+operator guidance in `RUN-A-NODE.md`, "A reference point for a node that syncs from genesis"). The
+argument, and the z3 model that checks it (the hash chain unrolled for 1,280 heights, properties P3a
+and P3b, with the negative control P3c showing that without a reference a short divergence below an
+anchor is ACCEPTED), are `../aere-research/research/rewrite-bound-round-free-seal-2026-10-07.md` and
+`../aere-research/formal-consensus/anchor_rewrite_bound_roundfree_smt.py` (public:
+https://git.aere.network/aere-network/aere-research/src/branch/main/research/rewrite-bound-round-free-seal-2026-10-07.md);
+the threat-model page has carried the reference-point form since 2026-10-05. The bound itself (32
+and 33 above block 20,746,736; 128 and 129 in the dated window) is machine-checked since 2026-10-07:
+section 7 (source: `../aere-research/research/rewrite-bound-round-free-seal-2026-10-07.md`, sections
+0 to 5 and 7; `../aere-research/formal-consensus/anchor_rewrite_bound_roundfree_smt.py` and its
+`RESULT.txt`; `patches/0008-aere-pq-aip22.patch`, `PqCheckpointRule`).
+
 ### 3.2 Activation is by node configuration, not by genesis, and that is a real caveat
 
 All anchor parameters are read from JVM system properties (`BESU_OPTS`), with environment-variable
@@ -559,6 +593,23 @@ Semantics of each parameter (source: `PqAnchorConfig.java`):
   verifies every block ever produced) (source: `registries/README.md`, `RUN-A-NODE.md`).
 - `aere.falcon.forkBlock`: a validator-side legacy per-block rule; see section 8, D6. A follower
   leaves it unset.
+- `aere.pq.checkpoint` (added to this list 2026-10-07; in the recipe since patch 0008 of 2026-10-01,
+  AIP-22 stage 4 code): `<height>:<block hash>[,<height>:<block hash>...]`, read by `PqCheckpointRule`,
+  an attached header rule of the QBFT rule set (`QbftBlockHeaderValidationRulesetFactory`, patch 0008),
+  NOT by `PqAnchorConfig`, so it is not one of the names whose presence arms the anchor loader above.
+  A header at a named height whose hash is not the named hash is refused at import
+  (`AERE-PQC-CHECKPOINT-02`, "a chain that does not run through the checkpoint is never adopted");
+  every other height is not judged by it. Unset or blank: inert, every header passes; `run-node.sh`
+  does not set it. A value that does not parse (no `:`, a height below 1, a hash that is not 32 bytes,
+  a height named twice) refuses at load with `AERE-PQC-CHECKPOINT-01` and never degrades to "no
+  checkpoint". It is the reference point of section 3.1 (correction of 2026-10-07): a from-genesis
+  node with no other knowledge of the chain names one recent anchor it trusts, and every history that
+  does not run through it is refused (source: `patches/0008-aere-pq-aip22.patch`,
+  `PqCheckpointRule.java` and its wiring; `RUN-A-NODE.md`, "A reference point for a node that syncs
+  from genesis"). The rule's own tests in the patch (`PqCheckpointRuleTest`) cover the refusal at the
+  named height, the pass at every other height, the inert unset form and five malformed values;
+  refusing a served fork at a checkpoint height on a running node has not been exercised on any
+  network [NOT MEASURED].
 
 An armed node refuses to start in any sync mode other than FULL (`PqAnchorSyncModeGuard`,
 `REQUIRED_MODE = "FULL"`) (source:
@@ -968,6 +1019,19 @@ set it will have at the evaluated HEIGHT (rather than at startup) can enforce th
 end to end; the published Besu-based package does not do this today [NOT MEASURED: no such
 implementation exists to compare against].
 
+Note added 2026-10-07: two separate things about this follower, in the terms of the rewrite-bound
+document of that date (this specification's section 7; the document's section 5). First, the
+ceiling: against an adversary holding every classical validator key and no post-quantum key, the
+follower at effective K=1 keeps the same bound as a validator at K=7 (at most 32 blocks above the
+latest anchor's parent, or 33 counting the parent itself in the sealed-sibling exception; model
+properties P5a, P5b), because one seal the adversary cannot make is enough; what the ceiling costs
+is that ONE leaked or misused validator post-quantum key makes this follower's rewrite depth
+unbounded (negative control N5d), where a validator at K=7 needs seven such keys (N4a). Second, the
+reference point: the configuration above gives a from-genesis node no knowledge of the chain beyond
+`genesis.json`, so it cannot tell a complete history from one that stops early (section 3.1,
+correction of 2026-10-07); `aere.pq.checkpoint` (section 3.2; `RUN-A-NODE.md`) is the published
+answer, and `run-node.sh` does not set it.
+
 ### 6.5 Facts a syncing client will observe, so they are expectations rather than surprises
 
 - Blocks are almost all empty; the chain advances ~2 blocks/second after the rate change.
@@ -1003,6 +1067,12 @@ Suite status [MEASURED 2026-08-24, `python run_consensus_verification.py`, Windo
 35 models, 35 pass (14 consensus + 11 contract + 10 application), 282 PROVED + 149 CEX-FOUND,
 0 FAILED, ~39 s wall (source: `RULEAZA-TOT.md`).
 
+Note added 2026-10-07 [MEASURED 2026-10-07, same runner, Windows, python 3.14.4, z3 4.16.0]: 37 models,
+37 pass (16 consensus + 11 contract + 10 application), 301 PROVED + 159 CEX-FOUND, 0 FAILED, ~37 s
+wall; the two consensus models added since the measurement above are `pq_message_enforcement_smt.py`
+(2026-09-02, section 2.6) and `anchor_rewrite_bound_roundfree_smt.py` (2026-10-07, the last row of the
+table below) (source: `anchor_rewrite_bound_roundfree_smt.RESULT.txt`).
+
 Consensus properties proven, with tool and scale (source: `RULEAZA-TOT.md` and the repository
 document `strategie/VERIFICARE-FORMALA-2026-08-24.md`):
 
@@ -1018,6 +1088,7 @@ document `strategie/VERIFICARE-FORMALA-2026-08-24.md`):
 | A round change on an anchor height cannot yield two different valid certificates; uniqueness comes from binding to the FINALIZED block, not from K (K=3 alone admits two, shown SAT). Note added 2026-10-01: a property of the MODEL only; the shipped rule does not require the certified block to be the decided one, and the AIP-22 erratum of that date shows a valid certificate over a block no round decided | SMT N=9 | `anchor_viewchange_smt.py` |
 | Emergency ceiling only lowers K | SMT | `pqanchor_ceiling_monotonicity_smt.py` |
 | Registry rotation covers every height exactly once; index binding | SMT | `registry_rotation_coverage_smt.py`, `registry_index_binding_smt.py` |
+| Added 2026-10-07. Rewrite bound under the round-free seal model (the AIP-22 erratum of 2026-10-01): an adversary holding every classical validator key and fewer than K_eff post-quantum keys can replace at most 32 blocks (the latest anchor and the 31 after it; the anchor's certificate is about its parent, so the anchor block itself is replaceable), 33 with the sealed-sibling exception (the latest anchor's grandparent and everything below it kept); 128 and 129 in the dated 128-interval window; the published follower at K_eff=1 keeps 32 and 33 against no post-quantum key; with a reference anchor everything through it is kept (the hash chain unrolled for 1,280 heights). 13 proofs, 2 lemmas, 4 configuration witnesses, 8 negative controls, all fired (no certificate needed, every post-quantum key, K_eff post-quantum keys, one key against the follower, no common grandparent, a hash that does not cover the parent, a certificate outside the hashed pre-image, no reference point); `--plant-bounds`, every claimed bound one too low, fails exactly the ten bound proofs and exits 1, so the bounds are tight. Combinatorics of acceptance over heights, not cryptography: keccak and Falcon-512 modelled as injective and unforgeable, QBFT safety assumed while the honest history was produced, the second scheme omitted (which only makes the real acceptance stricter), the sealed-sibling premise taken as free for any number of honest sibling seals, and "every anchor in the alternative history is accepted" checked on the first 40 anchor heights above the fork | SMT, z3; the regime in force today (fork above 20,746,736, interval 32, K=7) and the dated 128 window separately; `--plant-bounds` as the control of the control | `anchor_rewrite_bound_roundfree_smt.py` (argument: `../aere-research/research/rewrite-bound-round-free-seal-2026-10-07.md`; public: https://git.aere.network/aere-network/aere-research/src/branch/main/formal-consensus/anchor_rewrite_bound_roundfree_smt.py) |
 
 The honest boundary, stated as prominently as the results (source: `RULEAZA-TOT.md`, "Granita
 cinstita"; `VERIFICARE-FORMALA-2026-08-24.md`):
@@ -1037,6 +1108,14 @@ cinstita"; `VERIFICARE-FORMALA-2026-08-24.md`):
   and is not claimed.
 - Nothing in the formal results implies "post-quantum consensus" per block; the anchor is additive
   (section 3.1).
+- Added 2026-10-07: the rewrite-bound model bounds what a node ACCEPTS, not what an adversary can
+  deliver; it assumes the node holds the published registry epochs (an epoch fetched at sync time over
+  a channel the adversary controls is outside it), it does not model delivery, the transport layer or
+  either client's code, and z3 does not induct: the reference-point property is the hash chain unrolled
+  for 1,280 heights with the induction step as a lemma, and the acceptance of every anchor in the
+  alternative history is checked on the first 40 anchor heights above the fork. Whether the
+  sealed-sibling exception can be brought about on a network is not a question the model answers; it
+  takes the sealed sibling as given and bounds the rewrite even then.
 
 ---