2 Commits

Author	SHA1	Message	Date
dimgigov	422df08ab9	feat: clean build + crossmodal.tla + TLA+ symmetry (v1.0.0-prep) ... Build warnings cleanup (0 warnings): - Suppress threadpool deprecation warning (baradadb.nim) - Remove unused 'os' import (logging.nim) - Fix ImplicitDefaultValue for newNode params (ast.nim) - Add explicit cstring cast for posix.open (wal.nim) - Fix HoleEnumConv for MsgKind parsing (server.nim) TLA+ Formal Verification: - Add symmetry reduction (Permutations) to all 9 existing specs - Add SYMMETRY directive to all .cfg files - New crossmodal.tla: cross-modal consistency spec * MetadataVectorConsistency, HybridResultValid * CommittedAtomicity, AbortedAtomicity, TxnStateValid - New models/crossmodal.cfg Tests: - Add Cross-Modal TLA+ Faithfulness tests (4 tests) Docs: - Update PLAN.md and BUG_AUDIT.md with completed tasks	2026-05-13 09:24:04 +03:00
dimgigov	8f87491eca	FV-14: TLA+ faithfulness tests for Nim state machines ... Add tests/tla_faithfulness.nim verifying Nim code against TLA+ invariants: - Raft: ElectionSafety, LogMatching, CommittedIndexValid - MVCC: NoDirtyReads, CommittedMustStart - 2PC: Atomicity, RecoveryConsistency Documented gap: Nim MVCC allows multiple committed versions per key, while TLA+ spec enforces first-committer-wins (WriteWriteConflict). This test ensures future changes to Nim code maintain alignment with specs. Update PLAN.md (FV-14 done), CHANGELOG.md, test_all.nim includes new suite.	2026-05-07 21:59:06 +03:00