Follow VADCOP —1

Instructions

an instruction consists of:

- a name
- a set of inputs (assignment registers or labels)
- a set of outputs (assignment registers)
- a set of powdr-pil constraints to activate when the instruction is called
- a set of links calling into functions/operations in submachines

```
//name of the instruction, and four assignment register as inputs
instr mload X, Y, Z, W
```

These two link (call) sub-machine

```
link => bit2.check(tmp4_col)
link => bit6.check(X_b1)
```

=> and ~> is either permutation or lookup

The pil file generated from this asm file is

let me focus on the columns generated from the first instruction

constrains:

```
main.instr_mload * (main.tmp1_col + main.Y - (main.wrap_bit * 4294967296 + main.X_b4 * 16777216 + main.X_b3 * 65536 + main.X_b2 * 256 + main.X_b1 * 4 + main.tmp4_col)) = 0;
main.instr_mstore * (main.tmp1_col - main.tmp2_col + main.Z - (main.X_b1 + main.X_b2 * 256 + main.X_b3 * 65536 + main.X_b4 * 16777216 + main.wrap_bit * 4294967296)) = 0;
```

it constraints:

\(tmp_1+Y=wrap_{bit}\cdot 2^{32}+ x_{b4}\cdot 2^{24}+x_{b3}\cdot 2^{16}+x_{b2}\cdot 2^8+x_{b1}\cdot 2^2 +tmp_4\)

\(tmp_1-tmp_2+Z=x_{b1}+x_{b2}\cdot 2^8 +x_{b3}\cdot 2^{16}+x_{b4}\cdot 2^{24}+wrap_{bit}\cdot 2^{32} \)

….

okay, let return back a bit the VADCOP

this open issue is about logup, bus, sound

let’s check how the lookup is implemented

challenge in prover is defined like this

```
// let name: type type ->
let challenge: int, int -> expr = constr |st, id| std::prelude::challenge(st, id);
```

```
let unpack_lookup_constraint: Constr -> (expr, expr[], expr, expr[]) = |lookup_constraint| match lookup_constraint {
Constr::Lookup((lhs_selector, rhs_selector), values) => (
unwrap_or_else(lhs_selector, || 1),
map(values, |(lhs, _)| lhs),
unwrap_or_else(rhs_selector, || 1),
map(values, |(_, rhs)| rhs)
),
_ => panic("Expected lookup constraint")
};
```

get to know prelude.asm, many built-in types and values.

also specified in Modules section:

“Similar to Rust, any reference that cannot be resolved is looked up once more in `std::prelude`

. This module exposes basic types and values such as `Option`

, `true`

and `false`

. This means that you can use `Option`

anywhere without prefix.”

The lookup constraint is defined as below in prelude

```
/// A lookup constraint with selectors.
Lookup((Option<expr>, Option<expr>), (expr, expr)[]),
```

so in the test file, lookup constraint is declared as

```
let lookup_constraint = Constr::Lookup(
(Option::Some(random_six), Option::Some(first_seven)),
[(a1, b1), (a2, b2), (a3, b3)]
);
```

## Match

The match syntax : match term {marching_term_1 => output1, matching_term_2 => output2 …}

example:

```
// The match statement typically uses patterns to check for certain values
// but it can also destructure and create new local variables valid inside
// the match arm.
let t = match (x, f((1, x), 2)) {
(0, _) => 0,
(1, _) => 7,
(_, y) => y,
_ => 9
};
```

**Explanation:**

**Match Statement:**- The
`match`

statement takes the tuple`(x, f((1, x), 2))`

as its input:`x`

is`9`

from the previous example.`f((1, x), 2)`

calls the function`f`

with the arguments`(1, 9)`

and`2`

. This returns the tuple`(1 + 2, 9)`

, which is`(3, 9)`

.

- The
`match`

statement then evaluates this combined tuple`(9, (3, 9))`

against the provided patterns:`(0, _) => 0`

: If the first element is`0`

, return`0`

. This does not match.`(1, _) => 7`

: If the first element is`1`

, return`7`

. This does not match.`(_, y) => y`

: If the first element can be anything (`_`

), assign the second element to`y`

and return`y`

. In this case, the second element is`(3, 9)`

, so`y`

would be`(3, 9)`

.`_ => 9`

: A catch-all pattern that returns`9`

. This will match if none of the above patterns do.

**Final Value of**Since`t`

:`(9, (3, 9))`

matches the pattern`(_, y) => y`

,`t`

will be assigned the value`(3, 9)`

.

- The

## map

defined here

Explanation

1. **Generic Type Parameters: <T1, T2>**

: This part defines two generic type parameters,`<T1, T2>`

`T1`

and`T2`

. These generics allow the`map`

function to be flexible in terms of the types it can handle.`T1`

is the type of the elements in the input array.`T2`

is the type of the elements in the output array.

2. **Function Type Signature: T1[], (T1 -> T2) -> T2[]**

: The function`T1[]`

`map`

takes an array of type`T1`

as its first parameter.: The second parameter is a function`(T1 -> T2)`

`f`

that takes a single element of type`T1`

and returns an element of type`T2`

.: The function returns an array of type`T2[]`

`T2`

.

Function Body: `|arr, f| new(len(arr), |i| f(arr[i]))`

: This is the syntax for an anonymous function (or lambda). It takes two arguments:`|arr, f|`

`arr`

: An array of type`T1`

.`f`

: A function that maps elements from type`T1`

to type`T2`

.

:`new(len(arr), |i| f(arr[i]))`

: Creates a new array with the same length as`new(len(arr), ...)`

`arr`

.: Returns the length of the array`len(arr)`

`arr`

.: This is another lambda function that is used to populate the elements of the new array:`|i| f(arr[i])`

`i`

is the index of the array.`arr[i]`

accesses the element at index`i`

in the array`arr`

.`f(arr[i])`

applies the function`f`

to the element`arr[i]`

, converting it from type`T1`

to type`T2`

.- The result of
`f(arr[i])`

is stored in the new array at index`i`

.

## Panic

defined here

Taking note in next post.