VADCOP —2

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 t: Since (9, (3, 9)) matches the pattern (_, y) => y, t will be assigned the value (3, 9).

map

defined here

Explanation

1. Generic Type Parameters: <T1, T2>

• <T1, T2>: This part defines two generic type parameters, 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[]

• T1[]: The function map takes an array of type T1 as its first parameter.
• (T1 -> T2): The second parameter is a function f that takes a single element of type T1 and returns an element of type T2.
• T2[]: The function returns an array of type T2.

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

• |arr, f|: This is the syntax for an anonymous function (or lambda). It takes two arguments:
  • 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])):
  • new(len(arr), ...): Creates a new array with the same length as arr.
  • len(arr): Returns the length of the array arr.
  • |i| f(arr[i]): This is another lambda function that is used to populate the elements of the new array:
    • 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.