Skip to content

instruction.md

Latest commit

 

History

History
351 lines (254 loc) · 20.4 KB

instruction.md

File metadata and controls

351 lines (254 loc) · 20.4 KB
Raw

Here is the English version of your instruction.md. It has been translated to maintain the authoritative, "blacksmithing-inspired" tone of the Mumei project.

📜 instruction.md

1. Role and Purpose of Mumei

Mumei is a protocol designed to transform the uncertain code generated by AI agents (the result of "probabilistic inference") into verified, reliable assets. Developers and AI agents must define Immutable Truths (requires/ensures) before writing any algorithmic logic.

2. Syntactic Rules

2.1 Basic Structure of an Atom

All logic must be encapsulated within an atom.

  • requires: Conditions that must be satisfied before execution.
  • ensures: Outcomes that are guaranteed after execution. Use result == expr for precise equality propagation across chained calls.
  • body: The implementation of the algorithm. Using {} block syntax and let variable bindings is highly recommended.
  • consume: Declares ownership transfer. consume x; marks parameter x as consumed — it cannot be used after the atom returns.
  • ref: Declares read-only borrowing. ref v: T allows access without taking ownership. The owner cannot consume during the borrow.

2.2 Ironclad Rules for Control Flow

  • if-else: An else block must always be included to ensure mathematical totality (exhaustiveness).
  • let: Variables must be treated as immutable. Re-assignment is not permitted.
  • Block Evaluation: The final expression in a block { ... } is treated as the return value of that block.

3. Forging Guidelines

3.1 Absolute Elimination of Division by Zero

When performing division, you must either explicitly state in the requires clause that the divisor is non-zero or implement a dynamic guard using an if statement.

Bad: body: a / b; Good: body: if b != 0 { a / b } else { 0 };

3.2 Leveraging Quantifiers

When handling arrays or ranges, use forall to define boundary conditions.

Example: requires: forall(i, 0, len, arr[i] > 0);

3.3 Ownership and Borrowing

When working with heap-allocated resources (Vector<T>, HashMap<K, V>), follow these rules:

  • consume: Use consume x; to declare that a parameter's ownership is transferred. After consumption, the variable is dead — any subsequent access is a compile-time error.
  • ref: Use ref v: T for read-only access. The caller retains ownership, and the callee cannot free or consume the resource.
  • No double-free: The compiler's LinearityCtx tracks liveness via Z3 symbolic Bools. Consuming an already-consumed variable triggers: Double-free detected.
  • No use-after-free: Accessing a consumed variable triggers: Use-after-free detected.
  • No consume during borrow: Attempting to consume a borrowed variable triggers: Cannot consume: currently borrowed.

Bad: atom drop(ref v: i64) consume v; — ref and consume conflict Good: atom drop(v: i64) consume v; — ownership transfer without borrow

3.4 Trait Laws and Verification

When defining traits with law clauses, the compiler expands method calls using impl bodies and verifies with Z3:

  • law commutative_add: add(a, b) == add(b, a) → expanded to (a + b) == (b + a) → Z3 proves directly.
  • Use where constraints on trait method parameters: fn div(a: Self, b: Self where v != 0) -> Self;

3.5 Higher-Order Function Contracts (call_with_contract)

When defining atoms that accept function parameters via atom_ref, use the contract() clause to declare the expected preconditions and postconditions of the function parameter. This enables Z3 to verify the atom's body without relying on trusted.

Syntax:

atom apply(x: i64, f: atom_ref(i64) -> i64)
    requires: x >= 0;
    ensures: result >= 0;
    contract(f): ensures: result >= 0;
    body: call(f, x);
  • contract(f): ensures: <expr>; — declares the postcondition that f's result must satisfy.
  • contract(f): requires: <expr>, ensures: <expr>; — declares both precondition and postcondition.
  • In contract expressions, x / arg0 refer to the first call-site argument (not the atom's own parameter), y / arg1 to the second call-site argument, and result to the call's return value. Note: if the atom has a parameter named x, the contract's x will shadow it with the call-site argument value.

How it works: When the verifier encounters call(f, args...) and f is a parametric function parameter with a declared contract, it:

  1. Checks the requires clause (if any) holds at the call site — fails verification if the precondition may be violated.
  2. Asserts the ensures clause as a fact in the Z3 solver — constraining the symbolic result of the call.

This mechanism replaces the need for trusted on higher-order functions like map, fold_left, and result_map.

Subsumption warning: When calling apply(5, atom_ref(increment)), the verifier now performs a subsumption check: it verifies that increment's actual ensures clause, under its requires precondition, implies the declared contract(f): ensures. Formally: (concrete.requires ∧ concrete.ensures) ⇒ contract.ensures. If the implication does not hold, a warning is emitted to stderr (not a hard error, to maintain backward compatibility). For example, if increment has requires: x >= 0 and ensures: result == x + 1 and the contract declares ensures: result >= 0, no warning is emitted because x >= 0 ∧ result == x + 1 implies result >= 0. However, if the concrete atom's ensures does not imply the contract's ensures (even under its precondition), a warning like ⚠️ Subsumption warning: atom_ref(foo) passed to apply.f — concrete ensures '...' may not imply contract ensures '...' will be printed.

3.6 Effect-Polymorphic Higher-Order Functions

When defining atoms that are generic over effect sets, use <E: Effect> type parameter bounds and with E on function parameter types:

Syntax:

atom pipe<E: Effect>(f: atom_ref(i64) -> i64 with E)
    effects: [E];
    requires: true;
    ensures: true;
    body: call(f, 42);
  • <E: Effect> — declares E as an effect type parameter. The compiler verifies that the concrete type argument is a known effect definition.
  • with E — annotates the function parameter's effect set. After monomorphization, E is replaced with the concrete effect (e.g., FileWrite).
  • effects: [E] — the atom's own effect set includes the effect variable. After monomorphization, this becomes effects: [FileWrite].

How it works: Effect polymorphism is resolved through monomorphization (same as type polymorphism):

  1. pipe<FileWrite>(atom_ref(writer)) triggers monomorphization of pipe with E = FileWrite
  2. A concrete pipe<FileWrite> atom is generated with effects: [FileWrite] and with [FileWrite]
  3. The concrete atom is verified by Z3 using the standard effect containment check

Multiple effect parameters:

atom transform<E1: Effect, E2: Effect>(
    r: atom_ref(i64) -> i64 with E1,
    w: atom_ref(i64) -> i64 with E2
)
    effects: [E1, E2];
    requires: true;
    ensures: true;
    body: { let x = call(r, 1); call(w, x) };

3.7 Standard Library Usage

  • Prelude (std/prelude.mm): Auto-imported. Provides Eq, Ord, Numeric, Option<T>, Result<T, E>.
  • Alloc (std/alloc.mm): Import with import "std/alloc" as alloc;. Provides Vector<T>, HashMap<K, V>, alloc_raw, dealloc_raw.
  • FQN dot-notation: math.add(x, y) is equivalent to math::add(x, y).

4. Self-Healing Protocol (Handling Verification Failure)

If verification is marked as Failed, the developer or AI agent should follow these steps:

  1. Analyze the Counter-example: Refer to the Visualizer or report.json to identify which input values caused the logic to fail.
  2. Strengthen Requirements (requires): Re-evaluate if the input constraints are too loose.
  3. Repair the Body: Add if guards or implement proper edge-case handling.
  4. Re-forge: Run cargo run again to confirm that the mathematical contradiction has been resolved.

5. Output Semantics

Understand the following characteristics of the code exported by Mumei:

Language Characteristics Ownership Mapping Primary Use Case
LLVM IR Fast, Native Execution alloc_raw → malloc, dealloc_raw → free Performance-critical core logic

6. Numeric Safety

  • Optimization for i64: The current verification engine is optimized for i64 (Int64). u64 and f64 are also supported.
  • Overflow Responsibility: If there is a risk of overflow in arithmetic operations, limit the value range in the requires clause.
  • Float Verification: f64 is supported with sign propagation (pos×pos→pos, etc.). Use type Pos = f64 where v > 0.0; for positive-only floats.
  • Zero-Division Prevention: The Numeric trait's div method carries where v != 0 on the divisor. Z3 checks this at every call site automatically.

7. Prohibited Actions

  • Introducing Side Effects: Mumei focuses on pure functional verification. Modifying global variables or performing undefined external I/O within the body is strictly prohibited. Atoms without an effects: annotation are treated as pure — calling effectful atoms from a pure atom is a verification error.
  • Ignoring Type Constraints: Treat numbers as i64 by default and always account for potential overflows.

8. Comparison of Methods

Mumei serves as a bridge between heavyweight formal proof assistants and modern application development.

Item Lean 4 Coq / Rocq Mumei (無銘)
Primary Use General math proofs, SW verification Mathematical theorems, high-trust systems Secure code generation for AI agents
Difficulty Very High (Requires learning tactics) Very High (Requires math background) Moderate (Close to standard coding)
Verif. Engine Custom Kernel / Lean Checker Coq Kernel Z3 SMT Solver (Automated priority)
Automation Partially automated, mainly manual Mainly manual (via Ltac, etc.) Fully Automated (requires/ensures)
Target Output Lean runtime, C OCaml, Haskell, Scheme, etc. LLVM IR (native binary)
Memory Safety GC / managed GC / extracted Ownership + Borrowing (Z3-verified)
AI Synergy Research stage (LLM tactics) Research stage Native (JSON reports / Self-healing)
Design Logic Expressing math through code Building proofs as programs Preventing "unforged" (unsafe) code

9. Incremental Build

Mumei caches verification results per-atom in .mumei/cache/verification_cache.json:

  • Each atom's proof hash is computed from name | requires | ensures | body_expr | consume | ref | effects | trust level | callee signatures | type predicates.
  • The proof hash includes transitive callee signatures — if a callee's contract changes, all callers are automatically re-verified.
  • If the hash matches the cached value, Z3 verification is skipped — significantly reducing build times.
  • If verification fails, the atom is removed from cache and will be re-verified next time.
  • Old .mumei_build_cache files are automatically migrated to the new format.

On the second run: ✅ Verification passed: 2 verified, 6 skipped (unchanged) ⚡

10. Documentation

Document Purpose
README.md Language overview, features, quickstart
docs/LANGUAGE.md Language reference — types, generics, traits, ownership, async
docs/ROADMAP.md Strategic roadmap v0.3.0+ — 3 priorities, phases, dependencies, timeline
docs/CROSS_PROJECT_ROADMAP.md Cross-project roadmap (mumei + mumei-agent + mumei-lean + mumei-demo)
docs/ARCHITECTURE.md Compiler internals, pipeline, ModuleEnv, LinearityCtx
docs/STDLIB.md Standard library reference (all modules + atoms + planned std.json/std.http)
docs/EXAMPLES.md Verification suite, pattern matching, negative tests
docs/CHANGELOG.md Change history
docs/CAPABILITY_SECURITY.md Effect-based capability security evaluation
docs/DIAGNOSTICS.md Span-based diagnostics design and implementation status
docs/FFI.md FFI extern block design, implementation status, and bridge completion plan
docs/CONCURRENCY.md Structured concurrency (task/task_group) design, implementation status, and std.http integration plan
docs/TOOLCHAIN.md CLI commands, distribution, and future roadmap (3 priorities)
docs/PATTERNS.md Verification patterns — Verified Configuration, Verified State Machine
docs/CROSS_SPEC_GUIDE.md System-wide contract consistency, invariants, dependency cycles
docs/PLUGIN_GUIDE.md Emitter plugin architecture and external plugin development
docs/SPEC_GUIDE.md Decidable fragment guide, spec validation, property-based testing
docs/EDITORS.md Editor configuration (Neovim, Helix, Emacs, Sublime Text, Zed)
docs/LSP_INTEGRATION.md LSP CodeLens, intent drift, spec-code mapping
docs/PROOF_CERTIFICATE.md Proof certificate format and verification
docs/REPORT_SCHEMA.md report.json output schema for AI agent consumption
docs/STDLIB_METRICS.md Standard library proof health metrics (auto-updated by CI)
docs/STRUCTURED_FEEDBACK_SCHEMA.md Structured semantic feedback schema
docs/TRUSTED_ATOMS.md Trusted atom reduction roadmap and FFI contract test harness
docs/ZERO_HUMAN_CHALLENGE.md Zero-Human Challenge analysis and results
docs/META_ARCHITECT.md Meta-architect design notes
docs/SESSION_PLANS.md Detailed session plans for implementation priorities
docs/CLI.md CLI command reference
docs/CLAUDE_CODE_QUICKSTART.md Claude Code + mumei setup and workflow guide
mumei-agent/docs/VERIFICATION_WORKFLOW_GUIDE.md End-to-end verification workflows — NL spec validation, foreign-code verification, spec↔code alignment, cross-spec, MCP usage, self-healing loop
instruction.md This file — forging guidelines, development phase, coding conventions

11. Current Development Phase: Strategic Roadmap v0.3.0+

Details: docs/ROADMAP.md

LSP Status: Active

The LSP server (mumei lsp) has the following features implemented:

  • textDocument/didOpen / textDocument/didChange → parse error diagnostics
  • textDocument/hover → atom requires/ensures display
  • Z3 verification error diagnostics (with Span-based position info)
  • Real-time /// spec: natural-language comment validation via mumei-agent validate-spec
  • Inline contract diagnostics for opened .py / .rs / .ts / .tsx / .go files via mumei-agent validate-code
  • textDocument/completion → keyword, atom, effect, type/struct/enum completion (trigger characters: ., :)
  • textDocument/definition → jump to atom, type, struct, enum, effect, trait, and resource definitions
  • shutdown / exit handling
  • Parsed items cache for efficient completion and definition lookups

Editor configuration examples: docs/EDITORS.md

Deferred items:

  • Counter-example highlighting in editors
  • VS Code Marketplace publishing → ✅ Published (see editors/vscode/README.md)

Strategic Vision: From Experimental to Practical

Mumei's differentiators:

  • Rust-level safety (Z3 formal verification) combined with
  • Go-level simplicity for concurrent programming

Three strategic priorities to transform Mumei from an experimental language into a practical tool:

🥇 Priority 1: Network-First Standard Library (std.http + std.json)

Goal: Build a compelling demo: "API scripting is this simple and safe in Mumei."

Phases:

  1. P1-A: FFI Bridge Completion — extern → trusted atom auto-registration in ModuleEnv (prerequisite for all FFI-backed stdlib)
  2. P1-B: std.json — json.parse(str) / json.stringify(obj) / json.get_string() / json.get_int() (serde_json backend)
  3. P1-C: std.http — http.get(url) / http.post(url, body) → Response (reqwest FFI backend)
  4. P1-D: Integration Demo — task_group:all + concurrent HTTP requests example

Target API:

import "std/http" as http;
import "std/json" as json;

// Simple GET — extreme simplicity
let response = await http.get("https://api.example.com/users");
let data = json.parse(http.body(response));
let name = json.get_string(data, "name");

// Concurrent requests — Mumei's killer feature
task_group:all {
    task { http.get("https://api.example.com/users") };
    task { http.get("https://api.example.com/orders") };
    task { http.get("https://api.example.com/products") }
}

🥈 Priority 2: Runtime Portability

Goal: "Install in 30 seconds, run anywhere."

Phases:

  1. P2-A: Static Linking — musl target for fully static Linux binaries + Windows support
  2. P2-B: Homebrew Tap — brew install mumei-lang/mumei
  3. P2-C: WebInstall — curl -fsSL https://mumei-lang.github.io/install.sh | sh

🥉 Priority 3: CLI Developer Experience

Goal: "Best-in-class CLI development experience, no IDE required."

Phases:

  1. P3-A: mumei repl — Interactive REPL with incremental definition, verification feedback, and :verify-spec / :verify-code handoff to mumei-agent (spec_health_issues / verification_violations / cross_validation_gaps / next_steps)
  2. P3-B: mumei doc — rustdoc-style HTML documentation generation from /// comments
  3. P3-C: REPL + HTTP Integration — Try HTTP requests interactively in REPL

Task (Concurrency) Refinement (embedded in P1-D)

Improve the practicality of task / task_group introduced in PR-C.

Implemented (Plan 8):

  • Task return type inference — type checker infers return type from task { expr } block's final expression; await yields the correct type from the task handle
  • Syntax for binding task_group results to variables — let results = task_group { ... } binds the collection of individual task return types
  • Task cancellation semantics — cancel group_name; statement cancels pending tasks in a task_group; task_group scope exit implicitly cancels all pending tasks via cancellation token mechanism
  • Channel type (chan<T>) — built-in generic type with send(ch, value) and recv(ch) operations; requires Chan effect annotation; implemented in parser (send/recv keywords), AST (ChanSend/ChanRecv), HIR, MIR, codegen, and Z3 verification (channel and value sub-expressions are fully traversed)

12. Coding Conventions

  • Always run cargo fmt before committing.
  • When adding a new Expr variant, add match arms in all of these locations:
    • mumei-core/src/verification.rs: expr_to_z3, stmt_to_z3, collect_callees_expr, collect_callees_stmt, count_self_calls_expr, count_self_calls_stmt, collect_acquire_resources_expr, collect_acquire_resources_stmt, expr_has_symbolic_perform_args, body_has_symbolic_perform_args, has_acquire_in_while_expr
    • mumei-core/src/ast.rs: collect_from_expr, collect_from_stmt
    • mumei-core/src/hir.rs: collect_free_variables_expr, collect_free_variables_stmt
    • mumei-emit-llvm/src/codegen.rs: compile_hir_expr, compile_hir_stmt
    • mumei-core/src/mir.rs: lower_expr, lower_stmt
  • When adding a new Item variant, add match arms in all of these locations:
    • src/main.rs: load_and_prepare, cmd_check, cmd_build
    • mumei-core/src/resolver.rs: resolve_imports_recursive, register_imported_items
    • src/lsp.rs: verify_source_for_lsp
  • When adding Item::EffectDef, ensure match arms exist in all locations listed above.
  • When constructing Atom instances (including extern → atom conversion), always include effects: vec![] as default. Also include effect_pre: std::collections::HashMap::new(), effect_post: std::collections::HashMap::new() for modular verification fields.
  • The effect_pre / effect_post syntax in .mm files: effect_pre: { EffectName: StateName }; effect_post: { EffectName: StateName }; — parsed as HashMap<String, String>. Default is empty HashMap if omitted.
  • When monomorphizing atoms with effect_pre/effect_post, substitute effect type variable keys using type_map (same pattern as effects substitution). Do not simply .clone() — generic keys like E must be replaced with concrete names like FileWrite.
  • When using #[allow(dead_code)], always add a NOTE comment explaining the reason.