Fix: pin final PC to halt

bin/cli/src/main.rs

@@ -1044,6 +1044,12 @@ fn continuation_epoch_size(epoch_size_log2: u32) -> Result<usize, String> {
             "--epoch-size-log2 must be at least {MIN_CONTINUATION_EPOCH_SIZE_LOG2} for CLI proving"
         ));
     }
+    let max = prover::tables::cpu::MAX_EPOCH_SIZE_LOG2;
+    if epoch_size_log2 > max {
+        return Err(format!(
+            "--epoch-size-log2 must be at most {max} (an epoch has fewer than 2^30 CPU rows)"
+        ));
+    }
     1usize.checked_shl(epoch_size_log2).ok_or_else(|| {
         format!("--epoch-size-log2 {epoch_size_log2} is too large for this platform")
     })
@@ -1189,6 +1195,12 @@ mod tests {
         assert!(continuation_epoch_size(17).is_err());
     }
 
+    #[test]
+    fn continuation_epoch_size_rejects_epochs_over_the_cpu_row_bound() {
+        assert!(continuation_epoch_size(prover::tables::cpu::MAX_EPOCH_SIZE_LOG2).is_ok());
+        assert!(continuation_epoch_size(prover::tables::cpu::MAX_EPOCH_SIZE_LOG2 + 1).is_err());
+    }
+
     #[test]
     fn continuation_epoch_size_uses_exact_power_of_two() {
         assert_eq!(continuation_epoch_size(20).unwrap(), 1 << 20);

docs/continuations_design.md

@@ -93,6 +93,15 @@ an epoch. The cross-epoch chain is ordered by the **epoch number** (§3.3), so t
 GlobalMemory bus carries no timestamp at all (see §2 telescoping). `fini_timestamp`
 stays only because the epoch-local **Memory bus** needs it (matched against MEMW).
 
+The CPU timestamp is a **preprocessed** column (spec `Timestamp`): row `i` of every
+CPU table holds `4·(i + 1)`. An epoch splits its CPU rows over several tables, so
+table `k` adds `4·S_k` to every timestamp it sends, where `S_k` is the total
+height of tables `0..k`. The verifier reads the heights off the epoch proof, so
+every CPU timestamp, and the final PC timestamp `4·N + 1` (`N` = all CPU rows of
+the epoch), is verifier-known. The verifier rejects an epoch with more than
+`2^30 − 1` CPU rows: the last row's accesses reach `4·N + 2`, which must stay
+below HALT's `2^32 − 1`.
+
 ### Cross-epoch telescoping
 
 For a cell touched in epochs 1, 2, 3, the GlobalMemory bus checks:
@@ -441,9 +450,9 @@ global telescoping — we bind the whole snapshot directly.
 
 **Mechanism (no new bus).** The REGISTER table is the register analog of PAGE — it
 already puts each register's init/fini tokens on the epoch-local Memory bus
-(REG-C1 init, REG-C2 fini, matched against MEMW). For continuation epochs we
-**also preprocess the FINI column** = the epoch's final register file `R_{i+1}`
-(on top of the already-preprocessed INIT = `R_i`). "Preprocessed" means
+(REG-C1 init, REG-C2 fini, matched against MEMW). Every REGISTER table
+**preprocesses the FINI column** as well as INIT. For a continuation epoch, FINI
+is the epoch's final register file `R_{i+1}` (and INIT = `R_i`). "Preprocessed" means
 *verifier-known*: the verifier recomputes the column's commitment, so the prover
 cannot choose it. The verifier reuses the **same** `R_{i+1}` as epoch *i*'s FINI
 and epoch *i+1*'s INIT, so `init(i+1) == fini(i)` **by construction** — no equality
@@ -470,8 +479,16 @@ locks compose:
 Compose them: public `R_{i+1}` = trace FINI = real last write. So the value handed
 to the next epoch is pinned to real execution.
 
-The **monolithic prover is unchanged**: it keeps FINI as a main-trace column (it
-has no verifier-known final state) and preprocesses 2 columns, not 3.
+The **monolithic prover** preprocesses the same columns, with FINI pinned to the
+halted register file (`register::halted_fini`): x1-x31 = 0, x254 = the committed
+byte count, and the PC = 1. The final epoch's `R_{i+1}` must equal that same
+halted state. Pinning it ends the PC chain on `pc = 1`, so execution cannot
+continue past the exit ecall.
+
+REGISTER also preprocesses `IS_PC` (1 on the two x255 rows). REG-C2 sends the x255
+final token at the verifier-known final PC timestamp `4·N + 1` instead of the
+`timestamp` column (spec `halt.typ`), so both the value and the timestamp the PC
+chain ends on are verifier-known.
 
 ### Commit index (x254)
 
@@ -642,8 +659,10 @@ recursion/aggregation layer (deferred).
 - `prover/src/tables/global_memory.rs` — the genesis (ELF-bound for ELF/runtime pages,
   committed/private for private-input pages, §3.6) and finalization anchors.
 - `prover/src/tables/register.rs` — the REGISTER table: REG-C1/REG-C2 Memory-bus
-  tokens, the preprocessed FINI commitment (`compute_precomputed_commitment_with_fini`,
-  `NUM_PREPROCESSED_COLS_WITH_FINI`), and `fini_from_trace`.
+  tokens, the preprocessed FINI commitment (`compute_precomputed_commitment`,
+  `NUM_PREPROCESSED_COLS`), `fini_from_trace`, and the halted register
+  file that monolithic proofs and the final epoch pin FINI to (`halted_fini`,
+  `halted_commitment`).
 - `prover/src/statement.rs` — the Fiat-Shamir statement absorbers
   (`absorb_statement` with `StatementKind`, `absorb_continuation_global_statement`).
 - `prover/src/continuation.rs` — the split prover/verifier: `prove_continuation` /

executor/programs/asm/poc_halt_continue.s

@@ -0,0 +1,36 @@
+	.text
+	.attribute	5, "rv64i2p1"
+	.globl	main
+main:
+	# Two rows before the exit sequence, so the rows before the exit ecall fill a
+	# power-of-two continuation epoch (4 rows) on their own.
+	nop
+	nop
+
+	# Exit with a NON-ZERO code. HALT enforces x10 == 0, so an honest prover
+	# cannot prove this program.
+	li	a0, 1
+	li	a7, 93			# syscall = Halt
+	ecall
+
+	# Never reached by an honest execution. The HALT PoC runs these rows AFTER
+	# the exit ecall to zero x10 before the trace ends.
+	li	a0, 0
+	nop
+	nop
+	nop
+	nop
+	nop
+	nop
+	nop
+	nop
+	nop
+	nop
+	nop
+	nop
+	nop
+	nop
+
+	# Lets the PoC's patched copy (first ecall -> nop) terminate in the executor.
+	li	a7, 93
+	ecall

executor/programs/asm/poc_pc_double_read.s

@@ -0,0 +1,14 @@
+	.text
+	.attribute	5, "rv64i2p1"
+	.globl	main
+main:
+	# Exits with code 5. HALT enforces x10 == 0, so an honest prover cannot
+	# prove this program.
+	li	a0, 5
+	# The PoC proves this row with pc_double_read = 1 one timestamp after the
+	# previous row, so its read of a0 lands before the write above and returns
+	# the stale initial a0 = 0.
+	mv	a1, a0
+	mv	a0, a1
+	li	a7, 93			# syscall = Halt
+	ecall

prover/src/auto_storage.rs

@@ -120,8 +120,8 @@ fn table_specs(lengths: &TableLengths) -> Vec<TableSpec> {
         (
             lengths.cpu_padded_rows,
             CPU_COLS as u64,
-            aux_cols(cpu_buses().len()),
-            1,
+            aux_cols(cpu_buses(0).len()),
+            2, // TIMESTAMP is preprocessed: see the note above BITWISE
         ),
         (
             lengths.memw_padded_rows,
@@ -183,10 +183,10 @@ fn table_specs(lengths: &TableLengths) -> Vec<TableSpec> {
             aux_cols(copy_buses().len()),
             1,
         ),
-        // BITWISE / DECODE / PAGE / REGISTER take the preprocessed-trace commit
-        // path: it extracts ALL columns into the LDE and builds two Merkle trees
-        // (precomputed_tree + mult_tree), so main_cols = full NUM_COLUMNS and
-        // main_trees = 2.
+        // BITWISE / DECODE / PAGE / REGISTER, and CPU above, take the
+        // preprocessed-trace commit path: it extracts ALL columns into the LDE and
+        // builds two Merkle trees (precomputed_tree + mult_tree), so main_cols =
+        // full NUM_COLUMNS and main_trees = 2.
         (
             bitwise_rows,
             BITWISE_COLS as u64,
@@ -203,7 +203,7 @@ fn table_specs(lengths: &TableLengths) -> Vec<TableSpec> {
         (
             register_rows,
             REGISTER_COLS as u64,
-            aux_cols(register_buses().len()),
+            aux_cols(register_buses(0).len()),
             2,
         ),
     ];

prover/src/bin/compute_static_commitments.rs

@@ -2,6 +2,8 @@
 //! for a fixed set of `blowup_factor` values. The output is pasted into the
 //! `static_commitment` match bodies in `prover/src/tables/{bitwise,keccak_rc}.rs`
 //! and the `static_zero_page_commitment` match body in `prover/src/tables/page.rs`.
+//! It then prints the CPU timestamp table, pasted over
+//! `prover/src/tables/cpu_timestamp_commitments.rs`.
 //! The `static_commitments_tests` test suite pins the values so any drift in
 //! the AIR or FFT pipeline is caught at test time.
 //!
@@ -13,7 +15,7 @@
 //! `keccak_rc.rs` and `static_zero_page_commitment` in `page.rs` for when
 //! it's actually appropriate to bless new bytes.
 
-use lambda_vm_prover::tables::{STATIC_BLOWUP_FACTORS, bitwise, keccak_rc, page};
+use lambda_vm_prover::tables::{STATIC_BLOWUP_FACTORS, bitwise, cpu, keccak_rc, max_rows, page};
 use stark::config::Commitment;
 use stark::proof::options::GoldilocksCubicProofOptions;
 
@@ -72,4 +74,28 @@ fn main() {
             private_page_fmt = format_commitment(&private_page),
         );
     }
+
+    // ---- CPU timestamp (one commitment per table height):
+    println!(
+        "// Generated by `cargo run --bin compute_static_commitments --release`.\n\
+         // Do not edit by hand; see `static_timestamp_commitment`.\n\n\
+         /// `(blowup_factor, [commitment for log2(height) = MIN_LOG_HEIGHT..])`.\n\
+         const CPU_TIMESTAMP_COMMITMENTS: &[(u8, &[Commitment])] = &["
+    );
+    for &blowup in STATIC_BLOWUP_FACTORS {
+        let Ok(options) = GoldilocksCubicProofOptions::with_blowup(blowup) else {
+            continue;
+        };
+        println!("    (\n        {blowup},\n        &[");
+        for log_height in cpu::MIN_LOG_HEIGHT..=max_rows::CPU.trailing_zeros() {
+            let commitment = cpu::compute_timestamp_commitment(&options, 1 << log_height);
+            println!("            // 2^{log_height}");
+            println!(
+                "            {},",
+                format_commitment(&commitment).replace("\n    ", "\n        ")
+            );
+        }
+        println!("        ],\n    ),");
+    }
+    println!("];");
 }

prover/src/constraints/cpu.rs

@@ -37,15 +37,14 @@ pub const BIT_FLAG_COLUMNS: &[usize] = &[
     cols::BRANCH,
     cols::ECALL,
     cols::PC_DOUBLE_READ,
-    cols::PREV_PC_TIMESTAMP_BORROW,
 ];
 
 // =========================================================================
 // Assembly
 // =========================================================================
 
 /// Total number of CPU transition constraints (excludes bus lookups):
-/// - IS_BIT: 12
+/// - IS_BIT: 11
 /// - decode mutex: 6 (`word_instr · {MEMORY, BRANCH, ECALL, WRITE_REGISTER,
 ///   READ_REGISTER1, READ_REGISTER2}`)
 /// - ADD pair: 2, SUB pair: 2
@@ -56,7 +55,7 @@ pub const BIT_FLAG_COLUMNS: &[usize] = &[
 /// - branch_cond: 1
 /// - next_pc: 2
 /// - assumptions: 4 (MEMORY·BRANCH mutex 1 + arg2 exclusivity 2 + mem_flags IS_BIT 1)
-pub const NUM_CPU_CONSTRAINTS: usize = 12 + 6 + 2 + 2 + 2 + 4 + 2 + 2 + 1 + 2 + 4;
+pub const NUM_CPU_CONSTRAINTS: usize = 11 + 6 + 2 + 2 + 2 + 4 + 2 + 2 + 1 + 2 + 4;
 
 // =========================================================================
 // Single-body emit functions (ConstraintBuilder front-end)
@@ -355,7 +354,9 @@ impl ConstraintSet<GoldilocksField, GoldilocksExtension> for CpuConstraints {
         emit_branch_cond(b, idx);
         idx += 1;
 
-        // idx 33,34: next_pc = pc + instruction_length.
+        // idx 33,34: next_pc = pc + instruction_length. With pc even and an even
+        // length, next_pc stays even, so no real row writes `next_pc = 1` (the final
+        // PC pinned in `register::halted_fini`).
         emit_next_pc_add_pair(b, idx);
         idx += 2;