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

Tracking PR for v0.11.0 release #1472

Merged
merged 115 commits into from
Nov 5, 2024
Merged
Changes from 1 commit
Commits
Show all changes
115 commits
Select commit Hold shift + click to select a range
07134e3
chore: remove callset from `Procedure` (#1470)
plafer Aug 27, 2024
d7c8933
chore: Add warning about `no_std` environment (#1471)
plafer Aug 27, 2024
b192c61
refactor: wrap MastForest in Program and Library in Arc (#1465)
bobbinth Aug 27, 2024
6523811
`Assembler::invoke`: no longer returns an `Option`
plafer Aug 27, 2024
4c77063
`MastForestBuilder`: `ensure_node` -> `add_node`
plafer Aug 27, 2024
bc5cb74
`Library`: use `MastNodeId` as unique identifier for procedures
plafer Aug 27, 2024
7272a55
fix tests
plafer Aug 28, 2024
725eff5
add failing test
plafer Aug 28, 2024
62b4c52
use `MastNodeId` to identify procedures in ModuleGraph
plafer Aug 28, 2024
72a7093
ProcedureInfo: store `body_node_id`
plafer Aug 28, 2024
30d2933
`ResolvedProcedure`: store body_id when present
plafer Aug 28, 2024
c678944
create a new root node on exec
plafer Aug 28, 2024
a352fa2
Revert "ProcedureInfo: store `body_node_id`"
plafer Aug 28, 2024
5ae4fd5
fix build after `ProcedureInfo` revert
plafer Aug 28, 2024
de51e2c
Remove `ResolvedProcedure::BodyNodeId`
plafer Aug 28, 2024
03471eb
`Assembler::resolve_target` returns `Either<MastNodeId, RpoDigest>`
plafer Aug 28, 2024
bc045b6
fix failing test
plafer Aug 28, 2024
67a061a
fmt
plafer Aug 28, 2024
a3c5d8c
add back map digest -> GID to mast forest builder
plafer Aug 28, 2024
b45d459
`MastForestBuilder`: change all `ensure_*` to `add_*`
plafer Aug 28, 2024
961d6f6
fix regression
plafer Aug 28, 2024
a4cb422
fix failing test
plafer Aug 29, 2024
0665cf5
changelog
plafer Aug 29, 2024
ef307c2
docs
plafer Aug 29, 2024
cccf018
docs
plafer Aug 29, 2024
883356a
add test `ensure_unique_node_ids_for_identical_procedures`
plafer Aug 29, 2024
ecec03b
cleanup `MastForestBuilder`
plafer Aug 29, 2024
aa04649
remove `ensure_unique_node_ids_for_identical_procedures` test
plafer Aug 29, 2024
72a482b
`MastForestBuilder::eq_hash()`
plafer Aug 29, 2024
e18c4e7
`MastForestBuilder`: digest -> mast_root
plafer Aug 29, 2024
4a46d32
`MastForestBuilder`: don't duplicate equal nodes
plafer Aug 29, 2024
d959dd6
revert changes to tests
plafer Aug 29, 2024
187db6b
invoke: don't create new node needlessly
plafer Aug 29, 2024
53003b5
fix test
plafer Aug 29, 2024
126931e
fix docs
plafer Aug 29, 2024
45539ed
fmt
plafer Aug 29, 2024
ded33b4
cleanup `Assembler::invoke`
plafer Aug 29, 2024
c5e6b8b
remove stale TODOs
plafer Aug 29, 2024
485cbc8
fix doc tests
plafer Aug 29, 2024
191404a
fix no_std
plafer Aug 29, 2024
5b3285e
`TestContext`: don't use debug mode by default
plafer Aug 30, 2024
f141c76
fix asmop hash
plafer Aug 30, 2024
8dd1662
Remove redundant comments
plafer Sep 3, 2024
ca2d6d1
revert comment change
plafer Sep 3, 2024
1b619e6
fix docstring
plafer Sep 3, 2024
a30a9c7
`Library::new()`: check that every procedures are indeed exports
plafer Sep 3, 2024
3b280f1
rename `procedure_root_digest`
plafer Sep 3, 2024
41f45d4
fix docs
plafer Sep 3, 2024
ed09c6c
refactor `Assembler::resolve_target()`
plafer Sep 3, 2024
2125923
split `Assembler::get_proc_root_id_from_mast_root`
plafer Sep 3, 2024
d294d20
`Assembler::resolve_target` docstring
plafer Sep 3, 2024
43185ec
fmt
plafer Sep 3, 2024
4c139bb
`invoke`: document
plafer Sep 3, 2024
dd72f68
fmt
plafer Sep 3, 2024
72b9fe5
add `unwrap()` comment
plafer Sep 3, 2024
8243fa2
fmt
plafer Sep 3, 2024
4eeeb03
adjust `Assembler::invoke()` comment
plafer Sep 3, 2024
2ffd050
fix `Assembler::ensure_valid_procedure_mast_root`
plafer Sep 3, 2024
9b74a8b
cleanup proc alias
plafer Sep 3, 2024
245022e
fmt
plafer Sep 3, 2024
f7d179e
Merge pull request #1473 from 0xPolygonMiden/plafer-mast-forest-build…
bitwalker Sep 4, 2024
b4e84a5
fix(assembly): properly indent first op in nested blocks
bitwalker Sep 5, 2024
1b4609e
Merge pull request #1481 from 0xPolygonMiden/bitwalker/masm-pretty-pr…
bitwalker Sep 5, 2024
0ce2fe5
feat: add no_std once primitive for stdlib deserialization (#1463)
sergerad Sep 6, 2024
2c46076
feat: improve handling of u32 operations (#1480)
bitwalker Sep 7, 2024
4ba0c53
Plafer 1122 fix decorators (#1466)
plafer Sep 11, 2024
492ce81
Simplify `batch_ops()` (#1492)
plafer Sep 12, 2024
19b5643
Merge branch 'main' into next
bobbinth Sep 13, 2024
dcde6d1
chore: fix lint
bobbinth Sep 13, 2024
f06923b
Fix operation batch flags constraints (#1495)
plafer Sep 17, 2024
9a1c34f
feat: introduce `Emit` instruction
plafer Sep 13, 2024
0b1c2f6
feat: remove `Decorator::Event`
plafer Sep 13, 2024
354052b
docs: fix docs after adding emit instruction
plafer Sep 17, 2024
0e2d4c4
fix: move push instruction to degree 5 flags
plafer Sep 18, 2024
080597b
Merge pull request #1496 from 0xPolygonMiden/plafer-1457-emit-instr
plafer Sep 18, 2024
097f76d
Documentation fixes (#1506)
PhilippGackstatter Sep 23, 2024
8e9fe06
fix: fix block hash table construction and docs (#1509)
plafer Sep 24, 2024
c6e2bc8
feat: enable specifying debug mode via cli option (#1502)
yasonk Sep 24, 2024
8762dae
feat: implement procedure annotation syntax
bitwalker Sep 23, 2024
7ee5170
fix: block stack table (#1511)
plafer Sep 25, 2024
be14f5b
fix: make chiplets vtable only use current row
plafer Sep 26, 2024
6f60f74
Merge pull request #1514 from 0xPolygonMiden/plafer-1389-fix-chiplets…
plafer Sep 26, 2024
f2b9161
Merge pull request #1510 from 0xPolygonMiden/bitwalker/annotations
bitwalker Sep 27, 2024
5085999
fix: bug in chiplet bus (#1516)
Al-Kindi-0 Oct 1, 2024
b2c5215
refactor: restrict the number of stack inputs and outputs to 16 (#1456)
Fumuran Oct 3, 2024
a898596
fix: fix block stack table dealing of RESPAN
plafer Oct 2, 2024
8d06221
Merge pull request #1512 from 0xPolygonMiden/plafer-fix-block-stack-t…
plafer Oct 3, 2024
b648a8a
chore: simplify requests hasher (#1524)
Al-Kindi-0 Oct 4, 2024
5dc5c2e
chore: fix lifetime lints
bobbinth Oct 4, 2024
f92a463
fix: simplify chiplets bus hasher chiplet (#1525)
plafer Oct 7, 2024
b2294a1
Update the stack documentation (#1530)
Fumuran Oct 17, 2024
2a97d8d
fix: `Program` deserialization (#1543)
Fumuran Oct 22, 2024
25f9382
docs: document how call and syscall work
plafer Oct 16, 2024
8029102
Merge pull request #1536 from 0xPolygonMiden/plafer-483-docs
plafer Oct 23, 2024
62a113e
chore: disable chiplets aux columns check (#1546)
plafer Oct 23, 2024
ae34c56
refactor: migrate to new padding rule (#1343)
Al-Kindi-0 Oct 24, 2024
dc41735
chore: remove dependabot, add issue templates
bobbinth Oct 28, 2024
9f9cc63
feat: implement `MastForest` merging (#1534)
PhilippGackstatter Oct 28, 2024
db71e28
Rename `EqHash` to `MastNodeFingerprint` (#1539)
PhilippGackstatter Oct 29, 2024
12dd5e5
fix: blake example (#1553)
Al-Kindi-0 Oct 29, 2024
fc46c04
fix: fix kernel ROM multiset check
plafer Oct 30, 2024
34ea043
Merge pull request #1556 from 0xPolygonMiden/plafer-1545-fix-kernel-rom
plafer Oct 30, 2024
6bbee60
feat: `DYN` takes a memory address instead of digest on stack
plafer Oct 15, 2024
550668c
feat: add dyncall operation
plafer Oct 18, 2024
7f469c4
docs: update docs for dyn and dyncall
plafer Oct 23, 2024
a30bc62
fix: block stack table construction
plafer Oct 30, 2024
766292d
Merge pull request #1557 from 0xPolygonMiden/plafer-fix-block-stack-t…
plafer Oct 31, 2024
2b96b85
Merge pull request #1535 from 0xPolygonMiden/plafer-1091-dyn-op-rework
plafer Nov 1, 2024
f1c0553
Permit child `MastNodeId`s to exceed the `MastNodeId`s of their paren…
PhilippGackstatter Nov 1, 2024
1ea1e1e
chore: migrate to winterfell v0.10 (#1533)
Al-Kindi-0 Nov 3, 2024
a82a174
feat: make prover conditionally asynchronous (#1563)
bobbinth Nov 3, 2024
ce26595
docs: fix typos (#1500)
cratiu222 Nov 4, 2024
60a5f37
chore: add the string that failed validation to `IdentError::InvalidC…
greenhat Nov 4, 2024
e3fa9ec
fix: on Library deserialization, use unchecked constructor for proced…
greenhat Nov 4, 2024
0a9344c
chore: update crate versions to v0.11.0
bobbinth Nov 5, 2024
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
docs: fix docs after adding emit instruction
plafer committed Sep 18, 2024
commit 354052bab8eb081feb590962aa032b2dd7a3320e
26 changes: 13 additions & 13 deletions docs/src/design/decoder/constraints.md
Original file line number Diff line number Diff line change
@@ -422,18 +422,18 @@ Inside a *span* block, group count can either stay the same or decrease by one:
sp \cdot \Delta gc \cdot (\Delta gc - 1) = 0 \text{ | degree} = 3
$$

When group count is decremented inside a *span* block, either $h_0$ must be $0$ (we consumed all operations in a group) or we must be executing `PUSH` operation:
When group count is decremented inside a *span* block, either $h_0$ must be $0$ (we consumed all operations in a group) or we must be executing an operation with an immediate value:

> $$
sp \cdot \Delta gc \cdot (1 - f_{push})\cdot h_0 = 0 \text{ | degree} = 7
sp \cdot \Delta gc \cdot (1 - f_{imm})\cdot h_0 = 0 \text{ | degree} = 8
$$

Notice that the above constraint does not preclude $f_{push} = 1$ and $h_0 = 0$ from being true at the same time. If this happens, op group decoding constraints (described [here](#op-group-decoding-constraints)) will force that the operation following the `PUSH` operation is a `NOOP`.
Notice that the above constraint does not preclude $f_{imm} = 1$ and $h_0 = 0$ from being true at the same time. If this happens, op group decoding constraints (described [here](#op-group-decoding-constraints)) will force that the operation following the operation with an immediate value is a `NOOP`.

When executing a `SPAN`, a `RESPAN`, or a `PUSH` operation, group count must be decremented by $1$:
When executing a `SPAN`, a `RESPAN`, or an operation with an immediate value, group count must be decremented by $1$:

> $$
(f_{span} + f_{respan} + f_{push}) \cdot (\Delta gc - 1) = 0 \text{ | degree} = 6
(f_{span} + f_{respan} + f_{imm}) \cdot (\Delta gc - 1) = 0 \text{ | degree} = 6
$$

If the next operation is either an `END` or a `RESPAN`, group count must remain the same:
@@ -467,17 +467,17 @@ op = \sum_{i=0}^6 (b_i \cdot 2^i) \\
f_{sgc} = sp \cdot sp' \cdot (1 - \Delta gc)
$$

$op$ is just an opcode value implied by the values in `op_bits` registers. $f_{sgc}$ is a flag which is set to $1$ when the group count within a *span* block does not change. We multiply it by $sp'$ to make sure the flag is $0$ when we are about to end decoding of an operation batch. Note that $f_{sgc}$ flag is mutually exclusive with $f_{span}$, $f_{respan}$, and $f_{push}$ flags as these three operations decrement the group count.
$op$ is just an opcode value implied by the values in `op_bits` registers. $f_{sgc}$ is a flag which is set to $1$ when the group count within a *span* block does not change. We multiply it by $sp'$ to make sure the flag is $0$ when we are about to end decoding of an operation batch. Note that $f_{sgc}$ flag is mutually exclusive with $f_{span}$, $f_{respan}$, and $f_{imm}$ flags as these three operations decrement the group count.

Using these variables, we can describe operation group decoding constraints as follows:

When a `SPAN`, a `RESPAN`, or a `PUSH` operation is executed or when the group count does not change, the value in $h_0$ should be decremented by the value of the opcode in the next row.
When a `SPAN`, a `RESPAN`, or an operation with an immediate value is executed or when the group count does not change, the value in $h_0$ should be decremented by the value of the opcode in the next row.

> $$
(f_{span} + f_{respan} + f_{push} + f_{sgc}) \cdot (h_0 - h_0' \cdot 2^7 - op') = 0 \text{ | degree} = 6
(f_{span} + f_{respan} + f_{imm} + f_{sgc}) \cdot (h_0 - h_0' \cdot 2^7 - op') = 0 \text{ | degree} = 6
$$

Notice that when the group count does change, and we are not executing $f_{span}$, $f_{respan}$, or $f_{push}$ operations, no constraints are placed against $h_0$, and thus, the prover can populate this register non-deterministically.
Notice that when the group count does change, and we are not executing $f_{span}$, $f_{respan}$, or $f_{imm}$ operations, no constraints are placed against $h_0$, and thus, the prover can populate this register non-deterministically.

When we are in a *span* block and the next operation is `END` or `RESPAN`, the current value in $h_0$ column must be $0$.

@@ -491,11 +491,11 @@ The `op_index` column (denoted as $ox$) tracks index of an operation within its
To simplify the description of the constraints, we will define the following variables:

$$
ng = \Delta gc - f_{push} \\
ng = \Delta gc - f_{imm} \\
\Delta ox = ox' - ox
$$

The value of $ng$ is set to $1$ when we are about to start executing a new operation group (i.e., group count is decremented but we did not execute a `PUSH` operation). Using these variables, we can describe the constraints against the $ox$ column as follows.
The value of $ng$ is set to $1$ when we are about to start executing a new operation group (i.e., group count is decremented but we did not execute an operation with an immediate value). Using these variables, we can describe the constraints against the $ox$ column as follows.

When executing `SPAN` or `RESPAN` operations the next value of `op_index` must be set to $0$:

@@ -590,10 +590,10 @@ Where $i \in [1, 8)$. Thus, $v_1$ defines row value for group in $h_1$, $v_2$ de
We compute the value of the row to be removed from the op group table as follows:

$$
u = \alpha_0 + \alpha_1 \cdot a + \alpha_2 \cdot gc + \alpha_3 \cdot ((h_0' \cdot 2^7 + op') \cdot (1 - f_{push}) + s_0' \cdot f_{push}) \text{ | degree} = 5
u = \alpha_0 + \alpha_1 \cdot a + \alpha_2 \cdot gc + \alpha_3 \cdot ((h_0' \cdot 2^7 + op') \cdot (1 - f_{imm}) + s_0' \cdot f_{push} + h_2 \cdot f_{emit}) \text{ | degree} = 6
$$

In the above, the value of the group is computed as $(h_0' \cdot 2^7 + op') \cdot (1 - f_{push}) + s_0' \cdot f_{push}$. This basically says that when we execute a `PUSH` operation we need to remove the immediate value from the table. This value is at the top of the stack (column $s_0$) in the next row. However, when we are not executing a `PUSH` operation, the value to be removed is an op group value which is a combination of values in $h_0$ and `op_bits` columns (also in the next row). Note also that value for batch address comes from the current value in the block address column ($a$), and the group position comes from the current value of the group count column ($gc$).
In the above, the value of the group is computed as $(h_0' \cdot 2^7 + op') \cdot (1 - f_{push}) + s_0' \cdot f_{push} + h_2 \cdot f_{emit}$. This basically says that when we execute a `PUSH` or `EMIT` operation we need to remove the immediate value from the table. For `PUSH`, this value is at the top of the stack (column $s_0$) in the next row; for `EMIT`, it is found in $h_2$. However, when we are executing neither a `PUSH` nor `EMIT` operation, the value to be removed is an op group value which is a combination of values in $h_0$ and `op_bits` columns (also in the next row). Note also that value for batch address comes from the current value in the block address column ($a$), and the group position comes from the current value of the group count column ($gc$).

We also define a flag which is set to $1$ when a group needs to be removed from the op group table.

10 changes: 10 additions & 0 deletions docs/src/design/stack/op_constraints.md
Original file line number Diff line number Diff line change
@@ -294,3 +294,13 @@ $$
$$
f_{ctrl} = f_{span,join,split,loop} + f_{end,repeat,respan,halt} + f_{dyn} + f_{call} + f_{syscall} \text{ | degree} = 5
$$

### Immediate value flag

The immediate value flag $f_{imm}$ is set to 1 when an operation has an immediate value, and 0 otherwise:

$$
f_{imm} = f_{push} + f_{emit} \text{ | degree} = 5
$$

Note that the `ASSERT`, `MPVERIFY` and other operations have immediate values too. However, these immediate values are not included in the MAST digest, and hence are not considered for the $f_{imm}$ flag.