Merge pull request #673 from mir-protocol/start_at_route_txn

Start with PC=route_txn instead of 0
This commit is contained in:
Daniel Lubarov 2022-08-17 12:57:38 -07:00 committed by GitHub
commit 24cc29ff71
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 12 additions and 23 deletions

View File

@ -261,7 +261,8 @@ mod tests {
[F::ZERO; CpuStark::<F, D>::COLUMNS].into();
row.is_cpu_cycle = F::ONE;
row.is_kernel_mode = F::ONE;
row.program_counter = F::from_canonical_usize(i);
// Since these are the first cycle rows, we must start with PC=route_txn then increment.
row.program_counter = F::from_canonical_usize(KERNEL.global_labels["route_txn"] + i);
row.opcode = [
(logic::columns::IS_AND, 0x16),
(logic::columns::IS_OR, 0x17),

View File

@ -69,20 +69,14 @@ pub fn eval_packed_generic<P: PackedField>(
);
// If a non-CPU cycle row is followed by a CPU cycle row, then the `program_counter` of the CPU
// cycle row is 0 and it is in kernel mode.
yield_constr
.constraint_transition((lv.is_cpu_cycle - P::ONES) * nv.is_cpu_cycle * nv.program_counter);
// cycle row is route_txn (the entry point of our kernel) and it is in kernel mode.
let pc_diff =
nv.program_counter - P::Scalar::from_canonical_usize(KERNEL.global_labels["route_txn"]);
yield_constr.constraint_transition((lv.is_cpu_cycle - P::ONES) * nv.is_cpu_cycle * pc_diff);
yield_constr.constraint_transition(
(lv.is_cpu_cycle - P::ONES) * nv.is_cpu_cycle * (nv.is_kernel_mode - P::ONES),
);
// The first row has nowhere to continue execution from, so if it's a cycle row, then its
// `program_counter` must be 0.
// NB: I know the first few rows will be used for initialization and will not be CPU cycle rows.
// Once that's done, then this constraint can be removed. Until then, it is needed to ensure
// that execution starts at 0 and not at any arbitrary offset.
yield_constr.constraint_first_row(lv.is_cpu_cycle * lv.program_counter);
// The last row must be a CPU cycle row.
yield_constr.constraint_last_row(lv.is_cpu_cycle - P::ONES);
// Also, the last row's `program_counter` must be inside the `halt` infinite loop. Note that
@ -122,25 +116,19 @@ pub fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
}
// If a non-CPU cycle row is followed by a CPU cycle row, then the `program_counter` of the CPU
// cycle row is 0 and it is in kernel mode.
// cycle row is route_txn (the entry point of our kernel) and it is in kernel mode.
{
let filter = builder.mul_sub_extension(lv.is_cpu_cycle, nv.is_cpu_cycle, nv.is_cpu_cycle);
let pc_constr = builder.mul_extension(filter, nv.program_counter);
let route_txn = builder.constant_extension(F::Extension::from_canonical_usize(
KERNEL.global_labels["route_txn"],
));
let pc_diff = builder.sub_extension(nv.program_counter, route_txn);
let pc_constr = builder.mul_extension(filter, pc_diff);
yield_constr.constraint_transition(builder, pc_constr);
let kernel_constr = builder.mul_sub_extension(filter, nv.is_kernel_mode, filter);
yield_constr.constraint_transition(builder, kernel_constr);
}
// The first row has nowhere to continue execution from, so if it's a cycle row, then its
// `program_counter` must be 0.
// NB: I know the first few rows will be used for initialization and will not be CPU cycle rows.
// Once that's done, then this constraint can be removed. Until then, it is needed to ensure
// that execution starts at 0 and not at any arbitrary offset.
{
let constr = builder.mul_extension(lv.is_cpu_cycle, lv.program_counter);
yield_constr.constraint_first_row(builder, constr);
}
// The last row must be a CPU cycle row.
{
let one = builder.one_extension();