Skip to content

Commit 71d2c7f

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
proofs(octad): mechanise octad modality algebra (O-series + R1–R3) (#109)
## Summary First **post-foundation** Coq module. `formal/Octad.v` mechanises the **Modality Algebra** of the octad data-model paper (`docs/papers/arcvix-octad-data-model.tex`, `sec:modality-algebra`) — the octad-modularity experiment whose only stated proof so far was a one-line pen-and-paper argument. The keystone is the paper's **Merge Commutativity** proposition, now machine-checked, with its associativity/idempotence companions. Together these cover the **O-series** (octad identity invariants) and the **R-series** (CRDT-shaped merge) from the issue #77 inventory. ## Theorems (12, in one module) | Inventory | Theorem(s) | What it says | |---|---|---| | O2 | `modality_cardinality`, `modality_exhaustive` | the basis is exactly the 8 modalities (mirrors `ModalityStatus`) | | O10 | `complete_iff_no_missing` | `is_complete` ⇔ `missing = []` — cross-checks the two Rust methods | | Projection | `project_full`, `project_idempotent`, `project_compose` | `pi_M` is idempotent; `pi_M ∘ pi_N = pi_{M∧N}` (meet-semilattice) | | **R1** | **`merge_commutative`** | **the paper's Merge Commutativity proposition, mechanised** | | R2 | `merge_associative` | merge associative when `resolve` is | | R3 | `merge_idempotent` | merge idempotent when `resolve` is | | inv:persist | `merge_preserves_id`, `enrich_preserves_id`, `project_preserves_id` | identity is immutable under the algebra | | Enrichment | `enrich_sets_target`, `enrich_preserves_others`, `enrich_present` | the write primitive sets its target, leaves the rest | ## On #77's "honest uncertainty" about R1–R3 Issue #77 flags R1/R2/R3 as *"likely false as currently written"* because the concrete `AutoMerge` heuristic isn't unconditionally commutative. The faithful resolution — the paper's — is mechanised here: octad merge `⊕` **inherits exactly the algebra of its conflict-resolution kernel `resolve`**. `⊕` is commutative / associative / idempotent **iff** `resolve` is, so the laws are stated as implications. A CRDT-shaped `resolve` (a join on a semilattice) instantiates all three; `AutoMerge` does not — and the implication makes that explicit rather than over-claiming. ## Axiom discipline Closes on `mval`, `ident` (Parameters) and `functional_extensionality_dep` (Coq stdlib) only — the same whitelist entry `WAL.v`/`Normalizer.v` use. `Print Assumptions` confirms zero slippage; `modality_cardinality`/`modality_exhaustive` close under the global context with **no** axioms. ## Wiring - `formal/Justfile` — `octad` compile recipe + `check-octad` guard, added to `all` and `check-assumptions`. - `.github/workflows/coq-build.yml` — compile + assumptions-whitelist steps. - `formal/CROSS-REPO-MAP.adoc` — 5 new mapping rows (projection→`EchoTruncation`, completeness→`EchoCharacteristic`, merge→candidate new join-semilattice abstraction, enrichment→`EchoProvenance`), status refreshed. ## Verification (local, coqc 8.18.0) Clean rebuild, replicating CI exactly: ``` 9 modules compile · 9 assumption guards pass · zero axiom slippage ``` This run also re-verified the **existing 8** modules — the whole `formal/` corpus is green. Refs #77. Draft pending owner review of the spec choices (the `resolve`-conditional framing of R1–R3, and the echo-types companion-issue flag for the join-semilattice abstraction). 🤖 Generated with [Claude Code](https://claude.com/claude-code) --- _Generated by [Claude Code](https://claude.ai/code/session_01W9Voe3JceP66Bna9FT4jME)_ --------- Co-authored-by: Claude <noreply@anthropic.com>
1 parent 2704e0a commit 71d2c7f

15 files changed

Lines changed: 931 additions & 86 deletions

File tree

‎.clusterfuzzlite/build.sh‎

Lines changed: 36 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -12,20 +12,48 @@
1212

1313
set -euo pipefail
1414

15+
# ── Toolchain floor ──────────────────────────────────────────────────────
16+
# The OSS-Fuzz base-builder-rust image pins an older nightly (rustc 1.91 at
17+
# time of writing), but part of the dependency graph — burn / cubecl-zspace,
18+
# pulled transitively via verisim-tensor (fuzz -> verisim-api) —
19+
# declares rust-version = 1.92. cargo-fuzz rebuilds the standard library with
20+
# -Zbuild-std, so all we need is a new-enough nightly with rust-src present.
21+
# Install one and force it for the whole script via RUSTUP_TOOLCHAIN. This is
22+
# contained to the fuzz job: it never touches the main workspace toolchain or
23+
# any other CI job.
24+
rustup toolchain install nightly --profile minimal \
25+
--component rust-src --component llvm-tools-preview
26+
export RUSTUP_TOOLCHAIN=nightly
27+
1528
# cargo-fuzz drives libfuzzer; install it if missing.
1629
if ! command -v cargo-fuzz &>/dev/null; then
1730
cargo install cargo-fuzz --locked
1831
fi
1932

20-
# ── fuzz_octad_id — top-level fuzz crate ─────────────────────────────────
21-
cd "${SRC}/verisimdb/fuzz"
22-
cargo fuzz build --release --sanitizer="${SANITIZER:-address}"
23-
cp target/*/release/fuzz_octad_id "${OUT}/"
33+
# Build one named fuzz target from the project's single cargo-fuzz crate
34+
# (fuzz/) and copy the binary to $OUT. cargo-fuzz resolves ONE fuzz directory
35+
# per project, so both targets are hosted in fuzz/; building each by name is
36+
# reliable. We then locate the produced binary wherever cargo-fuzz placed it
37+
# (not a brittle glob), failing loudly if nothing was produced.
38+
build_target() {
39+
local crate_dir="$1" target="$2"
40+
echo "── building fuzz target '${target}' in ${crate_dir} ──"
41+
(
42+
cd "${crate_dir}"
43+
cargo fuzz build --release --sanitizer="${SANITIZER:-address}" "${target}"
44+
local bin
45+
bin="$(find . -type f -name "${target}" -path '*/release/*' -print -quit)"
46+
if [[ -z "${bin}" ]]; then
47+
echo "ERROR: no '${target}' binary produced under ${crate_dir}" >&2
48+
exit 1
49+
fi
50+
cp "${bin}" "${OUT}/${target}"
51+
echo "── copied ${bin} -> ${OUT}/${target} ──"
52+
)
53+
}
2454

25-
# ── fuzz_vql_parser — rust-core fuzz crate ───────────────────────────────
26-
cd "${SRC}/verisimdb/rust-core/fuzz"
27-
cargo fuzz build --release --sanitizer="${SANITIZER:-address}"
28-
cp target/*/release/fuzz_vql_parser "${OUT}/"
55+
build_target "${SRC}/verisimdb/fuzz" fuzz_octad_id
56+
build_target "${SRC}/verisimdb/fuzz" fuzz_vql_parser
2957

3058
# Optional seed corpora — empty for now, will populate as we discover
3159
# interesting inputs. Comment in once corpora exist:

‎.github/workflows/build-validation.yml‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -15,9 +15,9 @@ jobs:
1515
name: Rust build validation
1616
runs-on: ubuntu-latest
1717
steps:
18-
- uses: actions/checkout@v6.0.3
19-
- uses: dtolnay/rust-toolchain@stable
20-
- uses: Swatinem/rust-cache@v2
18+
- uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
19+
- uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable
20+
- uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2
2121
- run: cargo check --workspace
2222

2323
validate-elixir:
@@ -27,8 +27,8 @@ jobs:
2727
run:
2828
working-directory: elixir-orchestration
2929
steps:
30-
- uses: actions/checkout@v6.0.3
31-
- uses: erlef/setup-beam@v1
30+
- uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
31+
- uses: erlef/setup-beam@8251c48667b97e88a0a24ec512f5b72a039fcea7 # v1
3232
with:
3333
elixir-version: "1.17"
3434
otp-version: "27"

‎.github/workflows/coq-build.yml‎

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -90,6 +90,12 @@ jobs:
9090
set -euo pipefail
9191
coqc -q PlannerSemantic.v | tee PlannerSemantic.out
9292
93+
- name: Compile Octad.v
94+
working-directory: formal
95+
run: |
96+
set -euo pipefail
97+
coqc -q Octad.v | tee Octad.out
98+
9399
- name: Verify Provenance assumptions whitelist
94100
working-directory: formal
95101
run: |
@@ -220,3 +226,22 @@ jobs:
220226
exit 1
221227
fi
222228
echo "OK(PlannerSemantic): Q1-full semantic equivalence + membership"
229+
230+
- name: Verify Octad assumptions whitelist
231+
working-directory: formal
232+
run: |
233+
set -euo pipefail
234+
# Whitelist: 2 Parameters (mval, ident) + functional_extensionality_dep
235+
# (Coq stdlib). modality is inductive; resolve is an operation
236+
# argument — neither is an axiom.
237+
UNEXPECTED=$(awk '/^[A-Za-z_][A-Za-z0-9_]* :/ {print $1}' Octad.out \
238+
| sort -u \
239+
| grep -vE '^(mval|ident|functional_extensionality_dep)$' || true)
240+
if [ -n "$UNEXPECTED" ]; then
241+
echo "ERROR(Octad): unexpected axiom(s) in Print Assumptions:"
242+
echo "$UNEXPECTED"
243+
echo "---"
244+
cat Octad.out
245+
exit 1
246+
fi
247+
echo "OK(Octad): O-series + R1-R3 modality algebra whitelisted"

‎.github/workflows/fuzz.yml‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -25,9 +25,9 @@ jobs:
2525
permissions:
2626
contents: read
2727
steps:
28-
- uses: actions/checkout@v6.0.3
29-
- uses: dtolnay/rust-toolchain@stable
30-
- uses: Swatinem/rust-cache@v2
28+
- uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
29+
- uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable
30+
- uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2
3131
- name: Run core fuzz compile check
3232
run: |
3333
cd rust-core/fuzz
@@ -40,9 +40,9 @@ jobs:
4040
permissions:
4141
contents: read
4242
steps:
43-
- uses: actions/checkout@v6.0.3
44-
- uses: dtolnay/rust-toolchain@stable
45-
- uses: Swatinem/rust-cache@v2
43+
- uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
44+
- uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable
45+
- uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2
4646
- name: Run debugger fuzz compile check
4747
run: |
4848
cd debugger/fuzz

‎.github/workflows/rust-ci.yml‎

Lines changed: 31 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -28,8 +28,8 @@ jobs:
2828
name: rustfmt
2929
runs-on: ubuntu-latest
3030
steps:
31-
- uses: actions/checkout@v6.0.3
32-
- uses: dtolnay/rust-toolchain@stable
31+
- uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
32+
- uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable
3333
with:
3434
components: rustfmt
3535
- run: cargo fmt --all -- --check
@@ -38,20 +38,20 @@ jobs:
3838
name: clippy (all-targets)
3939
runs-on: ubuntu-latest
4040
steps:
41-
- uses: actions/checkout@v6.0.3
42-
- uses: dtolnay/rust-toolchain@stable
41+
- uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
42+
- uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable
4343
with:
4444
components: clippy
45-
- uses: Swatinem/rust-cache@v2
45+
- uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2
4646
- run: cargo clippy --workspace --all-targets --no-deps -- -D warnings
4747

4848
test:
4949
name: cargo test
5050
runs-on: ubuntu-latest
5151
steps:
52-
- uses: actions/checkout@v6.0.3
53-
- uses: dtolnay/rust-toolchain@stable
54-
- uses: Swatinem/rust-cache@v2
52+
- uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
53+
- uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable
54+
- uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2
5555
- run: cargo test --workspace --no-fail-fast
5656

5757
doc:
@@ -60,51 +60,51 @@ jobs:
6060
env:
6161
RUSTDOCFLAGS: "-D warnings"
6262
steps:
63-
- uses: actions/checkout@v6.0.3
64-
- uses: dtolnay/rust-toolchain@stable
65-
- uses: Swatinem/rust-cache@v2
63+
- uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
64+
- uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable
65+
- uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2
6666
- run: cargo doc --workspace --no-deps
6767

6868
audit:
6969
name: cargo audit
7070
runs-on: ubuntu-latest
7171
steps:
72-
- uses: actions/checkout@v6.0.3
73-
- uses: rustsec/audit-check@v2.0.0
72+
- uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
73+
- uses: rustsec/audit-check@69366f33c96575abad1ee0dba8212993eecbe998 # v2.0.0
7474
with:
7575
token: ${{ secrets.GITHUB_TOKEN }}
7676

7777
deny:
7878
name: cargo deny
7979
runs-on: ubuntu-latest
8080
steps:
81-
- uses: actions/checkout@v6.0.3
82-
- uses: EmbarkStudios/cargo-deny-action@v2
81+
- uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
82+
- uses: EmbarkStudios/cargo-deny-action@8f84122a46a358a27cb0625d85ad60ab436a1b87 # v2
8383
with:
8484
command: check advisories bans licenses sources
8585

8686
bench-compile:
8787
name: benchmarks compile
8888
runs-on: ubuntu-latest
8989
steps:
90-
- uses: actions/checkout@v6.0.3
91-
- uses: dtolnay/rust-toolchain@stable
92-
- uses: Swatinem/rust-cache@v2
90+
- uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
91+
- uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable
92+
- uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2
9393
- run: cargo bench --no-run
9494

9595
coverage:
9696
name: cargo-llvm-cov (≥60%)
9797
runs-on: ubuntu-latest
9898
steps:
99-
- uses: actions/checkout@v6.0.3
100-
- uses: dtolnay/rust-toolchain@stable
99+
- uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
100+
- uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable
101101
with:
102102
components: llvm-tools-preview
103-
- uses: Swatinem/rust-cache@v2
104-
- uses: taiki-e/install-action@cargo-llvm-cov
103+
- uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2
104+
- uses: taiki-e/install-action@28ba36d36bfc4814f98a469ff9f76b2a41e9aa8a # cargo-llvm-cov
105105
- name: Generate lcov report
106106
run: cargo llvm-cov --workspace --lcov --output-path lcov.info
107-
- uses: codecov/codecov-action@v6
107+
- uses: codecov/codecov-action@e79a6962e0d4c0c17b229090214935d2e33f8354 # v6
108108
with:
109109
files: lcov.info
110110
flags: rust
@@ -122,10 +122,10 @@ jobs:
122122
runs-on: ubuntu-latest
123123
if: github.event_name == 'workflow_dispatch' || github.event_name == 'schedule'
124124
steps:
125-
- uses: actions/checkout@v6.0.3
126-
- uses: dtolnay/rust-toolchain@stable
127-
- uses: Swatinem/rust-cache@v2
128-
- uses: taiki-e/install-action@v2
125+
- uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
126+
- uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable
127+
- uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2
128+
- uses: taiki-e/install-action@25435dc8dd3baed7417e0c96d3fe89013a5b2e09 # v2
129129
with:
130130
tool: cargo-mutants
131131
- name: Run mutation tests on core invariant crates
@@ -140,7 +140,7 @@ jobs:
140140
--no-shuffle \
141141
--output mutants-out/
142142
continue-on-error: true
143-
- uses: actions/upload-artifact@v7
143+
- uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7
144144
if: always()
145145
with:
146146
name: mutants-report
@@ -155,7 +155,7 @@ jobs:
155155
- fuzz/Cargo.toml
156156
- rust-core/fuzz/Cargo.toml
157157
steps:
158-
- uses: actions/checkout@v6.0.3
159-
- uses: dtolnay/rust-toolchain@stable
160-
- uses: Swatinem/rust-cache@v2
158+
- uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
159+
- uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable
160+
- uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2
161161
- run: cargo check --manifest-path ${{ matrix.manifest }}

0 commit comments

Comments
 (0)