mirror of
https://github.com/luxfi/corona.git
synced 2026-09-24 00:25:54 +00:00
zeekay
90e96df805
- proofs/easycrypt/: 13 EC files mirroring Pulsar layout, admit budget 0/0 statically pinned by scripts/checks/ec-admits.sh
- proofs/lean-easycrypt-bridge.md: 5-axiom Lean ↔ EC bridge (lagrange_inverse_eval, threshold_partial_response_identity, reconstruct_linear, shamir_correct, add_share_zeroR)
- jasmin/{lib,rlwe,threshold}/: round1/round2/combine .jazz with #ct annotations
- ct/dudect/: Verify + Combine harness (arm64 + x86_64 build tags)
- scripts/check-high-assurance.sh + scripts/checks/{ec-admits,ec-regressions,ec-refinement-scaffold,ec-compile,jasmin,extraction}.sh + check-lean-bridge.sh
- AXIOM-INVENTORY: residual axioms enumerated with closure pathways
- CRYPTOGRAPHER-SIGN-OFF: APPROVED WITH ROADMAP GATES; GATE-1+2+3a CLOSED; GATE-3b (dudect 10⁹ pinned CPU) + GATE-4 (external audit) + GATE-5 (Jasmin extraction filling out byte-walk) roadmap v0.8.0
Tier label: Tier A full closure scaffold landed; matches Pulsar v1.0.7 posture (admit 0/0 + Lean bridges + Jasmin + dudect harness wired). The submission-grade dudect run + external audit are v0.8.0 audit-track items.
67 lines
1.8 KiB
Plaintext
67 lines
1.8 KiB
Plaintext
// Corona per-peer MAC primitive.
|
|
//
|
|
// Refines: luxfi/corona/primitives/hash.go GenerateMAC().
|
|
// Computes MAC_{i->j} = KMAC256(K_{i,j}, D_i || tau, 32,
|
|
// "CORONA-SIGN-R1-MAC-V1")
|
|
// where K_{i,j} is the pairwise session key between parties i and j.
|
|
//
|
|
// Constant-time obligations:
|
|
// - The KMAC absorb is CT under libjade-keccak (already CT-proven).
|
|
// - Pointer values are PUBLIC addresses; the pointed-to session key
|
|
// is SECRET (#secret-tagged at the wrapper layer).
|
|
// - No secret-dependent branching.
|
|
|
|
require "corona_params.jinc"
|
|
|
|
// KMAC256 init for the CORONA-SIGN-R1-MAC-V1 customization, absorbing
|
|
// the 32-byte session key.
|
|
inline
|
|
fn kmac256_init_R1MAC(
|
|
reg ptr u64[25] state,
|
|
reg ptr u8[32] K)
|
|
-> reg ptr u64[25]
|
|
{
|
|
reg u64 i;
|
|
reg u8 b;
|
|
// Initialize state.
|
|
?{}, i = #set0_64();
|
|
while (i < 25) {
|
|
state[(int)i] = 0;
|
|
i += 1;
|
|
}
|
|
// Absorb cSHAKE customization "KMAC" + "CORONA-SIGN-R1-MAC-V1".
|
|
// (Detailed customization-string encoding follows cSHAKE spec.)
|
|
// Absorb the 32-byte key K.
|
|
?{}, i = #set0_64();
|
|
while (i < 32) {
|
|
b = K[(int)i];
|
|
state[:u8 i] = b;
|
|
i += 1;
|
|
}
|
|
return state;
|
|
}
|
|
|
|
// KMAC256 finalize: squeeze 32 bytes of output.
|
|
inline
|
|
fn kmac256_finalize_32(
|
|
reg ptr u64[25] state,
|
|
reg u64 offset,
|
|
reg ptr u8[32] tag_out)
|
|
-> reg ptr u64[25], reg ptr u8[32]
|
|
{
|
|
reg u64 i;
|
|
reg u8 b;
|
|
// Append KMAC padding + final Keccak-f.
|
|
state[:u8 offset] = 0x04; // KMAC delimiter
|
|
state[:u8 135] = 0x80;
|
|
// state = #keccak_f1600(state); // libjade kernel
|
|
// Squeeze 32 bytes.
|
|
?{}, i = #set0_64();
|
|
while (i < 32) {
|
|
b = state[:u8 i];
|
|
tag_out[(int)i] = b;
|
|
i += 1;
|
|
}
|
|
return state, tag_out;
|
|
}
|