eFrog — supported source frontends for the EML substrate

Forge compiles EML into targets. eFrog lifts supported source inputs into EML.

pip install efrog (pre-release)

eFrog reads supported source files and extracts their mathematical structure as EML — the same intermediate language Monogate Forge emits into. eFrog is the reverse direction for covered frontends: supported inputs become EML trees you can profile, classify against a corpus of canonical math patterns, optimize, and compile through Forge targets.

Current capability boundary:

• Local package: 12 source frontends — Python, C, JavaScript, Rust, MATLAB, Java, Go, Kotlin, GDScript, Lua, Julia, Solidity.
• Hosted efrog.dev / MCP: 12 source frontends — parity with the local package as of 2026-06-17 (Python, C, JavaScript, Rust, MATLAB, Java, Go, Kotlin, GDScript, Lua, Julia, Solidity).
• Forge contract: all 12 local frontends pass the small-fixture matrix for EML emission, Forge format check, Forge Python compile, and Python bytecode compile.
• This is small-fixture compatibility evidence, not a claim that arbitrary source programs decompile perfectly.

What's shipped (E1 + E2 + E2.5 + early E3 + E4 scaffolding + E5 + E6)

efrog gaussian.py              # Python AST → EML
efrog gaussian.c               # C (math.h) → EML, via pycparser
efrog gaussian.js              # JavaScript / TypeScript → EML, via esprima
efrog gaussian.rs              # Rust → EML, hand-rolled parser
efrog gaussian.m               # MATLAB / Octave → EML, hand-rolled parser
efrog gaussian.java            # Java → EML, via javalang
efrog gaussian.go              # Go → EML, hand-rolled parser
efrog gaussian.kt              # Kotlin → EML, hand-rolled parser
efrog gaussian.gd              # GDScript (Godot) → EML, hand-rolled parser
efrog gaussian.lua             # Lua → EML, hand-rolled parser
efrog gaussian.jl              # Julia → EML, hand-rolled parser
efrog gaussian.sol             # Solidity (pure/view fns) → EML, hand-rolled parser

efrog --profile  gaussian.py   # per-fn chain order, drift risk, node count
efrog --verify   gaussian.py   # round-trip the EML, sample N inputs, and
                               # compare numerically with the original
efrog --genome   gaussian.py   # classify each fn against a small corpus
                               # (gaussian / sigmoid / softplus / polynomial …)
efrog --lean     gaussian.py   # emit Lean 4 theorem skeletons
efrog --prove    gaussian.py   # run BFS prover; closes chain_order
                               # via concrete Nat reduction (--prove
                               # implies --lean)
efrog --optimize gaussian.py   # conservative algebraic simplifier
                               # (x+0, x*1, exp(0), x**2 → x*x, …)
efrog --capabilities           # JSON capability map for eFrog + Forge
efrog gaussian.py --normalize  # alpha-normalized EML shape JSON
efrog gaussian.py --obligations
                               # unresolved domain/stability obligation JSON
efrog gaussian.py --evidence   # Translation Evidence Packet v0 JSON
efrog --roundtrip-matrix --strict
                               # source -> EML -> Forge target matrix,
                               # with evidence packets when --out-dir is set
efrog gaussian.py --bridge-bundle --strict --out-dir build/bridge
                               # complete source -> EML -> targets +
                               # evidence/obligation/Lean bundle
efrog --audit-bundle build/bridge
                               # recompute bundle hashes and fail on drift
efrog --bridge-guard --out-dir build/bridge-guard
                               # CI guard: capability + bundle + audit +
                               # tamper probe + hosted roundtrip matrix
efrog --bridge-benchmark --out-dir build/bridge-benchmark
                               # 10-case bridge corpus with EML advantage
                               # labels, obligations, audits, and sampled
                               # Python/Rust equivalence
efrog --advantage-from-bridge --out-dir build/bridge-advantage
                               # derive conservative advantage signals from
                               # bridge evidence; writes JSON, Markdown, feed
efrog --advantage-from-bridge --witness-registry build/runtime-guard-witness/runtime_guard_witness_registry.json --out-dir build/bridge-advantage-witnessed
                               # derive the same conservative signals with
                               # runtime-witness maturity attached
efrog --close-obligations --out-dir build/obligation-closure
                               # plan runtime/proof closure routes for
                               # benchmark obligations; discharges nothing
efrog --guard-witness --out-dir build/runtime-guard-witness
                               # attach deterministic runtime guard
                               # witnesses to planned benchmark obligations
                               # and write a local witness registry;
                               # proves/certifies nothing
efrog --close-obligations --witness-registry build/runtime-guard-witness/runtime_guard_witness_registry.json --out-dir build/obligation-closure-witnessed
                               # re-render closure plans with witnessed
                               # statuses from the local registry
efrog --evidence-ladder-review --out-dir build/evidence-ladder-review
                               # consolidate benchmark, advantage,
                               # closure, and witness artifacts into one
                               # local reviewer case file
efrog --evidence-ladder-guard --out-dir build/evidence-ladder-guard
                               # strict local guard for reviewer artifacts,
                               # witness counts, schemas, and claim flags
efrog --holdout-trial --out-dir build/holdout-gaussian-stable
                               # one-source Gaussian holdout through
                               # benchmark, runtime witness, and reviewer;
                               # not part of the default benchmark corpus
efrog --holdout-registry --out-dir build/holdout-registry
                               # registered holdout kernels through the same
                               # evidence path, summarized without promoting
                               # them into the default corpus
efrog --validate-artifact build/bridge/bridge_bundle_manifest.json
                               # validate one JSON artifact against schemas/
efrog --mic                    # capture audio, FFT, emit single-sine EML

A typical extraction looks like this:

module gaussian;

fn gaussian(mu: Real, sigma: Real, x: Real) -> Real
    where chain_order <= 1
{
    let dx = x - mu;
    exp(-dx * dx / (2.0 * sigma * sigma)) / sigma
}

E1 — Python pure math

• math.exp/log/sqrt/sin/cos/tan/asin/acos/atan/sinh/cosh/tanh/pow/fabs → EML builtins
• math.pi, math.e, math.tau → exact-repr numeric literals
• ** (power), +, -, *, /, unary - → EML operators
• def f(x: float, ...) -> float → fn f(x: Real, ...) -> Real
• let bindings via local name = expr lines, then return expr
• Top-level MODULE_NAME = "..." overrides the inferred module name

E2 — Loops, conditionals, NumPy, C

• Fixed-iteration loop unrolling — for i in range(N): with literal N (≤ 64) expands to a flat let-chain
• Augmented assigns — x *= y, x += y etc. lower to let x = x * y;
• Conditional flattening — if cond: A else B and ternary A if cond else B become lerp(B, A, step01(cond)). Since EML has no native conditional, eFrog emits a step01 shim into the module preamble (clamp(x * 1e30, 0, 1)). Boolean composition: and → product of selectors, or → 1 − product of complements, not → 1 - sel.
• NumPy element-wise — np.exp/sin/... map to the same EML builtins as math.*; aliases like np.maximum/minimum/arcsin/... resolve to max/min/asin/...; np.pi/np.e/np.tau inlined
• C decompiler — double f(double x) { ... } style; math.h calls; M_PI/M_E/M_SQRT2/etc. constants; compound assigns (y *= x); cast strip ((double) n); f(void) parameter lists. Uses pycparser; no preprocessor required (we strip #-lines and comments)

E5 — Java

• Java — public static double f(double x) { ... } style methods in one or more top-level classes; Math.exp/sin/... calls strip the Math. namespace; Math.PI/Math.E inlined; Math.pow(x, y) lowers to the EML ^ operator; numeric literal suffixes (f/F/d/D/l/L) and _ separators stripped; compound assigns (acc *= x) lower to a re-bound let. Instance methods and void returns are skipped/rejected with a clear message. Pure-Python parser via javalang — no JDK required.

E2.5 — JavaScript, Rust, MATLAB

• JavaScript / TypeScript — function f(x) { ... } and arrow forms const f = (x) => …. Math.exp/sin/... calls strip the Math. namespace; Math.PI/E/SQRT2/... inlined; ternaries flatten branch-free. Pure-Python esprima parser, no native deps.
• Rust — fn f(x: f64) -> f64 { … } with explicit return or trailing tail expression; let (incl. let mut) bindings; compound assigns; method-call lowering (x.exp() → exp(x), x.powf(2.0) → pow(x, 2.0)); associated-function form (f64::sqrt(x)); path constants (std::f64::consts::PI).
• MATLAB / Octave — function y = f(x) ... end; output-var binding becomes the function's tail expression; pi/e inlined; .*/.^ treated as scalar; % and # comments; ... line continuation.

E3 partial — Numerical round-trip + Lean scaffolding + per-fn profile

• --profile — per-fn chain order, transcendental count, node count, drift-risk hint (low/medium/high), and flags for div/sub (the two ops most commonly responsible for fp64 cancellation).
• --verify — re-emits the decompiled EML as runnable Python via a self-contained primitive shim (no Forge install needed), samples --samples N random inputs per parameter using sane per-name domains (sigma → positive, omega → [0, 2π], ...), runs both the original and the round-trip on every sample, and reports max relative error. PASS if every sample agrees to within 1e-9 relative. The NumPy-using examples work without numpy installed thanks to a sys.modules['numpy'] shim.
• --lean — emits a Lean 4 module per source: a def translating the EML body into Real.exp/sin/... calls, plus two theorem skeletons per function (<name>_chain_order, <name>_eml_consistent). Default output is zero-Mathlib to align with MachLib. Bodies are deliberately sorry / trivial — these are scaffolds for local review.
• --legacy-mathlib-header — opt-in compatibility mode for older Mathlib-oriented Lean projects. It is not the MachLib default.
• --genome — classifies every decompiled function against a small curated corpus of canonical math landmarks (gaussian, sigmoid, softplus, ReLU, sinusoid, polynomial, …) with a structural similarity score (Jaccard over transcendentals + helpers + binops, weighted with a chain-order penalty). The full SuperBEST corpus ships separately.

E6 — Six more languages (v0.5.0)

• Go — func f(x, sigma float64) float64 { … } with both shared (x, y float64) and per-param (x int, y float64) parameter shapes; math.Exp/Sin/Pow/... with Math. namespace strip; math.Pi/math.E/math.Sqrt2 inlined; := and var x = … bindings; numeric suffix-free literals.
• Kotlin — both expression-bodied fun f(x: Double): Double = expr and block-bodied fun f(...): Double { … } forms; kotlin.math.exp/... strip; Math.PI / kotlin.math.PI and bare PI/E from import kotlin.math.* resolved; val/var bindings.
• GDScript (Godot) — indent-based parser for func f(x: float) -> float: signatures with body parsed as a token stream; Godot globals (PI, TAU, E) inlined; pow(x, n), sqrt, sin, cos, tan, exp, log as built-ins; var x = expr lowered to a let.
• Lua — both function name(...) … end and local function name(...) … end; ^ exponentiation lowered to pow(a, b) (right-associative); math.exp/sin/... table-dispatch + math.pi / math.huge constants; local x = expr bindings.
• Julia — both block form (function f(x) … end) and one-liner assignment form (f(x) = expr); Unicode π / ℯ supported in the identifier regex; exp/sin/... and Base.MathConstants.pi resolved; let re-bindings.
• Solidity — pragma solidity ^0.8.x accepted; only pure / view functions decompiled (state-mutating ones silently skipped); require / assert / revert and unchecked { … } blocks pass through; ternary a > b ? a : b lowered to max(a, b) and a < b ? a : b to min(a, b). Useful for verifying that on-chain math kernels match an EML reference.

E3-full — BFS Lean prover (v0.6.0 + Phase 2 in v0.7.0)

--prove runs a structural BFS over a small tactic ladder and discharges both the chain-order and consistency theorems --lean was previously emitting as True := by trivial. The prover:

1. Mirrors the decompiled body to a concrete EML inductive AST in the Lean preamble (the inductive EML plus a chainOrder : EML → Nat recursor land beside Mathlib imports). v0.7 adds an eval : EML → (String → ℝ) → ℝ evaluator and an evalCall atlas covering the 18 known transcendentals.
2. Emits def <name>_eml : EML := … per function — a structural lift of the body into the add / sub / mul / div / neg / call constructors. Integer-power expansion (x ** n → x * x * … * x) for n ∈ [1, 8]. v0.7 inlines let bindings so the AST never has free occurrences of let-bound names.
3. Replaces theorem <name>_chain_order : True := by trivial with theorem <name>_chain_order : chainOrder <name>_eml ≤ N := by decide — decide reduces a closed Nat inequality.
4. v0.7 — Replaces the consistency theorem's True body with a real equality: theorem <name>_eml_consistent : ∀ args, eval <name>_eml <env_of args> = <name> args. Tactic chosen by body shape:
   • Polynomial body (no calls) → simp [eval, fn, fn_eml]; ring (confidence: proven).
   • Transcendental body (has calls) → simp [eval, evalCall, fn, fn_eml] (confidence: likely — we predict closure but don't run Lean).
   • Var-only body (f x = x) → simp [eval, fn, fn_eml] reduces by definitional unfolding (confidence: proven).
   • Unsupported shape → True := by trivial fallback.
5. --prove-report prints a per-function pass/fail summary to stderr.

For the bundled gaussian / softplus / quadratic demo: 6/6 theorems emitted with non-trivial propositions — the polynomial quadratic closes via ring, gaussian + softplus go to simp [eval, evalCall, ...]. Bodies the AST mirror can't represent (NaN literals, comparison ops in conditionals, etc.) fall back to the True := by trivial scaffold with confidence = unknown.

E5 partial — Algebraic simplifier

• --optimize — conservative bottom-up rewriter with fixed-point iteration. Safe identities only: x + 0 → x, x * 1 → x, x * 0 → 0, -(-x) → x, x + x → 2*x, pow(x, 2) → x*x, exp(0) → 1, log(1) → 0, sin(0) → 0, cos(0) → 1, sqrt(0/1) → 0/1, plus constant folding for two-literal binops. Pair with --verify to confirm the rewrite preserved every value.

E7 bridge artifacts — eFrog decompiler + Forge compiler contract

The compiler/decompiler boundary now has machine-readable artifacts:

• efrog --capabilities prints efrog_forge_capability_map_v0, including local source frontends, hosted efrog.dev frontends, Forge free/pro targets, bridge-pair statuses, and explicit non-claims.
• efrog <source> --evidence --evidence-target <target> prints efrog_forge_translation_evidence_packet_v0, including the canonical EML SHA-256 fingerprint, normalized EML shape hash, preservation class, per-function profile rows, conservative domain/stability warnings, target metadata, and claim boundaries.
• efrog <source> --normalize prints efrog_normalized_eml_shape_v0. This alpha-normalizes argument and let names, normalizes numeric literals, and sorts commutative addition/multiplication terms. It is stronger than a text hash but weaker than a theorem prover.
• efrog <source> --obligations prints efrog_domain_obligation_report_v0, a static candidate list for proof/runtime routing. It catches common edges: positive log arguments, nonnegative sqrt arguments, nonzero denominators, finite bounded exp arguments, and inverse-trig intervals.
• efrog --roundtrip-matrix --strict --out-dir <dir> runs the current strict bridge matrix. Today the strict target is Python because it can be bytecode-compiled without external toolchains. The runner checks Forge canonical formatting, compiles through Forge, bytecode-compiles generated Python, writes one evidence packet per pair, and emits roundtrip_matrix.json.
• efrog <source> --bridge-bundle --strict --out-dir <dir> writes a complete end-to-end bundle: source copy, EML, normalized shape, unresolved obligations, translation evidence packet, Lean skeleton, Forge Python target, Forge Rust target, and bridge_bundle_manifest.json. Python is bytecode-checked. Rust is standalone rustc-checked through a local eFrog compatibility shim for the small monogate_sys f64 surface used by Forge output. The canonical runtime remains Forge's monogate_sys crate. When Python and Rust are both present, the bundle also writes python_rust_equivalence.json with deterministic sampled cross-target output checks. The bundle also writes artifact_manifest.json, a SHA-256 inventory for the emitted files plus a bundle hash for tamper-evident review.
• efrog --audit-bundle <dir> recomputes the SHA-256 and byte-size entries in artifact_manifest.json, recomputes the bundle hash, and exits non-zero on missing or changed artifacts.
• efrog --bridge-guard --out-dir <dir> runs the local CI guard for the eFrog/Forge bridge: capability-map validation, strict bundle generation, bundle audit, copied-bundle tamper probe, and hosted source roundtrip matrix, plus JSON Schema validation for generated artifacts. It exits non-zero if any check fails or if the sibling Forge checkout is unavailable.
• efrog --bridge-benchmark --out-dir <dir> runs a 10-case bridge corpus through source -> EML -> Forge Python/Rust targets. The corpus includes transcendental search signals (gaussian, sigmoid, softplus, damped_wave, rc_transient), guarded branch-free rewrites (relu, clamp_guard), and standard-runtime controls (poly_horner, poly_quadratic, voltage_divider). It emits efrog_bridge_benchmark_v0 with target statuses, audit status, sampled Python/Rust equivalence metrics, unresolved obligations, and EML advantage labels. These labels are research classifications, not performance claims.
• efrog --advantage-from-bridge --out-dir <dir> generates a fresh bridge benchmark and derives efrog_eml_advantage_from_bridge_v0. The report scores each case from actual bridge evidence: pass/audit status, sampled Python/Rust equivalence, checked target pair, obligation visibility, benchmark class, and optional runtime witness registry maturity. It also writes a human Markdown report and efrog_advantage_command_feed_v0. All broad claim flags remain false: no broad EML advantage, runtime performance, or formal equivalence claim is made.
• efrog --close-obligations --out-dir <dir> generates a fresh bridge benchmark and derives efrog_obligation_closure_v0. It maps visible domain/stability obligations to runtime guard candidates, MachLib proof-route candidates, or review-only lanes, then writes JSON, Markdown, a command feed, and schema validation. It does not discharge obligations and keeps proof/safety/public-claim flags false.
• efrog --guard-witness --out-dir <dir> generates a fresh benchmark and writes efrog_runtime_guard_witness_registry_v0 plus per-family guard witness artifacts. The default registry covers nonzero denominator, positive log argument, and finite exponent stability fixtures. These are runtime witnesses, not proof or certified safety claims.
• efrog --evidence-ladder-review --out-dir <dir> generates or ingests the bridge benchmark and witness registry, then writes efrog_evidence_ladder_review_v0, Markdown, a command feed, and schema validation. This is a private/local reviewer surface for case triage, not a public approval or proof claim.
• efrog --evidence-ladder-guard --out-dir <dir> rebuilds the local reviewer artifacts and fails closed if schema validation, witness count expectations, reviewer statuses, or claim flags drift.
• efrog --holdout-trial --out-dir <dir> runs the examples/gaussian_stable.py holdout through the bridge benchmark, a finite-exponent runtime witness, and the evidence ladder reviewer. The holdout is deliberately outside the default benchmark corpus and reports fixture-level evidence only: no proof, certified safety, public benchmark, runtime performance, or formal equivalence claim is made.
• efrog --holdout-registry --out-dir <dir> runs the registered holdout sources (gaussian_stable.py, rc_decay_stable.py, stretched_exponential.py, and stable_sigmoid.py) as independent one-source trials, then writes efrog_holdout_registry_v0, Markdown, a command feed, and schema validation. It is a private comparison surface for unseen kernels, not a public benchmark or default-corpus expansion.
• efrog --validate-artifact <path> validates a single JSON artifact against the schema selected by its top-level schema field.

Machine-readable schemas for the bridge artifacts live in schemas/*.schema.json:

• efrog_forge_capability_map_v0
• efrog_forge_translation_evidence_packet_v0
• efrog_normalized_eml_shape_v0
• efrog_domain_obligation_report_v0
• efrog_forge_bridge_bundle_v0
• efrog_bundle_artifact_manifest_v0
• efrog_bundle_audit_report_v0
• efrog_python_rust_equivalence_v0
• efrog_forge_roundtrip_matrix_v0
• efrog_bridge_guard_report_v0
• efrog_schema_validation_summary_v0
• efrog_bridge_benchmark_v0
• efrog_eml_advantage_from_bridge_v0
• efrog_advantage_command_feed_v0
• efrog_obligation_closure_v0
• efrog_obligation_closure_command_feed_v0
• efrog_runtime_guard_witness_v0
• efrog_runtime_guard_witness_command_feed_v0
• efrog_runtime_guard_witness_registry_v0
• efrog_runtime_guard_witness_registry_command_feed_v0
• efrog_evidence_ladder_review_v0
• efrog_evidence_ladder_review_command_feed_v0
• efrog_evidence_ladder_guard_v0
• efrog_holdout_trial_v0
• efrog_holdout_trial_command_feed_v0
• efrog_holdout_registry_v0
• efrog_holdout_registry_command_feed_v0

This is translation evidence, not arbitrary-program correctness. The strong claim is only: for the covered fixtures, eFrog emits Forge-canonical EML and Forge can compile that EML to the checked target.

Obligations are unresolved until a later Forge, MachLib, or runtime witness discharges them.

E4 scaffolding — The math microphone

• --mic — captures --mic-duration seconds from the default input device, runs an FFT, picks the dominant non-DC bin, and emits a single-sine EML fit mic_signal(t) = A * sin(2π f t + φ) plus amplitude / phase / SNR diagnostics. Multi-tone, harmonic, and envelope decomposition land in full E4. pip install efrog[mic] pulls in numpy + sounddevice.

Coming

Full roadmap: monogate-research/products/software/efrog/ROADMAP.md.

Status

Full pytest suite green. Twelve local source frontends (Python, C, JavaScript, Rust, MATLAB, Java, Go, Kotlin, GDScript, Lua, Julia, Solidity). Loops, ternaries, branch-free conditionals, NumPy aliases, per-function profiling, sample-based numerical round-trip, Lean 4 scaffolding plus BFS prover recipes for chain-order theorem shapes, genome classification, algebraic simplification, bridge bundles, bridge audits, bridge guard, bridge benchmark corpus, single-sine audio fit, and fixed-shape vectors — Python a[i] reads (constant, loop-induction, or integer-offset indices inside bounded for loops) lift to Forge Vec<N>; return [..] lifts to a Vec<N> and return (..) to a tuple; and --verify samples vector parameters as lists and compares vector/tuple returns element-wise — all working. while loops, sum() / comprehension reductions, free-variable indices outside a loop, classes, pointers, structs, multi-output MATLAB functions, state-mutating Solidity, and non-pure functions in any language still raise honest "not supported, see ROADMAP.md" errors.

License

Apache 2.0.