Metadata-Version: 2.4
Name: monogate-forge
Version: 0.15.0
Summary: EML language and compiler for verified mathematical computation across 36 targets: software, GPU shaders, hardware (FPGA/ASIC, SPICE, KiCad, and JLCPCB), formal verification, and safety-critical systems.
Author: Mosa Creates LLC
Author-email: "Arturo R. Almaguer" <contact@monogate.dev>
Maintainer-email: "Arturo R. Almaguer" <contact@monogate.dev>
License: MIT
Project-URL: Homepage, https://monogateforge.com
Project-URL: Documentation, https://monogate.dev/learn/eml/intro
Project-URL: VS Code Extension, https://marketplace.visualstudio.com/items?itemName=Monogate.monogate-forge-vscode
Project-URL: Research, https://monogate.org
Project-URL: MachLib, https://machlib.org
Keywords: compiler,programming-language,formal-verification,lean,fpga,hdl,verilog,vhdl,safety-critical,embedded,math,shader,hlsl,metal,wgsl,eml
Classifier: Development Status :: 4 - Beta
Classifier: Intended Audience :: Developers
Classifier: Intended Audience :: Science/Research
Classifier: License :: OSI Approved :: MIT License
Classifier: Operating System :: OS Independent
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Topic :: Scientific/Engineering
Classifier: Topic :: Scientific/Engineering :: Mathematics
Classifier: Topic :: Software Development :: Compilers
Classifier: Topic :: Software Development :: Code Generators
Classifier: Topic :: Software Development :: Embedded Systems
Classifier: Typing :: Typed
Requires-Python: >=3.11
Description-Content-Type: text/markdown
License-File: LICENSE
Requires-Dist: eml-cost>=0.19.0
Requires-Dist: cryptography>=42
Requires-Dist: numpy>=2.0
Provides-Extra: dev
Requires-Dist: pytest>=8; extra == "dev"
Requires-Dist: pytest-cov>=5; extra == "dev"
Requires-Dist: pytest-xdist>=3.5; extra == "dev"
Requires-Dist: ruff>=0.5; extra == "dev"
Requires-Dist: mypy>=1.10; extra == "dev"
Requires-Dist: pyyaml>=6; extra == "dev"
Provides-Extra: lsp
Requires-Dist: pygls>=2.0; extra == "lsp"
Requires-Dist: lsprotocol>=2024.0.0b1; extra == "lsp"
Dynamic: license-file

# Monogate Forge

[![PyPI](https://img.shields.io/pypi/v/monogate-forge.svg)](https://pypi.org/project/monogate-forge/)
[![License: MIT](https://img.shields.io/badge/license-MIT-blue.svg)](LICENSE)
[![Python](https://img.shields.io/pypi/pyversions/monogate-forge.svg)](https://pypi.org/project/monogate-forge/)

**Forge is the EML language and compiler. Write a math kernel once, compile it to 36 backends — all of them emitting locally from the CLI, no license and no account — with chain-order analysis, and contracts (`requires`, `ensures`, refinement types) that the Lean, Coq and Isabelle targets state as theorems wherever a function declares them. Whether another target checks a contract at run time depends on the target, and several emit nothing: see [the per-target table](docs/verify-guide.md#what-backends-respect-contracts). The catalog spans software, GPU shaders, compiler IRs, FPGA RTL, manufacturing artifacts, formal-verification proofs, safety-critical avionics, gaming and EVM. The tables below list every one, and what each needs in your source to fire.**

---

## Quick start

```bash
pip install monogate-forge
```

Create `hello.eml`:

```eml
module hello;

fn pid(error: Real, integral: Real, derivative: Real) -> Real
    where chain_order <= 0
    requires (-1.0 <= error && error <= 1.0)
    ensures  (-1.5 * 1.0 <= result && result <= 1.5 * 1.0)
{
    let kp = 1.0;
    let ki = 0.2;
    let kd = 0.3;
    kp * error + ki * integral + kd * derivative
}
```

Compile to every target at once:

```bash
eml-compile hello.eml --target all -o build/
```

You now have `build/hello.c`, `build/hello.rs`, `build/hello.py`, `build/hello.lean`, `build/hello.v`, `build/hello.hlsl`, `build/hello.metal`, `build/hello.swift`, … one file per target. Pick a single target instead:

```bash
eml-compile hello.eml --target rust -o hello.rs
eml-compile hello.eml --target c    -o hello.c
eml-compile hello.eml --target lean -o Hello.lean
```

A snippet of `hello.rs`:

```rust
use monogate_sys::*;

/// pid
/// Pfaffian chain count (eml-cost pfaffian_r): 0     Cost class: p0-d2-w0-c0
/// EML depth:   2  Symbolic band: LOW (from pfaffian_r only)
/// Numerical:   cancellation exposure NONE  (no mixed-sign subtraction)
/// source obligations for pid: {O1}
///   O1 [a99a5a5c258f] -> PRESERVED (equivalent)  assert! before the tail expression
///        build: unconditional -- assert! is kept in release builds -- only debug_assert! is compiled out
/// Dynamics:    0 osc, 0 decay  (predicted_r=0)
/// FPGA est:   2 MAC, 0 exp, 0 ln, 0 trig -> 4 cy @ 32-bit
pub fn pid(error: f64, integral: f64, derivative: f64) -> f64 {
    assert!((((-1.0) <= error) && (error <= 1.0)), "pid: requires ((((-1.0) <= error) && (error <= 1.0)))");
    let kp: f64 = 1.0;
    let ki: f64 = 0.2;
    let kd: f64 = 0.3;
    let result = (((kp * error) + (ki * integral)) + (kd * derivative));
    assert!(((((-1.5) * 1.0) <= result) && (result <= (1.5 * 1.0))), "pid: ensures violated");
    result
}
```

Every emitted function carries its EML profile (eml-cost's pfaffian_r,
cost class, EML depth, symbolic band, cancellation exposure, FPGA cycle
estimate) and its obligation map in the doc-comment header, so a
reviewer can see the analysis without leaving the file. The `requires`
and `ensures` contracts from the EML source become runtime `assert!`s,
which release builds keep. `tests/test_doc_emission_samples.py` holds
this snippet to what the Rust backend prints for the `hello.eml` above.

Five-minute tour: [`docs/quickstart.md`](docs/quickstart.md). Full tutorial: [monogate.dev/learn/eml/intro](https://monogate.dev/learn/eml/intro).

---

## What you get

**36 targets. All local. All free.** Every backend in the tables below emits from `eml-compile` on your machine — there is no Free/Pro split, no license token, and no hosted step in the path. What a target needs is not a tier but an *annotation*: the RTL family wants a `@target(fpga, ...)` function, the circuit family wants `@spice_*` components, and the proof family wants a `@verify(lean, ...)` block. Ask for a target the source has nothing to feed and the compiler says so instead of emitting a stub. The **Requires** column below records exactly that. Per-target notes — flag, file extension, what the output is for — are in [docs/backends.md](docs/backends.md).

### What each target's toolchain accepts

Emitting is not compiling, and compiling is not synthesizing. This table is what was measured, not what is
supported:

<!-- corpus-status:begin -->
Measured by the corpus gate over every tracked `.eml` file (348): each file is emitted for each target and read by that target's own toolchain (compiled, linked, run or validated: see `tools/scripts/corpus_checks/`). **Emits** is how many files the target produced an artifact for; the rest it refused with a stated reason (a missing `@target(fpga)`, `@spice_*` or `@verify` annotation is a refusal). **Accepted** is how many of those the toolchain accepted; **Broken** were rejected. Broken files are listed by name in `tools/corpus_compile_baseline.json`, each target's list may only shrink, and each broken target carries an owner and an expiry date there.

| Target | Checked | Emits | Accepted | Broken | Contract-stopped | Not measured |
|---|---|---|---|---|---|---|
| c | every push | 348 of 348 | 348 of 348 | 0 of 348 | 0 | — |
| cpp | nightly | 343 of 348 | 343 of 343 | 0 of 343 | 0 | execution |
| rust | every push | 343 of 348 | 343 of 343 | 0 of 343 | 0 | execution |
| python | nightly | 343 of 348 | 343 of 343 | 0 of 343 | 45 | — |
| go | nightly | 343 of 348 | 343 of 343 | 0 of 343 | 0 | execution |
| java | nightly | 343 of 348 | 343 of 343 | 0 of 343 | 0 | execution |
| kotlin | nightly | 343 of 348 | 343 of 343 | 0 of 343 | 0 | execution |
| csharp | nightly | 343 of 348 | 343 of 343 | 0 of 343 | 0 | execution |
| javascript | nightly | 338 of 348 | 338 of 338 | 0 of 338 | 45 | — |
| wasm | nightly | 337 of 348 | 337 of 337 | 0 of 337 | 0 | execution |
| matlab | nightly | 339 of 348 | 339 of 339 | 0 of 339 | 45 | — |
| lean | nightly | 282 of 348 | 279 of 282 | 3 of 282 (owner agent-maestro, expires 2026-10-16) | 0 | proofs: a sorry theorem compiles (tools/scripts/lean_discharge_census.py counts discharge) |
| zkproof | nightly | 29 of 348 | 29 of 29 | 0 of 29 | 0 | — |
| verilog | every push | 178 of 348 | 178 of 178 | 0 of 178 | 0 | synthesis is not gated (yosys synthesized every linted design on 2026-09-16, about an hour); simulation against C only for the demo kernels |
| systemverilog | nightly, advisory (not gating) | 214 of 348 | 80 of 214 | 134 of 214 | 0 | synthesis and simulation (Verilator lint only) |
| vhdl | nightly | 170 of 348 | 170 of 170 | 0 of 170 | 0 | synthesis and simulation (GHDL analysis and elaboration only) |
| chisel | nightly, advisory (not gating) | 214 of 348 | 20 of 214 | 194 of 214 | 0 | synthesis (compiled and elaborated to CHIRRTL only) |
| llvm | nightly | 337 of 348 | 337 of 337 | 0 of 337 | 0 | execution |
| hlsl | nightly | 337 of 348 | 337 of 337 | 0 of 337 | 0 | not run on a GPU (glslang, not DXC) |
| glsl | nightly | 337 of 348 | 337 of 337 | 0 of 337 | 0 | not run on a GPU |
| glsles | nightly | 337 of 348 | 337 of 337 | 0 of 337 | 0 | not run on a GPU |
| wgsl | nightly | 342 of 348 | 342 of 342 | 0 of 342 | 0 | not run on a GPU |
| metal | not covered: Apple's Metal shader compiler (`xcrun metal`) ships only for macOS and Windows; no Linux build exists, none is on this box, and compiling MSL as C++ would not apply Metal's rules | — | — | — | — | everything |
| swift | nightly | 343 of 348 | 343 of 343 | 0 of 343 | 0 | execution |
| ada | nightly | 332 of 348 | 332 of 332 | 0 of 332 | 0 | execution |
| autosar | nightly | 342 of 348 | 342 of 342 | 0 of 342 | 0 | AUTOSAR XSD conformance and an RTE generator run |
| aadl | not covered: no AADL front end is installed: osate, ocarina and aadl-inspector are all absent from PATH (measured 2026-09-16), and the target's output is AADL text that only such a tool can name-resolve and legality-check. OSATE is an Eclipse RCP download and Ocarina builds from source with GNAT; neither is here. | — | — | — | — | everything |
| ros2 | nightly | 337 of 348 | 337 of 337 | 0 of 337 | 0 | real rclcpp (compiled against a stub of the API it uses) |
| coq | nightly | 282 of 348 | 282 of 282 | 0 of 282 | 0 | proofs: an Admitted theorem compiles |
| isabelle | nightly | 282 of 348 | 282 of 282 | 0 of 282 | 0 | proofs: a sorry theorem compiles |
| solidity | nightly | 338 of 348 | 337 of 338 | 1 of 338 (owner agent-maestro, expires 2026-10-22) | 0 | execution on an EVM (compiled only) |
| luau | nightly | 339 of 348 | 339 of 339 | 0 of 339 | 45 | — |
| gdscript | nightly | 337 of 348 | 337 of 337 | 0 of 337 | 0 | execution (Godot --check-only) |
| spice | nightly | 7 of 348 | 7 of 7 | 0 of 7 | 0 | the circuit's behaviour against the kernel |
| kicad | not covered: kicad-cli here is 7.0.11 and the backend emits KiCad 8 (version 20231120): measured 2026-09-16, `kicad-cli sch export netlist` refuses all 7 emitted corpus schematics unmodified with `Failed to load schematic file` (rc 3). A dialect shim (software/backends/tests/test_kicad_schematic_actually_loads.py) loads 6 of 7, but that checks a transformation, not the artifact; examples/maglev/driver.eml fails even shimmed, cause undetermined without KiCad 8. | — | — | — | — | everything |
| jlcpcb | nightly | 7 of 348 | 7 of 7 | 0 of 7 | 0 | manufacturability at the fab |

**Contract-stopped** files emitted and ran, but every probe input fired one of the kernel's own contract checks, so the body past it never ran: not a failure, and not a full run either.
<!-- corpus-status:end -->

### Whether every target computes the same number

Accepting an artifact is not computing the right value. Every wrong number found in the week before the
differential gate existed compiled, linted or synthesized cleanly. This table is what one kernel's own
functions actually returned, target against target, bit for bit:

<!-- differential-status:begin -->
Measured by the differential gate (`tools/scripts/differential.py`) over every tracked `.eml` file (348): **1025 of 1098** functions are in round-1 scope (Real/f64 arguments, a Real/f64 or tuple return, no `state`, no `extern`), each is called with up to 48 generated inputs -- contract boundaries and one ulp either side, IEEE specials, seeded draws -- and every result is compared with the `c` artifact's **by bits**: 47320 calls per target. **Agree** means identical bits on every call (a NaN is one value; both sides firing the same contract counts). Every other function is listed by name in `tools/differential_baseline.json`, which may only shrink.

| Target | Agree | Signed zero | Ulp | Wrong | Contract differs | Contract unchecked | Target error | Refused | Burn-down |
|---|---|---|---|---|---|---|---|---|---|
| ada | 688 of 1012 | 19 | 129 | 177 | 7 | 0 | 64 | 13 | owner agent-maestro, expires 2026-10-17 |
| c | 1025 of 1025 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | — |
| cpp | 749 of 1025 | 16 | 71 | 192 | 16 | 0 | 0 | 0 | owner agent-maestro, expires 2026-10-17 |
| csharp | 969 of 1025 | 14 | 13 | 23 | 11 | 0 | 10 | 0 | owner agent-maestro, expires 2026-10-17 |
| gdscript | 947 of 1021 | 15 | 27 | 33 | 9 | 0 | 0 | 4 | owner agent-maestro, expires 2026-10-17 |
| go | 576 of 1025 | 6 | 264 | 225 | 18 | 0 | 0 | 0 | owner agent-maestro, expires 2026-10-17 |
| java | 797 of 1025 | 4 | 187 | 35 | 14 | 0 | 0 | 0 | owner agent-maestro, expires 2026-10-17 |
| javascript | 825 of 1025 | 0 | 160 | 32 | 14 | 0 | 0 | 0 | owner agent-maestro, expires 2026-10-17 |
| kotlin | 788 of 1025 | 14 | 189 | 36 | 15 | 0 | 10 | 0 | owner agent-maestro, expires 2026-10-17 |
| llvm | 310 of 1025 | 0 | 0 | 0 | 0 | **715** (disclosed) | 0 | 0 | — |
| luau | 967 of 1025 | 14 | 16 | 24 | 11 | 0 | 0 | 0 | owner agent-maestro, expires 2026-10-17 |
| matlab | 995 of 1025 | 15 | 10 | 2 | 3 | 0 | 0 | 0 | owner agent-maestro, expires 2026-10-17 |
| python | 815 of 1025 | 20 | 58 | 137 | 26 | 0 | 0 | 0 | owner agent-maestro, expires 2026-10-17 |
| rust | 866 of 1025 | 11 | 139 | 9 | 3 | 0 | 0 | 0 | owner agent-maestro, expires 2026-10-17 |
| swift | 979 of 1025 | 3 | 10 | 22 | 11 | 0 | 0 | 0 | owner agent-maestro, expires 2026-10-17 |
| wasm | 310 of 1025 | 0 | 0 | 0 | 0 | **715** (disclosed) | 0 | 0 | — |

Counts are FUNCTIONS, not calls. **Signed zero**, **Ulp** and **Contract unchecked** are tolerated classes, not defects: *signed zero* is equal except the sign of a zero; *ulp* is within 4 ulps, and the function reaches a libm call (glibc's exp/log/pow are not correctly rounded, and a target with its own libm is no less right); *contract unchecked* is the reference's contract fired and the target returned the body's value, on a target docs/verify-guide.md records as checking no contract.

**Contract unchecked is why llvm and wasm agree on a minority of functions, and it is not a failure rate.** docs/verify-guide.md's contract table records both targets as checking neither `requires` nor `ensures` (LLVM IR lowers a `requires` to an `llvm.assume`, a promise to the optimizer, and drops `ensures`; WebAssembly is built from that IR), so where the reference refuses an input they return the value the body computed. That comparison did not happen; it is disclosed, recorded and shrink-only, and no value difference hides behind it -- their **Wrong** and **Contract differs** columns are the same 0 as any agreeing target's.

**Not covered.** 73 of 1098 functions are outside round-1 scope and are refused with a stated reason per function in the baseline (`state` across calls, a `Vec`/`Mat`/`Int` parameter, an `extern` the host supplies), never counted as agreement. **Refused** above is a module that target's own toolchain would not emit or build at all. Every other target Forge has (lean, zkproof, verilog, systemverilog, vhdl, chisel, hlsl, glsl, glsles, wgsl, metal, autosar, aadl, ros2, coq, isabelle, solidity, spice, kicad, jlcpcb) executes nothing here: they are compared by the corpus gate's own checkers, which ask whether the toolchain ACCEPTS the artifact -- a different question, and the one the table above this answers.
<!-- differential-status:end -->

### Software (general-purpose)
| Target | Flag | Requires |
|---|---|---|
| C99 | `--target c` | — |
| C++17 | `--target cpp` | — |
| Rust | `--target rust` | — |
| Python 3 | `--target python` | — |
| Go | `--target go` | — |
| Java | `--target java` | — |
| Kotlin | `--target kotlin` | — |
| C# | `--target csharp` | — |
| JavaScript | `--target javascript` | — |
| MATLAB | `--target matlab` | — |
| Swift | `--target swift` | — |

### Compiler IRs
| Target | Flag | Requires |
|---|---|---|
| WebAssembly | `--target wasm` | — |
| LLVM IR | `--target llvm` | — |

### GPU shaders
| Target | Flag | Requires |
|---|---|---|
| HLSL (DirectX) | `--target hlsl` | — |
| GLSL (desktop) | `--target glsl` | — |
| GLSL ES | `--target glsles` | — |
| WGSL (WebGPU) | `--target wgsl` | — |
| Metal (Apple) | `--target metal` | — |

### Hardware (FPGA / ASIC)
| Target | Flag | Requires |
|---|---|---|
| Verilog | `--target verilog` | `@target(fpga)` fn |
| SystemVerilog | `--target systemverilog` | `@target(fpga)` fn |
| VHDL | `--target vhdl` | `@target(fpga)` fn |
| Chisel / FIRRTL | `--target chisel` | `@target(fpga)` fn |

### Manufacturing / circuits
| Target | Flag | Requires |
|---|---|---|
| spice | `--target spice` | `@spice_*` components |
| kicad | `--target kicad` | `@spice_*` components |
| jlcpcb | `--target jlcpcb` | `@spice_*` components |

### Formal verification
| Target | Flag | Requires |
|---|---|---|
| Lean 4 | `--target lean` | `@verify(lean)` block |
| Coq | `--target coq` | `@verify(lean)` block |
| Isabelle/HOL | `--target isabelle` | `@verify(lean)` block |

### Safety-critical
| Target | Flag | Requires |
|---|---|---|
| Ada/SPARK | `--target ada` | — |
| AUTOSAR C | `--target autosar` | — |
| AADL | `--target aadl` | — |
| ROS 2 / C++ | `--target ros2` | — |

### Gaming
| Target | Flag | Requires |
|---|---|---|
| Luau (Roblox) | `--target luau` | — |
| GDScript (Godot) | `--target gdscript` | — |

### Blockchain
| Target | Flag | Requires |
|---|---|---|
| Solidity (PRBMath SD59x18) | `--target solidity` | — |

### Zero-knowledge
| Target | Flag | Requires |
|---|---|---|
| Plonky2 ZK circuits (research) | `--target zkproof` | — |

Every target above is free and emits locally. The Free/Pro split that earlier releases shipped is retired: `ALL_TIERS_FREE` in `tools/license/verifier.py` is `True`, so `load_license` reads nothing, `target_allowed` passes everything, and no token is checked on any path. The signing machinery stays in the tree because deleting it would be a bigger change than parking it, not because it gates anything. If a target refuses to emit, the reason is in the **Requires** column — a missing annotation in your source, which the error message names.

---

## VS Code extension

[**Monogate Forge on the VS Code Marketplace**](https://marketplace.visualstudio.com/items?itemName=Monogate.monogate-forge-vscode)

```
ext install Monogate.monogate-forge-vscode
```

LSP features:

- **Chain-order on hover** — every function shows its profiled chain order, cost class, and node count.
- **Completions** — keywords (`fn`, `let`, `where`, `requires`, `ensures`, `module`, `use`), builtins (`exp`, `ln`, `sin`, `cos`, `sqrt`, `tanh`, `pow`, `clamp`, `eml`, …), stdlib modules.
- **Diagnostics** — type errors, unbound identifiers, chain-order violations, contract failures.
- **FPGA status bar** — for any function annotated `@target(fpga)`, the status bar shows estimated LUT / DSP / latency for the selected device.
- **Format on save** — canonical layout via `eml-fmt`.

Marketplace listing: [Monogate.monogate-forge-vscode](https://marketplace.visualstudio.com/items?itemName=Monogate.monogate-forge-vscode).

---

## Why Forge

Industrial automation today is stuck on ladder logic — Boolean rungs from the 1960s that can't express transcendental functions, can't prove correctness, can't optimize node count, and treat PID loops as black boxes. Structured Text is marginally better but still opaque. MATLAB/Simulink + HDL Coder will get you to FPGA, but the math hides inside vendor library calls and you have no formal proof of precision.

**EML makes every mathematical operation visible and measurable.** Every expression is an EML tree and every function carries a chain order. A contract a function declares is stated as a Lean theorem unless translation loses it, which the obligation map reports as LOST. Whether that theorem is then proved is a separate question, answered by `#print axioms`. The same source compiles to your laptop, your microcontroller, your FPGA, your Solidity contract, and your formal proof. The FPGA targets compute in Q-format fixed point, so they do not agree bit for bit with the IEEE-754 software targets.

---

## Documentation

- [Quickstart](docs/quickstart.md) — pip install to first compile in 5 minutes.
- [Language reference](docs/language-reference.md) — every keyword, builtin, type, and annotation.
- [Backends](docs/backends.md) — every compilation target with its CLI flag, file extension, and what it needs in your source.
- [Verify guide](docs/verify-guide.md) — `@verify`, `requires`/`ensures`, Lean output, MachLib integration.
- [FPGA guide](docs/fpga-guide.md) — `@target(fpga)`, LUT/DSP estimates, precision selection, vendor support.

External:

- [monogate.dev/learn/eml/intro](https://monogate.dev/learn/eml/intro) — guided beginner tutorial.
- [monogate.dev/learn/eml/engineering](https://monogate.dev/learn/eml/engineering) — intermediate engineering course (chain orders, contracts, FPGA targeting, Lean verification).
- [monogateforge.com/get-started](https://monogateforge.com/get-started) — install the CLI.
- [monogate.org](https://monogate.org) — research papers and theory.
- [machlib.org](https://machlib.org) — formal library of mathematical kernels with Lean proofs.
- [arXiv preprint](https://arxiv.org/) — the EML cost conjecture and Pfaffian profile.

---

## Contributing

See [`CONTRIBUTING.md`](CONTRIBUTING.md). Bug reports and feature requests via GitHub issues.

## License

Compiler is MIT (see [`LICENSE`](LICENSE)). Specific algorithmic methods covered by patents — open implementation, but commercial re-implementations may need a license. See `patents/index.md`.

Built by [Mosa Creates LLC](https://monogateforge.com).
