Speed up requiring large machine-generated theories

[bgregoir]

Two independent savings on the cost of require-ing a large
machine-generated theory. No user-visible behaviour change.

Reproducing

Jasmin extractions of constant tables are the workload that made this
visible: a few very large op bodies, whose elements are negative
word literals (Jasmin extracts bytes signed). This generates a file
of that shape — 20 tables of 5000 elements, ~1.9MB:

# gen.py
import sys
out = ["require import AllCore List.",
       "from Jasmin require import JModel_x86."]
for t in range(20):
    elts = "; ".join("(W8.of_int (-%d))" % (1 + (i % 120)) for i in range(5000))
    out.append("op [opaque smt_opaque] tbl%d : W8.t list = [%s]." % (t, elts))
sys.stdout.write("\n".join(out) + "\n")

python3 gen.py > tables.ec
echo 'require Tables.' > drv.ec
rm -f drv.eco && easycrypt compile drv.ec    # measure this

Going through a require matters: .eco records digests only, so a
required theory is re-parsed and re-elaborated in full on every run —
only its proofs are skipped. (Passing tables.ec to compile
directly would be skipped outright once its .eco is valid, and
measure nothing.)

CPU time, minimum of 16 runs split over the two orderings of the three
binaries, on a machine that was not quiet:

main	10.85s
+ [section]	9.09s	-16%
+ [unify]	8.74s	-19% cumulative

The section commit is ahead in 16 rounds out of 16, the unify commit
in 13 out of 16.

[section] skip the global dependency walk outside sections

check_op and check_tyd walk the whole body of every global
operator and type declaration, to check it only depends on things a
global item may depend on. Outside a section that walk can never
fail: local and declare items are rejected outside sections, so
everything bound in the environment is Global there.

check_ax, check_modtype and check_module already guard their
Global branch with scenv.sc_insec; this adds the same guard to the
two that were left out.

The walk is proportional to the size of the term, so it is cheap on
hand-written developments and expensive on generated ones. Requiring
the Array*/WArray*/BArray* theories a Jasmin extraction emits
gets about 20% faster on its own.

[unify] build the expected type once per overloading query

select_op_outcomes rebuilt tfun_expected inside the per-candidate
loop, so each candidate allocated its own throw-away unification
variable for the return type (plus the arrow type around it), even
though the expected type is the same for all of them. It is now built
once, in a scratch unienv that every candidate is forked from — the
candidates stay independent, since UniEnv.copy still gives each one
its own union-find. UniEnv.openty_r also short-circuits when there
is no type parameter to open and no explicit type argument; a
non-None tvi keeps the general path, which reports an arity
mismatch rather than silently ignoring it.

What makes this worth doing is that overloaded symbols are resolved
per occurrence. Counting the candidates select_op examines on the
file above:

TOTAL         calls=329678  cands=1161954
  [-]         calls=100213  cands=900584
  ::          calls=101005  cands=101005
  W8.of_int   calls=100015  cands=100015

Unary minus alone accounts for 78% of them: it has nine definitions in
scope once the word theories are imported, and eight are discarded at
every one of the 100k negative literals.

Testing

make unit 101/101, make stdlib 128/128.

Deliberately not included

• A more aggressive select_op pre-filter, rejecting a candidate
  whose rigid argument head already contradicts its domain before any
  of the unification machinery. Worth only about 2 further points, for
  ~30 lines and a soundness argument about type abbreviations.

• Generalising the section guard from sc_insec to "has this section
  introduced any local or declared item". That is the more accurate
  statement of the invariant and subsumes the guard above, but
  removing all section checks is worth only 2.5% on the most
  section-heavy stdlib theories (PROM, ROM, Hybrid,
  Strong_RP_RF, SplitRO, PRP, Birthday, LoopTransform,
  DLog, PKE, Indist, required as dependencies: 2.40s -> 2.34s),
  and stdlib sections open on their declares anyway, so the guard
  would almost never fire. It also has a trap worth recording: a flag
  stored in scenv is dropped by exit_theory, which returns
  oget scenv.sc_top, so

  section S.
    theory T. local op x : int = 0. end T.
    op y : int = T.x.
  end section S.
  

  would stop being rejected.

The structural cost is untouched and is larger than either of these:
.eco is a digest cache, not a compiled theory, so a required theory
is re-parsed and re-elaborated from source on every require, in
every session — for a file with no proof at all, the .eco saves
nothing.

🤖 Generated with Claude Code

https://claude.ai/code/session_016fkSDht523sZweUb7G7yR6