Levalicious · Jun 28, 2026 · Jun 27, 2026 · Jun 27, 2026
@@ -0,0 +1,88 @@
+name: benchmark-history
+
+# Accumulate a reference-normalized benchmark time-series so slow creep (which the
+# per-PR head-vs-base gate is blind to) becomes visible. On every push to master
+# we run the bench, append one sample to an append-only NDJSON on the ORPHAN
+# `bench-history` branch (isolated from master/PR history — no churn), and check
+# the new sample against a rolling baseline. Creep is a SOFT-fail + commit comment.
+on:
+  push:
+    branches: [master]
+
+permissions:
+  contents: write
+
+concurrency:
+  group: bench-history
+  cancel-in-progress: false
+
+jobs:
+  accumulate:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+
+      - uses: actions/setup-node@v4
+        with:
+          node-version: 20
+
+      - name: Build and run bench (interleaved)
+        run: |
+          make -C native bench >/dev/null 2>&1
+          cp /tmp/mf_test_bench /tmp/bench
+          for i in $(seq 1 7); do /tmp/bench > "/tmp/run_$i.json"; done
+
+      - name: Aggregate one normalized sample
+        run: |
+          R=$(ls /tmp/run_*.json | paste -sd,)
+          node scripts/bench-aggregate.mjs --runs "$R" \
+            --sha "$GITHUB_SHA" --date "$(date -u +%FT%TZ)" > /tmp/sample.ndjson
+          cat /tmp/sample.ndjson
+
+      - name: Append to bench-history + creep check
+        id: creep
+        run: |
+          git config user.name  "github-actions[bot]"
+          git config user.email "github-actions[bot]@users.noreply.github.com"
+          git fetch origin bench-history || true
+          if git rev-parse --verify origin/bench-history >/dev/null 2>&1; then
+            git worktree add /tmp/hist origin/bench-history
+          else
+            git worktree add --detach /tmp/hist
+            git -C /tmp/hist checkout --orphan bench-history
+            git -C /tmp/hist rm -rf . >/dev/null 2>&1 || true
+          fi
+          touch /tmp/hist/history.ndjson
+          # creep check: new sample vs the EXISTING history (before appending)
+          set +e
+          node scripts/bench-creep.mjs --history /tmp/hist/history.ndjson --sample /tmp/sample.ndjson > /tmp/creep.md
+          echo "rc=$?" >> "$GITHUB_OUTPUT"
+          set -e
+          cat /tmp/creep.md
+          # append + push (one retry if the branch advanced under us)
+          cat /tmp/sample.ndjson >> /tmp/hist/history.ndjson
+          git -C /tmp/hist add history.ndjson
+          git -C /tmp/hist commit -m "bench: sample for ${GITHUB_SHA}"
+          git -C /tmp/hist push origin HEAD:bench-history || {
+            git -C /tmp/hist fetch origin bench-history
+            git -C /tmp/hist reset --soft origin/bench-history
+            cat /tmp/sample.ndjson >> /tmp/hist/history.ndjson
+            git -C /tmp/hist add history.ndjson
+            git -C /tmp/hist commit -m "bench: sample for ${GITHUB_SHA} (retry)"
+            git -C /tmp/hist push origin HEAD:bench-history
+          }
+
+      - name: Comment creep on commit
+        if: steps.creep.outputs.rc != '0'
+        uses: actions/github-script@v7
+        with:
+          script: |
+            const fs = require('fs');
+            const body = '<!-- bench-creep -->\n' + fs.readFileSync('/tmp/creep.md', 'utf8');
+            await github.rest.repos.createCommitComment({ ...context.repo, commit_sha: context.sha, body });
+
+      - name: Soft-fail on creep
+        if: steps.creep.outputs.rc != '0'
+        run: |
+          echo "::warning::Benchmark slow-creep detected vs rolling baseline — see the commit comment. (soft-fail)"
+          exit 1
@@ -0,0 +1,88 @@
+name: benchmark
+
+# Per-op graph-store microbenchmark, base vs head, on ONE runner — no committed
+# baseline values (nothing for git to churn). Builds the SAME harness against the
+# base and head store sources, runs them interleaved, frequency-corrects head to
+# base via a fixed-work reference op, and diffs the medians. SOFT-fail: a
+# regression turns the check red and posts a PR comment, but this check is not
+# meant to be a required status, so it never hard-blocks a merge.
+on:
+  pull_request:
+
+permissions:
+  contents: read
+  pull-requests: write
+
+jobs:
+  op-bench:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
+
+      - uses: actions/setup-node@v4
+        with:
+          node-version: 20
+
+      - name: Build head benchmark
+        run: |
+          make -C native bench >/dev/null 2>&1
+          cp /tmp/mf_test_bench /tmp/bench_head
+
+      - name: Build base benchmark (head harness, base store sources)
+        id: base
+        run: |
+          BASE_SHA="${{ github.event.pull_request.base.sha }}"
+          git worktree add --detach /tmp/base "$BASE_SHA"
+          mkdir -p /tmp/base/native
+          # Overlay the head harness so ONLY the measured store code differs.
+          cp native/op_bench.c /tmp/base/native/op_bench.c
+          cp native/Makefile  /tmp/base/native/Makefile
+          if make -C /tmp/base/native bench >/tmp/base_build.log 2>&1; then
+            cp /tmp/mf_test_bench /tmp/bench_base
+            echo "ok=1" >> "$GITHUB_OUTPUT"
+          else
+            echo "ok=0" >> "$GITHUB_OUTPUT"
+            echo "Base build failed — base likely has no comparable benchmark/store. Skipping comparison."
+            tail -25 /tmp/base_build.log || true
+          fi
+
+      - name: Run interleaved and compare
+        if: steps.base.outputs.ok == '1'
+        id: cmp
+        run: |
+          for i in $(seq 1 5); do
+            /tmp/bench_head > "/tmp/head_$i.json"
+            /tmp/bench_base > "/tmp/base_$i.json"
+          done
+          H=$(ls /tmp/head_*.json | paste -sd,)
+          B=$(ls /tmp/base_*.json | paste -sd,)
+          set +e
+          node scripts/bench-compare.mjs --base "$B" --head "$H" > /tmp/report.md
+          echo "rc=$?" >> "$GITHUB_OUTPUT"
+          set -e
+          cat /tmp/report.md
+
+      - name: Comment results on PR
+        if: steps.base.outputs.ok == '1'
+        uses: actions/github-script@v7
+        with:
+          script: |
+            const fs = require('fs');
+            const body = '<!-- op-bench -->\n' + fs.readFileSync('/tmp/report.md', 'utf8');
+            const { owner, repo } = context.repo;
+            const issue_number = context.payload.pull_request.number;
+            const comments = await github.paginate(github.rest.issues.listComments, { owner, repo, issue_number });
+            const existing = comments.find((c) => c.body && c.body.includes('<!-- op-bench -->'));
+            if (existing) {
+              await github.rest.issues.updateComment({ owner, repo, comment_id: existing.id, body });
+            } else {
+              await github.rest.issues.createComment({ owner, repo, issue_number, body });
+            }
+
+      - name: Soft-fail on regression
+        if: steps.base.outputs.ok == '1' && steps.cmp.outputs.rc != '0'
+        run: |
+          echo "::warning::Per-op benchmark regression detected — see the op-bench PR comment. (soft-fail: not a required check)"
+          exit 1
@@ -0,0 +1,49 @@
+name: proofs
+
+# Frama-C/WP proofs of the v3 store's tractable algorithms: allocator size
+# quantization + open-addressing probe (fc_proofs), name-index traversal bounds
+# (fc_index), free-list descent memory-safety (fc_tree), and the adjacency edge
+# encoding round-trip/injectivity + edge-iteration bounds (fc_graph). These prove
+# memory-model-clean abstractions of the real algorithms — no mmap region for WP
+# to reason about. Only runs when the proofs (or their build) change.
+on:
+  pull_request:
+    paths:
+      - 'native/fc_*.c'
+      - 'native/fc_stubs.h'
+      - 'native/Makefile'
+      - '.github/workflows/proofs.yml'
+  push:
+    branches: [master]
+    paths:
+      - 'native/fc_*.c'
+      - 'native/fc_stubs.h'
+      - 'native/Makefile'
+      - '.github/workflows/proofs.yml'
+
+permissions:
+  contents: read
+
+jobs:
+  wp:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+
+      - uses: ocaml/setup-ocaml@v3
+        with:
+          ocaml-compiler: "5.2"
+
+      - name: Install Frama-C + Alt-Ergo
+        run: opam install -y frama-c alt-ergo
+
+      - name: Detect provers
+        run: |
+          eval $(opam env)
+          why3 config detect
+
+      - name: Run WP proofs
+        run: |
+          eval $(opam env)
+          frama-c -version
+          make -C native proofs
@@ -11,7 +11,7 @@ CFLAGS = -std=c11 -g -O1 -Wall -Wextra -fsanitize=address,undefined \
 LIBS = -lm
 OUT = /tmp/mf_test
 
-.PHONY: test verify-detector test_memfile test_stringtable test_graph test_entity clean
+.PHONY: test verify-detector test_memfile test_stringtable test_graph test_entity bench proofs proofs-eva clean
 
 # `make test` = prove the detector fires, then run every harness with it active.
 test: verify-detector test_memfile test_stringtable test_graph test_entity
@@ -34,5 +34,28 @@ test_graph: test_graph.c graph.c stringtable.c memoryfile.c
 test_entity: test_entity.c
 	$(CC) $(CFLAGS) $^ $(LIBS) -o $(OUT)_entity && $(OUT)_entity
 
+# Per-op graph benchmark: optimized build (NO ASan / NO double-free-check — those
+# skew timing). Emits per-op rdtsc cycle stats as JSON; CI compares base vs head.
+BENCH_CFLAGS = -std=c11 -O2 -march=native -Wall -D_GNU_SOURCE -I.
+bench: op_bench.c graph.c stringtable.c memoryfile.c
+	$(CC) $(BENCH_CFLAGS) $^ -lm -o $(OUT)_bench && $(OUT)_bench
+
+# ---- Frama-C/WP + EVA proofs ----------------------------------------------
+# Memory-model-clean abstractions in fc_*.c (NEVER compiled into the build):
+# allocator size-quantization + open-addressing probe (fc_proofs), name-index
+# traversal bounds (fc_index), free-list descent safety (fc_tree), adjacency
+# edge encoding + edge-iteration bounds (fc_graph), and an EVA pass over the
+# real allocator (fc_harness). frama-c + alt-ergo + z3 (CI installs via opam).
+FRAMAC ?= frama-c
+
+# frama-c exits 0 even with unproved goals, so the gate (scripts/run-proofs.sh)
+# parses the "Proved goals: P / T" summary: clean files must be 100%, fc_tree is
+# safety-only (termination = documented acyclicity frontier).
+proofs:
+	@FRAMAC="$(FRAMAC)" bash ../scripts/run-proofs.sh
+
+proofs-eva: fc_harness.c memoryfile.c
+	$(FRAMAC) -eva -main fc_main -cpp-extra-args="-include fc_stubs.h -I." $^
+
 clean:
 	rm -f $(OUT)_*
@@ -0,0 +1,86 @@
+/*
+ * ACSL/WP: adjacency edge ENCODING + edge-iteration bounds for the v3 graph store.
+ * Every traversal (neighbors, find_path, edges, remove_edge) decodes adjacency
+ * entries via this packing and walks the adjacency block, so both are load-bearing.
+ *
+ *   frama-c -wp -wp-rte -wp-prover alt-ergo,z3 fc_graph.c
+ *
+ * 1) adj_pack / adj_pack_injective: a target offset and a 2-bit direction share one
+ *    u64, ((target<<2)|dir). Proved a ROUND-TRIP (unpack o pack == identity) and
+ *    INJECTIVE, given target fits in 62 bits and dir < 4 — no high-offset truncation,
+ *    no two distinct (target,dir) pairs aliasing to the same packed word.
+ * 2) read_edges_model: iterating n = min(count,max) 24-byte entries at
+ *    adj + 8 + i*24 (the real ADJ_HEADER_SIZE / ADJ_ENTRY_SIZE) is memory-safe —
+ *    every 24-byte access in-bounds — and terminating, given the block fits.
+ *
+ * Reads go through spec'd accessors (rd32/rd64); the real code reads via memcpy for
+ * aliasing safety, so modeling the read with an in-bounds contract keeps the proof
+ * about the OFFSET ARITHMETIC, not libc memcpy separation (same idiom as fc_index).
+ */
+#include <stdint.h>
+
+#define ADJ_HEADER_SIZE 8u
+#define ADJ_ENTRY_SIZE  24u
+#define DIR_MASK        3u
+#define TARGET_MAX      0x3fffffffffffffffULL   /* 2^62 - 1: survives << 2 losslessly */
+
+/* ---- 1. adjacency encoding: round-trip + injectivity (pure arithmetic) ---- */
+
+/* The real encoding is ((target<<2)|(dir&3u)). With dir < 4 the two fields occupy
+ * disjoint bit ranges, so it equals target*4 + dir exactly — and target < 2^62
+ * means the shift never truncates. We prove the ALGORITHM (lossless round-trip +
+ * injectivity) over that arithmetic form; decode >>2 / &3 are the unsigned /4 / %4
+ * proved below. Same abstraction boundary as fc_index modeling hash32 % bc. */
+/*@ requires target <= TARGET_MAX;
+  @ requires dir <= DIR_MASK;
+  @ assigns \nothing;
+  @ ensures \result == target * 4 + dir;
+  @ ensures \result / 4 == target;     // decode target  (== packed >> 2)
+  @ ensures \result % 4 == dir;        // decode direction(== packed & 3)
+  @*/
+uint64_t adj_pack(uint64_t target, uint64_t dir) {
+    return target * 4 + dir;
+}
+
+/*@ requires t1 <= TARGET_MAX && d1 <= DIR_MASK;
+  @ requires t2 <= TARGET_MAX && d2 <= DIR_MASK;
+  @ assigns \nothing;
+  @ ensures \result != 0 <==> (t1 == t2 && d1 == d2);
+  @*/
+int adj_pack_injective(uint64_t t1, uint64_t d1, uint64_t t2, uint64_t d2) {
+    return adj_pack(t1, d1) == adj_pack(t2, d2);
+}
+
+/* ---- 2. edge-iteration bounds (real adj-block offset arithmetic) ---- */
+
+/*@ requires o + 8 <= msize;
+  @ requires \valid_read(mem + (0 .. msize - 1));
+  @ assigns \nothing; */
+uint64_t rd64(unsigned char *mem, uint64_t msize, uint64_t o);
+
+/*@ requires o + 4 <= msize;
+  @ requires \valid_read(mem + (0 .. msize - 1));
+  @ assigns \nothing; */
+uint32_t rd32(unsigned char *mem, uint64_t msize, uint64_t o);
+
+/*@ requires \valid_read(mem + (0 .. msize - 1));
+  @ requires n <= count;
+  @ requires adj + ADJ_HEADER_SIZE + (uint64_t)count * ADJ_ENTRY_SIZE <= msize;
+  @ assigns \nothing;
+  @*/
+void read_edges_model(unsigned char *mem, uint64_t msize, uint64_t adj,
+                      uint32_t count, uint32_t n) {
+    /*@ loop invariant 0 <= i <= n;
+      @ loop assigns i;
+      @ loop variant n - i;
+      @*/
+    for (uint32_t i = 0; i < n; i++) {
+        uint64_t base = adj + ADJ_HEADER_SIZE + (uint64_t)i * ADJ_ENTRY_SIZE;
+        //@ assert base + ADJ_ENTRY_SIZE <= msize;
+        uint64_t packed = rd64(mem, msize, base + 0);
+        uint32_t rel    = rd32(mem, msize, base + 8);
+        uint64_t mtime  = rd64(mem, msize, base + 16);
+        //@ assert (packed >> 2) <= TARGET_MAX;   // decoded target always in packable range
+        (void)packed; (void)rel; (void)mtime;
+    }
+}