ec-export

Imported from spitters/ec-export (AGENTS.md). Install upstream with npx skills add spitters/ec-export. Copyright stays with the author.

Maintenance notes

Fixture inventory and the mechanics of changing the export. Reference material for anyone modifying this repository; not needed to use the exporter.

Fixtures

What each pins

The importer is a separate Lean package; the paths below name files in it.

• otp.ec — the one-time pad.
• otpequiv.ec — the two one-time-pad games with three statements relating them: a relational judgement and two probability statements. Carried end to end in Examples/OTPEquivImport.lean.
• hoare.ec — a module with one bool global and two argument-free procedures, with the four Hoare judgements the importer accepts (one hoare and one phoare per hoarecmp comparison). Carried in Examples/HoareImport.lean.
• restr.ec — a section declaring an abstract module restricted away from a concrete module's memory, with a probability equality and an islossless implication. Carried in Examples/RestrictedImport.lean.
• functor.ec — two functors over one module type, one of them from that type to itself, applied as Exp(Neg(A)) to a section-declared abstract module, with the islossless implication passing through both. Carried in Examples/FunctorImport.lean.
• functor2.ec — a functor of two parameters over two module types, applied both to two abstract modules and to one abstract plus one concrete, with the islossless implication over each application. Also carries a functor whose two parameters share a source name: the shape EasyCrypt permits and the importer rejects. Carried in Examples/Functor2Import.lean.
• advequiv.ec — two experiments over a section-declared adversary, related by three equiv judgements whose preconditions are the adversary's footprint, the concrete module's footprint, and their conjunction: the three shapes ={glob M} reaches the export in. Carried in Examples/AdversaryEquivImport.lean.
• globimg.ec — the fourth shape. A concrete module with one var and no procedure, two functors over a section-declared adversary that read it, and one equiv per spelling of the precondition: ={glob Ret0(A)}, the footprint of the functor image, and ={glob A, glob Otp}, the two-conjunct form it must agree with. Carried in Examples/FunctorGlobImport.lean.
• nonunif.ec — one module per distribution operator the importer's EcDistr covers: dbool, dunit, dmap, dcond, and dbool \ (fun b => !b). Its distribution nodes are decoded by the golden #guards of Json.lean.
• distrbind.ec — one module per remaining EcDistr operator (dlet, the independent product (`*`), dscale, drestrict), plus two games whose lambda binder carries the source name of a program variable, one shadowing it and one not. The two denote different distributions, which is what makes the binder's stamp load-bearing. Carried in Examples/DistrBindImport.lean.
• ints.ec — integer literals, addition, both comparisons, a global at int, and a lemma whose probability event compares an integer result with an integer literal. Its nodes are decoded by the golden #guards of Json.lean and FormJson.lean.
• maps.ec — the finite-map operations: empty, binding a key, membership, and lookup with oget and with an explicit default, plus a global at a map code written in one module and read in another.
• loops.ec — two modules at the bounded while idiom the importer recognises and eight that differ from it in one respect each: the bound is a variable, the initialisation is missing, is of another variable or is not an integer assignment, the body does not increment or increments twice, the guard is not strict, and the body contains a call.
• multiarg.ec — the procedure-signature contract: a two-formal procedure, a one-formal procedure whose argty is not a 1-tuple, a call site passing one expression per formal, and a module type's anonymous formal.
• subtypewit.ec — a subtype's nonemptiness obligation in both places EasyCrypt puts it: spliced into the declaring scope for a subtype t, and in the subtheory C for a subtype t as C. Both are in scope at once, so the reference has to be resolved rather than assumed. A plain abstract type beside them carries a null subtype.
• opas.ec — the axioms an op binds beside the operator, in both positions: a refinement's as clause, an axiomatized by clause, a [lossless] tag and a second name, all at the top level, and the same refinement inside a theory. The section at the end is open at no declaration, so it separates a declaration's position from the presence of a section elsewhere in the file.
• clone.ec — the three clone shapes: an abstract theory exported as its compiled items (mode: "abstract"), a clone … as … whose inline override is substituted in and whose realize flips the cloned axiom to Lemma, and a clone include whose spliced items land at the top level under a rename clause with the override-inlined names gone.
• tcinstance.ec — the three shapes of a type-class instance and the two routes one reaches the output by. A ring over int, a boolean ring over bool and a field over real, each in its own theory, with the operator sets varied so that every optional operator is pinned present in one and absent in another; the General instances the algebraic hierarchy binds beside each; and an abstract theory carrying a ring instance, clone included at the top level, where the instance has no name to look up and is read out of the scope.
• sectiondecl.ec — a section with declare module inside a named theory, the PRF/ROM idiom: the theory's expansion carries the section-generalised lemma with its GTmodty binder, and section_local stays empty.
• datatype.ec — the three bodies that carry a constructor list. A datatype with a nullary and an argument-taking constructor, a datatype polymorphic in two parameters, a record, and an inductive predicate whose second clause binds a variable of its own and carries three premises; a recursive operator over the first datatype, so its OP_Fix case tree and the constructors it branches on are pinned together; and the same declarations inside a theory.
• topinstance.ec — the two global actions that produce an item without naming one. A top-level instance ring, which binds four items the exporter reads out of the scope, and a clear naming a theory and a subtheory of it, whose items are exported in full before the Th_clear that names them.
• forms.ec — a statement per f_node constructor reachable from the surface syntax. Its exception declaration is a non-exported global action, so it exits non-zero; the realize its subtype needs is tallied.
• unsupported.ec — the escape hatch on an operator body: an exception inside a theory, which reaches the export as an OP_Exn operator item rather than through the global-action walk globals.ec pins. A datatype and a recursive operator over it sit beside it, exported.
• globals.ec — the boundary of the global-action walk: a notation and an exception on the Unsupported side; an abbreviation, a theory and a theory clone on the exported side; a section, a setting, a hint and the proof scripts on the tallied side.

Adding a fixture

1. Write tests/<name>.ec, opening with a comment saying which export shape it pins and why that shape is hard.
2. Add the export rule and the diff rule to tests/dune, with the intended exit code.
3. Generate the golden: dune runtest --auto-promote.
4. Add a row to the table above and an entry under "What each pins".

A fixture the importer consumes is named by the Lean file that carries it, so that a change to the export surfaces as a failure there rather than only as a golden diff.

How dune runtest is wired

Per fixture: one rule exporting to <name>.actual.json, and one (diff <name>.expected.json <name>.actual.json) rule on the runtest alias.

The exporter runs under (chdir %{workspace_root} …) so the input path is tests/<name>.ec and the envelope's source field matches the goldens, which are generated by the root-relative command.

Each fixture's intended exit code is part of its rule, so a wrong exit code is a failure and the intended one is not. The three fixtures carrying an unsupported construct run without --allow-unsupported under (with-accepted-exit-codes 1 …); the exporter writes its output before exiting non-zero, so their output is compared like every other fixture's. The other twenty-one run under (with-accepted-exit-codes 0 …).

Regenerating after an EasyCrypt upgrade

An identifier's stamp is EcIdent.tag, a counter over every identifier the process creates, including those from the required theories. It is reproducible for a fixed EasyCrypt installation, and only its distinctness carries meaning, so every golden carrying a binder needs regenerating after an upgrade.

The envelope's ec_theories_digest is what such an upgrade shows up in; see docs/SCHEMA.md.