[metatheory] Proof of soundness of defunctionalization and FO-to-SMT semantic preservation

[AD1024]

Summary

This PR adds a mechanized soundness argument for the supported part of Crush's
lowering pipeline and connects that argument to the SMT commands retained by the
translator.

The formalized path is:

reified higher-order theory
  -> defunctionalized first-order theory
  -> typed FO-to-SMT encoding
  -> datatype declarations and guarded representations
  -> complete SMT command array retained by Crush

The central proof is by countermodel construction. Given a model of the
higher-order source theory, the development constructs:

1. a first-order model satisfying every translated formula and every equation
   introduced by defunctionalization;
2. a model of the encoded custom datatypes;
3. interpretations of generated datatype well-formedness predicates and
   guarded source-type representations; and
4. one SMT model satisfying the complete represented command array.

The final theorem, VCG.CommandEquiv.unsat_source_script, therefore establishes:

If the emitted SMT script belongs to the modeled fragment, matches the
proof-side encoding of the complete reified theory, and has no standard
model, then the reified higher-order source theory has no model satisfying
the supported custom-datatype assumptions.

Equivalently, the supported lowering path preserves satisfiability.

Main proof components

Intrinsically typed higher-order and first-order languages

The source language contains Booleans, opaque base types, nondependent function
types, lambda expressions, application, equality, Boolean connectives, and
quantifiers. Its terms are indexed by their context and result type.

The first-order target also uses intrinsically typed terms. Function-like
symbols carry a complete argument telescope and are always fully applied.
Ill-typed terms cannot be constructed in either language.

Custom datatypes appear as named base types at these two layers. Their
constructors, selectors, testers, and model laws are recorded separately.
Higher-order functions may consume or return datatype values. Datatype fields
in the supported declaration fragment contain first-order data; function-valued
fields such as Tree (α -> α) are outside that fragment.

Defunctionalization

The lowering from higher-order to first-order terms:

• collects the variables captured by each lambda;
• flattens complete applications into one fully applied first-order symbol;
• represents remaining function values with closures;
• emits equations describing closure application; and
• emits function-extensionality conditions for source function equality.

The principal results are:

• Flattened.translate_denote: a translated term has the same denotation as
  its higher-order source term in the constructed model;
• Flattened.generatedFormulas_valid: all generated closure and extensionality
  formulas hold in that model; and
• Flattened.model_extension_theory: one constructed first-order model
  satisfies the translation of the complete finite source theory.

The aggregate theorem uses one shared signature and one model for every source
fact, including all generated formulas.

Monomorphic custom datatypes

The datatype development covers finite groups of mutually recursive,
monomorphic datatype declarations. A block must be structurally well formed and
productive, so every datatype has a finite constructor value.

For admitted datatype declarations, the SMT semantics requires:

• total and well-typed constructors;
• injectivity of each constructor;
• disjointness of different constructors;
• exhaustiveness of constructors over the datatype carrier;
• matching tester behavior;
• selector equations on the matching constructor;
• unconstrained selector behavior on other constructors; and
• a rank that decreases along recursive datatype fields.

The development constructs a canonical datatype model and proves that it
satisfies these laws. This construction establishes that the datatype command
semantics is inhabited for every supported productive declaration block.

At the source boundary, Datatype.Env.IsFreeDatatypeModel states that custom
datatypes have their constructor-generated tree interpretation. This is the
source-model assumption used by the final theorem. Declaration well-formedness
checks syntax and productivity; the free-datatype property constrains a
particular source model.

SMT terms, commands, and interpreted theories

The SMT syntax used by the translator is untyped, so the metatheory gives it a
relational semantics and pairs it with a declaration-aware type checker.

The semantic fragment covers:

• Boolean literals, equality, not, implication, conjunction, and disjunction;
• let, universal quantification, and existential quantification;
• integer numerals and integer >=;
• declare-fun;
• define-fun;
• simultaneous define-funs-rec;
• monomorphic declare-datatypes;
• assertions; and
• sort declarations and administrative commands.

define-fun and define-funs-rec have explicit graph-equation semantics through
FunDef.Holds. A declared sort is interpreted by the model's nonempty carrier
for every SMT sort. Unsupported theory operators and higher-order SMT terms are
rejected by modeledScriptWellTyped.

Static and semantic conditions are kept separate:

• CommandsInFragment records semantic side conditions, including datatype
  productivity;
• CommandsWellTyped records successful declaration-aware checking; and
• Model.SatisfiesCommands states the mathematical obligations imposed by the
  commands.

This separation prevents malformed or unsupported syntax from establishing
unsatisfiability through an empty satisfaction clause.

The external semantic premise is CommandsUnsat. It quantifies over models
whose Boolean carrier has exactly two values, whose application graph is
functional, and whose integers have their standard interpretation whenever the
command array uses integer syntax. Boolean-only scripts therefore require no
unrelated integer carrier. standardModel_exists supplies a concrete global
standard model, ruling out an empty model class.

RawCommandsUnsat remains available for component theorems that quantify over
all relational models. The final translator theorem uses CommandsUnsat.

FO-to-SMT representation

SMT.Encoding assigns concrete SMT sorts and identifiers to typed first-order
sorts and symbols. It records injectivity and freshness of those assignments.
Built-in sorts such as Int are used directly and are never redeclared with
declare-sort.

SMT.TheoryRepr and SMT.GuardedTheoryRepr state that a concrete command array
contains exactly the commands generated from a typed first-order theory. The
semantic comparison ignores order and repeated occurrences because command
satisfaction is membership-based. The order-sensitive checker separately
enforces declaration-before-use and scope.

SMT.representation_sound constructs one raw SMT model satisfying ordinary
sort declarations, symbol declarations, datatype declarations, and assertions.
The model-extension infrastructure proves that fresh interpreted or generated
symbols preserve the denotation of previously encoded terms.

Guarded representations

A source type may be represented by an existing target type together with a
predicate selecting valid encodings. The code calls this a SubsetRepr.

The main example represents Nat by Int with the predicate 0 <= x.
Quantifiers are restricted to values satisfying the corresponding predicate.
For custom datatypes, generated recursive wf_T definitions combine:

• field predicates for values represented in an existing target type; and
• recursive wf_T calls for datatype-valued fields.

The development proves that these tester-and-selector formulas characterize
the intended source values and that the emitted recursive definitions have the
required graph semantics. SMT.guarded_lift then combines datatype commands,
guard definitions, ordinary declarations, and guarded assertions in one model.

GuardDefInterp supplies one uniform interpretation for every source model
satisfying the free-datatype condition. Keeping this interpretation outside the
quantified source-model predicate prevents the final theorem from discarding a
source model merely because target-model construction evidence was unavailable.

Connection to the commands emitted by Crush

When datatype certification is enabled, the translator retains:

• the reified datatype and ordinary signatures for each fact;
• typed descriptions of emitted datatype declarations;
• generated datatype guard definitions;
• their positions in the command array;
• allocated SMT names and the commands that use them; and
• every use of an unrestricted translation extension as an explicit trust
  reason.

FactTranslation is finalized after all facts have been processed, so its
locations refer to the complete emitted command array.

CommandEquiv.build? compares that array with the proof-side encoding of every
reified source fact under the same signature. It performs one semantic
normalization: removal of top-level :named assertion attributes. It then:

• checks the emitted command array;
• checks the normalized command array; and
• proves mutual command-set inclusion.

A successful comparison returns CommandEquivCert. The leading set-logic
command returned by buildScript is handled by a separate semantic equivalence
theorem, yielding CommandEquiv.unsat_source_script.

Review-driven fixes included in the current branch

The soundness and vacuity reviews led to the following changes:

• Added direct semantics for both nonrecursive and recursive SMT function
  definitions.
• Separated command membership in the modeled fragment from command
  satisfaction.
• Required both fragment membership and declaration-aware well-typedness in
  raw and standard unsatisfiability predicates.
• Restricted standard integer obligations to command arrays that actually use
  Int, numeric literals, or the modeled integer operator.
• Added a concrete standard-model witness.
• Made the checker kernel-reducible on scripts with declarations by using a
  list-based proof-facing environment and structural command traversal.
• Added kernel-checked well-typedness certificates without native_decide.
• Added a two-constant signature with genuine symbol inhabitants, injective
  encoding proofs, a quantified source theory, exact generated commands,
  successful CommandEquiv.build?, a satisfying standard target model, and an
  application of the final reflection theorem.
• Strengthened datatype admissibility with structural and productivity checks
  shared by the checker and semantic predicate.
• Constructed canonical datatype models to demonstrate non-vacuity of the
  datatype semantics.
• Ensured built-in SMT sorts are omitted from generated declare-sort
  commands.
• Replaced implementation-discussion labels with mathematical or
  PL-theoretical names and shortened common concepts under clear namespaces:
  Repr, ModelExt, DatatypeRepr, CommandEquiv, CommandEquivCert,
  FactTranslation, GuardDefEncoding, and GuardDefInterp.

Implementation-facing changes

• Added crush.datatype.certify, defaulting to false, for the path that
  retains proof-facing datatype and command information.
• Added typed command descriptions and allocation links so an emitted command
  cannot silently drift from the names used to construct it.
• Finalized fact translations against the full command array after all facts
  have been emitted.
• Added restricted extension points:
  • @[crush_certified_def] unfolds the annotated Lean definition;
  • @[crush_certified_lower] selects a fixed primitive mapping with a semantic
    certificate.
• Renamed targeted extension dispatch to describe its criterion:
  • @[crush_translate_head] dispatches on an application head;
  • @[crush_translate_family] dispatches on the result-type family.
• Retained general term and sort handlers as explicit trusted boundaries.

Scope and assumptions

• The final theorem starts from successfully reified higher-order terms. A
  semantic correctness theorem for conversion from arbitrary Lean.Expr values
  into the HO language remains a separate boundary.
• CommandsUnsat is a semantic no-model premise. Solver execution, proof
  replay, and UNSAT-core-guided reconstruction establish trust in a concrete
  solver result through separate mechanisms.
• The supported SMT theory operations are Boolean logic, equality, integer
  numerals, and integer >=. Arithmetic such as addition and multiplication,
  bit-vectors, strings, and arrays require corresponding semantic modules before
  entering this theorem.
• Supported datatype declarations are monomorphic, productive, and
  first-order. Dependent or indexed families, proof-valued fields,
  function-valued fields, unsafe cross-block recursion, quotient primitives,
  and unsupported recursors remain outside the reified datatype fragment.
• General translation callbacks can emit arbitrary SMT syntax. The theorem
  applies after the required representations, uniform guard interpretation,
  reified theory, and CommandEquivCert have been constructed.
• TranslateState.status reports whether a run used a marked trusted path. The
  final soundness theorem consumes the dependent proof objects listed above.
• The complete concrete SMT name encoding remains an explicit theorem premise.
  The translator retains collision-free allocation evidence used to construct
  and audit that encoding.

Reviewer guide

1. Start from the final theorem

Read:

• Crush/Metatheory/VCG/CommandEquiv.lean
• Crush/Metatheory/VCG/Datatype.lean

Focus on:

• CommandEquivCert;
• CommandEquiv.build?;
• CommandEquiv.unsat_source;
• CommandEquiv.unsat_source_script;
• FactTranslation.DatatypeRepr.sound; and
• FactTranslation.DatatypeRepr.theory_unsat.

Check that every bridge from a reified theory to the complete emitted command
array appears as an explicit premise or checked certificate.

2. Review defunctionalization

Suggested order:

1. Defunctionalization/Collect.lean
2. Defunctionalization/Flattened/Spine.lean
3. Defunctionalization/Flattened/Lambda.lean
4. Defunctionalization/Flattened/Translate.lean
5. Defunctionalization/Flattened/Denotation.lean
6. Defunctionalization/Flattened/Theory.lean

Check captured-variable order, complete application spines, closure equations,
function extensionality, and inclusion of every generated formula in the
aggregate target theory.

3. Review datatype semantics and non-vacuity

Suggested order:

1. Datatype/Core.lean
2. Datatype/Semantics.lean
3. Datatype/Model.lean
4. Datatype/Flattened.lean
5. SMT/Datatype.lean
6. SMT/DatatypeCanonical.lean
7. SMT/DatatypeTransport.lean
8. SMT/DatatypeRepr.lean

Check that the semantic datatype laws match SMT-LIB, that productivity is
required, and that the canonical construction supplies a model for every
admitted declaration block.

4. Review raw SMT semantics and checking

Read:

• Crush/SMT/Check.lean
• Crush/Metatheory/SMT/Semantics.lean
• Crush/Metatheory/SMT/Repr.lean
• Crush/Metatheory/SMT/Model.lean
• Crush/Metatheory/SMT/ModelExt.lean
• Crush/Metatheory/SMT/Soundness.lean
• Crush/Metatheory/SMT/Int.lean

Check:

• the modeled checker accepts exactly the semantic operator fragment;
• declarations, definitions, datatype commands, and assertions receive the
  stated semantics;
• CommandsInFragment and CommandsWellTyped prevent vacuous use of command
  satisfaction;
• StandardFor requests integer laws exactly when the commands use integers;
  and
• model extensions preserve previously established evaluations and command
  validity.

5. Review guarded representations

Read:

• FO/Guarded.lean
• Datatype/Guarded.lean
• Guarded/Encoding.lean
• SMT/Guarded.lean
• SMT/GuardedSoundness.lean
• SMT/DatatypeGuard.lean
• SMT/DatatypeGuarded.lean

Check universal and existential guard placement, recursive datatype guard
definitions, and the uniformity of GuardDefInterp over source models.

6. Review the implementation connection

Read:

• Reification/Witness.lean
• VCG/Generate.lean
• VCG/Datatype.lean
• VCG/CommandEquiv.lean
• Translation/Monad.lean
• Translation/Translate.lean
• Frontend/Tactic.lean

Check that command locations refer to the final array, allocated names remain
linked to their commands, assertion-name normalization is the only erased
syntax, and both the emitted and annotation-normalized arrays pass the modeled
checker.

7. Review executable regressions

Read:

• Test/Metatheory.lean
• Test/MetatheoryDatatype.lean
• Test/SMTCheck.lean
• Test/Smoke.lean

The two-constant regression near the end of Test/Metatheory.lean exercises
the complete command-equivalence and target-model construction path with real
ordinary symbols.

Validation

The following commands pass on the current branch:

lake build
lake build Test.Metatheory Test.MetatheoryDatatype Test.Smoke
lake build Test.SMTCheck

The metatheory and its regression tests contain no use of native_decide.