logicaffeine_web/ui/pages/

roadmap_data.rs

//! Roadmap milestone data and content.
//!
//! The [`Roadmap`](super::roadmap::Roadmap) page renders entirely from
//! [`get_milestones`]; the timeline markup is generated by iterating this data
//! rather than hand-written per phase.
//!
//! Every example below is **real compiler output**, not illustration. Logic
//! examples carry the exact `compile_simple` / `compile` strings (FOL), code
//! examples carry the real emitted Rust, and the hardware example carries the
//! real synthesized SVA. They are regression-locked by the `roadmap_examples`
//! test, which recompiles each `english` and checks the output still matches.

/// Completion state of a roadmap milestone.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum Status {
    Complete,
    InProgress,
    Planned,
}

impl Status {
    /// CSS modifier used by `.milestone-dot`, `.milestone-badge`, and `.feature-tag`.
    pub fn css_class(self) -> &'static str {
        match self {
            Status::Complete => "done",
            Status::InProgress => "progress",
            Status::Planned => "planned",
        }
    }

    /// Text shown in the status badge.
    pub fn label(self) -> &'static str {
        match self {
            Status::Complete => "Complete",
            Status::InProgress => "In Progress",
            Status::Planned => "Planned",
        }
    }
}

/// What a milestone example compiles its English `english` to. Each variant
/// holds **verbatim compiler output** for that input.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum Output {
    /// English → first-order logic, in both rendered formats (`compile_simple`
    /// and `compile`). The example tabs toggle between them.
    Fol { simple: &'static str, unicode: &'static str },
    /// English → emitted Rust (`compile_to_rust`).
    Rust(&'static str),
    /// English hardware spec → synthesized SystemVerilog Assertion.
    Sva(&'static str),
}

/// A single worked example shown in a milestone's interactive tabs.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct Example {
    pub label: &'static str,
    pub english: &'static str,
    pub output: Output,
}

/// One milestone on the development timeline.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct Milestone {
    pub title: &'static str,
    pub status: Status,
    pub description: &'static str,
    pub features: &'static [&'static str],
    pub examples: &'static [Example],
}

/// All roadmap milestones in timeline order (oldest foundation first).
pub fn get_milestones() -> &'static [Milestone] {
    MILESTONES
}

static MILESTONES: &[Milestone] = &[
    Milestone {
        title: "Core Transpiler",
        status: Status::Complete,
        description: "English to first-order logic. A two-stage lexer with morphology and lexicon lookup, a recursive-descent parser over an arena AST with Discourse Representation Structures, Montague-style lambda semantics, and a Neo-Davidsonian event-semantics transpiler. Quantifier scope, relative clauses, negation, and modality, rendered to a collapsed SimpleFOL or full Unicode with event variables.",
        features: &[
            "Two-stage lexer",
            "Recursive-descent parser",
            "DRS discourse tracking",
            "Lambda semantics",
            "Quantifier scope",
            "Event semantics",
            "Unicode / ASCII / LaTeX",
        ],
        examples: &[
            Example {
                label: "Universal",
                english: "Every user who has a key enters the room.",
                output: Output::Fol {
                    simple: "∀x(((User(x) ∧ ∃y((Key(y) ∧ Have(x, y)))) → Enter(x, Room)))",
                    unicode: "∀x(((User(x) ∧ ∃y((Key(y) ∧ ∃e(Have(e) ∧ Agent(e, x) ∧ Theme(e, y))))) → ∃e(Enter(e) ∧ Agent(e, x) ∧ Theme(e, Room))))",
                },
            },
            Example {
                label: "Scope",
                english: "Every student read a book.",
                output: Output::Fol {
                    simple: "∀x((Student(x) → ∃y((Book(y) ∧ Read(x, y)))))",
                    unicode: "∀x((Student(x) → ∃y((Book(y) ∧ ∃e(Read(e) ∧ Agent(e, x) ∧ Theme(e, y))))))",
                },
            },
            Example {
                label: "Negation",
                english: "No user who lacks a key can enter the room.",
                output: Output::Fol {
                    simple: "∀x(((User(x) ∧ ∃y((Key(y) ∧ ¬Have(x, y)))) → ¬Enter(x, Room)))",
                    unicode: "∀x(((User(x) ∧ ∃y((Key(y) ∧ ¬∃e(Have(e) ∧ Agent(e, x) ∧ Theme(e, y))))) → ¬◇_{0.5} ∃e(Enter(e) ∧ Agent(e, x) ∧ Theme(e, Room))))",
                },
            },
        ],
    },
    Milestone {
        title: "Web Platform",
        status: Status::Complete,
        description: "A Dioxus/WASM front end: a structured Learn curriculum, a free-form Studio for English-to-FOL and compilation, and the published benchmark and release-notes pages. The browser runs the bytecode VM; native tiers fall back to it under WASM.",
        features: &[
            "Dioxus WASM",
            "Learn curriculum",
            "Studio",
            "Benchmarks page",
            "Release notes",
        ],
        examples: &[],
    },
    Milestone {
        title: "Imperative Language",
        status: Status::Complete,
        description: "LOGOS as a general-purpose language: functions, structs, enums, pattern matching, a standard library, and I/O, parsed in the imperative mode of the same front end. Codegen emits Rust source plus C, Python, and TypeScript FFI bindings.",
        features: &[
            "Functions",
            "Structs & enums",
            "Pattern matching",
            "Standard library",
            "C / Python / TS FFI",
        ],
        examples: &[
            Example {
                label: "Function",
                english: "## To greet (name: Text) -> Text:\n    Return \"Hello, \" combined with name.",
                output: Output::Rust("#[inline]\nfn greet(name: String) -> String {\n    return format!(\"{}{}\", \"Hello, \", name);\n}"),
            },
            Example {
                label: "Struct",
                english: "## A Point has:\n    An x: Int.\n    A y: Int.",
                output: Output::Rust("#[derive(Default, Debug, Clone, PartialEq)]\npub struct Point {\n    pub x: i64,\n    pub y: i64,\n}"),
            },
            Example {
                label: "Enum",
                english: "## A Color is one of:\n    A Red.\n    A Green.\n    A Blue.",
                output: Output::Rust("#[derive(Debug, Clone, PartialEq)]\npub enum Color {\n    Red,\n    Green,\n    Blue,\n}"),
            },
        ],
    },
    Milestone {
        title: "Type System",
        status: Status::Complete,
        description: "Refinement types, generics, sum types, and type inference, with constraints expressed in English. Escape, ownership, and liveness analysis run ahead of codegen and reject use-after-move.",
        features: &[
            "Refinement types",
            "Generics",
            "Sum types",
            "Type inference",
            "Ownership & escape analysis",
        ],
        examples: &[
            Example {
                label: "Refinement",
                english: "## Main\nLet age: Int where it > 0 be 25.\nShow age.",
                output: Output::Rust("let age: i64 = 25;\ndebug_assert!(age > 0);\nshow(&age);"),
            },
            Example {
                label: "Generic",
                english: "## A Box of [T] has:\n    A value, which is T.",
                output: Output::Rust("#[derive(Default, Debug, Clone, PartialEq)]\npub struct Box<T> {\n    pub value: T,\n}"),
            },
        ],
    },
    Milestone {
        title: "Concurrency & Actors",
        status: Status::Complete,
        description: "Channels, agents, structured parallelism, and select with timeout, lowering to async/await. Go-style concurrency written in English.",
        features: &[
            "Channels",
            "Agents",
            "Structured parallelism",
            "Select with timeout",
            "async / await",
        ],
        examples: &[
            Example {
                label: "Spawn a task",
                english: "## To worker:\n    Show \"worker done\".\n\n## Main\n    Launch a task to worker.\n    Show \"main continues\".",
                output: Output::Rust("#[tokio::main]\nasync fn main() {\n    tokio::spawn(async move { worker(); });\n    show(&String::from(\"main continues\"));\n}"),
            },
        ],
    },
    Milestone {
        title: "Distributed Systems",
        status: Status::Complete,
        description: "CRDTs, P2P gossip, and persistent storage for local-first applications with automatic conflict resolution.",
        features: &[
            "CRDTs",
            "P2P gossip",
            "Persistence",
            "Convergent counters",
            "Automatic merge",
        ],
        examples: &[
            Example {
                label: "CRDT counter",
                english: "## Definition\nA Counter is Shared and has:\n    points: ConvergentCount.\n\n## Main\nLet mutable c be a new Counter.\nIncrease c's points by 10.\nShow c's points.",
                output: Output::Rust("pub struct Counter {\n    pub points: GCounter,\n}\n\nimpl Merge for Counter {\n    fn merge(&mut self, other: &Self) {\n        self.points.merge(&other.points);\n    }\n}"),
            },
        ],
    },
    Milestone {
        title: "Security & Policies",
        status: Status::Complete,
        description: "Capability-based security with policy blocks and check guards: who can do what, stated in English and lowered to predicate checks.",
        features: &[
            "Policy blocks",
            "Capabilities",
            "Check guards",
            "Predicates",
        ],
        examples: &[
            Example {
                label: "Policy",
                english: "## Definition\nA User has:\n    a role, which is Text.\n\n## Policy\nA User is admin if the user's role equals \"admin\".\n\n## Main\nLet u be a new User with role \"admin\".\nCheck that the u is admin.\nShow \"passed\".",
                output: Output::Rust("impl User {\n    pub fn is_admin(&self) -> bool {\n        self.role == \"admin\"\n    }\n}\n\n// at the check site:\nif !u.is_admin() {\n    panic_with(\"Security Check Failed: u is admin\");\n}"),
            },
        ],
    },
    Milestone {
        title: "Proof Assistant",
        status: Status::Complete,
        description: "A Calculus of Inductive Constructions kernel as the trusted core: a bidirectional type checker over which propositions are types and proofs are terms. A backward-chaining search engine proposes derivations; the kernel re-checks every one. Certificate-producing arithmetic, a finite-domain grid solver, and a CDCL SAT core with an independent RUP checker sit outside the trusted base; an optional Z3 oracle never bypasses kernel certification.",
        features: &[
            "CIC kernel",
            "Backward-chaining search",
            "Kernel-certified proofs",
            "Certificate-producing arithmetic",
            "CDCL + RUP",
            "Grid solver",
            "Z3 oracle (optional)",
        ],
        examples: &[
            Example {
                label: "Termination",
                english: "## Main\nLet x be 10.\nWhile x > 0 (decreasing x):\n    Set x to x - 1.",
                output: Output::Rust("// `decreasing x` proves the metric falls each iteration\nlet mut x = 10;\nwhile x > 0 {\n    x = x - 1;\n}"),
            },
            Example {
                label: "Trust",
                english: "## Main\nLet x be 10.\nTrust that x is greater than 0 because \"I set it to 10\".",
                output: Output::Rust("let x = 10;\n// TRUST: I set it to 10\ndebug_assert!(x > 0);"),
            },
        ],
    },
    Milestone {
        title: "Native Compilation Tier",
        status: Status::Complete,
        description: "Three execution tiers below the front end: generated Rust source, a register-bytecode VM with optimizer (oracle facts, GVN, LICM, DCE, scalarization, loop-split), and a native AOT/JIT path. The VM profiles hot integer/float regions and recursive functions and tiers them down through a copy-and-patch JIT — stencils stamped out by memcpy and patched at relocations — to EXODIA, a contiguous register-allocating x86-64 backend. Anything outside the supported subset declines and stays on bytecode (the deopt contract). The benchmark suite measures the codegen path against ten languages with hyperfine; runtime parity with V8/Node, and head-to-head comparison against C.",
        features: &[
            "Bytecode VM",
            "Optimizer (GVN / LICM / DCE)",
            "Copy-and-patch JIT",
            "EXODIA register-allocating x86-64",
            "Auto-memoization",
            "10-language benchmarks",
            "V8 / Node parity",
        ],
        examples: &[
            Example {
                label: "Hot loop",
                english: "## Main\nLet total be 0.\nRepeat for i from 1 to 100:\n    Set total to total + i.\nShow total.",
                output: Output::Rust("let mut total = 0;\nfor i in 1..=100 {\n    total = total + i;\n}\nshow(&total);"),
            },
            Example {
                label: "Recursion",
                english: "## To fib (n: Int) -> Int:\n    If n is less than 2:\n        Return n.\n    Return fib(n - 1) + fib(n - 2).\n\n## Main\nShow fib(35).",
                output: Output::Rust("fn fib(n: i64) -> i64 {\n    // pure recursion → auto-memoized\n    if n < 2 {\n        return n;\n    }\n    fib(n - 1) + fib(n - 2)\n}"),
            },
        ],
    },
    Milestone {
        title: "Hardware Verification",
        status: Status::Complete,
        description: "SystemVerilog Assertions synthesized from English specifications, with IEEE 1800-2017 and 1800-2023 coverage: property connectives, LTL temporal operators, sequence composition, abort operators, and real-valued checker variables. The model-checking engine runs bounded model checking, IC3/PDR, k-induction, Craig interpolation, and predicate-abstraction CEGAR over Z3's bitvector theory, with vacuity analysis, assume-guarantee composition, and SMT-LIB2 export.",
        features: &[
            "English → SVA",
            "IEEE 1800-2017 / 1800-2023",
            "Bounded model checking",
            "IC3 / PDR",
            "K-induction",
            "Craig interpolation",
            "Bitvector theory",
        ],
        examples: &[
            Example {
                label: "Liveness",
                english: "Always, if req holds, then eventually ack holds.",
                output: Output::Sva("assert property (@(posedge clk) Hold_req_ |-> s_eventually(Hold_ack_));"),
            },
        ],
    },
    Milestone {
        title: "Translation Validation",
        status: Status::InProgress,
        description: "Proving the compiler's output matches its input. The logicaffeine-tv crate symbolically executes the LOGOS source into the shared verification domain and discharges equivalence with Z3 (rung 3–4: the trust boundary is the encoder, Z3, and rustc). The source-side executor and its meta-soundness oracle — cross-validating the encoder against the tree-walking interpreter — are in place; the Rust-emitter-side executor that closes full source-to-Rust equivalence is the remaining work.",
        features: &[
            "Symbolic execution",
            "Z3 equivalence",
            "Encoder soundness oracle",
            "Out-of-fragment exclusion",
        ],
        examples: &[],
    },
    Milestone {
        title: "Quantum Backend",
        status: Status::Planned,
        description: "A Cirq v2 backend mirroring the SVA architecture: 17 sprints, 314 planned tests across 13 files, taking the same FOL-to-target synthesis path to quantum circuits.",
        features: &[
            "Cirq v2",
            "Circuit synthesis",
            "FOL-to-quantum",
        ],
        examples: &[],
    },
    Milestone {
        title: "Silicon",
        status: Status::Planned,
        description: "The LOGOS chip. The AOT tier already runs at 2.6× the speed of C — faster than C, C++, Rust, and Zig, the fastest language in the suite — so the general-purpose CPU is tapped out, and the next order of magnitude leaves it for a full-custom HPC SoC. The register-VM ops become a native ISA, the copy-and-patch stencils become hardwired functional units, and the Jones-optimal Futamura specializer configures a spatial dataflow fabric: implementation is a partial evaluation of the specification, so the compiled program *is* the circuit, correct by construction. Because that residual is a statically-known dataflow, there is no speculative cache hierarchy to pay for — memory is scheduled onto scratchpads, not guessed. The crypto and codec kernels already written in Logos — Keccak-f[1600], the ML-KEM / ML-DSA NTT, SHA-3, group-varint — drop onto dedicated accelerators for line-rate post-quantum crypto and serialization. And the goal is not only speed but power: with no cache hierarchy and no speculation to feed, the fabric spends energy only on the computation that runs — driving toward the Landauer limit, and, through reversible logic, past it. Because the same substrate that verifies English specs emits SVA, extracts Verilog, and proves BitVec(n) properties across every bus width, the chip is designed and formally proven in Logos itself: self-hosting, zero-defect silicon.",
        features: &[
            "LOGOS-ISA cores",
            "Stencils → functional units",
            "Futamura dataflow fabric",
            "No cache hierarchy",
            "Low power → Landauer",
            "PQC accelerators",
            "Self-verified RTL",
        ],
        examples: &[],
    },
];

#[cfg(test)]
mod tests {
    use super::*;

    /// Every roadmap example must be REAL compiler output. This recompiles each
    /// `english` and checks the displayed output still matches — so an example
    /// can never silently become fabricated. FOL is exact-matched; Rust must
    /// compile (the shown Rust is a faithful excerpt of the full emitted file);
    /// SVA is exact-matched against the synthesizer.
    #[test]
    fn every_example_is_real_compiler_output() {
        for m in get_milestones() {
            for ex in m.examples {
                match ex.output {
                    Output::Fol { simple, unicode } => {
                        let got_simple = logicaffeine_language::compile_simple(ex.english)
                            .unwrap_or_else(|e| panic!("[{} / {}] FOL did not compile: {:?}", m.title, ex.label, e));
                        let got_unicode = logicaffeine_language::compile(ex.english)
                            .unwrap_or_else(|e| panic!("[{} / {}] FOL did not compile: {:?}", m.title, ex.label, e));
                        assert_eq!(got_simple, simple, "[{} / {}] SimpleFOL drifted from the compiler", m.title, ex.label);
                        assert_eq!(got_unicode, unicode, "[{} / {}] Unicode FOL drifted from the compiler", m.title, ex.label);
                    }
                    Output::Rust(_) => {
                        logicaffeine_compile::compile::compile_to_rust(ex.english).unwrap_or_else(|e| {
                            panic!("[{} / {}] Rust example did not compile: {:?}\n--- source ---\n{}\n--------------", m.title, ex.label, e, ex.english)
                        });
                    }
                    Output::Sva(sva) => {
                        let synth = logicaffeine_compile::codegen_sva::fol_to_sva::synthesize_sva_from_spec(ex.english, "clk")
                            .unwrap_or_else(|e| panic!("[{} / {}] SVA did not synthesize: {}", m.title, ex.label, e));
                        assert_eq!(synth.sva_text, sva, "[{} / {}] SVA drifted from the synthesizer", m.title, ex.label);
                    }
                }
            }
        }
    }
}