darkfi/proofs/mint2.psm

constant edwards_d 0x2a9318e74bfa2b48f5fd9207e6bd7fd4292d7f6d37579d2601065fd6d6343eb1
constant one 0x0000000000000000000000000000000000000000000000000000000000000001
constant zero 0x0000000000000000000000000000000000000000000000000000000000000000
constant G_VCR_u 0x6800f4fa0f001cfc7ff6826ad58004b4d1d8da41af03744e3bce3b7793664337
constant G_VCR_v 0x6d81d3a9cb45dedbe6fb2a6e1e22ab50ad46f1b0473b803b3caefab9380b6a8b
constant G_VCV_u 0x273f910d9ecc1615d8618ed1d15fef4e9472c89ac043042d36183b2cb4d7ef51
constant G_VCV_v 0x466a7e3a82f67ab1d32294fd89774ad6bc3332d0fa1ccd18a77a81f50667c8d7

{% macro square(x2, x) %}
    ########################################################
    # square({{x2}}, {{x}})
    ########################################################
    private {{x2}}
    set {{x2}} {{x}}
    mul {{x2}} {{x}}

    lc0_add {{x}}
    lc1_add {{x}}
    lc2_add {{x2}}
    enforce
{% endmacro %}

{% macro jubjub_witness(p, u, v) %}
    ########################################################
    # jubjub_witness({{p}}, {{u}}, {{v}})
    ########################################################
    # -u^2 + v^2 = 1 + du^2v^2
    {{ square(p + "_u2", u) }}
    {{ square(p + "_v2", v) }}
    private {{p}}_u2v2
    set {{p}}_u2v2 {{p + "_u2"}}
    mul {{p}}_u2v2 {{p + "_v2"}}
    # on curve check
    lc0_sub {{p + "_u2"}}
    lc0_add {{p + "_v2"}}
    lc1_add_one
    lc2_add_one
    lc2_add_coeff edwards_d {{p}}_u2v2
    enforce
{% endmacro %}

{% macro jubjub_double(p, u, v) %}
    ########################################################
    # jubjub_double({{p}}, {{u}}, {{v}})
    ########################################################

    # Compute T = (u + v) * (v - EDWARDS_A*u)
    #           = (u + v) * (u + v)
    private {{p}}_t
    set {{p}}_t {{u}}
    add {{p}}_t {{v}}
    local {{p}}_t1
    set {{p}}_t1 {{u}}
    add {{p}}_t1 {{v}}
    mul {{p}}_t {{p}}_t1

    lc0_add {{u}}
    lc0_add {{v}}
    lc1_add {{u}}
    lc1_add {{v}}
    lc2_add {{p}}_t
    enforce

    # Compute A = u * v
    private {{p}}_A
    set {{p}}_A {{u}}
    mul {{p}}_A {{v}}

    # Compute C = d*A*A
    private {{p}}_C
    load {{p}}_C edwards_d
    mul {{p}}_C {{p}}_A
    mul {{p}}_C {{p}}_A

    lc0_add_coeff edwards_d {{p}}_A
    lc1_add {{p}}_A
    lc2_add {{p}}_C
    enforce

    # Compute u3 = (2.A) / (1 + C)
    private {{p}}_u
    set {{p}}_u {{p}}_A
    add {{p}}_u {{p}}_A
    local {{p}}_u3_t1
    load {{p}}_u3_t1 one
    add {{p}}_u3_t1 {{p}}_C
    divide {{p}}_u {{p}}_u3_t1

    lc0_add_one
    lc0_add {{p}}_C
    lc1_add {{p}}_u
    lc2_add {{p}}_A
    lc2_add {{p}}_A
    enforce

    # Compute v3 = (T + (EDWARDS_A-1)*A) / (1 - C)
    #            = (T - 2.A) / (1 - C)
    private {{p}}_v
    set {{p}}_v {{p}}_t
    local {{p}}_2A
    set {{p}}_2A {{p}}_A
    add {{p}}_2A {{p}}_A
    sub {{p}}_v {{p}}_2A
    local {{p}}_v3_t1
    load {{p}}_v3_t1 one
    sub {{p}}_v3_t1 {{p}}_C
    divide {{p}}_v {{p}}_v3_t1

    lc0_add_one
    lc0_sub {{p}}_C
    lc1_add {{p}}_v
    lc2_add {{p}}_t
    lc2_sub {{p}}_A
    lc2_sub {{p}}_A
    enforce
{% endmacro %}

{% macro jubjub_assert_not_small_order(p, u, v) %}
    ########################################################
    # jubjub_assert_not_small_order({{p}}, {{u}}, {{v}})
    ########################################################

    # First doubling
    {{ jubjub_double(p + "1", u, v) }}
    # Second doubling
    {{ jubjub_double(p + "2", p + "1_u", p + "1_v") }}
    # Third doubling
    {{ jubjub_double(p + "3", p + "2_u", p + "2_v") }}

    # (0, -1) is a small order point, but won't ever appear here
    # because cofactor is 2^3, and we performed three doublings.
    # (0, 1) is the neutral element, so checking if u is nonzero
    # is sufficient to prevent small order points here.

    # Check u != 0

    # Constrain a * inv = 1, which is only valid
    # iff a has a multiplicative inverse, untrue
    # for zero.
    private {{p}}_u3_inv
    set {{p}}_u3_inv {{p}}3_u
    invert {{p}}_u3_inv

    lc0_add {{p}}3_u
    lc1_add {{p}}_u3_inv
    lc2_add_one
    enforce
{% endmacro %}

{% macro jubjub_add(P, x1, y1, x2, y2) %}
    ########################################################
    # jubjub_add({{P}}, {{x1}}, {{y1}}, {{x2}}, {{y2}})
    ########################################################

    # Compute U = (x1 + y1) * (y2 - EDWARDS_A*x2)
    #           = (x1 + y1) * (x2 + y2)
    private {{P}}_U
    set {{P}}_U {{ x1 }}
    add {{P}}_U {{ y1 }}
    local {{P}}_tmp
    set {{P}}_tmp {{ x2 }}
    add {{P}}_tmp {{ y2 }}
    mul {{P}}_U {{P}}_tmp

    # assert (x1 + y1) * (x2 + y2) == U
    lc0_add {{ x1 }}
    lc0_add {{ y1 }}
    lc1_add {{ x2 }}
    lc1_add {{ y2 }}
    lc2_add {{P}}_U
    enforce

    # Compute A = y2 * x1
    private {{P}}_A
    set {{P}}_A {{ y2 }}
    mul {{P}}_A {{ x1 }}
    # Compute B = x2 * y1
    private {{P}}_B
    set {{P}}_B {{ x2 }}
    mul {{P}}_B {{ y1 }}
    # Compute C = d*A*B
    private {{P}}_C
    load {{P}}_C edwards_d
    mul {{P}}_C {{P}}_A
    mul {{P}}_C {{P}}_B

    # assert (d * A) * (B) == C
    lc0_add_coeff edwards_d {{P}}_A
    lc1_add {{P}}_B
    lc2_add {{P}}_C
    enforce

    # Compute P.x = (A + B) / (1 + C)
    private {{P}}_u
    set {{P}}_u {{P}}_A
    add {{P}}_u {{P}}_B
    local {{P}}_u_denom
    load {{P}}_u_denom one
    add {{P}}_u_denom {{P}}_C
    divide {{P}}_u {{P}}_u_denom

    lc0_add_one
    lc0_add {{P}}_C
    lc1_add {{P}}_u
    lc2_add {{P}}_A
    lc2_add {{P}}_B
    enforce

    # Compute P.y = (U - A - B) / (1 - C)
    private {{P}}_v
    set {{P}}_v {{P}}_U
    sub {{P}}_v {{P}}_A
    sub {{P}}_v {{P}}_B
    local {{P}}_v_denom
    load {{P}}_v_denom one
    sub {{P}}_v_denom {{P}}_C
    divide {{P}}_v {{P}}_v_denom

    lc0_add_one
    lc0_sub {{P}}_C
    lc1_add {{P}}_v
    lc2_add {{P}}_U
    lc2_sub {{P}}_A
    lc2_sub {{P}}_B
    enforce
{% endmacro %}

{% macro jubjub_conditionally_select(p, u, v, condition) %}
    ########################################################
    # jubjub_conditionally_select({{p}}, {{u}}, {{v}}, {{condition}})
    ########################################################

    # Compute u' = self.u if condition, and 0 otherwise
    private {{p}}_u
    set {{p}}_u {{u}}
    mul {{p}}_u {{condition}}

    # condition * u = u'
    # if condition is 0, u' must be 0
    # if condition is 1, u' must be u
    lc0_add {{u}}
    lc1_add {{condition}}
    lc2_add {{p}}_u
    enforce

    # Compute v' = self.v if condition, and 1 otherwise
    # v' = condition * v + 1 - condition
    private {{p}}_v
    set {{p}}_v {{v}}
    mul {{p}}_v {{condition}}
    local {{p}}_one
    load {{p}}_one one
    add {{p}}_v {{p}}_one
    sub {{p}}_v {{condition}}

    # condition * v = v' - (1 - condition)
    # if condition is 0, v' must be 1
    # if condition is 1, v' must be v
    lc0_add {{v}}
    lc1_add {{condition}}
    lc2_add {{p}}_v
    lc2_sub_one
    lc2_add {{condition}}
    enforce
{% endmacro %}

{% macro jubjub_mul(p, u, v, x, n) %}
    ########################################################
    # jubjub_mul({{p}}, {{u}}, {{v}}, {{x}}, {{n}})
    ########################################################
    # Performs a scalar multiplication of this twisted Edwards
    # point by a scalar represented as a sequence of booleans
    # in little-endian bit order.
    
    {% for i in range(n) %}
        {% if i == 0 %}
            {{ jubjub_conditionally_select(
                p + "_this_base_" + i|string,
                u,
                v,
                x + "_" + i|string
            ) }}

            debug {{x + "_" + i|string}}
            debug {{p + "_this_base_" + i|string}}_u
            debug {{p + "_this_base_" + i|string}}_v
        {% else %}
            {{ jubjub_conditionally_select(
                p + "_this_base_" + i|string,
                p + "_currbase_" + i|string + "_u",
                p + "_currbase_" + i|string + "_v",
                x + "_" + i|string
            ) }}

            debug {{x + "_" + i|string}}
            debug {{p + "_this_base_" + i|string}}_u
            debug {{p + "_this_base_" + i|string}}_v
        {% endif %}

        {% if i == 0 %}
            # Do nothing on first round
        {% elif i == 1 %}
            {{ jubjub_add(
                p + "_result_2",
                p + "_this_base_1_u",
                p + "_this_base_1_v",
                p + "_this_base_0_u",
                p + "_this_base_0_v"
            ) }}

            debug {{p + "_result_" + (i + 1)|string}}_u
            debug {{p + "_result_" + (i + 1)|string}}_v
        {% elif i == (n - 1) %}
            {{ jubjub_add(
                p,
                p + "_this_base_" + i|string + "_u",
                p + "_this_base_" + i|string + "_v",
                p + "_result_" + i|string + "_u",
                p + "_result_" + i|string + "_v",
            ) }}

            debug {{p}}_u
            debug {{p}}_v
        {% else %}
            {{ jubjub_add(
                p + "_result_" + (i + 1)|string,
                p + "_this_base_" + i|string + "_u",
                p + "_this_base_" + i|string + "_v",
                p + "_result_" + i|string + "_u",
                p + "_result_" + i|string + "_v",
            ) }}

            debug {{p + "_result_" + (i + 1)|string}}_u
            debug {{p + "_result_" + (i + 1)|string}}_v
        {% endif %}

        {% if i == 0 %}
            {{ jubjub_double(
                p + "_currbase_" + (i + 1)|string,
                u,
                v
            ) }}
        {% else %}
            {{ jubjub_double(
                p + "_currbase_" + (i + 1)|string,
                p + "_currbase_" + i|string + "_u",
                p + "_currbase_" + i|string + "_v"
            ) }}
        {% endif %}
    {% endfor %}
{% endmacro %}

contract mint_contract
    param public_u
    param public_v
    {{ jubjub_witness("public", "public_u", "public_v") }}
    {{ jubjub_assert_not_small_order("not_small", "public_u", "public_v") }}

    {% for i in range(256) %}
        param vc_randomness_{{i}}

        lc0_add vc_randomness_{{i}}
        enforce
    {% endfor %}

    private g_vcr_u
    private g_vcr_v
    load g_vcr_u G_VCR_u
    load g_vcr_v G_VCR_v
    {{ jubjub_mul("rcv", "g_vcr_u", "g_vcr_v", "vc_randomness", 256) }}

    public rcvu
    set rcvu rcv_u
    lc0_add rcvu
    lc1_add_one
    lc2_add rcv_u
    enforce

    public rcvv
    set rcvv rcv_v
    lc0_add rcvv
    lc1_add_one
    lc2_add rcv_v
    enforce

    #############
    {#
        {{ jubjub_double("pub_dbl_pre", "public_u", "public_v") }}

        private condition
        load condition zero
        {{ jubjub_conditionally_select("pub_dbl", "pub_dbl_pre_u", "pub_dbl_pre_v", "condition") }}

        # Use this code for testing point doubling
        public dbl_u
        set dbl_u pub_dbl_u
        lc0_add dbl_u
        lc1_add_one
        lc2_add pub_dbl_u
        enforce
        public dbl_v
        set dbl_v pub_dbl_v
        lc0_add dbl_v
        lc1_add_one
        lc2_add pub_dbl_v
        enforce
    #}
end