Module codegen 

Code generation from LOGOS AST to Rust source code.

This module transforms the parsed and type-checked LOGOS program into idiomatic Rust code. The generated code uses logicaffeine_data types for runtime values and integrates with the kernel for proof verification.

Pipeline Position

┌─────────────────────────────────────────────────────────┐
│  LOGOS Source → Lexer → Parser → AST → Analysis → HERE │
└─────────────────────────────────────────────────────────┘
                                                     ↓
                                              Rust Source

Code Generation Rules

LOGOS Statement	Rust Output
Let x be 5.	let x = 5;
Set x to 10.	x = 10;
Give x to y.	let y = x; (move)
Show x to show.	println!("{}", x);
If x > 0 then...	if x > 0 { ... }
Repeat while x > 0...	while x > 0 { ... }
Zone "name"...	{ /* zone scope */ }
Mount x at "path".	x.mount(vfs, "path").await;
Sync x on "topic".	x.subscribe("topic").await;

Key Features

• Refinement Types: Generates debug_assert! for type predicates
• Policy Enforcement: Emits capability checks for access control
• Zone Safety: Translates memory zones to Rust scopes
• CRDT Mutability: Uses .set() for LWWRegister/MVRegister fields
• Async Detection: Adds #[tokio::main] when async operations are present
• VFS Detection: Injects get_platform_vfs() for file operations (io_uring on Linux, NativeVfs elsewhere)
• Mount+Sync Detection: Uses Distributed<T> for combined persistence/sync

Refinement Context

The RefinementContext tracks type predicates across scopes:

Let x: { it: Int | it > 0 } be 5.   ←  Register constraint
     ↓
debug_assert!(5 > 0);               ←  Check at definition
     ↓
Set x to 10.                        ←  Re-check on mutation
     ↓
debug_assert!(10 > 0);              ←  Re-emit assertion

• When a variable with a refinement type is defined, its constraint is registered
• When that variable is mutated, the assertion is re-emitted
• Variable types are tracked for capability resolution

Entry Point

The main entry point is codegen_program, which generates a complete Rust program from a list of statements.

Structs

RefinementContext

Tracks refinement type constraints across scopes for mutation enforcement.

VariableCapabilities

Tracks which variables have Mount and/or Sync statements.

Functions

codegen_assertion

Converts a LogicExpr to a Rust boolean expression for debug_assert!(). Uses RustFormatter to unify all logic-to-Rust translation.

codegen_expr

codegen_native_tier_export

Emit the AOT-native export shim (HOTSWAP §Axis-3): a thin #[no_mangle] extern "C" calling-convention wrapper over the inner Rust fn that crosses our ACTUAL values — scalars BY VALUE — with NO CString/handle marshaling (unlike [codegen_c_export_with_marshaling]). The interpreter marshals VM Values to these scalar args, calls the loaded symbol, and re-boxes the scalar result.

codegen_program

codegen_program_mapped

Like codegen_program, but also builds the rustc→LOGOS SourceMap: every generated line maps to the top-level statement that produced it (stmt_spans is the parser’s side-table, 1:1 with stmts; zero-width spans mark prelude statements and are skipped), and variable origins carry ownership roles for the diagnostic bridge. This is the flycheck substrate.

codegen_program_with_proven

Like codegen_program, but bundles an extracted math/logic module into the output. proven is the body of a Rust module — functions, check_* property fns, a World/holds model-checker — produced by the Forge’s extraction with NO fn main. It is emitted as pub mod <module_name> { … } right after the prelude (before user_types), followed by use <module_name>::*; so a bare call in the imperative program below — e.g. double(21) — resolves into it. Naming the module (rather than dumping items at crate root) keeps multiple proven modules reachable and avoids polluting the imperative namespace. When proven is None/blank the output is byte-identical to codegen_program.

codegen_stmt

codegen_term

collect_async_functions

Phase 54: Collect function names that are async. Used by LaunchTask codegen to determine if .await is needed.

collect_pipe_sender_params

collect_pipe_vars

Phase 54: Collect variables that are pipe declarations (created with CreatePipe). These have _tx/_rx suffixes, while pipe parameters don’t.

empty_var_caps

Helper to create an empty VariableCapabilities map (for tests).

force_disable_borrow_hoist_for_test

Force borrow hoisting off (or back on) for the current thread only. Used by tests to verify the kill switch without the env-var data race.

function_slice

The statements needed to compile target standalone: the target function plus every function reachable from it through the call graph (transitively). Main and top-level functions unreachable from target are dropped; definition order is preserved.

generate_c_header

Generate the C header (.h) content for all C-exported functions.

generate_python_bindings

Generate Python ctypes bindings for all C-exported functions.

generate_typescript_bindings

Generate TypeScript type declarations (.d.ts) and FFI bindings (.js).

with_seeded_select

Run f with Mode-B Select lowering enabled, restoring the previous mode afterwards (panic-safe). Returns f’s result.