File size: 5,077 Bytes
2166d7e | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 | /* Walks jobs through the ten layers and shows where each refusal happens. */
#include <stdio.h>
#include <string.h>
#include "cs_sha256.h"
#include "cstack.h"
static cs_status matmul_work(void *ctx, sigma_ctx *sg, uint8_t digest[32])
{
size_t n = *(size_t *)ctx;
cs_status s = sigma_charge_mem(sg, 3 * n * n * sizeof(gl_t));
if (s == CS_OK) s = sigma_charge_steps(sg, n * n * n);
if (s != CS_OK) return s;
pmat a, b, c;
if (pmat_new(&a, n, n) != CS_OK || pmat_new(&b, n, n) != CS_OK) return CS_ERR_NOMEM;
for (size_t i = 0; i < n * n; i++) {
a.d[i] = gl_reduce(i * 2654435761u + 1);
b.d[i] = gl_reduce(i * 40503u + 7);
}
s = pmat_mul(&a, &b, &c);
if (s == CS_OK) {
cs_sha256(c.d, n * n * sizeof(gl_t), digest);
pmat_free(&c);
}
pmat_free(&a);
pmat_free(&b);
return s;
}
static void show(const char *what, cs_status s, const cstack_result *r)
{
printf(" %-34s -> %-24s", what, cs_status_str(s));
if (r->failed_layer >= 0) printf(" (stopped at layer %d)", r->failed_layer);
if (r->sealed) printf(" sealed as seal_%llu", (unsigned long long)r->seal.index);
printf("\n");
}
int main(void)
{
cstack cs;
cstack_config cfg;
memset(&cfg, 0, sizeof cfg);
cfg.policy.allowed_kinds = 1u << 1;
cfg.policy.max_payload = 256;
cfg.limits.max_mem_bytes = 1u << 20;
cfg.limits.max_steps = 1000000;
cfg.limits.max_ns = 5ull * 1000000000ull;
cs_status s = cstack_init(&cs, &cfg);
if (s != CS_OK) { printf("init failed: %s\n", cs_status_str(s)); return 1; }
printf("L0 boot cpu=%s/%s features=0x%x boot_id=", cs.boot.cpu.arch, cs.boot.cpu.vendor, cs.boot.cpu.features);
for (int i = 0; i < 8; i++) printf("%02x", cs.boot.boot_id[i]);
printf("... memory verified: %zu bytes\n", cs.boot.mem_verified_bytes);
printf("L1 uac Goldilocks p = 2^64 - 2^32 + 1, self-test %s\n", gl_selftest() == CS_OK ? "ok" : "FAILED");
const char *proof_ok = "theorem gl_mul_comm (a b : GL) : a * b = b * a := by ring\n";
const char *proof_sorry = "theorem fa_bound : x <= y := by\n sorry\n";
alp_attach_proof(&cs.alp, "gl_mul_comm", proof_ok, strlen(proof_ok));
alp_attach_proof(&cs.alp, "fa_bound", proof_sorry, strlen(proof_sorry));
char manifest[512];
alp_manifest(&cs.alp, manifest, sizeof manifest);
printf("L2 alp manifest:\n");
for (char *line = strtok(manifest, "\n"); line; line = strtok(NULL, "\n")) printf(" %s\n", line);
printf("L3-L9 jobs:\n");
size_t n = 8;
const char *needs_ok[] = {"gl_mul_comm"};
const char *needs_sorry[] = {"fa_bound"};
cstack_result r;
cstack_job j1 = {.id = 1, .kind = 1, .payload = "matmul 8x8", .payload_len = 10,
.requires = needs_ok, .nrequires = 1, .work = matmul_work, .work_ctx = &n};
show("job 1: 8x8 matmul, proven claim", cstack_submit(&cs, &j1, &r), &r);
cstack_job j2 = {.id = 2, .kind = 1, .payload = "needs fa_bound", .payload_len = 14,
.requires = needs_sorry, .nrequires = 1, .work = matmul_work, .work_ctx = &n};
show("job 2: relies on a sorry claim", cstack_submit(&cs, &j2, &r), &r);
cstack_job j3 = {.id = 3, .kind = 9, .payload = "kind not allowed", .payload_len = 16,
.work = matmul_work, .work_ctx = &n};
show("job 3: kind refused by Examiner", cstack_submit(&cs, &j3, &r), &r);
size_t huge = 200; /* 8e6 steps > 1e6 limit */
cstack_job j4 = {.id = 4, .kind = 1, .payload = "too big", .payload_len = 7,
.work = matmul_work, .work_ctx = &huge};
show("job 4: exceeds the step limit", cstack_submit(&cs, &j4, &r), &r);
n = 16;
cstack_job j5 = {.id = 5, .kind = 1, .payload = "matmul 16x16", .payload_len = 12,
.requires = needs_ok, .nrequires = 1, .work = matmul_work, .work_ctx = &n};
show("job 5: 16x16 matmul, proven claim", cstack_submit(&cs, &j5, &r), &r);
printf("L8 ledger %zu seals, chain %s\n", worm_count(&cs.worm), worm_verify(&cs.worm) == CS_OK ? "valid" : "BROKEN");
for (size_t i = 0; i < worm_count(&cs.worm); i++) {
char hex[17];
cs_hex(worm_at(&cs.worm, i)->seal, 8, hex);
printf(" seal_%zu = %s...\n", i, hex);
}
cs.worm.seals[1].witness_digest[0] ^= 1; /* simulate tampering with a past entry */
printf(" after altering one bit of seal_1's witness: %s\n",
cs_status_str(worm_verify(&cs.worm)));
cs.worm.seals[1].witness_digest[0] ^= 1;
char metrics[1024];
obs_export_metrics(&cs.obs, metrics, sizeof metrics);
printf("L9 metrics\n");
for (char *line = strtok(metrics, "\n"); line; line = strtok(NULL, "\n")) printf(" %s\n", line);
printf(" audit %llu events, chain %s\n", (unsigned long long)obs_audit_total(&cs.obs),
obs_audit_verify(&cs.obs) == CS_OK ? "valid" : "BROKEN");
cstack_shutdown(&cs);
return 0;
}
|