Skip to content

Modify comments in the security proofs #5588

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
IlyasRidhuan merged 1 commit into from
Apr 5, 2024
Merged

Modify comments in the security proofs #5588

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
70 changes: 36 additions & 34 deletions barretenberg/cpp/pil/avm/avm_alu.pil
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -357,62 +357,64 @@ namespace avm_alu(256);

// When IS_GT = 1, we enforce the condition that a > b and thus a - b - 1 does not underflow.
// When IS_GT = 0, we enforce the condition that a <= b and thus b - a does not underflow.
// ========= Analysing res_lo and res_hi scenarios for x <= y ===============================
// (1) An honest prover claims that LTE(x,y,1). Therefore ia = x, ib = y and ic = 1.
// ========= Analysing res_lo and res_hi scenarios for LTE =================================
// (1) Assume a proof satisfies the constraints for LTE(x,y,1), i.e., x <= y
// Therefore ia = x, ib = y and ic = 1.
// (a) We do not swap the operands, so a = x and b = y,
// (b) IS_GT = 1 - ic = 0
// (c) res_lo = B_SUB_A_LO and res_hi = B_SUB_A_HI
// (d) res_lo = y_lo - x_lo + borrow * 2**128 and res_hi = y_hi - x_hi - borrow.
// (e) the only valid input here to ensure no underflow is
// (i) x == y && borrow = 0 or,
// (ii) x < y where x_lo < y_lo && x_hi <= y_hi && borrow = 0 or
// (iii) x < y where x_lo > y_lo && x_hi < y_hi && borrow = 1
// (e) Due to 128-bit range checks on res_lo, res_hi, y_lo, x_lo, y_hi, y_lo, we
// have the guarantee that res_lo >= 0 && res_hi >= 0. Furthermore, borrow is
// boolean and so we have two cases to consider:
// (i) borrow == 0 ==> y_lo >= x_lo && y_hi >= x_hi
// (ii) borrow == 1 ==> y_hi >= x_hi + 1 ==> y_hi > x_hi
// This concludes the proof as for both cases, we must have: y >= x
//
// (2) A malicious prover claims that LTE(x,y,0), i.e. y > x. Therefore ia = x, ib = y and ic = 0.
// (2) Assume a proof satisfies the constraints for LTE(x,y,0), i.e. x > y.
Therefore ia = x, ib = y and ic = 0.
// (a) We do not swap the operands, so a = x and b = y,
// (b) IS_GT = 1 - ic = 1
// (c) res_lo = A_SUB_B_LO and res_hi = A_SUB_B_HI
// (d) res_lo = x_lo - y_lo - 1 + borrow * 2**128 and res_hi = x_hi - y_hi - borrow.
// (e) Given that, in reality, x <= y. The following underflows happen
// (i) x == y && borrow = 0, res_lo = -1 and underflows.
// (ii) x == y && borrow = 1, res_hi = -1 and underflows.
// (iii) x < y where x_lo < y_lo && x_hi == y_hi && borrow = 0, res_lo < 0 and underflows
// (iv) x < y where x_lo < y_lo && x_hi == y_hi && borrow = 1, res_hi = -1 and underflows
// (v) x < y where x_lo < y_lo && x_hi < y_hi && borrow = 0, res_lo & res_hi < 0 both underflows
// (vi) x < y where x_lo < y_lo && x_hi < y_hi && borrow = 1, res_hi < 0 and underflows
// (vii) x < y where x_lo == y_lo && x_hi < y_hi && borrow = 0, res_lo = -1 && res_hi < 0 both underflows
// (viii) x < y where x_lo == y_lo && x_hi < y_hi && borrow = 1, res_hi < 0 and underflows
// (ix) x < y where x_lo > y_lo && x_hi < y_hi && borrow = 0, res_hi < 0 and underflows
// (x) x < y where x_lo > y_lo && x_hi < y_hi && borrow = 1, res_hi < 0 and underflows


// ========= Analysing res_lo and res_hi scenarios for x < y ===============================
// (1) An honest prover claims that LT(x,y,1). Therefore ia = x, ib = y and ic = 1.
// (e) Due to 128-bit range checks on res_lo, res_hi, y_lo, x_lo, y_hi, y_lo, we
// have the guarantee that res_lo >= 0 && res_hi >= 0. Furthermore, borrow is
// boolean and so we have two cases to consider:
// (i) borrow == 0 ==> x_lo > y_lo && x_hi >= y_hi
// (ii) borrow == 1 ==> x_hi > y_hi
// This concludes the proof as for both cases, we must have: x > y
//

// ========= Analysing res_lo and res_hi scenarios for LT ==================================
// (1) Assume a proof satisfies the constraints for LT(x,y,1), i.e. x < y.
Therefore ia = x, ib = y and ic = 1.
// (a) We DO swap the operands, so a = y and b = x,
// (b) IS_GT = ic = 1
// (c) res_lo = A_SUB_B_LO and res_hi = A_SUB_B_HI, **remember we have swapped inputs**
// (d) res_lo = y_lo - x_lo - 1 + borrow * 2**128 and res_hi = y_hi - x_hi - borrow.
// (e) the only valid input here to ensure no underflow is
// (i) x < y where x_lo < y_lo && x_hi <= y_hi && borrow = 0 or
// (ii) x < y where x_lo >= y_lo && x_hi < y_hi && borrow = 1
// (e) Due to 128-bit range checks on res_lo, res_hi, y_lo, x_lo, y_hi, y_lo, we
// have the guarantee that res_lo >= 0 && res_hi >= 0. Furthermore, borrow is
// boolean and so we have two cases to consider:
// (i) borrow == 0 ==> y_lo > x_lo && y_hi >= x_hi
// (ii) borrow == 1 ==> y_hi > x_hi
// This concludes the proof as for both cases, we must have: x < y
//
// (2) A malicious prover claims that LT(x,y,0), i.e. !(x < y) -> (x >= y). Therefore ia = x, ib = y and ic = 0.
// (2) Assume a proof satisfies the constraint for LT(x,y,0), i.e. x >= y.
Therefore ia = x, ib = y and ic = 0.
// (a) We DO swap the operands, so a = y and b = x,
// (b) IS_GT = ic = 0
// (c) res_lo = B_SUB_A_LO and res_hi = B_SUB_A_HI, **remember we have swapped inputs**
// (d) res_lo = x_lo - y_lo + borrow * 2**128 and res_hi = x_hi - y_hi - borrow.
// (e) Given that, in reality, x < y. The following underflows happen
// (i) x < y where x_lo < y_lo && x_hi == y_hi && borrow = 0, res_lo < 0 and underflows
// (ii) x < y where x_lo < y_lo && x_hi == y_hi && borrow = 1, res_hi = -1 and underflows
// (iii) x < y where x_lo < y_lo && x_hi < y_hi && borrow = 0, res_lo && res_hi < 0 and underflows
// (iv) x < y where x_lo < y_lo && x_hi < y_hi && borrow = 1, res_hi < 0 and underflows
// (v) x < y where x_lo > y_lo && x_hi < y_hi && borrow = 0, res_hi < 0 and underflows
// (vi) x < y where x_lo > y_lo && x_hi < y_hi && borrow = 1, res_lo overflows && res_hi < 0 and underflows
// (e) Due to 128-bit range checks on res_lo, res_hi, y_lo, x_lo, y_hi, y_lo, we
// have the guarantee that res_lo >= 0 && res_hi >= 0. Furthermore, borrow is
// boolean and so we have two cases to consider:
// (i) borrow == 0 ==> x_lo >= y_lo && x_hi >= y_hi
// (ii) borrow == 1 ==> x_hi > y_hi
// This concludes the proof as for both cases, we must have: x >= y

res_lo = (A_SUB_B_LO * IS_GT + B_SUB_A_LO * (1 - IS_GT)) * cmp_sel;
res_hi = (A_SUB_B_HI * IS_GT + B_SUB_A_HI * (1 - IS_GT)) * cmp_sel;


// ========= RANGE OPERATIONS ===============================
// TODO: 8-bit and 16-bit range checks for the respective registers have not yet been implemented.

Expand Down