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);
  • Match
  • map
  • Panic

    • Match

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

    example:

    <span class="line"><span style="color: #616E88">// The match statement typically uses patterns to check for certain values</span></span>
<span class="line"><span style="color: #616E88">// but it can also destructure and create new local variables valid inside</span></span>
<span class="line"><span style="color: #616E88">// the match arm.</span></span>
<span class="line"><span style="color: #81A1C1">let</span><span style="color: #D8DEE9FF"> </span><span style="color: #D8DEE9">t</span><span style="color: #D8DEE9FF"> </span><span style="color: #81A1C1">=</span><span style="color: #D8DEE9FF"> </span><span style="color: #88C0D0">match</span><span style="color: #D8DEE9FF"> (</span><span style="color: #D8DEE9">x</span><span style="color: #ECEFF4">,</span><span style="color: #D8DEE9FF"> </span><span style="color: #88C0D0">f</span><span style="color: #D8DEE9FF">((</span><span style="color: #B48EAD">1</span><span style="color: #ECEFF4">,</span><span style="color: #D8DEE9FF"> </span><span style="color: #D8DEE9">x</span><span style="color: #D8DEE9FF">)</span><span style="color: #ECEFF4">,</span><span style="color: #D8DEE9FF"> </span><span style="color: #B48EAD">2</span><span style="color: #D8DEE9FF">)) </span><span style="color: #ECEFF4">{</span></span>
<span class="line"><span style="color: #D8DEE9FF">    (</span><span style="color: #B48EAD">0</span><span style="color: #ECEFF4">,</span><span style="color: #D8DEE9FF"> _) => </span><span style="color: #B48EAD">0</span><span style="color: #ECEFF4">,</span></span>
<span class="line"><span style="color: #D8DEE9FF">    (</span><span style="color: #B48EAD">1</span><span style="color: #ECEFF4">,</span><span style="color: #D8DEE9FF"> _) => </span><span style="color: #B48EAD">7</span><span style="color: #ECEFF4">,</span></span>
<span class="line"><span style="color: #D8DEE9FF">    (</span><span style="color: #D8DEE9">_</span><span style="color: #ECEFF4">,</span><span style="color: #D8DEE9FF"> y) => </span><span style="color: #D8DEE9">y</span><span style="color: #ECEFF4">,</span></span>
<span class="line"><span style="color: #D8DEE9FF">    </span><span style="color: #D8DEE9">_</span><span style="color: #D8DEE9FF"> </span><span style="color: #81A1C1">=></span><span style="color: #D8DEE9FF"> </span><span style="color: #B48EAD">9</span></span>
<span class="line"><span style="color: #ECEFF4">}</span><span style="color: #81A1C1">;</span></span>

    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 , return . 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.

    Leave a Reply

    Your email address will not be published. Required fields are marked *