Hugging Face's logo

Snapkitty
/
flash-attention-rtl

snapkitty
october-2026-drop
systemverilog
rtl
systolic-array
subleq
flash-attention
cocotb
hardware
nim
python
Model card Files
xet
 Community
flash-attention-rtl / cstack /tests /test_l2_alp.c
SNAPKITTYWEST's picture
SNAPKITTYWEST
October 2026 main drop: mirror from GitHub
2166d7e verified
Raw History Blame Contribute Delete
4.8 kB
#include "cs_test.h"
#include "l2_alp.h"
#include <stdio.h>
#include <string.h>
#define SCAN(s) alp_scan_sorries((s), strlen(s))
TEST_MAIN_BEGIN("l2 alp")
/* sorry scanner */
CHECK(SCAN("") == 0);
CHECK(SCAN("theorem t : 1 = 1 := rfl") == 0);
CHECK(SCAN("theorem t : 1 = 1 := by sorry") == 1);
CHECK(SCAN("sorry sorry\nsorry") == 3);
CHECK(SCAN("sorryAx mysorry sorry_2 sorry'") == 0); /* different identifiers */
CHECK(SCAN("-- sorry in a line comment\nby rfl") == 0);
CHECK(SCAN("/- sorry -/ by sorry") == 1);
CHECK(SCAN("/- outer /- inner sorry -/ still comment sorry -/ done") == 0); /* nesting */
CHECK(SCAN("/-- doc sorry -/ by rfl") == 0);
CHECK(SCAN("\"sorry\" ++ x") == 0); /* string literal */
CHECK(SCAN("\"a \\\" sorry\" by sorry") == 1); /* escaped quote */
CHECK(SCAN("(sorry)") == 1 && SCAN("by\n sorry\n") == 1);
CHECK(SCAN("/- unterminated sorry") == 0);
alp_registry r;
alp_init(&r);
CHECK(alp_state_of(&r, "x") == ALP_MISSING);
CHECK_EQ_STATUS(alp_require(&r, "x"), CS_ERR_UNPROVEN);
CHECK_EQ_STATUS(alp_declare(&r, "gl_mul_correct"), CS_OK);
CHECK(alp_state_of(&r, "gl_mul_correct") == ALP_MISSING);
CHECK_EQ_STATUS(alp_require(&r, "gl_mul_correct"), CS_ERR_UNPROVEN);
const char *good = "theorem gl_mul_correct : ∀ a b, a * b = b * a := by\n intro a b; ring\n";
const char *bad = "theorem fa_bound : x ≤ y := by\n sorry\n";
CHECK_EQ_STATUS(alp_attach_proof(&r, "gl_mul_correct", good, strlen(good)), CS_OK);
CHECK_EQ_STATUS(alp_attach_proof(&r, "fa_bound", bad, strlen(bad)), CS_OK);
CHECK(alp_state_of(&r, "gl_mul_correct") == ALP_PROVEN);
CHECK(alp_state_of(&r, "fa_bound") == ALP_SORRY);
CHECK(alp_proof_available(&r, "gl_mul_correct") && !alp_proof_available(&r, "fa_bound"));
CHECK_EQ_STATUS(alp_require(&r, "gl_mul_correct"), CS_OK);
CHECK_EQ_STATUS(alp_require(&r, "fa_bound"), CS_ERR_UNPROVEN);
CHECK(alp_total_sorries(&r) == 1);
/* proof drift: the recorded hash binds the proof source */
CHECK_EQ_STATUS(alp_verify_proof(&r, "gl_mul_correct", good, strlen(good)), CS_OK);
const char *edited = "theorem gl_mul_correct : ∀ a b, a * b = b * a := by\n intro a b; simp\n";
CHECK_EQ_STATUS(alp_verify_proof(&r, "gl_mul_correct", edited, strlen(edited)), CS_ERR_TAMPER);
CHECK_EQ_STATUS(alp_verify_proof(&r, "nope", good, strlen(good)), CS_ERR_UNPROVEN);
/* a sorry proof can be replaced by a complete one */
const char *fixed = "theorem fa_bound : x ≤ y := by\n omega\n";
CHECK_EQ_STATUS(alp_attach_proof(&r, "fa_bound", fixed, strlen(fixed)), CS_OK);
CHECK(alp_state_of(&r, "fa_bound") == ALP_PROVEN && alp_total_sorries(&r) == 0);
CHECK_EQ_STATUS(alp_attach_proof(&r, "fa_bound", bad, strlen(bad)), CS_OK); /* regression */
CHECK(alp_state_of(&r, "fa_bound") == ALP_SORRY);
/* file attach */
const char *path = "build/alp_test.lean";
FILE *f = fopen(path, "wb");
CHECK(f != NULL);
if (f) { fputs("lemma l : True := by trivial\n", f); fclose(f); }
CHECK_EQ_STATUS(alp_attach_file(&r, "from_file", path), CS_OK);
CHECK(alp_state_of(&r, "from_file") == ALP_PROVEN);
CHECK_EQ_STATUS(alp_attach_file(&r, "x2", "build/does_not_exist.lean"), CS_ERR_IO);
remove(path);
/* manifest: deterministic, snprintf-style sizing */
alp_declare(&r, "pending");
char big[1024], small[40];
size_t need = alp_manifest(&r, big, sizeof big);
CHECK(need == strlen(big));
CHECK(strncmp(big, "alp-manifest v1\n", 16) == 0);
CHECK(strstr(big, "fa_bound sorry sorries=1 sha256=") != NULL);
CHECK(strstr(big, "pending missing sorries=0 sha256=-\n") != NULL);
CHECK(strstr(big, "total_sorries=1\n") != NULL);
char big2[1024];
CHECK(alp_manifest(&r, big2, sizeof big2) == need && strcmp(big, big2) == 0);
CHECK(alp_manifest(&r, small, sizeof small) == need); /* truncated but sized correctly */
CHECK(strlen(small) == sizeof small - 1 && strncmp(small, big, sizeof small - 1) == 0);
CHECK(alp_manifest(&r, NULL, 0) == need);
/* limits and name validation */
CHECK_EQ_STATUS(alp_declare(&r, ""), CS_ERR_ARG);
CHECK_EQ_STATUS(alp_declare(&r, "has space"), CS_ERR_ARG);
char longname[ALP_NAME_MAX + 8];
memset(longname, 'a', sizeof longname - 1);
longname[sizeof longname - 1] = '\0';
CHECK_EQ_STATUS(alp_declare(&r, longname), CS_ERR_ARG);
alp_registry full;
alp_init(&full);
for (int i = 0; i < ALP_MAX_CLAIMS; i++) {
char n[16];
snprintf(n, sizeof n, "c%d", i);
CHECK_EQ_STATUS(alp_declare(&full, n), CS_OK);
}
CHECK_EQ_STATUS(alp_declare(&full, "one_too_many"), CS_ERR_NOMEM);
TEST_MAIN_END