| |
| |
| |
| |
|
|
| |
| #include <stdio.h> |
| #include <stdlib.h> |
| #include <string.h> |
| #include "tensor.h" |
| #include "generated_constraints.h" |
|
|
| static int load_vectors(const char *path, float (*neural)[ALP_MAXD], |
| int *expect_full, int max) { |
| FILE *f = fopen(path, "r"); |
| if (!f) return -1; |
| size_t cap = 1 << 24; |
| char *buf = malloc(cap); |
| if (!buf) { fclose(f); return -1; } |
| size_t n = fread(buf, 1, cap - 1, f); |
| buf[n] = 0; |
| fclose(f); |
| int count = 0; |
| char *p = buf; |
| while (count < max && (p = strstr(p, "\"neural\""))) { |
| p = strchr(p, '['); |
| if (!p) break; |
| p++; |
| for (int j = 0; j < ALP_MAXD; j++) { |
| neural[count][j] = strtof(p, &p); |
| while (*p == ',' || *p == ' ' || *p == '\n') p++; |
| } |
| p = strstr(p, "\"expect_clamp_full\""); |
| if (!p) break; |
| p = strchr(p, ':'); |
| if (!p) break; |
| p++; |
| while (*p == ' ') p++; |
| expect_full[count] = (*p == 't' || *p == '1'); |
| count++; |
| } |
| free(buf); |
| return count; |
| } |
|
|
| int alp_verify_encoder(const char *vector_path) { |
| static float neural[4096][ALP_MAXD]; |
| static int expect[4096]; |
| int n = load_vectors(vector_path, neural, expect, 4096); |
| if (n <= 0) { |
| fprintf(stderr, "[verifier] no vectors at %s\n", vector_path); |
| return -1; |
| } |
| int failures = 0; |
| const uint64_t head = 0x8000000000000000ull; |
| const uint64_t ident = 0xFFFFFFFFFFFFFFFFull; |
| for (int t = 0; t < n; t++) { |
| uint64_t words[4], out[2]; |
| int k = alp_encode_proofs(neural[t], neural[t], words); |
| alp_carry_prove(words, out, k); |
| int entailed = out[0] == head; |
| int ref = expect[t]; |
| |
| if (ref) { |
| if (!entailed) failures++; |
| } else if (out[0] != ident) { |
| failures++; |
| } |
| } |
| printf("[verifier] %d/%d vectors pass\n", n - failures, n); |
| return failures; |
| } |
|
|
