WIP - PIL relation

barretenberg/cpp/pil/avm/avm_alu.pil

@@ -17,6 +17,7 @@ namespace avm_alu(256);
     pol commit op_div;
     pol commit op_not;
     pol commit op_eq;
+    pol commit op_cast;
     pol commit alu_sel; // Predicate to activate the copy of intermediate registers to ALU table.
 
     // Instruction tag (1: u8, 2: u16, 3: u32, 4: u64, 5: u128, 6: field) copied from Main table
@@ -58,7 +59,7 @@ namespace avm_alu(256);
     pol commit cf;
 
     // Compute predicate telling whether there is a row entry in the ALU table.
-    alu_sel = op_add + op_sub + op_mul + op_not + op_eq;
+    alu_sel = op_add + op_sub + op_mul + op_not + op_eq + op_cast;
 
     // ========= Type Constraints =============================================
     // TODO: Range constraints
@@ -163,7 +164,6 @@ namespace avm_alu(256);
     #[ALU_MULTIPLICATION_FF]
     ff_tag * op_mul * (ia * ib - ic) = 0;
 
-
     // We need 2k bits to express the product (a*b) over the integer, i.e., for type uk
     // we express the product as sum_k (u8 is an exception as we need 8-bit registers)
 
@@ -264,4 +264,13 @@ namespace avm_alu(256);
     #[ALU_OP_EQ]
     op_eq * (DIFF * (ic * (1 - op_eq_diff_inv) + op_eq_diff_inv) - 1 + ic) = 0;
 
-
+    // ========= CAST Operation Constraints ===============================
+    // We handle the input ia independently of its tag, i.e., we suppose it can take
+    // any value between 0 and p-1.
+    // We decompose the input ia in 8-bit/16-bit limbs and prove that the decomposition
+    // sums up to ia over the integers (i.e., no modulo p wrapping). To prove this,
+    // we perform a "school subtraction" (borrowing) over 128-bit limbs.
+    // The input I is written I = I_l + I_h * 2^128 and the field order P = P_l + P_h * 2^128.
+    // The school subtraction result is D = D_l + D_h * 2^128 and we prove the correctness
+    // through: P_l - I_l - CF * 2^128 == D_l AND P_h - I_h + CF == D_h
+    // where CF is a carry/borrowing bit. CF == 1 <==> P_l < I_l.

barretenberg/cpp/pil/avm/avm_main.pil

@@ -271,10 +271,10 @@ namespace avm_main(256);
 
     #[PERM_MAIN_ALU]
     alu_sel {clk, ia, ib, ic, sel_op_add, sel_op_sub,
-             sel_op_mul, sel_op_eq, sel_op_not, alu_in_tag}
+             sel_op_mul, sel_op_eq, sel_op_not, sel_op_cast, alu_in_tag}
     is
     avm_alu.alu_sel {avm_alu.clk, avm_alu.ia, avm_alu.ib, avm_alu.ic, avm_alu.op_add, avm_alu.op_sub,
-                     avm_alu.op_mul, avm_alu.op_eq, avm_alu.op_not, avm_alu.in_tag};
+                     avm_alu.op_mul, avm_alu.op_eq, avm_alu.op_not, avm_alu.op_cast, avm_alu.in_tag};
     // Based on the boolean selectors, we derive the binary op id to lookup in the table;
     // TODO: Check if having 4 columns (op_id + 3 boolean selectors) is more optimal that just using the op_id
     // but with a higher degree constraint: op_id * (op_id - 1) * (op_id - 2)

barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_alu.hpp

@@ -15,6 +15,7 @@ template <typename FF> struct Avm_aluRow {
     FF avm_alu_ic{};
     FF avm_alu_in_tag{};
     FF avm_alu_op_add{};
+    FF avm_alu_op_cast{};
     FF avm_alu_op_eq{};
     FF avm_alu_op_eq_diff_inv{};
     FF avm_alu_op_mul{};
@@ -102,7 +103,8 @@ template <typename FF_> class avm_aluImpl {
             Avm_DECLARE_VIEWS(0);
 
             auto tmp = (avm_alu_alu_sel -
-                        ((((avm_alu_op_add + avm_alu_op_sub) + avm_alu_op_mul) + avm_alu_op_not) + avm_alu_op_eq));
+                        (((((avm_alu_op_add + avm_alu_op_sub) + avm_alu_op_mul) + avm_alu_op_not) + avm_alu_op_eq) +
+                         avm_alu_op_cast));
             tmp *= scaling_factor;
             std::get<0>(evals) += tmp;
         }

barretenberg/cpp/src/barretenberg/relations/generated/avm/declare_views.hpp

@@ -13,6 +13,7 @@
     [[maybe_unused]] auto avm_alu_ic = View(new_term.avm_alu_ic);                                                      \
     [[maybe_unused]] auto avm_alu_in_tag = View(new_term.avm_alu_in_tag);                                              \
     [[maybe_unused]] auto avm_alu_op_add = View(new_term.avm_alu_op_add);                                              \
+    [[maybe_unused]] auto avm_alu_op_cast = View(new_term.avm_alu_op_cast);                                            \
     [[maybe_unused]] auto avm_alu_op_div = View(new_term.avm_alu_op_div);                                              \
     [[maybe_unused]] auto avm_alu_op_eq = View(new_term.avm_alu_op_eq);                                                \
     [[maybe_unused]] auto avm_alu_op_eq_diff_inv = View(new_term.avm_alu_op_eq_diff_inv);                              \

barretenberg/cpp/src/barretenberg/relations/generated/avm/perm_main_alu.hpp

@@ -12,7 +12,7 @@ namespace bb {
 class perm_main_alu_permutation_settings {
   public:
     // This constant defines how many columns are bundled together to form each set.
-    constexpr static size_t COLUMNS_PER_SET = 10;
+    constexpr static size_t COLUMNS_PER_SET = 11;
 
     /**
      * @brief If this method returns true on a row of values, then the inverse polynomial at this index. Otherwise the
@@ -59,6 +59,7 @@ class perm_main_alu_permutation_settings {
                                      in.avm_main_sel_op_mul,
                                      in.avm_main_sel_op_eq,
                                      in.avm_main_sel_op_not,
+                                     in.avm_main_sel_op_cast,
                                      in.avm_main_alu_in_tag,
                                      in.avm_alu_clk,
                                      in.avm_alu_ia,
@@ -69,6 +70,7 @@ class perm_main_alu_permutation_settings {
                                      in.avm_alu_op_mul,
                                      in.avm_alu_op_eq,
                                      in.avm_alu_op_not,
+                                     in.avm_alu_op_cast,
                                      in.avm_alu_in_tag);
     }
 
@@ -105,6 +107,7 @@ class perm_main_alu_permutation_settings {
                                      in.avm_main_sel_op_mul,
                                      in.avm_main_sel_op_eq,
                                      in.avm_main_sel_op_not,
+                                     in.avm_main_sel_op_cast,
                                      in.avm_main_alu_in_tag,
                                      in.avm_alu_clk,
                                      in.avm_alu_ia,
@@ -115,6 +118,7 @@ class perm_main_alu_permutation_settings {
                                      in.avm_alu_op_mul,
                                      in.avm_alu_op_eq,
                                      in.avm_alu_op_not,
+                                     in.avm_alu_op_cast,
                                      in.avm_alu_in_tag);
     }
 };

barretenberg/cpp/src/barretenberg/vm/generated/avm_circuit_builder.hpp

@@ -43,6 +43,7 @@ template <typename FF> struct AvmFullRow {
     FF avm_alu_ic{};
     FF avm_alu_in_tag{};
     FF avm_alu_op_add{};
+    FF avm_alu_op_cast{};
     FF avm_alu_op_div{};
     FF avm_alu_op_eq{};
     FF avm_alu_op_eq_diff_inv{};
@@ -205,8 +206,8 @@ class AvmCircuitBuilder {
     using Polynomial = Flavor::Polynomial;
     using ProverPolynomials = Flavor::ProverPolynomials;
 
-    static constexpr size_t num_fixed_columns = 152;
-    static constexpr size_t num_polys = 133;
+    static constexpr size_t num_fixed_columns = 162;
+    static constexpr size_t num_polys = 143;
     std::vector<Row> rows;
 
     void set_trace(std::vector<Row>&& trace) { rows = std::move(trace); }
@@ -233,6 +234,7 @@ class AvmCircuitBuilder {
             polys.avm_alu_ic[i] = rows[i].avm_alu_ic;
             polys.avm_alu_in_tag[i] = rows[i].avm_alu_in_tag;
             polys.avm_alu_op_add[i] = rows[i].avm_alu_op_add;
+            polys.avm_alu_op_cast[i] = rows[i].avm_alu_op_cast;
             polys.avm_alu_op_div[i] = rows[i].avm_alu_op_div;
             polys.avm_alu_op_eq[i] = rows[i].avm_alu_op_eq;
             polys.avm_alu_op_eq_diff_inv[i] = rows[i].avm_alu_op_eq_diff_inv;

barretenberg/cpp/src/barretenberg/vm/generated/avm_flavor.hpp

@@ -46,11 +46,11 @@ class AvmFlavor {
     using RelationSeparator = FF;
 
     static constexpr size_t NUM_PRECOMPUTED_ENTITIES = 2;
-    static constexpr size_t NUM_WITNESS_ENTITIES = 131;
+    static constexpr size_t NUM_WITNESS_ENTITIES = 141;
     static constexpr size_t NUM_WIRES = NUM_WITNESS_ENTITIES + NUM_PRECOMPUTED_ENTITIES;
     // We have two copies of the witness entities, so we subtract the number of fixed ones (they have no shift), one for
     // the unshifted and one for the shifted
-    static constexpr size_t NUM_ALL_ENTITIES = 152;
+    static constexpr size_t NUM_ALL_ENTITIES = 162;
 
     using Relations = std::tuple<Avm_vm::avm_alu<FF>,
                                  Avm_vm::avm_binary<FF>,
@@ -106,6 +106,7 @@ class AvmFlavor {
                               avm_alu_ic,
                               avm_alu_in_tag,
                               avm_alu_op_add,
+                              avm_alu_op_cast,
                               avm_alu_op_div,
                               avm_alu_op_eq,
                               avm_alu_op_eq_diff_inv,
@@ -249,6 +250,7 @@ class AvmFlavor {
                      avm_alu_ic,
                      avm_alu_in_tag,
                      avm_alu_op_add,
+                     avm_alu_op_cast,
                      avm_alu_op_div,
                      avm_alu_op_eq,
                      avm_alu_op_eq_diff_inv,
@@ -398,6 +400,7 @@ class AvmFlavor {
                               avm_alu_ic,
                               avm_alu_in_tag,
                               avm_alu_op_add,
+                              avm_alu_op_cast,
                               avm_alu_op_div,
                               avm_alu_op_eq,
                               avm_alu_op_eq_diff_inv,
@@ -562,6 +565,7 @@ class AvmFlavor {
                      avm_alu_ic,
                      avm_alu_in_tag,
                      avm_alu_op_add,
+                     avm_alu_op_cast,
                      avm_alu_op_div,
                      avm_alu_op_eq,
                      avm_alu_op_eq_diff_inv,
@@ -726,6 +730,7 @@ class AvmFlavor {
                      avm_alu_ic,
                      avm_alu_in_tag,
                      avm_alu_op_add,
+                     avm_alu_op_cast,
                      avm_alu_op_div,
                      avm_alu_op_eq,
                      avm_alu_op_eq_diff_inv,
@@ -992,6 +997,7 @@ class AvmFlavor {
             Base::avm_alu_ic = "AVM_ALU_IC";
             Base::avm_alu_in_tag = "AVM_ALU_IN_TAG";
             Base::avm_alu_op_add = "AVM_ALU_OP_ADD";
+            Base::avm_alu_op_cast = "AVM_ALU_OP_CAST";
             Base::avm_alu_op_div = "AVM_ALU_OP_DIV";
             Base::avm_alu_op_eq = "AVM_ALU_OP_EQ";
             Base::avm_alu_op_eq_diff_inv = "AVM_ALU_OP_EQ_DIFF_INV";
@@ -1151,6 +1157,7 @@ class AvmFlavor {
         Commitment avm_alu_ic;
         Commitment avm_alu_in_tag;
         Commitment avm_alu_op_add;
+        Commitment avm_alu_op_cast;
         Commitment avm_alu_op_div;
         Commitment avm_alu_op_eq;
         Commitment avm_alu_op_eq_diff_inv;
@@ -1310,6 +1317,7 @@ class AvmFlavor {
             avm_alu_ic = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_frs_read);
             avm_alu_in_tag = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_frs_read);
             avm_alu_op_add = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_frs_read);
+            avm_alu_op_cast = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_frs_read);
             avm_alu_op_div = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_frs_read);
             avm_alu_op_eq = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_frs_read);
             avm_alu_op_eq_diff_inv = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_frs_read);
@@ -1474,6 +1482,7 @@ class AvmFlavor {
             serialize_to_buffer<Commitment>(avm_alu_ic, Transcript::proof_data);
             serialize_to_buffer<Commitment>(avm_alu_in_tag, Transcript::proof_data);
             serialize_to_buffer<Commitment>(avm_alu_op_add, Transcript::proof_data);
+            serialize_to_buffer<Commitment>(avm_alu_op_cast, Transcript::proof_data);
             serialize_to_buffer<Commitment>(avm_alu_op_div, Transcript::proof_data);
             serialize_to_buffer<Commitment>(avm_alu_op_eq, Transcript::proof_data);
             serialize_to_buffer<Commitment>(avm_alu_op_eq_diff_inv, Transcript::proof_data);

barretenberg/cpp/src/barretenberg/vm/generated/avm_verifier.cpp

@@ -61,6 +61,8 @@ bool AvmVerifier::verify_proof(const HonkProof& proof)
     commitments.avm_alu_ic = transcript->template receive_from_prover<Commitment>(commitment_labels.avm_alu_ic);
     commitments.avm_alu_in_tag = transcript->template receive_from_prover<Commitment>(commitment_labels.avm_alu_in_tag);
     commitments.avm_alu_op_add = transcript->template receive_from_prover<Commitment>(commitment_labels.avm_alu_op_add);
+    commitments.avm_alu_op_cast =
+        transcript->template receive_from_prover<Commitment>(commitment_labels.avm_alu_op_cast);
     commitments.avm_alu_op_div = transcript->template receive_from_prover<Commitment>(commitment_labels.avm_alu_op_div);
     commitments.avm_alu_op_eq = transcript->template receive_from_prover<Commitment>(commitment_labels.avm_alu_op_eq);
     commitments.avm_alu_op_eq_diff_inv =