README.md
1 # aleph-008: The Continuity Project 2 3 | Field | Value | 4 |-------|-------| 5 | RFC | aleph-008 | 6 | Title | The Continuity Project | 7 | Author | b7r6 | 8 | Status | Draft | 9 | Created | 2026-01-22 | 10 11 ## Abstract 12 13 Continuity is continuity. Continuity's job is continuity. 14 15 All computations run on "perfect conceptual computers." Correct by construction - 16 the result is saved. One content-addressing scheme - the hash is the artifact. 17 CA-derivations, Buck2, and Bazel are supports for a coset - they produce the 18 same cache keys because they're all content-addressing. 19 20 This RFC describes the unified build/cache/attestation system called 21 **straylight**, which eliminates redundancy in favor of superior alternatives 22 and composes a minimal set of atoms into a complete computational universe. 23 24 ## Core Thesis 25 26 ### The Atoms 27 28 Plan 9 failed because "everything is a file" is too simple. The algebra is 29 slightly bigger: 30 31 | Atom | What It Is | Implementation | 32 |------|------------|----------------| 33 | **namespace** | isolation boundary | `unshare` | 34 | **microvm** | compute unit | firecracker | 35 | **build** | computation with result | derivation | 36 | **store** | content-addressed storage | r2 | 37 | **identity** | cryptographic identity | ed25519 | 38 | **attestation** | signature on artifact | git | 39 40 These are the primitives. Not "hash -> bytes" - there's structure. 41 42 ### Eliminations 43 44 Redundant things eliminated in favor of superior alternatives: 45 46 | Eliminated | Replaced By | Rationale | 47 |------------|-------------|-----------| 48 | Bazel | Buck2 (DICE) | Obsolete junk | 49 | Starlark | Dhall | System Fomega, total, sufficient | 50 | Preludes | Explicit typed toolchains | No magic | 51 | Globs | Explicit file lists | "I'll know what I'm building or I'll know the reason why" | 52 | String-typed configs | Real triples, real compilers, real flags | Type safety | 53 | nix remote builders | isospin | Build hook is a Superfund site | 54 | nix daemon | armitage | Witness proxy, coeffect-aware | 55 | "purity" boolean | coeffect algebra | Graded resources, not pure/impure | 56 57 ### The Stack 58 59 ``` 60 straylight (CLI) 61 │ 62 ├── armitage (nix shim) 63 │ │ 64 │ ├── witness proxy (fetches → R2) 65 │ ├── coeffect checker (Lean4) 66 │ └── attestation (ed25519 + git) 67 │ 68 ├── DICE (real builds) 69 │ │ 70 │ ├── Dhall (BUILD files, System Fω, total) 71 │ ├── Buck2 core (action graph, RE, TSET) 72 │ └── Executor (wasm sandbox / isospin) 73 │ 74 └── Store 75 │ 76 ├── R2 (bytes, content-addressed) 77 ├── git (attestations, refs) 78 └── ed25519 (identity, signing) 79 ``` 80 81 See [armitage.md](armitage.md) for the nix compatibility layer design. 82 83 ## Component 1: Dhall Build Language 84 85 Dhall is sufficient. It is: 86 87 - System Fomega (typed, higher-kinded) 88 - Total (guaranteed termination) 89 - Content-addressed imports (the hash IS the version) 90 - Hermetic (no IO, no escape) 91 - Simple (not a general purpose language) 92 - Exists (dhall-rust is lootable) 93 94 ### BUILD.dhall 95 96 ```dhall 97 -- BUILD.dhall 98 99 let DICE = https://straylight.cx/dice/v1.dhall sha256:abc... 100 let Targets = https://straylight.cx/targets/v1.dhall sha256:def... 101 let Rust = https://straylight.cx/rules/rust/v1.dhall sha256:123... 102 let Lean = https://straylight.cx/rules/lean/v1.dhall sha256:456... 103 let C = https://straylight.cx/rules/c/v1.dhall sha256:789... 104 let Wasm = https://straylight.cx/rules/wasm/v1.dhall sha256:aaa... 105 106 -- targets 107 let targets = 108 { native = Targets.host 109 , orin = Targets.aarch64-linux { cpu = "cortex-a78ae" } 110 , wasm = Targets.wasm32-wasi 111 } 112 113 -- proven core (lean -> c -> wasm, never changes) 114 let r2_backend = Lean.library 115 { name = "r2-backend" 116 , srcs = [ "core/r2_backend.lean" ] 117 , deps = [ "//core:sha256", "//core:s3" ] 118 , extract = C.extract 119 { target = targets.wasm 120 , verified = True 121 } 122 } 123 124 let git_odb = Lean.library 125 { name = "git-odb" 126 , srcs = [ "core/git_odb.lean" ] 127 , deps = [ r2_backend ] 128 , extract = C.extract 129 { target = targets.wasm 130 , verified = True 131 } 132 } 133 134 -- wasm modules from proven C 135 let builtins_wasm = Wasm.module 136 { name = "builtins" 137 , src = builtins 138 , optimize = Wasm.O3 139 , features = [ Wasm.bulk_memory, Wasm.simd ] 140 } 141 142 -- rust tooling (uses proven wasm via wasmtime) 143 let straylight_core = Rust.library 144 { name = "straylight-core" 145 , srcs = 146 [ "src/core/lib.rs" 147 , "src/core/store.rs" 148 , "src/core/artifact.rs" 149 ] 150 , deps = 151 [ "//vendor:wasmtime" 152 , "//vendor:git2" 153 , "//vendor:aws-sdk-s3" 154 , "//vendor:ed25519-dalek" 155 ] 156 , embed = [ builtins_wasm, git_odb ] 157 , edition = Rust.Edition.2024 158 } 159 160 let straylight_cli = Rust.binary 161 { name = "straylight" 162 , main = "src/main.rs" 163 , deps = [ straylight_core ] 164 , targets = [ targets.native, targets.orin ] 165 } 166 167 in { straylight_cli, straylight_core, builtins_wasm } 168 ``` 169 170 ### No Globs 171 172 ```dhall 173 -- NO 174 srcs = glob "src/**/*.rs" 175 176 -- YES 177 srcs = 178 [ "src/lib.rs" 179 , "src/core/mod.rs" 180 , "src/core/store.rs" 181 , "src/core/artifact.rs" 182 ] 183 ``` 184 185 The CLI proposes, human approves: 186 187 ```bash 188 straylight srcs //mylib 189 190 # Found 3 new files not in BUILD.dhall: 191 # + src/core/namespace.rs 192 # + src/core/vm.rs 193 # + src/transport/git.rs 194 # 195 # Add them? [y/n/edit] 196 ``` 197 198 Every file in the build is a choice, not an accident. 199 200 ## Component 2: Typed Toolchains 201 202 Toolchains look complicated in Starlark. They aren't. 203 204 ``` 205 compiler + target + flags = toolchain 206 toolchain + sources + deps = build 207 build -> artifact -> hash 208 209 three lines. 210 ``` 211 212 ### Toolchain Types 213 214 ```dhall 215 -- https://straylight.cx/toolchains/v1.dhall 216 217 let Triple = 218 { arch : Arch 219 , vendor : Vendor 220 , os : OS 221 , abi : ABI 222 } 223 224 let Compiler = 225 < Clang : { version : Version, artifact : Artifact } 226 | Rustc : { version : Version, artifact : Artifact } 227 | GHC : { version : Version, artifact : Artifact } 228 | Lean : { version : Version, artifact : Artifact } 229 > 230 231 let Toolchain = 232 { compiler : Compiler 233 , host : Triple 234 , target : Triple 235 , flags : List Flag 236 , linker : Optional Artifact 237 , sysroot : Optional Artifact 238 } 239 ``` 240 241 ### Concrete Toolchains 242 243 ```dhall 244 let clang_18 = Compiler.Clang 245 { version = v "18.1.0" 246 , artifact = sha256:abc... 247 } 248 249 let rust_1_80 = Compiler.Rustc 250 { version = v "1.80.0" 251 , artifact = sha256:def... 252 } 253 254 let orin_sysroot = sha256:deadbeef... 255 256 let toolchains = 257 { native_rust = 258 { compiler = rust_1_80 259 , host = triples.x86_64_linux 260 , target = triples.x86_64_linux 261 , flags = [ Flag.TargetCpu Cpu.native ] 262 , linker = None Artifact 263 , sysroot = None Artifact 264 } 265 266 , orin_rust = 267 { compiler = rust_1_80 268 , host = triples.x86_64_linux 269 , target = triples.aarch64_linux 270 , flags = [ Flag.TargetCpu Cpu.cortex_a78ae ] 271 , linker = Some clang_18 272 , sysroot = Some orin_sysroot 273 } 274 275 , wasm_rust = 276 { compiler = rust_1_80 277 , host = triples.x86_64_linux 278 , target = triples.wasm32_wasi 279 , flags = [ Flag.OptLevel OptLevel.Oz ] 280 , linker = None Artifact 281 , sysroot = None Artifact 282 } 283 } 284 ``` 285 286 ### Typed Flags 287 288 ```dhall 289 let Flag = 290 < OptLevel : OptLevel 291 | TargetCpu : Cpu 292 | LTO : LTOMode 293 | Codegen : CodegenFlag 294 | Link : LinkFlag 295 | Debug : DebugInfo 296 | Feature : { enable : Bool, name : Text } 297 | Raw : Text -- escape hatch, logged + warned 298 > 299 300 let LTOMode = < Off | Thin | Fat > 301 ``` 302 303 Flags compose, validate, dedupe. Not strings. 304 305 ## Component 3: Target Types 306 307 ```dhall 308 -- https://straylight.cx/targets/v1.dhall 309 310 let Arch = < x86_64 | aarch64 | wasm32 | riscv64 > 311 312 let OS = < linux | darwin | wasi | none > 313 314 let Cpu = < generic 315 | cortex-a78ae -- orin 316 | neoverse-n1 -- graviton 317 | znver3 -- zen3 318 > 319 320 let Target = 321 { arch : Arch 322 , os : OS 323 , cpu : Cpu 324 , triple : Text -- derived, but explicit 325 } 326 327 let aarch64-linux = 328 \(cfg : { cpu : Cpu }) -> 329 { arch = Arch.aarch64 330 , os = OS.linux 331 , cpu = cfg.cpu 332 , triple = "aarch64-unknown-linux-gnu" 333 } : Target 334 335 let wasm32-wasi = 336 { arch = Arch.wasm32 337 , os = OS.wasi 338 , cpu = Cpu.generic 339 , triple = "wasm32-wasi" 340 } : Target 341 ``` 342 343 ## Component 4: Rust Object Model 344 345 Preludeless Rust in idiomatic Dhall. Useful for code generation, FFI bindings, 346 AST representation, and the stochastic_omega translation pipeline. 347 348 ```dhall 349 -- https://straylight.cx/lang/rust/v1.dhall 350 351 let Primitive = 352 < U8 | U16 | U32 | U64 | U128 | Usize 353 | I8 | I16 | I32 | I64 | I128 | Isize 354 | F32 | F64 355 | Bool 356 | Char 357 | Str 358 | Never 359 > 360 361 let Mutability = < Mut | Const > 362 363 let Lifetime = < Static | Named : Text | Elided > 364 365 let Type = 366 < Prim : Primitive 367 | Ref : { lifetime : Lifetime, mut : Mutability, inner : Type } 368 | Ptr : { mut : Mutability, inner : Type } 369 | Array : { inner : Type, len : Natural } 370 | Slice : { inner : Type } 371 | Tuple : List Type 372 | Fn : { args : List Type, ret : Type } 373 | Path : { segments : List Text, generics : List Type } 374 | Generic : Text 375 | Unit 376 > 377 378 let Struct = 379 < Unit : { name : Text } 380 | Tuple : { name : Text, fields : List Type } 381 | Fields : { name : Text, fields : List Field } 382 > 383 384 let Variant = 385 < Unit : Text 386 | Tuple : { name : Text, fields : List Type } 387 | Struct : { name : Text, fields : List Field } 388 > 389 390 let Enum = 391 { name : Text 392 , generics : List Generic 393 , variants : List Variant 394 } 395 396 let Fn = 397 { name : Text 398 , generics : List Generic 399 , params : List Param 400 , ret : Type 401 , vis : Visibility 402 , unsafe : Bool 403 , const : Bool 404 , async : Bool 405 , extern_abi : Optional ABI 406 } 407 408 let Trait = 409 { name : Text 410 , generics : List Generic 411 , supertraits: List TraitRef 412 , types : List AssocType 413 , methods : List TraitMethod 414 } 415 416 let Impl = 417 < Inherent : 418 { generics : List Generic 419 , self_ty : Type 420 , items : List ImplItem 421 } 422 | Trait : 423 { generics : List Generic 424 , trait_ : TraitRef 425 , self_ty : Type 426 , items : List ImplItem 427 } 428 > 429 430 let Crate = 431 { name : Text 432 , items : List Item 433 } 434 ``` 435 436 ### Usage: Define Option Without Prelude 437 438 ```dhall 439 let Rust = https://straylight.cx/lang/rust/v1.dhall sha256:... 440 441 let T = Rust.Generic { name = "T", bounds = [] : List Rust.Bound, default = None Rust.Type } 442 443 let Option = Rust.Enum 444 { name = "Option" 445 , generics = [ T ] 446 , variants = 447 [ Rust.Variant.Unit "None" 448 , Rust.Variant.Tuple { name = "Some", fields = [ Rust.Type.Generic "T" ] } 449 ] 450 } 451 ``` 452 453 Dhall IS the typed AST. The printer is one page. 454 455 ## Component 5: Storage Architecture 456 457 ### R2 is the Big Store in the Sky 458 459 Von Neumann's style - it won by economic necessity. R2 is: 460 461 - Cheap 462 - Free egress 463 - S3-compatible 464 - The obvious choice 465 466 ### Git for Attestation 467 468 Git can talk to the big store in the sky: 469 470 - Git stores attestation (small) 471 - R2 stores artifacts (big) 472 - Git references point to R2 objects 473 - ed25519 for signing 474 - ssh for transport 475 476 ### libgit2 ODB Backend 477 478 The libgit2 ODB backend for R2 is a one-shot if you can write it in 479 System Fomega or CIC. Correct by construction, write once, never touch again. 480 481 ``` 482 git objects -> sha256 -> r2 keys 483 git refs -> r2 metadata 484 git pack -> r2 multipart 485 ``` 486 487 ## Component 6: stochastic_omega 488 489 A Lean4 tactic. LLM-driven proof search constrained by `rfl` (reflexivity). 490 491 ``` 492 1. generate Dhall (typed, total) 493 2. typecheck (dhall) 494 3. emit Rust source (trivial printer) 495 4. compile (rustc) 496 5. test 497 6. if property fails -> refine Dhall 498 ``` 499 500 The type system is the oracle that accepts or rejects. Use probabilistic search 501 (LLM sampling) through the space of Fomega terms. 502 503 - "stochastic" = the droid's search is probabilistic/ML-driven 504 - "omega" = System Fomega, the type operator level of the lambda cube 505 506 **stochastic_omega is a Lean4 tactic. System Omega* is what it can do.** 507 508 ### The Degenerate Case 509 510 Lean compiles to certified C. The full pipeline: 511 512 1. stochastic_omega generates verified code 513 2. Lean4 compiles to C (certified extraction) 514 3. C compiles to native/wasm 515 4. The artifact is content-addressed 516 517 Proofs are erased after compilation - they were checked at compile time. 518 519 ### Roundtripping Through rfl 520 521 Put a droid in a loop trying to roundtrip PureScript's prelude through 522 rfl-carrying ASTs. If the AST carries proofs that transformations are 523 identity-preserving, and you iterate with LLM proposals + rfl verification, 524 you converge on proven transformations. 525 526 ## Component 7: The Language Coset 527 528 Same semantics, different tradeoffs: 529 530 ``` 531 PureScript <---> Haskell <---> Rust <---> Lean 532 | | | | 533 v v v v 534 bun GHC rustc lake 535 (fast) (native) (native) (C) 536 537 same logic. property tested against each other. 538 ``` 539 540 ### How Close is PureScript to Rust? 541 542 At the LLVM IR level, closer than you'd think. If both compile down to similar 543 LLVM IR, the high-level language differences become irrelevant for the artifact. 544 545 ### syn in Lean4 546 547 Can syn (Rust parser) be translated to Lean4? If syn existed in Lean4: 548 549 - Parse Rust source 550 - Verified parsing 551 - Round-trip through the proof system 552 - The Rust parser itself becomes part of the rfl nexus 553 554 This closes the loop. 555 556 ## Component 8: isospin microvm 557 558 A minimal VM for GPU workloads with a proven driver stack. 559 560 ### nvidia.ko is in-tree 561 562 NVIDIA open-sourced their kernel modules. nvidia.ko is now in the Linux kernel 563 tree (GPL dual licensed). This changes everything. 564 565 ### Hoisting the Driver to Lean 566 567 If you hoist the nvidia driver source into Lean: 568 569 1. Minimal VM with just enough for GPU workloads 570 2. Proven driver (Lean -> C) 571 3. Minimal kernel surface 572 4. True isolation (hypervisor, not namespaces) 573 574 ## The Straylight Cube 575 576 ``` 577 THE STRAYLIGHT CUBE 578 579 PROVEN (rfl) 580 | 581 | 582 Lean --------+-------- Liquid Haskell 583 | | | 584 | | | 585 TOTAL --+----------+------------- +-- ESCAPE 586 | | | 587 Dhall | PureScript 588 | | | 589 | | Haskell 590 | | | 591 +----------+------------- +--- Rust 592 | | 593 | | 594 stochastic_omega 595 (rfl oracle) 596 | 597 +------------+------------+ 598 | | 599 v v 600 WASM (portable) C (native/kernel) 601 | | 602 | | 603 +---------------+--------------------------+---------------+ 604 | | | | 605 | v v | 606 | +---------+ +-------------+ | 607 | |builtins | | isospin | | 608 | | .wasm | | (microvm) | | 609 | +----+----+ +------+------+ | 610 | | | | 611 | ISOLATION | | ISOLATION | 612 | (sandbox) | | (hypervisor) | 613 | | | | 614 | | +-- nvidia.ko | 615 | | | (proven) | 616 +--------------|------------------------|-----------------+ 617 | | 618 +-----------+------------+ 619 | 620 v 621 +------------+ 622 | DICE | 623 | | 624 | inputs | 625 | | | 626 | action | 627 | | | 628 | outputs | 629 +-----+------+ 630 | 631 v 632 +---------------------------------------+ 633 | ATOMS | 634 | | 635 | namespace -- vm -- build -- artifact | 636 | | | | | | 637 | +-------+-------+---------+ | 638 | | | 639 | store | 640 +------------------+--------------------+ 641 | 642 +------------+------------+ 643 | | | 644 v v v 645 +------+ +--------+ +---------+ 646 |sha256| | git | | r2 | 647 | | | | | | 648 | hash |<---|attest |-->| bytes | 649 +------+ +--------+ +---------+ 650 | 651 | 652 +----+----+ 653 | ed25519 | 654 | | 655 |identity | 656 +----+----+ 657 | 658 v 659 +---------+ 660 | ssh | 661 | | 662 |transport| 663 +---------+ 664 ``` 665 666 ## CLI Design 667 668 ```bash 669 # nix compat mode (training wheels) 670 straylight run nixpkgs#hello 671 straylight shell nixpkgs#rust 672 | 673 +-- translates to nix, uses nix store (for now) 674 675 # native mode 676 straylight build //mylib 677 straylight build //mylib:wasm 678 straylight test //mylib:test 679 680 # the schema nix run nixpkgs#program is inadequate 681 # (we will support it as a special case) 682 ``` 683 684 ## What's Left of Nix? 685 686 If we have: 687 688 1. PureNix for description (typed Fomega that compiles to Nix expressions) 689 2. builtins.wasm for evaluation (portable Nix evaluator) 690 3. wasm/firecracker for build isolation 691 4. git for content addressing 692 5. ed25519 for signing 693 6. ssh for transport 694 695 What's left of "Nix" as we know it? 696 697 - The DSL -> being replaced by typed languages 698 - The evaluator -> being replaced by builtins.wasm 699 - The daemon/store -> being replaced by r2 + git 700 - The sandbox -> being replaced by wasm/firecracker 701 702 **The answer: the protocol. The content-addressing scheme. The concept.** 703 704 ## Implementation Priorities 705 706 | Phase | Component | Status | 707 |-------|-----------|--------| 708 | 1 | CA derivations always-on | Complete (RFC-007) | 709 | 2 | builtins.wasm | Complete (RFC-007) | 710 | 3 | Typed package DSL | Complete (RFC-007) | 711 | 4 | Armitage witness proxy | **Complete** | 712 | 5 | Armitage OCI container (nix2gpu) | **Complete** | 713 | 6 | isospin TAP networking | **Complete** | 714 | 7 | NativeLink CAS integration | **Complete** (gRPC client, upload/download) | 715 | 8 | Armitage RE client | **Complete** (hand-rolled protobuf, Execute API) | 716 | 9 | Buck2 minimal prelude | **Complete** (~5.6k LOC, 57 modules) | 717 | 10 | DICE reference (Rust) | **Complete** (Meta's DICE, 36k LOC, benchmarks run) | 718 | 11 | Armitage DICE (Haskell) | **In Progress** (~1k LOC core) | 719 | 12 | tvix-eval integration | **Evaluation** (nixpkgs-compat, not bug-for-bug) | 720 | 13 | Graded monad executor | Design | 721 | 14 | Dhall rule schemas | Draft | 722 | 15 | R2 store backend | Planned | 723 | 16 | Lean proof discharge | Research | 724 | 17 | stochastic_omega tactic | Research | 725 726 ### Current Implementation Stats 727 728 ``` 729 aleph/ 730 ├── src/armitage/ 7.7k LOC Haskell 731 │ ├── DICE.hs 975 LOC - incremental computation core 732 │ ├── Proto.hs 910 LOC - hand-rolled RE protobuf 733 │ ├── Proxy.hs 890 LOC - witness proxy 734 │ ├── Dhall.hs 742 LOC - BUILD.dhall evaluation 735 │ ├── RE.hs 663 LOC - remote execution client 736 │ ├── Builder.hs 583 LOC - build orchestration 737 │ ├── Trace.hs 518 LOC - execution traces 738 │ ├── Nix.hs 499 LOC - nix compatibility 739 │ ├── CAS.hs 380 LOC - content-addressed storage 740 │ ├── Store.hs 348 LOC - artifact store 741 │ └── Toolchain.hs 317 LOC - toolchain management 742 │ 743 ├── src/dice-rs/ 36.1k LOC Rust (Meta's DICE, ported) 744 │ ├── dice/ 19.2k LOC - core engine 745 │ ├── allocative/ 4.1k LOC - memory profiling 746 │ ├── dice_futures/ 2.4k LOC - async/cancellation 747 │ └── ...support crates 748 │ 749 └── prelude/ 5.6k LOC Starlark (minimal Buck2 prelude) 750 └── 57 modules (haskell, cxx, linking, platforms, etc.) 751 ``` 752 753 ### External Dependencies 754 755 | Component | Source | Status | Notes | 756 |-----------|--------|--------|-------| 757 | Buck2 | Meta | Nix flake input | Hermetic Rust/Haskell toolchains | 758 | NativeLink | TraceMachina | Nix flake input | RE backend (Fly.io deployment) | 759 | tvix-eval | TVL | **Evaluating** | ~16k LOC, nixpkgs-compat | 760 | tvix nix-compat | TVL | **Usable** | ~2k LOC, derivation hashing | 761 | rnix-parser | nix-community | Via tvix | AST parsing | 762 763 ### The Nix Escape Plan 764 765 ``` 766 Current: Nix lang → nix-daemon → /nix/store 767 ──────────────────────────────────── 768 Phase 1: Nix lang → armitage → NativeLink CAS ← WE ARE HERE 769 (tvix-eval) (witness) 770 ──────────────────────────────────── 771 Phase 2: Dhall → armitage → NativeLink CAS 772 (typed) (DICE) 773 ──────────────────────────────────── 774 Phase 3: Dhall → DICE → R2 + git 775 (no nix evaluator in path) 776 ``` 777 778 ## Component Index 779 780 | Document | Description | 781 |----------|-------------| 782 | [README.md](README.md) | This document - overview | 783 | [armitage.md](armitage.md) | Nix compatibility layer, coeffects, graded monad execution | 784 | [dhall-bridge.md](dhall-bridge.md) | Dhall → Buck2 translation options | 785 | [ROADMAP.md](ROADMAP.md) | Timeline and milestones | 786 787 ## tvix: The Clean Nix Implementation 788 789 For temporary Nix language compatibility, we use [tvix](https://tvix.dev/) components: 790 791 ### Why tvix, not C++ Nix 792 793 | Aspect | C++ Nix | tvix | 794 |--------|---------|------| 795 | Language | C++ | Rust | 796 | Architecture | Monolithic daemon | Modular crates | 797 | Store coupling | Eval ↔ Store tightly coupled | Eval independent of store | 798 | Bug compatibility | THE bugs | nixpkgs-compatible only | 799 | Codebase | ~100k LOC | ~16k LOC (eval) | 800 801 ### tvix Components We Use 802 803 ``` 804 tvix/ 805 ├── eval/ 16k LOC - Nix language evaluator (bytecode VM) 806 │ ├── compiler/ 3k LOC - AST → bytecode 807 │ ├── vm/ 2k LOC - 52 opcodes 808 │ ├── value/ 4k LOC - runtime values 809 │ └── builtins/ 2k LOC - 80 builtins 810 │ 811 ├── nix-compat/ 2k LOC - Derivation hashing, NAR, store paths 812 │ ├── derivation/ 308 LOC - THE important part 813 │ └── store_path/ 500 LOC - hash calculations 814 │ 815 └── simstore/ - Dummy store for eval-only 816 ``` 817 818 ### What tvix Gets Right 819 820 1. **Separation of concerns**: eval doesn't need a store to run 821 2. **`hashDerivationModulo`**: correctly implemented in 50 lines 822 3. **Not bug-for-bug**: only replicates behavior nixpkgs needs 823 4. **Content-addressed from the start**: no legacy input-addressed paths 824 825 ### What We Skip 826 827 | Component | Why Skip | 828 |-----------|----------| 829 | tvix-build | We have armitage | 830 | tvix-store | We use NativeLink CAS | 831 | nix-daemon compat | We don't want daemon protocol | 832 | Flakes | Flakes are a mistake | 833 834 ### Integration Path 835 836 ```haskell 837 -- Option 1: FFI to tvix-eval 838 evalNix :: Text -> IO (Either Error NixValue) 839 evalNix expr = withTvixEval $ \eval -> do 840 result <- tvix_eval_expr eval expr 841 marshalValue result 842 843 -- Option 2: Port nix-compat to Haskell (~800 LOC) 844 hashDerivationModulo :: Derivation -> (StorePath -> Digest) -> Digest 845 hashDerivationModulo drv lookupDep = ... 846 ``` 847 848 The key insight: we only need `nix-compat` (~2k LOC) long-term. 849 The evaluator is temporary until Dhall replaces Nix lang. 850 851 ## Bucket Layout 852 853 All witnessed builds store artifacts in a unified content-addressed bucket: 854 855 ``` 856 r2.straylight.cx/ 857 ├── specs/ # Build computations (Lean/Dhall) 858 │ └── {hash}.lean 859 ├── traces/ # Execution traces (CBOR) 860 │ └── {hash}.cbor 861 ├── cas/ # Content-addressed blobs (outputs + fetches) 862 │ └── {hash} 863 ├── proofs/ # Compiled Lean discharge proofs 864 │ └── {hash}.olean 865 └── attestations/ # Signed attestations 866 └── {hash}.json 867 ``` 868 869 The proxy is both **witness** (records fetches) and **substitutor** (serves 870 cached content). Same infrastructure, two modes. 871 872 ## Infrastructure 873 874 | Service | Domain | Purpose | 875 |---------|--------|---------| 876 | DNS | ns1.straylight.cx | Dynamic DNS from attestation store | 877 | Resolver | resolve.straylight.cx | Name → CAS redirect for `nix run` | 878 | CAS | cas.straylight.cx | NativeLink gRPC endpoint | 879 | Storage | r2.straylight.cx | Cloudflare R2 (S3-compatible) | 880 | Git | git.straylight.cx | Attestation repository | 881 882 ## Naming 883 884 ``` 885 ca://sha256:abc... # content-addressed (sovereign) 886 att://straylight.cx/llvm@18 # attested package 887 nix://nixpkgs#hello # legacy compat (via registry redirect) 888 ``` 889 890 ## References 891 892 - RFC-007: Nix Formalization 893 - [Dhall Language](https://dhall-lang.org/) 894 - [Buck2](https://buck2.build/) 895 - [Firecracker](https://firecracker-microvm.github.io/) 896 - [Cloudflare R2](https://developers.cloudflare.com/r2/) 897 - [Lean4](https://lean-lang.org/) 898 - [libgit2](https://libgit2.org/) 899 - Petricek et al., "Coeffects: A calculus of context-dependent computation" 900 - Orchard et al., "Quantitative Type Theory"