Riscv bb #1790
Riscv bb #1790
Conversation
| addr.to_arbitrary_integer(), | ||
| value_expr | ||
| addr, | ||
| value1_expr |
There was a problem hiding this comment.
Why do we have only value1_expr here and not value2_expr?
| let value1_fe: T = value1_int.into(); | ||
| let value2_fe: T = value2_int.into(); | ||
|
|
||
| let ass = (value1_expr.clone() - value1_fe.into()) |
There was a problem hiding this comment.
It would be better name it ass1 since we also have ass2
| @@ -92,65 +92,75 @@ impl Runtime { | |||
| // Base submachines | |||
| // TODO: can/should the memory machine be part of the runtime also? | |||
| r.add_submachine( | |||
| "std::machines::binary::Binary", | |||
| "std::machines::binary_bb::Binary16", | |||
There was a problem hiding this comment.
It would be better to name binary_bb instead of binary16 since it will also work for other field elements, and we already have a Binary16 machine
There was a problem hiding this comment.
I will change the machine to named like that so that they can merge it.
| @@ -0,0 +1,32 @@ | |||
| use std::machines::range::Byte2; | |||
|
|
|||
| machine ArithBB(byte2: Byte2) with | |||
There was a problem hiding this comment.
Isn't Arith16 better than ArithBB?
| col witness operation_id; | ||
|
|
||
| // operation_id has to be either mul or div. | ||
| operation_id * (1 - operation_id) = 0; |
There was a problem hiding this comment.
It would be better to use std::utils::force_bool(operation_id) maybe?
| operation mload<0> m_addr, m_step -> m_value1, m_value2; | ||
| operation mstore<1> m_addr, m_step, m_value1, m_value2 ->; | ||
|
|
||
| let LATCH = 1; |
There was a problem hiding this comment.
I'm confused at this point. Is it 1 or [1]*? Is it just a one row computation?
| mod binary; | ||
| mod binary_bb; | ||
| mod range; | ||
| mod hash; | ||
| mod memory; | ||
| mod memory_bb; |
There was a problem hiding this comment.
What about, arith16, memory16, arith16_mul as we already name is shift16 by suggestion?
| mstore 100, 0, 7, 0; | ||
| mstore 100, 0, 8, 0; | ||
|
|
||
| // Read updated values (twice) |
There was a problem hiding this comment.
Why do we need to read the updated values twice?
| assert_eq A1, A2, 0xffff, 0xffff; | ||
|
|
||
| // Store at maximal address | ||
| mstore 0xffff, 0xfffc, 1, 0; |
There was a problem hiding this comment.
Why do we have the maximal address as 0xfffcffff instead of 0xffffffff?
| operation mload<0> m_addr, m_step -> m_value1, m_value2; | ||
| operation mstore<1> m_addr, m_step, m_value1, m_value2 ->; |
There was a problem hiding this comment.
Should't address be 32 bits according to memory_bb_test? This seems to be 16 bits only.
| // Except for the last row, if change is 1, then addr has to increase, | ||
| // if it is zero, step has to increase. | ||
| // `m_diff_upper * 2**16 + m_diff_lower` has to be equal to the difference **minus one**. | ||
| // Since we know that both addr and step can only be 32-Bit, this enforces that | ||
| // the values are strictly increasing. | ||
| // TODO check this | ||
| col diff = (m_change * (m_addr' - m_addr)) + (1 - m_change) * (m_step' - m_step); | ||
| (1 - LAST) * (diff - 1 - m_diff_upper * 2**16 - m_diff_lower) = 0; |
There was a problem hiding this comment.
This part needs to be updated too? Address should be two 16-bit limbs.
leonardoalt
force-pushed
the
riscv-bb
branch
from
f529d9a
to
e19487d
Compare
No description provided.