This repository was archived by the owner on Jul 13, 2026. It is now read-only.
Tags: bneb/lattice
Tags
v1.2.0: exists quantifier, algorithm suite, case-splitting Sprint complete: - Phase 1: Case-splitting for data-dependent loops (infrastructure) - Phase 2: Algorithm verification suite (4 algorithms, 21/21 Z3 pass) - Phase 3: exists quantifier syntax - Phase 4: BLOCKED (z3-0.12 Array::store crash) - Phase 5: DEFERRED (auto-invariant inference) - Phase 6: Documentation updated Z3 contracts: 21/21 pass. 38 test suites pass.
Salt v1.0.0 — first stable release Language: Z3 theorem prover embedded in the compiler. requires/ensures contracts proved at compile time. Arena memory. MLIR codegen. Compiler: 1,359 tests pass. 14 Z3 regression contracts. LLVM 21 compat. Linux, macOS, Windows targets. Academic-level language specification. Kernel: KeuOS microkernel boots in QEMU. TCP stack, SPSC rings, SYN cookies with Z3-verified non-zero ISN. ECS architecture. Lettuce: Verified Redis-compatible server. 7 modules. 4/4 Z3 contracts. Docs: SPEC.md v4.0 (EBNF grammar, formal semantics), SYNTAX.md, tutorial, FAQ, 3 blog posts, benchmark suite.
Salt Compiler v0.8.0: requires + ensures contracts, path-sensitive WP… … verification
docs: exhaustive documentation pass for v0.9.0 NetD release - README.md: bump kernel v0.8.0 → v0.9.0, add Dual-Path IPC + NetD Ring 3 data plane (60M+ PPS on KVM) to status table - docs/ARCH.md: expand kernel/net/ directory with 6 NetD modules (netd_bridge, netd_tx_bridge, netd_parse, netd_arp, netd_tcp, netd_tcp_parse), add lib/ipc_shm, add netd_bench to benchmarks - kernel/README.md: expand net/ component table with NetD subsystem, add NetD RX/TX throughput + C10M PPS to performance table, add lib/ component - docs/LATTICE_BENCHMARKS.md: add NetD RX (1319 cy) and TX (1382 cy) to TCG results table, add C10M benchmark note (6× C10M on KVM) - site/index.html: add second stat-card row with NetD C10M (60M+ PPS), Null Syscall (102cy), and SIP IPC (188cy)
v0.8.0: KPTI processes, SMP scheduler, Z3 verification, Basalt infere… …nce engine, benchmarks Salt Compiler: - Z3 formal verification: ptr bounds, slice verification, arena escape analysis, ownership state tracking - Async-to-state machine transformation with O(1) jump table dispatch - Pulse injection, yield injection, sync verifier passes - RAII-Lite: automatic Vec cleanup at scope exit - First-class function pointer types - MLIR dialect scaffolding for salt.atomic formal methods - --sip mode for software-isolated process safety enforcement Lattice Kernel: - Full process model with KPTI, PCID-tagged CR3, Ring 3 isolation - Syscall layer: sys_write, sys_brk, sys_mmap with user pointer validation - O(1) bitmap scheduler with per-core sharding (16 cores max) - Unified async/preemptive fiber dispatch via Universal Task Pointer - PMM: lock-free Treiber stack with atomic CAS cross-core stealing - VMM: 4-level page table walk, 2MB huge page splitting, guard pages - SMP bring-up: AP trampoline, per-CPU GS segment, idle loop - Flight recorder: per-core 5-cycle ring buffer tracing - ELF loader scaffolding for user-space binaries - VirtIO-Net driver with RX/TX buffer pools - Pulse event system for reactive Task 0 dispatch Basalt: - Llama 2 inference engine: transformer forward pass, RoPE, tokenizer - Z3-verified compute kernels: rmsnorm, softmax, tiled mat_mul - Mock and real model modes with tok/s benchmarking Benchmarks: - 23-program suite: Salt matches or beats C in 12/19 successful builds - KVM benchmark suite and cloud tooling
PreviousNext