Files
darkfi/proofs/mint2.psm
2021-03-17 09:31:25 +01:00

410 lines
11 KiB
Plaintext

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