Skip to content

Commit

Permalink
Updated extract-all.sh script
Browse files Browse the repository at this point in the history
  • Loading branch information
@cryptojedi
cryptojedi committed Aug 7, 2024
1 parent df1f7c5 commit 0534bc5
Show file tree
Hide file tree
Showing 6 changed files with 108 additions and 130 deletions.
11 changes: 11 additions & 0 deletions scripts/extract-all.sh
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
#!/usr/bin/env bash

SCRIPTDIR=$( cd -- "$( dirname -- "${BASH_SOURCE[0]}" )" &> /dev/null && pwd )
LIBJADE_ROOT="$SCRIPTDIR/.."

for SUBMODULE in "$LIBJADE_ROOT"/submodules/formosa-*;do
EXTRACT="$SUBMODULE/extract-libjade.sh"
for IMPLEMENTATION in $($EXTRACT --list-implementations); do
$EXTRACT --gen-implementation "$IMPLEMENTATION" "$LIBJADE_ROOT/src/$IMPLEMENTATION"
done
done
58 changes: 23 additions & 35 deletions src/crypto_scalarmult/curve25519/amd64/mulx/scalarmult.jazz
View file
Original file line number Diff line number Diff line change
@@ -1,24 +1,3 @@
//BOR#from formosa25519 require "crypto_scalarmult/curve25519/amd64/common/load_store4.jinc"#formosa-25519/src/crypto_scalarmult/curve25519/amd64/common/load_store4.jinc
inline fn __load4(reg u64 p) -> reg u64[4]
{
inline int i;
reg u64[4] a;

for i=0 to 4
{ a[i] = [p + 8*i]; }

return a;
}

inline fn __store4(reg u64 p, reg u64[4] a)
{
inline int i;

for i=0 to 4
{ [p + 8*i] = a[i]; }
}

//EOR#
//BOR#require "curve25519.jinc"#formosa-25519/src/crypto_scalarmult/curve25519/amd64/mulx/curve25519.jinc
//BOR#from formosa25519 require "crypto_scalarmult/curve25519/amd64/common/bit.jinc"#formosa-25519/src/crypto_scalarmult/curve25519/amd64/common/bit.jinc
inline fn __ith_bit(stack u8[32] k, reg u64 ctr) -> reg u64
Expand Down Expand Up @@ -1247,42 +1226,51 @@ inline fn __curve25519_mulx_base(reg u64[4] _k) -> reg u64[4]

//EOR#

export fn jade_scalarmult_curve25519_amd64_mulx(#spill_to_mmx reg u64 qp np pp) -> reg u64
export fn jade_scalarmult_curve25519_amd64_mulx(
#spill_to_mmx reg ptr u64[4] qp,
reg ptr u64[4] np,
reg ptr u64[4] pp)
->
reg ptr u64[4],
reg u64
{
reg u64 r;
reg u64[4] q n p;

_ = #init_msf();
() = #spill(qp);

() = #spill(qp);
n = __load4(np);
p = __load4(pp);

n = #copy(np);
p = #copy(pp);
q = __curve25519_mulx(n, p);

() = #unspill(qp);
__store4(qp, q);
() = #unspill(qp);
qp = #copy(q);

?{}, r = #set0();
return r;
return qp, r;
}

export fn jade_scalarmult_curve25519_amd64_mulx_base(#spill_to_mmx reg u64 qp np) -> reg u64
export fn jade_scalarmult_curve25519_amd64_mulx_base(
#spill_to_mmx reg ptr u64[4] qp,
reg ptr u64[4] np)
->
reg ptr u64[4],
reg u64
{
reg u64 r;
reg u64[4] q n;

_ = #init_msf();

() = #spill(qp);
n = __load4(np);
() = #spill(qp);
n = #copy(np);

q = __curve25519_mulx_base(n);

() = #unspill(qp);
__store4(qp, q);
qp = #copy(q);

?{}, r = #set0();
return r;
return qp, r;
}

107 changes: 49 additions & 58 deletions src/crypto_scalarmult/curve25519/amd64/ref4/scalarmult.jazz
View file
Original file line number Diff line number Diff line change
@@ -1,24 +1,3 @@
//BOR#from formosa25519 require "crypto_scalarmult/curve25519/amd64/common/load_store4.jinc"#formosa-25519/src/crypto_scalarmult/curve25519/amd64/common/load_store4.jinc
inline fn __load4(reg u64 p) -> reg u64[4]
{
inline int i;
reg u64[4] a;

for i=0 to 4
{ a[i] = [p + 8*i]; }

return a;
}

inline fn __store4(reg u64 p, reg u64[4] a)
{
inline int i;

for i=0 to 4
{ [p + 8*i] = a[i]; }
}

//EOR#
//BOR#require "curve25519.jinc"#formosa-25519/src/crypto_scalarmult/curve25519/amd64/ref4/curve25519.jinc
//BOR#from formosa25519 require "crypto_scalarmult/curve25519/amd64/common/bit.jinc"#formosa-25519/src/crypto_scalarmult/curve25519/amd64/common/bit.jinc
inline fn __ith_bit(stack u8[32] k, reg u64 ctr) -> reg u64
Expand Down Expand Up @@ -81,6 +60,25 @@ inline fn __decode_scalar_shl1(reg u64[4] k) -> stack u64[4]

//EOR#
//BOR#from formosa25519 require "crypto_scalarmult/curve25519/amd64/common/load_store4.jinc"#formosa-25519/src/crypto_scalarmult/curve25519/amd64/common/load_store4.jinc
inline fn __load4(reg u64 p) -> reg u64[4]
{
inline int i;
reg u64[4] a;

for i=0 to 4
{ a[i] = [p + 8*i]; }

return a;
}

inline fn __store4(reg u64 p, reg u64[4] a)
{
inline int i;

for i=0 to 4
{ [p + 8*i] = a[i]; }
}

//EOR#

//BOR#from formosa25519 require "crypto_scalarmult/curve25519/amd64/common/64/decode_u4.jinc"#formosa-25519/src/crypto_scalarmult/curve25519/amd64/common/64/decode_u4.jinc
Expand Down Expand Up @@ -1261,22 +1259,6 @@ fn _curve25519_ref4(reg u64[4] _k _u) -> reg u64[4]
return r;
}

inline fn __curve25519_ref4_ptr(#spill_to_mmx reg u64 rp, reg u64 kp up)
{
reg u64[4] r k u;

() = #spill(rp);

k = __load4(kp);
u = __load4(up);
r = _curve25519_ref4(k, u);

() = #unspill(rp);

__store4(rp, r);
}


fn _curve25519_ref4_base(reg u64[4] _k) -> reg u64[4]
{
stack u8[32] k;
Expand All @@ -1289,43 +1271,52 @@ fn _curve25519_ref4_base(reg u64[4] _k) -> reg u64[4]
return r;
}

inline fn __curve25519_ref4_base_ptr(#spill_to_mmx reg u64 rp, reg u64 kp)
{
reg u64[4] r k;

() = #spill(rp);

k = __load4(kp);
r = _curve25519_ref4_base(k);

() = #unspill(rp);

__store4(rp, r);
}

//EOR#

export fn jade_scalarmult_curve25519_amd64_ref4(#spill_to_mmx reg u64 qp np pp) -> reg u64
export fn jade_scalarmult_curve25519_amd64_ref4(
#spill_to_mmx reg ptr u64[4] qp,
reg ptr u64[4] np,
reg ptr u64[4] pp)
->
reg ptr u64[4],
reg u64
{
reg u64 r;
reg u64[4] q n p;

_ = #init_msf();
() = #spill(qp);

n = #copy(np);
p = #copy(pp);
q = _curve25519_ref4(n, p);

__curve25519_ref4_ptr(qp, np, pp);
() = #unspill(qp);
qp = #copy(q);

?{}, r = #set0();
return r;
return qp, r;
}

export fn jade_scalarmult_curve25519_amd64_ref4_base(#spill_to_mmx reg u64 qp np) -> reg u64
export fn jade_scalarmult_curve25519_amd64_ref4_base(
#spill_to_mmx reg ptr u64[4] qp,
reg ptr u64[4] np)
->
reg ptr u64[4],
reg u64
{
reg u64 r;
reg u64[4] q n;

_ = #init_msf();
() = #spill(qp);
n = #copy(np);

__curve25519_ref4_base_ptr(qp, np);
q = _curve25519_ref4_base(n);

() = #unspill(qp);
qp = #copy(q);

?{}, r = #set0();
return r;
return qp, r;
}

58 changes: 23 additions & 35 deletions src/crypto_scalarmult/curve25519/amd64/ref5/scalarmult.jazz
View file
Original file line number Diff line number Diff line change
@@ -1,24 +1,3 @@
//BOR#from formosa25519 require "crypto_scalarmult/curve25519/amd64/common/load_store4.jinc"#formosa-25519/src/crypto_scalarmult/curve25519/amd64/common/load_store4.jinc
inline fn __load4(reg u64 p) -> reg u64[4]
{
inline int i;
reg u64[4] a;

for i=0 to 4
{ a[i] = [p + 8*i]; }

return a;
}

inline fn __store4(reg u64 p, reg u64[4] a)
{
inline int i;

for i=0 to 4
{ [p + 8*i] = a[i]; }
}

//EOR#
//BOR#require "curve25519.jinc"#formosa-25519/src/crypto_scalarmult/curve25519/amd64/ref5/curve25519.jinc
//BOR#from formosa25519 require "crypto_scalarmult/curve25519/amd64/common/bit.jinc"#formosa-25519/src/crypto_scalarmult/curve25519/amd64/common/bit.jinc
inline fn __ith_bit(stack u8[32] k, reg u64 ctr) -> reg u64
Expand Down Expand Up @@ -1528,42 +1507,51 @@ inline fn __curve25519_ref5_base(reg u64[4] _k) -> reg u64[4]

//EOR#

export fn jade_scalarmult_curve25519_amd64_ref5(#spill_to_mmx reg u64 qp np pp) -> reg u64
export fn jade_scalarmult_curve25519_amd64_ref5(
#spill_to_mmx reg ptr u64[4] qp,
reg ptr u64[4] np,
reg ptr u64[4] pp)
->
reg ptr u64[4],
reg u64
{
reg u64 r;
reg u64[4] q n p;

_ = #init_msf();
() = #spill(qp);

() = #spill(qp);
n = __load4(np);
p = __load4(pp);

n = #copy(np);
p = #copy(pp);
q = __curve25519_ref5(n, p);

() = #unspill(qp);
__store4(qp, q);
() = #unspill(qp);
qp = #copy(q);

?{}, r = #set0();
return r;
return qp, r;
}

export fn jade_scalarmult_curve25519_amd64_ref5_base(#spill_to_mmx reg u64 qp np) -> reg u64
export fn jade_scalarmult_curve25519_amd64_ref5_base(
#spill_to_mmx reg ptr u64[4] qp,
reg ptr u64[4] np)
->
reg ptr u64[4],
reg u64
{
reg u64 r;
reg u64[4] q n;

_ = #init_msf();

() = #spill(qp);
n = __load4(np);
() = #spill(qp);
n = #copy(np);

q = __curve25519_ref5_base(n);

() = #unspill(qp);
__store4(qp, q);
qp = #copy(q);

?{}, r = #set0();
return r;
return qp, r;
}

2 changes: 1 addition & 1 deletion submodules/crypto-specs
Submodule crypto-specs updated 36 files
+38 −0 .github/workflows/ci.yml
+3 −2 Makefile
+3 −0 common/Array136.ec
+3 −0 common/Array1952.ec
+3 −0 common/Array2.ec
+3 −0 common/Array3309.ec
+3 −0 common/Array4032.ec
+3 −0 common/Array66.ec
+3 −0 common/Array96.ec
+7 −5 common/JWordList.ec
+1 −2 config/tests.config
+3 −4 easycrypt.project
+0 −12 fips202/.dir-locals.el
+0 −17 fips202/Makefile
+0 −0 fips202/TODO
+0 −96 fips202/properties/Example.ec
+0 −12 fips202/properties/Makefile
+0 −4 kyber768/.dir-locals.el
+0 −17 kyber768/Makefile
+0 −4 kyber768/properties/.dir-locals.el
+11 −11 kyber768/properties/Correctness.ec
+5 −5 kyber768/properties/KyberLib.ec
+103 −0 ml-dsa/Conversion.ec
+50 −0 ml-dsa/GFq.ec
+79 −0 ml-dsa/MLDSA.ec
+14 −0 ml-dsa/Parameters.ec
+93 −0 ml-dsa/Rq.ec
+140 −0 ml-dsa/Sampling.ec
+139 −0 ml-dsa/Serialization.ec
+92 −0 ml-dsa/Symmetric.ec
+122 −0 ml-dsa/VecMat.ec
+598 −12 ml-kem/properties/Correctness.ec
+4 −2 ml-kem/properties/DistrExtra.ec
+10 −9 ml-kem/properties/MLKEMLib.ec
+0 −4 xmss/.dir-locals.el
+0 −11 xmss/Makefile
2 changes: 1 addition & 1 deletion submodules/formosa-25519
Submodule formosa-25519 updated 10 files
+60 −3 .github/workflows/amd64-linux.yml
+4 −5 extract-libjade.sh
+4 −0 proof/.gitignore
+151 −0 proof/Makefile
+1 −1 src/Makefile
+2 −2 src/Makefile.common
+23 −15 src/crypto_scalarmult/curve25519/amd64/mulx/scalarmult.jazz
+0 −30 src/crypto_scalarmult/curve25519/amd64/ref4/curve25519.jinc
+30 −8 src/crypto_scalarmult/curve25519/amd64/ref4/scalarmult.jazz
+23 −15 src/crypto_scalarmult/curve25519/amd64/ref5/scalarmult.jazz

0 comments on commit 0534bc5

Please sign in to comment.