Skip to content

Commit cce9478

Browse files
committed
use explicit names for instruction encoding (instead of basic integers)
1 parent 140f21e commit cce9478

File tree

2 files changed

+21
-50
lines changed

2 files changed

+21
-50
lines changed

crates/lean_prover/vm_air/src/execution_air.rs

Lines changed: 0 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -5,35 +5,6 @@ use p3_field::PrimeCharacteristicRing;
55
use p3_matrix::Matrix;
66
use witness_generation::*;
77

8-
/*
9-
10-
Bytecode columns:
11-
12-
0: OPERAND_A
13-
1: OPERAND_B
14-
2: OPERAND_C
15-
3: FLAG_A
16-
4: FLAG_B
17-
5: FLAG_C
18-
6: ADD
19-
7: MUL
20-
8: DEREF
21-
9: JUMP
22-
10: AUX
23-
24-
Execution columns:
25-
26-
11: VALUE_A (virtual)
27-
12: VALUE_B (virtual)
28-
13: VALUE_C (virtual)
29-
14: PC
30-
15: FP
31-
16: ADDR_A
32-
17: ADDR_B
33-
18: ADDR_C
34-
35-
*/
36-
378
#[derive(Debug)]
389
pub struct VMAir;
3910

crates/lean_prover/witness_generation/src/instruction_encoder.rs

Lines changed: 21 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -14,10 +14,10 @@ pub fn field_representation(instr: &Instruction) -> [F; N_INSTRUCTION_COLUMNS] {
1414
} => {
1515
match operation {
1616
Operation::Add => {
17-
fields[6] = F::ONE;
17+
fields[COL_INDEX_ADD] = F::ONE;
1818
}
1919
Operation::Mul => {
20-
fields[7] = F::ONE;
20+
fields[COL_INDEX_MUL] = F::ONE;
2121
}
2222
}
2323

@@ -30,25 +30,25 @@ pub fn field_representation(instr: &Instruction) -> [F; N_INSTRUCTION_COLUMNS] {
3030
shift_1,
3131
res,
3232
} => {
33-
fields[8] = F::ONE; // DEREF = 1
34-
fields[3] = F::ZERO; // flag_A = 0
35-
fields[0] = F::from_usize(*shift_0);
36-
fields[5] = F::ONE; // flag_C = 1
37-
fields[2] = F::from_usize(*shift_1);
33+
fields[COL_INDEX_DEREF] = F::ONE;
34+
fields[COL_INDEX_FLAG_A] = F::ZERO;
35+
fields[COL_INDEX_OPERAND_A] = F::from_usize(*shift_0);
36+
fields[COL_INDEX_FLAG_C] = F::ONE;
37+
fields[COL_INDEX_OPERAND_C] = F::from_usize(*shift_1);
3838
match res {
3939
MemOrFpOrConstant::Constant(cst) => {
40-
fields[10] = F::ONE; // AUX = 1
41-
fields[4] = F::ONE; // flag_B = 1
42-
fields[1] = *cst;
40+
fields[COL_INDEX_AUX] = F::ONE;
41+
fields[COL_INDEX_FLAG_B] = F::ONE;
42+
fields[COL_INDEX_OPERAND_B] = *cst;
4343
}
4444
MemOrFpOrConstant::MemoryAfterFp { offset } => {
45-
fields[10] = F::ONE; // AUX = 1
46-
fields[4] = F::ZERO; // flag_B = 0
47-
fields[1] = F::from_usize(*offset);
45+
fields[COL_INDEX_AUX] = F::ONE;
46+
fields[COL_INDEX_FLAG_B] = F::ZERO;
47+
fields[COL_INDEX_OPERAND_B] = F::from_usize(*offset);
4848
}
4949
MemOrFpOrConstant::Fp => {
50-
fields[10] = F::ZERO; // AUX = 0
51-
fields[4] = F::ONE; // flag_B = 1
50+
fields[COL_INDEX_AUX] = F::ZERO;
51+
fields[COL_INDEX_FLAG_B] = F::ONE;
5252
}
5353
}
5454
}
@@ -58,7 +58,7 @@ pub fn field_representation(instr: &Instruction) -> [F; N_INSTRUCTION_COLUMNS] {
5858
dest,
5959
updated_fp,
6060
} => {
61-
fields[9] = F::ONE; // JUMP = 1
61+
fields[COL_INDEX_JUMP] = F::ONE;
6262
set_nu_a(&mut fields, condition);
6363
set_nu_b(&mut fields, dest);
6464
set_nu_c(&mut fields, updated_fp);
@@ -69,14 +69,14 @@ pub fn field_representation(instr: &Instruction) -> [F; N_INSTRUCTION_COLUMNS] {
6969
res,
7070
is_compression,
7171
} => {
72-
fields[11] = F::ONE; // POSEIDON_16 = 1
72+
fields[COL_INDEX_POSEIDON_16] = F::ONE;
7373
set_nu_a(&mut fields, arg_a);
7474
set_nu_b(&mut fields, arg_b);
7575
set_nu_c(&mut fields, res);
76-
fields[10] = F::from_bool(*is_compression); // AUX = "is_compression"
76+
fields[COL_INDEX_AUX] = F::from_bool(*is_compression); // AUX = "is_compression"
7777
}
7878
Instruction::Poseidon2_24 { arg_a, arg_b, res } => {
79-
fields[12] = F::ONE; // POSEIDON_24 = 1
79+
fields[COL_INDEX_POSEIDON_24] = F::ONE;
8080
set_nu_a(&mut fields, arg_a);
8181
set_nu_b(&mut fields, arg_b);
8282
set_nu_c(&mut fields, res);
@@ -87,11 +87,11 @@ pub fn field_representation(instr: &Instruction) -> [F; N_INSTRUCTION_COLUMNS] {
8787
res,
8888
size,
8989
} => {
90-
fields[13] = F::ONE; // DOT_PRODUCT_EXTENSION = 1
90+
fields[COL_INDEX_DOT_PRODUCT] = F::ONE;
9191
set_nu_a(&mut fields, arg0);
9292
set_nu_b(&mut fields, arg1);
9393
set_nu_c(&mut fields, res);
94-
fields[10] = F::from_usize(*size); // AUX stores size
94+
fields[COL_INDEX_AUX] = F::from_usize(*size); // AUX stores size
9595
}
9696
Instruction::MultilinearEval {
9797
coeffs,

0 commit comments

Comments
 (0)