mirror of
https://github.com/luxfi/corona.git
synced 2026-09-24 00:25:54 +00:00
- 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.
113 lines
3.5 KiB
C
113 lines
3.5 KiB
C
/*
|
|
* Copyright (C) 2025-2026, Lux Industries Inc. All rights reserved.
|
|
* See the file LICENSE for licensing terms.
|
|
*
|
|
* dudect_verify.c -- dudect main loop driving corona threshold.Verify
|
|
* through the cgo bridge in verify_ct.go.
|
|
*/
|
|
|
|
#define DUDECT_IMPLEMENTATION
|
|
#include "dudect/src/dudect.h"
|
|
|
|
#include <stdio.h>
|
|
#include <stdlib.h>
|
|
#include <string.h>
|
|
|
|
extern int corona_verify_ct_setup(void);
|
|
extern size_t corona_verify_ct_sig_size(void);
|
|
extern size_t corona_verify_ct_pool_size(void);
|
|
extern int corona_verify_ct_copy_pool(size_t idx, uint8_t *dst);
|
|
extern void corona_verify_ct(uint8_t *data);
|
|
|
|
static size_t g_chunk_size = 0;
|
|
static size_t g_pool_size = 0;
|
|
|
|
void prepare_inputs(dudect_config_t *cfg, uint8_t *input_data, uint8_t *classes) {
|
|
for (size_t i = 0; i < cfg->number_measurements; i++) {
|
|
classes[i] = randombit();
|
|
uint8_t *slot = input_data + (size_t)i * cfg->chunk_size;
|
|
if (classes[i] == 0) {
|
|
/* Class A: pool[0] every time. */
|
|
(void)corona_verify_ct_copy_pool(0, slot);
|
|
} else {
|
|
/* Class B: a uniformly-drawn valid sig from the pool. */
|
|
uint8_t pick_buf[8];
|
|
randombytes(pick_buf, sizeof pick_buf);
|
|
uint64_t pick = 0;
|
|
for (size_t k = 0; k < sizeof pick_buf; k++) {
|
|
pick = (pick << 8) | pick_buf[k];
|
|
}
|
|
(void)corona_verify_ct_copy_pool((size_t)(pick % g_pool_size), slot);
|
|
}
|
|
}
|
|
}
|
|
|
|
uint8_t do_one_computation(uint8_t *data) {
|
|
corona_verify_ct(data);
|
|
uint8_t acc = 0;
|
|
for (size_t i = 0; i < g_chunk_size; i++) acc ^= data[i];
|
|
return acc;
|
|
}
|
|
|
|
int main(int argc, char **argv) {
|
|
(void)argc;
|
|
(void)argv;
|
|
|
|
int rc = corona_verify_ct_setup();
|
|
if (rc != 0) {
|
|
fprintf(stderr, "corona_verify_ct_setup failed: rc=%d\n", rc);
|
|
return 1;
|
|
}
|
|
g_chunk_size = corona_verify_ct_sig_size();
|
|
if (g_chunk_size == 0) {
|
|
fprintf(stderr, "corona_verify_ct_sig_size returned 0\n");
|
|
return 1;
|
|
}
|
|
g_pool_size = corona_verify_ct_pool_size();
|
|
if (g_pool_size == 0) {
|
|
fprintf(stderr, "corona_verify_ct_pool_size returned 0\n");
|
|
return 1;
|
|
}
|
|
|
|
size_t number_measurements = 10000;
|
|
const char *env_n = getenv("DUDECT_SAMPLES");
|
|
if (env_n) {
|
|
long n = strtol(env_n, NULL, 10);
|
|
if (n > 0) number_measurements = (size_t)n;
|
|
}
|
|
size_t max_batches = 4;
|
|
const char *env_b = getenv("DUDECT_MAX_BATCHES");
|
|
if (env_b) {
|
|
long b = strtol(env_b, NULL, 10);
|
|
if (b > 0) max_batches = (size_t)b;
|
|
}
|
|
|
|
dudect_config_t cfg = {
|
|
.chunk_size = g_chunk_size,
|
|
.number_measurements = number_measurements,
|
|
};
|
|
dudect_ctx_t ctx;
|
|
if (dudect_init(&ctx, &cfg) != 0) {
|
|
fprintf(stderr, "dudect_init failed\n");
|
|
return 1;
|
|
}
|
|
|
|
fprintf(stderr, "dudect_verify: Corona R-LWE, chunk=%zu bytes, batch=%zu samples, max_batches=%zu, pool=%zu valid sigs\n",
|
|
g_chunk_size, number_measurements, max_batches, g_pool_size);
|
|
|
|
dudect_state_t state = DUDECT_NO_LEAKAGE_EVIDENCE_YET;
|
|
for (size_t batch = 0; batch < max_batches; batch++) {
|
|
state = dudect_main(&ctx);
|
|
if (state == DUDECT_LEAKAGE_FOUND) break;
|
|
}
|
|
dudect_free(&ctx);
|
|
|
|
if (state == DUDECT_LEAKAGE_FOUND) {
|
|
fprintf(stderr, "dudect_verify: LEAKAGE FOUND (t-statistic exceeded threshold)\n");
|
|
return 2;
|
|
}
|
|
fprintf(stderr, "dudect_verify: no leakage evidence after %zu batches of %zu samples\n",
|
|
max_batches, number_measurements);
|
|
return 0;
|
|
}
|