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.

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

chore: update docs #1291

Merged
merged 56 commits into from
Jan 27, 2025
Merged
Changes from 1 commit
Commits
Show all changes
56 commits
Select commit Hold shift + click to select a range
c509004
chore: structure ISA
yi-sun Jan 26, 2025
9eb6f2c
feat: update design and specs
yi-sun Jan 26, 2025
4878dee
feat: clean up ISA intro, move PUBLISH to system
yi-sun Jan 26, 2025
ca23852
feat: separate ISA docs into extensions
yi-sun Jan 26, 2025
3d0a658
feat: incorporate user IO section into RV32IM extensions
yi-sun Jan 26, 2025
2f408ea
feat: separate out phantom sub-instructions
yi-sun Jan 26, 2025
ed8b532
feat: move native, and add intro links
yi-sun Jan 26, 2025
08ec27f
feat: clean up native language
yi-sun Jan 26, 2025
10a091f
chore: align Poseidon2 opcode names
yi-sun Jan 26, 2025
6531ace
feat: remove register and immediate sections
yi-sun Jan 26, 2025
b267802
feat: move syscalls
yi-sun Jan 26, 2025
a320784
feat: explain x0 behavior
yi-sun Jan 26, 2025
d51eeb1
feat: align naming and wording for keccak, sha256, ecc
yi-sun Jan 26, 2025
2e88008
chore: align naming of pairing opcode with repo
yi-sun Jan 26, 2025
5d81e23
feat: compress memory explanation
yi-sun Jan 26, 2025
2c8981b
feat: explain hints
yi-sun Jan 26, 2025
aa6f929
feat: update public values description
yi-sun Jan 26, 2025
bc7536c
feat: more intro edits
yi-sun Jan 26, 2025
55a92af
feat: document address space constraints
yi-sun Jan 26, 2025
c6414f7
fix: replace e by 2 in keccak
yi-sun Jan 26, 2025
8164643
chore: revert extraneous RISCV
yi-sun Jan 26, 2025
dee48a7
feat: split custom instruction and transpiler pages
yi-sun Jan 26, 2025
f7055cb
feat: update readme to explain ELF and transpiler
yi-sun Jan 26, 2025
b6e349e
feat: separate custom instruction format into extensions
yi-sun Jan 26, 2025
d3b0c1d
feat: split transpiler format into extensions
yi-sun Jan 26, 2025
c8f2a57
chore: remove syscalls from ISA
yi-sun Jan 26, 2025
5514f82
feat: add missing links
yi-sun Jan 26, 2025
d9b5b8f
[chore] Mention the new `HintRandom` phantom discriminant in the docs…
Golovanov399 Jan 26, 2025
9103017
feat: update hintstorew and hintbuffer in RISCV
yi-sun Jan 26, 2025
cde2ed3
fix: hintstore and hintbuffer details
yi-sun Jan 26, 2025
a7c334b
feat: add todos and hintrandom to riscv
yi-sun Jan 26, 2025
851198f
feat: remove unsupported system phantom opcodes
yi-sun Jan 26, 2025
35df996
feat: add hintbuffer, split out RV32IM
yi-sun Jan 26, 2025
6122cf3
feat: reword x0 language
yi-sun Jan 26, 2025
8b56f40
feat: explicitly specify x0 handling
yi-sun Jan 26, 2025
098252e
feat: make setup transpilation explicit
yi-sun Jan 26, 2025
81b136c
feat: add setup for complex
yi-sun Jan 26, 2025
bf44ee2
feat: update pairing opcodes
yi-sun Jan 26, 2025
c5d796c
fix: Fp2 -> Fp
yi-sun Jan 26, 2025
6d6ffca
fix: correct ind(rd) definition
yi-sun Jan 26, 2025
8d8ff43
feat: add docs for HintLoad
yi-sun Jan 26, 2025
b709ba7
fix: typo
yi-sun Jan 26, 2025
1e764c7
feat: update hintrandom in transpiler
yi-sun Jan 26, 2025
96b99ad
fix: specify the phantom operand c for ecc and pairing hints
yi-sun Jan 26, 2025
4be6a3b
chore: clarify curve / pairing notation
yi-sun Jan 26, 2025
3947336
fix: make phantom notation consistent
yi-sun Jan 26, 2025
6de4347
fix: wording
yi-sun Jan 26, 2025
f901f23
Update docs/specs/ISA.md
yi-sun Jan 26, 2025
eca9059
feat: start ISA table
yi-sun Jan 26, 2025
cf05d1d
feat: add opcode mapping
yi-sun Jan 26, 2025
45dda66
feat: add phantom sub-instructions for system
yi-sun Jan 26, 2025
f2b11e7
chore: try formatting
yi-sun Jan 26, 2025
e85cbcd
chore: try formatting
yi-sun Jan 26, 2025
2fd1629
feat: add phantom instructions
yi-sun Jan 26, 2025
0c1bae2
feat: remove W generic from native BNE, BEQ
yi-sun Jan 27, 2025
46ab366
feat: constrain native extension to address space 0, 2, 4
yi-sun Jan 27, 2025
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
Prev Previous commit
Next Next commit
feat: incorporate user IO section into RV32IM extensions
yi-sun committed Jan 27, 2025
commit 3d0a6581fd803620e376cd2b15b44a6ba3a29f30
31 changes: 13 additions & 18 deletions docs/specs/ISA.md
Original file line number Diff line number Diff line change
@@ -307,6 +307,19 @@ Below `x[n:m]` denotes the bits from `n` to `m` inclusive of `x`.
| REM_RV32 | `a,b,c,1` | `[a:4]_1 = [b:4]_1 % [c:4]_1` integer remainder. Division by zero: if `i32([c:4]_1) = 0`, set `[a:4]_1 = [b:4]_1`. Overflow: if `i32([b:4]_1) = -2^31` and `i32([c:4]_1) = -1`, set `[a:4]_1 = 0`. |
| REMU_RV32 | `a,b,c,1` | `[a:4]_1 = [b:4]_1 % [c:4]_1` integer remainder. Division by zero: if `u32([c:4]_1) = 0`, set `[a:4]_1 = [b:4]_1`. |

#### User IO

In addition to opcodes which match 1-1 with the RV32IM opcodes, the following additional
opcodes interact with address spaces outside of 1 and 2 to enable verification of programs
with user input-output. We use the same notation for `r32{c}(b) := i32([b:4]_1) + sign_extend(decompose(c)[0:2])` as in [`LOADW_RV32` and
`STOREW_RV32`](#loadstore).

| Name | Operands | Description |
| ---------------- | ----------- | ----------------------------------------------------------------------------------------------------------------------------------- |
| HINT_STOREW_RV32 | `_,b,c,1,2` | `[r32{c}(b):4]_2 = next 4 bytes from hint stream`. Only valid if next 4 values in hint stream are bytes. |
| HINT_BUFFER_RV32 | `a,b,_,1,2` | `[r32{0}(b):4 * l]_2 = next 4 * l bytes from hint stream` where `l = r32{0}(a)`. Only valid if next `4 * l` values in hint stream are bytes. Very important: `l` should not be 0. |
| REVEAL_RV32 | `a,b,c,1,3` | Pseudo-instruction for `STOREW_RV32 a,b,c,1,3` writing to the user IO address space `3`. Only valid when continuations are enabled. |

#### Phantom Sub-Instructions

The RV32IM extension defines the following phantom sub-instructions.
@@ -316,24 +329,6 @@ The RV32IM extension defines the following phantom sub-instructions.
| Rv32HintInput | 0x20 | `_` | Pops a vector `hint` of field elements from the input stream and resets the hint stream to equal the vector `[(hint.len() as u32).to_le_bytes()), hint].concat()`. |
| Rv32PrintStr | 0x21 | `a,b,_` | Peeks at `[r32{0}(a)..r32{0}(a) + r32{0}(b)]_2`, tries to convert to byte array and then UTF-8 string and prints to host stdout. Prints error message if conversion fails. Does not change any VM state. |

### RV32 Intrinsics

RV32 intrinsics are custom OpenVM opcodes that are designed to be compatible with the RV32 architecture.
We continue to use \_RV32 to specify that the operand parsing is specifically targeting 32-bit RISC-V registers.

All instructions below assume that all memory cells in address spaces `1` and `2` are field elements that are in range
`[0, 2^LIMB_BITS)` where `LIMB_BITS = 8`. The instructions must all ensure that any writes will uphold this constraint.

We use the same notation for `r32{c}(b) := i32([b:4]_1) + sign_extend(decompose(c)[0:2])` as in [`LOADW_RV32` and
`STOREW_RV32`](#loadstore).

#### User IO

| Name | Operands | Description |
| ---------------- | ----------- | --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
| HINT_STOREW_RV32 | `_,b,_,1,2` | `[r32{0}(b):4]_2 = next 4 bytes from hint stream`. Only valid if next 4 values in hint stream are bytes. |
| HINT_BUFFER_RV32 | `a,b,_,1,2` | `[r32{0}(b):4 * l]_2 = next 4 * l bytes from hint stream` where `l = r32{0}(a)`. Only valid if next `4 * l` values in hint stream are bytes. Very important: `l` should not be 0. |
| REVEAL_RV32 | `a,b,c,1,3` | Pseudo-instruction for `STOREW_RV32 a,b,c,1,3` writing to the user IO address space `3`. Only valid when continuations are enabled. |

### Keccak Extension