Release/0.0.27

.github/workflows/automerge.yml

@@ -12,7 +12,7 @@ jobs:
       contents: write
     runs-on: ubuntu-latest
     steps:
-    - uses: actions/checkout@v6
+    - uses: actions/checkout@v7
     - name: Configure Git
       run: |
           git config user.name 'github-actions[bot]'

.github/workflows/benchmark-history.yml

@@ -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

.github/workflows/benchmark.yml

@@ -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

.github/workflows/codeql.yml

@@ -28,7 +28,7 @@ jobs:
           build-mode: none
     steps:
     - name: Checkout repository
-      uses: actions/checkout@v6
+      uses: actions/checkout@v7
     - name: Initialize CodeQL
       uses: github/codeql-action/init@v4
       with:

.github/workflows/proofs.yml

@@ -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

.github/workflows/sync-version.yml

@@ -12,7 +12,7 @@ jobs:
     permissions:
       contents: write
     steps:
-      - uses: actions/checkout@v6
+      - uses: actions/checkout@v7
         with:
           token: ${{ secrets.GITHUB_TOKEN }}
 

.github/workflows/typescript.yml

@@ -14,7 +14,7 @@ jobs:
       contents: read
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v6
+      - uses: actions/checkout@v7
       - uses: actions/setup-node@v6
         with:
           node-version: 22
@@ -35,7 +35,7 @@ jobs:
         os: [ubuntu-latest, macos-latest]
     runs-on: ${{ matrix.os }}
     steps:
-      - uses: actions/checkout@v6
+      - uses: actions/checkout@v7
       - uses: actions/setup-node@v6
         with:
           node-version: 22
@@ -63,7 +63,7 @@ jobs:
         os: [ubuntu-latest, macos-latest]
     runs-on: ${{ matrix.os }}
     steps:
-      - uses: actions/checkout@v6
+      - uses: actions/checkout@v7
       - uses: actions/setup-node@v6
         with:
           node-version: 22
@@ -83,7 +83,7 @@ jobs:
       contents: read
       id-token: write
     steps:
-      - uses: actions/checkout@v6
+      - uses: actions/checkout@v7
       - uses: actions/setup-node@v6
         with:
           node-version: 22

binding.gyp

@@ -1,22 +1,25 @@
 {
   "targets": [
     {
-      "target_name": "memoryfile",
+      "target_name": "graphstore",
       "sources": [
         "native/memoryfile.c",
-        "native/binding.c"
+        "native/stringtable.c",
+        "native/graph.c",
+        "native/graphbind.c"
       ],
       "include_dirs": [
         "native"
       ],
-      "cflags": ["-std=c11", "-Wall", "-Wextra", "-O2"],
+      "cflags": ["-std=c11", "-Wall", "-Wextra", "-O2", "-fno-strict-aliasing", "-fno-math-errno"],
       "conditions": [
         ["OS=='linux'", {
-          "defines": ["_GNU_SOURCE"]
+          "defines": ["_GNU_SOURCE"],
+          "libraries!": ["-lnode"]
         }],
         ["OS=='mac'", {
           "xcode_settings": {
-            "OTHER_CFLAGS": ["-std=c11", "-Wall", "-Wextra", "-O2"]
+            "OTHER_CFLAGS": ["-std=c11", "-Wall", "-Wextra", "-O2", "-fno-strict-aliasing", "-fno-math-errno"]
           }
         }]
       ]

native/Makefile

@@ -0,0 +1,61 @@
+# Dev-time test build for the v3 C store.
+#
+# Compiles the fuzz/unit harnesses with AddressSanitizer + UBSan AND the
+# test-only double-free detector (-DMEMFILE_DOUBLE_FREE_CHECK). The PUBLISHED
+# addon is built by binding.gyp / node-gyp, which NEVER defines that macro, so
+# the detector is physically absent from the shipped binary (the production
+# allocator stays clean — Principle_FixCauseNotChecks).
+CC ?= cc
+CFLAGS = -std=c11 -g -O1 -Wall -Wextra -fsanitize=address,undefined \
+         -D_GNU_SOURCE -DMEMFILE_DOUBLE_FREE_CHECK -I.
+LIBS = -lm
+OUT = /tmp/mf_test
+
+.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
+
+verify-detector: test_doublefree.c memoryfile.c
+	@$(CC) $(CFLAGS) test_doublefree.c memoryfile.c $(LIBS) -o $(OUT)_df
+	@if $(OUT)_df 2>&1 | grep -q "DOUBLE-FREE detected"; then \
+	  echo "ok:   double-free detector fires (abort) on a deliberate double-free"; \
+	else echo "FAIL: double-free detector did NOT fire"; exit 1; fi
+
+test_memfile: test_memfile.c memoryfile.c
+	$(CC) $(CFLAGS) $^ $(LIBS) -o $(OUT)_memfile && $(OUT)_memfile
+
+test_stringtable: test_stringtable.c stringtable.c memoryfile.c
+	$(CC) $(CFLAGS) $^ $(LIBS) -o $(OUT)_st && $(OUT)_st
+
+test_graph: test_graph.c graph.c stringtable.c memoryfile.c
+	$(CC) $(CFLAGS) $^ $(LIBS) -o $(OUT)_graph && $(OUT)_graph
+
+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)_*

native/bench/.gitignore

@@ -0,0 +1,6 @@
+# Compiled allocator bench/test binaries (build via this dir's Makefile).
+bench_cart
+bench_radix
+bench_radix_asan
+test_cart
+test_coalesce