public_data_read.pil

include "merkle_check.pil";
include "ff_gt.pil";
include "poseidon2_hash.pil";
include "constants_gen.pil";
include "precomputed.pil";

// This gadget checks reads in the public data tree. The public data tree is an indexed tree where leaves
// have slot and value. Slot is the "key" and value is the stored data. When we read from the public data tree,
// we assume that a slot that has not been written before has value zero.
// For this we perform a low leaf membership proof and:
//  - if the low leaf slot is equal to the slot, that means that slot has been written before, and we assert that
//    the low leaf value is equal to the value we are reading.
//  - if the low leaf slot is not equal to the slot, we assert that the low leaf is indeed the low leaf for the
//    requested slot, proving non existance of the slot in the tree. In that case we check value to be zero.
//
// Usage:
// sel { value, leaf_slot, public_data_tree_root }
// in public_data_read.sel { public_data_read.value, public_data_read.slot, public_data_read.root };
//
namespace public_data_read;
    pol commit sel;
    sel * (1 - sel) = 0;

    #[skippable_if]
    sel = 0;

    // Inputs to the gadget
    pol commit value;
    pol commit slot;
    pol commit root;

    // Hints
    pol commit low_leaf_slot;
    pol commit low_leaf_value;
    pol commit low_leaf_next_index;
    pol commit low_leaf_next_slot;

    pol commit low_leaf_index;

    // ========= LOW LEAF MEMBERSHIP =========
    pol commit low_leaf_hash;
    // TODO: We need this temporarily while we do not allow for aliases in the lookup tuple
    pol commit tree_height;
    sel * (tree_height - constants.PUBLIC_DATA_TREE_HEIGHT) = 0;

    #[LOW_LEAF_POSEIDON2_0]
    sel { low_leaf_slot, low_leaf_value, low_leaf_next_index, low_leaf_hash }
    in poseidon2_hash.start { poseidon2_hash.input_0, poseidon2_hash.input_1, poseidon2_hash.input_2, poseidon2_hash.output };

    #[LOW_LEAF_POSEIDON2_1]
    sel { low_leaf_next_slot, precomputed.zero, precomputed.zero, low_leaf_hash }
    in poseidon2_hash.end { poseidon2_hash.input_0, poseidon2_hash.input_1, poseidon2_hash.input_2, poseidon2_hash.output };

    #[LOW_LEAF_MEMBERSHIP]
    sel { low_leaf_hash, low_leaf_index, tree_height, root }
    in merkle_check.start { merkle_check.read_node, merkle_check.index, merkle_check.path_len, merkle_check.read_root };

    // ========= LOW LEAF VALIDATION =========
    // We commit leaf not exists instead of leaf exists since it'll be used as a selector for a lookup
    pol commit leaf_not_exists;
    leaf_not_exists * (1 - leaf_not_exists) = 0;
    pol LEAF_EXISTS = 1 - leaf_not_exists;

    pol commit slot_low_leaf_slot_diff_inv;
    pol SLOT_LOW_LEAF_SLOT_DIFF = slot - low_leaf_slot;

    //  SLOT_LOW_LEAF_SLOT_DIFF == 0 <==> LEAF_EXISTS == 1
    #[EXISTS_FLAG_CHECK]
    sel * (SLOT_LOW_LEAF_SLOT_DIFF * (LEAF_EXISTS * (1 - slot_low_leaf_slot_diff_inv) + slot_low_leaf_slot_diff_inv) - 1 + LEAF_EXISTS) = 0;

    // If the leaf doesn't exist, we need to validate that the slot is greater than the low leaf slot

    // TODO: We need this temporarily while we do not allow for aliases in the lookup tuple
    pol commit one;
    sel * (1 - one) = 0;

    #[LOW_LEAF_SLOT_VALIDATION]
    leaf_not_exists { slot, low_leaf_slot, one }
    in ff_gt.sel_gt { ff_gt.a, ff_gt.b, ff_gt.result };

    // If next slot is not zero (which would be infinity), it has to be greater than the slot.
    // We commit next_slot_is_nonzero instead of next_slot_is_zero since it'll be used as a selector for a lookup
    pol commit next_slot_is_nonzero;
    next_slot_is_nonzero * (1 - next_slot_is_nonzero) = 0;
    pol NEXT_SLOT_IS_ZERO = 1 - next_slot_is_nonzero;

    pol commit next_slot_inv;
    #[NEXT_SLOT_IS_ZERO_CHECK]
    leaf_not_exists * (low_leaf_next_slot * (NEXT_SLOT_IS_ZERO * (1 - next_slot_inv) + next_slot_inv) - 1 + NEXT_SLOT_IS_ZERO) = 0;

    #[LOW_LEAF_NEXT_SLOT_VALIDATION]
    next_slot_is_nonzero { low_leaf_next_slot, slot, one }
    in ff_gt.sel_gt { ff_gt.a, ff_gt.b, ff_gt.result };

    // ========= VALUE VALIDATION =========
    // value = LEAF_EXISTS ? low_leaf_value : 0
    #[VALUE_IS_CORRECT]
    low_leaf_value * LEAF_EXISTS - value = 0;