Skip to content

Commit

Permalink
misc!: rename instruction div to div_mod
Browse files Browse the repository at this point in the history
  • Loading branch information
@jan-ferdinand
jan-ferdinand committed Oct 9, 2023
1 parent ee83ab6 commit c3ad923
Show file tree
Hide file tree
Showing 11 changed files with 54 additions and 53 deletions.
2 changes: 1 addition & 1 deletion specification/src/instruction-groups.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ A summary of all instructions and which groups they are part of is given in the
| `xor` | | x | | x | | | | | | | | | | x | |
| `log_2_floor` | | x | | x | | | | | | | x | | | | |
| `pow` | | x | | x | | | | | | | | | | x | |
| `div` | | x | | x | | | | | | x | | | | | |
| `div_mod` | | x | | x | | | | | | x | | | | | |
| `pop_count` | | x | | x | | | | | | | x | | | | |
| `xxadd` | | x | | x | | | | | | x | | | | | |
| `xxmul` | | x | | x | | | | | | x | | | | | |
Expand Down
4 changes: 2 additions & 2 deletions specification/src/instruction-specific-transition-constraints.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -573,12 +573,12 @@ This instruction uses all constraints defined by [instruction groups](instructio
Beyond that, this instruction has no transition constraints.
Instead, correct transition is guaranteed by the [U32 Table](u32-table.md).

## Instruction `div`
## Instruction `div_mod`

This instruction uses all constraints defined by [instruction groups](instruction-groups.md) `step_1`, `stack_remains_and_top_3_unconstrained`, and `keep_ram`.
Additionally, it defines the following transition constraints.

Recall that instruction `div` takes stack `_ d n` and computes `_ q r` where `n` is the numerator, `d` is the denominator, `r` is the remainder, and `q` is the quotient.
Recall that instruction `div_mod` takes stack `_ d n` and computes `_ q r` where `n` is the numerator, `d` is the denominator, `r` is the remainder, and `q` is the quotient.
The following two properties are guaranteed by the [U32 Table](u32-table.md):
1. The remainder `r` is smaller than the denominator `d`, and
1. all four of `n`, `d`, `q`, and `r` are u32s.
Expand Down
2 changes: 1 addition & 1 deletion specification/src/instructions.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -115,7 +115,7 @@ Triton VM cannot know the number of elements that will be absorbed.
| `xor` | 22 | `_ b a` | `_ a^b` | Bitwise exclusive or of the stack's two top-most elements. Crashes the VM if `a` or `b` is not u32. |
| `log_2_floor` | 12 | `_ a` | `_ ⌊log₂(a)⌋` | The number of bits in `a` minus 1, _i.e._, $\lfloor\log_2\texttt{a}\rfloor$. Crashes the VM if `a` is 0 or not u32. |
| `pow` | 30 | `_ e b` | `_ b**e` | The top of the stack to the power of the stack's runner up. Crashes the VM if exponent `e` is not u32. |
| `div` | 20 | `_ d n` | `_ q r` | Division with remainder of numerator `n` by denominator `d`. Guarantees the properties `n == q·d + r` and `r < d`. Crashes the VM if `n` or `d` is not u32 or if `d` is 0. |
| `div_mod` | 20 | `_ d n` | `_ q r` | Division with remainder of numerator `n` by denominator `d`. Guarantees the properties `n == q·d + r` and `r < d`. Crashes the VM if `n` or `d` is not u32 or if `d` is 0. |
| `pop_count` | 28 | `_ a` | `_ w` | Computes the [hamming weight](https://en.wikipedia.org/wiki/Hamming_weight) or “population count” of `a`. Crashes the VM if `a` is not u32. |

## Extension Field Arithmetic on Stack
Expand Down
4 changes: 2 additions & 2 deletions specification/src/processor-table.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -185,7 +185,7 @@ The following additional constraints also apply to every pair of rows.
1. 1. If the current instruction is `split`, then the logarithmic derivative for the Lookup Argument with the U32 Table accumulates `st0` and `st1` in the next row and `ci` in the current row with respect to challenges 🥜, 🌰, and 🥑, and indeterminate 🧷.
1. If the current instruction is `lt`, `and`, `xor`, or `pow`, then the logarithmic derivative for the Lookup Argument with the U32 Table accumulates `st0`, `st1`, and `ci` in the current row and `st0` in the next row with respect to challenges 🥜, 🌰, 🥑, and 🥕, and indeterminate 🧷.
1. If the current instruction is `log_2_floor`, then the logarithmic derivative for the Lookup Argument with the U32 Table accumulates `st0` and `ci` in the current row and `st0` in the next row with respect to challenges 🥜, 🥑, and 🥕, and indeterminate 🧷.
1. If the current instruction is `div`, then the logarithmic derivative for the Lookup Argument with the U32 Table accumulates both
1. If the current instruction is `div_mod`, then the logarithmic derivative for the Lookup Argument with the U32 Table accumulates both
1. `st0` in the next row and `st1` in the current row as well as the constants `opcode(lt)` and `1` with respect to challenges 🥜, 🌰, 🥑, and 🥕, and indeterminate 🧷.
1. `st0` in the current row and `st1` in the next row as well as `opcode(split)` with respect to challenges 🥜, 🌰, and 🥑, and indeterminate 🧷.
1. If the current instruction is `pop_count`, then the logarithmic derivative for the Lookup Argument with the U32 Table accumulates `st0` and `ci` in the current row and `st0` in the next row with respect to challenges 🥜, 🥑, and 🥕, and indeterminate 🧷.
Expand Down Expand Up @@ -219,7 +219,7 @@ The following additional constraints also apply to every pair of rows.
1. `+ xor_deselector·((U32LookupClientLogDerivative' - U32LookupClientLogDerivative)·(🧷 - 🥜·st0 - 🌰·st1 - 🥑·ci - 🥕·st0') - 1)`
1. `+ pow_deselector·((U32LookupClientLogDerivative' - U32LookupClientLogDerivative)·(🧷 - 🥜·st0 - 🌰·st1 - 🥑·ci - 🥕·st0') - 1)`
1. `+ log_2_floor_deselector·((U32LookupClientLogDerivative' - U32LookupClientLogDerivative)·(🧷 - 🥜·st0 - 🥑·ci - 🥕·st0') - 1)`
1. `+ div_deselector·(`<br />
1. `+ div_mod_deselector·(`<br />
&emsp;&emsp;`(U32LookupClientLogDerivative' - U32LookupClientLogDerivative)·(🧷 - 🥜·st0' - 🌰·st1 - 🥑·opcode(lt) - 🥕·1)·(🧷 - 🥜·st0 - 🌰·st1' - 🥑·opcode(split))`<br />
&emsp;&emsp;`- (🧷 - 🥜·st0' - 🌰·st1 - 🥑·opcode(lt) - 🥕·1)`<br />
&emsp;&emsp;`- (🧷 - 🥜·st0 - 🌰·st1' - 🥑·opcode(split))`<br />
Expand Down
2 changes: 1 addition & 1 deletion specification/src/u32-table.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -75,7 +75,7 @@ $$a \texttt{ xor } b = a + b - 2 \cdot (a \texttt{ and } b)$$

Credit for this trick goes, to the best of our knowledge, to [Daniel Lubarov](https://github.com/dlubarov).

For the remaining u32 instruction `div`, the processor triggers the creation of two sections in the U32 Table:
For the remaining u32 instruction `div_mod`, the processor triggers the creation of two sections in the U32 Table:

- One section to ensure that the remainder `r` is smaller than the divisor `d`.
The processor requests the result of `lt` by setting the U32 Table's `CI` register to the opcode of `lt`.
Expand Down
2 changes: 1 addition & 1 deletion triton-vm/src/error.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -156,7 +156,7 @@ mod tests {
#[test]
#[should_panic(expected = "Division by 0 is impossible")]
fn division_by_zero_test() {
let program = triton_program!(push 0 push 5 div halt);
let program = triton_program!(push 0 push 5 div_mod halt);
program.run([].into(), [].into()).unwrap();
}

Expand Down
10 changes: 5 additions & 5 deletions triton-vm/src/example_programs.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -69,7 +69,7 @@ fn greatest_common_divisor() -> Program {
call terminate // _ d n where d != 0
dup 1 // _ d n d
dup 1 // _ d n d n
div // _ d n q r
div_mod // _ d n q r
swap 2 // _ d r q n
pop // _ d r q
pop // _ d r
Expand All @@ -90,8 +90,8 @@ fn program_with_many_u32_instructions() -> Program {
push 5 push 7 pow
push 69584 push 6796 xor
push 64972 push 3915 and
push 98668 push 15787 div
push 15787 push 98668 div
push 98668 push 15787 div_mod
push 15787 push 98668 div_mod
push 98141 push 7397 and
push 67749 push 60797 lt
push 49528 split
Expand All @@ -102,10 +102,10 @@ fn program_with_many_u32_instructions() -> Program {
push 86323 push 37607 xor
push 32374 push 20636 pow
push 97416 log_2_floor
push 14392 push 31589 div
push 14392 push 31589 div_mod
halt
lsb:
push 2 swap 1 div return
push 2 swap 1 div_mod return
is_u32:
split pop push 0 eq return
)
Expand Down
14 changes: 7 additions & 7 deletions triton-vm/src/instruction.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -134,7 +134,7 @@ pub enum AnInstruction<Dest: PartialEq + Default> {
Xor,
Log2Floor,
Pow,
Div,
DivMod,
PopCount,

// Extension field arithmetic on stack
Expand Down Expand Up @@ -182,7 +182,7 @@ impl<Dest: PartialEq + Default> AnInstruction<Dest> {
Xor => 22,
Log2Floor => 12,
Pow => 30,
Div => 20,
DivMod => 20,
PopCount => 28,
XxAdd => 104,
XxMul => 112,
Expand Down Expand Up @@ -225,7 +225,7 @@ impl<Dest: PartialEq + Default> AnInstruction<Dest> {
Xor => "xor",
Log2Floor => "log_2_floor",
Pow => "pow",
Div => "div",
DivMod => "div_mod",
PopCount => "pop_count",
XxAdd => "xxadd",
XxMul => "xxmul",
Expand Down Expand Up @@ -290,7 +290,7 @@ impl<Dest: PartialEq + Default> AnInstruction<Dest> {
Xor => Xor,
Log2Floor => Log2Floor,
Pow => Pow,
Div => Div,
DivMod => DivMod,
PopCount => PopCount,
XxAdd => XxAdd,
XxMul => XxMul,
Expand Down Expand Up @@ -345,7 +345,7 @@ impl<Dest: PartialEq + Default> AnInstruction<Dest> {
Xor => -1,
Log2Floor => 0,
Pow => -1,
Div => 0,
DivMod => 0,
PopCount => 0,
XxAdd => 0,
XxMul => 0,
Expand All @@ -360,7 +360,7 @@ impl<Dest: PartialEq + Default> AnInstruction<Dest> {
pub fn is_u32_instruction(&self) -> bool {
matches!(
self,
Split | Lt | And | Xor | Log2Floor | Pow | Div | PopCount
Split | Lt | And | Xor | Log2Floor | Pow | DivMod | PopCount
)
}
}
Expand Down Expand Up @@ -523,7 +523,7 @@ const fn all_instructions_without_args() -> [AnInstruction<BFieldElement>; Instr
Xor,
Log2Floor,
Pow,
Div,
DivMod,
PopCount,
XxAdd,
XxMul,
Expand Down
9 changes: 5 additions & 4 deletions triton-vm/src/parser.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -255,7 +255,7 @@ fn an_instruction(s: &str) -> ParseResult<AnInstruction<String>> {
let absorb = instruction("absorb", Absorb);
let squeeze = instruction("squeeze", Squeeze);

let hashing_related = alt((hash, divine_sibling, absorb_init, absorb, squeeze));
let hashing_related = alt((hash, absorb_init, absorb, squeeze));

// Arithmetic on stack instructions
let add = instruction("add", Add);
Expand All @@ -268,15 +268,16 @@ fn an_instruction(s: &str) -> ParseResult<AnInstruction<String>> {
let xor = instruction("xor", Xor);
let log_2_floor = instruction("log_2_floor", Log2Floor);
let pow = instruction("pow", Pow);
let div = instruction("div", Div);
let div_mod = instruction("div_mod", DivMod);
let pop_count = instruction("pop_count", PopCount);
let xxadd = instruction("xxadd", XxAdd);
let xxmul = instruction("xxmul", XxMul);
let xinvert = instruction("xinvert", XInvert);
let xbmul = instruction("xbmul", XbMul);

let base_field_arithmetic_on_stack = alt((add, mul, invert, eq));
let bitwise_arithmetic_on_stack = alt((split, lt, and, xor, log_2_floor, pow, div, pop_count));
let bitwise_arithmetic_on_stack =
alt((split, lt, and, xor, log_2_floor, pow, div_mod, pop_count));
let extension_field_arithmetic_on_stack = alt((xxadd, xxmul, xinvert, xbmul));
let arithmetic_on_stack = alt((
base_field_arithmetic_on_stack,
Expand All @@ -295,7 +296,7 @@ fn an_instruction(s: &str) -> ParseResult<AnInstruction<String>> {
// Successfully parsing "assert" before trying "assert_vector" can lead to
// picking the wrong one. By trying them in the order of longest first, less
// backtracking is necessary.
let syntax_ambiguous = alt((assert_vector, assert_, divine));
let syntax_ambiguous = alt((assert_vector, assert_, divine_sibling, divine));

alt((
opstack_manipulation,
Expand Down
Loading

0 comments on commit c3ad923

Please sign in to comment.