Skip to content

Commit

Permalink
feat: Introduce instruction recurse_or_return
Browse files Browse the repository at this point in the history 
Instruction `recurse_or_return` behaves – surprise! – either like
instruction `recurse` or like instruction `return`. The (deterministic)
decision which behavior to exhibit is made at runtime and depends on the
current stack, in particular, on stack elements `ST5` and `ST6`.

If `ST5 == ST6`, instruction `recurse_or_return` exhibits the same
behavior as instruction `return`. Otherwise, the instruction exhibits
the same behavior as instruction `recurse`.
  • Loading branch information
@jan-ferdinand
jan-ferdinand committed May 29, 2024
2 parents be87aef + d669ed9 commit 98dbd9f
Show file tree
Hide file tree
Showing 11 changed files with 312 additions and 85 deletions.
8 changes: 4 additions & 4 deletions specification/src/arithmetization-overview.md
View file
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 | 220 | 36 | 328 |
| DegreeLowering | 223 | 36 | 331 |
| Randomizers | 0 | 1 | 3 |
| **TOTAL** | **369** | **86** | **627** |
| **TOTAL** | **372** | **86** | **630** |
<!-- auto-gen info stop -->

## Constraints
Expand Down Expand Up @@ -50,7 +50,7 @@ After automatically lowering degree to 4:
| table name | #initial | #consistency | #transition | #terminal |
|:-----------------------------------------------|---------:|-------------:|------------:|----------:|
| [ProgramTable](program-table.md) | 6 | 4 | 10 | 2 |
| [ProcessorTable](processor-table.md) | 31 | 10 | 255 | 1 |
| [ProcessorTable](processor-table.md) | 31 | 10 | 258 | 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 |
Expand All @@ -59,5 +59,5 @@ After automatically lowering degree to 4:
| [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** | **414** | **23** |
| **TOTAL** | **81** | **94** | **417** | **23** |
<!-- auto-gen info stop -->
4 changes: 2 additions & 2 deletions specification/src/data-structures.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -46,8 +46,8 @@ The other mechanism is [dedicated instructions](instructions.md#opstack-manipula

Another last-in;first-out data structure, similar to the op stack.
The jump stack keeps track of return and destination addresses.
It changes only when control follows a `call` or `return` instruction.
Furthermore, executing instruction `recurse` requires a non-empty jump stack.
It changes only when control follows a `call` or `return` instruction, and might change through the `recurse_or_return` instruction.
Furthermore, executing instructions `return`, `recurse`, and `recurse_or_return` require a non-empty jump stack.

---

Expand Down
1 change: 1 addition & 0 deletions specification/src/instruction-groups.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,7 @@ A summary of all instructions and which groups they are part of is given in the
| `call` + `d` | | | x | x | | | | | | x | 0 | x | | | |
| `return` | | | x | x | | | | | | x | 0 | x | | | |
| `recurse` | | | x | x | x | | | | | x | 0 | x | | | |
| `recurse_or_return` | | | x | x | | | | | | x | 0 | x | | | |
| `assert` | | | x | x | | x | | | | | | | | x | |
| `halt` | | | x | x | | x | | | | x | 0 | x | | | |
| `read_mem` + `n` | x | x | x | | | | x | | | | | | | | |
Expand Down
19 changes: 19 additions & 0 deletions specification/src/instruction-specific-transition-constraints.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -286,6 +286,25 @@ In addition to its [instruction groups](instruction-groups.md), this instruction
1. `jsd' - jsd`
1. `ip' - jsd`

## Instruction `recurse_or_return`

In addition to its [instruction groups](instruction-groups.md), this instruction has the following constraints.

### Description

1. If `ST5` equals `ST6`, then `ip` in the next row equals `jso` in the current row.
1. If `ST5` equals `ST6`, then `jsp` decrements by one.
1. If `ST5` equals `ST6`, then `hv0` in the current row is 0.
1. If `ST5` is unequal to `ST6`, then `hv0` in the current row is the inverse of `(ST6 - ST5)`.
1. If `ST5` is unequal to `ST6`, then `ip` in the next row is equal to `jsd` in the current row.
1. If `ST5` is unequal to `ST6`, then `jsp` remains unchanged.
1. If `ST5` is unequal to `ST6`, then `jso` remains unchanged.
1. If `ST5` is unequal to `ST6`, then `jsd` remains unchanged.

### Helper variable definitions for `recurse_or_return`

To help arithmetizing the equality check between `ST5` and `ST6`, helper variable `hv0` is the inverse-or-zero of `(ST6 - ST5)`.

## Instruction `assert`

In addition to its [instruction groups](instruction-groups.md), this instruction has the following constraints.
Expand Down
Loading

0 comments on commit 98dbd9f

Please sign in to comment.