Make gas fit in 2 limbs

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`).

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);
 }
 

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);
     }
 }
 

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);
     }
 

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
@@ -867,8 +874,9 @@ 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
-        builder.connect(x.extra_block_data.gas_used_before, zero);
+        // 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);
 
         // The initial bloom filter is all zeroes.
         for t in x.extra_block_data.block_bloom_before {

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 {

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);
 }
 
@@ -108,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]));
     }
@@ -133,8 +141,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);
 }