Keep record-flattening refactorings tractable in TLAPS

[lemmy]

Two independent changes for behaviour-preservation proofs over a flattened state record:

1. Expr.Elab: fold record-literal EXCEPT during normalization (prevents front-end term explosion).
2. SMT encoding: Encode.Rewrite.simpl_receq decomposes an equality of two record constructors into its field equalities (avoids record/function extensionality on the back end).

Both fire only on explicit record constructors and never push a selection/update/equality through IF (unsound unless the guard is Boolean), so neither assumes a type for any subterm.

Motivation

Larger, mechanical refactorings of existing specs are likely to become more common as specs are increasingly synthesized and rewritten by AI tooling. Proving one behaviour-preserving -- Next <=> R_Next, per action, under a refinement mapping relating the two variable sets -- is thus a shape TLAPS should discharge cheaply. The FlashProtocol flattening in tlaplus/Examples#216 (FlashWithMutexEquiv, a >20-field state record) is the working example.

Flattening a record-valued state variable into separate variables (replace Sta by dir, p, ...) is one such refactoring: the refinement mapping glues them back, StaBar == [dir |-> dir, p |-> p, ...], so per action the equivalence reduces to comparing the two next-state records. The obligations are therefore dominated by EXCEPT-updates of, and equalities between, wide record CONSTRUCTORS.

Discharging them is not a formality: in the Flash flattening the per-action proof refuted the refactoring and pinpointed a real divergence that model checking had missed -- in NI_Local_GetX_PutX under ~Dir.Dirty /\ elsifCond /\ ~Dir.Local the flat spec left Proc unchanged where the record spec invalidates the home cache line -- fixed in tlaplus/Examples#216 ("Fix NI_Local_GetX_PutX to invalidate Proc[Home] when not Dir.Local"). No reachable state and none of the invariants distinguished the two encodings.

1. Front-end blow-up: fold record-literal EXCEPT

The refinement mapping expands the update to [ recLit EXCEPT !.h ... = v ] over a wide constructor. The naive EXCEPT desugaring re-embeds the base once per path component and per exspec -- multiplicative: one Flash per-action obligation expanded to millions of terms in Expr.Elab.normalize, exhausting memory before any backend ran.

Fix: fold each update into the constructor in place (materialising a shared prefix once), and run let_normalize before except_normalize so LET-bound constructors are exposed, not re-embedded. Result is linear in the record width. A size regression guards it (test/regression_tests/record_except_explosion_test.tla): at 4 layers the normalized obligation is ~5000 printed lines with the fold, >=39000 without (>=9M at 6 layers).

2. Back-end cost: decompose record-constructor equalities

A record is a function whose domain is its field names, so rec1 = rec2 is discharged via FunExt plus RecIsafcn/RecDomDef/RecAppDef; instantiating the nested \A x \in DOMAIN dominates for wide records and for obligations with many such equalities. simpl_receq reduces this syntactically on constructors (domain and field values statically known):

[h1 |-> a1, ..., hn |-> an] = [h1 |-> b1, ..., hn |-> bn]
  -->  a1 = b1 /\ ... /\ an = bn      (fields paired by name)

The result is ground, quantifier-free, and emits no extensionality axiom. It runs in the SMT-LIB pipeline before type synthesis, recurses into nested constructors, decomposes only equal field sets (unequal domains left to the solver), and rewrites equalities in every position; Zenon/Isabelle are unaffected.

Performance (FlashWithMutexEquiv, 266 obligations, from scratch, --threads 8 --stretch 30): with simpl_receq 1046 s, all on Z3; without ~1490 s, the widest equality (ABS_NI_Local_GetX_PutX) times out on Z3 and falls back to zenon. ~30% wall-clock and no fallback.

Prior art

The old SMT backend already specialized record equality (finite extensionality instances); the new minimal-axiom encoding ("a record is a function") dropped it. simpl_receq reinstates it as a pre-encoding REWRITE, not an axiom: it removes the equality (and the outer \A f, g) entirely, so it costs the solver nothing and cannot misfire.

Deferred: tuple constructors

The same decomposition applies to tuple literals (arity fixed by syntax, position as field name; drops the Tup* axioms), but is deferred: flattening produces records, not tuples, so its payoff here is less clear. Sequences and arbitrary function constructors stay on FunExt (domain not a statically known finite enumeration).

[muenchnerkindl]

Thank you for this contribution! The code looks good to me (but I cannot claim to have understood every detail) and the tests are convincing.
@damiendoligez Can you also have a look?

[lemmy]

@glondu If time permits, could you please review the Ocaml code in this PR?

[glondu]

@glondu If time permits, could you please review the Ocaml code in this PR?

Yes, sure.

I had a look at 134f78b. same_fieldset is correct only if each field label appears once (is it the case in this context?). Moreover, the combination of List.length, List.for_all and List.mem_assoc (plus List.assoc in decompose_receq), each linear in the list size, looks very inefficient, especially if the record is big (what is the typical/worst size?). I would have used a string map.

I will have a look at the other commit later.

[lemmy]

The TLAPM parser accepts duplicate record fields, and the encoding is then inconsistent, so FALSE is provable:

---- MODULE Foo -----
THEOREM Eq    == [a |-> 1, a |-> 2] = [a |-> 1, a |-> 3] OBVIOUS
THEOREM False == ASSUME NEW r, r = [a |-> 1, a |-> 2] PROVE FALSE OBVIOUS
=====

-> % opam exec -- tlapm Foo.tla
File "./Foo.tla", line 1, character 1 to line 4, character 5:
[INFO]: All 2 obligations proved.

False has no constructor-to-constructor equality, so simpl_receq never fires: this is pre-existing and orthogonal to this PR. The cause shows in [a |-> 1, a |-> 2].a = 1 /\ [a |-> 1, a |-> 2].a = 2, also proved — the record axioms are instantiated per field entry, giving the duplicated name two values. Only Zenon objects (duplicate record field "a").

Silver lining: SANY rejects the constructor ("Non-unique fields in constructor"), so #213 would keep this input away from the backends.

[lemmy]

@glondu Record widths in practice are small, so this was never a bottleneck, but it's changed anyway: same_fieldset and the List.assoc pairing are gone, replaced by Util.Coll.Sm. Both field lists are indexed by name, Sm.equal (fun _ _ -> true) compares the domains and Sm.find does the pairing, so it's no longer quadratic.