From cd871c04396c2d262617a40dc28b0e76d44e52ec Mon Sep 17 00:00:00 2001
From: Robin Salen <salenrobin@gmail.com>
Date: Thu, 28 Sep 2023 15:39:10 -0400
Subject: [PATCH 1/5] Make gas fit in 2 limbs

---
 evm/src/cpu/columns/mod.rs          |  4 +-
 evm/src/cpu/gas.rs                  | 34 ++++++------
 evm/src/cpu/jumps.rs                | 13 +++--
 evm/src/cpu/syscalls_exceptions.rs  | 21 ++++----
 evm/src/fixed_recursive_verifier.rs | 26 +++++----
 evm/src/generation/mod.rs           |  5 +-
 evm/src/get_challenges.rs           | 16 +++---
 evm/src/proof.rs                    | 83 +++++++++++++++++------------
 evm/src/recursive_verifier.rs       | 72 ++++++++++++++-----------
 evm/src/witness/operation.rs        |  6 +--
 evm/src/witness/transition.rs       |  5 +-
 11 files changed, 167 insertions(+), 118 deletions(-)

diff --git a/evm/src/cpu/columns/mod.rs b/evm/src/cpu/columns/mod.rs
index fecc8df986..cc98fceb3f 100644
--- a/evm/src/cpu/columns/mod.rs
+++ b/evm/src/cpu/columns/mod.rs
@@ -58,8 +58,8 @@ pub struct CpuColumnsView<T: Copy> {
     /// If CPU cycle: We're in kernel (privileged) mode.
     pub is_kernel_mode: T,
 
-    /// If CPU cycle: Gas counter.
-    pub gas: T,
+    /// If CPU cycle: Gas counter, split in two 32-bit limbs in little-endian order.
+    pub gas: [T; 2],
 
     /// If CPU cycle: flags for EVM instructions (a few cannot be shared; see the comments in
     /// `OpsColumnsView`).
diff --git a/evm/src/cpu/gas.rs b/evm/src/cpu/gas.rs
index 51f375c056..ae923fde6b 100644
--- a/evm/src/cpu/gas.rs
+++ b/evm/src/cpu/gas.rs
@@ -70,20 +70,22 @@ fn eval_packed_accumulate<P: PackedField>(
         })
         .sum();
 
-    let constr = nv.gas - (lv.gas + gas_used);
+    let gas_diff = nv.gas[1] * P::Scalar::from_canonical_u64(1 << 32) + nv.gas[0]
+        - (lv.gas[1] * P::Scalar::from_canonical_u64(1 << 32) + lv.gas[0]);
+    let constr = gas_diff - gas_used;
     yield_constr.constraint_transition(filter * constr);
 
     for (maybe_cost, op_flag) in izip!(SIMPLE_OPCODES.into_iter(), lv.op.into_iter()) {
         if let Some(cost) = maybe_cost {
             let cost = P::Scalar::from_canonical_u32(cost);
-            yield_constr.constraint_transition(op_flag * (nv.gas - lv.gas - cost));
+            yield_constr.constraint_transition(op_flag * (gas_diff - cost));
         }
     }
 
     // For jumps.
     let jump_gas_cost = P::Scalar::from_canonical_u32(G_MID.unwrap())
         + lv.opcode_bits[0] * P::Scalar::from_canonical_u32(G_HIGH.unwrap() - G_MID.unwrap());
-    yield_constr.constraint_transition(lv.op.jumps * (nv.gas - lv.gas - jump_gas_cost));
+    yield_constr.constraint_transition(lv.op.jumps * (gas_diff - jump_gas_cost));
 
     // For binary_ops.
     // MUL, DIV and MOD are differentiated from ADD, SUB, LT, GT and BYTE by their first and fifth bits set to 0.
@@ -92,13 +94,13 @@ fn eval_packed_accumulate<P: PackedField>(
         + cost_filter
             * (P::Scalar::from_canonical_u32(G_VERYLOW.unwrap())
                 - P::Scalar::from_canonical_u32(G_LOW.unwrap()));
-    yield_constr.constraint_transition(lv.op.binary_op * (nv.gas - lv.gas - binary_op_cost));
+    yield_constr.constraint_transition(lv.op.binary_op * (gas_diff - binary_op_cost));
 
     // For ternary_ops.
     // SUBMOD is differentiated by its second bit set to 1.
     let ternary_op_cost = P::Scalar::from_canonical_u32(G_MID.unwrap())
         - lv.opcode_bits[1] * P::Scalar::from_canonical_u32(G_MID.unwrap());
-    yield_constr.constraint_transition(lv.op.ternary_op * (nv.gas - lv.gas - ternary_op_cost));
+    yield_constr.constraint_transition(lv.op.ternary_op * (gas_diff - ternary_op_cost));
 }
 
 fn eval_packed_init<P: PackedField>(
@@ -111,7 +113,8 @@ fn eval_packed_init<P: PackedField>(
     // `nv` is the first row that executes an instruction.
     let filter = (is_cpu_cycle - P::ONES) * is_cpu_cycle_next;
     // Set initial gas to zero.
-    yield_constr.constraint_transition(filter * nv.gas);
+    yield_constr.constraint_transition(filter * nv.gas[0]);
+    yield_constr.constraint_transition(filter * nv.gas[1]);
 }
 
 pub fn eval_packed<P: PackedField>(
@@ -154,16 +157,18 @@ fn eval_ext_circuit_accumulate<F: RichField + Extendable<D>, const D: usize>(
         },
     );
 
-    let constr = {
-        let t = builder.add_extension(lv.gas, gas_used);
-        builder.sub_extension(nv.gas, t)
-    };
+    let nv_gas =
+        builder.mul_const_add_extension(F::from_canonical_u64(1 << 32), nv.gas[1], nv.gas[0]);
+    let lv_gas =
+        builder.mul_const_add_extension(F::from_canonical_u64(1 << 32), lv.gas[1], lv.gas[0]);
+    let nv_lv_diff = builder.sub_extension(nv_gas, lv_gas);
+
+    let constr = builder.sub_extension(nv_lv_diff, gas_used);
     let filtered_constr = builder.mul_extension(filter, constr);
     yield_constr.constraint_transition(builder, filtered_constr);
 
     for (maybe_cost, op_flag) in izip!(SIMPLE_OPCODES.into_iter(), lv.op.into_iter()) {
         if let Some(cost) = maybe_cost {
-            let nv_lv_diff = builder.sub_extension(nv.gas, lv.gas);
             let constr = builder.arithmetic_extension(
                 F::ONE,
                 -F::from_canonical_u32(cost),
@@ -184,7 +189,6 @@ fn eval_ext_circuit_accumulate<F: RichField + Extendable<D>, const D: usize>(
     let jump_gas_cost =
         builder.add_const_extension(jump_gas_cost, F::from_canonical_u32(G_MID.unwrap()));
 
-    let nv_lv_diff = builder.sub_extension(nv.gas, lv.gas);
     let gas_diff = builder.sub_extension(nv_lv_diff, jump_gas_cost);
     let constr = builder.mul_extension(filter, gas_diff);
     yield_constr.constraint_transition(builder, constr);
@@ -204,7 +208,6 @@ fn eval_ext_circuit_accumulate<F: RichField + Extendable<D>, const D: usize>(
     let binary_op_cost =
         builder.add_const_extension(binary_op_cost, F::from_canonical_u32(G_LOW.unwrap()));
 
-    let nv_lv_diff = builder.sub_extension(nv.gas, lv.gas);
     let gas_diff = builder.sub_extension(nv_lv_diff, binary_op_cost);
     let constr = builder.mul_extension(filter, gas_diff);
     yield_constr.constraint_transition(builder, constr);
@@ -219,7 +222,6 @@ fn eval_ext_circuit_accumulate<F: RichField + Extendable<D>, const D: usize>(
     let ternary_op_cost =
         builder.add_const_extension(ternary_op_cost, F::from_canonical_u32(G_MID.unwrap()));
 
-    let nv_lv_diff = builder.sub_extension(nv.gas, lv.gas);
     let gas_diff = builder.sub_extension(nv_lv_diff, ternary_op_cost);
     let constr = builder.mul_extension(filter, gas_diff);
     yield_constr.constraint_transition(builder, constr);
@@ -236,7 +238,9 @@ fn eval_ext_circuit_init<F: RichField + Extendable<D>, const D: usize>(
     let is_cpu_cycle_next = builder.add_many_extension(COL_MAP.op.iter().map(|&col_i| nv[col_i]));
     let filter = builder.mul_sub_extension(is_cpu_cycle, is_cpu_cycle_next, is_cpu_cycle_next);
     // Set initial gas to zero.
-    let constr = builder.mul_extension(filter, nv.gas);
+    let constr = builder.mul_extension(filter, nv.gas[0]);
+    yield_constr.constraint_transition(builder, constr);
+    let constr = builder.mul_extension(filter, nv.gas[1]);
     yield_constr.constraint_transition(builder, constr);
 }
 
diff --git a/evm/src/cpu/jumps.rs b/evm/src/cpu/jumps.rs
index 62d9bdfd25..1829177384 100644
--- a/evm/src/cpu/jumps.rs
+++ b/evm/src/cpu/jumps.rs
@@ -23,9 +23,8 @@ pub fn eval_packed_exit_kernel<P: PackedField>(
     // but we trust the kernel to set them to zero).
     yield_constr.constraint_transition(filter * (input[0] - nv.program_counter));
     yield_constr.constraint_transition(filter * (input[1] - nv.is_kernel_mode));
-    yield_constr.constraint_transition(filter * (input[6] - nv.gas));
-    // High limb of gas must be 0 for convenient detection of overflow.
-    yield_constr.constraint(filter * input[7]);
+    yield_constr.constraint_transition(filter * (input[6] - nv.gas[0]));
+    yield_constr.constraint_transition(filter * (input[7] - nv.gas[1]));
 }
 
 pub fn eval_ext_circuit_exit_kernel<F: RichField + Extendable<D>, const D: usize>(
@@ -50,14 +49,14 @@ pub fn eval_ext_circuit_exit_kernel<F: RichField + Extendable<D>, const D: usize
     yield_constr.constraint_transition(builder, kernel_constr);
 
     {
-        let diff = builder.sub_extension(input[6], nv.gas);
+        let diff = builder.sub_extension(input[6], nv.gas[0]);
         let constr = builder.mul_extension(filter, diff);
         yield_constr.constraint_transition(builder, constr);
     }
     {
-        // High limb of gas must be 0 for convenient detection of overflow.
-        let constr = builder.mul_extension(filter, input[7]);
-        yield_constr.constraint(builder, constr);
+        let diff = builder.sub_extension(input[7], nv.gas[1]);
+        let constr = builder.mul_extension(filter, diff);
+        yield_constr.constraint_transition(builder, constr);
     }
 }
 
diff --git a/evm/src/cpu/syscalls_exceptions.rs b/evm/src/cpu/syscalls_exceptions.rs
index abc47baf73..f9ea9a0a9f 100644
--- a/evm/src/cpu/syscalls_exceptions.rs
+++ b/evm/src/cpu/syscalls_exceptions.rs
@@ -99,7 +99,8 @@ pub fn eval_packed<P: PackedField>(
     // Maintain current context
     yield_constr.constraint_transition(total_filter * (nv.context - lv.context));
     // Reset gas counter to zero.
-    yield_constr.constraint_transition(total_filter * nv.gas);
+    yield_constr.constraint_transition(total_filter * nv.gas[0]);
+    yield_constr.constraint_transition(total_filter * nv.gas[1]);
 
     // This memory channel is constrained in `stack.rs`.
     let output = lv.mem_channels[NUM_GP_CHANNELS - 1].value;
@@ -108,9 +109,9 @@ pub fn eval_packed<P: PackedField>(
     yield_constr.constraint(filter_exception * (output[0] - lv.program_counter));
     // Check the kernel mode, for syscalls only
     yield_constr.constraint(filter_syscall * (output[1] - lv.is_kernel_mode));
-    yield_constr.constraint(total_filter * (output[6] - lv.gas));
-    // TODO: Range check `output[6]`.
-    yield_constr.constraint(total_filter * output[7]); // High limb of gas is zero.
+    // TODO: Range check `output[6] and output[7]`.
+    yield_constr.constraint(total_filter * (output[6] - lv.gas[0]));
+    yield_constr.constraint(total_filter * (output[7] - lv.gas[1]));
 
     // Zero the rest of that register
     // output[1] is 0 for exceptions, but not for syscalls
@@ -265,7 +266,9 @@ pub fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
     }
     // Reset gas counter to zero.
     {
-        let constr = builder.mul_extension(total_filter, nv.gas);
+        let constr = builder.mul_extension(total_filter, nv.gas[0]);
+        yield_constr.constraint_transition(builder, constr);
+        let constr = builder.mul_extension(total_filter, nv.gas[1]);
         yield_constr.constraint_transition(builder, constr);
     }
 
@@ -290,15 +293,15 @@ pub fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
         let constr = builder.mul_extension(filter_syscall, diff);
         yield_constr.constraint(builder, constr);
     }
+    // TODO: Range check `output[6]` and `output[7].
     {
-        let diff = builder.sub_extension(output[6], lv.gas);
+        let diff = builder.sub_extension(output[6], lv.gas[0]);
         let constr = builder.mul_extension(total_filter, diff);
         yield_constr.constraint(builder, constr);
     }
-    // TODO: Range check `output[6]`.
     {
-        // High limb of gas is zero.
-        let constr = builder.mul_extension(total_filter, output[7]);
+        let diff = builder.sub_extension(output[7], lv.gas[1]);
+        let constr = builder.mul_extension(total_filter, diff);
         yield_constr.constraint(builder, constr);
     }
 
diff --git a/evm/src/fixed_recursive_verifier.rs b/evm/src/fixed_recursive_verifier.rs
index 1c0928e4a8..d3fab17af7 100644
--- a/evm/src/fixed_recursive_verifier.rs
+++ b/evm/src/fixed_recursive_verifier.rs
@@ -655,15 +655,18 @@ where
         builder.connect(pvs.txn_number_before, lhs.txn_number_before);
         builder.connect(pvs.txn_number_after, rhs.txn_number_after);
 
-        // Connect lhs `txn_number_after`with rhs `txn_number_before`.
+        // Connect lhs `txn_number_after` with rhs `txn_number_before`.
         builder.connect(lhs.txn_number_after, rhs.txn_number_before);
 
         // Connect the gas used in public values to the lhs and rhs values correctly.
-        builder.connect(pvs.gas_used_before, lhs.gas_used_before);
-        builder.connect(pvs.gas_used_after, rhs.gas_used_after);
+        builder.connect(pvs.gas_used_before[0], lhs.gas_used_before[0]);
+        builder.connect(pvs.gas_used_before[1], lhs.gas_used_before[1]);
+        builder.connect(pvs.gas_used_after[0], rhs.gas_used_after[0]);
+        builder.connect(pvs.gas_used_after[1], rhs.gas_used_after[1]);
 
-        // Connect lhs `gas_used_after`with rhs `gas_used_before`.
-        builder.connect(lhs.gas_used_after, rhs.gas_used_before);
+        // Connect lhs `gas_used_after` with rhs `gas_used_before`.
+        builder.connect(lhs.gas_used_after[0], rhs.gas_used_before[0]);
+        builder.connect(lhs.gas_used_after[1], rhs.gas_used_before[1]);
 
         // Connect the `block_bloom` in public values to the lhs and rhs values correctly.
         for (&limb0, &limb1) in pvs.block_bloom_after.iter().zip(&rhs.block_bloom_after) {
@@ -672,7 +675,7 @@ where
         for (&limb0, &limb1) in pvs.block_bloom_before.iter().zip(&lhs.block_bloom_before) {
             builder.connect(limb0, limb1);
         }
-        // Connect lhs `block_bloom_after`with rhs `block_bloom_before`.
+        // Connect lhs `block_bloom_after` with rhs `block_bloom_before`.
         for (&limb0, &limb1) in lhs.block_bloom_after.iter().zip(&rhs.block_bloom_before) {
             builder.connect(limb0, limb1);
         }
@@ -846,8 +849,12 @@ where
         F: RichField + Extendable<D>,
     {
         builder.connect(
-            x.block_metadata.block_gas_used,
-            x.extra_block_data.gas_used_after,
+            x.block_metadata.block_gas_used[0],
+            x.extra_block_data.gas_used_after[0],
+        );
+        builder.connect(
+            x.block_metadata.block_gas_used[1],
+            x.extra_block_data.gas_used_after[1],
         );
 
         for (&limb0, &limb1) in x
@@ -868,7 +875,8 @@ where
         // The initial number of transactions is 0.
         builder.connect(x.extra_block_data.txn_number_before, zero);
         // The initial gas used is 0
-        builder.connect(x.extra_block_data.gas_used_before, zero);
+        builder.connect(x.extra_block_data.gas_used_before[0], zero);
+        builder.connect(x.extra_block_data.gas_used_before[1], zero);
 
         // The initial bloom filter is all zeroes.
         for t in x.extra_block_data.block_bloom_before {
diff --git a/evm/src/generation/mod.rs b/evm/src/generation/mod.rs
index 628a0600bb..317326e8b6 100644
--- a/evm/src/generation/mod.rs
+++ b/evm/src/generation/mod.rs
@@ -304,7 +304,10 @@ fn simulate_cpu<F: RichField + Extendable<D>, const D: usize>(
             row.context = F::from_canonical_usize(state.registers.context);
             row.program_counter = F::from_canonical_usize(pc);
             row.is_kernel_mode = F::ONE;
-            row.gas = F::from_canonical_u64(state.registers.gas_used);
+            row.gas = [
+                F::from_canonical_u32(state.registers.gas_used as u32),
+                F::from_canonical_u32((state.registers.gas_used >> 32) as u32),
+            ];
             row.stack_len = F::from_canonical_usize(state.registers.stack_len);
 
             loop {
diff --git a/evm/src/get_challenges.rs b/evm/src/get_challenges.rs
index 1d0aeac9da..287b652c56 100644
--- a/evm/src/get_challenges.rs
+++ b/evm/src/get_challenges.rs
@@ -62,12 +62,16 @@ fn observe_block_metadata<
     challenger.observe_element(u256_to_u32(block_metadata.block_number)?);
     challenger.observe_element(u256_to_u32(block_metadata.block_difficulty)?);
     challenger.observe_elements(&h256_limbs::<F>(block_metadata.block_random));
-    challenger.observe_element(u256_to_u32(block_metadata.block_gaslimit)?);
+    let gaslimit = u256_to_u64(block_metadata.block_gaslimit)?;
+    challenger.observe_element(gaslimit.0);
+    challenger.observe_element(gaslimit.1);
     challenger.observe_element(u256_to_u32(block_metadata.block_chain_id)?);
     let basefee = u256_to_u64(block_metadata.block_base_fee)?;
     challenger.observe_element(basefee.0);
     challenger.observe_element(basefee.1);
-    challenger.observe_element(u256_to_u32(block_metadata.block_gas_used)?);
+    let gas_used = u256_to_u64(block_metadata.block_gas_used)?;
+    challenger.observe_element(gas_used.0);
+    challenger.observe_element(gas_used.1);
     for i in 0..8 {
         challenger.observe_elements(&u256_limbs(block_metadata.block_bloom[i]));
     }
@@ -90,10 +94,10 @@ fn observe_block_metadata_target<
     challenger.observe_element(block_metadata.block_number);
     challenger.observe_element(block_metadata.block_difficulty);
     challenger.observe_elements(&block_metadata.block_random);
-    challenger.observe_element(block_metadata.block_gaslimit);
+    challenger.observe_elements(&block_metadata.block_gaslimit);
     challenger.observe_element(block_metadata.block_chain_id);
     challenger.observe_elements(&block_metadata.block_base_fee);
-    challenger.observe_element(block_metadata.block_gas_used);
+    challenger.observe_elements(&block_metadata.block_gas_used);
     challenger.observe_elements(&block_metadata.block_bloom);
 }
 
@@ -133,8 +137,8 @@ fn observe_extra_block_data_target<
     challenger.observe_elements(&extra_data.genesis_state_root);
     challenger.observe_element(extra_data.txn_number_before);
     challenger.observe_element(extra_data.txn_number_after);
-    challenger.observe_element(extra_data.gas_used_before);
-    challenger.observe_element(extra_data.gas_used_after);
+    challenger.observe_elements(&extra_data.gas_used_before);
+    challenger.observe_elements(&extra_data.gas_used_after);
     challenger.observe_elements(&extra_data.block_bloom_before);
     challenger.observe_elements(&extra_data.block_bloom_after);
 }
diff --git a/evm/src/proof.rs b/evm/src/proof.rs
index c6d15dd1e3..640c37a042 100644
--- a/evm/src/proof.rs
+++ b/evm/src/proof.rs
@@ -101,14 +101,15 @@ pub struct BlockMetadata {
     pub block_number: U256,
     /// The difficulty (before PoS transition) of this block.
     pub block_difficulty: U256,
+    /// The `mix_hash` value of this block.
     pub block_random: H256,
-    /// The gas limit of this block. It must fit in a `u32`.
+    /// The gas limit of this block.
     pub block_gaslimit: U256,
     /// The chain id of this block.
     pub block_chain_id: U256,
     /// The base fee of this block.
     pub block_base_fee: U256,
-    /// The total gas used in this block. It must fit in a `u32`.
+    /// The total gas used in this block.
     pub block_gas_used: U256,
     /// The block bloom of this block, represented as the consecutive
     /// 32-byte chunks of a block's final bloom filter string.
@@ -191,10 +192,10 @@ impl PublicValuesTarget {
         buffer.write_target(block_number)?;
         buffer.write_target(block_difficulty)?;
         buffer.write_target_array(&block_random)?;
-        buffer.write_target(block_gaslimit)?;
+        buffer.write_target_array(&block_gaslimit)?;
         buffer.write_target(block_chain_id)?;
         buffer.write_target_array(&block_base_fee)?;
-        buffer.write_target(block_gas_used)?;
+        buffer.write_target_array(&block_gas_used)?;
         buffer.write_target_array(&block_bloom)?;
 
         let BlockHashesTarget {
@@ -216,8 +217,8 @@ impl PublicValuesTarget {
         buffer.write_target_array(&genesis_state_root)?;
         buffer.write_target(txn_number_before)?;
         buffer.write_target(txn_number_after)?;
-        buffer.write_target(gas_used_before)?;
-        buffer.write_target(gas_used_after)?;
+        buffer.write_target_array(&gas_used_before)?;
+        buffer.write_target_array(&gas_used_after)?;
         buffer.write_target_array(&block_bloom_before)?;
         buffer.write_target_array(&block_bloom_after)?;
 
@@ -243,10 +244,10 @@ impl PublicValuesTarget {
             block_number: buffer.read_target()?,
             block_difficulty: buffer.read_target()?,
             block_random: buffer.read_target_array()?,
-            block_gaslimit: buffer.read_target()?,
+            block_gaslimit: buffer.read_target_array()?,
             block_chain_id: buffer.read_target()?,
             block_base_fee: buffer.read_target_array()?,
-            block_gas_used: buffer.read_target()?,
+            block_gas_used: buffer.read_target_array()?,
             block_bloom: buffer.read_target_array()?,
         };
 
@@ -259,8 +260,8 @@ impl PublicValuesTarget {
             genesis_state_root: buffer.read_target_array()?,
             txn_number_before: buffer.read_target()?,
             txn_number_after: buffer.read_target()?,
-            gas_used_before: buffer.read_target()?,
-            gas_used_after: buffer.read_target()?,
+            gas_used_before: buffer.read_target_array()?,
+            gas_used_after: buffer.read_target_array()?,
             block_bloom_before: buffer.read_target_array()?,
             block_bloom_after: buffer.read_target_array()?,
         };
@@ -417,15 +418,15 @@ pub struct BlockMetadataTarget {
     pub block_number: Target,
     pub block_difficulty: Target,
     pub block_random: [Target; 8],
-    pub block_gaslimit: Target,
+    pub block_gaslimit: [Target; 2],
     pub block_chain_id: Target,
     pub block_base_fee: [Target; 2],
-    pub block_gas_used: Target,
+    pub block_gas_used: [Target; 2],
     pub block_bloom: [Target; 64],
 }
 
 impl BlockMetadataTarget {
-    pub const SIZE: usize = 85;
+    pub const SIZE: usize = 87;
 
     pub fn from_public_inputs(pis: &[Target]) -> Self {
         let block_beneficiary = pis[0..5].try_into().unwrap();
@@ -433,11 +434,11 @@ impl BlockMetadataTarget {
         let block_number = pis[6];
         let block_difficulty = pis[7];
         let block_random = pis[8..16].try_into().unwrap();
-        let block_gaslimit = pis[16];
-        let block_chain_id = pis[17];
-        let block_base_fee = pis[18..20].try_into().unwrap();
-        let block_gas_used = pis[20];
-        let block_bloom = pis[21..85].try_into().unwrap();
+        let block_gaslimit = pis[16..18].try_into().unwrap();
+        let block_chain_id = pis[18];
+        let block_base_fee = pis[19..21].try_into().unwrap();
+        let block_gas_used = pis[21..23].try_into().unwrap();
+        let block_bloom = pis[23..87].try_into().unwrap();
 
         Self {
             block_beneficiary,
@@ -473,12 +474,16 @@ impl BlockMetadataTarget {
             block_random: core::array::from_fn(|i| {
                 builder.select(condition, bm0.block_random[i], bm1.block_random[i])
             }),
-            block_gaslimit: builder.select(condition, bm0.block_gaslimit, bm1.block_gaslimit),
+            block_gaslimit: core::array::from_fn(|i| {
+                builder.select(condition, bm0.block_gaslimit[i], bm1.block_gaslimit[i])
+            }),
             block_chain_id: builder.select(condition, bm0.block_chain_id, bm1.block_chain_id),
             block_base_fee: core::array::from_fn(|i| {
                 builder.select(condition, bm0.block_base_fee[i], bm1.block_base_fee[i])
             }),
-            block_gas_used: builder.select(condition, bm0.block_gas_used, bm1.block_gas_used),
+            block_gas_used: core::array::from_fn(|i| {
+                builder.select(condition, bm0.block_gas_used[i], bm1.block_gas_used[i])
+            }),
             block_bloom: core::array::from_fn(|i| {
                 builder.select(condition, bm0.block_bloom[i], bm1.block_bloom[i])
             }),
@@ -499,12 +504,16 @@ impl BlockMetadataTarget {
         for i in 0..8 {
             builder.connect(bm0.block_random[i], bm1.block_random[i]);
         }
-        builder.connect(bm0.block_gaslimit, bm1.block_gaslimit);
+        for i in 0..2 {
+            builder.connect(bm0.block_gaslimit[i], bm1.block_gaslimit[i])
+        }
         builder.connect(bm0.block_chain_id, bm1.block_chain_id);
         for i in 0..2 {
             builder.connect(bm0.block_base_fee[i], bm1.block_base_fee[i])
         }
-        builder.connect(bm0.block_gas_used, bm1.block_gas_used);
+        for i in 0..2 {
+            builder.connect(bm0.block_gas_used[i], bm1.block_gas_used[i])
+        }
         for i in 0..64 {
             builder.connect(bm0.block_bloom[i], bm1.block_bloom[i])
         }
@@ -561,23 +570,23 @@ pub struct ExtraBlockDataTarget {
     pub genesis_state_root: [Target; 8],
     pub txn_number_before: Target,
     pub txn_number_after: Target,
-    pub gas_used_before: Target,
-    pub gas_used_after: Target,
+    pub gas_used_before: [Target; 2],
+    pub gas_used_after: [Target; 2],
     pub block_bloom_before: [Target; 64],
     pub block_bloom_after: [Target; 64],
 }
 
 impl ExtraBlockDataTarget {
-    const SIZE: usize = 140;
+    const SIZE: usize = 142;
 
     pub fn from_public_inputs(pis: &[Target]) -> Self {
         let genesis_state_root = pis[0..8].try_into().unwrap();
         let txn_number_before = pis[8];
         let txn_number_after = pis[9];
-        let gas_used_before = pis[10];
-        let gas_used_after = pis[11];
-        let block_bloom_before = pis[12..76].try_into().unwrap();
-        let block_bloom_after = pis[76..140].try_into().unwrap();
+        let gas_used_before = pis[10..12].try_into().unwrap();
+        let gas_used_after = pis[12..14].try_into().unwrap();
+        let block_bloom_before = pis[14..78].try_into().unwrap();
+        let block_bloom_after = pis[78..142].try_into().unwrap();
 
         Self {
             genesis_state_root,
@@ -610,8 +619,12 @@ impl ExtraBlockDataTarget {
                 ed1.txn_number_before,
             ),
             txn_number_after: builder.select(condition, ed0.txn_number_after, ed1.txn_number_after),
-            gas_used_before: builder.select(condition, ed0.gas_used_before, ed1.gas_used_before),
-            gas_used_after: builder.select(condition, ed0.gas_used_after, ed1.gas_used_after),
+            gas_used_before: core::array::from_fn(|i| {
+                builder.select(condition, ed0.gas_used_before[i], ed1.gas_used_before[i])
+            }),
+            gas_used_after: core::array::from_fn(|i| {
+                builder.select(condition, ed0.gas_used_after[i], ed1.gas_used_after[i])
+            }),
             block_bloom_before: core::array::from_fn(|i| {
                 builder.select(
                     condition,
@@ -639,8 +652,12 @@ impl ExtraBlockDataTarget {
         }
         builder.connect(ed0.txn_number_before, ed1.txn_number_before);
         builder.connect(ed0.txn_number_after, ed1.txn_number_after);
-        builder.connect(ed0.gas_used_before, ed1.gas_used_before);
-        builder.connect(ed1.gas_used_after, ed1.gas_used_after);
+        for i in 0..2 {
+            builder.connect(ed0.gas_used_before[i], ed1.gas_used_before[i]);
+        }
+        for i in 0..2 {
+            builder.connect(ed1.gas_used_after[i], ed1.gas_used_after[i]);
+        }
         for i in 0..64 {
             builder.connect(ed0.block_bloom_before[i], ed1.block_bloom_before[i]);
         }
diff --git a/evm/src/recursive_verifier.rs b/evm/src/recursive_verifier.rs
index 601b16687f..4d873b650a 100644
--- a/evm/src/recursive_verifier.rs
+++ b/evm/src/recursive_verifier.rs
@@ -519,26 +519,10 @@ pub(crate) fn get_memory_extra_looking_products_circuit<
             GlobalMetadata::BlockDifficulty as usize,
             public_values.block_metadata.block_difficulty,
         ),
-        (
-            GlobalMetadata::BlockGasLimit as usize,
-            public_values.block_metadata.block_gaslimit,
-        ),
         (
             GlobalMetadata::BlockChainId as usize,
             public_values.block_metadata.block_chain_id,
         ),
-        (
-            GlobalMetadata::BlockGasUsed as usize,
-            public_values.block_metadata.block_gas_used,
-        ),
-        (
-            GlobalMetadata::BlockGasUsedBefore as usize,
-            public_values.extra_block_data.gas_used_before,
-        ),
-        (
-            GlobalMetadata::BlockGasUsedAfter as usize,
-            public_values.extra_block_data.gas_used_after,
-        ),
         (
             GlobalMetadata::TxnNumberBefore as usize,
             public_values.extra_block_data.txn_number_before,
@@ -549,7 +533,10 @@ pub(crate) fn get_memory_extra_looking_products_circuit<
         ),
     ];
 
-    let beneficiary_random_base_fee_cur_hash_fields: [(usize, &[Target]); 4] = [
+    // This contains the `block_beneficiary`, `block_random`, `block_base_fee`,
+    // `block_gaslimit`, `block_gas_used` as well as `cur_hash`, `gas_used_before`
+    // and `gas_used_after`.
+    let block_fields_arrays: [(usize, &[Target]); 8] = [
         (
             GlobalMetadata::BlockBeneficiary as usize,
             &public_values.block_metadata.block_beneficiary,
@@ -562,10 +549,26 @@ pub(crate) fn get_memory_extra_looking_products_circuit<
             GlobalMetadata::BlockBaseFee as usize,
             &public_values.block_metadata.block_base_fee,
         ),
+        (
+            GlobalMetadata::BlockBaseFee as usize,
+            &public_values.block_metadata.block_gaslimit,
+        ),
+        (
+            GlobalMetadata::BlockBaseFee as usize,
+            &public_values.block_metadata.block_gas_used,
+        ),
         (
             GlobalMetadata::BlockCurrentHash as usize,
             &public_values.block_hashes.cur_hash,
         ),
+        (
+            GlobalMetadata::BlockGasUsedBefore as usize,
+            &public_values.extra_block_data.gas_used_before,
+        ),
+        (
+            GlobalMetadata::BlockGasUsedAfter as usize,
+            &public_values.extra_block_data.gas_used_after,
+        ),
     ];
 
     let metadata_segment = builder.constant(F::from_canonical_u32(Segment::GlobalMetadata as u32));
@@ -581,7 +584,7 @@ pub(crate) fn get_memory_extra_looking_products_circuit<
         );
     });
 
-    beneficiary_random_base_fee_cur_hash_fields.map(|(field, targets)| {
+    block_fields_arrays.map(|(field, targets)| {
         product = add_data_write(
             builder,
             challenge,
@@ -778,10 +781,10 @@ pub(crate) fn add_virtual_block_metadata<F: RichField + Extendable<D>, const D:
     let block_number = builder.add_virtual_public_input();
     let block_difficulty = builder.add_virtual_public_input();
     let block_random = builder.add_virtual_public_input_arr();
-    let block_gaslimit = builder.add_virtual_public_input();
+    let block_gaslimit = builder.add_virtual_public_input_arr();
     let block_chain_id = builder.add_virtual_public_input();
     let block_base_fee = builder.add_virtual_public_input_arr();
-    let block_gas_used = builder.add_virtual_public_input();
+    let block_gas_used = builder.add_virtual_public_input_arr();
     let block_bloom = builder.add_virtual_public_input_arr();
     BlockMetadataTarget {
         block_beneficiary,
@@ -813,8 +816,8 @@ pub(crate) fn add_virtual_extra_block_data<F: RichField + Extendable<D>, const D
     let genesis_state_root = builder.add_virtual_public_input_arr();
     let txn_number_before = builder.add_virtual_public_input();
     let txn_number_after = builder.add_virtual_public_input();
-    let gas_used_before = builder.add_virtual_public_input();
-    let gas_used_after = builder.add_virtual_public_input();
+    let gas_used_before = builder.add_virtual_public_input_arr();
+    let gas_used_after = builder.add_virtual_public_input_arr();
     let block_bloom_before: [Target; 64] = builder.add_virtual_public_input_arr();
     let block_bloom_after: [Target; 64] = builder.add_virtual_public_input_arr();
     ExtraBlockDataTarget {
@@ -1027,10 +1030,10 @@ where
         &block_metadata_target.block_random,
         &h256_limbs(block_metadata.block_random),
     );
-    witness.set_target(
-        block_metadata_target.block_gaslimit,
-        u256_to_u32(block_metadata.block_gaslimit)?,
-    );
+    // Gaslimit fits in 2 limbs
+    let gaslimit = u256_to_u64(block_metadata.block_gaslimit)?;
+    witness.set_target(block_metadata_target.block_gaslimit[0], gaslimit.0);
+    witness.set_target(block_metadata_target.block_gaslimit[1], gaslimit.1);
     witness.set_target(
         block_metadata_target.block_chain_id,
         u256_to_u32(block_metadata.block_chain_id)?,
@@ -1039,10 +1042,10 @@ where
     let basefee = u256_to_u64(block_metadata.block_base_fee)?;
     witness.set_target(block_metadata_target.block_base_fee[0], basefee.0);
     witness.set_target(block_metadata_target.block_base_fee[1], basefee.1);
-    witness.set_target(
-        block_metadata_target.block_gas_used,
-        u256_to_u32(block_metadata.block_gas_used)?,
-    );
+    // Gas used fits in 2 limbs
+    let gas_used = u256_to_u64(block_metadata.block_gas_used)?;
+    witness.set_target(block_metadata_target.block_gas_used[0], gas_used.0);
+    witness.set_target(block_metadata_target.block_gas_used[1], gas_used.1);
     let mut block_bloom_limbs = [F::ZERO; 64];
     for (i, limbs) in block_bloom_limbs.chunks_exact_mut(8).enumerate() {
         limbs.copy_from_slice(&u256_limbs(block_metadata.block_bloom[i]));
@@ -1092,8 +1095,13 @@ where
         ed_target.txn_number_after,
         u256_to_u32(ed.txn_number_after)?,
     );
-    witness.set_target(ed_target.gas_used_before, u256_to_u32(ed.gas_used_before)?);
-    witness.set_target(ed_target.gas_used_after, u256_to_u32(ed.gas_used_after)?);
+    // Gas used before/after fit in 2 limbs
+    let gas_used_before = u256_to_u64(ed.gas_used_before)?;
+    witness.set_target(ed_target.gas_used_before[0], gas_used_before.0);
+    witness.set_target(ed_target.gas_used_before[1], gas_used_before.1);
+    let gas_used_after = u256_to_u64(ed.gas_used_after)?;
+    witness.set_target(ed_target.gas_used_after[0], gas_used_after.0);
+    witness.set_target(ed_target.gas_used_after[1], gas_used_after.1);
 
     let block_bloom_before = ed.block_bloom_before;
     let mut block_bloom_limbs = [F::ZERO; 64];
diff --git a/evm/src/witness/operation.rs b/evm/src/witness/operation.rs
index 2abeaea4c3..0620069f00 100644
--- a/evm/src/witness/operation.rs
+++ b/evm/src/witness/operation.rs
@@ -557,7 +557,7 @@ pub(crate) fn generate_syscall<F: Field>(
     state: &mut GenerationState<F>,
     mut row: CpuColumnsView<F>,
 ) -> Result<(), ProgramError> {
-    if TryInto::<u32>::try_into(state.registers.gas_used).is_err() {
+    if TryInto::<u64>::try_into(state.registers.gas_used).is_err() {
         return Err(ProgramError::GasLimitError);
     }
 
@@ -650,7 +650,7 @@ pub(crate) fn generate_exit_kernel<F: Field>(
     assert!(is_kernel_mode_val == 0 || is_kernel_mode_val == 1);
     let is_kernel_mode = is_kernel_mode_val != 0;
     let gas_used_val = kexit_info.0[3];
-    if TryInto::<u32>::try_into(gas_used_val).is_err() {
+    if TryInto::<u64>::try_into(gas_used_val).is_err() {
         return Err(ProgramError::GasLimitError);
     }
 
@@ -792,7 +792,7 @@ pub(crate) fn generate_exception<F: Field>(
     state: &mut GenerationState<F>,
     mut row: CpuColumnsView<F>,
 ) -> Result<(), ProgramError> {
-    if TryInto::<u32>::try_into(state.registers.gas_used).is_err() {
+    if TryInto::<u64>::try_into(state.registers.gas_used).is_err() {
         return Err(ProgramError::GasLimitError);
     }
 
diff --git a/evm/src/witness/transition.rs b/evm/src/witness/transition.rs
index 5ce2a0ce43..2a710f4b94 100644
--- a/evm/src/witness/transition.rs
+++ b/evm/src/witness/transition.rs
@@ -242,7 +242,10 @@ fn base_row<F: Field>(state: &mut GenerationState<F>) -> (CpuColumnsView<F>, u8)
     row.context = F::from_canonical_usize(state.registers.context);
     row.program_counter = F::from_canonical_usize(state.registers.program_counter);
     row.is_kernel_mode = F::from_bool(state.registers.is_kernel);
-    row.gas = F::from_canonical_u64(state.registers.gas_used);
+    row.gas = [
+        F::from_canonical_u32(state.registers.gas_used as u32),
+        F::from_canonical_u32((state.registers.gas_used >> 32) as u32),
+    ];
     row.stack_len = F::from_canonical_usize(state.registers.stack_len);
 
     let opcode = read_code_memory(state, &mut row);

From 88842798b69a7f7ac569a84745c0e6809a31950f Mon Sep 17 00:00:00 2001
From: Robin Salen <salenrobin@gmail.com>
Date: Thu, 28 Sep 2023 16:08:05 -0400
Subject: [PATCH 2/5] Fix recursive challenger

---
 evm/src/fixed_recursive_verifier.rs | 2 +-
 evm/src/get_challenges.rs           | 8 ++++++--
 2 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/evm/src/fixed_recursive_verifier.rs b/evm/src/fixed_recursive_verifier.rs
index d3fab17af7..766b9102bb 100644
--- a/evm/src/fixed_recursive_verifier.rs
+++ b/evm/src/fixed_recursive_verifier.rs
@@ -874,7 +874,7 @@ where
         let zero = builder.constant(F::ZERO);
         // The initial number of transactions is 0.
         builder.connect(x.extra_block_data.txn_number_before, zero);
-        // The initial gas used is 0
+        // The initial gas used is 0.
         builder.connect(x.extra_block_data.gas_used_before[0], zero);
         builder.connect(x.extra_block_data.gas_used_before[1], zero);
 
diff --git a/evm/src/get_challenges.rs b/evm/src/get_challenges.rs
index 287b652c56..715c1097be 100644
--- a/evm/src/get_challenges.rs
+++ b/evm/src/get_challenges.rs
@@ -112,8 +112,12 @@ fn observe_extra_block_data<
     challenger.observe_elements(&h256_limbs(extra_data.genesis_state_root));
     challenger.observe_element(u256_to_u32(extra_data.txn_number_before)?);
     challenger.observe_element(u256_to_u32(extra_data.txn_number_after)?);
-    challenger.observe_element(u256_to_u32(extra_data.gas_used_before)?);
-    challenger.observe_element(u256_to_u32(extra_data.gas_used_after)?);
+    let gas_used_before = u256_to_u64(extra_data.gas_used_before)?;
+    challenger.observe_element(gas_used_before.0);
+    challenger.observe_element(gas_used_before.1);
+    let gas_used_after = u256_to_u64(extra_data.gas_used_after)?;
+    challenger.observe_element(gas_used_after.0);
+    challenger.observe_element(gas_used_after.1);
     for i in 0..8 {
         challenger.observe_elements(&u256_limbs(extra_data.block_bloom_before[i]));
     }

From bbfbf396c09c8f652a81beb8d3492b51b3bd044c Mon Sep 17 00:00:00 2001
From: Robin Salen <salenrobin@gmail.com>
Date: Thu, 28 Sep 2023 16:39:28 -0400
Subject: [PATCH 3/5] Fix indices

---
 evm/src/recursive_verifier.rs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/evm/src/recursive_verifier.rs b/evm/src/recursive_verifier.rs
index 4d873b650a..04259208b8 100644
--- a/evm/src/recursive_verifier.rs
+++ b/evm/src/recursive_verifier.rs
@@ -550,11 +550,11 @@ pub(crate) fn get_memory_extra_looking_products_circuit<
             &public_values.block_metadata.block_base_fee,
         ),
         (
-            GlobalMetadata::BlockBaseFee as usize,
+            GlobalMetadata::BlockGasLimit as usize,
             &public_values.block_metadata.block_gaslimit,
         ),
         (
-            GlobalMetadata::BlockBaseFee as usize,
+            GlobalMetadata::BlockGasUsed as usize,
             &public_values.block_metadata.block_gas_used,
         ),
         (

From e11592ea5537f012f83d5673e4514993cd7edf5b Mon Sep 17 00:00:00 2001
From: Robin Salen <salenrobin@gmail.com>
Date: Fri, 29 Sep 2023 11:05:27 -0400
Subject: [PATCH 4/5] Add clarifying comments on ranges supported

---
 evm/src/proof.rs | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/evm/src/proof.rs b/evm/src/proof.rs
index 640c37a042..d63ddc8914 100644
--- a/evm/src/proof.rs
+++ b/evm/src/proof.rs
@@ -95,21 +95,21 @@ pub struct BlockHashes {
 pub struct BlockMetadata {
     /// The address of this block's producer.
     pub block_beneficiary: Address,
-    /// The timestamp of this block.
+    /// The timestamp of this block. It must fit in a `u32`.
     pub block_timestamp: U256,
-    /// The index of this block.
+    /// The index of this block. It must fit in a `u32`.
     pub block_number: U256,
     /// The difficulty (before PoS transition) of this block.
     pub block_difficulty: U256,
     /// The `mix_hash` value of this block.
     pub block_random: H256,
-    /// The gas limit of this block.
+    /// The gas limit of this block. It must fit in a `u64`.
     pub block_gaslimit: U256,
-    /// The chain id of this block.
+    /// The chain id of this block. It must fit in a `u32`.
     pub block_chain_id: U256,
-    /// The base fee of this block.
+    /// The base fee of this block. It must fit in a `u64`.
     pub block_base_fee: U256,
-    /// The total gas used in this block.
+    /// The total gas used in this block. It must fit in a `u64`.
     pub block_gas_used: U256,
     /// The block bloom of this block, represented as the consecutive
     /// 32-byte chunks of a block's final bloom filter string.

From 725c38e156b49914c8dae4ea2560a293e76d45b1 Mon Sep 17 00:00:00 2001
From: Robin Salen <salenrobin@gmail.com>
Date: Fri, 29 Sep 2023 14:16:23 -0400
Subject: [PATCH 5/5] Add mention to revert before production

---
 evm/src/cpu/gas.rs | 8 ++++++++
 evm/src/proof.rs   | 4 ++++
 2 files changed, 12 insertions(+)

diff --git a/evm/src/cpu/gas.rs b/evm/src/cpu/gas.rs
index ae923fde6b..694fb0f47e 100644
--- a/evm/src/cpu/gas.rs
+++ b/evm/src/cpu/gas.rs
@@ -70,6 +70,10 @@ fn eval_packed_accumulate<P: PackedField>(
         })
         .sum();
 
+    // TODO: This may cause soundness issue if the recomputed gas (as u64) overflows the field size.
+    // This is fine as we are only using two-limbs for testing purposes (to support all cases from
+    // the Ethereum test suite).
+    // This should be changed back to a single 32-bit limb before going into production!
     let gas_diff = nv.gas[1] * P::Scalar::from_canonical_u64(1 << 32) + nv.gas[0]
         - (lv.gas[1] * P::Scalar::from_canonical_u64(1 << 32) + lv.gas[0]);
     let constr = gas_diff - gas_used;
@@ -157,6 +161,10 @@ fn eval_ext_circuit_accumulate<F: RichField + Extendable<D>, const D: usize>(
         },
     );
 
+    // TODO: This may cause soundness issue if the recomputed gas (as u64) overflows the field size.
+    // This is fine as we are only using two-limbs for testing purposes (to support all cases from
+    // the Ethereum test suite).
+    // This should be changed back to a single 32-bit limb before going into production!
     let nv_gas =
         builder.mul_const_add_extension(F::from_canonical_u64(1 << 32), nv.gas[1], nv.gas[0]);
     let lv_gas =
diff --git a/evm/src/proof.rs b/evm/src/proof.rs
index d63ddc8914..fd6c4f3e9a 100644
--- a/evm/src/proof.rs
+++ b/evm/src/proof.rs
@@ -89,6 +89,10 @@ pub struct BlockHashes {
     pub cur_hash: H256,
 }
 
+// TODO: Before going into production, `block_gas_used` and `block_gaslimit` here
+// as well as `gas_used_before` / `gas_used_after` in `ExtraBlockData` should be
+// updated to fit in a single 32-bit limb, as supporting 64-bit values for those
+// fields is only necessary for testing purposes.
 /// Metadata contained in a block header. Those are identical between
 /// all state transition proofs within the same block.
 #[derive(Debug, Clone, Default, Deserialize, Serialize)]