Metadata-Version: 2.4
Name: efrog
Version: 0.8.0
Summary: Supported source frontends to Forge-compatible EML — eFrog is Forge spelled backwards.
Author-email: "Arturo R. Almaguer" <almaguer1986@gmail.com>
License: Apache-2.0
Project-URL: Homepage, https://monogateforge.com
Project-URL: Source, https://github.com/agent-maestro/efrog
Keywords: eml,decompiler,monogate,forge,symbolic,ast
Classifier: Development Status :: 3 - Alpha
Classifier: Intended Audience :: Developers
Classifier: License :: OSI Approved :: Apache Software License
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.10
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Topic :: Software Development :: Compilers
Classifier: Topic :: Scientific/Engineering :: Mathematics
Requires-Python: >=3.10
Description-Content-Type: text/markdown
Requires-Dist: pycparser>=2.21
Requires-Dist: esprima>=4.0
Requires-Dist: javalang>=0.13
Provides-Extra: dev
Requires-Dist: pytest>=8; extra == "dev"
Requires-Dist: pytest-xdist>=3.5; extra == "dev"
Requires-Dist: jsonschema>=4.0; extra == "dev"
Provides-Extra: mic
Requires-Dist: numpy>=1.21; extra == "mic"
Requires-Dist: sounddevice>=0.4; extra == "mic"

# 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](https://monogateforge.com) — the same intermediate language
[Monogate Forge](https://github.com/agent-maestro/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)

```bash
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:

```eml
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

| Phase | What | When |
|-------|------|------|
| E3-Lean | Hosted Lean runner — actually invoke `lake build` to confirm `likely` proofs close | month 4–6 |
| E4-full | Multi-tone / harmonic / envelope decomposition | month 6–8 |
| E5-full | Broader optimizer pipe (CSE, trig identities) | month 6–8 |
| E7 | Sensor expansion (camera / stethoscope / ...)       | month 8+ |

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.
