Causm

A Domain-Specific Language for Temporal and Entropic Memory Models

Important

Causm is an experimental toolchain for exploring temporal and entropic memory models. Specifications and implementation are subject to changes.

---

Causm is a domain-specific research language designed to address inherent non-determinism in concurrent systems. By treating time as a first-class execution primitive and implementing an entropic memory model, Causm provides a framework where race conditions are eliminated through the mathematical enforcement of temporal invariants.

This repository contains the reference implementation of the Causm toolchain, including the compiler, entropic analyzer, and Z3-governed Register-based Temporal Virtual Machine (TVM).

---

Research Objectives

1. Temporal Execution Primitives: Eliminating race conditions via Isochronous Scheduling.
2. Entropic Memory Model: Modeling memory safety through state decay (Valid, Leased, Decayed, Consumed, Pending).
3. Causal Synchronization: Synchronizing cross-timeline state transitions without lock contention.
4. SMT-Based Temporal Correctness: Formally proving Worst-Case Execution Time (WCET) bounds using a Z3 correctness kernel.

---

Architecture

graph TD
    Source[".csm Source Code"] --> Parser["Causm Parser (Pest)"]
    Parser --> AST["Abstract Syntax Tree"]

    subgraph "Correctness Kernel"
        AST --> Analyzer["Entropic Analyzer"]
        Analyzer --> Z3Guard["Formal Verification Guard (Z3)"]
        Z3Guard --> Proofs{{"Symbolic Proofs + WCET Bounds"}}
    end

    Proofs -- "UNSAT (Violation)" --> Error["Semantic Error"]
    Proofs -- "SAT (Safe)" --> Lowering["IR Lowering"]

    subgraph "IR Optimization Pipeline"
        Lowering --> CfgSimp["CfgSimplificationPass"]
        CfgSimp --> ChanLive["ChannelLivenessPass"]
        ChanLive --> LeaseOpt["LeaseOptimizationPass"]
        LeaseOpt --> ConcurAn["ConcurrencyAnalysisPass"]
        ConcurAn --> Verifier["VerifierPass (SSA Phi)"]
    end

    Verifier --> TVM["Register-based TVM"]

Loading

---

Code Example

@0ms: {
    isolate main_system {
        enable cpu(5000ms)
        require System.Log

        from "module_sensor_lib.csm" import compute_telemetry_digest

        let raw_reading = 150
        let ref_reading = &raw_reading

        let digest = call compute_telemetry_digest(raw_reading)
        let sensor_pack = struct { status = "active", level = digest }

        lease current_pack = sensor_pack 30ms {
            let active_level = current_pack.level
            print(active_level)
        } reconcile auto

        match entropy(raw_reading) {
            Valid(v) if v == 150: { print("High Precision Match") }
            Consumed: { print("Consumed") }
        }
    }
}

---

Documentation

See the Full Documentation Hub for complete specifications.

• Specifications (docs/spec/): Syntax, Semantics, Types, Modules & Imports, OOP, Leases, Verification Guard
• TVM Internals (docs/tvm/): TVM Optimizations, Acausal Debugging, Memory Reclamation
• Proposals & RFCs (docs/proposals/): Module System Proposal

---

Getting Started & Execution

# Analyze and run a source file
causm run examples/module_import_showcase.csm

# Run with timeline merge diagnostics
causm run --explain-merge examples/module_import_showcase.csm

# Perform formal Z3 verification check only
causm check examples/module_import_showcase.csm

# Emit intermediate representations (AST, IR, CFG, SSA)
causm emit examples/module_import_showcase.csm --emit cfg-dot

---

License

Licensed under the GNU Affero General Public License v3.0 (AGPL-3.0). See LICENSE.

---

Built with 🦀 & ⏳ by Seuriin