Created
November 20, 2019 19:19
-
-
Save imeckler/1346878f77c520695d46c34761f15b4e to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
let n = something | |
let k = log2 n | |
let b (u : f_q array) (x : f_q) : f_q = | |
let x_to_pow2s = | |
let res = Array.create k x in | |
for i = 1 to k - 1 do | |
res.(i) <- square (res.(i - 1)) | |
done | |
in | |
product k (fun i -> u.(i) + 1 / u.(i) * x_to_pow2s.(i)) | |
(* Inside here we have F_q arithmetic, so we can incrementally check | |
the polynomial commitments from the pairing-based Marlin *) | |
let dlog_main | |
app_state (* F_p based (passed through) *) | |
pairing_marlin_vk (* F_q based *) | |
next_pairing_marlin_acc (* F_q based *) | |
dlog_marlin_vk (* F_p based (passed through) *) | |
g_old (* F_p based (passed through) *) | |
x_old (* F_q based *) | |
u_old (* F_q based *) | |
b_u_x_old (* F_q based *) | |
prev_dlog_marlin_acc (* F_p based *) | |
prev_deferred_fp_arithmetic (* F_p based *) | |
= | |
let prev_pairing_marlin_acc = exists Pairing_marlin_acc | |
and prev_deferred_fq_arithmetic = exists Deferred_fq_arithmetic | |
in | |
List.iter prev_deferred_fq_arithmetic ~f:(fun a -> | |
perform a); | |
(* This is kind of a special case of deferred fq arithmetic. *) | |
assert (b u_old x_old = b_u_x_old); | |
let updated_pairing_marlin_acc, deferred_fp_arithmetic = | |
let prev_marlin_proof = exists Prev_pairing_marlin_proof in | |
(* This performs the marlin verifier, does the incremental update of | |
the polynomial commitment verification but does not perform all the | |
F_p arithmetic equality checks. *) | |
Pairing_marlin.incrementally_verify_openings | |
pairing_marlin_vk | |
prev_marlin_proof | |
~public_input:[ | |
pairing_marlin_vk; (* This may need to be passed in using the hashing trick. It could be hashed together with prev_pairing_marlin_acc since they're both just passed through anyway. *) | |
prev_pairing_marlin_acc; | |
dlog_marlin_vk; | |
g_old; | |
prev_dlog_marlin_acc; | |
prev_deferred_fq_arithmetic; | |
] | |
in | |
assert (updated_pairing_marlin_macc = next_pairing_marlin_acc); | |
assert (prev_deferred_fp_arithmetic = deferred_fp_arithmetic); | |
(* Inside here we have F_p arithmetic so we can incrementally check the | |
polynomial commitments from the DLog-based marlin *) | |
let pairing_main | |
app_state | |
pairing_marlin_vk | |
prev_pairing_marlin_acc | |
dlog_marlin_vk | |
g_new | |
u_new | |
x_new | |
next_dlog_marlin_acc | |
next_deferred_fq_arithmetic | |
= | |
(* The actual computation *) | |
let prev_app_state = exists Prev_app_state in | |
let transition = exists Transition in | |
assert (transition_function prev_app_state transition = app_state); | |
let prev_dlog_marlin_acc = exists Dlog_marlin_acc | |
and prev_deferred_fp_arithmetic = exists Deferred_fp_arithmetic in | |
List.iter prev_deferred_fp_arithmetic ~f:perform; | |
let (actual_g_new, actual_u_new), deferred_fq_arithmetic = | |
let g_old, x_old, u_old, b_u_old = exists G_old in | |
let updated_dlog_marlin_acc, deferred_fq_arithmetic, polynomial_evaluation_checks = | |
let prev_dlog_marlin_proof = exists Prev_dlog_marlin_proof in | |
Dlog_marlin.incrementally_execute_protocol | |
dlog_marlin_vk | |
prev_dlog_marlin_proof | |
~public_input:[ | |
prev_app_state; | |
pairing_marlin_vk; | |
prev_pairing_marlin_acc; | |
dlog_marlin_vk; | |
g_old; | |
x_old; | |
u_old; | |
b_u_old_x; | |
prev_dlog_marlin_acc; | |
prev_deferred_fp_arithmetic; | |
] | |
in | |
let g_new_u_new = | |
batched_inner_product_argument | |
((g_old, x_old, b_u_old_x) :: polynomial_evaluation_checks) | |
in | |
g_new_u_new, deferred_fq_arithmetic | |
in | |
(* This should be sampled using the hash state at the end of | |
"Dlog_marlin.incrementally_execute_protocol" *) | |
let x_new = sample () in | |
assert (actual_g_new = g_new); | |
assert (actual_u_new = u_new); | |
assert (actual_x_new = x_new) | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment