Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Start VM with initialized Sponge state #296

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Start VM with initialized Sponge state #296

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions specification/src/arithmetization-overview.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,12 +38,12 @@ Before automatic degree lowering:
| [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 |
| [HashTable](hash-table.md) | 22 | 45 | 47 | 2 | 9 |
| [HashTable](hash-table.md) | 22 | 45 | 48 | 2 | 10 |
| [CascadeTable](cascade-table.md) | 2 | 1 | 3 | 0 | 4 |
| [LookupTable](lookup-table.md) | 3 | 1 | 4 | 1 | 3 |
| [U32Table](u32-table.md) | 1 | 15 | 22 | 2 | 12 |
| [Grand Cross-Table Argument](table-linking.md) | 0 | 0 | 0 | 14 | 1 |
| **TOTAL** | **79** | **76** | **178** | **23** | **19** |
| **TOTAL** | **79** | **76** | **179** | **23** | **19** |

After automatically lowering degree to 4:

Expand All @@ -54,10 +54,10 @@ After automatically lowering degree to 4:
| [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 |
| [HashTable](hash-table.md) | 22 | 52 | 84 | 2 |
| [HashTable](hash-table.md) | 22 | 52 | 85 | 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** | **414** | **23** |
| **TOTAL** | **81** | **94** | **415** | **23** |
<!-- auto-gen info stop -->
91 changes: 7 additions & 84 deletions specification/src/hash-table.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -119,17 +119,6 @@ Both types of challenges are X-field elements, _i.e._, elements of $\mathbb{F}_{
1. For `i` $\in \{0, \dots, 3\}$ and `limb` $\in \{$`highest`, `mid_high`, `mid_low`, `lowest` $\}$:<br />
`state_i_limb_LookupClientLogDerivative` has accumulated `state_i_limb_lkin` and `state_i_limb_lkout` with respect to challenges 🍒, 🍓 and indeterminate 🧺.

### Initial Constraints as Polynomials

1. `Mode - 1`
1. `round_no`
1. `RunningEvaluationReceiveChunk - 🪣 - (🪑^10 + state_0·🪑^9 + state_1·🪑^8 + state_2·🪑^7 + state_3·🪑^6 + state_4·🪑^5 + state_5·🪑^4 + state_6·🪑^3 + state_7·🪑^2 + state_8·🪑 + state_9)`
1. `RunningEvaluationHashInput - 1`
1. `RunningEvaluationHashDigest - 1`
1. `RunningEvaluationSponge - 1`
1. For `i` $\in \{0, \dots, 3\}$ and `limb` $\in \{$`highest`, `mid_high`, `mid_low`, `lowest` $\}$:<br />
`state_i_limb_LookupClientLogDerivative·(🧺 - 🍒·state_i_limb_lkin - 🍓·state_i_limb_lkout) - 1`

## Consistency Constraints

1. The `Mode` is a valid mode, _i.e._, $\in \{0, \dots, 3\}$.
Expand All @@ -153,34 +142,13 @@ Let `state_i_hi_limbs_minus_2_pow_32` be an alias for that difference:
1. The `state_i_inv` is the inverse of `state_i_hi_limbs_minus_2_pow_32` or `state_i_hi_limbs_minus_2_pow_32` is 0.
1. The round constants adhere to the specification of Tip5.

### Consistency Constraints as Polynomials

1. `(Mode - 0)·(Mode - 1)·(Mode - 2)·(Mode - 3)`
1. `(Mode - 2)·(CI - opcode(hash))`
1. `(Mode - 0)·(Mode - 1)·(Mode - 3)`<br />
` ·(CI - opcode(sponge_init))·(CI - opcode(sponge_absorb))·(CI - opcode(sponge_squeeze))`
1. `(Mode - 1)·(Mode - 2)·(Mode - 3)·(round_no - 0)`
1. `(CI - opcode(hash))·(CI - opcode(sponge_absorb))·(CI - opcode(sponge_squeeze))·(round_no - 0)`
1. For `i` $\in\{10, \dots, 15\}$:<br />
`·(CI - opcode(hash))·(CI - opcode(sponge_absorb))·(CI - opcode(sponge_squeeze))`<br />
`·(state_i - 0)`
1. For `i` $\in\{10, \dots, 15\}$:<br />
`(round_no - 1)·(round_no - 2)·(round_no - 3)·(round_no - 4)·(round_no - 5)`<br />
`·(Mode - 0)·(Mode - 1)·(Mode - 2)`<br />
`·(state_i - 1)`
1. For `i` $\in\{0, \dots, 3\}$:
define `state_i_hi_limbs_minus_2_pow_32 := 2^32 - 1 - 2^16·state_i_highest_lk_in - state_i_mid_high_lk_in`.
1. `(1 - state_i_inv · state_i_hi_limbs_minus_2_pow_32)·(2^16·state_i_mid_low_lk_in + state_i_lowest_lk_in)`
1. `(1 - state_i_inv · state_i_hi_limbs_minus_2_pow_32)·state_i_inv`
1. `(1 - state_i_inv · state_i_hi_limbs_minus_2_pow_32)·state_i_hi_limbs_minus_2_pow_32`

## Transition Constraints

1. If the `round_no` is 5, then the `round_no` in the next row is 0.
1. If the `Mode` is not `pad` and the current instruction `CI` is not `sponge_init` and the `round_no` is not 5, then the `round_no` increments by 1.
1. If the `Mode` in the next row is `program_hashing` and the `round_no` in the next row is 0, then receive a chunk of instructions with respect to challenges 🪣 and 🪑.
1. If the `Mode` changes from `program_hashing`, then the [Evaluation Argument](evaluation-argument.md) of `state_0` through `state_4` with respect to indeterminate 🥬 equals the public program digest challenge, 🫑.
1. If the `Mode` is `program_hashing` and the `Mode` in the next row is `sponge`, then the current instruction in the next row is `sponge_init`.
1. If the `Mode` is `program_hashing` and the `Mode` in the next row is `sponge`, then the capacity in the next row is 0.
1. If the `round_no` is not 5 and the current instruction `CI` is not `sponge_init`, then the current instruction does not change.
1. If the `round_no` is not 5 and the current instruction `CI` is not `sponge_init`, then the `Mode` does not change.
1. If the `Mode` is `sponge`, then the `Mode` in the next row is `sponge` or `hash` or `pad`.
Expand All @@ -189,8 +157,12 @@ define `state_i_hi_limbs_minus_2_pow_32 := 2^32 - 1 - 2^16·state_i_highest_lk_i
1. If the `round_no` in the next row is 0
and the `Mode` in the next row is either `program_hashing` or `sponge`
and the instruction in the next row is either `sponge_absorb` or `sponge_init`,
then the capacity's state registers don't change.
1. If the `round_no` in the next row is 0 and the current instruction in the next row is `sponge_squeeze`, then none of the state registers change.
then the capacity's state registers don't change,
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The capacity elements do not change if the next instruction is sponge_init? That doesn't sound right. I would expect them to be set to zero.

or the `Mode` in the current row is `program_hashing` and the `Mode` in the next row is `sponge`.
1. If the `round_no` in the next row is 0
and the current instruction in the next row is `sponge_squeeze`,
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

"current instruction in the next row" is confusing; consider abbreviating to "CI".

then none of the state registers change,
or the `Mode` in the current row is `program_hashing`.
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So if the current mode is program_hashing and the next instruction is sponge_squeeze then the state registers can change? Very counter-intuitive.

1. If the `round_no` in the next row is 0 and the `Mode` in the next row is `hash`, then `RunningEvaluationHashInput` accumulates the next row with respect to challenges 🧄₀ through 🧄₉ and indeterminate 🚪.
Otherwise, it remains unchanged.
1. If the `round_no` in the next row is 5 and the `Mode` in the next row is `hash`, then `RunningEvaluationHashDigest` accumulates the next row with respect to challenges 🧄₀ through 🧄₄ and indeterminate 🪟.
Expand All @@ -203,59 +175,10 @@ Otherwise, `state_i_limb_LookupClientLogDerivative` remains unchanged.
1. For `r` $\in\{0, \dots, 4\}$:<br />
If the `round_no` is `r`, the `state` registers adhere to the rules of applying round `r` of the Tip5 permutation.

### Transition Constraints as Polynomials

1. `(round_no - 0)·(round_no - 1)·(round_no - 2)·(round_no - 3)·(round_no - 4)·(round_no' - 0)`
1. `(Mode - 0)·(round_no - 5)·(CI - opcode(sponge_init))·(round_no' - round_no - 1)`
1. `RunningEvaluationReceiveChunk' - 🪣·RunningEvaluationReceiveChunk - (🪑^10 + state_0·🪑^9 + state_1·🪑^8 + state_2·🪑^7 + state_3·🪑^6 + state_4·🪑^5 + state_5·🪑^4 + state_6·🪑^3 + state_7·🪑^2 + state_8·🪑 + state_9)`
1. `(Mode - 0)·(Mode - 2)·(Mode - 3)·(Mode' - 1)·(🥬^5 + state_0·🥬^4 + state_1·🥬^3 + state_2·🥬^2 + state_3·🥬^1 + state_4 - 🫑)`
1. `(Mode - 0)·(Mode - 2)·(Mode - 3)·(Mode' - 2)·(CI' - opcode(sponge_init))`
1. `(round_no - 5)·(CI - opcode(sponge_init))·(CI' - CI)`
1. `(round_no - 5)·(CI - opcode(sponge_init))·(Mode' - Mode)`
1. `(Mode - 0)·(Mode - 1)·(Mode - 3)·(Mode' - 0)·(Mode' - 2)·(Mode' - 3)`
1. `(Mode - 0)·(Mode - 1)·(Mode - 2)·(Mode' - 0)·(Mode' - 3)`
1. `(Mode - 1)·(Mode - 2)·(Mode - 3)·(Mode' - 0)`
1. `(round_no' - 1)·(round_no' - 2)·(round_no' - 3)·(round_no' - 4)·(round_no' - 5)`<br />
`·(Mode' - 3)·(Mode' - 0)`<br />
`·(CI' - opcode(sponge_init))`<br />
`·(🧄₁₀·(state_10' - state_10) + 🧄₁₁·(state_11' - state_11) + 🧄₁₂·(state_12' - state_12) + 🧄₁₃·(state_13' - state_13) + 🧄₁₄·(state_14' - state_14) + 🧄₁₅·(state_15' - state_15))`
1. `(round_no' - 1)·(round_no' - 2)·(round_no' - 3)·(round_no' - 4)·(round_no' - 5)`<br />
`·(CI' - opcode(hash))·(CI' - opcode(sponge_init))·(CI' - opcode(sponge_absorb))`<br />
`·(🧄₀·(state_0' - state_0) + 🧄₁·(state_1' - state_1) + 🧄₂·(state_2' - state_2) + 🧄₃·(state_3' - state_3) + 🧄₄·(state_4' - state_4)`<br />
` + 🧄₅·(state_5' - state_5) + 🧄₆·(state_6' - state_6) + 🧄₇·(state_7' - state_7) + 🧄₈·(state_8' - state_8) + 🧄₉·(state_9' - state_9)`<br />
` + 🧄₁₀·(state_10' - state_10) + 🧄₁₁·(state_11' - state_11) + 🧄₁₂·(state_12' - state_12) + 🧄₁₃·(state_13' - state_13) + 🧄₁₄·(state_14' - state_14) + 🧄₁₅·(state_15' - state_15))`
1. `(round_no' - 0)·(round_no' - 1)·(round_no' - 2)·(round_no' - 3)·(round_no' - 4)`<br />
`·(RunningEvaluationHashInput' - 🚪·RunningEvaluationHashInput - 🧄₀·state_0' - 🧄₁·state_1' - 🧄₂·state_2' - 🧄₃·state_3' - 🧄₄·state_4' - 🧄₅·state_5' - 🧄₆·state_6' - 🧄₇·state_7' - 🧄₈·state_8' - 🧄₉·state_9')`<br />
`+ (round_no' - 0)·(RunningEvaluationHashInput' - RunningEvaluationHashInput)`<br />
`+ (Mode' - 3)·(RunningEvaluationHashInput' - RunningEvaluationHashInput)`
1. `(round_no' - 0)·(round_no' - 1)·(round_no' - 2)·(round_no' - 3)·(round_no' - 4)`<br />
`·(Mode' - 0)·(Mode' - 1)·(Mode' - 2)`<br />
`·(RunningEvaluationHashDigest' - 🪟·RunningEvaluationHashDigest - 🧄₀·state_0' - 🧄₁·state_1' - 🧄₂·state_2' - 🧄₃·state_3' - 🧄₄·state_4')`<br />
`+ (round_no' - 5)·(RunningEvaluationHashDigest' - RunningEvaluationHashDigest)`<br />
`+ (Mode' - 3)·(RunningEvaluationHashDigest' - RunningEvaluationHashDigest)`
1. `(round_no' - 1)·(round_no' - 2)·(round_no' - 3)·(round_no' - 4)·(round_no' - 5)`<br />
`·(CI' - opcode(hash))`<br />
`·(RunningEvaluationSponge' - 🧽·RunningEvaluationSponge - 🧅·CI' - 🧄₀·state_0' - 🧄₁·state_1' - 🧄₂·state_2' - 🧄₃·state_3' - 🧄₄·state_4' - 🧄₅·state_5' - 🧄₆·state_6' - 🧄₇·state_7' - 🧄₈·state_8' - 🧄₉·state_9')`<br />
`+ (RunningEvaluationSponge' - RunningEvaluationSponge)·(round_no' - 0)`<br />
`+ (RunningEvaluationSponge' - RunningEvaluationSponge)·(CI' - opcode(sponge_init))·(CI' - opcode(sponge_absorb))·(CI' - opcode(sponge_squeeze))`
1. For `i` $\in \{0, \dots, 3\}$ and `limb` $\in \{$`highest`, `mid_high`, `mid_low`, `lowest` $\}$:<br />
`(round_no' - 5)·(Mode' - 0)·(CI' - opcode(sponge_init))·((state_i_limb_LookupClientLogDerivative' - state_i_limb_LookupClientLogDerivative)·(🧺 - 🍒·state_i_limb_lkin' - 🍓·state_i_limb_lkout') - 1)`<br />
`+ (round_no' - 0)·(round_no' - 1)·(round_no' - 2)·(round_no' - 3)·(round_no' - 4)`<br />
`·(state_i_limb_LookupClientLogDerivative' - state_i_limb_LookupClientLogDerivative)`<br />
`+ (CI' - opcode(hash))·(CI' - opcode(sponge_absorb))·(CI' - opcode(sponge_squeeze))`<br />
`·(state_i_limb_LookupClientLogDerivative' - state_i_limb_LookupClientLogDerivative)`
1. The remaining constraints are left as an exercise to the reader.
For hints, see the [Tip5 paper](https://eprint.iacr.org/2023/107.pdf).

## Terminal Constraints

1. If the `Mode` is `program_hashing`, then the [Evaluation Argument](evaluation-argument.md) of `state_0` through `state_4` with respect to indeterminate 🥬 equals the public program digest challenge, 🫑.
1. If the `Mode` is not `pad` and the current instruction `CI` is not `sponge_init`, then the `round_no` is 5.

### Terminal Constraints as Polynomials

1. `🥬^5 + state_0·🥬^4 + state_1·🥬^3 + state_2·🥬^2 + state_3·🥬 + state_4 - 🫑`
1. `(Mode - 0)·(CI - opcode(sponge_init))·(round_no - 5)`

[^oxfoi]:
This is a special property of the Oxfoi prime.
3 changes: 0 additions & 3 deletions triton-vm/src/error.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,9 +75,6 @@ pub enum InstructionError {
#[error("division by 0 is impossible")]
DivisionByZero,

#[error("the Sponge state must be initialized before it can be used")]
SpongeNotInitialized,

#[error("the logarithm of 0 does not exist")]
LogarithmOfZero,

Expand Down
Loading