-
Notifications
You must be signed in to change notification settings - Fork 164
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
* Skeleton + hint55 implementation * Refactor * Implement hint66 * Hint 57 * Appease clippy * Fix: change SECP_P_V2 instead of SECP_P * Add integration tests Also renamed: - `ASSIGN_PACK_MOD_SECP_PRIME_TO_X` -> `IS_ZERO_PACK_ED25519` - `ASSIGN_PACK_MOD_SECP_PRIME_TO_VALUE` -> `REDUCE_ED25519` - `ASSIGN_DIV_MOD_1_X_SECP_PRIME_TO_X_INV_AND_VALUE` -> `IS_ZERO_PACK_ED25519` * Update changelog * Insert SECP_P to exec_scopes, and rename functions * Add call to `test_reduce_ed25519` on reduce.cairo Co-authored-by: fmoletta <[email protected]> * Apply changes requesed by @fmoletta - fix: `test_reduce_ed25519` wasn't being called in main of reduce.cairo - don't call `add_segments` macro when using `segments` - use `check_scope` instead of manual `assert_eq`s - change `run_program_simple_with_memory_holes(..., 0)` -> `run_program_simple` * Use `scope` macro instead of manual build Also allow trailing commas in `scope` macro * Add missing `check_scope` * Allow use of `scope` macro without args * Change `assert_matches`+`Ok` for `assert`+`is_ok` * Fix: remove unused import --------- Co-authored-by: Tomás <[email protected]> Co-authored-by: Tomás <[email protected]> Co-authored-by: fmoletta <[email protected]> Co-authored-by: Pedro Fontana <[email protected]>
- Loading branch information
1 parent
2891936
commit 4bc7c54
Showing
10 changed files
with
476 additions
and
3 deletions.
There are no files selected for viewing
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
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
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
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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,89 @@ | ||
%builtins range_check | ||
|
||
from starkware.cairo.common.cairo_secp.bigint import BigInt3, UnreducedBigInt3, nondet_bigint3 | ||
|
||
const BASE = 2 ** 86; | ||
const SECP_REM = 19; | ||
|
||
func verify_zero{range_check_ptr}(val: UnreducedBigInt3) { | ||
let q = [ap]; | ||
%{ | ||
from starkware.cairo.common.cairo_secp.secp_utils import pack | ||
SECP_P = 2**255-19 | ||
to_assert = pack(ids.val, PRIME) | ||
q, r = divmod(pack(ids.val, PRIME), SECP_P) | ||
assert r == 0, f"verify_zero: Invalid input {ids.val.d0, ids.val.d1, ids.val.d2}." | ||
ids.q = q % PRIME | ||
%} | ||
let q_biased = [ap + 1]; | ||
q_biased = q + 2 ** 127, ap++; | ||
[range_check_ptr] = q_biased, ap++; | ||
// This implies that q is in the range [-2**127, 2**127). | ||
|
||
tempvar r1 = (val.d0 + q * SECP_REM) / BASE; | ||
assert [range_check_ptr + 1] = r1 + 2 ** 127; | ||
// This implies that r1 is in the range [-2**127, 2**127). | ||
// Therefore, r1 * BASE is in the range [-2**213, 2**213). | ||
// By the soundness assumption, val.d0 is in the range (-2**250, 2**250). | ||
// This implies that r1 * BASE = val.d0 + q * SECP_REM (as integers). | ||
|
||
tempvar r2 = (val.d1 + r1) / BASE; | ||
assert [range_check_ptr + 2] = r2 + 2 ** 127; | ||
// Similarly, this implies that r2 * BASE = val.d1 + r1 (as integers). | ||
// Therefore, r2 * BASE**2 = val.d1 * BASE + r1 * BASE. | ||
|
||
assert val.d2 = q * (BASE / 8) - r2; | ||
// Similarly, this implies that q * BASE / 4 = val.d2 + r2 (as integers). | ||
// Therefore, | ||
// q * BASE**3 / 4 = val.d2 * BASE**2 + r2 * BASE ** 2 = | ||
// val.d2 * BASE**2 + val.d1 * BASE + r1 * BASE = | ||
// val.d2 * BASE**2 + val.d1 * BASE + val.d0 + q * SECP_REM = | ||
// val + q * SECP_REM. | ||
// Hence, val = q * (BASE**3 / 4 - SECP_REM) = q * (2**256 - SECP_REM) = q * secp256k1_prime. | ||
|
||
let range_check_ptr = range_check_ptr + 3; | ||
return (); | ||
} | ||
|
||
// Receives an unreduced number, and returns a number that is equal to the original number mod | ||
// Ed25519 prime and in reduced form (meaning every limb is in the range [0, BASE)). | ||
// | ||
// Completeness assumption: x's limbs are in the range (-2**210.99, 2**210.99). | ||
// Soundness assumption: x's limbs are in the range (-2**249.99, 2**249.99). | ||
func reduce_ed25519{range_check_ptr}(x: UnreducedBigInt3) -> (reduced_x: BigInt3) { | ||
%{ | ||
from starkware.cairo.common.cairo_secp.secp_utils import pack | ||
SECP_P=2**255-19 | ||
value = pack(ids.x, PRIME) % SECP_P | ||
%} | ||
let (reduced_x: BigInt3) = nondet_bigint3(); | ||
|
||
verify_zero( | ||
UnreducedBigInt3(d0=x.d0 - reduced_x.d0, d1=x.d1 - reduced_x.d1, d2=x.d2 - reduced_x.d2) | ||
); | ||
return (reduced_x=reduced_x); | ||
} | ||
|
||
func test_reduce_ed25519{range_check_ptr}() { | ||
let x = UnreducedBigInt3(0, 0, 0); | ||
let (res) = reduce_ed25519(x); | ||
assert res = BigInt3(0, 0, 0); | ||
|
||
let x = UnreducedBigInt3( | ||
1113660525233188137217661511617697775365785011829423399545361443, | ||
1243997169368861650657124871657865626433458458266748922940703512, | ||
1484456708474143440067316914074363277495967516029110959982060577, | ||
); | ||
let (res) = reduce_ed25519(x); | ||
assert res = BigInt3( | ||
42193159084937489098474581, 19864776835133205750023223, 916662843592479469328893 | ||
); | ||
|
||
return (); | ||
} | ||
|
||
func main{range_check_ptr}() { | ||
test_reduce_ed25519(); | ||
return (); | ||
} |
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
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
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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,2 +1,3 @@ | ||
pub mod fq; | ||
pub mod inv_mod_p_uint512; | ||
pub mod pack; |
Oops, something went wrong.