Merge branch 'feature-export-rng' into feature-export-rng-lean

Use the agreed exportSigSetHash sidecar map, not the live ExportSigCollector, as the network-mode ttEXPORT signer snapshot. Preserve export convergence state through RNG onPreBuild cleanup so buildLCL apply can see the gate result, and require a UNLReport-backed validator view before non-standalone Export finalization. Add regression coverage for agreed-vs-live collector mutation and onPreBuild export-state preservation.

.codecov.yml

@@ -1,6 +1,37 @@
+codecov:
+  require_ci_to_pass: true
+
+comment:
+  behavior: default
+  layout: reach,diff,flags,tree,reach
+  show_carryforward_flags: false
+
 coverage:
+  range: "60..80"
+  precision: 1
+  round: nearest
   status:
     project:
       default:
         target: 60%
         threshold: 2%
+    patch:
+      default:
+        target: auto
+        threshold: 2%
+    changes: false
+
+github_checks:
+  annotations: true
+
+parsers:
+  cobertura:
+    partials_as_hits: true
+    handle_missing_conditions : true
+
+slack_app: false
+
+ignore:
+  - "src/test/"
+  - "include/xrpl/beast/test/"
+  - "include/xrpl/beast/unit_test/"

.git-blame-ignore-revs

@@ -1,8 +1,25 @@
 # This feature requires Git >= 2.24
 # To use it by default in git blame:
 # git config blame.ignoreRevsFile .git-blame-ignore-revs
+# Format first-party source according to .clang-format
 50760c693510894ca368e90369b0cc2dabfd07f3
-e2384885f5f630c8f0ffe4bf21a169b433a16858
-241b9ddde9e11beb7480600fd5ed90e1ef109b21
-760f16f56835663d9286bd29294d074de26a7ba6
-0eebe6a5f4246fced516d52b83ec4e7f47373edd
+# Reintroduce Clang-Format & Levelization
+da1d20d6d5d862716125d60899b80fab5302954a
+# Consolidate external libraries
+da1d20d6d5d862716125d60899b80fab5302954a
+# Rename .hpp to .h
+0345a2645d0f5ad900f4fbbcaff96040d3a887fc
+# Format formerly .hpp files
+5a227dc719016e10045e17c9396ad401118044f1
+# Rewrite includes
+e61880699997398f5a746e6c4034edc7632661f5
+# Move CMake directory (#4997)
+e47b1c1b3b97c3f6d11858ee02f463596e29e7f0
+# Rearrange sources (#4997)
+bfafa2bb39e562901736d656806bd700c3699a2f
+# Rewrite includes (#4997)
+e61880699997398f5a746e6c4034edc7632661f5
+# Recompute loops (#4997)
+d25b5dcd568bb96c18e347d55fac10fe901a1bfb
+# Reformat code with clang-format-18
+02749feea88ce61c1f7eeb2d61a57d8ecf07ab11

.github/workflows/check-genesis-hooks.yml

@@ -40,7 +40,7 @@ jobs:
         run: |
           # Download install.sh
           curl -o /tmp/wasienv-install.sh https://raw.githubusercontent.com/wasienv/wasienv/master/install.sh
-          
+
           # Replace /bin to /local/bin
           sed -i 's|/bin|/local/bin|g' /tmp/wasienv-install.sh
 

.github/workflows/formal-verification.yml

@@ -0,0 +1,127 @@
+name: Formal Verification (Lean)
+
+on:
+  push:
+    branches: ["feature-export-rng-lean"]
+  pull_request:
+    branches: ["**"]
+    types: [opened, synchronize, reopened]
+  workflow_dispatch:
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  lean-consensus:
+    name: Lean/C++ drift checks
+    runs-on: [self-hosted, macOS]
+    env:
+      BUILD_DIR: .build-formal
+      CMAKE_BUILD_DIR: .build-formal-cmake
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: Add Homebrew to PATH
+        run: |
+          echo "/opt/homebrew/bin" >> "$GITHUB_PATH"
+          echo "/opt/homebrew/sbin" >> "$GITHUB_PATH"
+
+      - name: Install core tools
+        run: |
+          brew install coreutils
+          echo "Num proc: $(nproc)"
+
+      - name: Setup toolchain (mise)
+        uses: jdx/mise-action@v3.6.1
+        with:
+          cache: false
+          install: true
+          mise_toml: |
+            [tools]
+            cmake = "3.25.3"
+            python = "3.12"
+            pipx = "latest"
+            conan = "2"
+            ninja = "latest"
+
+      - name: Install tools via mise
+        run: |
+          mise install
+          mise reshim
+          echo "$HOME/.local/share/mise/shims" >> "$GITHUB_PATH"
+
+      - name: Install Lean toolchain
+        run: |
+          toolchain="$(cat formal_verification/lean-toolchain)"
+          curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
+            | sh -s -- -y --default-toolchain "$toolchain"
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+          "$HOME/.elan/bin/lake" --version
+          "$HOME/.elan/bin/lean" --version
+
+      - name: Build Lean proofs
+        run: |
+          cd formal_verification
+          "$HOME/.elan/bin/lake" build XahauConsensus:static
+
+      - name: Detect compiler version
+        id: detect-compiler
+        run: |
+          compiler_version=$(clang --version | grep -oE 'version [0-9]+' | grep -oE '[0-9]+')
+          echo "compiler_version=${compiler_version}" >> "$GITHUB_OUTPUT"
+          echo "Detected Apple Clang version: ${compiler_version}"
+
+      - name: Configure Conan profile
+        run: |
+          mkdir -p ~/.conan2/profiles
+          cat > ~/.conan2/profiles/default <<EOF
+          [settings]
+          arch=armv8
+          build_type=Debug
+          compiler=apple-clang
+          compiler.cppstd=20
+          compiler.libcxx=libc++
+          compiler.version=${{ steps.detect-compiler.outputs.compiler_version }}
+          os=Macos
+
+          [conf]
+          tools.build:cxxflags=["-Wno-missing-template-arg-list-after-template-kw"]
+          EOF
+          conan profile show
+
+      - name: Export custom Conan recipes
+        run: |
+          conan export external/snappy --version 1.1.10 --user xahaud --channel stable
+          conan export external/soci --version 4.0.3 --user xahaud --channel stable
+          conan export external/wasmedge --version 0.11.2 --user xahaud --channel stable
+
+      - name: Install Conan dependencies
+        env:
+          CONAN_REQUEST_TIMEOUT: 180
+        run: |
+          conan install . \
+            --output-folder "$BUILD_DIR" \
+            --build missing \
+            --settings build_type=Debug \
+            -o '&:tests=True' \
+            -o '&:xrpld=True' \
+            -o '&:formal_verification=True'
+
+      - name: Configure formal build
+        run: |
+          cmake -S . -B "$CMAKE_BUILD_DIR" -G Ninja \
+            -DCMAKE_TOOLCHAIN_FILE="$PWD/$BUILD_DIR/build/generators/conan_toolchain.cmake" \
+            -DCMAKE_BUILD_TYPE=Debug \
+            -Dtests=ON \
+            -Dxrpld=ON \
+            -Dformal_verification=ON
+
+      - name: Build formal-enabled rippled
+        run: |
+          cmake --build "$CMAKE_BUILD_DIR" --target rippled --parallel "$(nproc)"
+
+      - name: Run Lean/C++ drift checks
+        run: |
+          "$CMAKE_BUILD_DIR/rippled" --unittest=LeanConsensus --unittest-log

.gitignore

@@ -127,5 +127,12 @@ bld.rippled/
 generated
 .vscode
 
+# AI docs (local working documents)
+.ai-docs/
+
+# Local formal-methods workspace; kept as a separate repository and optionally
+# symlinked here for navigation.
+formal/lean/xahau_consensus
+
 # Suggested in-tree build directory
 /.build/

.testnet/.gitignore

@@ -0,0 +1,4 @@
+output/
+__pycache__/
+scenarios/odd-cases/
+scenarios/suite-experiments.yml

.testnet/scenarios/entropy/consensus_entropy_crash.py

@@ -0,0 +1,29 @@
+"""Scenario: ConsensusEntropy amendment crashes non-supporting node.
+
+Votes ConsensusEntropy accept on all nodes except n4, then waits for n4
+to crash as the amendment activates without its support.
+
+    x-testnet run --scenario-script consensus_entropy_crash.py
+"""
+
+from helpers import CONSENSUS_ENTROPY_FEATURE
+
+
+async def scenario(ctx, log):
+    await ctx.wait_for_ledger_close()
+    ctx.feature(CONSENSUS_ENTROPY_FEATURE, vetoed=False, exclude_nodes=[4])
+
+    log("Waiting for ConsensusEntropy to be voted for...")
+    await ctx.wait_for_feature(
+        CONSENSUS_ENTROPY_FEATURE,
+        check=lambda s: not s.get("vetoed"),
+        exclude_nodes=[4],
+        timeout=60,
+    )
+
+    log("Waiting for n4 to crash...")
+    op = await ctx.wait_for_nodes_down(nodes=[4], timeout=600)
+
+    ctx.assert_log("unsupported amendments activated", since=op.started, nodes=[4])
+    ctx.assert_exit_status(0, nodes=[4])
+    log("PASS: n4 shut down due to unsupported amendment")

.testnet/scenarios/entropy/entropy_with_transactions.py

@@ -0,0 +1,52 @@
+""":descr: entropy stays valid under transaction load"""
+
+from __future__ import annotations
+
+from helpers import require_entropy, get_entropy_tx, assert_valid_entropy
+
+variants = [
+    {"label": "light", "min_txns": 5, "max_txns": 10},
+    {"label": "heavy", "min_txns": 50, "max_txns": 60},
+    {"label": "super_heavy", "min_txns": 90, "max_txns": 120},
+]
+
+
+async def scenario(ctx, log, *, min_txns=5, max_txns=10, **_):
+    await require_entropy(ctx, log)
+
+    gen = ctx.txn_generator(min_txns=min_txns, max_txns=max_txns)
+    await gen.start()
+    await gen.wait_until_ready()
+    log(f"Transaction generator ready ({min_txns}-{max_txns} txns/ledger)")
+
+    # Wait for pipeline warmup + a few txn-bearing ledgers.
+    await ctx.wait_for_ledgers(3, node_id=0, timeout=60)
+
+    start_seq = ctx.validated_ledger_index(0)
+    await ctx.wait_for_ledgers(10, node_id=0, timeout=120)
+    end_seq = ctx.validated_ledger_index(0)
+    log(f"Inspecting ledgers {start_seq + 1} → {end_seq}")
+
+    digests = set()
+    total_user_txns = 0
+
+    for seq in range(start_seq + 1, end_seq + 1):
+        ce, user_txns = get_entropy_tx(ctx, seq)
+        digest, count = assert_valid_entropy(ce, seq, seen_digests=digests)
+        total_user_txns += len(user_txns)
+        log(
+            f"  Ledger {seq}: EntropyCount={count} "
+            f"user_txns={len(user_txns)} Digest={digest[:16]}..."
+        )
+
+    await gen.stop()
+
+    log(
+        f"Verified {end_seq - start_seq} ledgers: {total_user_txns} user txns, "
+        f"all entropy valid and unique"
+    )
+
+    if total_user_txns == 0:
+        raise AssertionError("No user transactions were included in any ledger")
+
+    log("PASS")

.testnet/scenarios/entropy/fallback_without_unl_report.py

@@ -0,0 +1,28 @@
+""":descr: healthy non-standalone testnet without UNLReport mints Tier 1 fallback"""
+
+from __future__ import annotations
+
+from helpers import require_entropy, get_entropy_tx, assert_consensus_fallback
+
+
+async def scenario(ctx, log):
+    await require_entropy(ctx, log)
+
+    # Non-standalone nodes require a ledger-anchored UNLReport before assigning
+    # validator_quorum / participant_aligned labels. Without it, the RNG pipeline
+    # may still collect commits/reveals, but injection must remain Tier 1.
+    await ctx.wait_for_ledgers(3, node_id=0, timeout=60)
+    log("Pipeline warmed up without UNLReport")
+
+    start_seq = ctx.validated_ledger_index(0)
+    await ctx.wait_for_ledgers(5, node_id=0, timeout=90)
+    end_seq = ctx.validated_ledger_index(0)
+    log(f"Inspecting ledgers {start_seq + 1} -> {end_seq}")
+
+    for seq in range(start_seq + 1, end_seq + 1):
+        ce, _ = get_entropy_tx(ctx, seq)
+        digest, count = assert_consensus_fallback(ce, seq)
+        log(f"  Ledger {seq}: EntropyCount={count} Digest={digest[:16]}...")
+
+    log(f"Verified {end_seq - start_seq} ledgers: all consensus_fallback")
+    log("PASS")

.testnet/scenarios/entropy/participant_aligned_smoke.py

@@ -0,0 +1,160 @@
+""":descr: 5/6 validator_quorum, 4/6 participant_aligned (tier 2), recovery
+
+Requires node_count: 6 (see suite.yml) — the smallest NON-degenerate Tier 2
+size. At n=6: tier2 floor = 4, validator quorum = 5, validation quorum = 5. So
+  6/6, 5/6 present -> validator_quorum  (EntropyTier=3)
+  4/6 present      -> participant_aligned (EntropyTier=2, count 4)   <-- the band
+  3/6 present      -> consensus_fallback (EntropyTier=1)
+n=5 has NO tier-2 band (tier2 == quorum == 4), which is why the existing
+degradation smoke at 5 nodes only ever sees tier 3 / fallback.
+
+KEY: the 4/6 window is BELOW the 80% validation quorum (5). The 4 survivors
+keep CLOSING ledgers that carry tier-2 entropy, but those ledgers do NOT
+validate until the network recovers — exactly the transition window Tier 2
+serves. So validated_ledger_index() stalls; we instead inspect a surviving
+node's CLOSED ledger (its LCL) directly, and cross-check the injection from the
+cohort's logs.
+"""
+
+from __future__ import annotations
+
+from helpers import (
+    require_entropy,
+    get_entropy_tx,
+    assert_participant_aligned,
+    assert_validator_quorum,
+)
+
+
+def _closed_entropy(result):
+    """(seq, ConsensusEntropy tx) from a ctx.ledger('closed', transactions=True)
+    result, or (None, None) if the fetch returned no usable ledger.
+
+    Enforces the per-ledger invariant that an entropy-enabled closed ledger
+    carries EXACTLY ONE ConsensusEntropy pseudo-tx (mirroring get_entropy_tx):
+    a duplicate or missing injection raises here with a clear error instead of
+    being silently skipped and resurfacing later as a generic 'no tier-2 ledger'.
+    """
+    if not result or not isinstance(result.get("ledger"), dict):
+        return None, None
+    led = result["ledger"]
+    try:
+        seq = int(led.get("ledger_index"))
+    except (TypeError, ValueError):
+        return None, None
+    ce = [
+        t
+        for t in led.get("transactions", [])
+        if isinstance(t, dict) and t.get("TransactionType") == "ConsensusEntropy"
+    ]
+    if len(ce) != 1:
+        raise AssertionError(
+            f"Closed ledger {seq}: expected 1 ConsensusEntropy txn, got {len(ce)}"
+        )
+    return seq, ce[0]
+
+
+async def scenario(ctx, log):
+    await require_entropy(ctx, log)
+
+    # Baseline: healthy 6/6 produces validator_quorum entropy.
+    await ctx.wait_for_ledgers(1, node_id=0, timeout=30)
+
+    # --- 5/6: settles back to validator_quorum (5 present >= quorum 5) ---
+    val_before_drop = ctx.validated_ledger_index(0)
+    ctx.stop_node(5)
+    await ctx.wait_for_nodes_down(nodes=[5], timeout=30)
+    # Settle a few ledgers past the membership change. The ledger right at a
+    # validator drop can carry a transient consensus_fallback (tier 1, count 0,
+    # deterministic and by design) before the commit/reveal pipeline re-primes,
+    # so we do NOT assume any single post-drop ledger is already tier 3.
+    await ctx.wait_for_ledgers(4, node_id=0, timeout=90)
+
+    # 5/6 is at/above the 80% quorum (5), so steady state is validator_quorum.
+    # Scan the post-drop validated ledgers (all carry the 5-node cohort, so a
+    # tier-3 here has count == 5) and require at least one clean validator_quorum
+    # — EntropyTier=3, count >= quorum, non-zero digest — tolerating the
+    # transition fallback instead of depending on where the tip happened to land.
+    val_5of6 = ctx.validated_ledger_index(0)
+    t3_seq = None
+    for seq in range(val_5of6, val_before_drop, -1):
+        ce, _ = get_entropy_tx(ctx, seq)
+        tier = ce.get("EntropyTier")
+        log(f"  5/6 ledger {seq}: tier={tier} count={ce.get('EntropyCount')}")
+        if tier == 3:
+            assert_validator_quorum(ce, seq, min_count=5)
+            t3_seq = seq
+            break
+    if t3_seq is None:
+        raise AssertionError(
+            f"5/6: no validator_quorum (tier 3) entropy in post-drop validated "
+            f"ledgers {val_before_drop + 1}..{val_5of6}"
+        )
+    log(f"5/6: validator_quorum at validated seq {t3_seq}")
+
+    #@@start test-participant-aligned-window
+    # --- 4/6: participant_aligned (Tier 2) degraded window ---
+    ctx.stop_node(4)
+    await ctx.wait_for_nodes_down(nodes=[4], timeout=30)
+
+    # ~12s window: confirm tier-2 INJECTION from the cohort's logs, and that the
+    # round is NOT the impossible/fallback path (which is what distinguishes the
+    # tier-2 band from the tier-1 fallback regime).
+    op = await ctx.sleep(12, name="tier2_window")
+    selected_t2 = ctx.search_logs(
+        r"RNG: entropy selected seq=\d+ tier=2 count=4",
+        within=op.window,
+        nodes=[0, 1, 2, 3],
+    )
+    log(f"4/6: 'entropy selected tier=2 count=4' logs: {selected_t2.count}")
+    if selected_t2.count == 0:
+        raise AssertionError(
+            "4/6 window injected no participant_aligned (tier 2) entropy: no "
+            "'RNG: entropy selected ... tier=2 count=4' on the surviving cohort"
+        )
+    ctx.assert_not_log(
+        r"reason=impossible-entropy-gate", within=op.window, nodes=[0, 1, 2, 3]
+    )
+
+    # Verify the on-ledger EntropyTier=2 DIRECTLY: validation is stalled (4 < 5),
+    # so sample the surviving cohort's CLOSED ledger (its LCL — built but not yet
+    # validated). At least one must be participant_aligned with EntropyCount=4.
+    tier2_on_ledger = 0
+    last_seq = None
+    for _ in range(5):
+        seq, ce = _closed_entropy(
+            ctx.ledger("closed", transactions=True, node_id=0)
+        )
+        if ce is not None and seq is not None and seq != last_seq:
+            last_seq = seq
+            tier = ce.get("EntropyTier")
+            count = ce.get("EntropyCount", -1)
+            log(f"  closed ledger {seq}: tier={tier} count={count}")
+            if tier == 2:
+                assert_participant_aligned(ce, seq, expected_count=4)
+                tier2_on_ledger += 1
+        await ctx.sleep(3)
+
+    if tier2_on_ledger == 0:
+        raise AssertionError(
+            "no closed participant_aligned (tier 2) ledger observed during the "
+            "4/6 window (tier 2 was injected per logs, but not seen on a closed "
+            "ledger)"
+        )
+    log(f"4/6: {tier2_on_ledger} participant_aligned closed ledger(s) verified")
+    #@@end test-participant-aligned-window
+
+    # --- Recovery: liveness — validation resumes once quorum is restored ---
+    ctx.start_node(4)
+    ctx.start_node(5)
+    await ctx.wait_for_ledgers(1, node_id=0, timeout=120)
+
+    val_recovered = ctx.validated_ledger_index(0)
+    if not val_recovered or val_recovered <= val_5of6:
+        raise AssertionError(
+            f"Validated ledger did not advance after recovery "
+            f"({val_5of6} -> {val_recovered})"
+        )
+    log(f"Recovered: validated seq {val_5of6} -> {val_recovered}")
+
+    log("PASS")

.testnet/scenarios/entropy/quorum_degradation_smoke.py

@@ -0,0 +1,148 @@
+""":descr: 4/5 liveness, 3/5 fallback-entropy (consensus_fallback), recovery"""
+
+from __future__ import annotations
+
+from helpers import ZERO_DIGEST, require_entropy, get_entropy_tx, entropy_fields
+
+
+async def scenario(ctx, log):
+    await require_entropy(ctx, log)
+
+    # Baseline: wait 1 ledger to confirm network is healthy.
+    await ctx.wait_for_ledgers(1, node_id=0, timeout=30)
+
+    # --- 4/5 liveness ---
+    ctx.stop_node(4)
+    await ctx.wait_for_nodes_down(nodes=[4], timeout=30)
+    await ctx.wait_for_ledgers(1, node_id=0, timeout=30)
+    log("4/5: liveness OK")
+
+    # Snapshot validated seq before dropping to 3/5.
+    val_before = ctx.validated_ledger_index(0)
+
+    # --- 3/5 degraded window ---
+    ctx.stop_node(3)
+    await ctx.wait_for_nodes_down(nodes=[3], timeout=30)
+
+    # 10s ≈ 3 rounds at 3s cadence.
+    await ctx.sleep(10)
+
+    val_after = ctx.validated_ledger_index(0)
+    log(f"3/5: validated ledger {val_before} → {val_after}")
+
+    # Accepted/built ledgers may still later appear as validated once the full
+    # network rejoins. For ConsensusEntropy the key invariant is that every
+    # ledger created during this sub-quorum window carries FALLBACK entropy
+    # (consensus_fallback: non-zero consensus-bound digest, count 0) — never
+    # validator-tier entropy.
+    degraded_fallback = 0
+    degraded_end = val_after or val_before
+    if val_before and degraded_end and degraded_end > val_before:
+        for seq in range(val_before + 1, degraded_end + 1):
+            ce, _ = get_entropy_tx(ctx, seq)
+            digest, entropy_count, is_fallback = entropy_fields(ce)
+            tier = ce.get("EntropyTier")
+
+            # consensus_fallback (EntropyTier=1): explicit tier, count 0,
+            # deterministic NON-zero digest.
+            if tier != 1:
+                raise AssertionError(
+                    f"Ledger {seq}: expected EntropyTier==1 "
+                    f"(consensus_fallback) during 3/5 window, got {tier} "
+                    f"(EntropyCount={entropy_count})"
+                )
+            if entropy_count != 0:
+                raise AssertionError(
+                    f"Ledger {seq}: fallback EntropyCount must be 0, got "
+                    f"{entropy_count}"
+                )
+            if not digest or digest == ZERO_DIGEST:
+                raise AssertionError(
+                    f"Ledger {seq}: fallback digest must be non-zero "
+                    f"(consensus_fallback), got {digest[:16]}..."
+                )
+            assert is_fallback  # tier==1 implies fallback
+
+            degraded_fallback += 1
+            log(
+                f"  Degraded ledger {seq}: EntropyCount={entropy_count} "
+                f"FALLBACK"
+            )
+
+    log(f"3/5 entropy summary: {degraded_fallback} fallback")
+
+    # Log checks tied to current transition mechanics:
+    # - commit-set SHAMap publication is the observable output of entering the
+    #   commit sidecar phase
+    # - ConvergingCommit transition is the gateway out of seq=0-only behavior
+    # - reason=impossible-entropy-gate is the explicit degraded-window fallback path
+    ctx.log_level("LedgerConsensus", "trace")
+    ctx.log_level("ConsensusExtensions", "trace")
+    op = await ctx.sleep(6, name="stall_window")
+
+    ctx.assert_not_log(
+        r"RNG: transitioned to ConvergingCommit", within=op.window, nodes=[0, 1, 2]
+    )
+    ctx.assert_not_log(
+        r"RNG: built commitSet SHAMap", within=op.window, nodes=[0, 1, 2]
+    )
+
+    gate_blocked = ctx.search_logs(
+        r"STALLDIAG: establish gate blocked reason=(pause|no-tx-consensus)",
+        within=op.window,
+        nodes=[0, 1, 2],
+    )
+    log(f"3/5: establish gate-blocked logs in 6s: {gate_blocked.count}")
+
+    impossible = ctx.search_logs(
+        r"RNG: skipping commit wait reason=impossible-entropy-gate",
+        within=op.window,
+        nodes=[0, 1, 2],
+    )
+    log(f"3/5: RNG impossible-entropy-gate skips in 6s: {impossible.count}")
+
+    # --- Recovery: restart nodes, verify ledger advancement ---
+    ctx.start_node(3)
+    ctx.start_node(4)
+    await ctx.wait_for_ledgers(1, node_id=0, timeout=120)
+
+    val_recovered = ctx.validated_ledger_index(0)
+    pre_recovery = max(v for v in [val_before, val_after] if v is not None)
+    log(f"Recovered: validated seq {pre_recovery} → {val_recovered}")
+
+    if not val_recovered or val_recovered <= pre_recovery:
+        raise AssertionError(
+            f"Validated ledger did not advance after recovery "
+            f"({pre_recovery} → {val_recovered})"
+        )
+
+    # Inspect post-recovery ledgers separately from the degraded window above.
+    # Once the network is back at quorum, validator-tier entropy is expected
+    # again (transitional fallback ledgers are fine) and must be quorum-met.
+    fallback_count = 0
+    validator_count = 0
+    for seq in range(pre_recovery + 1, val_recovered + 1):
+        ce, _ = get_entropy_tx(ctx, seq)
+        digest, entropy_count, is_fallback = entropy_fields(ce)
+
+        if is_fallback:
+            fallback_count += 1
+        else:
+            validator_count += 1
+            if entropy_count < 4:
+                raise AssertionError(
+                    f"Ledger {seq}: validator entropy with sub-quorum "
+                    f"EntropyCount={entropy_count} (need >= 4)"
+                )
+
+        log(
+            f"  Ledger {seq}: EntropyCount={entropy_count} "
+            f"{'FALLBACK' if is_fallback else 'VALIDATOR'}"
+        )
+
+    log(
+        f"Entropy summary: {fallback_count} fallback, "
+        f"{validator_count} validator"
+    )
+
+    log("PASS")

.testnet/scenarios/entropy/quorum_recovery_smoke.py

@@ -0,0 +1,44 @@
+""":descr: drop 2 nodes (3/5 stall), restart both, verify recovery"""
+
+from __future__ import annotations
+
+from helpers import require_entropy
+
+
+async def scenario(ctx, log):
+    await require_entropy(ctx, log)
+
+    await ctx.wait_for_ledgers(1, node_id=0, timeout=60)
+    log("Baseline OK")
+
+    # Drop 2 nodes → validation stall.
+    ctx.stop_node(3)
+    ctx.stop_node(4)
+    await ctx.wait_for_nodes_down(nodes=[3, 4], timeout=30)
+
+    info = ctx.rpc.server_info(node_id=0)
+    val_before = info.get("info", {}).get("validated_ledger", {}).get("seq", 0)
+    log(f"Stalled at validated seq {val_before}")
+
+    # Let it sit for a few rounds in degraded state.
+    await ctx.sleep(6)
+
+    # Bring both nodes back.
+    ctx.start_node(3)
+    ctx.start_node(4)
+    log("Restarted n3 and n4, waiting for recovery...")
+
+    # Recovery: wait for ANY validated ledger advance on n0.
+    await ctx.wait_for_ledger_close(node_id=0, timeout=60)
+
+    info = ctx.rpc.server_info(node_id=0)
+    val_after = info.get("info", {}).get("validated_ledger", {}).get("seq", 0)
+    log(f"Recovered: validated seq {val_before} → {val_after}")
+
+    if val_after <= val_before:
+        raise AssertionError(
+            f"Validated ledger did not advance after recovery "
+            f"({val_before} → {val_after})"
+        )
+
+    log("PASS")

.testnet/scenarios/entropy/steady_state_entropy.py

@@ -0,0 +1,27 @@
+""":descr: all 5 nodes healthy, every ledger has valid unique quorum-met entropy"""
+
+from __future__ import annotations
+
+from helpers import require_entropy, get_entropy_tx, assert_valid_entropy
+
+
+async def scenario(ctx, log):
+    await require_entropy(ctx, log)
+
+    # Wait for RNG pipeline to warm up past bootstrap skip.
+    await ctx.wait_for_ledgers(3, node_id=0, timeout=60)
+    log("Pipeline warmed up")
+
+    start_seq = ctx.validated_ledger_index(0)
+    await ctx.wait_for_ledgers(10, node_id=0, timeout=120)
+    end_seq = ctx.validated_ledger_index(0)
+    log(f"Inspecting ledgers {start_seq + 1} → {end_seq}")
+
+    digests = set()
+    for seq in range(start_seq + 1, end_seq + 1):
+        ce, _ = get_entropy_tx(ctx, seq)
+        digest, count = assert_valid_entropy(ce, seq, seen_digests=digests)
+        log(f"  Ledger {seq}: EntropyCount={count} Digest={digest[:16]}...")
+
+    log(f"Verified {end_seq - start_seq} ledgers: all quorum entropy, all unique")
+    log("PASS")

.testnet/scenarios/export-suite.yml

@@ -0,0 +1,104 @@
+defaults:
+  network:
+    node_count: 5
+    launcher: tmux
+    find_ports: true
+    slave_delay: 0.2
+    features:
+      - ConsensusEntropy
+      - Export
+    track_features:
+      - ConsensusEntropy
+      - Export
+    unl_report: true
+    log_levels:
+      TxQ: info
+      Protocol: debug
+      Peer: debug
+      LedgerConsensus: debug
+      ConsensusExtensions: debug
+      NetworkOPs: info
+    env:
+      XAHAU_RESOURCE_PER_PORT: "1"
+    rc:
+      - rng_poll_ms=333
+
+tests:
+  # --- CE + Export (80% quorum, SHAMap convergence) ---
+  - name: steady_state_export_ce
+    script: .testnet/scenarios/export/steady_state_export.py
+
+  - name: retriable_export_ce
+    script: .testnet/scenarios/export/retriable_export.py
+
+  - name: export_degradation_ce
+    script: .testnet/scenarios/export/export_degradation.py
+    network:
+      rc:
+        - rng_poll_ms=333
+        - n3:no_export_sig=true
+        - n4:no_export_sig=true
+
+  - name: export_without_unl_report
+    script: .testnet/scenarios/export/export_without_unl_report.py
+    network:
+      features:
+        - Export
+      track_features:
+        - Export
+      unl_report: false
+
+  - name: export_no_veto_missing_observation
+    script: .testnet/scenarios/export/export_no_veto_missing_observation.py
+    network:
+      rc:
+        - rng_poll_ms=333
+        - n4:no_export_sig_hash=true
+
+  # CE + Export: 1 node suppressed, 4/5 = 80% quorum, should succeed
+  - name: export_ce_one_node_down
+    script: .testnet/scenarios/export/export_quorum.py
+    params:
+      expect_success: true
+    network:
+      rc:
+        - rng_poll_ms=333
+        - n4:no_export_sig=true
+
+  # --- Export only, no CE (80% active-view quorum) ---
+  - name: export_only_all_up
+    script: .testnet/scenarios/export/export_quorum.py
+    params:
+      expect_success: true
+    network:
+      features:
+        - Export
+      track_features:
+        - Export
+
+  - name: export_only_one_node_down
+    script: .testnet/scenarios/export/export_quorum.py
+    params:
+      expect_success: true
+    network:
+      features:
+        - Export
+      track_features:
+        - Export
+      rc:
+        - rng_poll_ms=333
+        - n4:no_export_sig=true
+
+  - name: export_only_two_nodes_down
+    script: .testnet/scenarios/export/export_quorum.py
+    params:
+      expect_success: false
+    network:
+      features:
+        - Export
+      track_features:
+        - Export
+      rc:
+        - rng_poll_ms=333
+        - n3:no_export_sig=true
+        - n4:no_export_sig=true

.testnet/scenarios/export/export_degradation.py

@@ -0,0 +1,123 @@
+""":descr: Submit ttEXPORT with 2 nodes suppressing export sigs, verify it
+retries via terRETRY_EXPORT until LLS expiry (insufficient signatures).
+
+Nodes 3 and 4 have runtime_config no_export_sig=true, so only 3/5 nodes
+provide export signatures. With 80% quorum = ceil(5*0.8) = 4 required,
+the export cannot reach quorum and should expire via tecEXPORT_EXPIRED.
+
+Flow:
+  1. Fund alice and bob
+  2. alice submits ttEXPORT with tight LLS
+  3. Export retries (only 3/5 sigs available, need 4)
+  4. Verify export expires with tecEXPORT_EXPIRED
+  5. Verify subsequent payment still works (sequence not permanently blocked)
+"""
+
+from __future__ import annotations
+
+from export_helpers import require_export, assert_shadow_ticket
+
+
+async def scenario(ctx, log):
+    await require_export(ctx, log)
+
+    # --- Setup ---
+    await ctx.fund_accounts({"alice": 10000, "bob": 1000})
+    log("Accounts funded")
+
+    alice = ctx.account("alice")
+    bob = ctx.account("bob")
+    current_seq = ctx.validated_ledger_index(0)
+
+    log(f"Current ledger: {current_seq}")
+    log("Nodes 3,4 have runtime_config no_export_sig=true (3/5 sigs, need 4)")
+
+    #@@start test-export-below-quorum-expiry
+    # --- Submit ttEXPORT (should retry then expire -- only 3/5 sigs) ---
+    export_start = ctx.mark("export-degradation-submit-start")
+    result = await ctx.submit_and_wait(
+        {
+            "TransactionType": "Export",
+            "LastLedgerSequence": current_seq + 8,
+            "Fee": "1000000",
+            "ExportedTxn": {
+                "TransactionType": "Payment",
+                "Account": alice.address,
+                "Destination": bob.address,
+                "Amount": "1000000",
+                "Fee": "10",
+                "Sequence": 0,
+                "TicketSequence": 1,
+                "FirstLedgerSequence": current_seq + 1,
+                "LastLedgerSequence": current_seq + 6,
+                "Flags": 2147483648,
+                "SigningPubKey": "",
+            },
+        },
+        alice.wallet,
+        timeout=60,
+    )
+    export_end = ctx.mark("export-degradation-submit-end")
+
+    final_seq = ctx.validated_ledger_index(0)
+    engine_result = result.get("engine_result", "")
+    log(f"Export completed at ledger {final_seq}, result: {engine_result}")
+
+    # With only 3/5 sigs and 80% quorum (4 required), export MUST fail
+    if engine_result == "tesSUCCESS":
+        raise AssertionError(
+            "Export should NOT have succeeded with only 3/5 sigs "
+            "(need 4 for 80% quorum) -- check runtime_config no_export_sig"
+        )
+
+    # Should be tecEXPORT_EXPIRED (LLS reached without quorum). Be exact here:
+    # any other non-success means the retry/expiry boundary regressed.
+    if engine_result != "tecEXPORT_EXPIRED":
+        raise AssertionError(
+            f"Expected tecEXPORT_EXPIRED below quorum, got {engine_result}"
+        )
+
+    log(f"Export failed as expected ({engine_result})")
+
+    retry_logs = ctx.assert_log(
+        r"Export: insufficient signatures .*result=terRETRY_EXPORT",
+        since=export_start,
+        until=export_end,
+    )
+    log(f"Export insufficient-signature retries: {retry_logs.count}")
+
+    expired_logs = ctx.assert_log(
+        r"Export: last ledger expired .*result=tecEXPORT_EXPIRED",
+        since=export_start,
+        until=export_end,
+    )
+    log(f"Export LLS expiry logs: {expired_logs.count}")
+
+    # No shadow ticket should exist (export never reached quorum)
+    assert_shadow_ticket(ctx, alice.address, log, expect_exists=False)
+    #@@end test-export-below-quorum-expiry
+
+    # --- Verify subsequent payment works regardless ---
+    log("Submitting payment from alice to bob...")
+    pay_result = await ctx.submit_and_wait(
+        {
+            "TransactionType": "Payment",
+            "Destination": bob.address,
+            "Amount": "1000000",
+            "Fee": "12",
+        },
+        alice.wallet,
+        timeout=30,
+    )
+
+    pay_engine = pay_result.get("engine_result", "")
+    log(f"Payment result: {pay_engine}")
+
+    if pay_engine != "tesSUCCESS":
+        raise AssertionError(
+            f"Payment failed after expired export: {pay_engine} "
+            f"-- sequence may be blocked"
+        )
+
+    log("Payment succeeded -- account not permanently blocked")
+    log("PASS")

.testnet/scenarios/export/export_helpers.py

@@ -0,0 +1,181 @@
+"""Shared helpers for Export scenario tests."""
+
+from __future__ import annotations
+
+from xahaud_scripts.testnet.config import _unl_report_index, feature_name_to_hash
+
+
+async def require_export(
+    ctx, log, *, require_unl_report=True, require_runtime_config=True
+):
+    """Wait for first ledger and assert Export is enabled.
+
+    Network-mode Export success requires a parent-ledger UNLReport-backed
+    active validator view. Most export scenarios seed that report in genesis;
+    assert it here so a success-path test cannot accidentally pass setup
+    without the condition Export::doApply requires. The no-UNLReport retry
+    scenario opts out deliberately.
+
+    The tracked export suite also uses XAHAUD_RUNTIME_TEST_CONFIG for polling
+    and fault-injection knobs. Default binaries reject the runtime_config RPC,
+    so check it up front rather than silently running without those knobs.
+    """
+    await ctx.wait_for_ledger_close(timeout=120)
+
+    if require_runtime_config:
+        result = ctx.rpc.runtime_config(0)
+        if not result or result.get("error"):
+            raise AssertionError(
+                "Export suite requires a binary built with "
+                "xahaud_runtime_test_config=ON; runtime_config RPC returned "
+                f"{result}"
+            )
+        log("RuntimeConfig RPC active")
+
+    feature = ctx.feature_check(feature_name_to_hash("Export"), node_id=0)
+    if not feature or not feature.get("enabled", False):
+        raise AssertionError(f"Export not enabled: {feature}")
+    log("Export enabled")
+
+    if require_unl_report:
+        result = ctx.rpc.ledger_entry(0, _unl_report_index())
+        node = (result or {}).get("node", {})
+        active = node.get("ActiveValidators", [])
+        if node.get("LedgerEntryType") != "UNLReport" or not active:
+            raise AssertionError(
+                "Export success scenario requires a ledger UNLReport with "
+                f"ActiveValidators, got: {result}"
+            )
+        log(f"UNLReport active validators: {len(active)}")
+
+
+def find_export_txns(ctx, seq):
+    """Find Export transactions in a ledger.
+
+    Returns list of Export transaction dicts.
+    """
+    result = ctx.ledger(seq, transactions=True)
+    if not result:
+        return []
+
+    txns = result.get("ledger", {}).get("transactions", [])
+    return [tx for tx in txns if tx.get("TransactionType") == "Export"]
+
+
+def dst_param(address):
+    """Encode an address as a HookParameter entry for the DST param."""
+    from xrpl.core.addresscodec import decode_classic_address
+
+    dst_hex = decode_classic_address(address).hex().upper()
+    return {
+        "HookParameter": {
+            "HookParameterName": "445354",  # "DST"
+            "HookParameterValue": dst_hex,
+        }
+    }
+
+
+def assert_hook_accepted(meta, log, *, expected_emits=1):
+    """Assert hook executed with ACCEPT and the expected emit count.
+
+    Checks sfHookExecutions in transaction metadata.
+    Returns the hook execution entry for further inspection.
+    """
+    hook_execs = meta.get("HookExecutions", [])
+    if not hook_execs:
+        raise AssertionError("No HookExecutions in metadata")
+
+    exec_entry = hook_execs[0].get("HookExecution", {})
+    hook_result = exec_entry.get("HookResult", -1)
+    emit_count = exec_entry.get("HookEmitCount", -1)
+    return_code = exec_entry.get("HookReturnCode", "")
+
+    log(f"  HookResult={hook_result} EmitCount={emit_count} ReturnCode={return_code}")
+
+    # HookResult 3 = ExitType::ACCEPT
+    if hook_result != 3:
+        raise AssertionError(
+            f"Hook did not ACCEPT: HookResult={hook_result} "
+            f"ReturnCode={return_code}"
+        )
+
+    if emit_count != expected_emits:
+        raise AssertionError(
+            f"Expected {expected_emits} emits, got {emit_count}"
+        )
+
+    # ReturnCode 0 = success; non-zero = ASSERT line number in hook
+    if return_code and str(return_code) != "0":
+        raise AssertionError(
+            f"Hook returned error code {return_code} "
+            f"(likely ASSERT failure at that line)"
+        )
+
+    return exec_entry
+
+
+def assert_export_result(meta, log, *, require_signers=True):
+    """Assert ExportResult is present and well-formed in metadata.
+
+    Returns the ExportResult dict.
+    """
+    export_result = meta.get("ExportResult", {})
+    if not export_result:
+        raise AssertionError("ExportResult not found in metadata")
+
+    # Must have LedgerSequence and TransactionHash
+    if "LedgerSequence" not in export_result:
+        raise AssertionError("ExportResult missing LedgerSequence")
+    if "TransactionHash" not in export_result:
+        raise AssertionError("ExportResult missing TransactionHash")
+
+    # Must have the inner ExportedTxn object
+    inner = export_result.get("ExportedTxn", {})
+    if not inner:
+        raise AssertionError("ExportResult missing ExportedTxn (multisigned blob)")
+
+    log(f"  ExportResult: seq={export_result['LedgerSequence']} "
+        f"hash={export_result['TransactionHash'][:16]}...")
+
+    # Inner tx should have Account, Destination, TransactionType
+    if "Account" not in inner:
+        raise AssertionError("ExportedTxn missing Account")
+    if "TransactionType" not in inner:
+        raise AssertionError("ExportedTxn missing TransactionType")
+
+    # Should have empty SigningPubKey (multisigned)
+    if inner.get("SigningPubKey", "NOT_EMPTY") != "":
+        raise AssertionError(
+            f"ExportedTxn SigningPubKey should be empty, "
+            f"got '{inner.get('SigningPubKey')}'"
+        )
+
+    if require_signers:
+        signers = inner.get("Signers", [])
+        if not signers:
+            raise AssertionError("ExportedTxn has no Signers (multisig not applied)")
+        log(f"  Signers: {len(signers)} validator(s)")
+
+    return export_result
+
+
+def assert_shadow_ticket(ctx, account_address, log, *, expect_exists=True):
+    """Assert shadow ticket exists (or doesn't) for the account."""
+    obj_result = ctx.rpc.request(
+        0, "account_objects", {"account": account_address}
+    )
+    all_objects = (obj_result or {}).get("account_objects", [])
+    shadow_tickets = [
+        obj for obj in all_objects
+        if obj.get("LedgerEntryType") == "ShadowTicket"
+    ]
+    log(f"  Shadow tickets: {len(shadow_tickets)}")
+
+    if expect_exists and not shadow_tickets:
+        raise AssertionError("Expected shadow ticket but none found")
+    if not expect_exists and shadow_tickets:
+        raise AssertionError(
+            f"Expected no shadow tickets but found {len(shadow_tickets)}"
+        )
+
+    return shadow_tickets

.testnet/scenarios/export/export_no_veto_missing_observation.py

@@ -0,0 +1,87 @@
+""":descr: Export succeeds when quorum sidecar material exists but one active
+validator withholds exportSigSetHash observation.
+
+Node 4 has runtime_config no_export_sig_hash=true. It still attaches export
+signatures, but it does not publish its exportSigSetHash in proposals. The
+remaining 4/5 active validators can still align on the same export sidecar
+hash, so the round must not retry/expire just because fullObservation is false.
+"""
+
+from __future__ import annotations
+
+from export_helpers import (
+    require_export,
+    assert_export_result,
+    assert_shadow_ticket,
+)
+
+
+async def scenario(ctx, log):
+    await require_export(ctx, log)
+
+    await ctx.fund_accounts({"alice": 10000, "bob": 1000})
+    log("Accounts funded")
+
+    alice = ctx.account("alice")
+    bob = ctx.account("bob")
+    current_seq = ctx.validated_ledger_index(0)
+
+    log(f"Current ledger: {current_seq}")
+    log("Node 4 withholds exportSigSetHash but still attaches export signatures")
+
+    export_start = ctx.mark("export-no-veto-submit-start")
+    result = await ctx.submit_and_wait(
+        {
+            "TransactionType": "Export",
+            "LastLedgerSequence": current_seq + 10,
+            "Fee": "1000000",
+            "ExportedTxn": {
+                "TransactionType": "Payment",
+                "Account": alice.address,
+                "Destination": bob.address,
+                "Amount": "1000000",
+                "Fee": "10",
+                "Sequence": 0,
+                "TicketSequence": 1,
+                "FirstLedgerSequence": current_seq + 1,
+                "LastLedgerSequence": current_seq + 8,
+                "Flags": 2147483648,
+                "SigningPubKey": "",
+            },
+        },
+        alice.wallet,
+        timeout=60,
+    )
+    export_end = ctx.mark("export-no-veto-submit-end")
+
+    final_seq = ctx.validated_ledger_index(0)
+    engine_result = result.get("engine_result", "")
+    meta = result.get("meta", {})
+
+    log(f"Export completed at ledger {final_seq}, result: {engine_result}")
+    if engine_result != "tesSUCCESS":
+        raise AssertionError(f"Expected tesSUCCESS, got {engine_result}")
+
+    export_result = assert_export_result(meta, log, require_signers=True)
+    signers = export_result.get("ExportedTxn", {}).get("Signers", [])
+    if len(signers) < 4:
+        raise AssertionError(f"Expected at least 4 signers, got {len(signers)}")
+    log(f"Export signer count: {len(signers)}")
+
+    no_veto_logs = ctx.assert_log(
+        r"Export: missing exportSigSetHash observation ignored",
+        since=export_start,
+        until=export_end,
+    )
+    log(f"Export no-veto missing-observation logs: {no_veto_logs.count}")
+
+    withhold_logs = ctx.assert_log(
+        r"Export: withholding exportSigSetHash",
+        since=export_start,
+        until=export_end,
+    )
+    log(f"Export sidecar hash withholding logs: {withhold_logs.count}")
+
+    assert_shadow_ticket(ctx, alice.address, log, expect_exists=True)
+
+    log("PASS")

.testnet/scenarios/export/export_quorum.py

@@ -0,0 +1,117 @@
+""":descr: Test Export quorum behavior. When enough active validators sign,
+the export should succeed whether or not CE is enabled. When fewer than the
+active-view quorum sign, the export should expire.
+
+Parameterized via `expect_success` kwarg from suite.yml.
+
+Flow:
+  1. Fund alice and bob
+  2. alice submits ttEXPORT
+  3. Verify result matches expectation (tesSUCCESS or tecEXPORT_EXPIRED)
+  4. Verify ExportResult + shadow ticket on success, absence on failure
+  5. Verify subsequent payment works regardless
+"""
+
+from __future__ import annotations
+
+from export_helpers import (
+    require_export,
+    assert_export_result,
+    assert_shadow_ticket,
+)
+
+
+async def scenario(ctx, log, expect_success=True):
+    await require_export(ctx, log)
+
+    # --- Setup ---
+    await ctx.fund_accounts({"alice": 10000, "bob": 1000})
+    log("Accounts funded")
+
+    alice = ctx.account("alice")
+    bob = ctx.account("bob")
+    current_seq = ctx.validated_ledger_index(0)
+
+    log(f"Current ledger: {current_seq}")
+    outcome = "success" if expect_success else "failure (below quorum)"
+    log(f"Expecting export {outcome}")
+
+    # --- Submit ttEXPORT ---
+    result = await ctx.submit_and_wait(
+        {
+            "TransactionType": "Export",
+            "LastLedgerSequence": current_seq + 10,
+            "Fee": "1000000",
+            "ExportedTxn": {
+                "TransactionType": "Payment",
+                "Account": alice.address,
+                "Destination": bob.address,
+                "Amount": "1000000",
+                "Fee": "10",
+                "Sequence": 0,
+                "TicketSequence": 1,
+                "FirstLedgerSequence": current_seq + 1,
+                "LastLedgerSequence": current_seq + 8,
+                "Flags": 2147483648,
+                "SigningPubKey": "",
+            },
+        },
+        alice.wallet,
+        timeout=60,
+    )
+
+    final_seq = ctx.validated_ledger_index(0)
+    engine_result = result.get("engine_result", "")
+    meta = result.get("meta", {})
+
+    log(f"Export at ledger {final_seq}, result: {engine_result}")
+
+    if expect_success:
+        if engine_result != "tesSUCCESS":
+            raise AssertionError(
+                f"Expected tesSUCCESS, got {engine_result}"
+            )
+
+        # Assert ExportResult is well-formed with signers
+        assert_export_result(meta, log, require_signers=True)
+
+        # Assert shadow ticket was created
+        assert_shadow_ticket(ctx, alice.address, log, expect_exists=True)
+
+        log("Export succeeded as expected (active-view quorum reached)")
+    else:
+        if engine_result == "tesSUCCESS":
+            raise AssertionError(
+                "Export should NOT have succeeded below active-view quorum"
+            )
+        if engine_result != "tecEXPORT_EXPIRED":
+            raise AssertionError(
+                "Expected tecEXPORT_EXPIRED below active-view quorum, "
+                f"got {engine_result}"
+            )
+        log(f"Export failed as expected ({engine_result})")
+
+        # No shadow ticket should exist
+        assert_shadow_ticket(ctx, alice.address, log, expect_exists=False)
+
+    # --- Verify subsequent payment works ---
+    log("Submitting payment from alice to bob...")
+    pay_result = await ctx.submit_and_wait(
+        {
+            "TransactionType": "Payment",
+            "Destination": bob.address,
+            "Amount": "1000000",
+            "Fee": "12",
+        },
+        alice.wallet,
+        timeout=30,
+    )
+
+    pay_engine = pay_result.get("engine_result", "")
+    log(f"Payment result: {pay_engine}")
+
+    if pay_engine != "tesSUCCESS":
+        raise AssertionError(f"Payment failed: {pay_engine}")
+
+    log("Payment succeeded -- account not blocked")
+    log("PASS")

.testnet/scenarios/export/export_without_unl_report.py

@@ -0,0 +1,92 @@
+""":descr: Export retries/expires without a ledger-anchored UNLReport view.
+
+All validators may sign, but network-mode Export must not assemble quorum
+material from a node-local trusted-config view. Without UNLReport, the export
+should retry until LastLedgerSequence and expire without creating a shadow
+ticket.
+"""
+
+from __future__ import annotations
+
+from export_helpers import require_export, assert_shadow_ticket
+
+
+async def scenario(ctx, log):
+    await require_export(ctx, log, require_unl_report=False)
+
+    await ctx.fund_accounts({"alice": 10000, "bob": 1000})
+    log("Accounts funded")
+
+    alice = ctx.account("alice")
+    bob = ctx.account("bob")
+    current_seq = ctx.validated_ledger_index(0)
+
+    log(f"Current ledger: {current_seq}")
+    log("UNLReport intentionally absent; export must not use local config view")
+
+    export_start = ctx.mark("export-without-unlreport-submit-start")
+    result = await ctx.submit_and_wait(
+        {
+            "TransactionType": "Export",
+            "LastLedgerSequence": current_seq + 8,
+            "Fee": "1000000",
+            "ExportedTxn": {
+                "TransactionType": "Payment",
+                "Account": alice.address,
+                "Destination": bob.address,
+                "Amount": "1000000",
+                "Fee": "10",
+                "Sequence": 0,
+                "TicketSequence": 1,
+                "FirstLedgerSequence": current_seq + 1,
+                "LastLedgerSequence": current_seq + 6,
+                "Flags": 2147483648,
+                "SigningPubKey": "",
+            },
+        },
+        alice.wallet,
+        timeout=60,
+    )
+    export_end = ctx.mark("export-without-unlreport-submit-end")
+
+    final_seq = ctx.validated_ledger_index(0)
+    engine_result = result.get("engine_result", "")
+    log(f"Export completed at ledger {final_seq}, result: {engine_result}")
+
+    if engine_result == "tesSUCCESS":
+        raise AssertionError(
+            "Export should not succeed without a ledger-anchored UNLReport view"
+        )
+
+    # Be exact: without a UNLReport view the export should retry until LLS and
+    # expire, not fail by some unrelated terminal code.
+    if engine_result != "tecEXPORT_EXPIRED":
+        raise AssertionError(
+            "Expected tecEXPORT_EXPIRED without UNLReport view, "
+            f"got {engine_result}"
+        )
+
+    warning_logs = ctx.assert_log(
+        r"Export: retrying without ledger-anchored validator view",
+        since=export_start,
+        until=export_end,
+    )
+    log(f"Export no-UNLReport retry warnings: {warning_logs.count}")
+
+    retry_logs = ctx.assert_log(
+        r"Export: insufficient signatures .*result=terRETRY_EXPORT",
+        since=export_start,
+        until=export_end,
+    )
+    log(f"Export retry logs: {retry_logs.count}")
+
+    expired_logs = ctx.assert_log(
+        r"Export: last ledger expired .*result=tecEXPORT_EXPIRED",
+        since=export_start,
+        until=export_end,
+    )
+    log(f"Export expiry logs: {expired_logs.count}")
+
+    assert_shadow_ticket(ctx, alice.address, log, expect_exists=False)
+
+    log("PASS")

.testnet/scenarios/export/retriable_export.py

@@ -0,0 +1,94 @@
+""":descr: Submit ttEXPORT directly (no hook), verify it succeeds with
+ExportResult in metadata. Then submit a payment from the same account
+to verify sequence handling doesn't block subsequent transactions.
+
+Flow:
+  1. Fund alice and bob
+  2. alice submits ttEXPORT with inner payment -> tesSUCCESS (provisional)
+  3. Validators attach sigs via proposals -> quorum -> ExportResult in metadata
+  4. alice submits a Payment to bob -> should succeed (sequence not blocked)
+"""
+
+from __future__ import annotations
+
+from export_helpers import require_export, assert_export_result, assert_shadow_ticket
+
+
+async def scenario(ctx, log):
+    await require_export(ctx, log)
+
+    # --- Setup ---
+    await ctx.fund_accounts({"alice": 10000, "bob": 1000})
+    log("Accounts funded")
+
+    alice = ctx.account("alice")
+    bob = ctx.account("bob")
+    current_seq = ctx.validated_ledger_index(0)
+
+    log(f"Current ledger: {current_seq}")
+
+    # --- 1. Submit ttEXPORT ---
+    result = await ctx.submit_and_wait(
+        {
+            "TransactionType": "Export",
+            "LastLedgerSequence": current_seq + 15,
+            "Fee": "1000000",
+            "ExportedTxn": {
+                "TransactionType": "Payment",
+                "Account": alice.address,
+                "Destination": bob.address,
+                "Amount": "1000000",
+                "Fee": "10",
+                "Sequence": 0,
+                "TicketSequence": 1,
+                "FirstLedgerSequence": current_seq + 1,
+                "LastLedgerSequence": current_seq + 10,
+                "Flags": 2147483648,
+                "SigningPubKey": "",
+            },
+        },
+        alice.wallet,
+        timeout=60,
+    )
+
+    export_seq = ctx.validated_ledger_index(0)
+    engine_result = result.get("engine_result", "")
+    log(f"Export completed at ledger {export_seq}, result: {engine_result}")
+
+    if engine_result != "tesSUCCESS":
+        raise AssertionError(
+            f"Expected tesSUCCESS for export, got {engine_result}"
+        )
+
+    # Assert ExportResult is well-formed with signers
+    meta = result.get("meta", {})
+    assert_export_result(meta, log, require_signers=True)
+
+    # Assert shadow ticket was created
+    assert_shadow_ticket(ctx, alice.address, log, expect_exists=True)
+
+    # --- 2. Submit Payment from same account ---
+    log("Submitting payment from alice to bob...")
+    pay_result = await ctx.submit_and_wait(
+        {
+            "TransactionType": "Payment",
+            "Destination": bob.address,
+            "Amount": "1000000",
+            "Fee": "12",
+        },
+        alice.wallet,
+        timeout=30,
+    )
+
+    pay_engine = pay_result.get("engine_result", "")
+    log(f"Payment result: {pay_engine}")
+
+    if pay_engine != "tesSUCCESS":
+        raise AssertionError(f"Payment failed: {pay_engine}")
+
+    log(
+        f"Both transactions succeeded: "
+        f"Export at ledger {export_seq}, Payment at ledger {ctx.validated_ledger_index(0)}"
+    )
+    log("Sequence handling OK - export didn't block subsequent txns")
+    log("PASS")

.testnet/scenarios/export/steady_state_export.py

@@ -0,0 +1,211 @@
+""":descr: install xport hook, trigger export, verify emitted ttEXPORT lifecycle
+
+  1. Fund alice (hook holder), bob (trigger), carol (export destination)
+  2. Install xport hook on alice
+  3. bob pays alice with DST=carol → hook calls xport() → emits ttEXPORT
+  4. Emitted ttEXPORT enters open ledger, validators attach sigs via proposals
+  5. Verify Export transaction appears in a subsequent ledger
+"""
+
+from __future__ import annotations
+
+from export_helpers import (
+    require_export,
+    find_export_txns,
+    dst_param,
+    assert_hook_accepted,
+    assert_export_result,
+    assert_shadow_ticket,
+)
+
+# C source for the xport hook — verbatim from src/test/app/Export_test_hooks.h
+# On Payment to the hook account, exports a 1 XAH payment to the DST param.
+XPORT_HOOK_C = r"""
+#include <stdint.h>
+extern int32_t _g(uint32_t id, uint32_t maxiter);
+extern int64_t accept(uint32_t read_ptr, uint32_t read_len, int64_t error_code);
+extern int64_t rollback(uint32_t read_ptr, uint32_t read_len, int64_t error_code);
+extern int64_t xport(uint32_t write_ptr, uint32_t write_len, uint32_t read_ptr, uint32_t read_len);
+extern int64_t xport_reserve(uint32_t count);
+extern int64_t hook_account(uint32_t write_ptr, uint32_t write_len);
+extern int64_t otxn_param(uint32_t write_ptr, uint32_t write_len, uint32_t name_ptr, uint32_t name_len);
+extern int64_t otxn_type(void);
+extern int64_t ledger_seq(void);
+
+#define SBUF(x) (uint32_t)(x), sizeof(x)
+#define ASSERT(x) if (!(x)) rollback((uint32_t)#x, sizeof(#x), __LINE__)
+
+#define ttPAYMENT 0
+#define tfCANONICAL 0x80000000UL
+#define amAMOUNT 1
+#define amFEE 8
+#define atACCOUNT 1
+#define atDESTINATION 3
+
+#define ENCODE_TT(buf_out, tt) \
+    buf_out[0] = 0x12U; buf_out[1] = (tt >> 8) & 0xFFU; buf_out[2] = tt & 0xFFU; buf_out += 3;
+
+#define ENCODE_FLAGS(buf_out, flags) \
+    buf_out[0] = 0x22U; buf_out[1] = (flags >> 24) & 0xFFU; buf_out[2] = (flags >> 16) & 0xFFU; \
+    buf_out[3] = (flags >> 8) & 0xFFU; buf_out[4] = flags & 0xFFU; buf_out += 5;
+
+#define ENCODE_SEQUENCE(buf_out, seq) \
+    buf_out[0] = 0x24U; buf_out[1] = (seq >> 24) & 0xFFU; buf_out[2] = (seq >> 16) & 0xFFU; \
+    buf_out[3] = (seq >> 8) & 0xFFU; buf_out[4] = seq & 0xFFU; buf_out += 5;
+
+#define ENCODE_FLS(buf_out, fls) \
+    buf_out[0] = 0x20U; buf_out[1] = 0x1AU; buf_out[2] = (fls >> 24) & 0xFFU; \
+    buf_out[3] = (fls >> 16) & 0xFFU; buf_out[4] = (fls >> 8) & 0xFFU; \
+    buf_out[5] = fls & 0xFFU; buf_out += 6;
+
+#define ENCODE_LLS(buf_out, lls) \
+    buf_out[0] = 0x20U; buf_out[1] = 0x1BU; buf_out[2] = (lls >> 24) & 0xFFU; \
+    buf_out[3] = (lls >> 16) & 0xFFU; buf_out[4] = (lls >> 8) & 0xFFU; \
+    buf_out[5] = lls & 0xFFU; buf_out += 6;
+
+#define ENCODE_DROPS(buf_out, drops, amt_type) \
+    buf_out[0] = 0x60U + amt_type; buf_out[1] = 0x40U + ((drops >> 56) & 0x3FU); \
+    buf_out[2] = (drops >> 48) & 0xFFU; buf_out[3] = (drops >> 40) & 0xFFU; \
+    buf_out[4] = (drops >> 32) & 0xFFU; buf_out[5] = (drops >> 24) & 0xFFU; \
+    buf_out[6] = (drops >> 16) & 0xFFU; buf_out[7] = (drops >> 8) & 0xFFU; \
+    buf_out[8] = drops & 0xFFU; buf_out += 9;
+
+#define ENCODE_SIGNING_PUBKEY_EMPTY(buf_out) \
+    buf_out[0] = 0x73U; buf_out[1] = 0x00U; buf_out += 2;
+
+#define ENCODE_ACCOUNT(buf_out, acc, acc_type) \
+    buf_out[0] = 0x80U + acc_type; buf_out[1] = 0x14U; \
+    for (int i = 0; i < 20; ++i) buf_out[2+i] = acc[i]; buf_out += 22;
+
+#define PREPARE_PAYMENT_SIMPLE_SIZE 270U
+
+int64_t hook(uint32_t reserved) {
+    _g(1, 1);
+
+    if (otxn_type() != ttPAYMENT)
+        return accept(0, 0, 0);
+
+    ASSERT(xport_reserve(1) == 1);
+
+    uint8_t dst[20];
+    int64_t dst_len = otxn_param(SBUF(dst), "DST", 3);
+    ASSERT(dst_len == 20);
+
+    uint8_t acc[20];
+    ASSERT(hook_account(SBUF(acc)) == 20);
+
+    uint32_t cls = (uint32_t)ledger_seq();
+
+    uint8_t tx[PREPARE_PAYMENT_SIMPLE_SIZE];
+    uint8_t* buf = tx;
+
+    ENCODE_TT(buf, ttPAYMENT);
+    ENCODE_FLAGS(buf, tfCANONICAL);
+    ENCODE_SEQUENCE(buf, 0);
+    ENCODE_FLS(buf, cls + 1);
+    ENCODE_LLS(buf, cls + 5);
+    // sfTicketSequence = UINT32 field 41 = 0x20 0x29
+    buf[0] = 0x20U; buf[1] = 0x29U;
+    buf[2] = 0; buf[3] = 0; buf[4] = 0; buf[5] = 1;
+    buf += 6;
+
+    uint64_t drops = 1000000;
+    ENCODE_DROPS(buf, drops, amAMOUNT);
+    ENCODE_DROPS(buf, 10, amFEE);
+
+    ENCODE_SIGNING_PUBKEY_EMPTY(buf);
+    ENCODE_ACCOUNT(buf, acc, atACCOUNT);
+    ENCODE_ACCOUNT(buf, dst, atDESTINATION);
+
+    uint8_t hash[32];
+    int64_t xport_result = xport(SBUF(hash), (uint32_t)tx, buf - tx);
+    ASSERT(xport_result == 32);
+
+    return accept(0, 0, 0);
+}
+"""
+
+
+async def scenario(ctx, log):
+    # Wait for network to start and amendments to activate
+    await require_export(ctx, log)
+
+    # --- Setup ---
+    await ctx.fund_accounts({"alice": 10000, "bob": 10000, "carol": 1000})
+    log("Accounts funded")
+
+    alice = ctx.account("alice")
+    carol = ctx.account("carol")
+
+    # Compile and install xport hook on alice
+    wasm = ctx.compile_hook(XPORT_HOOK_C, label="xport")
+    await ctx.submit_and_wait(
+        {
+            "TransactionType": "SetHook",
+            "Hooks": [
+                {
+                    "Hook": {
+                        "CreateCode": wasm.hex().upper(),
+                        "HookOn": "0" * 64,
+                        "HookNamespace": "0" * 64,
+                        "HookApiVersion": 0,
+                        "Flags": 1,  # hsfOVERRIDE
+                    }
+                }
+            ],
+            "Fee": "100000000",
+        },
+        alice.wallet,
+    )
+    log(
+        f"Hook installed on alice ({alice.address[:12]}...) "
+        f"ledger {ctx.validated_ledger_index(0)}"
+    )
+
+    # --- Trigger ---
+    # bob pays alice → hook calls xport() → emits ttEXPORT
+    trigger_result = await ctx.submit_and_wait(
+        {
+            "TransactionType": "Payment",
+            "Destination": alice.address,
+            "Amount": "100000000",
+            "Fee": "1000000",
+            "HookParameters": [dst_param(carol.address)],
+        },
+        ctx.account("bob").wallet,
+    )
+    trigger_seq = ctx.validated_ledger_index(0)
+    log(f"Export triggered at ledger {trigger_seq}")
+
+    # Assert hook fired with ACCEPT and emitted 1 tx
+    trigger_meta = trigger_result.get("meta", {})
+    assert_hook_accepted(trigger_meta, log, expected_emits=1)
+
+    # --- Verify: check each ledger close for the Export transaction ---
+    max_ledgers = 10
+    for i in range(max_ledgers):
+        await ctx.wait_for_ledgers(1, node_id=0, timeout=30)
+        seq = ctx.validated_ledger_index(0)
+        exports = find_export_txns(ctx, seq)
+        if exports:
+            export_tx = exports[0]
+            meta = export_tx.get("meta", export_tx.get("metaData", {}))
+            result = meta.get("TransactionResult", "")
+            log(f"Ledger {seq}: Export txn found, result={result}")
+
+            if result != "tesSUCCESS":
+                raise AssertionError(f"Export did not succeed: {result}")
+
+            # Assert ExportResult is well-formed with signers and inner tx
+            assert_export_result(meta, log, require_signers=True)
+
+            # Assert shadow ticket was created
+            assert_shadow_ticket(ctx, alice.address, log, expect_exists=True)
+
+            log("PASS")
+            return
+        log(f"Ledger {seq}: no Export txn yet")
+
+    raise AssertionError(
+        f"No Export transaction found after {max_ledgers} ledger closes"
+    )

.testnet/scenarios/helpers.py

@@ -0,0 +1,180 @@
+"""Shared helpers for ConsensusEntropy scenario tests."""
+
+from __future__ import annotations
+
+from xahaud_scripts.testnet.config import feature_name_to_hash
+
+ZERO_DIGEST = "0" * 64
+CONSENSUS_ENTROPY_FEATURE = feature_name_to_hash("ConsensusEntropy")
+
+
+def feature_hash(name: str) -> str:
+    """Return the amendment hash accepted by feature RPC."""
+    return feature_name_to_hash(name)
+
+
+def feature_status(ctx, name: str, node_id=0):
+    """Query a feature by amendment hash; feature RPC names are ambiguous."""
+    return ctx.feature_check(feature_hash(name), node_id=node_id)
+
+
+def consensus_entropy_feature(ctx, node_id=0):
+    """Query ConsensusEntropy by amendment hash."""
+    return feature_status(ctx, "ConsensusEntropy", node_id=node_id)
+
+
+async def require_entropy(ctx, log):
+    """Wait for first ledger and assert ConsensusEntropy is enabled."""
+    await ctx.wait_for_ledger_close(timeout=120)
+    feature = consensus_entropy_feature(ctx, node_id=0)
+    if not feature or not feature.get("enabled", False):
+        raise AssertionError(f"ConsensusEntropy not enabled: {feature}")
+    log("ConsensusEntropy enabled")
+
+
+def get_entropy_tx(ctx, seq):
+    """Fetch ledger and return (ce_tx, user_txns) or raise."""
+    result = ctx.ledger(seq, transactions=True)
+    if not result:
+        raise AssertionError(f"Ledger {seq}: fetch failed")
+
+    ledger = result.get("ledger")
+    if not isinstance(ledger, dict):
+        raise AssertionError(f"Ledger {seq}: fetch returned no ledger: {result}")
+
+    txns = ledger.get("transactions", [])
+    ce = [tx for tx in txns if tx.get("TransactionType") == "ConsensusEntropy"]
+    user = [tx for tx in txns if tx.get("TransactionType") != "ConsensusEntropy"]
+
+    if len(ce) != 1:
+        raise AssertionError(
+            f"Ledger {seq}: expected 1 ConsensusEntropy txn, got {len(ce)}"
+        )
+
+    return ce[0], user
+
+
+def entropy_fields(ce_tx):
+    """Return (digest, entropy_count, is_fallback) from a ConsensusEntropy tx.
+
+    consensus_fallback rounds carry a deterministic non-zero consensus-bound
+    digest with EntropyCount=0 and EntropyTier=1 (consensus_fallback).
+    Validator entropy has EntropyTier=3 (validator_quorum).
+
+    WARNING: is_fallback is ``tier != 3``, so it lumps participant_aligned
+    (Tier 2) in with fallback. It is only safe where no Tier 2 band exists
+    (e.g. 5-node networks, where tier2 == quorum). For band-aware scenarios use
+    the explicit assert_consensus_fallback / assert_participant_aligned /
+    assert_validator_quorum helpers, which check EntropyTier directly.
+    """
+    digest = ce_tx.get("Digest", "")
+    entropy_count = ce_tx.get("EntropyCount", -1)
+    tier = ce_tx.get("EntropyTier", None)
+    if tier is not None:
+        is_fallback = tier != 3
+    else:
+        is_fallback = entropy_count == 0
+    return digest, entropy_count, is_fallback
+
+
+def assert_participant_aligned(ce_tx, seq, expected_count=None):
+    """Assert participant_aligned (Tier 2) entropy on a ConsensusEntropy tx.
+
+    Tier 2 is the sub-quorum band: the agreed reveal cohort is >= the
+    participant floor but < the 80% validator quorum, so it carries
+    EntropyTier=2 with a deterministic non-zero digest. NOTE entropy_fields()'s
+    is_fallback lumps tier 2 in with fallback (is_fallback = tier != 3), so the
+    tier must be checked EXPLICITLY here.
+    """
+    digest = ce_tx.get("Digest", "")
+    count = ce_tx.get("EntropyCount", -1)
+    tier = ce_tx.get("EntropyTier", None)
+    if tier != 2:
+        raise AssertionError(
+            f"Ledger {seq}: expected EntropyTier==2 (participant_aligned), "
+            f"got {tier} (EntropyCount={count})"
+        )
+    if not digest or digest == ZERO_DIGEST:
+        raise AssertionError(
+            f"Ledger {seq}: participant_aligned digest must be non-zero, got "
+            f"{digest[:16]}..."
+        )
+    if expected_count is not None and count != expected_count:
+        raise AssertionError(
+            f"Ledger {seq}: participant_aligned EntropyCount must be "
+            f"{expected_count} (the surviving cohort), got {count}"
+        )
+    return digest, count
+
+
+def assert_validator_quorum(ce_tx, seq, min_count=None):
+    """Assert validator_quorum (Tier 3) entropy on a ConsensusEntropy tx:
+    EntropyTier=3, a deterministic non-zero digest, and (optionally)
+    EntropyCount >= min_count (the active quorum). The count can EXCEED the
+    quorum (e.g. a still-full 6/6 ledger caught at a 6->5 transition), so check
+    >=, not ==.
+    """
+    digest = ce_tx.get("Digest", "")
+    count = ce_tx.get("EntropyCount", -1)
+    tier = ce_tx.get("EntropyTier", None)
+    if tier != 3:
+        raise AssertionError(
+            f"Ledger {seq}: expected EntropyTier==3 (validator_quorum), got "
+            f"{tier} (EntropyCount={count})"
+        )
+    if not digest or digest == ZERO_DIGEST:
+        raise AssertionError(
+            f"Ledger {seq}: validator_quorum digest must be non-zero, got "
+            f"{digest[:16]}..."
+        )
+    if min_count is not None and count < min_count:
+        raise AssertionError(
+            f"Ledger {seq}: validator_quorum EntropyCount={count} < quorum "
+            f"{min_count}"
+        )
+    return digest, count
+
+
+def assert_consensus_fallback(ce_tx, seq):
+    """Assert consensus_fallback (Tier 1) entropy on a ConsensusEntropy tx:
+    EntropyTier=1, EntropyCount=0, and a deterministic NON-zero digest.
+    """
+    digest = ce_tx.get("Digest", "")
+    count = ce_tx.get("EntropyCount", -1)
+    tier = ce_tx.get("EntropyTier", None)
+    if tier != 1:
+        raise AssertionError(
+            f"Ledger {seq}: expected EntropyTier==1 (consensus_fallback), got "
+            f"{tier} (EntropyCount={count})"
+        )
+    if count != 0:
+        raise AssertionError(
+            f"Ledger {seq}: consensus_fallback EntropyCount must be 0, got "
+            f"{count}"
+        )
+    if not digest or digest == ZERO_DIGEST:
+        raise AssertionError(
+            f"Ledger {seq}: consensus_fallback digest must be non-zero, got "
+            f"{digest[:16]}..."
+        )
+    return digest, count
+
+
+def assert_valid_entropy(ce_tx, seq, seen_digests=None):
+    """Assert quorum-met validator entropy. Optionally check uniqueness."""
+    digest, entropy_count, is_fallback = entropy_fields(ce_tx)
+
+    if is_fallback or not digest or digest == ZERO_DIGEST:
+        raise AssertionError(f"Ledger {seq}: fallback/empty Digest")
+
+    if entropy_count < 4:
+        raise AssertionError(
+            f"Ledger {seq}: EntropyCount={entropy_count} < 4 (sub-quorum)"
+        )
+
+    if seen_digests is not None:
+        if digest in seen_digests:
+            raise AssertionError(f"Ledger {seq}: duplicate Digest {digest[:16]}...")
+        seen_digests.add(digest)
+
+    return digest, entropy_count

.testnet/scenarios/latency-suite.yml

@@ -0,0 +1,92 @@
+defaults:
+  network:
+    node_count: 5
+    launcher: tmux
+    find_ports: true
+    slave_delay: 0.2
+    features:
+      - ConsensusEntropy
+      - Export
+    track_features:
+      - ConsensusEntropy
+      - Export
+    unl_report: true
+    log_levels:
+      TxQ: info
+      Protocol: debug
+      Peer: debug
+      LedgerConsensus: debug
+      ConsensusExtensions: debug
+      NetworkOPs: info
+    env:
+      XAHAU_RESOURCE_PER_PORT: "1"
+    rc:
+      - rng_poll_ms=250
+tests:
+  - name: latency_baseline_ce
+    script: .testnet/scenarios/perf/ce_export_latency_probe.py
+    params:
+      warmup_ledgers: 3
+      ledgers: 8
+      submit_export: false
+
+  - name: latency_baseline_export
+    script: .testnet/scenarios/perf/ce_export_latency_probe.py
+    params:
+      warmup_ledgers: 3
+      ledgers: 8
+      submit_export: true
+
+  - name: latency_proposal_delay_export
+    script: .testnet/scenarios/perf/ce_export_latency_probe.py
+    params:
+      warmup_ledgers: 3
+      ledgers: 8
+      submit_export: true
+    network:
+      rc:
+        - rng_poll_ms=250
+        - delay=100,jitter=25,msg=proposal
+
+  - name: latency_directed_pair_delay_export
+    script: .testnet/scenarios/perf/ce_export_latency_probe.py
+    params:
+      warmup_ledgers: 3
+      ledgers: 8
+      submit_export: true
+    network:
+      rc:
+        - rng_poll_ms=250
+        - n0->n2:delay=750,jitter=100,msg=proposal
+        - n2->n0:delay=750,jitter=100,msg=proposal
+
+  - name: latency_slow_minority_export
+    script: .testnet/scenarios/perf/ce_export_latency_probe.py
+    params:
+      warmup_ledgers: 3
+      ledgers: 8
+      submit_export: true
+      export_timeout: 120
+    network:
+      rc:
+        - rng_poll_ms=250
+        - n3->n0:delay=500,jitter=100,msg=proposal
+        - n3->n1:delay=500,jitter=100,msg=proposal
+        - n3->n2:delay=500,jitter=100,msg=proposal
+        - n4->n0:delay=500,jitter=100,msg=proposal
+        - n4->n1:delay=500,jitter=100,msg=proposal
+        - n4->n2:delay=500,jitter=100,msg=proposal
+        - n0->n3:delay=500,jitter=100,msg=proposal
+        - n1->n3:delay=500,jitter=100,msg=proposal
+        - n2->n3:delay=500,jitter=100,msg=proposal
+        - n0->n4:delay=500,jitter=100,msg=proposal
+        - n1->n4:delay=500,jitter=100,msg=proposal
+        - n2->n4:delay=500,jitter=100,msg=proposal
+
+  - name: latency_export_no_veto_with_delay
+    script: .testnet/scenarios/export/export_no_veto_missing_observation.py
+    network:
+      rc:
+        - rng_poll_ms=250
+        - delay=300,jitter=100,msg=proposal
+        - n4:no_export_sig_hash=true

.testnet/scenarios/perf/ce_export_latency_probe.py

@@ -0,0 +1,196 @@
+""":descr: measure CE/export behavior while RuntimeConfig injects latency/drop.
+
+The suite supplies runtime fault injection through network.rc. This scenario
+does not mutate RuntimeConfig itself; it observes what the launched network does
+under that condition and logs enough counters to compare variants.
+"""
+
+from __future__ import annotations
+
+from collections import Counter
+import json
+
+from export.export_helpers import assert_export_result, require_export
+from helpers import consensus_entropy_feature, get_entropy_tx
+
+
+async def _require_runtime_config(ctx, log):
+    result = ctx.rpc.runtime_config(0)
+    if not result or result.get("error"):
+        raise AssertionError(
+            "Latency probe requires a binary built with "
+            "xahaud_runtime_test_config=ON; runtime_config RPC returned "
+            f"{result}"
+        )
+    log("RuntimeConfig RPC active")
+
+
+async def _require_consensus_entropy(ctx, log):
+    feature = consensus_entropy_feature(ctx, node_id=0)
+    if not feature or not feature.get("enabled", False):
+        raise AssertionError(f"ConsensusEntropy not enabled: {feature}")
+    log("ConsensusEntropy enabled")
+
+
+def _log_runtime_config(ctx, log):
+    for node_id in range(ctx.node_count):
+        cfg = ctx.rpc.runtime_config(node_id)
+        if cfg is None:
+            raise AssertionError(f"runtime_config RPC failed on node {node_id}")
+        log(
+            f"runtime_config n{node_id}: "
+            f"{json.dumps(cfg, sort_keys=True, separators=(',', ':'))}"
+        )
+
+
+async def _submit_direct_export(ctx, log, *, timeout):
+    await ctx.fund_accounts({"alice": 10000, "bob": 1000})
+    alice = ctx.account("alice")
+    bob = ctx.account("bob")
+    current_seq = ctx.validated_ledger_index(0)
+
+    if current_seq is None:
+        raise AssertionError("validated ledger is not available before Export")
+
+    log(f"Submitting direct Export at validated ledger {current_seq}")
+    started = ctx.mark("latency-export-submit-start")
+    result = await ctx.submit_and_wait(
+        {
+            "TransactionType": "Export",
+            "LastLedgerSequence": current_seq + 12,
+            "Fee": "1000000",
+            "ExportedTxn": {
+                "TransactionType": "Payment",
+                "Account": alice.address,
+                "Destination": bob.address,
+                "Amount": "1000000",
+                "Fee": "10",
+                "Sequence": 0,
+                "TicketSequence": 1,
+                "FirstLedgerSequence": current_seq + 1,
+                "LastLedgerSequence": current_seq + 10,
+                "Flags": 2147483648,
+                "SigningPubKey": "",
+            },
+        },
+        alice.wallet,
+        timeout=timeout,
+    )
+    ended = ctx.mark("latency-export-submit-end")
+
+    elapsed = (ended.monotonic_ns - started.monotonic_ns) / 1_000_000_000
+    engine_result = result.get("engine_result", "")
+    log(f"Export result={engine_result} elapsed={elapsed:.3f}s")
+
+    if engine_result != "tesSUCCESS":
+        raise AssertionError(f"Expected Export tesSUCCESS, got {engine_result}")
+
+    export_result = assert_export_result(result.get("meta", {}), log)
+    signers = export_result.get("ExportedTxn", {}).get("Signers", [])
+    log(f"Export signer count={len(signers)}")
+    return started, ended
+
+
+def _summarize_logs(ctx, log, *, label, started, ended):
+    patterns = {
+        "rng_selected": r"RNG: entropy selected",
+        "rng_fallback": r"tier=1",
+        "rng_participant_aligned": r"tier=2",
+        "rng_validator_quorum": r"tier=3",
+        "export_retry": r"terRETRY_EXPORT",
+        "export_quorum_timeout": r"Export: exportSigSet quorum alignment timeout",
+        "export_missing_observation_ignored": (
+            r"Export: missing exportSigSetHash observation ignored"
+        ),
+    }
+    for name, pattern in patterns.items():
+        result = ctx.search_logs(pattern, since=started, until=ended, limit=500)
+        log(f"log_count {label}.{name}={result.count}")
+
+
+async def scenario(
+    ctx,
+    log,
+    *,
+    warmup_ledgers=3,
+    ledgers=8,
+    submit_export=False,
+    export_timeout=90,
+):
+    await ctx.wait_for_ledger_close(timeout=120)
+    await _require_runtime_config(ctx, log)
+    _log_runtime_config(ctx, log)
+    await _require_consensus_entropy(ctx, log)
+
+    if submit_export:
+        # require_export also asserts the UNLReport precondition for successful
+        # network-mode Export. Keep that explicit in perf runs so a missing
+        # report does not masquerade as a latency failure.
+        await require_export(ctx, log, require_runtime_config=False)
+
+    await ctx.wait_for_ledgers(warmup_ledgers, node_id=0, timeout=120)
+    warm_seq = ctx.validated_ledger_index(0)
+    log(f"Warmup complete at validated ledger {warm_seq}")
+
+    export_window = None
+    if submit_export:
+        export_window = await _submit_direct_export(
+            ctx, log, timeout=export_timeout
+        )
+
+    started = ctx.mark("latency-probe-start")
+    start_seq = ctx.validated_ledger_index(0)
+    await ctx.wait_for_ledgers(ledgers, node_id=0, timeout=max(120, ledgers * 30))
+    ended = ctx.mark("latency-probe-end")
+    end_seq = ctx.validated_ledger_index(0)
+
+    if start_seq is None or end_seq is None:
+        raise AssertionError("validated ledger index unavailable during probe")
+
+    elapsed = (ended.monotonic_ns - started.monotonic_ns) / 1_000_000_000
+    closed = max(0, end_seq - start_seq)
+    cadence = elapsed / closed if closed else 0.0
+    log(
+        f"Observed validated ledgers {start_seq + 1}..{end_seq} "
+        f"closed={closed} elapsed={elapsed:.3f}s cadence={cadence:.3f}s/ledger"
+    )
+
+    tiers: Counter[int] = Counter()
+    counts: Counter[int] = Counter()
+    missing_entropy = 0
+    for seq in range(start_seq + 1, end_seq + 1):
+        try:
+            ce, user_txns = get_entropy_tx(ctx, seq)
+        except AssertionError as exc:
+            missing_entropy += 1
+            log(f"  Ledger {seq}: no ConsensusEntropy tx ({exc})")
+            continue
+
+        tier = ce.get("EntropyTier", -1)
+        count = ce.get("EntropyCount", -1)
+        tiers[tier] += 1
+        counts[count] += 1
+        log(
+            f"  Ledger {seq}: tier={tier} count={count} "
+            f"user_txns={len(user_txns)} digest={ce.get('Digest', '')[:16]}..."
+        )
+
+    log(
+        "SUMMARY "
+        f"closed={closed} elapsed_s={elapsed:.3f} cadence_s={cadence:.3f} "
+        f"tiers={dict(sorted(tiers.items()))} "
+        f"counts={dict(sorted(counts.items()))} "
+        f"missing_entropy={missing_entropy}"
+    )
+
+    _summarize_logs(ctx, log, label="probe", started=started, ended=ended)
+    if export_window is not None:
+        _summarize_logs(
+            ctx,
+            log,
+            label="export",
+            started=export_window[0],
+            ended=export_window[1],
+        )
+
+    log("PASS")

.testnet/scenarios/suite.yml

@@ -0,0 +1,62 @@
+defaults:
+  network:
+    node_count: 5
+    launcher: tmux
+    find_ports: true
+    slave_delay: 0.2
+    features:
+      - ConsensusEntropy
+    track_features:
+      - ConsensusEntropy
+    unl_report: true
+    log_levels:
+      TxQ: info
+      Protocol: debug
+      Peer: debug
+      LedgerConsensus: debug
+      ConsensusExtensions: debug
+      NetworkOPs: info
+    env:
+      XAHAU_RESOURCE_PER_PORT: "1"
+    rc:
+      - rng_poll_ms=333
+
+tests:
+  - name: steady_state_entropy
+    script: .testnet/scenarios/entropy/steady_state_entropy.py
+
+  - name: fallback_without_unl_report
+    script: .testnet/scenarios/entropy/fallback_without_unl_report.py
+    network:
+      unl_report: false
+
+  - name: steady_state_entropy_fast_start
+    script: .testnet/scenarios/entropy/steady_state_entropy.py
+    network:
+      env:
+        XAHAUD_RUNTIME_TEST_CONFIG: '{"set":{"global":{"rng_poll_ms":333,"bootstrap_fast_start":true}}}'
+
+  - name: entropy_with_transactions
+    script: .testnet/scenarios/entropy/entropy_with_transactions.py
+
+  - name: quorum_recovery_smoke
+    script: .testnet/scenarios/entropy/quorum_recovery_smoke.py
+
+  - name: quorum_degradation_smoke
+    script: .testnet/scenarios/entropy/quorum_degradation_smoke.py
+    network:
+      log_levels:
+        LedgerConsensus: trace
+        ConsensusExtensions: trace
+
+  # Tier 2 (participant_aligned) needs 6 nodes: n=5 has no band (tier2 ==
+  # quorum). At 6, the 4/6 window is the participant_aligned band.
+  - name: participant_aligned_smoke
+    script: .testnet/scenarios/entropy/participant_aligned_smoke.py
+    network:
+      node_count: 6
+      log_levels:
+        LedgerConsensus: trace
+        ConsensusExtensions: trace
+
+  # Export scenarios: see export-suite.yml

Builds/levelization/results/loops.txt

@@ -26,7 +26,7 @@ Loop: xrpld.app xrpld.nodestore
   xrpld.app > xrpld.nodestore
 
 Loop: xrpld.app xrpld.overlay
-  xrpld.overlay ~= xrpld.app
+  xrpld.overlay == xrpld.app
 
 Loop: xrpld.app xrpld.peerfinder
   xrpld.app > xrpld.peerfinder

Builds/levelization/results/ordering.txt

@@ -12,6 +12,7 @@ libxrpl.server > xrpl.basics
 libxrpl.server > xrpl.json
 libxrpl.server > xrpl.protocol
 libxrpl.server > xrpl.server
+test.app > test.shamap
 test.app > test.toplevel
 test.app > test.unit_test
 test.app > xrpl.basics
@@ -21,6 +22,7 @@ test.app > xrpld.ledger
 test.app > xrpld.nodestore
 test.app > xrpld.overlay
 test.app > xrpld.rpc
+test.app > xrpld.shamap
 test.app > xrpl.hook
 test.app > xrpl.json
 test.app > xrpl.protocol
@@ -43,6 +45,7 @@ test.consensus > xrpld.app
 test.consensus > xrpld.consensus
 test.consensus > xrpld.core
 test.consensus > xrpld.ledger
+test.consensus > xrpl.json
 test.consensus > xrpl.protocol
 test.core > test.jtx
 test.core > test.toplevel
@@ -56,6 +59,8 @@ test.csf > xrpl.basics
 test.csf > xrpld.consensus
 test.csf > xrpl.json
 test.csf > xrpl.protocol
+test.formal_verification > xrpld.app
+test.formal_verification > xrpld.consensus
 test.json > test.jtx
 test.json > xrpl.json
 test.jtx > xrpl.basics
@@ -84,6 +89,7 @@ test.nodestore > xrpl.basics
 test.nodestore > xrpld.core
 test.nodestore > xrpld.nodestore
 test.nodestore > xrpld.unity
+test.nodestore > xrpl.protocol
 test.overlay > test.jtx
 test.overlay > test.toplevel
 test.overlay > test.unit_test
@@ -118,6 +124,7 @@ test.rpc > xrpld.core
 test.rpc > xrpld.net
 test.rpc > xrpld.overlay
 test.rpc > xrpld.rpc
+test.rpc > xrpld.shamap
 test.rpc > xrpl.hook
 test.rpc > xrpl.json
 test.rpc > xrpl.protocol

build-core.sh

@@ -95,8 +95,16 @@ if [[ "$4" == "" ]]; then
   echo "Non GH, local building, no Action runner magic"
 else
   # GH Action, runner
-  cp /io/release-build/xahaud /data/builds/$(date +%Y).$(date +%-m).$(date +%-d)-$(git rev-parse --abbrev-ref HEAD)+$4
-  cp /io/release-build/release.info /data/builds/$(date +%Y).$(date +%-m).$(date +%-d)-$(git rev-parse --abbrev-ref HEAD)+$4.releaseinfo
+    if [[ "$(git rev-parse --abbrev-ref HEAD)" == "release" ]]; then
+        echo "building on the release branch... placing it in builds/candidate"
+        mkdir /data/builds/candidate
+        cp /io/release-build/xahaud /data/builds/candidate/$(date +%Y).$(date +%-m).$(date +%-d)-$(git rev-parse --abbrev-ref HEAD)+$4
+        cp /io/release-build/release.info /data/builds/candidate/$(date +%Y).$(date +%-m).$(date +%-d)-$(git rev-parse --abbrev-ref HEAD)+$4.releaseinfo
+    else
+        echo "building non-release branch, placing it in builds root"
+        cp /io/release-build/xahaud /data/builds/$(date +%Y).$(date +%-m).$(date +%-d)-$(git rev-parse --abbrev-ref HEAD)+$4
+        cp /io/release-build/release.info /data/builds/$(date +%Y).$(date +%-m).$(date +%-d)-$(git rev-parse --abbrev-ref HEAD)+$4.releaseinfo
+    fi  
   echo "Published build to: http://build.xahau.tech/"
   echo $(date +%Y).$(date +%-m).$(date +%-d)-$(git rev-parse --abbrev-ref HEAD)+$4
 fi

build-full.sh

@@ -12,17 +12,16 @@ echo "-- GITHUB_REPOSITORY: $1"
 echo "-- GITHUB_SHA:        $2"
 echo "-- GITHUB_RUN_NUMBER: $4"
 
-umask 0000;
+umask 0000
 
 ####
 
-cd /io;
-mkdir -p src/certs;
-curl --silent -k https://raw.githubusercontent.com/RichardAH/rippled-release-builder/main/ca-bundle/certbundle.h -o src/certs/certbundle.h;
-if [ "`grep certbundle.h src/xrpld/net/detail/RegisterSSLCerts.cpp | wc -l`" -eq "0" ]
-then
-    cp src/xrpld/net/detail/RegisterSSLCerts.cpp src/xrpld/net/detail/RegisterSSLCerts.cpp.old
-    perl -i -pe "s/^{/{
+cd /io
+mkdir -p src/certs
+curl --silent -k https://raw.githubusercontent.com/RichardAH/rippled-release-builder/main/ca-bundle/certbundle.h -o src/certs/certbundle.h
+if [ "$(grep certbundle.h src/xrpld/net/detail/RegisterSSLCerts.cpp | wc -l)" -eq "0" ]; then
+  cp src/xrpld/net/detail/RegisterSSLCerts.cpp src/xrpld/net/detail/RegisterSSLCerts.cpp.old
+  perl -i -pe "s/^{/{
     #ifdef EMBEDDED_CA_BUNDLE
     BIO *cbio = BIO_new_mem_buf(ca_bundle.data(), ca_bundle.size());
     X509_STORE  *cts = SSL_CTX_get_cert_store(ctx.native_handle());
@@ -68,15 +67,14 @@ fi
 source /opt/rh/gcc-toolset-11/enable
 export PATH=/usr/local/bin:$PATH
 export CC='/usr/lib64/ccache/gcc' &&
-export CXX='/usr/lib64/ccache/g++' &&
-echo "-- Build Rippled --" &&
-pwd &&
+  export CXX='/usr/lib64/ccache/g++' &&
+  echo "-- Build Rippled --" &&
+  pwd &&
+  echo "MOVING TO [ build-core.sh ]"
 
-echo "MOVING TO [ build-core.sh ]";
-
-printenv > .env.temp;
-cat .env.temp | grep '=' | sed s/\\\(^[^=]\\+=\\\)/\\1\\\"/g|sed s/\$/\\\"/g > .env;
-rm .env.temp;
+printenv >.env.temp
+cat .env.temp | grep '=' | sed s/\\\(^[^=]\\+=\\\)/\\1\\\"/g | sed s/\$/\\\"/g >.env
+rm .env.temp
 
 echo "Persisting ENV:"
 cat .env

cmake/CodeCoverage.cmake

@@ -95,6 +95,9 @@
 #     - replace both functions setup_target_for_coverage_gcovr_* with a single setup_target_for_coverage_gcovr
 #     - add support for all gcovr output formats
 #
+# 2024-04-03, Bronek Kozicki
+#     - add support for output formats: jacoco, clover, lcov
+#
 # USAGE:
 #
 # 1. Copy this file into your cmake modules path.
@@ -256,10 +259,10 @@ endif()
 #     BASE_DIRECTORY "../"                   # Base directory for report
 #                                            #  (defaults to PROJECT_SOURCE_DIR)
 #     FORMAT "cobertura"                     # Output format, one of:
-#                                            #  xml cobertura sonarqube json-summary
-#                                            #  json-details coveralls csv txt
-#                                            #  html-single html-nested html-details
-#                                            #  (xml is an alias to cobertura;
+#                                            #  xml cobertura sonarqube jacoco clover
+#                                            #  json-summary json-details coveralls csv
+#                                            #  txt html-single html-nested html-details
+#                                            #  lcov (xml is an alias to cobertura;
 #                                            #  if no format is set, defaults to xml)
 #     EXCLUDE "src/dir1/*" "src/dir2/*"      # Patterns to exclude (can be relative
 #                                            #  to BASE_DIRECTORY, with CMake 3.4+)
@@ -308,6 +311,8 @@ function(setup_target_for_coverage_gcovr)
             set(GCOVR_OUTPUT_FILE ${Coverage_NAME}.txt)
         elseif(Coverage_FORMAT STREQUAL "csv")
             set(GCOVR_OUTPUT_FILE ${Coverage_NAME}.csv)
+        elseif(Coverage_FORMAT STREQUAL "lcov")
+            set(GCOVR_OUTPUT_FILE ${Coverage_NAME}.lcov)
         else()
             set(GCOVR_OUTPUT_FILE ${Coverage_NAME}.xml)
         endif()
@@ -320,6 +325,14 @@ function(setup_target_for_coverage_gcovr)
         set(Coverage_FORMAT cobertura) # overwrite xml
     elseif(Coverage_FORMAT STREQUAL "sonarqube")
         list(APPEND GCOVR_ADDITIONAL_ARGS --sonarqube "${GCOVR_OUTPUT_FILE}" )
+    elseif(Coverage_FORMAT STREQUAL "jacoco")
+        list(APPEND GCOVR_ADDITIONAL_ARGS --jacoco "${GCOVR_OUTPUT_FILE}" )
+        list(APPEND GCOVR_ADDITIONAL_ARGS --jacoco-pretty )
+    elseif(Coverage_FORMAT STREQUAL "clover")
+        list(APPEND GCOVR_ADDITIONAL_ARGS --clover "${GCOVR_OUTPUT_FILE}" )
+        list(APPEND GCOVR_ADDITIONAL_ARGS --clover-pretty )
+    elseif(Coverage_FORMAT STREQUAL "lcov")
+        list(APPEND GCOVR_ADDITIONAL_ARGS --lcov "${GCOVR_OUTPUT_FILE}" )
     elseif(Coverage_FORMAT STREQUAL "json-summary")
         list(APPEND GCOVR_ADDITIONAL_ARGS --json-summary "${GCOVR_OUTPUT_FILE}" )
         list(APPEND GCOVR_ADDITIONAL_ARGS --json-summary-pretty)

cmake/RippledCore.cmake

@@ -160,11 +160,18 @@ target_link_modules(xrpl PUBLIC
 #     $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}/include>
 #     $<INSTALL_INTERFACE:include>)
 
+if(formal_verification AND NOT xrpld)
+  message(FATAL_ERROR "formal_verification requires xrpld=ON")
+endif()
+
 if(xrpld)
   add_executable(rippled)
   if(tests)
     target_compile_definitions(rippled PUBLIC ENABLE_TESTS)
   endif()
+  if(xahaud_runtime_test_config)
+    target_compile_definitions(rippled PUBLIC XAHAUD_ENABLE_RUNTIME_TEST_CONFIG=1)
+  endif()
   target_include_directories(rippled
     PRIVATE
       $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}/src>
@@ -180,6 +187,21 @@ if(xrpld)
       "${CMAKE_CURRENT_SOURCE_DIR}/src/test/*.cpp"
     )
     target_sources(rippled PRIVATE ${sources})
+
+    set(HOOKS_TEST_DIR "" CACHE PATH "External hook Env-test directory")
+    if(NOT HOOKS_TEST_DIR AND DEFINED ENV{HOOKS_TEST_DIR})
+      set(HOOKS_TEST_DIR "$ENV{HOOKS_TEST_DIR}")
+    endif()
+    if(HOOKS_TEST_DIR)
+      file(GLOB_RECURSE hook_test_sources CONFIGURE_DEPENDS
+        "${HOOKS_TEST_DIR}/*_test.cpp"
+      )
+      if(hook_test_sources)
+        message(STATUS "Including external hook Env tests from ${HOOKS_TEST_DIR}")
+        target_sources(rippled PRIVATE ${hook_test_sources})
+        target_include_directories(rippled PRIVATE "${HOOKS_TEST_DIR}")
+      endif()
+    endif()
   endif()
 
   target_link_libraries(rippled
@@ -193,6 +215,7 @@ if(xrpld)
     # This is likely not strictly necessary, but listed explicitly as a good practice.
     m
   )
+  include(XahaudFormalVerification)
   exclude_if_included(rippled)
   # define a macro for tests that might need to
   # be exluded or run differently in CI environment

cmake/RippledInterface.cmake

@@ -22,6 +22,9 @@ target_compile_definitions (opts
     $<$<BOOL:${beast_no_unit_test_inline}>:BEAST_NO_UNIT_TEST_INLINE=1>
     $<$<BOOL:${beast_disable_autolink}>:BEAST_DONT_AUTOLINK_TO_WIN32_LIBRARIES=1>
     $<$<BOOL:${single_io_service_thread}>:RIPPLE_SINGLE_IO_SERVICE_THREAD=1>
+    # Enhanced logging is enabled for Debug builds, or explicitly via
+    # -DBEAST_ENHANCED_LOGGING=ON for other build types.
+    $<$<OR:$<CONFIG:Debug>,$<BOOL:${BEAST_ENHANCED_LOGGING}>>:BEAST_ENHANCED_LOGGING=1>
     $<$<BOOL:${voidstar}>:ENABLE_VOIDSTAR>)
 target_compile_options (opts
   INTERFACE

cmake/RippledSettings.cmake

@@ -12,6 +12,21 @@ option(xrpld "Build xrpld" ON)
 
 option(tests "Build tests" ON)
 
+option(xahaud_runtime_test_config
+  "Enable XAHAUD_RUNTIME_TEST_CONFIG env and runtime_config RPC fault-injection controls"
+  OFF)
+# Conan 2 local opt-in:
+# [conf]
+# tools.cmake.cmaketoolchain:extra_variables={"xahaud_runtime_test_config":"ON"}
+
+option(formal_verification
+  "Enable Lean-backed formal-verification cross-check tests"
+  OFF)
+# Default off: this pulls the Lean runtime and the vendored formal model into
+# the test binary. Conan/local opt-in mirrors the runtime-test-config pattern:
+# [conf]
+# tools.cmake.cmaketoolchain:extra_variables={"formal_verification":"ON"}
+
 option(unity "Creates a build using UNITY support in cmake. This is the default" ON)
 if(unity)
   if(NOT is_ci)

cmake/XahaudFormalVerification.cmake

@@ -0,0 +1,65 @@
+if(NOT formal_verification)
+  return()
+endif()
+
+if(NOT xrpld)
+  message(FATAL_ERROR "formal_verification requires xrpld=ON")
+endif()
+
+if(NOT tests)
+  message(FATAL_ERROR "formal_verification requires tests=ON")
+endif()
+
+if(CMAKE_CROSSCOMPILING)
+  message(FATAL_ERROR "formal_verification currently supports native builds only")
+endif()
+
+if(WIN32)
+  message(FATAL_ERROR "formal_verification currently supports Unix-like native builds only")
+endif()
+
+set(XAHAU_FORMAL_VERIFICATION_DIR
+  "${CMAKE_CURRENT_SOURCE_DIR}/formal_verification"
+  CACHE PATH
+  "Lean formal-verification project used by formal_verification=ON")
+
+include(XahaudLean)
+xahaud_require_lean_toolchain("${XAHAU_FORMAL_VERIFICATION_DIR}")
+
+set(XAHAU_FORMAL_ARCHIVE
+  "${XAHAU_FORMAL_VERIFICATION_DIR}/.lake/build/lib/libxahau__consensus_XahauConsensus.a")
+
+file(GLOB_RECURSE XAHAU_FORMAL_SOURCES CONFIGURE_DEPENDS
+  "${XAHAU_FORMAL_VERIFICATION_DIR}/*.lean")
+
+# Lake currently writes package artifacts under the Lean workspace's .lake/
+# directory. Keep this option native/test-only until the build is moved to a
+# copied CMake-binary-dir workspace or Lake grows a stable external build-dir
+# interface we can rely on here.
+#
+# This target deliberately invokes Lake whenever the formal-enabled `rippled`
+# target is built. Lake still performs its own incremental rebuild, but CMake
+# must not trust a source-tree `.lake` archive purely by timestamp.
+add_custom_target(xahaud_formal_verification_lean
+  COMMAND "${LAKE_EXECUTABLE}" build XahauConsensus:static
+  WORKING_DIRECTORY "${XAHAU_FORMAL_VERIFICATION_DIR}"
+  DEPENDS
+    "${XAHAU_FORMAL_VERIFICATION_DIR}/lakefile.toml"
+    "${XAHAU_FORMAL_VERIFICATION_DIR}/lean-toolchain"
+    "${XAHAU_FORMAL_VERIFICATION_DIR}/lake-manifest.json"
+    ${XAHAU_FORMAL_SOURCES}
+  BYPRODUCTS "${XAHAU_FORMAL_ARCHIVE}"
+  COMMENT "Building Lean formal-verification archive"
+  VERBATIM)
+
+add_dependencies(rippled xahaud_formal_verification_lean)
+target_compile_definitions(rippled PRIVATE XAHAUD_ENABLE_FORMAL_VERIFICATION=1)
+target_include_directories(rippled PRIVATE "${LEAN_INCLUDE_DIR}")
+target_link_libraries(rippled "${XAHAU_FORMAL_ARCHIVE}" "${LEAN_SHARED_LIBRARY}")
+
+if(UNIX)
+  set_property(TARGET rippled APPEND PROPERTY BUILD_RPATH "${LEAN_SYSROOT}/lib/lean")
+endif()
+
+message(STATUS "Formal verification enabled: ${XAHAU_FORMAL_VERIFICATION_DIR}")
+message(STATUS "Lean ${LEAN_EXPECTED_VERSION} sysroot: ${LEAN_SYSROOT}")

cmake/XahaudLean.cmake

@@ -0,0 +1,113 @@
+include_guard(GLOBAL)
+
+function(xahaud_require_lean_toolchain project_dir)
+  if(NOT EXISTS "${project_dir}/lean-toolchain")
+    message(FATAL_ERROR "Lean project is missing lean-toolchain: ${project_dir}")
+  endif()
+
+  file(READ "${project_dir}/lean-toolchain" lean_toolchain)
+  string(STRIP "${lean_toolchain}" lean_toolchain)
+  if(NOT lean_toolchain MATCHES "^leanprover/lean4:v([0-9]+\\.[0-9]+\\.[0-9]+([-+._A-Za-z0-9]+)?)$")
+    message(FATAL_ERROR
+      "Unsupported lean-toolchain format `${lean_toolchain}` in ${project_dir}")
+  endif()
+  set(expected_lean_version "${CMAKE_MATCH_1}")
+
+  find_program(LAKE_EXECUTABLE
+    NAMES lake
+    HINTS "$ENV{HOME}/.elan/bin")
+  if(NOT LAKE_EXECUTABLE)
+    message(FATAL_ERROR
+      "formal_verification=ON requires Lake on PATH or in ~/.elan/bin. "
+      "Install elan, then run `lake build` once in ${project_dir}.")
+  endif()
+
+  execute_process(
+    COMMAND "${LAKE_EXECUTABLE}" env lean --version
+    WORKING_DIRECTORY "${project_dir}"
+    OUTPUT_VARIABLE lean_version_output
+    ERROR_VARIABLE lean_version_error
+    OUTPUT_STRIP_TRAILING_WHITESPACE
+    ERROR_STRIP_TRAILING_WHITESPACE
+    RESULT_VARIABLE lean_version_result)
+  if(NOT lean_version_result EQUAL 0)
+    message(FATAL_ERROR
+      "Could not run `${LAKE_EXECUTABLE} env lean --version`: "
+      "${lean_version_error}")
+  endif()
+  if(NOT lean_version_output MATCHES "^Lean \\(version ([^,)]+)[,)]")
+    message(FATAL_ERROR
+      "Could not parse Lean version from `${lean_version_output}`")
+  endif()
+  set(actual_lean_version "${CMAKE_MATCH_1}")
+  if(NOT actual_lean_version STREQUAL expected_lean_version)
+    message(FATAL_ERROR
+      "Lean version mismatch for formal_verification=ON. "
+      "Expected ${expected_lean_version} from ${project_dir}/lean-toolchain, "
+      "but `${LAKE_EXECUTABLE} env lean --version` returned "
+      "`${lean_version_output}`")
+  endif()
+
+  execute_process(
+    COMMAND "${LAKE_EXECUTABLE}" --version
+    WORKING_DIRECTORY "${project_dir}"
+    OUTPUT_VARIABLE lake_version_output
+    ERROR_VARIABLE lake_version_error
+    OUTPUT_STRIP_TRAILING_WHITESPACE
+    ERROR_STRIP_TRAILING_WHITESPACE
+    RESULT_VARIABLE lake_version_result)
+  if(NOT lake_version_result EQUAL 0)
+    message(FATAL_ERROR
+      "Could not run `${LAKE_EXECUTABLE} --version`: ${lake_version_error}")
+  endif()
+  if(NOT lake_version_output MATCHES "Lean version ([^)]+)\\)")
+    message(FATAL_ERROR
+      "Could not parse Lake's Lean version from `${lake_version_output}`")
+  endif()
+  set(lake_lean_version "${CMAKE_MATCH_1}")
+  if(NOT lake_lean_version STREQUAL expected_lean_version)
+    message(FATAL_ERROR
+      "Lake version mismatch for formal_verification=ON. "
+      "Expected Lean ${expected_lean_version} from ${project_dir}/lean-toolchain, "
+      "but `${LAKE_EXECUTABLE} --version` returned `${lake_version_output}`")
+  endif()
+
+  if(NOT EXISTS "${project_dir}/lakefile.toml")
+    message(FATAL_ERROR
+      "formal_verification=ON requires ${project_dir}/lakefile.toml")
+  endif()
+
+  execute_process(
+    COMMAND "${LAKE_EXECUTABLE}" env printenv LEAN_SYSROOT
+    WORKING_DIRECTORY "${project_dir}"
+    OUTPUT_VARIABLE lean_sysroot
+    ERROR_VARIABLE lean_sysroot_error
+    OUTPUT_STRIP_TRAILING_WHITESPACE
+    ERROR_STRIP_TRAILING_WHITESPACE
+    RESULT_VARIABLE lean_sysroot_result)
+  if(NOT lean_sysroot_result EQUAL 0 OR NOT lean_sysroot)
+    message(FATAL_ERROR
+      "Could not determine Lean sysroot via "
+      "`${LAKE_EXECUTABLE} env printenv LEAN_SYSROOT`: ${lean_sysroot_error}")
+  endif()
+
+  set(lean_include_dir "${lean_sysroot}/include")
+  if(NOT EXISTS "${lean_include_dir}/lean/lean.h")
+    message(FATAL_ERROR "Lean header not found: ${lean_include_dir}/lean/lean.h")
+  endif()
+
+  find_library(lean_shared_library
+    NAMES leanshared libleanshared
+    PATHS "${lean_sysroot}/lib/lean"
+    NO_DEFAULT_PATH)
+  if(NOT lean_shared_library)
+    message(FATAL_ERROR
+      "Lean shared runtime not found under ${lean_sysroot}/lib/lean")
+  endif()
+
+  set(LAKE_EXECUTABLE "${LAKE_EXECUTABLE}" PARENT_SCOPE)
+  set(LEAN_SYSROOT "${lean_sysroot}" PARENT_SCOPE)
+  set(LEAN_INCLUDE_DIR "${lean_include_dir}" PARENT_SCOPE)
+  set(LEAN_SHARED_LIBRARY "${lean_shared_library}" PARENT_SCOPE)
+  set(LEAN_EXPECTED_VERSION "${expected_lean_version}" PARENT_SCOPE)
+endfunction()

conanfile.py

@@ -1,4 +1,5 @@
 from conan import ConanFile
+from conan.errors import ConanInvalidConfiguration
 from conan.tools.cmake import CMake, CMakeToolchain, cmake_layout
 import re
 
@@ -14,6 +15,7 @@ class Xrpl(ConanFile):
         'assertions': [True, False],
         'coverage': [True, False],
         'fPIC': [True, False],
+        'formal_verification': [True, False],
         'jemalloc': [True, False],
         'rocksdb': [True, False],
         'shared': [True, False],
@@ -45,6 +47,7 @@ class Xrpl(ConanFile):
         'assertions': False,
         'coverage': False,
         'fPIC': True,
+        'formal_verification': False,
         'jemalloc': False,
         'rocksdb': True,
         'shared': False,
@@ -110,6 +113,14 @@ class Xrpl(ConanFile):
         if self.settings.compiler == 'apple-clang':
             self.options['boost/*'].visibility = 'global'
 
+    def validate(self):
+        if self.options.formal_verification and (
+            not self.options.tests or not self.options.xrpld
+        ):
+            raise ConanInvalidConfiguration(
+                'formal_verification=True requires tests=True and xrpld=True'
+            )
+
     def requirements(self):
         # Force sqlite3 version to avoid conflicts with soci
         self.requires('sqlite3/3.47.0', override=True)
@@ -132,6 +143,18 @@ class Xrpl(ConanFile):
         'cfg/*',
         'cmake/*',
         'external/*',
+        'formal_verification/*.json',
+        'formal_verification/*.lean',
+        'formal_verification/*.md',
+        'formal_verification/*.toml',
+        'formal_verification/lean-toolchain',
+        'formal_verification/XahauConsensus/*.lean',
+        '!formal_verification/.lake',
+        '!formal_verification/.lake/*',
+        '!formal_verification/.lake/**',
+        '!formal_verification/**/.lake',
+        '!formal_verification/**/.lake/*',
+        '!formal_verification/**/.lake/**',
         'include/*',
         'src/*',
     )
@@ -148,6 +171,7 @@ class Xrpl(ConanFile):
         tc.variables['tests'] = self.options.tests
         tc.variables['assert'] = self.options.assertions
         tc.variables['coverage'] = self.options.coverage
+        tc.variables['formal_verification'] = self.options.formal_verification
         tc.variables['jemalloc'] = self.options.jemalloc
         tc.variables['rocksdb'] = self.options.rocksdb
         tc.variables['BUILD_SHARED_LIBS'] = self.options.shared
@@ -163,6 +187,11 @@ class Xrpl(ConanFile):
         cmake.build()
 
     def package(self):
+        if self.options.formal_verification:
+            raise ConanInvalidConfiguration(
+                'formal_verification=True is a local/CI test build option and '
+                'is not supported for Conan packages'
+            )
         cmake = CMake(self)
         cmake.verbose = True
         cmake.install()

formal_verification/.gitignore

@@ -0,0 +1 @@
+/.lake

formal_verification/README.md

@@ -0,0 +1,166 @@
+# xahau_consensus
+
+Lean proofs for small Xahau consensus invariants.
+
+This package is intentionally narrow. It does **not** try to verify the C++
+implementation directly. It mirrors small formulas and decision ladders from
+the consensus-extension code so the safety arguments can be checked as theorems
+instead of repeatedly re-derived in review notes.
+
+Current modules:
+
+- `XahauConsensus.Threshold`
+  - mirrors `calculateParticipantThreshold`
+  - proves the Tier-2 intersection inequality:
+    `count + floor(count / 5) < 2 * participantThreshold count`
+  - proves the threshold is minimal for that strict inequality
+  - proves the original-view threshold remains safe when nUNL shrinks the
+    effective view
+  - includes the `original=10`, `effective=8` regression example showing why
+    using the effective view for the Tier-2 floor is forkable
+  - proves `participantThreshold count <= quorumThreshold count` for
+    non-empty views
+  - distinguishes raw formula helpers from the live safety-wrapped gate
+    thresholds used by `ConsensusExtensions`
+- `XahauConsensus.ThresholdFacts`
+  - records small-network values and band-empty/band-present examples
+  - proves exact multiple-of-five behavior
+  - proves threshold monotonicity facts
+- `XahauConsensus.SixtyPercent`
+  - defines a naive `ceil(60%)` threshold
+  - proves naive 60% is unsafe at exact multiples of five
+  - proves the live derived floor is one higher there and restores strict
+    intersection safety
+- `XahauConsensus.Intersection`
+  - proves the abstract cardinality argument behind quorum intersection
+  - shows two threshold-sized cohorts must overlap above the fault bound
+    whenever `n + f < 2t`
+  - specializes that argument to the live participant threshold, including
+    nUNL-shrunk effective views
+- `XahauConsensus.HonestOverlap`
+  - bridges overlap arithmetic to the consensus claim that two cohorts share at
+    least one honest validator
+  - specializes that bridge to the participant threshold and `floor(n/5)` fault
+    bound
+- `XahauConsensus.ViewUniverse`
+  - proves original-view anchoring remains safe under nUNL shrink
+  - separates strict safety from threshold reachability
+  - defines cross-view participant-band presence/absence
+  - shows effective-view thresholds can be unsafe against the original fault
+    bound
+  - shows trusted-superset counting universes erode the intersection margin
+- `XahauConsensus.NunlCap`
+  - models the protocol's ceil-25% nUNL disablement cap
+  - proves 8/6 and 10/8 band collapse examples
+  - records that 10 at max cap has effective view 7, below the original
+    participant floor
+  - records the important counterexample: original `20`, effective `15` does
+    **not** make validator quorum meet the original participant floor
+- `XahauConsensus.SidecarAlignment`
+  - models aligned participant counting for sidecar hashes
+  - proves non-active peers and non-active local publication cannot pad the
+    alignment count
+  - proves changing nonmember reports cannot change quorum alignment
+- `XahauConsensus.EntropySelector`
+  - models the tier-label ladder from `ConsensusExtensions::selectEntropy`
+  - proves non-UNLReport views select fallback
+  - proves the quorum / participant / fallback bands select the expected tier
+- `XahauConsensus.SelectorDeterminism`
+  - models labeled digest output
+  - proves digest payload bytes do not affect the label when consensus metadata
+    is fixed
+  - records examples where changing view provenance or view sizes changes labels
+- `XahauConsensus.ExportGate`
+  - models export's quorum-aligned success rule
+  - models export's sidecar-gate outcome as `proceed` or `retryOrExpire`, with
+    no deterministic fallback signature set
+  - proves missing minority observation does not block a quorum-aligned export
+  - proves `fullObservation` alone cannot change the export decision
+- `XahauConsensus.ExportQuorum`
+  - proves two 80% export quorums overlap above the standard Byzantine bound
+    in nonempty active universes
+  - proves export quorum overlap remains above the original-view Byzantine
+    bound when nUNL shrinkage is within the protocol cap
+  - proves Byzantine validators at the standard bound cannot veto quorum
+  - records concrete overlap margins for 5/10/20-validator universes
+- `XahauConsensus.FinsetIntersection`
+  - uses Mathlib finite sets to prove the cardinality premise behind the
+    arithmetic intersection theorems
+  - specializes that bridge for Tier-2 cohorts, nUNL-shrunk cohorts, and export
+    80% quorums
+- `XahauConsensus.Invariants`
+  - restates cross-module design contracts in one place
+  - pins the live safety-wrapped threshold relationship
+  - proves the cross-view entropy gate is exactly the selector's non-fallback
+    boundary
+  - pins non-UNLReport fallback and export full-observation independence
+
+Run:
+
+```sh
+~/.elan/bin/lake build
+```
+
+## Optional C++ cross-checks
+
+The xahaud CMake build can also compile a Lean-backed unit-test path, but it is
+off by default and is not part of normal release builds:
+
+Install Lean through `elan` first. The CMake integration intentionally keeps the
+tooling rule simple: when `formal_verification=ON`, it looks for `lake` on
+`PATH` or in `~/.elan/bin`, asks that Lake environment to run `lean --version`,
+verifies the exact version specified by this package's `lean-toolchain`, then
+asks Lake for `LEAN_SYSROOT` and checks that `lean.h` and `libleanshared`
+exist.
+
+```sh
+conan install . --output-folder=build-formal --build=missing \
+  -s build_type=Release \
+  -o '&:tests=True' \
+  -o '&:xrpld=True' \
+  -o '&:formal_verification=True'
+
+cmake -S . -B build-formal-cmake \
+  -DCMAKE_TOOLCHAIN_FILE=$PWD/build-formal/build/generators/conan_toolchain.cmake \
+  -Dtests=ON \
+  -Dxrpld=ON \
+  -Dformal_verification=ON
+
+cmake --build build-formal-cmake --target rippled
+./build-formal-cmake/rippled --unittest=LeanConsensus
+```
+
+This path currently supports native test builds only. It builds
+`XahauConsensus:static`, links the resulting Lean archive and runtime into the
+test binary, and runs C++ drift tests over selected scalar formulas and helper
+predicates. Some checks compare directly to named production helpers; others are
+review-oriented safety predicates computed from those helpers. The exported
+surface is intentionally scalar and reviewable:
+
+- Byzantine bound, participant threshold, and validator quorum threshold.
+- The safety-wrapped zero-view thresholds used by the live gates.
+- The cross-view entropy gate threshold, with effective and original view
+  denominators kept separate.
+- The entropy tier selector policy for `(fromUNLReport, participantCount,
+  effectiveView, originalView)`.
+- Sidecar aligned-participant counting, full-observation, quorum-aligned
+  predicates, and active-view mask-counting samples.
+- Export's quorum-only sidecar-gate proceed predicate, where `fullObservation`
+  is diagnostic rather than success-gating; a small final-apply snapshot model
+  makes explicit that gate proceed is not the same as closed-ledger
+  `Export::doApply` success.
+- NegativeUNL cap/effective-view arithmetic.
+- View-universe safety predicates and naive-60% regression anchors.
+
+This is still a model-to-code cross-check, not a proof that the C++ implements
+the Lean model. Its value is narrower and practical: if a production formula,
+decision ladder, or helper predicate changes without the formal model changing
+too, the gated unit test fails. The formal CMake target invokes Lake on each
+formal-enabled `rippled` build and lets Lake decide whether its own artifacts
+are current; CMake does not trust an existing source-tree archive by timestamp.
+Lake still writes build artifacts under the Lean workspace's `.lake/`
+directory, and the Conan recipe intentionally excludes that directory from
+exported sources, so keep this option as a local/CI confidence build rather
+than a release packaging input. The Conan recipe rejects
+`formal_verification=True` unless `tests=True` and `xrpld=True`, and refuses to
+package formal-enabled builds.

formal_verification/ROADMAP.md

@@ -0,0 +1,32 @@
+# Xahau Lean Roadmap
+
+This package should stay focused on invariants that are compact enough to be
+reviewable and stable enough to mirror from C++.
+
+Good targets:
+
+1. Threshold arithmetic
+   - Tier-2 participant threshold formula
+   - quorum threshold relation
+   - nUNL original-view anchoring
+   - small-network boundary examples
+2. Sidecar alignment
+   - active-view-only counting
+   - quorum-aligned predicate
+   - full-observation as diagnostic vs success precondition where applicable
+3. Entropy selector
+   - non-UNLReport fallback
+   - tier ladder from agreed participant count
+   - no local pending-state dependency in the tier decision
+4. Export gate
+   - quorum-aligned success without full observation
+   - no deterministic fallback value
+   - retry/expire as liveness behavior, not ledger-content substitution
+
+Poor targets for this package:
+
+- direct verification of C++ implementation details
+- wall-clock timing and network scheduling liveness
+- full ledger execution semantics
+
+Those belong in C++ tests, CSF/testnet scenarios, or a dedicated temporal model.

formal_verification/XahauConsensus.lean

@@ -0,0 +1,17 @@
+-- This module serves as the root of the `XahauConsensus` library.
+-- Import modules here that should be built as part of the library.
+import XahauConsensus.Threshold
+import XahauConsensus.ThresholdFacts
+import XahauConsensus.SixtyPercent
+import XahauConsensus.Intersection
+import XahauConsensus.HonestOverlap
+import XahauConsensus.ViewUniverse
+import XahauConsensus.NunlCap
+import XahauConsensus.SidecarAlignment
+import XahauConsensus.EntropySelector
+import XahauConsensus.SelectorDeterminism
+import XahauConsensus.ExportGate
+import XahauConsensus.ExportQuorum
+import XahauConsensus.FinsetIntersection
+import XahauConsensus.Invariants
+import XahauConsensus.FFI

formal_verification/XahauConsensus/EntropySelector.lean

@@ -0,0 +1,74 @@
+import XahauConsensus.Threshold
+
+namespace XahauConsensus
+
+inductive EntropyTier where
+  | consensusFallback
+  | participantAligned
+  | validatorQuorum
+  deriving DecidableEq, Repr
+
+/-- Minimal model of `ConsensusExtensions::selectEntropy`'s network,
+non-failed, non-empty tier ladder.
+
+The real C++ also computes a digest. This model deliberately focuses on the
+part that can fork by labeling the same agreed set differently: the tier
+decision from `(fromUNLReport, participantCount, effectiveView, originalView)`.
+It does not model the standalone development shortcut, timeout-driven
+`entropyFailed_` downgrade, or empty-map fallback; those paths all bypass or
+downgrade this ladder rather than producing a stronger non-fallback label.
+-/
+def selectEntropyTier
+    (fromUNLReport : Bool)
+    (participantCount effectiveView originalView : Nat) : EntropyTier :=
+  if !fromUNLReport then
+    EntropyTier.consensusFallback
+  else if participantCount >= safeQuorumThreshold effectiveView then
+    EntropyTier.validatorQuorum
+  else if participantCount >= safeParticipantThreshold originalView then
+    EntropyTier.participantAligned
+  else
+    EntropyTier.consensusFallback
+
+/-- Non-standalone nodes must fail closed to fallback until the validator view
+is ledger-anchored by a UNLReport. -/
+theorem no_unl_report_selects_fallback
+    (participantCount effectiveView originalView : Nat) :
+    selectEntropyTier false participantCount effectiveView originalView =
+      EntropyTier.consensusFallback := by
+  rfl
+
+/-- At or above the effective-view quorum threshold, the ladder selects the
+strongest entropy tier. -/
+theorem quorum_count_selects_validator_quorum
+    {participantCount effectiveView originalView : Nat}
+    (hQuorum : safeQuorumThreshold effectiveView <= participantCount) :
+    selectEntropyTier true participantCount effectiveView originalView =
+      EntropyTier.validatorQuorum := by
+  unfold selectEntropyTier
+  simp [hQuorum]
+
+/-- Below validator quorum but at or above the original-view participant floor,
+the ladder selects Tier 2. -/
+theorem participant_band_selects_tier2
+    {participantCount effectiveView originalView : Nat}
+    (hBelowQuorum : participantCount < safeQuorumThreshold effectiveView)
+    (hParticipant : safeParticipantThreshold originalView <= participantCount) :
+    selectEntropyTier true participantCount effectiveView originalView =
+      EntropyTier.participantAligned := by
+  unfold selectEntropyTier
+  simp [Nat.not_le_of_gt hBelowQuorum, hParticipant]
+
+/-- Below both thresholds, the ladder falls back. -/
+theorem below_participant_floor_selects_fallback
+    {participantCount effectiveView originalView : Nat}
+    (hBelowQuorum : participantCount < safeQuorumThreshold effectiveView)
+    (hBelowParticipant : participantCount < safeParticipantThreshold originalView) :
+    selectEntropyTier true participantCount effectiveView originalView =
+      EntropyTier.consensusFallback := by
+  unfold selectEntropyTier
+  simp [
+    Nat.not_le_of_gt hBelowQuorum,
+    Nat.not_le_of_gt hBelowParticipant]
+
+end XahauConsensus

formal_verification/XahauConsensus/ExportGate.lean

@@ -0,0 +1,139 @@
+namespace XahauConsensus
+
+/-- Minimal model of the sidecar export gate.
+
+`alignedParticipants` is the number of participants observed on the export
+sidecar, `quorumThreshold` is the required aligned count, and
+`fullObservation` records whether every participant was observed. The C++ gate
+must use quorum alignment for success; full observation is only diagnostic.
+-/
+structure ExportGate where
+  alignedParticipants : Nat
+  quorumThreshold : Nat
+  fullObservation : Bool
+  deriving DecidableEq, Repr
+
+/-- Export sidecar-gate outcome. This is not the final `Export::doApply`
+result: closed-ledger apply re-validates the frozen agreed signature snapshot
+before it can create a shadow ticket. -/
+inductive ExportOutcome where
+  | proceed
+  | retryOrExpire
+  deriving DecidableEq, Repr
+
+/-- The success predicate used by export: enough participants are aligned. -/
+def ExportGate.quorumAligned (gate : ExportGate) : Bool :=
+  decide (gate.quorumThreshold <= gate.alignedParticipants)
+
+/-- Export proceeds exactly when quorum alignment is met. -/
+def ExportGate.proceed (gate : ExportGate) : Bool :=
+  gate.quorumAligned
+
+/-- Export's externally visible decision shape. -/
+def ExportGate.outcome (gate : ExportGate) : ExportOutcome :=
+  if gate.proceed then ExportOutcome.proceed else ExportOutcome.retryOrExpire
+
+/-- Minimal model of the additional closed-ledger apply preconditions.
+
+The sidecar gate only proves that one `exportSigSetHash` had quorum alignment.
+Network-mode `Export::doApply` then independently requires a ledger-anchored
+validator view, no convergence failure for the round, a frozen agreed sidecar
+map, a parseable/valid signature set, and enough verified signers in that map.
+The model intentionally excludes cryptography and metadata construction; it
+exists to prevent reading `ExportGate.proceed` as final apply success.
+-/
+structure ExportApplySnapshot where
+  fromUNLReport : Bool
+  convergenceFailed : Bool
+  agreedSetPresent : Bool
+  agreedSetValid : Bool
+  signerCount : Nat
+  quorumThreshold : Nat
+  deriving DecidableEq, Repr
+
+/-- Closed-ledger apply can use only a valid, frozen agreed sidecar snapshot. -/
+def ExportApplySnapshot.validAgreedSnapshot
+    (snapshot : ExportApplySnapshot) : Bool :=
+  snapshot.fromUNLReport &&
+    !snapshot.convergenceFailed &&
+    snapshot.agreedSetPresent &&
+    snapshot.agreedSetValid &&
+    decide (snapshot.quorumThreshold <= snapshot.signerCount)
+
+/-- Minimal network-mode apply decision: valid agreed snapshot applies; all
+other cases retry or expire. -/
+def ExportApplySnapshot.outcome
+    (snapshot : ExportApplySnapshot) : ExportOutcome :=
+  if snapshot.validAgreedSnapshot then
+    ExportOutcome.proceed
+  else
+    ExportOutcome.retryOrExpire
+
+theorem apply_success_iff_valid_agreed_snapshot
+    (snapshot : ExportApplySnapshot) :
+    snapshot.outcome = ExportOutcome.proceed ↔
+      snapshot.validAgreedSnapshot = true := by
+  unfold ExportApplySnapshot.outcome
+  by_cases h : snapshot.validAgreedSnapshot <;> simp [h]
+
+/-- Gate success alone is not final apply success. For example, the sidecar
+gate may have quorum alignment while the final apply path has no frozen agreed
+sidecar map available and therefore retries. -/
+theorem gate_proceed_does_not_imply_apply_success :
+    ∃ gate : ExportGate, ∃ snapshot : ExportApplySnapshot,
+      ExportGate.proceed gate = true ∧
+        ExportApplySnapshot.outcome snapshot =
+          ExportOutcome.retryOrExpire := by
+  refine ⟨
+    ExportGate.mk 4 4 false,
+    ExportApplySnapshot.mk true false false true 4 4,
+    ?_,
+    ?_⟩ <;> rfl
+
+/-- A missing minority, represented by `fullObservation = false`, does not
+prevent export when the quorum threshold is met. -/
+theorem missing_minority_does_not_prevent_proceed
+    {alignedParticipants quorumThreshold : Nat}
+    (hQuorum : quorumThreshold <= alignedParticipants) :
+    (ExportGate.mk alignedParticipants quorumThreshold false).proceed = true := by
+  unfold ExportGate.proceed ExportGate.quorumAligned
+  simp [hQuorum]
+
+theorem missing_minority_proceeds
+    {alignedParticipants quorumThreshold : Nat}
+    (hQuorum : quorumThreshold <= alignedParticipants) :
+    (ExportGate.mk alignedParticipants quorumThreshold false).outcome =
+      ExportOutcome.proceed := by
+  unfold ExportGate.outcome
+  simp [missing_minority_does_not_prevent_proceed hQuorum]
+
+/-- Export must not proceed below the aligned-participant quorum threshold. -/
+theorem below_quorum_does_not_proceed
+    {alignedParticipants quorumThreshold : Nat}
+    (fullObservation : Bool)
+    (hBelow : alignedParticipants < quorumThreshold) :
+    (ExportGate.mk alignedParticipants quorumThreshold fullObservation).proceed =
+      false := by
+  unfold ExportGate.proceed ExportGate.quorumAligned
+  simp [Nat.not_le_of_gt hBelow]
+
+/-- Below quorum, export retries or expires. There is no deterministic fallback
+signature set analogous to RNG's Tier 1 fallback digest. -/
+theorem below_quorum_retries_or_expires
+    {alignedParticipants quorumThreshold : Nat}
+    (fullObservation : Bool)
+    (hBelow : alignedParticipants < quorumThreshold) :
+    (ExportGate.mk alignedParticipants quorumThreshold fullObservation).outcome =
+      ExportOutcome.retryOrExpire := by
+  unfold ExportGate.outcome
+  simp [below_quorum_does_not_proceed fullObservation hBelow]
+
+/-- Flipping only the diagnostic `fullObservation` field cannot change the
+export decision. -/
+theorem changing_fullObservation_alone_does_not_change_proceed
+    (alignedParticipants quorumThreshold : Nat) :
+    (ExportGate.mk alignedParticipants quorumThreshold true).proceed =
+      (ExportGate.mk alignedParticipants quorumThreshold false).proceed := by
+  rfl
+
+end XahauConsensus

formal_verification/XahauConsensus/ExportQuorum.lean

@@ -0,0 +1,254 @@
+import XahauConsensus.Intersection
+import XahauConsensus.NunlCap
+import XahauConsensus.ThresholdFacts
+
+namespace XahauConsensus
+
+/-!
+Nat-cardinality arithmetic for export sidecar quorum uniqueness.
+
+The model deliberately stays at the level used by `Intersection.lean`:
+
+* `n` is the active validator universe size.
+* `a` and `b` are the numbers of validators supporting two export sidecar
+  hashes in that same universe.
+* `overlap` is the size of the intersection between those two support sets.
+* `faultyOverlap + honestOverlap = overlap` splits that intersection.
+
+No `Finset` structure is needed here; callers supply the usual
+inclusion-exclusion cardinality inequality `a + b <= n + overlap`.
+-/
+
+theorem disabled_le_cap_mul_four_le
+    {originalView disabled : Nat}
+    (hCap : disabled <= disabledCap originalView) :
+    disabled * 4 <= originalView + 3 := by
+  unfold disabledCap ceilDiv at hCap
+  have hFour : 0 < 4 := by decide
+  simp at hCap
+  have hMul :=
+    (Nat.le_div_iff_mul_le hFour).mp hCap
+  omega
+
+theorem quorumThreshold_mul_five_ge_four_mul (n : Nat) :
+    4 * n <= 5 * quorumThreshold n := by
+  unfold quorumThreshold
+  have hHundred : 0 < 100 := by decide
+  have hDiv :
+      (n * 80 + 99) / 100 <= (n * 80 + 99) / 100 :=
+    Nat.le_refl _
+  have hBound :=
+    (Nat.div_le_iff_le_mul hHundred).mp hDiv
+  omega
+
+theorem byzantineBound_mul_five_le (n : Nat) :
+    byzantineBound n * 5 <= n := by
+  unfold byzantineBound
+  exact Nat.div_mul_le_self n 5
+
+/-- Two 80% export quorums in one active universe overlap by at least
+`2 * quorumThreshold n - n`. -/
+theorem two_export_quorums_overlap_lower_bound
+    {n a b overlap : Nat}
+    (hCardinality : a + b <= n + overlap)
+    (hA : quorumThreshold n <= a)
+    (hB : quorumThreshold n <= b) :
+    2 * quorumThreshold n - n <= overlap := by
+  omega
+
+/-- The 80% quorum threshold is intersection-safe against the standard
+`floor(n / 5)` fault bound for every nonempty active universe. -/
+theorem quorumThreshold_intersection_safe
+    {n : Nat} (hPositive : 0 < n) :
+    n + byzantineBound n < 2 * quorumThreshold n := by
+  unfold quorumThreshold byzantineBound
+  omega
+
+/-- The unconditional version is false: the empty active universe has raw
+quorum threshold zero, so there is no strict intersection margin. -/
+theorem quorumThreshold_empty_not_intersection_safe :
+    ¬ 0 + byzantineBound 0 < 2 * quorumThreshold 0 := by
+  native_decide
+
+/-- Two export sidecar hashes both clearing 80% quorum in the same nonempty
+active universe must have overlap larger than the standard fault bound. -/
+theorem export_hash_quorums_overlap_gt_byzantine
+    {n a b overlap : Nat}
+    (hPositive : 0 < n)
+    (hCardinality : a + b <= n + overlap)
+    (hA : quorumThreshold n <= a)
+    (hB : quorumThreshold n <= b) :
+    byzantineBound n < overlap := by
+  exact overlap_gt_fault_of_two_threshold_cohorts
+    hCardinality
+    hA
+    hB
+    (quorumThreshold_intersection_safe hPositive)
+
+/-- If the overlap between two quorum-clearing export hashes is split into
+faulty and honest validators, and at most `floor(n / 5)` validators in that
+overlap are faulty, then the overlap contains an honest validator. -/
+theorem export_hash_quorums_force_honest_overlap
+    {n a b overlap faultyOverlap honestOverlap : Nat}
+    (hPositive : 0 < n)
+    (hCardinality : a + b <= n + overlap)
+    (hA : quorumThreshold n <= a)
+    (hB : quorumThreshold n <= b)
+    (hSplit : overlap = faultyOverlap + honestOverlap)
+    (hFaulty : faultyOverlap <= byzantineBound n) :
+    0 < honestOverlap := by
+  have hOverlap :
+      byzantineBound n < overlap :=
+    export_hash_quorums_overlap_gt_byzantine
+      hPositive
+      hCardinality
+      hA
+      hB
+  omega
+
+/-- Export quorum intersection remains above the original-view Byzantine bound
+when nUNL shrinkage is within the protocol's ceil-25% cap. -/
+theorem export_quorum_intersection_safe_under_nunl_cap
+    {originalView effectiveView disabled : Nat}
+    (hEffective : effectiveView = originalView - disabled)
+    (hCap : disabled <= disabledCap originalView)
+    (hPositive : 0 < effectiveView) :
+    effectiveView + byzantineBound originalView <
+      2 * quorumThreshold effectiveView := by
+  have hCapBound :
+      disabled * 4 <= originalView + 3 :=
+    disabled_le_cap_mul_four_le hCap
+  have hQuorumBound :
+      4 * effectiveView <= 5 * quorumThreshold effectiveView :=
+    quorumThreshold_mul_five_ge_four_mul effectiveView
+  have hByzBound :
+      byzantineBound originalView * 5 <= originalView :=
+    byzantineBound_mul_five_le originalView
+  omega
+
+/-- Two export sidecar hashes both clearing 80% quorum in an nUNL-shrunk
+effective view must still overlap above the original-view Byzantine bound,
+provided the shrinkage stays within the protocol cap. -/
+theorem export_hash_quorums_overlap_gt_original_byzantine_under_nunl_cap
+    {originalView effectiveView disabled a b overlap : Nat}
+    (hEffective : effectiveView = originalView - disabled)
+    (hCap : disabled <= disabledCap originalView)
+    (hPositive : 0 < effectiveView)
+    (hCardinality : a + b <= effectiveView + overlap)
+    (hA : quorumThreshold effectiveView <= a)
+    (hB : quorumThreshold effectiveView <= b) :
+    byzantineBound originalView < overlap := by
+  exact overlap_gt_fault_of_two_threshold_cohorts
+    hCardinality
+    hA
+    hB
+    (export_quorum_intersection_safe_under_nunl_cap
+      hEffective
+      hCap
+      hPositive)
+
+/-- A Byzantine minority at the standard bound cannot veto export quorum:
+after removing `floor(n / 5)` validators, enough validators remain to meet the
+80% quorum threshold. -/
+theorem byzantineBound_cannot_veto_quorum (n : Nat) :
+    byzantineBound n + quorumThreshold n <= n := by
+  unfold byzantineBound quorumThreshold
+  omega
+
+/-- Equivalent no-veto form using subtraction. -/
+theorem quorumThreshold_le_universe_minus_byzantineBound (n : Nat) :
+    quorumThreshold n <= n - byzantineBound n := by
+  have hNoVeto := byzantineBound_cannot_veto_quorum n
+  omega
+
+/-- Concrete regression anchor: in a 5-validator active universe, two 80%
+export quorums overlap in at least three validators. -/
+theorem export_quorum_five_overlap_at_least_three
+    {a b overlap : Nat}
+    (hCardinality : a + b <= 5 + overlap)
+    (hA : quorumThreshold 5 <= a)
+    (hB : quorumThreshold 5 <= b) :
+    3 <= overlap := by
+  have hLower :
+      2 * quorumThreshold 5 - 5 <= overlap :=
+    two_export_quorums_overlap_lower_bound
+      hCardinality
+      hA
+      hB
+  have hExact : 2 * quorumThreshold 5 - 5 = 3 := by
+    native_decide
+  omega
+
+/-- Concrete regression anchor: in a 10-validator active universe, two 80%
+export quorums overlap in at least six validators. -/
+theorem export_quorum_ten_overlap_at_least_six
+    {a b overlap : Nat}
+    (hCardinality : a + b <= 10 + overlap)
+    (hA : quorumThreshold 10 <= a)
+    (hB : quorumThreshold 10 <= b) :
+    6 <= overlap := by
+  have hLower :
+      2 * quorumThreshold 10 - 10 <= overlap :=
+    two_export_quorums_overlap_lower_bound
+      hCardinality
+      hA
+      hB
+  have hExact : 2 * quorumThreshold 10 - 10 = 6 := by
+    native_decide
+  omega
+
+/-- Concrete regression anchor: in a 20-validator active universe, two 80%
+export quorums overlap in at least twelve validators. -/
+theorem export_quorum_twenty_overlap_at_least_twelve
+    {a b overlap : Nat}
+    (hCardinality : a + b <= 20 + overlap)
+    (hA : quorumThreshold 20 <= a)
+    (hB : quorumThreshold 20 <= b) :
+    12 <= overlap := by
+  have hLower :
+      2 * quorumThreshold 20 - 20 <= overlap :=
+    two_export_quorums_overlap_lower_bound
+      hCardinality
+      hA
+      hB
+  have hExact : 2 * quorumThreshold 20 - 20 = 12 := by
+    native_decide
+  omega
+
+/-- On exact multiples of five, two 80% export quorums overlap in at least
+`3 * k` validators. -/
+theorem export_quorum_five_mul_overlap_at_least_three_mul
+    {k a b overlap : Nat}
+    (hCardinality : a + b <= 5 * k + overlap)
+    (hA : quorumThreshold (5 * k) <= a)
+    (hB : quorumThreshold (5 * k) <= b) :
+    3 * k <= overlap := by
+  have hLower :
+      2 * quorumThreshold (5 * k) - 5 * k <= overlap :=
+    two_export_quorums_overlap_lower_bound
+      hCardinality
+      hA
+      hB
+  rw [quorumThreshold_five_mul] at hLower
+  omega
+
+/-- On exact multiples of five, quorum overlap strictly exceeds the standard
+fault bound by at least `2 * k`. For `k = 0` this is only a non-strict
+difference statement; strict safety is provided by
+`export_hash_quorums_overlap_gt_byzantine` for nonempty universes. -/
+theorem export_quorum_five_mul_overlap_margin
+    {k a b overlap : Nat}
+    (hCardinality : a + b <= 5 * k + overlap)
+    (hA : quorumThreshold (5 * k) <= a)
+    (hB : quorumThreshold (5 * k) <= b) :
+    byzantineBound (5 * k) + 2 * k <= overlap := by
+  have hOverlap :
+      3 * k <= overlap :=
+    export_quorum_five_mul_overlap_at_least_three_mul
+      hCardinality
+      hA
+      hB
+  rw [byzantineBound_five_mul]
+  omega
+
+end XahauConsensus

formal_verification/XahauConsensus/FFI.lean

@@ -0,0 +1,188 @@
+import XahauConsensus.Threshold
+import XahauConsensus.Invariants
+import XahauConsensus.NunlCap
+import XahauConsensus.SidecarAlignment
+import XahauConsensus.ViewUniverse
+import XahauConsensus.ExportQuorum
+import XahauConsensus.SixtyPercent
+
+namespace XahauConsensus
+
+/-! Scalar C ABI exports used by the optional C++ drift tests.
+
+These functions intentionally expose only plain integer formulas. The broader
+Lean project proves properties about these definitions; the C++ tests then
+check that selected production formulas and helper predicates still compute the
+same values.
+-/
+
+-- @@start ffi-scalar-export-surface
+@[export xahau_byzantine_bound]
+def xahauByzantineBound (count : UInt64) : UInt64 :=
+  (byzantineBound count.toNat).toUInt64
+
+@[export xahau_participant_threshold]
+def xahauParticipantThreshold (count : UInt64) : UInt64 :=
+  (participantThreshold count.toNat).toUInt64
+
+@[export xahau_quorum_threshold]
+def xahauQuorumThreshold (count : UInt64) : UInt64 :=
+  (quorumThreshold count.toNat).toUInt64
+
+@[export xahau_safe_quorum_threshold]
+def xahauSafeQuorumThreshold (count : UInt64) : UInt64 :=
+  (safeQuorumThreshold count.toNat).toUInt64
+
+@[export xahau_safe_participant_threshold]
+def xahauSafeParticipantThreshold (count : UInt64) : UInt64 :=
+  (safeParticipantThreshold count.toNat).toUInt64
+
+@[export xahau_entropy_gate_threshold_for_view]
+def xahauEntropyGateThresholdForView
+    (effectiveView originalView : UInt64) : UInt64 :=
+  (entropyGateThresholdForView effectiveView.toNat originalView.toNat).toUInt64
+
+def entropyTierCode : EntropyTier → UInt8
+  | EntropyTier.consensusFallback => 1
+  | EntropyTier.participantAligned => 2
+  | EntropyTier.validatorQuorum => 3
+
+@[export xahau_select_entropy_tier]
+def xahauSelectEntropyTier
+    (fromUNLReport participantCount effectiveView originalView : UInt64) : UInt8 :=
+  entropyTierCode <|
+    selectEntropyTier
+      (fromUNLReport != 0)
+      participantCount.toNat
+      effectiveView.toNat
+      originalView.toNat
+
+@[export xahau_aligned_participants]
+def xahauAlignedParticipants
+    (aligned localIsMember localPublished : UInt64) : UInt64 :=
+  (alignedParticipants
+      aligned.toNat
+      (localIsMember != 0)
+      (localPublished != 0)).toUInt64
+
+@[export xahau_quorum_aligned]
+def xahauQuorumAligned
+    (threshold aligned localIsMember localPublished : UInt64) : UInt8 :=
+  if quorumAligned
+      threshold.toNat
+      aligned.toNat
+      (localIsMember != 0)
+      (localPublished != 0) then
+    1
+  else
+    0
+
+@[export xahau_full_observation]
+def xahauFullObservation (peersSeen txConverged : UInt64) : UInt8 :=
+  if fullObservation peersSeen.toNat txConverged.toNat then 1 else 0
+
+@[export xahau_export_gate_proceed]
+def xahauExportGateProceed
+    (alignedParticipants quorumThreshold fullObservation : UInt64) : UInt8 :=
+  if (ExportGate.mk
+        alignedParticipants.toNat
+        quorumThreshold.toNat
+        (fullObservation != 0)).proceed then
+    1
+  else
+    0
+
+
+@[export xahau_strict_intersection_safe]
+def xahauStrictIntersectionSafe
+    (activeView byzantineUniverse threshold : UInt64) : UInt8 :=
+  if activeView.toNat + byzantineBound byzantineUniverse.toNat <
+      2 * threshold.toNat then
+    1
+  else
+    0
+
+@[export xahau_nonvacuous_strict_intersection_safe]
+def xahauNonvacuousStrictIntersectionSafe
+    (activeView byzantineUniverse threshold : UInt64) : UInt8 :=
+  if threshold.toNat <= activeView.toNat ∧
+      activeView.toNat + byzantineBound byzantineUniverse.toNat <
+        2 * threshold.toNat then
+    1
+  else
+    0
+
+@[export xahau_participant_band_nonempty]
+def xahauParticipantBandNonempty
+    (effectiveView originalView : UInt64) : UInt8 :=
+  if participantThreshold originalView.toNat < quorumThreshold effectiveView.toNat then
+    1
+  else
+    0
+
+@[export xahau_export_quorum_overlap_lower_bound]
+def xahauExportQuorumOverlapLowerBound (activeView : UInt64) : UInt64 :=
+  (2 * quorumThreshold activeView.toNat - activeView.toNat).toUInt64
+
+@[export xahau_export_quorum_safe_under_nunl_cap]
+def xahauExportQuorumSafeUnderNunlCap
+    (originalView effectiveView disabled : UInt64) : UInt8 :=
+  if effectiveView.toNat = originalView.toNat - disabled.toNat ∧
+      disabled.toNat <= disabledCap originalView.toNat ∧
+      0 < effectiveView.toNat ∧
+      effectiveView.toNat + byzantineBound originalView.toNat <
+        2 * quorumThreshold effectiveView.toNat then
+    1
+  else
+    0
+
+private def maskBit (mask : UInt64) (peer : Nat) : Bool :=
+  ((mask.toNat / (2 ^ peer)) % 2) == 1
+
+@[export xahau_active_aligned_count_mask]
+def xahauActiveAlignedCountMask
+    (count activeMask alignedMask : UInt64) : UInt64 :=
+  (activeAlignedCount
+      (maskBit activeMask)
+      (maskBit alignedMask)
+      count.toNat).toUInt64
+
+@[export xahau_quorum_aligned_mask]
+def xahauQuorumAlignedMask
+    (threshold count activeMask alignedMask localIsMember localPublished : UInt64) : UInt8 :=
+  let aligned :=
+    activeAlignedCount
+      (maskBit activeMask)
+      (maskBit alignedMask)
+      count.toNat
+  if quorumAligned
+      threshold.toNat
+      aligned
+      (localIsMember != 0)
+      (localPublished != 0) then
+    1
+  else
+    0
+
+@[export xahau_naive_sixty_percent_threshold]
+def xahauNaiveSixtyPercentThreshold (count : UInt64) : UInt64 :=
+  (naiveSixtyPercentThreshold count.toNat).toUInt64
+
+@[export xahau_naive_sixty_percent_is_safe]
+def xahauNaiveSixtyPercentIsSafe (count : UInt64) : UInt8 :=
+  if count.toNat + byzantineBound count.toNat <
+      2 * naiveSixtyPercentThreshold count.toNat then
+    1
+  else
+    0
+
+@[export xahau_disabled_cap]
+def xahauDisabledCap (originalView : UInt64) : UInt64 :=
+  (disabledCap originalView.toNat).toUInt64
+
+@[export xahau_effective_view]
+def xahauEffectiveView (originalView disabled : UInt64) : UInt64 :=
+  (effectiveView originalView.toNat disabled.toNat).toUInt64
+-- @@end ffi-scalar-export-surface
+
+end XahauConsensus

formal_verification/XahauConsensus/FinsetIntersection.lean

@@ -0,0 +1,88 @@
+import Mathlib.Data.Finset.Card
+import XahauConsensus.ExportQuorum
+import XahauConsensus.Intersection
+
+namespace XahauConsensus
+
+/-!
+Finite-set bridge for the quorum-intersection arithmetic.
+
+The arithmetic modules prove useful facts from the premise
+`a + b <= n + overlap`. This module discharges that premise for actual finite
+cohorts `A` and `B` that are both subsets of a common validator universe `U`.
+-/
+
+open Finset
+
+/-- Inclusion-exclusion bridge: two finite cohorts inside one universe satisfy
+the cardinality premise used by `Intersection.lean`. -/
+theorem finset_cardinality_bound
+    [DecidableEq α]
+    {U A B : Finset α}
+    (hA : A ⊆ U)
+    (hB : B ⊆ U) :
+    A.card + B.card <= U.card + (A ∩ B).card := by
+  have hUnionSubset : A ∪ B ⊆ U := by
+    intro x hx
+    rcases Finset.mem_union.mp hx with hxA | hxB
+    · exact hA hxA
+    · exact hB hxB
+  have hUnionCard : (A ∪ B).card <= U.card :=
+    Finset.card_le_card hUnionSubset
+  have hInclusion :
+      (A ∪ B).card + (A ∩ B).card = A.card + B.card :=
+    Finset.card_union_add_card_inter A B
+  omega
+
+/-- Set-level Tier-2 form: two participant-threshold cohorts in the same
+validator universe overlap above the Byzantine bound. -/
+theorem finset_participant_threshold_cohorts_overlap_gt_byzantine
+    [DecidableEq α]
+    {U A B : Finset α}
+    (hAUniverse : A ⊆ U)
+    (hBUniverse : B ⊆ U)
+    (hAThreshold : participantThreshold U.card <= A.card)
+    (hBThreshold : participantThreshold U.card <= B.card) :
+    byzantineBound U.card < (A ∩ B).card := by
+  exact participant_threshold_cohorts_overlap_gt_byzantine
+    (finset_cardinality_bound hAUniverse hBUniverse)
+    hAThreshold
+    hBThreshold
+
+/-- nUNL/set-level form: two original-view participant-threshold cohorts in a
+shrunk effective universe still overlap above the original Byzantine bound. -/
+theorem finset_participant_threshold_cohorts_overlap_gt_byzantine_under_shrink
+    [DecidableEq α]
+    {Original Effective A B : Finset α}
+    (hEffectiveSubset : Effective ⊆ Original)
+    (hAUniverse : A ⊆ Effective)
+    (hBUniverse : B ⊆ Effective)
+    (hAThreshold : participantThreshold Original.card <= A.card)
+    (hBThreshold : participantThreshold Original.card <= B.card) :
+    byzantineBound Original.card < (A ∩ B).card := by
+  have hShrink : Effective.card <= Original.card :=
+    Finset.card_le_card hEffectiveSubset
+  exact participant_threshold_cohorts_overlap_gt_byzantine_under_shrink
+    hShrink
+    (finset_cardinality_bound hAUniverse hBUniverse)
+    hAThreshold
+    hBThreshold
+
+/-- Set-level export form: two 80% export sidecar quorums in the same nonempty
+active universe overlap above the standard Byzantine bound. -/
+theorem finset_export_hash_quorums_overlap_gt_byzantine
+    [DecidableEq α]
+    {U A B : Finset α}
+    (hNonempty : 0 < U.card)
+    (hAUniverse : A ⊆ U)
+    (hBUniverse : B ⊆ U)
+    (hAThreshold : quorumThreshold U.card <= A.card)
+    (hBThreshold : quorumThreshold U.card <= B.card) :
+    byzantineBound U.card < (A ∩ B).card := by
+  exact export_hash_quorums_overlap_gt_byzantine
+    hNonempty
+    (finset_cardinality_bound hAUniverse hBUniverse)
+    hAThreshold
+    hBThreshold
+
+end XahauConsensus

formal_verification/XahauConsensus/HonestOverlap.lean

@@ -0,0 +1,70 @@
+import XahauConsensus.Intersection
+
+namespace XahauConsensus
+
+/-!
+Bridge from cardinality arithmetic to the consensus-language statement:
+if cohort overlap is larger than the maximum faulty overlap, then the overlap
+contains at least one honest validator.
+-/
+
+/-- If the overlap is larger than the number of faulty validators in it, then
+some honest validator remains in the overlap. -/
+theorem honest_overlap_exists
+    {overlap faultyInOverlap : Nat}
+    (hFaultyLtOverlap : faultyInOverlap < overlap) :
+    0 < overlap - faultyInOverlap := by
+  omega
+
+/-- If total faulty validators are bounded by `faultBound`, and the overlap is
+larger than `faultBound`, then the overlap contains an honest validator. -/
+theorem honest_overlap_exists_of_fault_bound
+    {overlap faultyInOverlap faultBound : Nat}
+    (hFaultyBound : faultyInOverlap <= faultBound)
+    (hOverlapGtFaultBound : faultBound < overlap) :
+    0 < overlap - faultyInOverlap := by
+  omega
+
+/-- Direct bridge from the abstract two-cohort intersection theorem: two
+threshold-sized cohorts under the strict safety inequality have honest overlap,
+provided faulty validators in the overlap are bounded by `f`.
+-/
+theorem honest_overlap_of_two_threshold_cohorts
+    {n a b overlap threshold faultBound faultyInOverlap : Nat}
+    (hCardinality : a + b <= n + overlap)
+    (hA : threshold <= a)
+    (hB : threshold <= b)
+    (hSafety : n + faultBound < 2 * threshold)
+    (hFaultyBound : faultyInOverlap <= faultBound) :
+    0 < overlap - faultyInOverlap := by
+  have hOverlapGtFaultBound :
+      faultBound < overlap :=
+    overlap_gt_fault_of_two_threshold_cohorts
+      hCardinality
+      hA
+      hB
+      hSafety
+  exact honest_overlap_exists_of_fault_bound
+    hFaultyBound
+    hOverlapGtFaultBound
+
+/-- Direct participant-threshold form: two Tier-2-sized cohorts in the same
+view have honest overlap under the `floor(n/5)` Byzantine bound. -/
+theorem honest_overlap_of_participant_threshold_cohorts
+    {count a b overlap faultyInOverlap : Nat}
+    (hCardinality : a + b <= count + overlap)
+    (hA : participantThreshold count <= a)
+    (hB : participantThreshold count <= b)
+    (hFaultyBound : faultyInOverlap <= byzantineBound count) :
+    0 < overlap - faultyInOverlap := by
+  have hOverlapGtBound :
+      byzantineBound count < overlap :=
+    participant_threshold_cohorts_overlap_gt_byzantine
+      hCardinality
+      hA
+      hB
+  exact honest_overlap_exists_of_fault_bound
+    hFaultyBound
+    hOverlapGtBound
+
+end XahauConsensus

formal_verification/XahauConsensus/Intersection.lean

@@ -0,0 +1,96 @@
+import XahauConsensus.Threshold
+
+namespace XahauConsensus
+
+/-!
+Abstract cardinality arithmetic for quorum intersection arguments.
+
+The variables are plain natural-number cardinalities:
+
+* `n`: universe size
+* `a`, `b`: cohort sizes
+* `o`: overlap size
+* `t`: quorum threshold
+* `f`: tolerated faulty overlap
+
+The shape `a + b <= n + o` captures the inclusion-exclusion upper bound
+without committing to a concrete `Finset` model.
+-/
+
+/-- If two threshold-sized cohorts fit in an `n`-sized universe only by
+overlapping by `o`, and `n + f < 2 * t`, then the overlap is larger than the
+fault bound `f`. -/
+theorem overlap_gt_fault_of_two_threshold_cohorts
+    {n a b o t f : Nat}
+    (hCardinality : a + b <= n + o)
+    (hA : t <= a)
+    (hB : t <= b)
+    (hSafety : n + f < 2 * t) :
+    f < o := by
+  omega
+
+/-- Reviewer-facing contrapositive form: if the overlap is no larger than the
+fault bound, then under the strict safety inequality the two cohorts cannot
+both meet threshold. -/
+theorem not_both_threshold_cohorts_of_overlap_le_fault
+    {n a b o t f : Nat}
+    (hOverlap : o <= f)
+    (hCardinality : a + b <= n + o)
+    (hSafety : n + f < 2 * t) :
+    ¬ (t <= a ∧ t <= b) := by
+  intro hBoth
+  have hStrict :
+      f < o :=
+    overlap_gt_fault_of_two_threshold_cohorts
+      hCardinality hBoth.1 hBoth.2 hSafety
+  omega
+
+/-- Equivalent disjunctive form of the reviewer fact: with insufficient
+overlap, at least one candidate cohort must be below threshold. -/
+theorem overlap_le_fault_forces_cohort_below_threshold
+    {n a b o t f : Nat}
+    (hOverlap : o <= f)
+    (hCardinality : a + b <= n + o)
+    (hSafety : n + f < 2 * t) :
+    a < t ∨ b < t := by
+  have hNotBoth :
+      ¬ (t <= a ∧ t <= b) :=
+    not_both_threshold_cohorts_of_overlap_le_fault
+      hOverlap hCardinality hSafety
+  omega
+
+/-- Direct Tier-2 form: two cohorts at the participant threshold in the same
+original-view universe must overlap by more than the tolerated Byzantine bound.
+-/
+theorem participant_threshold_cohorts_overlap_gt_byzantine
+    {count a b overlap : Nat}
+    (hCardinality : a + b <= count + overlap)
+    (hA : participantThreshold count <= a)
+    (hB : participantThreshold count <= b) :
+    byzantineBound count < overlap := by
+  exact overlap_gt_fault_of_two_threshold_cohorts
+    hCardinality
+    hA
+    hB
+    (participantThreshold_intersection_safe count)
+
+/-- nUNL form: when the effective universe shrinks, the original-view
+participant threshold still forces overlap above the original Byzantine bound.
+-/
+theorem participant_threshold_cohorts_overlap_gt_byzantine_under_shrink
+    {originalView effectiveView a b overlap : Nat}
+    (hShrink : effectiveView <= originalView)
+    (hCardinality : a + b <= effectiveView + overlap)
+    (hA : participantThreshold originalView <= a)
+    (hB : participantThreshold originalView <= b) :
+    byzantineBound originalView < overlap := by
+  exact overlap_gt_fault_of_two_threshold_cohorts
+    hCardinality
+    hA
+    hB
+    (participantThreshold_safe_under_effective_shrink
+      originalView
+      effectiveView
+      hShrink)
+
+end XahauConsensus

formal_verification/XahauConsensus/Invariants.lean

@@ -0,0 +1,112 @@
+import XahauConsensus.Threshold
+import XahauConsensus.EntropySelector
+import XahauConsensus.ExportGate
+
+namespace XahauConsensus
+
+/-!
+Small cross-module invariants that state the design contract in one place.
+
+These do not verify C++ directly. They pin the consensus arguments that the C++
+is intended to implement.
+-/
+
+/-- Same-count band fact: with both thresholds computed from one view size,
+Tier 2 is never stricter than validator quorum. Production nUNL rounds use
+cross-view thresholds instead; see `entropyGateThresholdForView`. -/
+theorem same_count_tier2_not_stricter_than_validator_quorum (count : Nat) :
+    safeParticipantThreshold count <= safeQuorumThreshold count :=
+  safeParticipantThreshold_le_safeQuorumThreshold count
+
+/-- Same-view shorthand: the live entropy gate is the weaker of Tier 2 and
+validator quorum, so it is never above validator quorum. -/
+def entropyGateThresholdModel (count : Nat) : Nat :=
+  min (safeQuorumThreshold count) (safeParticipantThreshold count)
+
+theorem entropy_gate_le_validator_quorum (count : Nat) :
+    entropyGateThresholdModel count <= safeQuorumThreshold count := by
+  unfold entropyGateThresholdModel
+  exact Nat.min_le_left _ _
+
+theorem entropy_gate_le_participant_threshold (count : Nat) :
+    entropyGateThresholdModel count <= safeParticipantThreshold count := by
+  unfold entropyGateThresholdModel
+  exact Nat.min_le_right _ _
+
+/-- Production shape: validator quorum is over the effective post-nUNL view,
+while Tier 2 is over the original pre-nUNL view. -/
+def entropyGateThresholdForView (effectiveView originalView : Nat) : Nat :=
+  min (safeQuorumThreshold effectiveView) (safeParticipantThreshold originalView)
+
+theorem entropy_gate_for_view_le_validator_quorum
+    (effectiveView originalView : Nat) :
+    entropyGateThresholdForView effectiveView originalView <=
+      safeQuorumThreshold effectiveView := by
+  unfold entropyGateThresholdForView
+  exact Nat.min_le_left _ _
+
+theorem entropy_gate_for_view_le_participant_threshold
+    (effectiveView originalView : Nat) :
+    entropyGateThresholdForView effectiveView originalView <=
+      safeParticipantThreshold originalView := by
+  unfold entropyGateThresholdForView
+  exact Nat.min_le_right _ _
+
+/-- The entropy gate is exactly the selector's non-fallback boundary: reaching
+the lower of the validator-quorum and participant-aligned thresholds is enough
+to select a non-fallback tier, and below it the selector falls back. -/
+theorem selectEntropyTier_nonfallback_iff_entropy_gate
+    (participantCount effectiveView originalView : Nat) :
+    selectEntropyTier true participantCount effectiveView originalView ≠
+        EntropyTier.consensusFallback ↔
+      entropyGateThresholdForView effectiveView originalView <=
+        participantCount := by
+  unfold selectEntropyTier entropyGateThresholdForView
+  by_cases hQuorum : safeQuorumThreshold effectiveView <= participantCount
+  · constructor
+    · intro _
+      exact Nat.le_trans (Nat.min_le_left _ _) hQuorum
+    · intro _
+      simp [hQuorum]
+  · by_cases hParticipant :
+      safeParticipantThreshold originalView <= participantCount
+    · constructor
+      · intro _
+        exact Nat.le_trans (Nat.min_le_right _ _) hParticipant
+      · intro _
+        simp [hQuorum, hParticipant]
+    · constructor
+      · intro hNonfallback
+        simp [hQuorum, hParticipant] at hNonfallback
+      · intro hGate
+        have hBelowQuorum :
+            participantCount < safeQuorumThreshold effectiveView :=
+          Nat.lt_of_not_ge hQuorum
+        have hBelowParticipant :
+            participantCount < safeParticipantThreshold originalView :=
+          Nat.lt_of_not_ge hParticipant
+        have hBelowGate :
+            participantCount <
+              min (safeQuorumThreshold effectiveView)
+                (safeParticipantThreshold originalView) :=
+          (Nat.lt_min).mpr ⟨hBelowQuorum, hBelowParticipant⟩
+        exact False.elim (Nat.not_lt_of_ge hGate hBelowGate)
+
+/-- Until the view is ledger-anchored, entropy tier labeling fails closed. -/
+theorem non_unl_report_cannot_mint_nonfallback
+    (participantCount effectiveView originalView : Nat) :
+    selectEntropyTier false participantCount effectiveView originalView =
+      EntropyTier.consensusFallback :=
+  no_unl_report_selects_fallback participantCount effectiveView originalView
+
+/-- Export success is a quorum-alignment property, not a full-observation
+property. -/
+theorem export_success_independent_of_full_observation
+    (alignedParticipants quorumThreshold : Nat) :
+    (ExportGate.mk alignedParticipants quorumThreshold true).proceed =
+      (ExportGate.mk alignedParticipants quorumThreshold false).proceed :=
+  changing_fullObservation_alone_does_not_change_proceed
+    alignedParticipants
+    quorumThreshold
+
+end XahauConsensus

formal_verification/XahauConsensus/NunlCap.lean

@@ -0,0 +1,147 @@
+import XahauConsensus.Threshold
+
+namespace XahauConsensus
+
+/-!
+Arithmetic facts for nUNL-capped view shrinkage.
+
+The examples here intentionally use the original view for the participant
+floor and the effective post-nUNL view for validator quorum.  That is the
+cross-view comparison that matters when disabled validators collapse the space
+between the Tier-2 participant floor and the Tier-3 validator-quorum floor.
+-/
+
+/-- Integer ceiling division, defined defensively for `d = 0`. -/
+def ceilDiv (n d : Nat) : Nat :=
+  if d = 0 then 0 else (n + d - 1) / d
+
+/-- The protocol's ceil-25% nUNL disablement cap for an original validator view. -/
+def disabledCap (originalView : Nat) : Nat :=
+  ceilDiv originalView 4
+
+/-- The post-nUNL effective validator view after `disabled` validators drop. -/
+def effectiveView (originalView disabled : Nat) : Nat :=
+  originalView - disabled
+
+theorem ceilDiv_zero_right (n : Nat) : ceilDiv n 0 = 0 := by
+  simp [ceilDiv]
+
+theorem ceilDiv_four_eight : ceilDiv 8 4 = 2 := by
+  native_decide
+
+theorem ceilDiv_four_ten : ceilDiv 10 4 = 3 := by
+  native_decide
+
+theorem ceilDiv_four_twenty : ceilDiv 20 4 = 5 := by
+  native_decide
+
+theorem disabledCap_eight : disabledCap 8 = 2 := by
+  native_decide
+
+theorem disabledCap_ten : disabledCap 10 = 3 := by
+  native_decide
+
+theorem disabledCap_twenty : disabledCap 20 = 5 := by
+  native_decide
+
+theorem effectiveView_eight_at_disabledCap :
+    effectiveView 8 (disabledCap 8) = 6 := by
+  native_decide
+
+theorem effectiveView_ten_at_disabledCap :
+    effectiveView 10 (disabledCap 10) = 7 := by
+  native_decide
+
+theorem effectiveView_twenty_at_disabledCap :
+    effectiveView 20 (disabledCap 20) = 15 := by
+  native_decide
+
+/-- Original 8 with two disabled validators collapses the participant/quorum band. -/
+theorem band_collapse_original8_effective6 :
+    quorumThreshold 6 = participantThreshold 8 := by
+  native_decide
+
+theorem quorum_original8_effective6_meets_participant_floor :
+    participantThreshold 8 <= quorumThreshold 6 := by
+  native_decide
+
+/-- Original 10 with two disabled validators collapses the participant/quorum band. -/
+theorem band_collapse_original10_effective8 :
+    quorumThreshold 8 = participantThreshold 10 := by
+  native_decide
+
+theorem quorum_original10_effective8_meets_participant_floor :
+    participantThreshold 10 <= quorumThreshold 8 := by
+  native_decide
+
+/-- Original 10 at the full ceil-25% cap leaves effective view 7, below the participant floor. -/
+theorem quorum_original10_effective7_below_participant_floor :
+    quorumThreshold 7 < participantThreshold 10 := by
+  native_decide
+
+theorem max_cap_original10_below_participant_floor :
+    quorumThreshold (effectiveView 10 (disabledCap 10)) <
+      participantThreshold 10 := by
+  native_decide
+
+/-- At original 20, the full ceil-25% cap leaves effective view 15, which is too small. -/
+theorem quorum_original20_effective15_below_participant_floor :
+    quorumThreshold 15 < participantThreshold 20 := by
+  native_decide
+
+theorem quorum_original20_effective15_does_not_meet_participant_floor :
+    ¬ participantThreshold 20 <= quorumThreshold 15 := by
+  native_decide
+
+/-- Original 20 with four disabled validators collapses the participant/quorum band. -/
+theorem band_collapse_original20_effective16 :
+    quorumThreshold 16 = participantThreshold 20 := by
+  native_decide
+
+theorem quorum_original20_effective16_meets_participant_floor :
+    participantThreshold 20 <= quorumThreshold 16 := by
+  native_decide
+
+/-- The ceil-25% cap does not by itself guarantee collapse at size 20. -/
+theorem max_cap_original20_below_participant_floor :
+    quorumThreshold (effectiveView 20 (disabledCap 20)) <
+      participantThreshold 20 := by
+  native_decide
+
+/--
+General cross-view comparison: an effective-view quorum satisfies the
+original-view participant floor whenever that quorum clears the original
+intersection boundary.
+-/
+theorem quorumThreshold_meets_participantThreshold_of_intersection_premise
+    {originalView effectiveView : Nat}
+    (h :
+      originalView + byzantineBound originalView <
+        2 * quorumThreshold effectiveView) :
+    participantThreshold originalView <= quorumThreshold effectiveView := by
+  exact participantThreshold_minimal originalView (quorumThreshold effectiveView) h
+
+/--
+Once the effective-view quorum threshold meets the original-view participant
+floor, any validator count meeting validator quorum also meets the participant
+floor anchored to the original view.
+-/
+theorem validators_meet_participant_floor_of_meet_quorum
+    {originalView effectiveView validators : Nat}
+    (hBand : participantThreshold originalView <= quorumThreshold effectiveView)
+    (hQuorum : quorumThreshold effectiveView <= validators) :
+    participantThreshold originalView <= validators :=
+  Nat.le_trans hBand hQuorum
+
+/-- If cross-view quorum is no higher than the participant floor, the in-between band is empty. -/
+theorem cross_view_participant_band_empty
+    {originalView effectiveView : Nat}
+    (hCollapse : quorumThreshold effectiveView <= participantThreshold originalView) :
+    ¬ ∃ participants,
+      participantThreshold originalView <= participants ∧
+        participants < quorumThreshold effectiveView := by
+  intro hExists
+  rcases hExists with ⟨participants, hParticipant, hBelowQuorum⟩
+  omega
+
+end XahauConsensus

formal_verification/XahauConsensus/SelectorDeterminism.lean

@@ -0,0 +1,64 @@
+import XahauConsensus.EntropySelector
+
+namespace XahauConsensus
+
+/-- A minimal digest model: the payload is opaque to the selector, while the
+label is the entropy tier chosen from the consensus metadata. -/
+structure LabeledDigest (α : Type) where
+  payload : α
+  label : EntropyTier
+  deriving Repr
+
+def labelDigest
+    (fromUNLReport : Bool)
+    (participantCount effectiveView originalView : Nat)
+    (payload : α) : LabeledDigest α :=
+  { payload
+    label :=
+      selectEntropyTier
+        fromUNLReport
+        participantCount
+        effectiveView
+        originalView }
+
+/-- The digest payload itself does not affect the selected tier. The label is
+entirely determined by the consensus metadata. -/
+theorem payload_does_not_affect_tier
+    {α : Type}
+    {payloadA payloadB : α}
+    (fromUNLReport : Bool)
+    (participantCount effectiveView originalView : Nat) :
+    (labelDigest
+        fromUNLReport
+        participantCount
+        effectiveView
+        originalView
+        payloadA).label =
+      (labelDigest
+        fromUNLReport
+        participantCount
+        effectiveView
+        originalView
+        payloadB).label := by
+  rfl
+
+/-- Without a UNLReport anchor the same count and views can receive a different
+label. -/
+theorem label_can_differ_when_fromUNLReport_differs :
+    (labelDigest true 8 10 10 0).label ≠
+      (labelDigest false 8 10 10 0).label := by
+  native_decide
+
+/-- Changing the effective validator view can change the digest label. -/
+theorem label_can_differ_when_effective_view_differs :
+    (labelDigest true 7 8 10 0).label ≠
+      (labelDigest true 7 10 10 0).label := by
+  native_decide
+
+/-- Changing the original validator view can change the digest label. -/
+theorem label_can_differ_when_original_view_differs :
+    (labelDigest true 6 10 8 0).label ≠
+      (labelDigest true 6 10 10 0).label := by
+  native_decide
+
+end XahauConsensus

formal_verification/XahauConsensus/SidecarAlignment.lean

@@ -0,0 +1,241 @@
+namespace XahauConsensus
+
+/-- Count a local boolean contribution as the `Nat` value used in threshold
+comparisons. -/
+def localPublishedCount (localPublished : Bool) : Nat :=
+  if localPublished then 1 else 0
+
+/-- The proof-level participant count behind sidecar alignment.
+
+`aligned` is the count of aligned remote active-view participants; a local
+publication contributes one more participant. -/
+def alignedParticipants
+    (aligned : Nat)
+    (localIsMember localPublished : Bool) : Nat :=
+  aligned + localPublishedCount (localIsMember && localPublished)
+
+/-- Sidecar quorum predicate, kept boolean to mirror the implementation check. -/
+def quorumAligned
+    (threshold aligned : Nat)
+    (localIsMember localPublished : Bool) : Bool :=
+  decide (threshold <= alignedParticipants aligned localIsMember localPublished)
+
+/-- Full sidecar observation means every converged transaction has been seen. -/
+def fullObservation (peersSeen txConverged : Nat) : Bool :=
+  peersSeen == txConverged
+
+/-- Count aligned peers from a finite peer prefix, filtering through the active
+view before any alignment bit contributes. -/
+def activeAlignedCount
+    (inActiveView peerAligned : Nat → Bool) : Nat → Nat
+  | 0 => 0
+  | peer + 1 =>
+      activeAlignedCount inActiveView peerAligned peer +
+        localPublishedCount (inActiveView peer && peerAligned peer)
+
+theorem localPublishedCount_true :
+    localPublishedCount true = 1 := by
+  rfl
+
+theorem localPublishedCount_false :
+    localPublishedCount false = 0 := by
+  rfl
+
+theorem localPublishedCount_le_one (published : Bool) :
+    localPublishedCount published <= 1 := by
+  cases published <;> simp [localPublishedCount]
+
+/-- Core participant-count equation: aligned remotes plus the local published
+contribution. -/
+theorem alignedParticipants_eq_aligned_plus_localPublished
+    (aligned : Nat) (localIsMember localPublished : Bool) :
+    alignedParticipants aligned localIsMember localPublished =
+      aligned + localPublishedCount (localIsMember && localPublished) := by
+  rfl
+
+/-- A non-active local node cannot pad the participant count. -/
+theorem alignedParticipants_local_nonmember
+    (aligned : Nat) (localPublished : Bool) :
+    alignedParticipants aligned false localPublished = aligned := by
+  cases localPublished <;> rfl
+
+/-- An active local node contributes exactly when it published the sidecar hash. -/
+theorem alignedParticipants_local_member
+    (aligned : Nat) (localPublished : Bool) :
+    alignedParticipants aligned true localPublished =
+      aligned + localPublishedCount localPublished := by
+  cases localPublished <;> rfl
+
+/-- The local node can add at most one participant to the remote aligned count. -/
+theorem alignedParticipants_le_aligned_succ
+    (aligned : Nat) (localIsMember localPublished : Bool) :
+    alignedParticipants aligned localIsMember localPublished <= aligned + 1 := by
+  cases localIsMember <;> cases localPublished <;>
+    simp [alignedParticipants, localPublishedCount]
+
+/-- The boolean quorum predicate is exactly the threshold comparison over
+`alignedParticipants`. -/
+theorem quorumAligned_iff_threshold_le_alignedParticipants
+    (threshold aligned : Nat) (localIsMember localPublished : Bool) :
+    quorumAligned threshold aligned localIsMember localPublished = true ↔
+      threshold <= alignedParticipants aligned localIsMember localPublished := by
+  unfold quorumAligned
+  simp
+
+/-- The boolean full-observation predicate is exactly equality of the observed
+and converged counts. -/
+theorem fullObservation_iff_peersSeen_eq_txConverged
+    (peersSeen txConverged : Nat) :
+    fullObservation peersSeen txConverged = true ↔
+      peersSeen = txConverged := by
+  unfold fullObservation
+  simp
+
+/-- A peer outside the active view contributes zero, even if its sidecar
+alignment bit is set. -/
+theorem activeAlignedCount_succ_nonmember
+    {inActiveView peerAligned : Nat → Bool} {peer : Nat}
+    (hNonmember : inActiveView peer = false) :
+    activeAlignedCount inActiveView peerAligned (peer + 1) =
+      activeAlignedCount inActiveView peerAligned peer := by
+  simp [activeAlignedCount, hNonmember, localPublishedCount]
+
+/-- A prefix of `n` peer positions can contribute at most `n` aligned active
+remote participants. -/
+theorem activeAlignedCount_le_prefix
+    (inActiveView peerAligned : Nat → Bool) (n : Nat) :
+    activeAlignedCount inActiveView peerAligned n <= n := by
+  induction n with
+  | zero =>
+      simp [activeAlignedCount]
+  | succ n ih =>
+      cases hAligned : inActiveView n && peerAligned n
+      · simp [activeAlignedCount, hAligned, localPublishedCount]
+        exact Nat.le_trans ih (Nat.le_succ n)
+      · simp [activeAlignedCount, hAligned, localPublishedCount]
+        exact ih
+
+/-- With the optional local contribution included, the participant count is
+bounded by the inspected remote prefix plus one. -/
+theorem alignedParticipants_le_prefix_succ
+    (inActiveView peerAligned : Nat → Bool)
+    (n : Nat)
+    (localIsMember localPublished : Bool) :
+    alignedParticipants
+        (activeAlignedCount inActiveView peerAligned n)
+        localIsMember
+        localPublished <= n + 1 := by
+  have hRemote := activeAlignedCount_le_prefix inActiveView peerAligned n
+  cases localIsMember <;> cases localPublished <;>
+    simp [alignedParticipants, localPublishedCount]
+  · exact Nat.le_trans hRemote (Nat.le_succ n)
+  · exact Nat.le_trans hRemote (Nat.le_succ n)
+  · exact Nat.le_trans hRemote (Nat.le_succ n)
+  · exact hRemote
+
+/-- Adding a nonmember peer to the inspected prefix cannot increase
+`alignedParticipants`. -/
+theorem alignedParticipants_succ_nonmember
+    {inActiveView peerAligned : Nat → Bool} {peer : Nat}
+    (localIsMember localPublished : Bool)
+    (hNonmember : inActiveView peer = false) :
+    alignedParticipants
+        (activeAlignedCount inActiveView peerAligned (peer + 1))
+        localIsMember
+        localPublished =
+      alignedParticipants
+        (activeAlignedCount inActiveView peerAligned peer)
+        localIsMember
+        localPublished := by
+  simp [alignedParticipants, activeAlignedCount_succ_nonmember hNonmember]
+
+/-- Consequently, a nonmember peer cannot change the quorum-aligned result. -/
+theorem quorumAligned_succ_nonmember
+    {inActiveView peerAligned : Nat → Bool} {peer threshold : Nat}
+    (localIsMember localPublished : Bool)
+    (hNonmember : inActiveView peer = false) :
+    quorumAligned threshold
+        (activeAlignedCount inActiveView peerAligned (peer + 1))
+        localIsMember
+        localPublished =
+      quorumAligned threshold
+        (activeAlignedCount inActiveView peerAligned peer)
+        localIsMember
+        localPublished := by
+  simp [
+    quorumAligned,
+    alignedParticipants_succ_nonmember
+      localIsMember
+      localPublished
+      hNonmember]
+
+/-- Active-view filtering: only member peers' alignment bits can affect the
+aligned remote count. -/
+theorem activeAlignedCount_ext_on_members
+    {n : Nat} {inActiveView alignedA alignedB : Nat → Bool}
+    (hSameOnMembers :
+      ∀ peer, peer < n → inActiveView peer = true →
+        alignedA peer = alignedB peer) :
+    activeAlignedCount inActiveView alignedA n =
+      activeAlignedCount inActiveView alignedB n := by
+  induction n with
+  | zero =>
+      rfl
+  | succ n ih =>
+      have hPrefix :
+          ∀ peer, peer < n → inActiveView peer = true →
+            alignedA peer = alignedB peer := by
+        intro peer hLt hMember
+        exact hSameOnMembers peer (Nat.lt_trans hLt (Nat.lt_succ_self n)) hMember
+      have hAt :
+          localPublishedCount (inActiveView n && alignedA n) =
+            localPublishedCount (inActiveView n && alignedB n) := by
+        cases hMember : inActiveView n
+        · simp [localPublishedCount]
+        · have hEq := hSameOnMembers n (Nat.lt_succ_self n) hMember
+          simp [hEq, localPublishedCount]
+      simp [activeAlignedCount, ih hPrefix, hAt]
+
+/-- Changing sidecar alignment reports for nonmembers cannot change the final
+participant count. -/
+theorem alignedParticipants_ext_on_members
+    {n : Nat} {inActiveView alignedA alignedB : Nat → Bool}
+    {localIsMember : Bool}
+    {localPublished : Bool}
+    (hSameOnMembers :
+      ∀ peer, peer < n → inActiveView peer = true →
+        alignedA peer = alignedB peer) :
+    alignedParticipants
+        (activeAlignedCount inActiveView alignedA n)
+        localIsMember
+        localPublished =
+      alignedParticipants
+        (activeAlignedCount inActiveView alignedB n)
+        localIsMember
+        localPublished := by
+  simp [
+    alignedParticipants,
+    activeAlignedCount_ext_on_members hSameOnMembers]
+
+/-- Changing sidecar alignment reports for nonmembers cannot turn quorum on or
+off. -/
+theorem quorumAligned_ext_on_members
+    {n threshold : Nat} {inActiveView alignedA alignedB : Nat → Bool}
+    {localIsMember : Bool}
+    {localPublished : Bool}
+    (hSameOnMembers :
+      ∀ peer, peer < n → inActiveView peer = true →
+        alignedA peer = alignedB peer) :
+    quorumAligned threshold
+        (activeAlignedCount inActiveView alignedA n)
+        localIsMember
+        localPublished =
+      quorumAligned threshold
+        (activeAlignedCount inActiveView alignedB n)
+        localIsMember
+        localPublished := by
+  simp [
+    quorumAligned,
+    alignedParticipants_ext_on_members hSameOnMembers]
+
+end XahauConsensus

formal_verification/XahauConsensus/SixtyPercent.lean

@@ -0,0 +1,56 @@
+import XahauConsensus.Threshold
+
+namespace XahauConsensus
+
+/-!
+Review-oriented facts about the tempting `ceil(60%)` participant threshold.
+
+The live `participantThreshold` is one higher than naive 60% at exact
+multiples of five. That extra vote is what turns equality at the
+Byzantine-overlap boundary into strict intersection safety.
+-/
+
+/-- A naive `ceil(0.6 * count)` threshold. -/
+def naiveSixtyPercentThreshold (count : Nat) : Nat :=
+  (count * 60 + 99) / 100
+
+theorem naiveSixtyPercentThreshold_five_mul (k : Nat) :
+    naiveSixtyPercentThreshold (5 * k) = 3 * k := by
+  unfold naiveSixtyPercentThreshold
+  omega
+
+theorem participantThreshold_five_mul_eq_naiveSixtyPercentThreshold_succ
+    (k : Nat) :
+    participantThreshold (5 * k) =
+      naiveSixtyPercentThreshold (5 * k) + 1 := by
+  unfold participantThreshold byzantineBound naiveSixtyPercentThreshold
+  omega
+
+/-- At exact multiples of five, naive 60% only reaches the unsafe boundary. -/
+theorem naiveSixtyPercentThreshold_five_mul_hits_intersection_boundary
+    (k : Nat) :
+    2 * naiveSixtyPercentThreshold (5 * k) =
+      5 * k + byzantineBound (5 * k) := by
+  unfold naiveSixtyPercentThreshold byzantineBound
+  omega
+
+theorem naiveSixtyPercentThreshold_five_mul_not_intersection_safe
+    (k : Nat) :
+    ¬ 5 * k + byzantineBound (5 * k) <
+      2 * naiveSixtyPercentThreshold (5 * k) := by
+  rw [naiveSixtyPercentThreshold_five_mul_hits_intersection_boundary k]
+  omega
+
+theorem participantThreshold_five_mul_intersection_safe (k : Nat) :
+    5 * k + byzantineBound (5 * k) <
+      2 * participantThreshold (5 * k) := by
+  exact participantThreshold_intersection_safe (5 * k)
+
+/-- At exact multiples of five, the live threshold clears the boundary by two. -/
+theorem participantThreshold_five_mul_intersection_margin (k : Nat) :
+    2 * participantThreshold (5 * k) =
+      (5 * k + byzantineBound (5 * k)) + 2 := by
+  unfold participantThreshold byzantineBound
+  omega
+
+end XahauConsensus

formal_verification/XahauConsensus/Threshold.lean

@@ -0,0 +1,124 @@
+namespace XahauConsensus
+
+/-- C++: `count / 5`, the conservative Byzantine bound used by
+`calculateParticipantThreshold`. -/
+def byzantineBound (count : Nat) : Nat :=
+  count / 5
+
+/-- C++: `calculateParticipantThreshold(count)`.
+
+This is the smallest integer `t` satisfying `2 * t > count + floor(count / 5)`.
+-/
+def participantThreshold (count : Nat) : Nat :=
+  (count + byzantineBound count) / 2 + 1
+
+/-- C++: `calculateQuorumThreshold(count)`, i.e. `ceil(0.8 * count)`. -/
+def quorumThreshold (count : Nat) : Nat :=
+  (count * 80 + 99) / 100
+
+/-- C++: `ConsensusExtensions::quorumThreshold()`.
+
+The raw formula gives `0` for an empty view, but the live consensus-extension
+gate requires at least one aligned participant for safety.
+-/
+def safeQuorumThreshold (count : Nat) : Nat :=
+  if count = 0 then 1 else quorumThreshold count
+
+/-- C++: `ConsensusExtensions::tier2Threshold()`.
+
+`participantThreshold 0` already returns `1`; this wrapper makes the
+zero-view safety rule explicit and mirrors the C++ method shape.
+-/
+def safeParticipantThreshold (count : Nat) : Nat :=
+  if count = 0 then 1 else participantThreshold count
+
+/-- The Tier-2 threshold strictly exceeds the Byzantine-overlap boundary.
+
+This is the load-bearing equivocation invariant behind participant-aligned
+entropy: two cohorts of this size in a `count`-sized universe overlap in more
+than `floor(count / 5)` validators.
+-/
+theorem participantThreshold_intersection_safe (count : Nat) :
+    count + byzantineBound count < 2 * participantThreshold count := by
+  unfold participantThreshold byzantineBound
+  omega
+
+/-- Anchoring the Tier-2 threshold to the original pre-nUNL view remains safe
+when the effective post-nUNL view shrinks.
+
+This is the arithmetic reason `originalViewSize` is the right denominator:
+smaller effective universes only increase the intersection margin.
+-/
+theorem participantThreshold_safe_under_effective_shrink
+    (originalView effectiveView : Nat)
+    (hShrink : effectiveView <= originalView) :
+    effectiveView + byzantineBound originalView <
+      2 * participantThreshold originalView := by
+  have hSafe := participantThreshold_intersection_safe originalView
+  omega
+
+/-- Concrete regression example: if `originalView = 10` and `effectiveView = 8`,
+using the effective view's participant threshold (`5`) leaves the overlap equal
+to the original-view Byzantine bound (`2`), not strictly greater than it.
+
+This is why the C++ must not replace `originalViewSize` with `size()` for the
+Tier-2 floor.
+-/
+theorem effective_threshold_regression_hits_boundary_example :
+    2 * participantThreshold 8 <= 8 + byzantineBound 10 := by
+  native_decide
+
+theorem threshold_minimal_for_boundary (boundary threshold : Nat) :
+    boundary < 2 * threshold → boundary / 2 + 1 <= threshold := by
+  omega
+
+theorem below_threshold_not_safe_for_boundary (boundary threshold : Nat) :
+    threshold < boundary / 2 + 1 → 2 * threshold <= boundary := by
+  omega
+
+/-- `participantThreshold` is the smallest threshold satisfying the strict
+intersection-safety inequality. -/
+theorem participantThreshold_minimal (count threshold : Nat) :
+    count + byzantineBound count < 2 * threshold →
+      participantThreshold count <= threshold := by
+  intro hSafe
+  unfold participantThreshold
+  exact threshold_minimal_for_boundary
+    (count + byzantineBound count)
+    threshold
+    hSafe
+
+/-- Anything below `participantThreshold` fails the strict intersection-safety
+inequality. -/
+theorem below_participantThreshold_not_safe (count threshold : Nat) :
+    threshold < participantThreshold count →
+      2 * threshold <= count + byzantineBound count := by
+  intro hBelow
+  unfold participantThreshold at hBelow
+  exact below_threshold_not_safe_for_boundary
+    (count + byzantineBound count)
+    threshold
+    hBelow
+
+/-- The participant threshold never exceeds the 80% validator-quorum threshold.
+
+This is useful because Tier 2 should form a band below Tier 3, not a stricter
+condition than validator quorum.
+-/
+theorem participantThreshold_le_quorumThreshold (count : Nat) :
+    0 < count → participantThreshold count <= quorumThreshold count := by
+  intro hCount
+  unfold participantThreshold quorumThreshold byzantineBound
+  omega
+
+/-- With the live safety wrappers, the participant threshold never exceeds the
+validator-quorum threshold, including the empty-view edge case. -/
+theorem safeParticipantThreshold_le_safeQuorumThreshold (count : Nat) :
+    safeParticipantThreshold count <= safeQuorumThreshold count := by
+  unfold safeParticipantThreshold safeQuorumThreshold
+  by_cases hZero : count = 0
+  · simp [hZero]
+  · have hPositive : 0 < count := Nat.pos_of_ne_zero hZero
+    simp [hZero, participantThreshold_le_quorumThreshold count hPositive]
+
+end XahauConsensus

formal_verification/XahauConsensus/ThresholdFacts.lean

@@ -0,0 +1,223 @@
+import XahauConsensus.Threshold
+
+namespace XahauConsensus
+
+/-!
+Additional arithmetic facts about the Xahau consensus thresholds.
+
+These lemmas are deliberately small and review-oriented: they expose concrete
+edge cases, exact multiples-of-five behavior, participant/quorum band facts,
+and monotonicity of the threshold functions.
+-/
+
+theorem byzantineBound_zero : byzantineBound 0 = 0 := by
+  native_decide
+
+theorem participantThreshold_zero : participantThreshold 0 = 1 := by
+  native_decide
+
+theorem quorumThreshold_zero : quorumThreshold 0 = 0 := by
+  native_decide
+
+theorem safeQuorumThreshold_zero : safeQuorumThreshold 0 = 1 := by
+  native_decide
+
+theorem safeParticipantThreshold_zero : safeParticipantThreshold 0 = 1 := by
+  native_decide
+
+theorem byzantineBound_one : byzantineBound 1 = 0 := by
+  native_decide
+
+theorem participantThreshold_one : participantThreshold 1 = 1 := by
+  native_decide
+
+theorem quorumThreshold_one : quorumThreshold 1 = 1 := by
+  native_decide
+
+theorem safeQuorumThreshold_one : safeQuorumThreshold 1 = 1 := by
+  native_decide
+
+theorem safeParticipantThreshold_one : safeParticipantThreshold 1 = 1 := by
+  native_decide
+
+theorem participantThreshold_two : participantThreshold 2 = 2 := by
+  native_decide
+
+theorem quorumThreshold_two : quorumThreshold 2 = 2 := by
+  native_decide
+
+theorem participantThreshold_three : participantThreshold 3 = 2 := by
+  native_decide
+
+theorem quorumThreshold_three : quorumThreshold 3 = 3 := by
+  native_decide
+
+theorem participantThreshold_four : participantThreshold 4 = 3 := by
+  native_decide
+
+theorem quorumThreshold_four : quorumThreshold 4 = 4 := by
+  native_decide
+
+theorem byzantineBound_five : byzantineBound 5 = 1 := by
+  native_decide
+
+theorem participantThreshold_five : participantThreshold 5 = 4 := by
+  native_decide
+
+theorem quorumThreshold_five : quorumThreshold 5 = 4 := by
+  native_decide
+
+theorem byzantineBound_ten : byzantineBound 10 = 2 := by
+  native_decide
+
+theorem participantThreshold_ten : participantThreshold 10 = 7 := by
+  native_decide
+
+theorem quorumThreshold_ten : quorumThreshold 10 = 8 := by
+  native_decide
+
+theorem byzantineBound_twenty : byzantineBound 20 = 4 := by
+  native_decide
+
+theorem participantThreshold_twenty : participantThreshold 20 = 13 := by
+  native_decide
+
+theorem quorumThreshold_twenty : quorumThreshold 20 = 16 := by
+  native_decide
+
+theorem byzantineBound_five_mul (k : Nat) :
+    byzantineBound (5 * k) = k := by
+  unfold byzantineBound
+  omega
+
+theorem participantThreshold_five_mul (k : Nat) :
+    participantThreshold (5 * k) = 3 * k + 1 := by
+  unfold participantThreshold byzantineBound
+  omega
+
+theorem quorumThreshold_five_mul (k : Nat) :
+    quorumThreshold (5 * k) = 4 * k := by
+  unfold quorumThreshold
+  omega
+
+/-- On exact multiples of five, the strict safety margin is exactly two. -/
+theorem participantThreshold_five_mul_margin (k : Nat) :
+    2 * participantThreshold (5 * k) =
+      (5 * k + byzantineBound (5 * k)) + 2 := by
+  rw [participantThreshold_five_mul, byzantineBound_five_mul]
+  omega
+
+/-- One below the multiple-of-five participant threshold reaches only equality
+with the unsafe boundary, so the strict safety inequality fails. -/
+theorem below_participantThreshold_five_mul_hits_boundary (k : Nat) :
+    2 * (participantThreshold (5 * k) - 1) =
+      5 * k + byzantineBound (5 * k) := by
+  rw [participantThreshold_five_mul, byzantineBound_five_mul]
+  omega
+
+theorem participantThreshold_five_mul_lt_quorumThreshold_five_mul
+    {k : Nat} (h : 1 < k) :
+    participantThreshold (5 * k) < quorumThreshold (5 * k) := by
+  rw [participantThreshold_five_mul, quorumThreshold_five_mul]
+  omega
+
+theorem participantThreshold_five_eq_quorumThreshold_five :
+    participantThreshold 5 = quorumThreshold 5 := by
+  native_decide
+
+theorem participantThreshold_ten_lt_quorumThreshold_ten :
+    participantThreshold 10 < quorumThreshold 10 := by
+  native_decide
+
+theorem participant_band_nonempty {count : Nat}
+    (h : participantThreshold count < quorumThreshold count) :
+    ∃ participants,
+      participantThreshold count <= participants ∧
+        participants < quorumThreshold count := by
+  exact ⟨participantThreshold count, Nat.le_refl _, h⟩
+
+theorem participant_band_empty {count : Nat}
+    (h : quorumThreshold count <= participantThreshold count) :
+    ¬ ∃ participants,
+      participantThreshold count <= participants ∧
+        participants < quorumThreshold count := by
+  intro hExists
+  rcases hExists with ⟨participants, hParticipant, hBelowQuorum⟩
+  omega
+
+theorem participant_band_empty_zero :
+    ¬ ∃ participants,
+      participantThreshold 0 <= participants ∧
+        participants < quorumThreshold 0 := by
+  apply participant_band_empty
+  native_decide
+
+theorem participant_band_empty_one :
+    ¬ ∃ participants,
+      participantThreshold 1 <= participants ∧
+        participants < quorumThreshold 1 := by
+  apply participant_band_empty
+  native_decide
+
+theorem participant_band_empty_two :
+    ¬ ∃ participants,
+      participantThreshold 2 <= participants ∧
+        participants < quorumThreshold 2 := by
+  apply participant_band_empty
+  native_decide
+
+theorem participant_band_empty_five :
+    ¬ ∃ participants,
+      participantThreshold 5 <= participants ∧
+        participants < quorumThreshold 5 := by
+  apply participant_band_empty
+  native_decide
+
+theorem participant_band_nonempty_three :
+    ∃ participants,
+      participantThreshold 3 <= participants ∧
+        participants < quorumThreshold 3 := by
+  apply participant_band_nonempty
+  native_decide
+
+theorem participant_band_nonempty_four :
+    ∃ participants,
+      participantThreshold 4 <= participants ∧
+        participants < quorumThreshold 4 := by
+  apply participant_band_nonempty
+  native_decide
+
+theorem participant_band_nonempty_ten :
+    ∃ participants,
+      participantThreshold 10 <= participants ∧
+        participants < quorumThreshold 10 := by
+  apply participant_band_nonempty
+  native_decide
+
+theorem participant_band_nonempty_five_mul {k : Nat} (h : 1 < k) :
+    ∃ participants,
+      participantThreshold (5 * k) <= participants ∧
+        participants < quorumThreshold (5 * k) := by
+  exact participant_band_nonempty
+    (participantThreshold_five_mul_lt_quorumThreshold_five_mul h)
+
+theorem byzantineBound_mono {a b : Nat} (h : a <= b) :
+    byzantineBound a <= byzantineBound b := by
+  unfold byzantineBound
+  exact Nat.div_le_div_right h
+
+theorem participantThreshold_mono {a b : Nat} (h : a <= b) :
+    participantThreshold a <= participantThreshold b := by
+  unfold participantThreshold
+  apply Nat.succ_le_succ
+  apply Nat.div_le_div_right
+  have hByzantine := byzantineBound_mono h
+  omega
+
+theorem quorumThreshold_mono {a b : Nat} (h : a <= b) :
+    quorumThreshold a <= quorumThreshold b := by
+  unfold quorumThreshold
+  apply Nat.div_le_div_right
+  omega
+
+end XahauConsensus

formal_verification/XahauConsensus/ViewUniverse.lean

@@ -0,0 +1,201 @@
+import XahauConsensus.ThresholdFacts
+
+namespace XahauConsensus
+
+/-!
+Concrete arithmetic examples for the distinction between the active effective
+view, the original pre-nUNL view, and any larger trusted counting universe.
+
+The safety shape is deliberately Nat-only: two cohorts of size `threshold` in
+an `activeView` overlap strictly beyond the Byzantine bound charged to
+`byzantineUniverse` when
+
+  `activeView + byzantineBound byzantineUniverse < 2 * threshold`.
+-/
+
+def strictIntersectionSafe
+    (activeView byzantineUniverse threshold : Nat) : Prop :=
+  activeView + byzantineBound byzantineUniverse < 2 * threshold
+
+/-- Strict intersection safety plus reachability of the threshold inside the
+active view. This separates "safe if it happens" from "possible to happen". -/
+def nonvacuousStrictIntersectionSafe
+    (activeView byzantineUniverse threshold : Nat) : Prop :=
+  threshold <= activeView ∧ strictIntersectionSafe activeView byzantineUniverse threshold
+
+/-- Cross-view Tier-2 band: participant floor is anchored to the original view,
+validator quorum to the effective view. -/
+def participantBandNonempty
+    (effectiveView originalView : Nat) : Prop :=
+  ∃ participants,
+    participantThreshold originalView <= participants ∧
+      participants < quorumThreshold effectiveView
+
+theorem participantBandNonempty_iff
+    (effectiveView originalView : Nat) :
+    participantBandNonempty effectiveView originalView ↔
+      participantThreshold originalView < quorumThreshold effectiveView := by
+  constructor
+  · intro h
+    rcases h with ⟨participants, hParticipant, hBelowQuorum⟩
+    omega
+  · intro h
+    exact ⟨participantThreshold originalView, Nat.le_refl _, h⟩
+
+/-- The original-view participant threshold remains safe when nUNL shrinks the
+active effective view. -/
+theorem original_threshold_safe_under_nunl_shrink
+    {originalView effectiveView : Nat}
+    (hShrink : effectiveView <= originalView) :
+    strictIntersectionSafe
+      effectiveView
+      originalView
+      (participantThreshold originalView) := by
+  unfold strictIntersectionSafe
+  exact participantThreshold_safe_under_effective_shrink
+    originalView
+    effectiveView
+    hShrink
+
+theorem original_threshold_nonvacuous_under_nunl_shrink
+    {originalView effectiveView : Nat}
+    (hShrink : effectiveView <= originalView)
+    (hReachable : participantThreshold originalView <= effectiveView) :
+    nonvacuousStrictIntersectionSafe
+      effectiveView
+      originalView
+      (participantThreshold originalView) := by
+  constructor
+  · exact hReachable
+  · exact original_threshold_safe_under_nunl_shrink hShrink
+
+/-- The original-view threshold is also safe if the Byzantine counting universe
+is no larger than the original view. -/
+theorem original_threshold_safe_for_no_larger_counting_universe
+    {originalView effectiveView countingUniverse : Nat}
+    (hShrink : effectiveView <= originalView)
+    (hCounting : countingUniverse <= originalView) :
+    strictIntersectionSafe
+      effectiveView
+      countingUniverse
+      (participantThreshold originalView) := by
+  unfold strictIntersectionSafe
+  have hOriginal :=
+    participantThreshold_safe_under_effective_shrink
+      originalView
+      effectiveView
+      hShrink
+  have hBound := byzantineBound_mono hCounting
+  omega
+
+/-- Any threshold at or below the overlap boundary is not strictly safe. -/
+theorem not_strictIntersectionSafe_of_threshold_le_boundary
+    {activeView byzantineUniverse threshold : Nat}
+    (hBoundary : 2 * threshold <= activeView + byzantineBound byzantineUniverse) :
+    ¬ strictIntersectionSafe activeView byzantineUniverse threshold := by
+  unfold strictIntersectionSafe
+  omega
+
+/-- If the effective-view threshold is below what the original Byzantine bound
+requires, it cannot prove strict intersection safety against that original
+bound. -/
+theorem effective_threshold_not_safe_against_original_bound
+    {originalView effectiveView : Nat}
+    (hBelow :
+      participantThreshold effectiveView <
+        (effectiveView + byzantineBound originalView) / 2 + 1) :
+    ¬ strictIntersectionSafe
+      effectiveView
+      originalView
+      (participantThreshold effectiveView) := by
+  apply not_strictIntersectionSafe_of_threshold_le_boundary
+  exact below_threshold_not_safe_for_boundary
+    (effectiveView + byzantineBound originalView)
+    (participantThreshold effectiveView)
+    hBelow
+
+/-- A larger trusted counting universe increases the Byzantine side of the
+boundary, eroding the strict-intersection margin. -/
+theorem original_boundary_le_trusted_superset_boundary
+    {originalView effectiveView trustedUniverse : Nat}
+    (hSuperset : originalView <= trustedUniverse) :
+    effectiveView + byzantineBound originalView <=
+      effectiveView + byzantineBound trustedUniverse := by
+  have hBound := byzantineBound_mono hSuperset
+  omega
+
+/-- Concrete nUNL example: `originalView = 10`, `effectiveView = 8`, and the
+original threshold still clears the original Byzantine bound. -/
+theorem original_ten_effective_eight_original_threshold_safe :
+    strictIntersectionSafe 8 10 (participantThreshold 10) := by
+  unfold strictIntersectionSafe
+  native_decide
+
+theorem original_ten_effective_eight_participant_band_empty :
+    ¬ participantBandNonempty 8 10 := by
+  rw [participantBandNonempty_iff]
+  native_decide
+
+theorem original_ten_effective_eight_original_threshold_reachable :
+    nonvacuousStrictIntersectionSafe 8 10 (participantThreshold 10) := by
+  apply original_threshold_nonvacuous_under_nunl_shrink
+  · native_decide
+  · native_decide
+
+/-- Concrete regression: for `originalView = 10` and `effectiveView = 8`, the
+effective threshold does not strictly clear the original Byzantine bound. -/
+theorem original_ten_effective_eight_effective_threshold_not_safe :
+    ¬ strictIntersectionSafe 8 10 (participantThreshold 8) := by
+  apply not_strictIntersectionSafe_of_threshold_le_boundary
+  native_decide
+
+/-- The same failure as a direct boundary comparison, useful when reviewing the
+raw arithmetic. -/
+theorem original_ten_effective_eight_effective_threshold_hits_boundary :
+    2 * participantThreshold 8 <= 8 + byzantineBound 10 := by
+  native_decide
+
+/-- Larger concrete nUNL example with the original threshold anchored at
+`20`. -/
+theorem original_twenty_effective_sixteen_original_threshold_safe :
+    strictIntersectionSafe 16 20 (participantThreshold 20) := by
+  unfold strictIntersectionSafe
+  native_decide
+
+theorem original_twenty_effective_sixteen_participant_band_empty :
+    ¬ participantBandNonempty 16 20 := by
+  rw [participantBandNonempty_iff]
+  native_decide
+
+theorem original_twenty_effective_fifteen_participant_band_empty :
+    ¬ participantBandNonempty 15 20 := by
+  rw [participantBandNonempty_iff]
+  native_decide
+
+theorem original_twenty_effective_fifteen_original_threshold_reachable :
+    nonvacuousStrictIntersectionSafe 15 20 (participantThreshold 20) := by
+  apply original_threshold_nonvacuous_under_nunl_shrink
+  · native_decide
+  · native_decide
+
+/-- With `originalView = 20` and `effectiveView = 16`, using the effective
+threshold again reaches the unsafe boundary. -/
+theorem original_twenty_effective_sixteen_effective_threshold_not_safe :
+    ¬ strictIntersectionSafe 16 20 (participantThreshold 16) := by
+  apply not_strictIntersectionSafe_of_threshold_le_boundary
+  native_decide
+
+/-- Counting Byzantine stake over a trusted universe of `20` instead of the
+original view of `10` erodes the margin all the way to equality. -/
+theorem trusted_superset_twenty_erodes_original_ten_margin_to_boundary :
+    2 * participantThreshold 10 = 10 + byzantineBound 20 := by
+  native_decide
+
+/-- The equality above means the original threshold for `10` is not strictly
+safe if Byzantine weight is counted over the larger trusted universe `20`. -/
+theorem trusted_superset_twenty_original_ten_threshold_not_safe :
+    ¬ strictIntersectionSafe 10 20 (participantThreshold 10) := by
+  apply not_strictIntersectionSafe_of_threshold_le_boundary
+  native_decide
+
+end XahauConsensus

formal_verification/lake-manifest.json

@@ -0,0 +1,96 @@
+{"version": "1.2.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover-community/mathlib4.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "fabf563a7c95a166b8d7b6efca11c8b4dc9d911f",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.31.0",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "63045536fe95024e6c18fc7b48e03f506701c5bc",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "5c7542ed018c78194f1e2b903eaf6a792b74c03d",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "24b0d9dc081c5423f8eec7e866c441e5184f29d9",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "e3cb2f741431ce31bf73549fb52316a57368b06f",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "f46324995fca5f0483b742e4eb4daec7f4ee50d2",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "fa08db58b30eb033edcdab331bba000827f9f785",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "92564e5770e4d09f2d86dfbf8ada1e9c715b384c",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.31.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
+ "name": "xahau_consensus",
+ "lakeDir": ".lake",
+ "fixedToolchain": false}

formal_verification/lakefile.toml

@@ -0,0 +1,11 @@
+name = "xahau_consensus"
+version = "0.1.0"
+defaultTargets = ["XahauConsensus"]
+
+[[require]]
+name = "mathlib"
+git = "https://github.com/leanprover-community/mathlib4.git"
+rev = "v4.31.0"
+
+[[lean_lib]]
+name = "XahauConsensus"

formal_verification/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.31.0

hook/error.h

@@ -47,5 +47,8 @@
 #define MEM_OVERLAP -43
 #define TOO_MANY_STATE_MODIFICATIONS -44
 #define TOO_MANY_NAMESPACES -45
+#define EXPORT_FAILURE -46
+#define TOO_MANY_EXPORTED_TXN -47
+#define TOO_LITTLE_ENTROPY -48
 #define HOOK_ERROR_CODES
 #endif //HOOK_ERROR_CODES

hook/extern.h

@@ -2,6 +2,9 @@
 // Generated using generate_extern.sh
 #include <stdint.h>
 #ifndef HOOK_EXTERN
+#ifdef __cplusplus
+extern "C" {
+#endif
 
 extern int32_t __attribute__((noduplicate))
 _g(uint32_t guard_id, uint32_t maxiter);
@@ -336,5 +339,43 @@ prepare(
     uint32_t read_ptr,
     uint32_t read_len);
 
+extern int64_t
+xport_reserve(uint32_t count);
+
+extern int64_t
+xport(
+    uint32_t write_ptr,
+    uint32_t write_len,
+    uint32_t read_ptr,
+    uint32_t read_len);
+
+extern int64_t
+xport_cancel(uint32_t ticket_seq);
+
+/*
+    Consensus entropy APIs.
+
+    min_tier is a fail-closed floor:
+      1 = consensus_fallback, 2 = participant_aligned, 3 = validator_quorum.
+    min_count is the minimum validator/reveal count the caller accepts.
+
+    If the most recent finalized entropy object does not satisfy both floors,
+    these APIs return TOO_LITTLE_ENTROPY. Open-ledger and simulate execution
+    are provisional previews over the entropy currently visible to the node;
+    final ordered ledger execution may see a different entropy object.
+*/
+extern int64_t
+dice(uint32_t sides, uint32_t min_tier, uint32_t min_count);
+
+extern int64_t
+random(
+    uint32_t write_ptr,
+    uint32_t write_len,
+    uint32_t min_tier,
+    uint32_t min_count);
+
+#ifdef __cplusplus
+}
+#endif
 #define HOOK_EXTERN
 #endif  // HOOK_EXTERN

hook/generate_error.sh

@@ -9,7 +9,7 @@ ENUM_FILE="$SCRIPT_DIR/../include/xrpl/hook/Enum.h"
 echo '// For documentation please see: https://xrpl-hooks.readme.io/reference/'
 echo '// Generated using generate_error.sh'
 echo '#ifndef HOOK_ERROR_CODES'
-sed -n '/enum hook_return_code/,/};/p' "$ENUM_FILE" |
+sed -n '/enum class hook_return_code/,/};/p' "$ENUM_FILE" |
     awk '
         function ltrim(s) { sub(/^[[:space:]]+/, "", s); return s }
         function rtrim(s) { sub(/[[:space:]]+$/, "", s); return s }
@@ -31,7 +31,7 @@ sed -n '/enum hook_return_code/,/};/p' "$ENUM_FILE" |
 
         {
             line = $0
-            if (line ~ /enum[[:space:]]+hook_return_code/)
+            if (line ~ /enum[[:space:]]+class[[:space:]]+hook_return_code/)
                 next
             if (line ~ /^[[:space:]]*\{/)
                 next

hook/generate_extern.sh

@@ -11,6 +11,9 @@ APPLY_HOOK="$SCRIPT_DIR/../include/xrpl/hook/hook_api.macro"
     echo '// Generated using generate_extern.sh'
     echo '#include <stdint.h>'
     echo '#ifndef HOOK_EXTERN'
+    echo '#ifdef __cplusplus'
+    echo 'extern "C" {'
+    echo '#endif'
     echo
     awk '
         function trim(s) {
@@ -38,6 +41,21 @@ APPLY_HOOK="$SCRIPT_DIR/../include/xrpl/hook/hook_api.macro"
                     # Insert __attribute__((noduplicate)) before _g
                     sub(/[[:space:]]+_g/, " __attribute__((noduplicate)) _g", line);
                 }
+
+                if (line ~ /[[:space:]]+dice[[:space:]]*\(/) {
+                    print "/*";
+                    print "    Consensus entropy APIs.";
+                    print "";
+                    print "    min_tier is a fail-closed floor:";
+                    print "      1 = consensus_fallback, 2 = participant_aligned, 3 = validator_quorum.";
+                    print "    min_count is the minimum validator/reveal count the caller accepts.";
+                    print "";
+                    print "    If the most recent finalized entropy object does not satisfy both floors,";
+                    print "    these APIs return TOO_LITTLE_ENTROPY. Open-ledger and simulate execution";
+                    print "    are provisional previews over the entropy currently visible to the node;";
+                    print "    final ordered ledger execution may see a different entropy object.";
+                    print "*/";
+                }
                 
                 # printf("\n");
                 
@@ -46,6 +64,9 @@ APPLY_HOOK="$SCRIPT_DIR/../include/xrpl/hook/hook_api.macro"
         }
     ' "$APPLY_HOOK"
 
+    echo '#ifdef __cplusplus'
+    echo '}'
+    echo '#endif'
     echo '#define HOOK_EXTERN'
     echo '#endif  // HOOK_EXTERN'
 } | (

hook/genesis/headers/macro.h

@@ -607,31 +607,37 @@ int out_len = 0;\
 #define PREPARE_PAYMENT_SIMPLE_SIZE 248U
 #endif
 
-#define PREPARE_PAYMENT_SIMPLE(buf_out_master, drops_amount_raw, to_address, dest_tag_raw, src_tag_raw)\
-    {\
-        uint8_t* buf_out = buf_out_master;\
-        uint8_t acc[20];\
-        uint64_t drops_amount = (drops_amount_raw);\
-        uint32_t dest_tag = (dest_tag_raw);\
-        uint32_t src_tag = (src_tag_raw);\
-        uint32_t cls = (uint32_t)ledger_seq();\
-        hook_account(SBUF(acc));\
-        _01_02_ENCODE_TT                   (buf_out, ttPAYMENT                      );      /* uint16  | size   3 */ \
-        _02_02_ENCODE_FLAGS                (buf_out, tfCANONICAL                    );      /* uint32  | size   5 */ \
-        _02_03_ENCODE_TAG_SRC              (buf_out, src_tag                        );      /* uint32  | size   5 */ \
-        _02_04_ENCODE_SEQUENCE             (buf_out, 0                              );      /* uint32  | size   5 */ \
-        _02_14_ENCODE_TAG_DST              (buf_out, dest_tag                       );      /* uint32  | size   5 */ \
-        _02_26_ENCODE_FLS                  (buf_out, cls + 1                        );      /* uint32  | size   6 */ \
-        _02_27_ENCODE_LLS                  (buf_out, cls + 5                        );      /* uint32  | size   6 */ \
-        _06_01_ENCODE_DROPS_AMOUNT         (buf_out, drops_amount                   );      /* amount  | size   9 */ \
-        uint8_t* fee_ptr = buf_out;\
-        _06_08_ENCODE_DROPS_FEE            (buf_out, 0                              );      /* amount  | size   9 */ \
-        _07_03_ENCODE_SIGNING_PUBKEY_NULL  (buf_out                                 );      /* pk      | size  35 */ \
-        _08_01_ENCODE_ACCOUNT_SRC          (buf_out, acc                            );      /* account | size  22 */ \
-        _08_03_ENCODE_ACCOUNT_DST          (buf_out, to_address                     );      /* account | size  22 */ \
-        int64_t edlen = etxn_details((uint32_t)buf_out, PREPARE_PAYMENT_SIMPLE_SIZE);       /* emitdet | size 1?? */ \
-        int64_t fee = etxn_fee_base(buf_out_master, PREPARE_PAYMENT_SIMPLE_SIZE);                                    \ 
-        _06_08_ENCODE_DROPS_FEE            (fee_ptr, fee                            );                               \
+#define PREPARE_PAYMENT_SIMPLE(                                              \
+    buf_out_master, drops_amount_raw, to_address, dest_tag_raw, src_tag_raw) \
+    {                                                                        \
+        uint8_t* buf_out = buf_out_master;                                   \
+        uint8_t acc[20];                                                     \
+        uint64_t drops_amount = (drops_amount_raw);                          \
+        uint32_t dest_tag = (dest_tag_raw);                                  \
+        uint32_t src_tag = (src_tag_raw);                                    \
+        uint32_t cls = (uint32_t)ledger_seq();                               \
+        hook_account(SBUF(acc));                                             \
+        _01_02_ENCODE_TT(buf_out, ttPAYMENT);      /* uint16  | size   3 */  \
+        _02_02_ENCODE_FLAGS(buf_out, tfCANONICAL); /* uint32  | size   5 */  \
+        _02_03_ENCODE_TAG_SRC(buf_out, src_tag);   /* uint32  | size   5 */  \
+        _02_04_ENCODE_SEQUENCE(buf_out, 0);        /* uint32  | size   5 */  \
+        _02_14_ENCODE_TAG_DST(buf_out, dest_tag);  /* uint32  | size   5 */  \
+        _02_26_ENCODE_FLS(buf_out, cls + 1);       /* uint32  | size   6 */  \
+        _02_27_ENCODE_LLS(buf_out, cls + 5);       /* uint32  | size   6 */  \
+        _06_01_ENCODE_DROPS_AMOUNT(                                          \
+            buf_out, drops_amount); /* amount  | size   9 */                 \
+        uint8_t* fee_ptr = buf_out;                                          \
+        _06_08_ENCODE_DROPS_FEE(buf_out, 0);        /* amount  | size   9 */ \
+        _07_03_ENCODE_SIGNING_PUBKEY_NULL(buf_out); /* pk      | size  35 */ \
+        _08_01_ENCODE_ACCOUNT_SRC(buf_out, acc);    /* account | size  22 */ \
+        _08_03_ENCODE_ACCOUNT_DST(                                           \
+            buf_out, to_address); /* account | size  22 */                   \
+        int64_t edlen = etxn_details(                                        \
+            (uint32_t)buf_out,                                               \
+            PREPARE_PAYMENT_SIMPLE_SIZE); /* emitdet | size 1?? */           \
+        int64_t fee =                                                        \
+            etxn_fee_base(buf_out_master, PREPARE_PAYMENT_SIMPLE_SIZE);      \
+        _06_08_ENCODE_DROPS_FEE(fee_ptr, fee);                               \
     }
 
 #ifdef HAS_CALLBACK
@@ -639,33 +645,35 @@ int out_len = 0;\
 #else
 #define PREPARE_PAYMENT_SIMPLE_TRUSTLINE_SIZE 287
 #endif
-#define PREPARE_PAYMENT_SIMPLE_TRUSTLINE(buf_out_master, tlamt, to_address, dest_tag_raw, src_tag_raw)\
-    {\
-        uint8_t* buf_out = buf_out_master;\
-        uint8_t acc[20];\
-        uint32_t dest_tag = (dest_tag_raw);\
-        uint32_t src_tag = (src_tag_raw);\
-        uint32_t cls = (uint32_t)ledger_seq();\
-        hook_account(SBUF(acc));\
-        _01_02_ENCODE_TT                   (buf_out, ttPAYMENT                      );      /* uint16  | size   3 */ \
-        _02_02_ENCODE_FLAGS                (buf_out, tfCANONICAL                    );      /* uint32  | size   5 */ \
-        _02_03_ENCODE_TAG_SRC              (buf_out, src_tag                        );      /* uint32  | size   5 */ \
-        _02_04_ENCODE_SEQUENCE             (buf_out, 0                              );      /* uint32  | size   5 */ \
-        _02_14_ENCODE_TAG_DST              (buf_out, dest_tag                       );      /* uint32  | size   5 */ \
-        _02_26_ENCODE_FLS                  (buf_out, cls + 1                        );      /* uint32  | size   6 */ \
-        _02_27_ENCODE_LLS                  (buf_out, cls + 5                        );      /* uint32  | size   6 */ \
-        _06_01_ENCODE_TL_AMOUNT            (buf_out, tlamt                          );      /* amount  | size  48 */ \
-        uint8_t* fee_ptr = buf_out;\
-        _06_08_ENCODE_DROPS_FEE            (buf_out, 0                              );      /* amount  | size   9 */ \
-        _07_03_ENCODE_SIGNING_PUBKEY_NULL  (buf_out                                 );      /* pk      | size  35 */ \
-        _08_01_ENCODE_ACCOUNT_SRC          (buf_out, acc                            );      /* account | size  22 */ \
-        _08_03_ENCODE_ACCOUNT_DST          (buf_out, to_address                     );      /* account | size  22 */ \
-        etxn_details((uint32_t)buf_out, PREPARE_PAYMENT_SIMPLE_TRUSTLINE_SIZE);             /* emitdet | size 1?? */  \
-        int64_t fee = etxn_fee_base(buf_out_master, PREPARE_PAYMENT_SIMPLE_TRUSTLINE_SIZE);                          \ 
-        _06_08_ENCODE_DROPS_FEE            (fee_ptr, fee                            );                               \
+#define PREPARE_PAYMENT_SIMPLE_TRUSTLINE(                                    \
+    buf_out_master, tlamt, to_address, dest_tag_raw, src_tag_raw)            \
+    {                                                                        \
+        uint8_t* buf_out = buf_out_master;                                   \
+        uint8_t acc[20];                                                     \
+        uint32_t dest_tag = (dest_tag_raw);                                  \
+        uint32_t src_tag = (src_tag_raw);                                    \
+        uint32_t cls = (uint32_t)ledger_seq();                               \
+        hook_account(SBUF(acc));                                             \
+        _01_02_ENCODE_TT(buf_out, ttPAYMENT);      /* uint16  | size   3 */  \
+        _02_02_ENCODE_FLAGS(buf_out, tfCANONICAL); /* uint32  | size   5 */  \
+        _02_03_ENCODE_TAG_SRC(buf_out, src_tag);   /* uint32  | size   5 */  \
+        _02_04_ENCODE_SEQUENCE(buf_out, 0);        /* uint32  | size   5 */  \
+        _02_14_ENCODE_TAG_DST(buf_out, dest_tag);  /* uint32  | size   5 */  \
+        _02_26_ENCODE_FLS(buf_out, cls + 1);       /* uint32  | size   6 */  \
+        _02_27_ENCODE_LLS(buf_out, cls + 5);       /* uint32  | size   6 */  \
+        _06_01_ENCODE_TL_AMOUNT(buf_out, tlamt);   /* amount  | size  48 */  \
+        uint8_t* fee_ptr = buf_out;                                          \
+        _06_08_ENCODE_DROPS_FEE(buf_out, 0);        /* amount  | size   9 */ \
+        _07_03_ENCODE_SIGNING_PUBKEY_NULL(buf_out); /* pk      | size  35 */ \
+        _08_01_ENCODE_ACCOUNT_SRC(buf_out, acc);    /* account | size  22 */ \
+        _08_03_ENCODE_ACCOUNT_DST(                                           \
+            buf_out, to_address); /* account | size  22 */                   \
+        etxn_details(                                                        \
+            (uint32_t)buf_out,                                               \
+            PREPARE_PAYMENT_SIMPLE_TRUSTLINE_SIZE); /* emitdet | size 1?? */ \
+        int64_t fee = etxn_fee_base(                                         \
+            buf_out_master, PREPARE_PAYMENT_SIMPLE_TRUSTLINE_SIZE);          \
+        _06_08_ENCODE_DROPS_FEE(fee_ptr, fee);                               \
     }
 
-
-
 #endif
-

hook/sfcodes.h

@@ -9,6 +9,8 @@
 #define sfUNLModifyDisabling ((16U << 16U) + 17U)
 #define sfHookResult ((16U << 16U) + 18U)
 #define sfWasLockingChainSend ((16U << 16U) + 19U)
+#define sfSidecarType ((16U << 16U) + 20U)
+#define sfEntropyTier ((16U << 16U) + 21U)
 #define sfLedgerEntryType ((1U << 16U) + 1U)
 #define sfTransactionType ((1U << 16U) + 2U)
 #define sfSignerWeight ((1U << 16U) + 3U)
@@ -22,6 +24,8 @@
 #define sfHookApiVersion ((1U << 16U) + 20U)
 #define sfHookStateScale ((1U << 16U) + 21U)
 #define sfLedgerFixType ((1U << 16U) + 22U)
+#define sfHookExportCount ((1U << 16U) + 98U)
+#define sfEntropyCount ((1U << 16U) + 99U)
 #define sfNetworkID ((2U << 16U) + 1U)
 #define sfFlags ((2U << 16U) + 2U)
 #define sfSourceTag ((2U << 16U) + 3U)
@@ -80,6 +84,7 @@
 #define sfRewardTime ((2U << 16U) + 98U)
 #define sfRewardLgrFirst ((2U << 16U) + 99U)
 #define sfRewardLgrLast ((2U << 16U) + 100U)
+#define sfCancelTicketSequence ((2U << 16U) + 101U)
 #define sfIndexNext ((3U << 16U) + 1U)
 #define sfIndexPrevious ((3U << 16U) + 2U)
 #define sfBookNode ((3U << 16U) + 3U)
@@ -159,6 +164,7 @@
 #define sfEmittedTxnID ((5U << 16U) + 97U)
 #define sfGovernanceMarks ((5U << 16U) + 98U)
 #define sfGovernanceFlags ((5U << 16U) + 99U)
+#define sfEntropyDigest ((5U << 16U) + 100U)
 #define sfNumber ((9U << 16U) + 1U)
 #define sfAmount ((6U << 16U) + 1U)
 #define sfBalance ((6U << 16U) + 2U)
@@ -189,6 +195,7 @@
 #define sfSignatureReward ((6U << 16U) + 29U)
 #define sfMinAccountCreateAmount ((6U << 16U) + 30U)
 #define sfLPTokenBalance ((6U << 16U) + 31U)
+#define sfTrustLineRewardAccumulator ((6U << 16U) + 99U)
 #define sfPublicKey ((7U << 16U) + 1U)
 #define sfMessageKey ((7U << 16U) + 2U)
 #define sfSigningPubKey ((7U << 16U) + 3U)
@@ -220,6 +227,7 @@
 #define sfProvider ((7U << 16U) + 30U)
 #define sfMPTokenMetadata ((7U << 16U) + 31U)
 #define sfCredentialType ((7U << 16U) + 32U)
+#define sfHookName ((7U << 16U) + 97U)
 #define sfRemarkValue ((7U << 16U) + 98U)
 #define sfRemarkName ((7U << 16U) + 99U)
 #define sfAccount ((8U << 16U) + 1U)
@@ -255,6 +263,7 @@
 #define sfIssuingChainIssue ((24U << 16U) + 2U)
 #define sfAsset ((24U << 16U) + 3U)
 #define sfAsset2 ((24U << 16U) + 4U)
+#define sfClaimCurrency ((24U << 16U) + 5U)
 #define sfXChainBridge ((25U << 16U) + 1U)
 #define sfTransactionMetaData ((14U << 16U) + 2U)
 #define sfCreatedNode ((14U << 16U) + 3U)
@@ -285,6 +294,7 @@
 #define sfXChainCreateAccountAttestationCollectionElement ((14U << 16U) + 31U)
 #define sfPriceData ((14U << 16U) + 32U)
 #define sfCredential ((14U << 16U) + 33U)
+#define sfExportedTxn ((14U << 16U) + 90U)
 #define sfAmountEntry ((14U << 16U) + 91U)
 #define sfMintURIToken ((14U << 16U) + 92U)
 #define sfHookEmission ((14U << 16U) + 93U)
@@ -292,6 +302,9 @@
 #define sfActiveValidator ((14U << 16U) + 95U)
 #define sfGenesisMint ((14U << 16U) + 96U)
 #define sfRemark ((14U << 16U) + 97U)
+#define sfHighReward ((14U << 16U) + 98U)
+#define sfLowReward ((14U << 16U) + 99U)
+#define sfExportResult ((14U << 16U) + 100U)
 #define sfSigners ((15U << 16U) + 3U)
 #define sfSignerEntries ((15U << 16U) + 4U)
 #define sfTemplate ((15U << 16U) + 5U)

hook/tts.h

@@ -61,6 +61,7 @@
 #define ttNFTOKEN_MODIFY 70
 #define ttPERMISSIONED_DOMAIN_SET 71
 #define ttPERMISSIONED_DOMAIN_DELETE 72
+#define ttEXPORT 91
 #define ttCRON 92
 #define ttCRON_SET 93
 #define ttREMARKS_SET 94
@@ -74,3 +75,4 @@
 #define ttUNL_MODIFY 102
 #define ttEMIT_FAILURE 103
 #define ttUNL_REPORT 104
+#define ttCONSENSUS_ENTROPY 105

hook/tx_flags.h

@@ -115,3 +115,8 @@ enum AMMClawbackFlags : uint32_t {
 enum BridgeModifyFlags : uint32_t {
     tfClearAccountCreateAmount = 0x00010000,
 };
+
+enum ConsensusEntropyFlags : uint32_t {
+    tfEntropyCommit = 0x00000001,  // entry is a commitment in commitSet
+    tfEntropyReveal = 0x00000002,  // entry is a reveal in entropySet
+};

include/xrpl/hook/Enum.h

@@ -15,7 +15,10 @@
 #define uint256 std::string
 #define featureHooksUpdate1 "1"
 #define featureHooksUpdate2 "1"
+#define featureExport "1"
+#define featureConsensusEntropy "1"
 #define fix20250131 "1"
+#define fixGuardDepth32 "1"
 namespace hook_api {
 struct Rules
 {
@@ -319,7 +322,7 @@ namespace compare_mode {
 enum compare_mode : uint32_t { EQUAL = 1, LESS = 2, GREATER = 4 };
 }
 
-enum hook_return_code : int64_t {
+enum class hook_return_code : int64_t {
     SUCCESS =
         0,  // return codes > 0 are reserved for hook apis to return "success"
     OUT_OF_BOUNDS =
@@ -383,10 +386,13 @@ enum hook_return_code : int64_t {
     MEM_OVERLAP = -43,   // one or more specified buffers are the same memory
     TOO_MANY_STATE_MODIFICATIONS = -44,  // more than 5000 modified state
                                          // entires in the combined hook chains
-    TOO_MANY_NAMESPACES = -45
+    TOO_MANY_NAMESPACES = -45,
+    EXPORT_FAILURE = -46,
+    TOO_MANY_EXPORTED_TXN = -47,
+    TOO_LITTLE_ENTROPY = -48,
 };
 
-enum ExitType : uint8_t {
+enum class ExitType : uint8_t {
     UNSET = 0,
     WASM_ERROR = 1,
     ROLLBACK = 2,
@@ -397,6 +403,7 @@ const uint16_t max_state_modifications = 256;
 const uint8_t max_slots = 255;
 const uint8_t max_nonce = 255;
 const uint8_t max_emit = 255;
+const uint8_t max_export = 2;
 const uint8_t max_params = 16;
 const double fee_base_multiplier = 1.1f;
 
@@ -437,12 +444,9 @@ getImportWhitelist(Rules const& rules)
     return whitelist;
 }
 
-#undef HOOK_API_DEFINITION
-#undef I32
-#undef I64
-
 enum GuardRulesVersion : uint64_t {
     GuardRuleFix20250131 = 0x00000001,
+    GuardRuleDepth32 = 0x00000002,
 };
 
 inline uint64_t
@@ -451,6 +455,8 @@ getGuardRulesVersion(Rules const& rules)
     uint64_t version = 0;
     if (rules.enabled(fix20250131))
         version |= GuardRuleFix20250131;
+    if (rules.enabled(fixGuardDepth32))
+        version |= GuardRuleDepth32;
     return version;
 }
 

include/xrpl/hook/Guard.h

@@ -204,9 +204,13 @@ struct WasmBlkInf
     }
 // compute worst case execution time
 inline uint64_t
-compute_wce(const WasmBlkInf* blk, int level, bool* recursion_limit_reached)
+compute_wce(
+    const WasmBlkInf* blk,
+    int level,
+    int max_level,
+    bool* recursion_limit_reached)
 {
-    if (level > 16)
+    if (level > max_level)
     {
         *recursion_limit_reached = true;
         return 0;
@@ -233,8 +237,8 @@ compute_wce(const WasmBlkInf* blk, int level, bool* recursion_limit_reached)
 
     if (blk->children.size() > 0)
         for (auto const& child : blk->children)
-            worst_case_execution +=
-                compute_wce(child, level + 1, recursion_limit_reached);
+            worst_case_execution += compute_wce(
+                child, level + 1, max_level, recursion_limit_reached);
 
     if (parent == 0 ||
         parent->iteration_bound ==
@@ -788,12 +792,17 @@ check_guard(
     }
 
     bool recursion_limit_reached = false;
-    uint64_t wce = compute_wce(&(*root), 0, &recursion_limit_reached);
+    int max_level = 16;
+    if (rulesVersion & hook_api::GuardRuleDepth32)
+        max_level = 32;
+    uint64_t wce =
+        compute_wce(&(*root), 0, max_level, &recursion_limit_reached);
     if (recursion_limit_reached)
     {
         GUARDLOG(hook::log::NESTING_LIMIT)
             << "GuardCheck "
-            << "Maximum allowable depth of blocks reached (16 levels). Flatten "
+            << "Maximum allowable depth of blocks reached (" << max_level
+            << " levels). Flatten "
                "your loops and conditions!.\n";
         return {};
     }

include/xrpl/hook/Macro.h

@@ -89,58 +89,69 @@
 
 #define WASM_VAL_TYPE(T, b) CAT2(TYP_, T)
 
-#define DECLARE_HOOK_FUNCTION(R, F, ...)                         \
-    R F(hook::HookContext& hookCtx,                              \
-        WasmEdge_CallingFrameContext const& frameCtx __VA_OPT__( \
-            COMMA __VA_ARGS__));                                 \
-    extern WasmEdge_Result WasmFunction##F(                      \
-        void* data_ptr,                                          \
-        const WasmEdge_CallingFrameContext* frameCtx,            \
-        const WasmEdge_Value* in,                                \
-        WasmEdge_Value* out);                                    \
-    extern WasmEdge_ValType WasmFunctionParams##F[];             \
-    extern WasmEdge_ValType WasmFunctionResult##F[];             \
-    extern WasmEdge_FunctionTypeContext* WasmFunctionType##F;    \
+#define UNSIGNED_TYPE(T) std::make_unsigned_t<T>
+
+#define DECLARE_HOOK_FUNCTION(R, F, ...)                          \
+    std::variant<UNSIGNED_TYPE(R), hook_api::hook_return_code> F( \
+        hook::HookContext& hookCtx,                               \
+        WasmEdge_CallingFrameContext const& frameCtx __VA_OPT__(  \
+            COMMA __VA_ARGS__));                                  \
+    extern WasmEdge_Result WasmFunction##F(                       \
+        void* data_ptr,                                           \
+        const WasmEdge_CallingFrameContext* frameCtx,             \
+        const WasmEdge_Value* in,                                 \
+        WasmEdge_Value* out);                                     \
+    extern WasmEdge_ValType WasmFunctionParams##F[];              \
+    extern WasmEdge_ValType WasmFunctionResult##F[];              \
+    extern WasmEdge_FunctionTypeContext* WasmFunctionType##F;     \
     extern WasmEdge_String WasmFunctionName##F;
 
-#define DEFINE_HOOK_FUNCTION(R, F, ...)                             \
-    WasmEdge_Result hook_api::WasmFunction##F(                      \
-        void* data_ptr,                                             \
-        const WasmEdge_CallingFrameContext* frameCtx,               \
-        const WasmEdge_Value* in,                                   \
-        WasmEdge_Value* out)                                        \
-    {                                                               \
-        __VA_OPT__(int _stack = 0;)                                 \
-        __VA_OPT__(FOR_VARS(VAR_ASSIGN, 2, __VA_ARGS__);)           \
-        hook::HookContext* hookCtx =                                \
-            reinterpret_cast<hook::HookContext*>(data_ptr);         \
-        R return_code = hook_api::F(                                \
-            *hookCtx,                                               \
-            *const_cast<WasmEdge_CallingFrameContext*>(frameCtx)    \
-                __VA_OPT__(COMMA STRIP_TYPES(__VA_ARGS__)));        \
-        if (return_code == RC_ROLLBACK || return_code == RC_ACCEPT) \
-            return WasmEdge_Result_Terminate;                       \
-        out[0] = RET_ASSIGN(R, return_code);                        \
-        return WasmEdge_Result_Success;                             \
-    };                                                              \
-    WasmEdge_ValType hook_api::WasmFunctionParams##F[] = {          \
-        __VA_OPT__(FOR_VARS(WASM_VAL_TYPE, 0, __VA_ARGS__))};       \
-    WasmEdge_ValType hook_api::WasmFunctionResult##F[1] = {         \
-        WASM_VAL_TYPE(R, dummy)};                                   \
-    WasmEdge_FunctionTypeContext* hook_api::WasmFunctionType##F =   \
-        WasmEdge_FunctionTypeCreate(                                \
-            WasmFunctionParams##F,                                  \
-            VA_NARGS(NULL __VA_OPT__(, __VA_ARGS__)),               \
-            WasmFunctionResult##F,                                  \
-            1);                                                     \
-    WasmEdge_String hook_api::WasmFunctionName##F =                 \
-        WasmEdge_StringCreateByCString(#F);                         \
-    R hook_api::F(                                                  \
-        hook::HookContext& hookCtx,                                 \
-        WasmEdge_CallingFrameContext const& frameCtx __VA_OPT__(    \
+#define DEFINE_HOOK_FUNCTION(R, F, ...)                                        \
+    WasmEdge_Result hook_api::WasmFunction##F(                                 \
+        void* data_ptr,                                                        \
+        const WasmEdge_CallingFrameContext* frameCtx,                          \
+        const WasmEdge_Value* in,                                              \
+        WasmEdge_Value* out)                                                   \
+    {                                                                          \
+        __VA_OPT__(int _stack = 0;)                                            \
+        __VA_OPT__(FOR_VARS(VAR_ASSIGN, 2, __VA_ARGS__);)                      \
+        hook::HookContext* hookCtx =                                           \
+            reinterpret_cast<hook::HookContext*>(data_ptr);                    \
+        auto const& return_code = hook_api::F(                                 \
+            *hookCtx,                                                          \
+            *const_cast<WasmEdge_CallingFrameContext*>(frameCtx)               \
+                __VA_OPT__(COMMA STRIP_TYPES(__VA_ARGS__)));                   \
+        if (std::holds_alternative<hook_api::hook_return_code>(return_code) && \
+            (std::get<hook_api::hook_return_code>(return_code) ==              \
+                 RC_ROLLBACK ||                                                \
+             std::get<hook_api::hook_return_code>(return_code) == RC_ACCEPT))  \
+            return WasmEdge_Result_Terminate;                                  \
+        out[0] = RET_ASSIGN(                                                   \
+            R,                                                                 \
+            std::holds_alternative<UNSIGNED_TYPE(R)>(return_code)              \
+                ? std::get<UNSIGNED_TYPE(R)>(return_code)                      \
+                : R(std::get<hook_api::hook_return_code>(return_code)));       \
+        return WasmEdge_Result_Success;                                        \
+    };                                                                         \
+    WasmEdge_ValType hook_api::WasmFunctionParams##F[] = {                     \
+        __VA_OPT__(FOR_VARS(WASM_VAL_TYPE, 0, __VA_ARGS__))};                  \
+    WasmEdge_ValType hook_api::WasmFunctionResult##F[1] = {                    \
+        WASM_VAL_TYPE(R, dummy)};                                              \
+    WasmEdge_FunctionTypeContext* hook_api::WasmFunctionType##F =              \
+        WasmEdge_FunctionTypeCreate(                                           \
+            WasmFunctionParams##F,                                             \
+            VA_NARGS(NULL __VA_OPT__(, __VA_ARGS__)),                          \
+            WasmFunctionResult##F,                                             \
+            1);                                                                \
+    WasmEdge_String hook_api::WasmFunctionName##F =                            \
+        WasmEdge_StringCreateByCString(#F);                                    \
+    std::variant<UNSIGNED_TYPE(R), hook_api::hook_return_code> hook_api::F(    \
+        hook::HookContext& hookCtx,                                            \
+        WasmEdge_CallingFrameContext const& frameCtx __VA_OPT__(               \
             COMMA __VA_ARGS__))
 
 #define HOOK_SETUP()                                                 \
+    using enum hook_api::hook_return_code;                           \
     try                                                              \
     {                                                                \
         [[maybe_unused]] ApplyContext& applyCtx = hookCtx.applyCtx;  \
@@ -203,7 +214,7 @@
     host_memory_ptr,                  \
     guest_memory_length)              \
     {                                 \
-        int64_t bytes_written = 0;    \
+        uint64_t bytes_written = 0;   \
         WRITE_WASM_MEMORY(            \
             bytes_written,            \
             guest_dst_ptr,            \
@@ -272,7 +283,7 @@
             data_ptr < (data_ptr_in))                                    \
             return INTERNAL_ERROR;                                       \
         if (data_len == 0)                                               \
-            return 0;                                                    \
+            return 0ULL;                                                 \
         if ((write_ptr_in) == 0)                                         \
             return data_as_int64(data_ptr, data_len);                    \
         if (data_len > (write_len_in))                                   \

include/xrpl/hook/hook_api.macro

@@ -372,3 +372,28 @@ HOOK_API_DEFINITION(
 HOOK_API_DEFINITION(
   int64_t, prepare, (uint32_t, uint32_t, uint32_t, uint32_t),
   featureHooksUpdate2)
+
+// int64_t xport_reserve(uint32_t count);
+HOOK_API_DEFINITION(
+  int64_t, xport_reserve, (uint32_t),
+  featureExport)
+
+// int64_t xport(uint32_t write_ptr, uint32_t write_len, uint32_t read_ptr, uint32_t read_len);
+HOOK_API_DEFINITION(
+  int64_t, xport, (uint32_t, uint32_t, uint32_t, uint32_t),
+  featureExport)
+
+// int64_t xport_cancel(uint32_t ticket_seq);
+HOOK_API_DEFINITION(
+  int64_t, xport_cancel, (uint32_t),
+  featureExport)
+
+// int64_t dice(uint32_t sides, uint32_t min_tier, uint32_t min_count);
+HOOK_API_DEFINITION(
+  int64_t, dice, (uint32_t, uint32_t, uint32_t),
+  featureConsensusEntropy)
+
+// int64_t random(uint32_t write_ptr, uint32_t write_len, uint32_t min_tier, uint32_t min_count);
+HOOK_API_DEFINITION(
+  int64_t, random, (uint32_t, uint32_t, uint32_t, uint32_t),
+  featureConsensusEntropy)

include/xrpl/proto/.clang-format

@@ -0,0 +1,2 @@
+---
+DisableFormat: true

include/xrpl/proto/ripple.proto

@@ -153,7 +153,11 @@ message TMStatusChange
 message TMProposeSet
 {
     required uint32 proposeSeq          = 1;
-    required bytes currentTxHash        = 2;    // the hash of the ledger we are proposing
+    // Proposed transaction-set identity. Legacy/plain proposals carry the
+    // tx-set hash directly; ConsensusExtensions proposals carry a serialized
+    // ExtendedPosition whose first field is that tx-set hash, followed by
+    // signed RNG/Export sidecar fields.
+    required bytes currentTxHash        = 2;
     required bytes nodePubKey           = 3;
     required uint32 closeTime           = 4;
     required bytes signature            = 5;    // signature of above fields
@@ -166,6 +170,14 @@ message TMProposeSet
 
     // Number of hops traveled
     optional uint32 hops                = 12    [deprecated=true];
+
+    // Export signatures for pending exports seen in the proposal set. The
+    // proposal's ExtendedPosition includes a digest of this repeated field, so
+    // these side-channel blobs are covered by the proposal signature.
+    // Each entry is: txnHash (32 bytes) + validator pubkey (33 bytes)
+    // + multisign signature (variable length). Validators attach these
+    // so export quorum can be reached within the same consensus round.
+    repeated bytes exportSignatures     = 13;
 }
 
 enum TxSetStatus
@@ -384,4 +396,3 @@ message TMHaveTransactions
 {
     repeated bytes hashes = 1;
 }
-

include/xrpl/protocol/EntropyTier.h

@@ -0,0 +1,42 @@
+#ifndef RIPPLE_PROTOCOL_ENTROPY_TIER_H_INCLUDED
+#define RIPPLE_PROTOCOL_ENTROPY_TIER_H_INCLUDED
+
+#include <cstdint>
+
+namespace ripple {
+
+/// Which gate the ledger's entropy passed. Stored in sfEntropyTier (UINT8)
+/// on the ttCONSENSUS_ENTROPY pseudo-transaction and the ConsensusEntropy
+/// ledger entry.
+///
+/// EntropyCount says how many validators contributed; EntropyTier says which
+/// gate the result passed. Values are strength-ordered so consumers can gate
+/// with a numeric comparison (tier >= required).
+enum EntropyTier : std::uint8_t {
+    /// No usable entropy (reserved; a fresh ConsensusEntropy entry should
+    /// always carry one of the tiers below).
+    entropyTierNone = 0,
+
+    /// Consensus-bound deterministic fallback: derived from already-agreed
+    /// round inputs (parent ledger hash, base tx set hash, sequence) under
+    /// HashPrefix::entropyFallback when no agreed reveal set reaches either
+    /// participant_aligned or validator_quorum. Unpredictable in practice but
+    /// user-influenceable via transaction submission — never suitable for
+    /// value-bearing outcomes.
+    entropyTierConsensusFallback = 1,
+
+    /// Participant-aligned sub-quorum entropy: the agreed reveal set aligned at
+    /// the tier-2 participant threshold — below the 80% validator quorum but at
+    /// or above the equivocation-intersection floor over the original
+    /// (pre-nUNL)
+    /// view. Weaker than validator_quorum; opt-in for hooks via min_tier.
+    entropyTierParticipantAligned = 2,
+
+    /// Validator commit/reveal entropy whose sidecar set passed the
+    /// active-validator-view quorum alignment gate.
+    entropyTierValidatorQuorum = 3,
+};
+
+}  // namespace ripple
+
+#endif

include/xrpl/protocol/ExportLimits.h

@@ -0,0 +1,33 @@
+#ifndef RIPPLE_PROTOCOL_EXPORT_LIMITS_H_INCLUDED
+#define RIPPLE_PROTOCOL_EXPORT_LIMITS_H_INCLUDED
+
+#include <cstdint>
+
+namespace ripple {
+
+// Export system caps.
+//
+// These limits bound the DoS surface of the export signature system:
+// - Each pending export requires every validator to sign it every round
+//   (sign-once, attach once via TMProposeSet)
+// - Inbound signature processing involves crypto verification per sig
+// - The open-ledger cap (maxPendingExports) is the root constraint;
+//   signing throughput and inbound processing are transitively bounded by it
+struct ExportLimits
+{
+    // Maximum exports a single hook execution may produce
+    // (also enforced by hook_api::max_export in Enum.h)
+    static constexpr std::uint8_t maxExportsPerHook = 2;
+
+    // Maximum pending export transactions in an open/apply ledger.
+    // Hook-emitted export backlog drains into the open ledger at this cap.
+    // This transitively caps:
+    //   - signatures per TMProposeSet message (1 per pending export)
+    //   - inbound proposal signature processing (clamped to this)
+    //   - validator signing work per round
+    static constexpr std::uint8_t maxPendingExports = 8;
+};
+
+}  // namespace ripple
+
+#endif

include/xrpl/protocol/Feature.h

@@ -33,35 +33,39 @@
  *
  * Steps required to add new features to the code:
  *
- * 1) In this file, increment `numFeatures` and add a uint256 declaration
- *    for the feature at the bottom
- * 2) Add a uint256 definition for the feature to the corresponding source
- *    file (Feature.cpp). Use `registerFeature` to create the feature with
- *    the feature's name, `Supported::no`, and `VoteBehavior::DefaultNo`. This
- *    should be the only place the feature's name appears in code as a string.
- * 3) Use the uint256 as the parameter to `view.rules.enabled()` to
- *    control flow into new code that this feature limits.
- * 4) If the feature development is COMPLETE, and the feature is ready to be
- *    SUPPORTED, change the `registerFeature` parameter to Supported::yes.
- * 5) When the feature is ready to be ENABLED, change the `registerFeature`
- *    parameter to `VoteBehavior::DefaultYes`.
- * In general, any newly supported amendments (`Supported::yes`) should have
- * a `VoteBehavior::DefaultNo` for at least one full release cycle. High
- * priority bug fixes can be an exception to this rule of thumb.
+ * 1) Add the appropriate XRPL_FEATURE or XRPL_FIX macro definition for the
+ *    feature to features.macro with the feature's name, `Supported::no`, and
+ *    `VoteBehavior::DefaultNo`.
+ *
+ * 2) Use the generated variable name as the parameter to `view.rules.enabled()`
+ *    to control flow into new code that this feature limits. (featureName or
+ *    fixName)
+ *
+ * 3) If the feature development is COMPLETE, and the feature is ready to be
+ *    SUPPORTED, change the macro parameter in features.macro to Supported::yes.
+ *
+ * 4) In general, any newly supported amendments (`Supported::yes`) should have
+ *    a `VoteBehavior::DefaultNo` indefinitely so that external governance can
+ *    make the decision on when to activate it. High priority bug fixes can be
+ *    an exception to this rule. In such cases, ensure the fix has been
+ *    clearly communicated to the community using appropriate channels,
+ *    then change the macro parameter in features.macro to
+ *    `VoteBehavior::DefaultYes`. The communication process is beyond
+ *    the scope of these instructions.
+ *
  *
  * When a feature has been enabled for several years, the conditional code
  * may be removed, and the feature "retired". To retire a feature:
- * 1) Remove the uint256 declaration from this file.
- * 2) MOVE the uint256 definition in Feature.cpp to the "retired features"
- *    section at the end of the file.
- * 3) CHANGE the name of the variable to start with "retired".
- * 4) CHANGE the parameters of the `registerFeature` call to `Supported::yes`
- *    and `VoteBehavior::DefaultNo`.
+ *
+ * 1) MOVE the macro definition in features.macro to the "retired features"
+ *    section at the end of the file, and change the macro to XRPL_RETIRE.
+ *
  * The feature must remain registered and supported indefinitely because it
- * still exists in the ledger, but there is no need to vote for it because
- * there's nothing to vote for. If it is removed completely from the code, any
- * instances running that code will get amendment blocked. Removing the
- * feature from the ledger is beyond the scope of these instructions.
+ * may exist in the Amendments object on ledger. There is no need to vote
+ * for it because there's nothing to vote for. If the feature definition is
+ * removed completely from the code, any instances running that code will get
+ * amendment blocked. Removing the feature from the ledger is beyond the scope
+ * of these instructions.
  *
  */
 
@@ -76,11 +80,32 @@ allAmendments();
 
 namespace detail {
 
+#pragma push_macro("XRPL_FEATURE")
+#undef XRPL_FEATURE
+#pragma push_macro("XRPL_FIX")
+#undef XRPL_FIX
+#pragma push_macro("XRPL_RETIRE")
+#undef XRPL_RETIRE
+
+#define XRPL_FEATURE(name, supported, vote) +1
+#define XRPL_FIX(name, supported, vote) +1
+#define XRPL_RETIRE(name) +1
+
 // This value SHOULD be equal to the number of amendments registered in
 // Feature.cpp. Because it's only used to reserve storage, and determine how
 // large to make the FeatureBitset, it MAY be larger. It MUST NOT be less than
 // the actual number of amendments. A LogicError on startup will verify this.
-static constexpr std::size_t numFeatures = 115;
+static constexpr std::size_t numFeatures =
+    (0 +
+#include <xrpl/protocol/detail/features.macro>
+    );
+
+#undef XRPL_RETIRE
+#pragma pop_macro("XRPL_RETIRE")
+#undef XRPL_FIX
+#pragma pop_macro("XRPL_FIX")
+#undef XRPL_FEATURE
+#pragma pop_macro("XRPL_FEATURE")
 
 /** Amendments that this server supports and the default voting behavior.
    Whether they are enabled depends on the Rules defined in the validated
@@ -320,12 +345,17 @@ foreachFeature(FeatureBitset bs, F&& f)
 #undef XRPL_FEATURE
 #pragma push_macro("XRPL_FIX")
 #undef XRPL_FIX
+#pragma push_macro("XRPL_RETIRE")
+#undef XRPL_RETIRE
 
 #define XRPL_FEATURE(name, supported, vote) extern uint256 const feature##name;
 #define XRPL_FIX(name, supported, vote) extern uint256 const fix##name;
+#define XRPL_RETIRE(name)
 
 #include <xrpl/protocol/detail/features.macro>
 
+#undef XRPL_RETIRE
+#pragma pop_macro("XRPL_RETIRE")
 #undef XRPL_FIX
 #pragma pop_macro("XRPL_FIX")
 #undef XRPL_FEATURE

include/xrpl/protocol/HashPrefix.h

@@ -96,6 +96,15 @@ enum class HashPrefix : std::uint32_t {
 
     /** Credentials signature */
     credential = detail::make_hash_prefix('C', 'R', 'D'),
+
+    /** consensus extension sidecar object */
+    sidecar = detail::make_hash_prefix('S', 'C', 'R'),
+
+    /** consensus-bound fallback entropy digest (Tier 1: derived from
+        already-agreed round inputs when no agreed reveal set reaches an
+        accepted validator-participant tier; never to be confused with
+        validator entropy) */
+    entropyFallback = detail::make_hash_prefix('E', 'F', 'B'),
 };
 
 template <class Hasher>

include/xrpl/protocol/Indexes.h

@@ -62,6 +62,9 @@ emittedDir() noexcept;
 Keylet
 emittedTxn(uint256 const& id) noexcept;
 
+Keylet
+shadowTicket(AccountID const& account, std::uint32_t ticketSeq) noexcept;
+
 Keylet
 hookDefinition(uint256 const& hash) noexcept;
 
@@ -118,6 +121,10 @@ negativeUNL() noexcept;
 Keylet const&
 UNLReport() noexcept;
 
+/** The (fixed) index of the object containing consensus-derived entropy. */
+Keylet const&
+consensusEntropy() noexcept;
+
 /** The beginning of an order book */
 struct book_t
 {

include/xrpl/protocol/SidecarType.h

@@ -0,0 +1,21 @@
+#ifndef RIPPLE_PROTOCOL_SIDECAR_TYPE_H_INCLUDED
+#define RIPPLE_PROTOCOL_SIDECAR_TYPE_H_INCLUDED
+
+#include <cstdint>
+
+namespace ripple {
+
+/// Discriminator for sidecar set entries (SHAMap leaves used for
+/// consensus extension data: RNG commit/reveal, export signatures).
+///
+/// Stored in sfSidecarType (UINT8) on each STObject entry.
+/// Makes sidecar sets self-describing — no content-sniffing needed.
+enum SidecarType : std::uint8_t {
+    sidecarRngCommit = 1,
+    sidecarRngReveal = 2,
+    sidecarExportSig = 3,
+};
+
+}  // namespace ripple
+
+#endif

include/xrpl/protocol/TER.h

@@ -68,6 +68,7 @@ enum TELcodes : TERUnderlyingType {
     telNON_LOCAL_EMITTED_TXN,
     telIMPORT_VL_KEY_NOT_RECOGNISED,
     telCAN_NOT_QUEUE_IMPORT,
+    telSHADOW_TICKET_REQUIRED,
     telENV_RPC_FAILED,
 };
 
@@ -137,6 +138,7 @@ enum TEMcodes : TERUnderlyingType {
     temXCHAIN_BRIDGE_NONDOOR_OWNER,
     temXCHAIN_BRIDGE_BAD_MIN_ACCOUNT_CREATE_AMOUNT,
     temXCHAIN_BRIDGE_BAD_REWARD_AMOUNT,
+    temXCHAIN_TOO_MANY_ATTESTATIONS,  // RESERVED - not used
 
     temHOOK_DATA_TOO_LARGE,
     temEMPTY_DID,
@@ -233,8 +235,10 @@ enum TERcodes : TERUnderlyingType {
     terQUEUED,       // Transaction is being held in TxQ until fee drops
     terPRE_TICKET,   // Ticket is not yet in ledger but might be on its way
     terNO_AMM,       // AMM doesn't exist for the asset pair
-    terNO_HOOK       // Transaction requires a non-existent hook definition
+    terNO_HOOK,      // Transaction requires a non-existent hook definition
                      // (referenced by sfHookHash)
+    terRETRY_EXPORT  // Export does not yet have enough validator signatures.
+                     // Retained in retriable set for next ledger.
 };
 
 //------------------------------------------------------------------------------
@@ -362,6 +366,7 @@ enum TECcodes : TERUnderlyingType {
     tecARRAY_TOO_LARGE = 197,
     tecLOCKED = 198,
     tecBAD_CREDENTIALS = 199,
+    tecEXPORT_EXPIRED = 200,
     tecLAST_POSSIBLE_ENTRY = 255,
 };
 

include/xrpl/protocol/TxFlags.h

@@ -274,6 +274,13 @@ enum BridgeModifyFlags : uint32_t {
     tfClearAccountCreateAmount = 0x00010000,
 };
 constexpr std::uint32_t tfBridgeModifyMask = ~(tfUniversal | tfClearAccountCreateAmount);
+
+// ConsensusEntropy flags (used on ttCONSENSUS_ENTROPY SHAMap entries):
+enum ConsensusEntropyFlags : uint32_t {
+    tfEntropyCommit = 0x00000001,  // entry is a commitment in commitSet
+    tfEntropyReveal = 0x00000002,  // entry is a reveal in entropySet
+};
+// flag=0 (no tfEntropyCommit/tfEntropyReveal) = final injected pseudo-tx
 // clang-format on
 
 }  // namespace ripple

include/xrpl/protocol/TxMeta.h

@@ -140,6 +140,12 @@ public:
         mHookEmissions = hookEmissions;
     }
 
+    void
+    setExportResult(STObject const& exportResult)
+    {
+        mExportResult = exportResult;
+    }
+
     bool
     hasHookExecutions() const
     {
@@ -152,6 +158,12 @@ public:
         return static_cast<bool>(mHookEmissions);
     }
 
+    bool
+    hasExportResult() const
+    {
+        return static_cast<bool>(mExportResult);
+    }
+
     STAmount
     getDeliveredAmount() const
     {
@@ -176,6 +188,7 @@ private:
     std::optional<STAmount> mDelivered;
     std::optional<STArray> mHookExecutions;
     std::optional<STArray> mHookEmissions;
+    std::optional<STObject> mExportResult;
 
     STArray mNodes;
 };

include/xrpl/protocol/detail/features.macro

@@ -23,6 +23,9 @@
 #if !defined(XRPL_FIX)
 #error "undefined macro: XRPL_FIX"
 #endif
+#if !defined(XRPL_RETIRE)
+#error "undefined macro: XRPL_RETIRE"
+#endif
 
 // clang-format off
 
@@ -31,6 +34,10 @@
 // If you add an amendment here, then do not forget to increment `numFeatures`
 // in include/xrpl/protocol/Feature.h.
 
+XRPL_FIX    (HookMap,                    Supported::yes, VoteBehavior::DefaultYes)
+XRPL_FIX    (GuardDepth32,               Supported::yes, VoteBehavior::DefaultNo)
+XRPL_FEATURE(NamedHooks,                 Supported::yes, VoteBehavior::DefaultNo)
+XRPL_FEATURE(IOURewardClaim,             Supported::yes, VoteBehavior::DefaultNo)
 XRPL_FIX    (IOULockedBalanceInvariant,  Supported::yes, VoteBehavior::DefaultNo)
 XRPL_FIX    (ImportIssuer,               Supported::yes, VoteBehavior::DefaultYes)
 XRPL_FEATURE(HookAPISerializedType240,   Supported::yes, VoteBehavior::DefaultNo)
@@ -54,18 +61,20 @@ XRPL_FIX    (FillOrKill,                 Supported::yes, VoteBehavior::DefaultYe
 XRPL_FEATURE(DID,                        Supported::no,  VoteBehavior::DefaultNo)
 XRPL_FIX    (DisallowIncomingV1,         Supported::yes, VoteBehavior::DefaultYes)
 XRPL_FEATURE(XChainBridge,               Supported::no,  VoteBehavior::DefaultNo)
-XRPL_FEATURE(AMM,                        Supported::yes, VoteBehavior::DefaultNo)
+XRPL_FEATURE(AMM,                        Supported::no,  VoteBehavior::DefaultNo)
 XRPL_FIX    (ReducedOffersV1,            Supported::yes, VoteBehavior::DefaultYes)
-XRPL_FEATURE(HooksUpdate2,               Supported::yes, VoteBehavior::DefaultNo);
-XRPL_FEATURE(HookOnV2,                   Supported::yes, VoteBehavior::DefaultNo);
-XRPL_FIX    (HookAPI20251128,            Supported::yes, VoteBehavior::DefaultYes);
-XRPL_FIX    (CronStacking,               Supported::yes, VoteBehavior::DefaultYes);
-XRPL_FEATURE(ExtendedHookState,          Supported::yes, VoteBehavior::DefaultNo);
-XRPL_FIX    (InvalidTxFlags,             Supported::yes, VoteBehavior::DefaultYes);
-XRPL_FEATURE(Cron,                       Supported::yes, VoteBehavior::DefaultNo);
-XRPL_FEATURE(IOUIssuerWeakTSH,           Supported::yes, VoteBehavior::DefaultNo);
-XRPL_FEATURE(DeepFreeze,                 Supported::yes, VoteBehavior::DefaultNo);
-XRPL_FIX    (ProvisionalDoubleThreading, Supported::yes, VoteBehavior::DefaultYes);
+XRPL_FEATURE(HooksUpdate2,               Supported::yes, VoteBehavior::DefaultNo)
+XRPL_FEATURE(HookOnV2,                   Supported::yes, VoteBehavior::DefaultNo)
+XRPL_FEATURE(Export,                     Supported::yes, VoteBehavior::DefaultNo)
+XRPL_FEATURE(ConsensusEntropy,           Supported::yes, VoteBehavior::DefaultNo)
+XRPL_FIX    (HookAPI20251128,            Supported::yes, VoteBehavior::DefaultYes)
+XRPL_FIX    (CronStacking,               Supported::yes, VoteBehavior::DefaultYes)
+XRPL_FEATURE(ExtendedHookState,          Supported::yes, VoteBehavior::DefaultNo)
+XRPL_FIX    (InvalidTxFlags,             Supported::yes, VoteBehavior::DefaultYes)
+XRPL_FEATURE(Cron,                       Supported::yes, VoteBehavior::DefaultNo)
+XRPL_FEATURE(IOUIssuerWeakTSH,           Supported::yes, VoteBehavior::DefaultNo)
+XRPL_FEATURE(DeepFreeze,                 Supported::yes, VoteBehavior::DefaultNo)
+XRPL_FIX    (ProvisionalDoubleThreading, Supported::yes, VoteBehavior::DefaultYes)
 XRPL_FEATURE(Clawback,                   Supported::yes, VoteBehavior::DefaultNo)
 XRPL_FIX    (RewardClaimFlags,           Supported::yes, VoteBehavior::DefaultYes)
 XRPL_FEATURE(HookCanEmit,                Supported::yes, VoteBehavior::DefaultNo)
@@ -149,4 +158,24 @@ XRPL_FIX    (NFTokenDirV1,          Supported::yes, VoteBehavior::Obsolete)
 XRPL_FEATURE(NonFungibleTokensV1,   Supported::yes, VoteBehavior::Obsolete)
 XRPL_FEATURE(CryptoConditionsSuite, Supported::yes, VoteBehavior::Obsolete)
 
+// The following amendments have been active for at least two years. Their
+// pre-amendment code has been removed and the identifiers are deprecated.
+// All known amendments and amendments that may appear in a validated
+// ledger must be registered either here or above with the "active" amendments
+XRPL_RETIRE(MultiSign)
+XRPL_RETIRE(TrustSetAuth)
+XRPL_RETIRE(FeeEscalation)
+XRPL_RETIRE(PayChan)
+XRPL_RETIRE(CryptoConditions)
+XRPL_RETIRE(TickSize)
+XRPL_RETIRE(fix1368)
+XRPL_RETIRE(Escrow)
+XRPL_RETIRE(fix1373)
+XRPL_RETIRE(EnforceInvariants)
+XRPL_RETIRE(SortedDirectories)
+XRPL_RETIRE(fix1201)
+XRPL_RETIRE(fix1512)
+XRPL_RETIRE(fix1523)
+XRPL_RETIRE(fix1528)
+
 // clang-format on

include/xrpl/protocol/detail/ledger_entries.macro

@@ -93,7 +93,7 @@ LEDGER_ENTRY(ltCHECK, 0x0043, Check, check, ({
 */
 LEDGER_ENTRY(ltHOOK_DEFINITION, 'D', HookDefinition, hook_definition, ({
     {sfHookHash,             soeREQUIRED},
-    {sfHookOn,               soeREQUIRED},
+    {sfHookOn,               soeOPTIONAL},
     {sfHookOnIncoming,       soeOPTIONAL},
     {sfHookOnOutgoing,       soeOPTIONAL},
     {sfHookCanEmit,          soeOPTIONAL},
@@ -223,6 +223,21 @@ LEDGER_ENTRY(ltURI_TOKEN, 0x0055, URIToken, uri_token, ({
     {sfPreviousTxnLgrSeq,    soeREQUIRED},
 }))
 
+/** The ledger object which stores consensus-derived entropy.
+
+    \note This is a singleton: only one such object exists in the ledger.
+
+    \sa keylet::consensusEntropy
+ */
+LEDGER_ENTRY_DUPLICATE(ltCONSENSUS_ENTROPY, 0x0058, ConsensusEntropy, consensus_entropy, ({
+    {sfDigest,               soeREQUIRED},
+    {sfEntropyCount,         soeREQUIRED},
+    {sfEntropyTier,          soeREQUIRED},
+    {sfLedgerSequence,       soeREQUIRED},
+    {sfPreviousTxnID,        soeREQUIRED},
+    {sfPreviousTxnLgrSeq,    soeREQUIRED},
+}))
+
 /** A ledger object which describes an account.
 
     \sa keylet::account
@@ -396,6 +411,8 @@ LEDGER_ENTRY(ltRIPPLE_STATE, 0x0072, RippleState, state, ({
     {sfHighQualityOut,       soeOPTIONAL},
     {sfLockedBalance,        soeOPTIONAL},
     {sfLockCount,            soeOPTIONAL},
+    {sfHighReward,           soeOPTIONAL},
+    {sfLowReward,            soeOPTIONAL},
 }))
 
 /** The ledger object which lists the network's fee settings.
@@ -590,6 +607,22 @@ LEDGER_ENTRY(ltDID, 0x008D, DID, did, ({
     {sfPreviousTxnLgrSeq,    soeREQUIRED},
 }))
 
+//@@start shadow-ticket-ledger-entry
+/** A shadow ticket for export replay protection.
+
+    Created when a transaction is exported. Consumed when
+    proof-of-execution is imported back. Account-owned (pays reserve).
+
+    \sa keylet::shadowTicket
+ */
+LEDGER_ENTRY(ltSHADOW_TICKET, 0x5374, ShadowTicket, shadow_ticket, ({
+    {sfAccount,              soeREQUIRED},
+    {sfTicketSequence,       soeREQUIRED},
+    {sfTransactionHash,      soeREQUIRED},
+    {sfLedgerSequence,       soeREQUIRED},
+    {sfOwnerNode,            soeREQUIRED},
+}))
+//@@end shadow-ticket-ledger-entry
+
 #undef EXPAND
 #undef LEDGER_ENTRY_DUPLICATE
-

include/xrpl/protocol/detail/sfields.macro

@@ -42,6 +42,8 @@ TYPED_SFIELD(sfTickSize,                 UINT8,     16)
 TYPED_SFIELD(sfUNLModifyDisabling,       UINT8,     17)
 TYPED_SFIELD(sfHookResult,               UINT8,     18)
 TYPED_SFIELD(sfWasLockingChainSend,      UINT8,     19)
+TYPED_SFIELD(sfSidecarType,              UINT8,     20)
+TYPED_SFIELD(sfEntropyTier,              UINT8,     21)
 
 // 16-bit integers (common)
 TYPED_SFIELD(sfLedgerEntryType,          UINT16,     1, SField::sMD_Never)
@@ -59,6 +61,8 @@ TYPED_SFIELD(sfHookExecutionIndex,       UINT16,    19)
 TYPED_SFIELD(sfHookApiVersion,           UINT16,    20)
 TYPED_SFIELD(sfHookStateScale,           UINT16,    21)
 TYPED_SFIELD(sfLedgerFixType,            UINT16,    22)
+TYPED_SFIELD(sfHookExportCount,          UINT16,    98)
+TYPED_SFIELD(sfEntropyCount,             UINT16,    99)
 
 // 32-bit integers (common)
 TYPED_SFIELD(sfNetworkID,                UINT32,     1)
@@ -123,6 +127,7 @@ TYPED_SFIELD(sfImportSequence,           UINT32,    97)
 TYPED_SFIELD(sfRewardTime,               UINT32,    98)
 TYPED_SFIELD(sfRewardLgrFirst,           UINT32,    99)
 TYPED_SFIELD(sfRewardLgrLast,            UINT32,   100)
+TYPED_SFIELD(sfCancelTicketSequence,     UINT32,   101)
 
 // 64-bit integers (common)
 TYPED_SFIELD(sfIndexNext,                UINT64,     1)
@@ -217,6 +222,7 @@ TYPED_SFIELD(sfHookCanEmit,              UINT256,   96)
 TYPED_SFIELD(sfEmittedTxnID,             UINT256,   97)
 TYPED_SFIELD(sfGovernanceMarks,          UINT256,   98)
 TYPED_SFIELD(sfGovernanceFlags,          UINT256,   99)
+TYPED_SFIELD(sfEntropyDigest,            UINT256,  100)
 
 // number (common)
 TYPED_SFIELD(sfNumber,                   NUMBER,     1)
@@ -257,6 +263,7 @@ TYPED_SFIELD(sfPrice,                    AMOUNT,    28)
 TYPED_SFIELD(sfSignatureReward,          AMOUNT,    29)
 TYPED_SFIELD(sfMinAccountCreateAmount,   AMOUNT,    30)
 TYPED_SFIELD(sfLPTokenBalance,           AMOUNT,    31)
+TYPED_SFIELD(sfTrustLineRewardAccumulator,AMOUNT,   99)
 
 // variable length (common)
 TYPED_SFIELD(sfPublicKey,                VL,         1)
@@ -292,6 +299,7 @@ TYPED_SFIELD(sfAssetClass,               VL,        29)
 TYPED_SFIELD(sfProvider,                 VL,        30)
 TYPED_SFIELD(sfMPTokenMetadata,          VL,        31)
 TYPED_SFIELD(sfCredentialType,           VL,        32)
+TYPED_SFIELD(sfHookName,                 VL,        97)
 TYPED_SFIELD(sfRemarkValue,              VL,        98)
 TYPED_SFIELD(sfRemarkName,               VL,        99)
 
@@ -340,6 +348,7 @@ TYPED_SFIELD(sfLockingChainIssue,        ISSUE,      1)
 TYPED_SFIELD(sfIssuingChainIssue,        ISSUE,      2)
 TYPED_SFIELD(sfAsset,                    ISSUE,      3)
 TYPED_SFIELD(sfAsset2,                   ISSUE,      4)
+TYPED_SFIELD(sfClaimCurrency,            ISSUE,      5)
 
 // bridge
 TYPED_SFIELD(sfXChainBridge,             XCHAIN_BRIDGE, 1)
@@ -379,6 +388,7 @@ UNTYPED_SFIELD(sfXChainClaimAttestationCollectionElement, OBJECT, 30)
 UNTYPED_SFIELD(sfXChainCreateAccountAttestationCollectionElement, OBJECT, 31)
 UNTYPED_SFIELD(sfPriceData,              OBJECT,    32)
 UNTYPED_SFIELD(sfCredential,             OBJECT,    33)
+UNTYPED_SFIELD(sfExportedTxn,            OBJECT,    90)
 UNTYPED_SFIELD(sfAmountEntry,            OBJECT,    91)
 UNTYPED_SFIELD(sfMintURIToken,           OBJECT,    92)
 UNTYPED_SFIELD(sfHookEmission,           OBJECT,    93)
@@ -386,6 +396,9 @@ UNTYPED_SFIELD(sfImportVLKey,            OBJECT,    94)
 UNTYPED_SFIELD(sfActiveValidator,        OBJECT,    95)
 UNTYPED_SFIELD(sfGenesisMint,            OBJECT,    96)
 UNTYPED_SFIELD(sfRemark,                 OBJECT,    97)
+UNTYPED_SFIELD(sfHighReward,             OBJECT,    98)
+UNTYPED_SFIELD(sfLowReward,              OBJECT,    99)
+UNTYPED_SFIELD(sfExportResult,           OBJECT,    100)
 
 // array of objects (common)
 // ARRAY/1 is reserved for end of array

include/xrpl/protocol/detail/transactions.macro

@@ -500,6 +500,17 @@ TRANSACTION(ttPERMISSIONED_DOMAIN_DELETE, 72, PermissionedDomainDelete, ({
     {sfDomainID, soeREQUIRED},
 }))
 
+//@@start export-transaction-types
+/* User-submittable export: creates a cross-chain transaction for
+   validator signing. Retries via terRETRY_EXPORT until quorum.
+   Also supports shadow ticket cancellation via sfCancelTicketSequence.
+   At least one of sfExportedTxn or sfCancelTicketSequence must be present. */
+TRANSACTION(ttEXPORT, 91, Export, ({
+    {sfExportedTxn, soeOPTIONAL},
+    {sfCancelTicketSequence, soeOPTIONAL},
+}))
+//@@end export-transaction-types
+
 /* A pseudo-txn alarm signal for invoking a hook, emitted by validators after alarm set conditions are met */
 TRANSACTION(ttCRON, 92, Cron, ({
     {sfOwner, soeREQUIRED},
@@ -550,6 +561,7 @@ TRANSACTION(ttIMPORT, 97, Import, ({
   * from a specified hook */
 TRANSACTION(ttCLAIM_REWARD, 98, ClaimReward, ({
     {sfIssuer, soeOPTIONAL},
+    {sfClaimCurrency, soeOPTIONAL},
 }))
 
 /** This transaction invokes a hook, providing arbitrary data. Essentially as a 0 drop payment. **/
@@ -605,3 +617,11 @@ TRANSACTION(ttUNL_REPORT, 104, UNLReport, ({
     {sfActiveValidator, soeOPTIONAL},
     {sfImportVLKey, soeOPTIONAL},
 }))
+
+TRANSACTION(ttCONSENSUS_ENTROPY, 105, ConsensusEntropy, ({
+    {sfLedgerSequence, soeREQUIRED},
+    {sfDigest, soeREQUIRED},
+    {sfEntropyCount, soeREQUIRED},
+    {sfEntropyTier, soeREQUIRED},
+    {sfBlob, soeOPTIONAL},
+}))

include/xrpl/protocol/jss.h

@@ -76,6 +76,7 @@ JSS(Holder);              // field.
 JSS(HookApiVersion);      // field
 JSS(HookCanEmit);         // field
 JSS(HookHash);            // field
+JSS(HookName);            // field
 JSS(HookNamespace);       // field
 JSS(HookOn);              // field
 JSS(HookOnIncoming);      // field

include/xrpl/resource/detail/Logic.h

@@ -109,14 +109,22 @@ public:
     Consumer
     newInboundEndpoint(beast::IP::Endpoint const& address)
     {
+        //@@start rng-local-testnet-resource-bucket
+        // Inbound connections from the same IP normally share one
+        // resource bucket (port stripped) for DoS protection.  For
+        // loopback addresses, preserve the port so local testnet nodes
+        // each get their own bucket instead of all sharing one.
+        auto const key = is_loopback(address) ? address : address.at_port(0);
+        //@@end rng-local-testnet-resource-bucket
+
         Entry* entry(nullptr);
 
         {
             std::lock_guard _(lock_);
             auto [resultIt, resultInserted] = table_.emplace(
                 std::piecewise_construct,
-                std::make_tuple(kindInbound, address.at_port(0)),  // Key
-                std::make_tuple(m_clock.now()));                   // Entry
+                std::make_tuple(kindInbound, key),
+                std::make_tuple(m_clock.now()));
 
             entry = &resultIt->second;
             entry->key = &resultIt->first;

release-builder.sh

@@ -11,11 +11,11 @@ echo "START BUILDING (HOST)"
 echo "Cleaning previously built binary"
 rm -f release-build/xahaud
 
-BUILD_CORES=$(echo "scale=0 ; `nproc` / 1.337" | bc)
+BUILD_CORES=$(echo "scale=0 ; $(nproc) / 1.337" | bc)
 
 if [[ "$GITHUB_REPOSITORY" == "" ]]; then
   #Default
-  BUILD_CORES=${BUILD_CORES:-8} 
+  BUILD_CORES=${BUILD_CORES:-8}
 fi
 
 # Ensure still works outside of GH Actions by setting these to /dev/null
@@ -31,21 +31,19 @@ echo "-- GITHUB_SHA:        $GITHUB_SHA"
 echo "-- GITHUB_RUN_NUMBER: $GITHUB_RUN_NUMBER"
 echo "-- CONTAINER_NAME:    $CONTAINER_NAME"
 
-which docker 2> /dev/null 2> /dev/null
-if [ "$?" -eq "1" ]
-then
+which docker 2>/dev/null 2>/dev/null
+if [ "$?" -eq "1" ]; then
   echo 'Docker not found. Install it first.'
   exit 1
 fi
 
-stat .git 2> /dev/null 2> /dev/null
-if [ "$?" -eq "1" ]
-then
+stat .git 2>/dev/null 2>/dev/null
+if [ "$?" -eq "1" ]; then
   echo 'Run this inside the source directory. (.git dir not found).'
   exit 1
 fi
 
-STATIC_CONTAINER=$(docker ps -a | grep $CONTAINER_NAME |wc -l)
+STATIC_CONTAINER=$(docker ps -a | grep $CONTAINER_NAME | wc -l)
 
 CACHE_VOLUME_NAME="xahau-release-builder-cache"
 
@@ -57,13 +55,14 @@ if false; then
   docker stop $CONTAINER_NAME
 else
   echo "No static container, build on temp container"
-  rm -rf release-build;
-  mkdir -p release-build;
+  rm -rf release-build
+  mkdir -p release-build
 
   docker volume create $CACHE_VOLUME_NAME
 
   # Create inline Dockerfile with environment setup for build-full.sh
-  DOCKERFILE_CONTENT=$(cat <<'DOCKERFILE_EOF'
+  DOCKERFILE_CONTENT=$(
+    cat <<'DOCKERFILE_EOF'
 FROM ghcr.io/phusion/holy-build-box:4.0.1-amd64
 
 ARG BUILD_CORES=8
@@ -218,7 +217,7 @@ RUN /hbb_exe/activate-exec bash -c "ccache -M 100G && \
     ln -s ../../bin/ccache /usr/lib64/ccache/c++"
 
 DOCKERFILE_EOF
-)
+  )
 
   # Build custom Docker image
   IMAGE_NAME="xahaud-builder:latest"
@@ -228,14 +227,14 @@ DOCKERFILE_EOF
   if [[ "$GITHUB_REPOSITORY" == "" ]]; then
     # Non GH, local building
     echo "Non-GH runner, local building, temp container"
-    docker run -i --user 0:$(id -g) --rm -v /data/builds:/data/builds -v `pwd`:/io -v "$CACHE_VOLUME_NAME":/cache --network host "$IMAGE_NAME" /hbb_exe/activate-exec bash -c "source /opt/rh/gcc-toolset-11/enable && bash -x /io/build-full.sh '$GITHUB_REPOSITORY' '$GITHUB_SHA' '$BUILD_CORES' '$GITHUB_RUN_NUMBER'"
+    docker run -i --user 0:$(id -g) --rm -v /data/builds:/data/builds -v $(pwd):/io -v "$CACHE_VOLUME_NAME":/cache --network host "$IMAGE_NAME" /hbb_exe/activate-exec bash -c "source /opt/rh/gcc-toolset-11/enable && bash -x /io/build-full.sh '$GITHUB_REPOSITORY' '$GITHUB_SHA' '$BUILD_CORES' '$GITHUB_RUN_NUMBER'"
   else
     # GH Action, runner
     echo "GH Action, runner, clean & re-create create persistent container"
     docker rm -f $CONTAINER_NAME
-    echo "echo 'Stopping container: $CONTAINER_NAME'" >> "$JOB_CLEANUP_SCRIPT"
-    echo "docker stop --time=15 \"$CONTAINER_NAME\" || echo 'Failed to stop container or container not running'" >> "$JOB_CLEANUP_SCRIPT"
-    docker run -di --user 0:$(id -g) --name $CONTAINER_NAME -v /data/builds:/data/builds -v `pwd`:/io -v "$CACHE_VOLUME_NAME":/cache --network host "$IMAGE_NAME" /hbb_exe/activate-exec bash
+    echo "echo 'Stopping container: $CONTAINER_NAME'" >>"$JOB_CLEANUP_SCRIPT"
+    echo "docker stop --time=15 \"$CONTAINER_NAME\" || echo 'Failed to stop container or container not running'" >>"$JOB_CLEANUP_SCRIPT"
+    docker run -di --user 0:$(id -g) --name $CONTAINER_NAME -v /data/builds:/data/builds -v $(pwd):/io -v "$CACHE_VOLUME_NAME":/cache --network host "$IMAGE_NAME" /hbb_exe/activate-exec bash
     docker exec -i $CONTAINER_NAME /hbb_exe/activate-exec bash -c "source /opt/rh/gcc-toolset-11/enable && bash -x /io/build-full.sh '$GITHUB_REPOSITORY' '$GITHUB_SHA' '$BUILD_CORES' '$GITHUB_RUN_NUMBER'"
     docker stop $CONTAINER_NAME
   fi

src/libxrpl/basics/Log.cpp

@@ -31,6 +31,7 @@
 #include <cassert>
 #include <cstring>
 #include <ctime>
+#include <exception>
 #include <fstream>
 #include <functional>
 #include <iostream>
@@ -351,9 +352,18 @@ Logs::format(
 
     if (useLocalTime)
     {
-        auto now = std::chrono::system_clock::now();
-        auto local = date::make_zoned(date::current_zone(), now);
-        output = date::format(fmt, local);
+        try
+        {
+            auto now = std::chrono::system_clock::now();
+            auto local = date::make_zoned(date::current_zone(), now);
+            output = date::format(fmt, local);
+        }
+        catch (std::exception const&)
+        {
+            // Enhanced logging should not make startup fatal if tzdb lookup is
+            // unavailable or misconfigured. Fall back to UTC formatting.
+            output = date::format(fmt, std::chrono::system_clock::now());
+        }
     }
     else
     {

src/libxrpl/protocol/AMMCore.cpp

@@ -66,7 +66,7 @@ invalidAMMAsset(
     Issue const& issue,
     std::optional<std::pair<Issue, Issue>> const& pair)
 {
-    if (badCurrency() == issue.currency)
+    if (isBadCurrency(issue.currency))
         return temBAD_CURRENCY;
     if (isXRP(issue) && issue.account.isNonZero())
         return temBAD_ISSUER;

src/libxrpl/protocol/Feature.cpp

@@ -250,12 +250,9 @@ FeatureCollections::registerFeature(
     Feature const* i = getByName(name);
     if (!i)
     {
-        // If this check fails, and you just added a feature, increase the
-        // numFeatures value in Feature.h
         check(
             features.size() < detail::numFeatures,
-            "More features defined than allocated. Adjust numFeatures in "
-            "Feature.h.");
+            "More features defined than allocated.");
 
         auto const f = sha512Half(Slice(name.data(), name.size()));
 
@@ -424,45 +421,26 @@ featureToName(uint256 const& f)
 #undef XRPL_FEATURE
 #pragma push_macro("XRPL_FIX")
 #undef XRPL_FIX
+#pragma push_macro("XRPL_RETIRE")
+#undef XRPL_RETIRE
 
 #define XRPL_FEATURE(name, supported, vote) \
     uint256 const feature##name = registerFeature(#name, supported, vote);
 #define XRPL_FIX(name, supported, vote) \
     uint256 const fix##name = registerFeature("fix" #name, supported, vote);
+#define XRPL_RETIRE(name)                                                     \
+    [[deprecated("The referenced amendment has been retired"), maybe_unused]] \
+    uint256 const retired##name = retireFeature(#name);
 
 #include <xrpl/protocol/detail/features.macro>
 
+#undef XRPL_RETIRE
+#pragma pop_macro("XRPL_RETIRE")
 #undef XRPL_FIX
 #pragma pop_macro("XRPL_FIX")
 #undef XRPL_FEATURE
 #pragma pop_macro("XRPL_FEATURE")
 
-// clang-format off
-
-// The following amendments have been active for at least two years. Their
-// pre-amendment code has been removed and the identifiers are deprecated.
-// All known amendments and amendments that may appear in a validated
-// ledger must be registered either here or above with the "active" amendments
-[[deprecated("The referenced amendment has been retired"), maybe_unused]]
-uint256 const
-    retiredMultiSign         = retireFeature("MultiSign"),
-    retiredTrustSetAuth      = retireFeature("TrustSetAuth"),
-    retiredFeeEscalation     = retireFeature("FeeEscalation"),
-    retiredPayChan           = retireFeature("PayChan"),
-    retiredCryptoConditions  = retireFeature("CryptoConditions"),
-    retiredTickSize          = retireFeature("TickSize"),
-    retiredFix1368           = retireFeature("fix1368"),
-    retiredEscrow            = retireFeature("Escrow"),
-    retiredFix1373           = retireFeature("fix1373"),
-    retiredEnforceInvariants = retireFeature("EnforceInvariants"),
-    retiredSortedDirectories = retireFeature("SortedDirectories"),
-    retiredFix1201           = retireFeature("fix1201"),
-    retiredFix1512           = retireFeature("fix1512"),
-    retiredFix1523           = retireFeature("fix1523"),
-    retiredFix1528           = retireFeature("fix1528");
-
-// clang-format on
-
 // All of the features should now be registered, since variables in a cpp file
 // are initialized from top to bottom.
 //

src/libxrpl/protocol/Indexes.cpp

@@ -74,6 +74,7 @@ enum class LedgerNameSpace : std::uint16_t {
     HOOK_DEFINITION = 'D',
     EMITTED_TXN = 'E',
     EMITTED_DIR = 'F',
+    SHADOW_TICKET = 0x5374,  // St
     NFTOKEN_OFFER = 'q',
     NFTOKEN_BUY_OFFERS = 'h',
     NFTOKEN_SELL_OFFERS = 'i',
@@ -81,6 +82,7 @@ enum class LedgerNameSpace : std::uint16_t {
     IMPORT_VLSEQ = 'I',
     UNL_REPORT = 'R',
     CRON = 'L',
+    CONSENSUS_ENTROPY = 'X',
     AMM = 'A',
     BRIDGE = LEDGER_NAMESPACE2(0x01, 'H'),
     XCHAIN_CLAIM_ID = 'Q',
@@ -188,6 +190,15 @@ emittedTxn(uint256 const& id) noexcept
     return {ltEMITTED_TXN, indexHash(LedgerNameSpace::EMITTED_TXN, id)};
 }
 
+Keylet
+shadowTicket(AccountID const& account, std::uint32_t ticketSeq) noexcept
+{
+    return {
+        ltSHADOW_TICKET,
+        indexHash(
+            LedgerNameSpace::SHADOW_TICKET, account, std::uint32_t(ticketSeq))};
+}
+
 Keylet
 hook(AccountID const& id) noexcept
 {
@@ -546,6 +557,14 @@ cron(uint32_t timestamp, std::optional<AccountID> const& id)
     return {ltCRON, uint256::fromVoid(h)};
 }
 
+Keylet const&
+consensusEntropy() noexcept
+{
+    static Keylet const ret{
+        ltCONSENSUS_ENTROPY, indexHash(LedgerNameSpace::CONSENSUS_ENTROPY)};
+    return ret;
+}
+
 Keylet
 amm(Asset const& issue1, Asset const& issue2) noexcept
 {

src/libxrpl/protocol/InnerObjectFormats.cpp

@@ -78,6 +78,7 @@ InnerObjectFormats::InnerObjectFormats()
          {sfHookExecutionIndex, soeREQUIRED},
          {sfHookStateChangeCount, soeREQUIRED},
          {sfHookEmitCount, soeREQUIRED},
+         {sfHookExportCount, soeOPTIONAL},
          {sfFlags, soeOPTIONAL}});
 
     add(sfHookEmission.jsonName,
@@ -99,6 +100,7 @@ InnerObjectFormats::InnerObjectFormats()
          {sfHookOnOutgoing, soeOPTIONAL},
          {sfHookCanEmit, soeOPTIONAL},
          {sfHookApiVersion, soeOPTIONAL},
+         {sfHookName, soeOPTIONAL},
          {sfFlags, soeOPTIONAL}});
 
     add(sfHookGrant.jsonName,
@@ -253,6 +255,24 @@ InnerObjectFormats::InnerObjectFormats()
             {sfIssuer, soeREQUIRED},
             {sfCredentialType, soeREQUIRED},
         });
+
+    add(sfHighReward.jsonName,
+        sfHighReward.getCode(),
+        {
+            {sfRewardLgrFirst, soeREQUIRED},
+            {sfRewardLgrLast, soeREQUIRED},
+            {sfRewardTime, soeREQUIRED},
+            {sfTrustLineRewardAccumulator, soeREQUIRED},
+        });
+
+    add(sfLowReward.jsonName,
+        sfLowReward.getCode(),
+        {
+            {sfRewardLgrFirst, soeREQUIRED},
+            {sfRewardLgrLast, soeREQUIRED},
+            {sfRewardTime, soeREQUIRED},
+            {sfTrustLineRewardAccumulator, soeREQUIRED},
+        });
 }
 
 InnerObjectFormats const&

src/libxrpl/protocol/Issue.cpp

@@ -111,7 +111,7 @@ issueFromJson(Json::Value const& v)
     }
 
     auto const currency = to_currency(curStr.asString());
-    if (currency == badCurrency() || currency == noCurrency())
+    if (isBadCurrency(currency) || currency == noCurrency())
     {
         Throw<Json::error>("issueFromJson currency must be a valid currency");
     }

src/libxrpl/protocol/STCurrency.cpp

@@ -103,7 +103,7 @@ currencyFromJson(SField const& name, Json::Value const& v)
     }
 
     auto const currency = to_currency(v.asString());
-    if (currency == badCurrency() || currency == noCurrency())
+    if (isBadCurrency(currency) || currency == noCurrency())
     {
         Throw<std::runtime_error>(
             "currencyFromJson currency must be a valid currency");

src/libxrpl/protocol/STTx.cpp

@@ -684,7 +684,8 @@ isPseudoTx(STObject const& tx)
 
     auto tt = safe_cast<TxType>(*t);
     return tt == ttAMENDMENT || tt == ttFEE || tt == ttUNL_MODIFY ||
-        tt == ttEMIT_FAILURE || tt == ttUNL_REPORT || tt == ttCRON;
+        tt == ttEMIT_FAILURE || tt == ttUNL_REPORT || tt == ttCRON ||
+        tt == ttCONSENSUS_ENTROPY;
 }
 
 }  // namespace ripple

src/libxrpl/protocol/TER.cpp

@@ -124,6 +124,7 @@ transResults()
         MAKE_ERROR(tecARRAY_TOO_LARGE,               "Array is too large."),
         MAKE_ERROR(tecLOCKED,                        "Fund is locked."),
         MAKE_ERROR(tecBAD_CREDENTIALS,               "Bad credentials."),
+        MAKE_ERROR(tecEXPORT_EXPIRED,                "Export expired without reaching signature quorum."),
 
         MAKE_ERROR(tefALREADY,                     "The exact transaction was already in this ledger."),
         MAKE_ERROR(tefBAD_ADD_AUTH,                "Not authorized to add account."),
@@ -171,6 +172,7 @@ transResults()
         MAKE_ERROR(telNON_LOCAL_EMITTED_TXN, "Emitted transaction cannot be applied because it was not generated locally."),
         MAKE_ERROR(telIMPORT_VL_KEY_NOT_RECOGNISED, "Import vl key was not recognized."),
         MAKE_ERROR(telCAN_NOT_QUEUE_IMPORT,   "Import transaction was not able to be directly applied and cannot be queued."),
+        MAKE_ERROR(telSHADOW_TICKET_REQUIRED, "The imported transaction uses a TicketSequence but no shadow ticket exists."),
         MAKE_ERROR(telENV_RPC_FAILED,         "Unit test RPC failure."),
 
         MAKE_ERROR(temMALFORMED,                 "Malformed transaction."),
@@ -238,6 +240,7 @@ transResults()
         MAKE_ERROR(terPRE_TICKET,             "Ticket is not yet in ledger."),
         MAKE_ERROR(terNO_HOOK,                "No hook with that hash exists on the ledger."),
         MAKE_ERROR(terNO_AMM,                 "AMM doesn't exist for the asset pair."),
+        MAKE_ERROR(terRETRY_EXPORT,          "Export awaiting validator signatures."),
 
         MAKE_ERROR(tesSUCCESS,                "The transaction was applied. Only final in a validated ledger."),
         MAKE_ERROR(tesPARTIAL,                "The transaction was applied but should be submitted again until returning tesSUCCESS."),

src/libxrpl/protocol/TxFormats.cpp

@@ -48,6 +48,7 @@ TxFormats::TxFormats()
         {sfFirstLedgerSequence, soeOPTIONAL},
         {sfNetworkID, soeOPTIONAL},
         {sfHookParameters, soeOPTIONAL},
+        {sfHookName, soeOPTIONAL},
     };
 
 #pragma push_macro("UNWRAP")

src/libxrpl/protocol/TxMeta.cpp

@@ -49,6 +49,11 @@ TxMeta::TxMeta(
 
     if (obj.isFieldPresent(sfHookEmissions))
         setHookEmissions(obj.getFieldArray(sfHookEmissions));
+
+    if (obj.isFieldPresent(sfExportResult))
+        setExportResult(const_cast<STObject&>(obj)
+                            .getField(sfExportResult)
+                            .downcast<STObject>());
 }
 
 TxMeta::TxMeta(uint256 const& txid, std::uint32_t ledger, STObject const& obj)
@@ -75,6 +80,11 @@ TxMeta::TxMeta(uint256 const& txid, std::uint32_t ledger, STObject const& obj)
 
     if (obj.isFieldPresent(sfHookEmissions))
         setHookEmissions(obj.getFieldArray(sfHookEmissions));
+
+    if (obj.isFieldPresent(sfExportResult))
+        setExportResult(const_cast<STObject&>(obj)
+                            .getField(sfExportResult)
+                            .downcast<STObject>());
 }
 
 TxMeta::TxMeta(uint256 const& txid, std::uint32_t ledger, Blob const& vec)
@@ -245,6 +255,14 @@ TxMeta::getAsObject() const
     if (hasHookEmissions())
         metaData.setFieldArray(sfHookEmissions, getHookEmissions());
 
+    if (hasExportResult())
+    {
+        Serializer s;
+        mExportResult->add(s);
+        SerialIter sit(s.slice());
+        metaData.emplace_back(STObject(sit, sfExportResult));
+    }
+
     return metaData;
 }