Skip to content
This repository was archived by the owner on Jul 13, 2026. It is now read-only.

Tags: bneb/lattice

Tags

v1.2.1

Toggle v1.2.1's commit message
Salt v1.2.1 — fix crate rename regression in test files

75 test files and fuzz target still referenced the old salt_front
crate name after the salt-front -> saltc rename. CI caught these.

v1.2.0

Toggle v1.2.0's commit message
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.

v1.1.0

Toggle v1.1.0's commit message
v1.1.0: Forall quantifiers, loop invariants, concrete verification

v1.0.0

Toggle v1.0.0's commit message
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.

v0.9.3

Toggle v0.9.3's commit message
v0.9.3: Sovereign ABI to distributed MoE convergence (7.7ms)

v0.9.2

Toggle v0.9.2's commit message
Postcondition Pivot: Z3-backed ensures verification, path-sensitive W…

…P, 6/6 GREEN

salt-v0.8.0

Toggle salt-v0.8.0's commit message
Salt Compiler v0.8.0: requires + ensures contracts, path-sensitive WP…

… verification

v0.9.1

Toggle v0.9.1's commit message
Sovereign Foundation: Cache-line isolation, Proof-Carrying IPC, SipHa…

…sh-2-4, Sovereign Reclaim

v0.9.0

Toggle v0.9.0's commit message
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

Toggle v0.8.0's commit message
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