Skip to content

Commit

Permalink
fix: Fix completeness bug of recurse_or_return
Browse files Browse the repository at this point in the history
The Jump Stack Table did not know that instruction `recurse_or_return`
could return. Consequently, proving correct execution of programs
making use of instruction `recurse_or_return` was not possible (except
for a few specific cases).
  • Loading branch information
jan-ferdinand committed Jul 22, 2024
1 parent 6fd207f commit 32ac704
Show file tree
Hide file tree
Showing 3 changed files with 27 additions and 44 deletions.
12 changes: 6 additions & 6 deletions specification/src/arithmetization-overview.md
Original file line number Diff line number Diff line change
Expand Up @@ -15,9 +15,9 @@
| [CascadeTable](cascade-table.md) | 6 | 2 | 12 |
| [LookupTable](lookup-table.md) | 4 | 2 | 10 |
| [U32Table](u32-table.md) | 10 | 1 | 13 |
| DegreeLowering | 200 | 36 | 308 |
| DegreeLowering | 201 | 36 | 309 |
| Randomizers | 0 | 1 | 3 |
| **TOTAL** | **349** | **86** | **607** |
| **TOTAL** | **350** | **86** | **608** |
<!-- auto-gen info stop table_overview -->

## Constraints
Expand All @@ -37,7 +37,7 @@ Before automatic degree lowering:
| [ProcessorTable](processor-table.md) | 29 | 10 | 41 | 1 | 19 |
| [OpStackTable](operational-stack-table.md) | 3 | 0 | 5 | 0 | 4 |
| [RamTable](random-access-memory-table.md) | 7 | 0 | 12 | 1 | 5 |
| [JumpStackTable](jump-stack-table.md) | 6 | 0 | 6 | 0 | 4 |
| [JumpStackTable](jump-stack-table.md) | 6 | 0 | 6 | 0 | 5 |
| [HashTable](hash-table.md) | 22 | 45 | 47 | 2 | 9 |
| [CascadeTable](cascade-table.md) | 2 | 1 | 3 | 0 | 4 |
| [LookupTable](lookup-table.md) | 3 | 1 | 4 | 1 | 3 |
Expand All @@ -53,13 +53,13 @@ After automatically lowering degree to 4:
| [ProcessorTable](processor-table.md) | 31 | 10 | 207 | 1 |
| [OpStackTable](operational-stack-table.md) | 3 | 0 | 5 | 0 |
| [RamTable](random-access-memory-table.md) | 7 | 0 | 13 | 1 |
| [JumpStackTable](jump-stack-table.md) | 6 | 0 | 6 | 0 |
| [JumpStackTable](jump-stack-table.md) | 6 | 0 | 7 | 0 |
| [HashTable](hash-table.md) | 22 | 52 | 84 | 2 |
| [CascadeTable](cascade-table.md) | 2 | 1 | 3 | 0 |
| [LookupTable](lookup-table.md) | 3 | 1 | 4 | 1 |
| [U32Table](u32-table.md) | 1 | 26 | 34 | 2 |
| [Grand Cross-Table Argument](table-linking.md) | 0 | 0 | 0 | 14 |
| **TOTAL** | **81** | **94** | **366** | **23** |
| **TOTAL** | **81** | **94** | **367** | **23** |
<!-- auto-gen info stop constraints_overview -->


Expand All @@ -71,5 +71,5 @@ In order to gauge the runtime cost for this step, the following table provides e
<!-- auto-gen info start tasm_air_evaluation_cost -->
| Processor | Op Stack | RAM |
|----------:|---------:|------:|
| 34469 | 63967 | 22617 |
| 34477 | 63981 | 22620 |
<!-- auto-gen info stop tasm_air_evaluation_cost -->
9 changes: 5 additions & 4 deletions specification/src/jump-stack-table.md
Original file line number Diff line number Diff line change
Expand Up @@ -164,16 +164,17 @@ None.
1. The jump stack pointer `jsp` increases by 1, *or*
1. (`jsp` does not change and `jso` does not change and `jsd` does not change and the cycle counter `clk` increases by 1), *or*
1. (`jsp` does not change and `jso` does not change and `jsd` does not change and the current instruction `ci` is `call`), *or*
1. (`jsp` does not change and the current instruction `ci` is `return`).
1. (`jsp` does not change and the current instruction `ci` is `return`), *or*
1. (`jsp` does not change and the current instruction `ci` is `recurse_or_return`).
1. The running product for the permutation argument `rppa` absorbs the next row with respect to challenges 🍇, 🍅, 🍌, 🍏, and 🍐 and indeterminate 🧴.
1. If the jump stack pointer `jsp` does not change, then the logarithmic derivative for the clock jump difference lookup `ClockJumpDifferenceLookupClientLogDerivative` accumulates a factor `(clk' - clk)` relative to indeterminate 🪞.
Otherwise, it remains the same.

Written as Disjunctive Normal Form, the same constraints can be expressed as:
1. The jump stack pointer `jsp` increases by 1 or the jump stack pointer `jsp` does not change
1. The jump stack pointer `jsp` increases by 1 or the jump stack origin `jso` does not change or current instruction `ci` is `return`
1. The jump stack pointer `jsp` increases by 1 or the jump stack destination `jsd` does not change or current instruction `ci` is `return`
1. The jump stack pointer `jsp` increases by 1 or the cycle count `clk` increases by 1 or current instruction `ci` is `call` or current instruction `ci` is `return`
1. The jump stack pointer `jsp` increases by 1 or the jump stack origin `jso` does not change or current instruction `ci` is `return` or `recurse_or_return`
1. The jump stack pointer `jsp` increases by 1 or the jump stack destination `jsd` does not change or current instruction `ci` is `return` or `recurse_or_return`
1. The jump stack pointer `jsp` increases by 1 or the cycle count `clk` increases by 1 or current instruction `ci` is `call` or current instruction `ci` is `return` or `recurse_or_return`
1. `rppa' - rppa·(🧴 - 🍇·clk' - 🍅·ci' - 🍌·jsp' - 🍏·jso' - 🍐·jsd')`
1. - the `jsp` changes or the logarithmic derivative accumulates a summand, and
- the `jsp` does not change or the logarithmic derivative does not change.
Expand Down
50 changes: 16 additions & 34 deletions triton-vm/src/table/jump_stack_table.rs
Original file line number Diff line number Diff line change
Expand Up @@ -82,6 +82,8 @@ impl ExtJumpStackTable {
let call_opcode =
circuit_builder.b_constant(Instruction::Call(BFieldElement::default()).opcode_b());
let return_opcode = circuit_builder.b_constant(Instruction::Return.opcode_b());
let recurse_or_return_opcode =
circuit_builder.b_constant(Instruction::RecurseOrReturn.opcode_b());

let clk = circuit_builder.input(CurrentBaseRow(CLK.master_base_table_index()));
let ci = circuit_builder.input(CurrentBaseRow(CI.master_base_table_index()));
Expand All @@ -106,50 +108,30 @@ impl ExtJumpStackTable {
ClockJumpDifferenceLookupClientLogDerivative.master_ext_table_index(),
));

// 1. The jump stack pointer jsp increases by 1
// or the jump stack pointer jsp does not change
let jsp_inc_or_stays =
(jsp_next.clone() - jsp.clone() - one()) * (jsp_next.clone() - jsp.clone());

// 2. The jump stack pointer jsp increases by 1
// or current instruction ci is return
// or the jump stack origin jso does not change
let jsp_inc_by_one_or_ci_is_return =
(jsp_next.clone() - jsp.clone() - one()) * (ci.clone() - return_opcode.clone());
let jsp_inc_or_jso_stays_or_ci_is_ret =
jsp_inc_by_one_or_ci_is_return.clone() * (jso_next.clone() - jso);

// 3. The jump stack pointer jsp increases by 1
// or current instruction ci is return
// or the jump stack destination jsd does not change
let jsp_inc_or_jsd_stays_or_ci_ret =
jsp_inc_by_one_or_ci_is_return * (jsd_next.clone() - jsd);

// 4. The jump stack pointer jsp increases by 1
// or the cycle count clk increases by 1
// or current instruction ci is call
// or current instruction ci is return
let jsp_inc_or_clk_inc_or_ci_call_or_ci_ret = (jsp_next.clone() - jsp.clone() - one())
let jsp_inc_by_one_or_ci_can_return = (jsp_next.clone() - jsp.clone() - one())
* (ci.clone() - return_opcode)
* (ci.clone() - recurse_or_return_opcode);
let jsp_inc_or_jso_stays_or_ci_can_ret =
jsp_inc_by_one_or_ci_can_return.clone() * (jso_next.clone() - jso);

let jsp_inc_or_jsd_stays_or_ci_can_ret =
jsp_inc_by_one_or_ci_can_return.clone() * (jsd_next.clone() - jsd);

let jsp_inc_or_clk_inc_or_ci_call_or_ci_can_ret = jsp_inc_by_one_or_ci_can_return
* (clk_next.clone() - clk.clone() - one())
* (ci.clone() - call_opcode)
* (ci - return_opcode);
* (ci.clone() - call_opcode);

// The running product for the permutation argument `rppa` accumulates one row in each
// row, relative to weights `a`, `b`, `c`, `d`, `e`, and indeterminate `α`.
let compressed_row = circuit_builder.challenge(JumpStackClkWeight) * clk_next.clone()
+ circuit_builder.challenge(JumpStackCiWeight) * ci_next
+ circuit_builder.challenge(JumpStackJspWeight) * jsp_next.clone()
+ circuit_builder.challenge(JumpStackJsoWeight) * jso_next
+ circuit_builder.challenge(JumpStackJsdWeight) * jsd_next;

let rppa_updates_correctly =
rppa_next - rppa * (circuit_builder.challenge(JumpStackIndeterminate) - compressed_row);

// The running sum of the logarithmic derivative for the clock jump difference Lookup
// Argument accumulates a summand of `clk_diff` if and only if the `jsp` does not change.
// Expressed differently:
// - the `jsp` changes or the log derivative accumulates a summand, and
// - the `jsp` does not change or the log derivative does not change.
let log_derivative_remains =
clock_jump_diff_log_derivative_next.clone() - clock_jump_diff_log_derivative.clone();
let clk_diff = clk_next - clk;
Expand All @@ -163,9 +145,9 @@ impl ExtJumpStackTable {

vec![
jsp_inc_or_stays,
jsp_inc_or_jso_stays_or_ci_is_ret,
jsp_inc_or_jsd_stays_or_ci_ret,
jsp_inc_or_clk_inc_or_ci_call_or_ci_ret,
jsp_inc_or_jso_stays_or_ci_can_ret,
jsp_inc_or_jsd_stays_or_ci_can_ret,
jsp_inc_or_clk_inc_or_ci_call_or_ci_can_ret,
rppa_updates_correctly,
log_derivative_updates_correctly,
]
Expand Down

0 comments on commit 32ac704

Please sign in to comment.