add doc and debug_assert

Author: nicole-graus

prover/src/continuation.rs

@@ -123,6 +123,14 @@ fn l2g_constraints()
 ///
 /// `epoch_label` is this epoch's 1-based label; it is the `fini_epoch` constant
 /// the fini token carries (not a trace column, since it's the same for every row).
+///
+/// Uses `empty_constraints()` deliberately: the MU boolean (`MU·(1-MU)=0`), the
+/// column range checks, and the `init_epoch < fini_epoch` ordering are NOT
+/// re-asserted here. They are enforced once in the epoch proof's `l2g_memory_air`,
+/// and `verify_l2g_commitment_binding` ties this global L2G sub-table to the *same*
+/// committed trace (equal Merkle roots). So under collision resistance the trace the
+/// global bus runs over already satisfies all those constraints — do not add them
+/// here (it would be redundant, not a missing check).
 fn l2g_global_air(
     opts: &ProofOptions,
     epoch_label: u64,

prover/src/tables/global_memory.rs

@@ -189,6 +189,10 @@ pub fn bus_interactions(page_base: u64) -> Vec<BusInteraction> {
             ],
         ),
         // GM-FINAL: receive the finalization token [address, fini, fini_epoch].
+        // Note: FINI has no explicit AreBytes range check here (unlike PAGE's fini).
+        // It's byte-checked transitively: this receiver must match an L2G fini token
+        // on the GlobalMemory bus, and L2G already AreBytes-checks its fini value. So
+        // a non-byte FINI could never balance. Do not "add a missing AreBytes" here.
         BusInteraction::receiver(
             BusId::GlobalMemory,
             Multiplicity::One,

prover/src/tables/local_to_global.rs

@@ -409,6 +409,11 @@ pub fn memory_bus_interactions() -> Vec<BusInteraction> {
 /// trace, so its columns inherit the same guarantee via the commitment binding.
 /// Keep this in sync with [`collect_bitwise_from_l2g`].
 pub fn range_check_interactions(epoch_label: u64) -> Vec<BusInteraction> {
+    // `epoch_label` is a 1-based fini epoch, never `GENESIS_EPOCH` (0): genesis is
+    // only ever an `init`/originating epoch, never a fini. The ordering term below
+    // computes `epoch_label - 1 - init_epoch`, so a 0 label would make the constant
+    // `-1` (field `p-1`) and no honest prover could satisfy the IsB20 check.
+    debug_assert!(epoch_label >= 1, "epoch_label must be a 1-based fini epoch");
     let mut interactions = Vec::with_capacity(2 + cols::RANGE_CHECKED_HALFWORDS.len());
     interactions.push(BusInteraction::sender(
         BusId::AreBytes,