#LunaFlow

#Features

• A funnel, not a mode switch
  --level 1|2|3 is cumulative and --funnel runs all three. L1 deduplicates its findings, L2 splits its results into confirmed and new, and L3 is applied only to functions with an L1/L2 finding plus every function that already carries a contract. Functions escalated without a contract are reported as specification gaps — the funnel's explicit to-do list. When a target has no annotations, L3 reports 0 VCs and the gaps, not invented proofs.

• A control-flow graph you can argue with
  The CFG is built from the parsed statement tree: branch nodes with true and false edges, loop heads with back edges, merge points, and dead nodes for statements after an unconditional exit. Execution paths come from the trace and are rendered beside the diagram. Dead code and unreachable nodes are static findings; non-termination is a static + dynamic finding; path coverage is dynamic and exact only for the executed trials. Each finding carries its method and confidence.

• Taint with stated rules
  Sources are entry-function parameters (and @env.args when the frontend sees it). Propagation follows recorded definitions and the variables each statement read; array reads inherit container taint; length() inherits receiver taint; a tainted loop condition taints the numeric loop counters (implicit flow). Sinks are array indices and allocation sizes. The rules and their imprecision — field- and index-insensitive, no alias analysis, depth-6 calls, unsupported match arms — are printed in every report.

• Values at every point
  L1 records every def event keyed by function, source line and variable, so report §6.1 is a per-program-point value table and the JSONL trace has the full stream. L2 adds may-ranges from the abstract fixpoint. The distinction is explicit: observed samples are not a proof, and the abstract interval is an over-approximation at widening.

• Slices over the trace
  The dynamic dependence graph is built from def/cond/index/call events. Backward slicing walks to sources, forward slicing walks to sinks and returns. Criteria are <var>@<fn>, <fn>:<line> or a bare <var>. A slice is exact for the recorded trace, not a static closure; --function ensures the target function is executed before slicing.

• Contracts that admit ignorance
  Specifications are MoonBit comments: //@ requires, //@ ensures, //@ invariant, //@ assigns. L3 generates WP-style verification conditions for index bounds, allocation sizes, division, assertions and postconditions at every return and tail expression. Each VC is proved, failed or unknown; unknown is an honest third state, not a failure. This is a three-state interval prover, not an SMT-backed WP.

• Markdown is the UI
  Reports use flowchart TD for CFGs and slices, flowchart LR for taint and the funnel. Labels are sanitized, node counts are capped (8 CFGs, 90 nodes per diagram, 40 taint/slice nodes), and every node and table row carries a file:line. The artifacts are diff-friendly and render on GitHub, GitLab and VS Code.

• Version pinning you can reproduce
  A bare coordinate or @latest is resolved once by moon fetch, then pinned: the report records the resolved version, the source root (.repos/<author>/<module>/<version>) and the declared target. The analyzer never compiles the target, so heavy modules are analyzable without their dependencies. The optional Cobertura bridge is the only path that needs a buildable target.

#What you get

#Install

moon add riantr/LunaFlow@0.1.3

import {
  "riantr/LunaFlow@0.1.3",
}

///|
import {
  "riantr/LunaFlow/src/app",
}

Cannot find import 'riantr/LunaFlow/src/app@0.1.0' in my/app/src/thing@0.1.0

///|
import {
  "riantr/LunaFlow/src/app" @lf,
}

moon run src/cli -- analyze <author>/<module>[@<version>|@latest]

#What the release was checked on

moonx riantr/LunaFlow@latest riantr/LunaFlow@latest

moonx riantr/LunaFlow/src/cli@latest analyze riantr/LunaFlow@latest

moon run src/cli -- analyze --dir .

#What changed in 0.1.1

#What changed in 0.1.0

• A hostile module could abort the process. 5,000 nested if statements and 2,000 nested parentheses exhausted the native stack (0xC0000409, STATUS_STACK_BUFFER_OVERRUN). The parser now refuses constructs nested deeper than 256 levels and records them as a parse gap instead: the region is skipped whole and counted as one unsupported statement, so the frontend-coverage number in the report stays honest rather than reading 100 % on a file that was skipped. This is pinned by hardening_test.mbt and by scripts/qa/depth_sweep.mjs.
• A hostile module could steer the report path. The output file name is built from the analysed module's own moon.mod, and only / was neutralised, so a version field of ..\..\..\..\escaped wrote the report, the trace and the summary into an arbitrary directory. The stem now goes through a whitelist sanitiser, and scripts/qa/path_traversal.mjs is the regression.
• A --dir scan could describe someone else's code. The source walker skipped _build, .git, .repos, target and node_modules, but not .mooncakes — the directory the toolchain vendors a module's dependencies into. A self-scan of this repository therefore reported 384 parsed files, 362 of them from the vendored moonbitlang/async module: every file, function and statement count in that report described a third party's code. .mooncakes is skipped as well now, and scripts/qa/vendor_isolation.mjs plants one file behind every skipped directory name and asserts that exactly the module's own source is parsed.

• The version was scanned out of the moon fetch log, which is free-form text whose shape differs between platforms. On Linux the scan took everything up to the next " to " and produced the version 0.164.64\nSuccess\nSuccessfully fetched … — a name that matches no directory. The analyzer then read an empty tree and reported 0 statements, 0 coverage, 0 findings, exit 0. The filesystem is now the authority: the version is cut at the first character that cannot be part of a version, and a candidate is only accepted when the directory it names really exists.
• The harness looked for the built CLI under the wrong name. The MoonBit native target names the executable cli.exe on every platform, Linux included, where the file is an ELF binary with a Windows extension. The resolver picked the name by platform, so on the runner the CLI never ran and the failure surfaced three steps later as a missing output file.
• The vendored-tree regression asserted the wrong thing. It checked that the report does not contain the string _build/, but the report records the analysed root and the harness's scratch directory lives under _build/. It now asserts on ingested content — a foreign file name and a foreign function — and it was checked against a reverted fix to prove it can go red.

#Packages and targets

#Layout

LunaFlow.png               the mark this README shows
LunaFlow_Logo.png          the same artwork at 1024x1024
LICENSE                    MIT
moon.mod                   module metadata (native target)
src/app/                   14 library files: parser, CFG, L1 interpreter,
                           L2 abstract interpreter, L3 contracts, funnel,
                           taint/slice, report renderer
src/app/*_test.mbt         37 tests in 7 files
src/cli/main.mbt           async native CLI
fixtures/vuln_demo/        taint / dead-code / infinite-loop / contract fixture
features/                  acceptance scenarios in Gherkin
docs/design.md             design, comparison, acceptance criteria (A1-A18)
docs/qa/REPORT.md          deep QA report (security, coverage, metrics)
reports/                   generated reports for the validation modules
scripts/verify.mjs         dependency-free acceptance checker
scripts/qa/                dependency-free QA harnesses

#Verification

#What this is not

• Not sound. L1 reports what happened on synthesized inputs. L2 reports what the abstract input set cannot exclude. L3 proves individual VCs from specifications. Absence of a finding is never a proof.
• Not a full MoonBit frontend. Unsupported syntax is measured and reported (0.13 % of statements on doubleML, 2.68 % on static_analysis). Expression and statement nesting beyond 256 levels is refused as a recorded parse gap rather than risked on the native stack.
• Not alias-aware. Taint is field- and index-insensitive, with a depth-6 interprocedural cutoff; loop-counter implicit taint is deliberately conservative and can over-report.
• Not trace-complete. Slices and ranges cover the recorded trace only. Function names are not package-qualified, so a name-only criterion can match several packages (three packages define render_reports in static_analysis).
• Not SMT-backed. L3 is a WP-style VC generator with an interval decision procedure. Loop invariants are not yet placed per loop, so loop-dependent goals are havocked to unknown. The //@ syntax is ACSL-inspired but adapted to MoonBit comments; ACSL itself targets C.
• Not a database. Reports, traces and summaries are plain files: diffable, human-readable, reproducible. riantr/tesseract was evaluated as a storage dependency — 0.1.17 raises the durable-memory ceiling to 9999 entries, but its dependency footprint is ~28 MB, so it is not adopted. If cross-run queries are needed, an optional SQLite sidecar is the smaller change.

#Quick Start

# analyze a published module; @latest is resolved once and pinned
moon run src/cli --target native -- analyze riantr/moonbit_doubleML@latest --out reports

# the full funnel, with a slice on a variable
moon run src/cli --target native -- analyze riantr/moonbit_doubleML@latest \
  --out reports --funnel --slice "theta_hat@aggregate_coef_se"

# a local checkout, no registry resolution
moon run src/cli --target native -- analyze --dir fixtures/vuln_demo \
  --out reports --funnel --slice "i@copy_prefix"

# focus on one function in a large module
moon run src/cli --target native -- analyze riantr/moonbit_static_analysis@latest \
  --function render_reports --slice "buf@render_reports" --out reports

# compiled coverage, when the target builds
moon coverage analyze
moon coverage report -f cobertura -o cov.xml
moon run src/cli --target native -- analyze <coord> --coverage cov.xml --out reports

#Example

L1 concrete: 12 findings
L2 abstract: 11 findings, 4 new
L3 contracts: 2 proved / 1 failed / 3 unknown

flowchart LR
  L1["L1 concrete: 12 findings"] -->|"dedup, escalate"| L2["L2 abstract: 11 findings, 4 new"]
  L2 -->|"critical functions"| L3["L3 contracts: 2 proved / 1 failed / 3 unknown"]

#Gates and drift detectors

• moon test pins the fixture's static findings: 3 dead, 1 unreachable, 1 infinite loop, and the L3 proved/failed/unknown split.
• scripts/verify.mjs fails on missing sections, invalid Mermaid structure, empty slices, missing L2/L3 counters, coverage below 95 %, or a runtime above 60 s.
• scripts/qa/gherkin.mjs states the acceptance criteria as executable scenarios, including the two hostile-input regressions.
• docs/design.md §10 lists the quantified acceptance table (A1–A18); the measured column is updated from real runs, not from intent.
• Determinism: two runs produce identical summary.json except elapsed_ms, and a byte-identical trace.

#Used By

• src/cli — the executable in this module, the command line over the same library.
• scripts/qa/ — seventeen dependency-free harnesses and tools; eleven of them drive the built binary as a real process against the fixture, the two registry modules and a hostile-input corpus.
• docs/design.md — the design record for the implementation in src/app.

#Attribution

• License: MIT (see LICENSE).
• The documentation layout of this README follows the riantr/tesseract module, whose release notes are a model of stating exactly what changed and what did not.
• The comparison baseline in docs/design.md §8 covers Frama-C / TrustInSoft Analyzer, Joern, CodeQL, SVF and Soot. Every place this module answers differently from those tools is a stated limitation in What this is not, not an omission.