Work on adding benchmarks based on the Rocq standard library.

.gitignore

@@ -58,6 +58,10 @@ results/
 !benchmarks/plots/**
 !benchmarks/results/
 !benchmarks/results/**
+!benchmarks/stdlib/plots/
+!benchmarks/stdlib/plots/**
+!benchmarks/stdlib/results/
+!benchmarks/stdlib/results/**
 benchmarks/flame_trends/
 
 # Local profiling and packaging artifacts.

benchmarks/README.md

@@ -53,3 +53,16 @@ python3 bench.py plot rewrite_nm --fixed m=3
 ## Adding a Benchmark
 
 Create `benchmarks/my_benchmark.py` with a class extending `Benchmark`. The registry, CLI, and plotter pick it up automatically.
+
+## Rocq standard-library benchmark
+
+A separate, fixed-corpus suite comparing MEngine vs Rocq on auto-translated
+stdlib lemmas lives under [`stdlib/`](stdlib/README.md). It is driven by its own
+runner (it iterates a manifest rather than sweeping a parameter range):
+
+```bash
+python3 stdlib/stdlib_bench.py regen     # rebuild every generated file (translate, time, report)
+python3 stdlib/stdlib_bench.py test      # faithfulness gate
+python3 stdlib/stdlib_bench.py fidelity  # statement vs the real stdlib
+python3 stdlib/stdlib_bench.py clean     # remove generated files
+```

benchmarks/config.json

@@ -11,6 +11,14 @@
   "max_consecutive_failures": 2,
   "trials": 2,
   "coq_timeout_multiplier": 1.5,
+  "stdlib": {
+    "corpus_dir": "stdlib/corpus",
+    "compat": "stdlib/compat/stdlib_compat.me",
+    "results": "stdlib/results/stdlib.json",
+    "plots_dir": "stdlib/plots",
+    "timeout": 20,
+    "trials": 10
+  },
   "mengine_variants": {
     "baseline": {
       "path": "~/mengine/build/ablations/mengine-baseline",

benchmarks/stdlib/README.md

@@ -0,0 +1,136 @@
+# Rocq standard-library benchmark for MEngine
+
+Per-module benchmark comparing **MEngine** against **Rocq** on a curated,
+mechanically-translated subset of the Rocq standard library. Each unit is one
+stdlib **module** — a `.v` file grouping that module's lemmas, mirroring the
+library's own file structure.
+
+| Module  | Source                                              |
+|---------|-----------------------------------------------------|
+| `Bool`  | `Coq.Bool.Bool`                                     |
+| `Lists` | `Coq.Lists.List` (app/length/map/rev over `list A`) |
+| `Logic` | `Coq.Init.Logic` (eq, and/or, ex)                   |
+| `Nat`   | `Coq.Init.Nat` (inductive arithmetic, max/min)      |
+| `Peano` | `Coq.Init.Peano` (the `le` order)                   |
+
+## Layout
+
+```
+benchmarks/stdlib/
+  translate.py             Rocq .v -> MEngine .me translator (via Rocq `Set Printing All`)
+  stdlib_bench.py          runner: test / fidelity / clean / regen
+  report.py                markdown table + log-log scatter plot
+  fidelity.py              statement-vs-stdlib correspondence check (via Rocq's kernel)
+  compat/stdlib_compat.me  compat prelude: nat/bool/list/option + pred/max/min/le + emulated tactics
+  corpus/
+    manifest.json          locked corpus + per-statement digests + excluded boundary
+    stdlib_map.json         each curated lemma -> its real stdlib counterpart + per-module file(s)
+    <Module>/rocq.v         benchmarked Rocq source (hand-curated)
+    <Module>/mengine.me     auto-translated MEngine source
+  results/                 generated: stdlib.json (timings) + REPORT.md (table)
+  plots/stdlib_scatter.png generated scatter
+```
+
+## Usage
+
+```bash
+cd benchmarks
+python3 stdlib/stdlib_bench.py regen     # rebuild every generated file, in dependency order
+python3 stdlib/stdlib_bench.py clean     # remove every generated file (keep sources)
+python3 stdlib/stdlib_bench.py test      # faithfulness gate (see below)
+python3 stdlib/stdlib_bench.py fidelity  # check each statement vs the real stdlib
+```
+
+`regen` rebuilds every generated file from source in order (mengine.me ->
+manifest -> run -> report); `clean` removes them. Hand-authored sources
+(`rocq.v`, `stdlib_map.json`, the compat prelude) are never touched. `test` and
+`fidelity` check that the benchmarks are consistent between Rocq and MEngine
+and relate to the actual standard library, respectively.
+
+
+## Translation (`Set Printing All`)
+
+MEngine has no notation system and no elaboration, so notation, implicits, and
+numeric literals must all be made explicit. Rather than re-implement Rocq's
+elaborator, `translate.py` replays each unit through Rocq with `Set Printing All`
+and translates the fully-explicit, notation-free form it prints (so a working
+`coqc`/`rocq`, `--coq`, is required):
+
+```
+(* surface *)      forall (A:Type) (l:list A), nil ++ l = l
+(* Printing All *) forall (A : Type) (l : list A), @eq (list A) (@app A (@nil A) l) l
+(* MEngine *)      forall (A : Type), forall (l : (list A)), (((eq (list A)) (((app A) (nil A)) l)) l)
+```
+
+Every implicit is supplied by Rocq, so no type synthesis is needed. Terms inside
+*tactics* are still translated from surface source. The guiding principle is
+**flag, never guess**: any construct it cannot translate soundly is reported and
+the unit excluded, never mistranslated (a wrong translation that happened to
+compile would silently benchmark two *different* theorems).
+
+## Timing
+
+`run` times each unit end-to-end in both engines (whole process, best of N).
+Both pay a fixed startup — MEngine loads `prelude/tactics.me` + compat, Rocq
+loads its prelude — which at this problem size dominates the whole-file number.
+To isolate proof cost, `run` also times each engine's preamble *alone* as a
+startup floor: for Rocq, each module's Require/Import commands,
+and for MEngine, the statements in the preamble.
+`report` subtracts each module's floor (clamped at zero).
+A residual at or below the floor's run-to-run jitter is reported `~0`.
+
+`plots/stdlib_scatter.png` plots each module's own-floor-subtracted proof
+time (Rocq x vs MEngine y, log-log, parity `y = x`) — the same pair as its
+REPORT.md row. Whole-file time would be dishonest: `Lists`' one-time `List` load
+would drop it below any single parity line and read as an MEngine win, when on
+proof cost MEngine is actually *slower* on `map`/`rev` induction. Whiskers run to
+the slowest trial; shaded bands at each engine's startup-noise floor (the std-dev
+of its baseline trials) mark where a residual stops being trustworthy.
+
+## `test` — faithfulness gate
+
+Per unit, before any timing:
+
+- `rocq.v` compiles under `coqc`.
+- `mengine.me` runs clean under `mengine -q` (compat prelude prepended).
+- `mengine.me` is exactly what `translate.py` re-emits from `rocq.v` (no drift),
+  with matching theorem names.
+
+Needs `coqc` on `PATH` (or `coq_path` in `config.json`).
+
+## `fidelity` — statement vs the real stdlib
+
+`test` checks that `.me` faithfully follows `.v`; it does **not** check that the
+hand-curated `.v` statement matches the stdlib lemma it claims to be.
+`fidelity` closes that gap with Rocq's own kernel:
+`corpus/stdlib_map.json` records each module's source file(s) and
+maps every lemma to a stdlib ref. The ref is qualified with the file (`andb_diag`
+→ `Stdlib.Bool.Bool.andb_diag`) and checked by `Check (<file>.<ref> :
+<curated statement>).`, which passes iff the lemma both belongs to that file and
+is convertible to the curated one. An unmapped lemma, a stale map entry, a
+missing/absent ref, or a non-convertible match all fail (non-zero exit). Because
+it shells out to `coqc` once per lemma it is slower than `test` and kept separate;
+run it after editing any statement or the map.
+
+## Scope
+
+The computational/structural corner reachable by MEngine + the compat prelude:
+
+- **Bool** — identities by ground reduction and single-variable `destruct`.
+- **Nat** — `add`/`mul`/`sub` reductions and computational induction over the
+  `add`/`mul` fixpoints (the full additive/multiplicative theory up to
+  `mul_assoc` and both distributive laws), plus the `max`/`min` identities.
+- **Lists** — parametric `list` induction: `app`/`length` plus the `map`/`rev`
+  theory (`map_app`, `map_map`, `rev_app_distr`, `rev_involutive`, …).
+- **`le` / order** — structural induction with a fixpoint-free motive.
+- **Logic** — propositional introduction (`split`/`left`/`right`/`apply`).
+- **Polymorphic `eq` / `ex`** — over an arbitrary type, unlocked by the
+  `Set Printing All` elaboration supplying the implicit type argument.
+
+## Why not verbatim stdlib files
+
+Running the translator over the installed stdlib per file, essentially none
+translate whole, even in `Coq.Init`: real files are saturated with
+`Notation`/`Ltac`/`Variant`/`Register`/multi-scrutinee `match`/qualified names.
+Hence the corpus is curated lemmas drawn from stdlib content, grouped one file
+per module to mirror the library's structure.

benchmarks/stdlib/compat/stdlib_compat.me

@@ -0,0 +1,215 @@
+(* stdlib_compat.me — compatibility prelude for the Rocq-stdlib benchmark.
+
+   Loaded ahead of every translated unit (the translator prepends it).  It
+   supplies the base datatypes and functions that the Rocq standard library
+   assumes but that MEngine's C core (src/runtime/core.c) does not provide
+   (core.c only defines eq/and/or/ex/Reflexive), plus a handful of emulated
+   tactics written in the tactic language.
+
+   Each datatype/function mirrors the *semantics* of its Rocq counterpart so
+   that a translated theorem statement denotes the same proposition and ground
+   computation reduces identically.  Function bodies use single-scrutinee
+   matches (MEngine has no multi-scrutinee match); this is extensionally equal
+   to Rocq's definitions, which is all the benchmark requires.
+
+   Every emulated tactic carries a comment stating exactly how it differs from
+   Rocq's, so divergence is auditable in one place. *)
+
+(* ── Base datatypes ─────────────────────────────────────────────────── *)
+
+Inductive True : Prop := | I : True.
+
+Inductive bool : Type := | true : bool | false : bool.
+
+Inductive nat : Type :=
+| O : nat
+| S : forall (n : nat), nat.
+
+(* list/option take A as a *parameter* (not an index): MEngine then generates the
+   Rocq-shaped parametric eliminator
+     list_ind : forall (A : Type) (P : list A -> Prop),
+                  P (nil A) -> (forall x l, P l -> P (cons A x l)) -> forall l, P l
+   so `induction` on a list translates to `apply (list_ind A <motive>)`.  The
+   constructor types are identical to the index form (the parameter is just a
+   leading forall), so every statement and the app/length fixpoints are unchanged. *)
+Inductive list (A : Type) : Type :=
+| nil  : list A
+| cons : forall (x : A), forall (l : list A), list A.
+
+Inductive option (A : Type) : Type :=
+| None : option A
+| Some : forall (x : A), option A.
+
+(* ── bool functions (Coq.Init.Datatypes) ───────────────────────────── *)
+
+Definition negb : forall (_ : bool), bool :=
+  fun (b : bool) => match b with | true => false | false => true end.
+
+Definition andb : forall (_ : bool), forall (_ : bool), bool :=
+  fun (b1 : bool) => fun (b2 : bool) => match b1 with | true => b2 | false => false end.
+
+Definition orb : forall (_ : bool), forall (_ : bool), bool :=
+  fun (b1 : bool) => fun (b2 : bool) => match b1 with | true => true | false => b2 end.
+
+Definition implb : forall (_ : bool), forall (_ : bool), bool :=
+  fun (b1 : bool) => fun (b2 : bool) => match b1 with | true => b2 | false => true end.
+
+Definition xorb : forall (_ : bool), forall (_ : bool), bool :=
+  fun (b1 : bool) => fun (b2 : bool) =>
+    match b1 with
+    | true  => match b2 with | true => false | false => true end
+    | false => b2
+    end.
+
+(* ── nat functions (Coq.Init.Nat) ──────────────────────────────────── *)
+
+Fixpoint add (n : nat) (m : nat) {struct n} : nat :=
+  match n with | O => m | S p => S (add p m) end.
+
+Fixpoint mul (n : nat) (m : nat) {struct n} : nat :=
+  match n with | O => O | S p => add m (mul p m) end.
+
+(* sub: Rocq matches on both n and m; here nested single-scrutinee matches. *)
+Fixpoint sub (n : nat) (m : nat) {struct n} : nat :=
+  match n with
+  | O => O
+  | S k => match m with | O => n | S l => sub k l end
+  end.
+
+Fixpoint eqb (n : nat) (m : nat) {struct n} : bool :=
+  match n with
+  | O => match m with | O => true | S q => false end
+  | S p => match m with | O => false | S q => eqb p q end
+  end.
+
+Fixpoint leb (n : nat) (m : nat) {struct n} : bool :=
+  match n with
+  | O => true
+  | S p => match m with | O => false | S q => leb p q end
+  end.
+
+Definition ltb : forall (_ : nat), forall (_ : nat), bool :=
+  fun (n : nat) => fun (m : nat) => leb (S n) m.
+
+(* pred (Coq.Init.Nat): predecessor, with pred O = O. *)
+Definition pred : forall (_ : nat), nat :=
+  fun (n : nat) => match n with | O => O | S k => k end.
+
+(* max/min (Coq.Init.Nat): Rocq matches on both n and m; here nested
+   single-scrutinee matches, extensionally identical (the `S p, O` arm returns
+   the outer scrutinee `n` = `S p`, exactly as Nat.max/Nat.min do). *)
+Fixpoint max (n : nat) (m : nat) {struct n} : nat :=
+  match n with
+  | O => m
+  | S p => match m with | O => n | S q => S (max p q) end
+  end.
+
+Fixpoint min (n : nat) (m : nat) {struct n} : nat :=
+  match n with
+  | O => O
+  | S p => match m with | O => O | S q => S (min p q) end
+  end.
+
+(* ── list functions (Coq.Lists.List / Coq.Init.Datatypes) ──────────── *)
+
+Fixpoint app (A : Type) (l : list A) (k : list A) {struct l} : list A :=
+  match l with
+  | nil _ => k
+  | cons _ x xs => cons A x (app A xs k)
+  end.
+
+Fixpoint length (A : Type) (l : list A) {struct l} : nat :=
+  match l with
+  | nil _ => O
+  | cons _ x xs => S (length A xs)
+  end.
+
+Fixpoint map (A : Type) (B : Type) (f : forall (_ : A), B) (l : list A) {struct l} : list B :=
+  match l with
+  | nil _ => nil B
+  | cons _ x xs => cons B (f x) (map A B f xs)
+  end.
+
+(* rev: Coq.Lists.List's naive reverse, rev (x :: xs) = rev xs ++ (x :: nil). *)
+Fixpoint rev (A : Type) (l : list A) {struct l} : list A :=
+  match l with
+  | nil _ => nil A
+  | cons _ x xs => app A (rev A xs) (cons A x (nil A))
+  end.
+
+(* ── Relational predicates (Coq.Init.Peano / Coq.Init.Datatypes) ───── *)
+
+(* le, as in Coq.Init.Peano: le n n and le n m -> le n (S m). *)
+Inductive le : forall (_ : nat), forall (_ : nat), Prop :=
+| le_n : forall (n : nat), le n n
+| le_S : forall (n : nat), forall (m : nat), forall (_ : le n m), le n (S m).
+
+(* ── Emulated tactics ──────────────────────────────────────────────── *)
+
+(* reflexivity (override): build `eq_refl A x` for a goal `eq A x y` and let
+   the kernel's conversion checker verify `x` converts to `y`.  Differs from
+   the prelude's reflexivity, which matches `eq ?A ?x ?x` purely syntactically
+   (pointer equality) and so cannot close a goal whose two sides are equal only
+   up to computation, e.g. `eq nat (add (S O) O) (S O)`.  Like Rocq's
+   `reflexivity`, it fails (cleanly) when the sides are not convertible. *)
+Tactic reflexivity := match Goal with
+| [ |- (((eq ?A) ?x) ?y) ] => exact ((eq_refl A) x)
+end.
+
+(* symmetry := apply eq_sym.  eq_sym : forall A x y, eq A x y -> eq A y x, so
+   applying it to `eq A y x` leaves the subgoal `eq A x y`.  Identical to Rocq. *)
+Tactic symmetry := apply eq_sym.
+
+(* simpl := cbv (full beta/delta/iota/fix normalization).  Rocq's simpl is a
+   heuristic partial reduction that avoids unfolding some applications; cbv is
+   strictly more aggressive but agrees with simpl whenever simpl makes progress
+   on the closed/structural goals in this corpus. *)
+Tactic simpl := cbv.
+
+(* trivial / easy / now : close trivial goals.  Rocq's are stronger (trivial
+   runs a hint database; easy/now also discharge by `congruence`/`lia`-free
+   automation).  Here: try reflexivity, then try assumption. *)
+Tactic trivial := try reflexivity; try assumption.
+Tactic easy := intros; try reflexivity; try assumption.
+Tactic now := intros; try reflexivity; try assumption.
+
+(* constructor (sec. 6a): generalization of split/left/right.  One arm per
+   inductive whose constructors this corpus uses.  `first` tries them in
+   declaration order, exactly like Rocq's `constructor`.  Each arm builds a
+   full proof term, so this stays sound under flag-never-guess.  Witness-guessing
+   (constructor on `ex`, i.e. eexists) is intentionally excluded. *)
+Tactic constructor := match Goal with
+| [ |- True ]            => exact I
+| [ |- ((and ?A) ?B) ]   => eapply ((conj A) B)
+| [ |- ((or ?A) ?B) ]    => first [ eapply ((or_introl A) B) | eapply ((or_intror A) B) ]
+| [ |- ((le ?n) ?m) ]    => first [ eapply (le_n n) | eapply (le_S n) ]
+end.
+
+(* f_equal (approximation): reduce a goal `eq T (h .. a) (h .. b)` to its
+   differing-argument subgoals, discharging the unchanged layers by reflexivity.
+   Built on the kernel congruence `Bad_App_Congruence : forall A B (f g : A -> B)
+   (x y : A), f = g -> x = y -> f x = g y` — the *same* congruence the prelude's
+   `rewrite` is built on — so it adds no new trust.  One application layer of the
+   goal becomes two subgoals, `eq (A -> T) f g` (the function) and `eq A x y`
+   (the argument); `try reflexivity` closes the layers that didn't change and the
+   recursive `try f_equal` peels nested applications, so `f_equal` on
+   `cons A a X = cons A a Y` leaves exactly `X = Y`.
+
+   How it differs from Rocq's `f_equal`: it peels exactly one application layer
+   and reads the head `?f`/`?g` off the goal first-order (no higher-order
+   unification).  `try reflexivity` discharges the function subgoal when the head
+   is unchanged (the common case — `cons A a`, `S`) and the argument subgoal when
+   the arguments are convertible, leaving any genuinely-different argument as the
+   single remaining goal.  It deliberately does **not** recurse into that
+   argument subgoal: an argument that is itself a compound application (e.g.
+   `app A l (app A m n)`) is the proof obligation to discharge (here, by the
+   induction hypothesis), not a congruence to peel further — recursing there
+   would manufacture false subgoals.  So this is a single-layer structural
+   congruence adequate for the `cons`/`S` goals an induction step produces, not a
+   general multi-argument `f_equal`.  A bare `f_equal` on a non-application
+   equality fails (no match arm), as Rocq's does. *)
+Tactic f_equal := match Goal with
+| [ |- (((eq ?T) (?f ?x)) (?g ?y)) ] =>
+  let A := type_of x in
+  apply ((((((Bad_App_Congruence A) T) f) g) x) y); try reflexivity
+end.