Files
zeekay 90e96df805 Tier A full closure (v0.7.0): EC theories admit 0/0 + Lean bridges + Jasmin CT + dudect harness + e2e/fuzz
- 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.
2026-05-19 08:38:09 -07:00

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;
}