Conversation
Two refinements to the witness-selector resolver: 1. [select] in [select_op] catches [InvalidSelector] from [opentvi] and treats it as a candidate-rejection signal (raises [E.Failure]) rather than letting the anomaly bubble out. The error surfaces as a normal "no matching operator" if no candidate accepts the selector. 2. Concrete vs abstract dispatch: previously any [Tconstr p] with [tyd_type = `Abstract _] went to the abstract-search branch. But primitive types like [int] are declared abstract with an EMPTY bound list — they should be treated as concrete carriers. Fixed by requiring at least one bound to take the abstract path; empty-bound abstract types fall through to env-level instance lookup. Verified: selectors work on [int] (concrete), on [t <: comring] (declared-abstract with bounds), and (transitively) on type variables in op signatures.
Renames monoid's op to neutral [mop] and axioms to [mopA]/[mopC]/[mop0]. Section lemmas use [m] suffix ([mop0m], [mopCAm], etc.). [addmonoid] and [mulmonoid] rename ops via [(monoid with idm = zero, mop = (+))] and [(monoid with idm = oner, mop = ( * ))], with re-export section lemmas [addm*]/[mulm*] specialized to those subclasses. [comring] drops body axioms [mulrA]/[mulrC]/[mul1r]. They come for free through the [mulmonoid] chain; the comring section re-exports them under conventional names via [apply: mulm*]. Instance files (TcInt, TcReal, TcZModP, TcPoly) use labeled proof obligations: [proof mopA<:addmonoid> by ...] and [proof mopA<:mulmonoid> by ...]. Discharges both views distinctly. [src/ecScope.ml]: restore the per-entry obligation substitution fix (reverted in 03cb8f4). Now safe to land because the user can disambiguate via labels. [TcBigop]: parametric over [t <: monoid] using neutral [mop]. [local abbrev (+) = mop<:t>] (as a direct alias, NOT [fun x y => mop x y]) so partial applications [(+) x] keep their curried shape without introducing a [fun y => ...] lambda that would defeat rewrites. Status: 9/13 tcalgebra files pass. Four downstream (TcBigalg, TcBinomial, TcPoly, TcPolySmokeTest) fail with the same root cause: [zero<:t>] (the auto-promoted addmonoid op) and [idm<:t>] (monoid's op) have distinct global paths and the unifier doesn't see through [tc_reduce] when matching them. Manifests as [bigop_endo oppr0 opprD] failing because [oppr0]'s [-zero = zero] doesn't unify with [f idm = idm]. Tracked as follow-up; needs either unifier improvement or a redesign where renamed inherited ops are transparent aliases (like the original [abbrev zero] in TcMonoid) rather than fresh promoted ops. sandbox.ec is pre-existing failure unrelated to this migration.
When the rigid [Fop, Fop] match case encounters paths that differ but resolve to the same canonical TC origin (via [tc_ops_origin]), treat the ops as equivalent. The canonical origin is the path of the class where the op was originally introduced — followed through auto-import [tc_ops_origin] chains. Two ops match when: 1. They share an origin, AND 2. One's declared class is an ancestor (or descendant) of the other's — i.e., they sit on a single inheritance chain. The ancestor constraint distinguishes legitimate aliases ([monoid.idm] ↔ [addmonoid.zero], related by [addmonoid <: monoid] with the [idm = zero] rename) from sibling views that share an origin but are NOT equivalent ([addmonoid.(+)] vs [mulmonoid.( * )] — both auto-imported renamings of [monoid.mop], but [addmonoid] and [mulmonoid] are siblings, not ancestors). When paths differ but the ops are origin-equivalent, only the carrier types of the etyargs are unified (witness univars stay independent, since the tparam constraints differ — [<:monoid>] on one side, [<:addmonoid>] on the other; TC inference will resolve them through the appropriate chain view once carriers are pinned). New helpers in [EcEnv.Op]: - [tc_op_canonical_origin env p]: follows [tc_ops_origin]. - [tc_ops_same_origin env p1 p2]: origin + chain-relation check. Fixes TcBigalg.ec ([sumrN] via [big_endo oppr0 opprD] now works at section [t <: addgroup]: pattern [f idm = idm] matches subject [-zero = zero] because [monoid.idm] and [addmonoid.zero] are recognized as the same canonical op). 10/13 tcalgebra files now pass (was 9). TcPoly / TcBinomial / TcPolySmokeTest still fail on related but different bigop-at-poly issues.
Class declarations like [addmonoid <: (monoid with idm = zero, mop = (+))] no longer auto-import renamed inherited ops as new global OP_TCs. The rename clause is pure metadata; ergonomic local names ((+), zero, ( * ), oner) are wired up at the theory level via manual abbrev declarations that expand at typing time to the parent op (mop / idm). This makes class-decl renames symmetric with type-variable-constraint renames (which can never create ops) and eliminates the [Top.TcMonoid.+] vs [Top.TcMonoid.mop] duality that broke congr in TcBinomial and forced the same-origin scaffolding in the matcher. Resolver/SMT changes: - [match_tc_offsets] single-candidate guard ([ecUnify.ml]): with a single chain path, use it even when the rename clobbers the op name - the parent op is still accessible via that path. Without this [mop<:'a>] at ['a <: addmonoid] doesn't resolve. - [drop_tc_bounded_notation] removed from canonicalize: it preferred unbounded ops by name regardless of type, killing the new TC-bounded abbrevs. Real ambiguities (e.g. legacy Real.ec [(^)] vs TC [(^)]) are resolved at the user-code site (use [exp] in TcBinomial.binomial_r). - [tc_reduce_abstract_via_rename] removed entirely: it folded TC ops through rename edges to produce Fops at the renamed name. With renames now being abbreviations, the produced path resolves to an OB_nott that doesn't survive typing; the resulting Fop leaks an opaque why3 symbol into SMT tasks, breaking proofs like TcRing.expr_pred. - [head_op_after_tc_reduce] and the [tc_ops_same_origin] / [same_op] matcher clause removed (dead with the duality gone). Scope changes: - [inherited_tc_ops], [inherited_origins] always empty; body-local bindings for renamed inherited ops dropped (they'd leave dangling Flocals in axiom bodies otherwise). TcAlgebra changes: - TcMonoid.ec gains four abbrevs ((+) / zero / ( * ) / oner). - TcBinomial.binomial_r uses [exp] explicitly to pick the TC variant past the legacy Real.ec [(^) : real -> int -> real] abbrev. - TcPoly.ec instance proof tactic name updates. Batch: 11/11 examples/tcalgebra, 16/16 tests/tc.
Each TC class becomes a why3 record of its flattened ops (the dict).
Concrete instances and goal-context type carriers each get their own
dict const; Fop applications of TC class ops translate to record-field
projections on the appropriate dict. Different chain-leg views of the
same ancestor get distinct dicts, so the addmonoid leg and mulmonoid
leg of comring no longer collapse to the same why3 symbol.
Verified sound: `lemma false : false` at a `t::comring` carrier no
longer goes through smt() — previously the unsound encoding made it
derivable via `idm <> idm` collapsing to False.
Phases (see project memory `tc-smt-encoding-dict`):
A. per class, dict record type + uninterpreted axioms predicate.
B. per registered chain-instance, dict const + bridges to concrete
realisations + axioms-hold assertion.
C. per tparam / declared-abstract type bound, dict const + projected
ancestor axioms (substituted via the witness's chain lift).
D. trans_app intercepts class-op Fops, projecting through le_tdict
(tparam-bound) or te_idict (instance) dicts.
E. legacy `trans_tc_axioms`, `trans_reducible_instance_bridges`, and
`delta_tc` pre-reduce removed from the goal init path.
+ trans_axiom now dict-passes for polymorphic axioms — universal
over a fresh dict per TC bound, with `<class>_axioms` as premise
matching against each instance's axioms-hold.
Two follow-up fixes for the dict-passing encoding: 1. [te_absdict]: declared-abstract type carriers (section-introduced `declare type t <: comring`) now register their dicts at tenv level, not just in the goal's [lenv]. Lemma translations and operator-body translations build their own [lenv]s and need to see the same dict to project class ops through it — otherwise a lemma's body emits an opaque `Top_TcMonoid_mop` and the goal's body emits `fld_mop @ d_t_comring_0`, and SMT can't connect the two even though they denote the same value. 2. [<class>_axioms] axhold for tparam / declared-abstract dicts. Polymorphic lemmas now translate with [<class>_axioms 'a d] as premise — without this axhold, the SMT can't instantiate the universal lemma at the section's [t] / its dict because the premise has no witness in scope. Together these fix the TC SMT regression at [TcRing.ec:530] (which is the indicator goal `expr_pred (x : t) (i : int) : 0 < i => exp x i = x * exp x (i-1)` inside the comring section). Without the fix, the lemma `exprS` translated as a polymorphic axiom over an opaque `Top_TcMonoid_mop`, while the goal's `*` projected on [d_t_comring_0] — the symbols didn't match. tcalgebra status: 5 failures total on HEAD vs 7 at parent. Net +2 (TcRing:530 + TcNumber:1288 newly pass under the dict encoding); the five remaining failures are pre-existing and unrelated to this work.
Two interlocking changes to make the sound dict encoding work at concrete carriers without sacrificing tcalgebra obligation proofs: 1. **Instance-dict emission is lazy.** Triggered from [try_dict_proj] when an Fop with [TCIConcrete] witness is first encountered, via a forward-declared [emit_instance_dict_ref] so the mutual recursion stays well-typed. Eagerly emitting all reducible instances overwhelmed Alt-Ergo (5s timeout) — most goals don't need most instance dicts. Eager emission in [init] is kept for reducible instances so polymorphic lemma hints can still match against axhold facts. 2. **delta_tc reduction at two points.** In [init], the goal is pre-reduced so concrete-carrier class-op Fops resolve to their user-provided realisations (CoreInt.add etc.) instead of going through dict projection. In [emit_instance_dict], the substituted ancestor class axioms are similarly reduced — the bridges they'd otherwise reference now connect concrete-only facts, matching the goal's encoding. Other adjustments: - Phase D's projection uses HO form: [proj_ls : dict -> field_ty] (single dict arg, function-typed result), applied via [apply_highorder]. Avoids lambda eta-expansion (which Alt-Ergo handles poorly) and works uniformly for full/partial/over- application. - Per-class axioms-hold is asserted for both tparam dicts (Phase C) and instance dicts (Phase B) — polymorphic lemma premises match. - [ancestors_with_lifts] moved before [emit_instance_dict] (was defined later, broken forward reference). tcalgebra results (5/10 pass cleanly, 5 remaining failures all in proofs that previously relied on the encoding's unsoundness to discharge): TcMonoid TcRing TcInt[1] TcReal TcBigop pass TcBigalg[1] TcBinomial[1] TcNumber TcPoly[1] TcZModP[1] [1] one obligation each still relies on encoding-unsoundness in the parent state; sound discharge needs `inv 0 = 0`-style hints that aren't pulled by select_relevant. Documented as follow-up. Soundness sanity: `lemma false : false. by smt()` at `t::comring` no longer goes through (as before this commit).
Two changes to make polymorphic class-op uses fire reliably at concrete
carriers:
1. **First-order projections + lazy HO wrapper** (mirroring [trans_op]):
- [wcf_proj : dict -> arg_tys -> codom] (first-order, full
application path — what 99% of uses look like).
- [wcf_proj_ho]: lazily-emitted function-typed constant with a
[mk_highorder_func]-style spec axiom, only materialised when an
Fop is partially applied (e.g. [mop] passed to [associative]).
- Phase D's [try_dict_proj] picks: full app → first-order direct;
over-app → first-order then [apply_highorder]; partial → HO
wrapper applied via [@]. This keeps SMT bridges in first-order
form (which Alt-Ergo handles without HO machinery), matching
the existing [trans_op] / [w3op_ho_lsymbol] strategy.
2. **Specialised instances of polymorphic axioms** (extends [trans_axiom]):
For each lemma over a TC bound, in addition to the dict-passing
polymorphic version, ALSO emit a substituted-and-reduced version
at each registered reducible instance whose class matches. The
substituted form has the carrier and dict pinned to the instance;
[delta_tc] then resolves class-op Fops to the concrete realisations
(CoreInt.add etc.). SMT uses these concrete axioms directly without
having to instantiate the polymorphic version's universal dict.
Closes the [TcInt:60 / intmulz / smt(opprK mulrNz opprK)] gap — the
specialised [mulrNz_at_TcInt_addgroup] now reads
[forall x:int n:int. intmul x (-n) = -(intmul x n)] and Alt-Ergo
chains it with the [have h] hypothesis to handle the c<0 case.
tcalgebra: 6 of 10 pass clean (TcMonoid TcRing TcInt TcReal TcBigop
TcNumber); 4 remain (TcBigalg:198 TcBinomial:14 TcPoly:683 TcZModP:141).
Soundness sanity (false at t::comring) still holds.
[create_op] gated [OneShot.now register] inside [if not known then], so ops mapped to why3 builtins via [te_known_w3] (e.g. CoreInt.add, CoreInt.mul, CoreInt.opp) were NEVER cached in [te_op]. Each call to [trans_op] for such ops re-ran [create_op] from scratch, producing a fresh [w3op] with a fresh [HO_TODO] — and when [w3op_ho_lsymbol] fired in HO context (e.g. passing [( * )] to [Top_Logic_associative]), [mk_highorder_func] emitted yet another [(+)_hoN] / [( * )_hoN] copy + spec axiom. Visible as 10 copies of [(+)_ho], 10 of [( * )_ho], etc. in the 0014 task dump for TcInt.ec — bloating the task and probably slowing the SMT solver. Moving the [OneShot.now register] call out of the guard makes the cache fire uniformly, and the dump drops from 749 → 576 lines. tcalgebra status unchanged (6/10 pass clean); soundness sanity still holds.
[fld_invr1] / [fld__1] / [fld____1] / [fld__2] aren't useful for debugging — sub all the operator characters before why3's automatic disambiguation kicks in: + -> plus * -> times - -> minus [-] -> neg 0 -> zero 1 -> one < -> lt <= -> le > -> gt >= -> ge ( * ) -> times / -> div % -> mod Prefix with the class basename so different classes' fields don't collide either: comring_invr comring_unit comring_neg comring_plus comring_times comring_zero comring_oner monoid_mop monoid_idm addgroup_plus addgroup_neg addgroup_zero ... tcalgebra status unchanged.
[inst_Top_comring_107002 : Top_TcRing_comring int] → [inst_int_comring : Top_TcRing_comring int]. Build the instance name from the carrier head-type basename + the chain-label path (which the TC registration already records, and which ends in the class itself for chain ancestors — so we don't need to append the class separately). Bridges and tcinstax axioms reuse the same [inst_name] for consistency. For [int <: idomain] the chain now reads: inst_int_idomain (leaf) inst_int_comring inst_int_comring_addgroup inst_int_comring_mulmonoid inst_int_comring_addgroup_addmonoid inst_int_comring_mulmonoid_monoid (addmonoid+monoid leg) inst_int_comring_addgroup_addmonoid_monoid (mulmonoid+monoid leg) Each leg of the monoid diamond gets a distinct, leg-disambiguated dict — readable AND sound. tcalgebra status unchanged.
For each TC class C, for each parent edge i in C.tc_prts to parent class P with rename ren_i, emit a why3 function symbol C_to_P_<i> : C_dict 'a -> P_dict 'a plus one spec axiom per parent field f_P matching (by [wcf_origin] and [wcf_orig_name]) a child field f_C — asserting forall (d : C_dict 'a) (xs...), f_P (C_to_P_<i> d) xs... = f_C d xs... This is the dict-level analogue of [trans_class]'s flat-field projections, and bridges the polymorphic chain: a comring dict projects to its addgroup view, which projects to its addmonoid view, which projects to its monoid view (either leg). The projection lsymbols are cached per (class, edge index) in the new [wcd_chain_projs] field. Not yet consumed by [compute_op_dicts] / [try_dict_proj] — that's the next step, but the dict terms need to exist before call-site resolution can walk lifts via composition. tcalgebra: 6/10 still pass clean; soundness sanity still holds. The extra symbols and axioms are inert until call sites start projecting through them.
…ssing call sites) Two helpers that consume the chain-projection lsymbols emitted by [trans_class] (commit 628ed53): [walk_dict_lift]: given a starting (dict_term, w3_class_decl) and a [lift : int list], compose the per-edge [wcd_chain_projs] lsymbols to produce the (dict_term, w3_class_decl) at the target ancestor class. This is the dict-level analogue of [walk_lift] (which only walks the metadata, not term-level projections). [compute_op_dicts]: at a polymorphic op's call site, walk [op.op_tparams] paired with the Fop's etyargs witnesses; for each TC bound, resolve the witness to a (start dict, w3cd) — via [emit_instance_dict] for TCIConcrete, [le_tdict] for TCIAbstract `Var, [te_absdict] for TCIAbstract `Abs — and apply [walk_dict_lift] for the [lift]. Skips OP_TC class ops (handled by Phase D at call site directly). Falls back to typed-opaque [missing_dict] placeholder when resolution fails (polymorphic instances aren't yet handled). These helpers aren't wired into [create_op] / [trans_app] yet — that's the next step, but the underlying terms now exist for use. tcalgebra unchanged: 6/10 pass, soundness OK.
Polymorphic instances ([tci_params <> []]) now emit as why3 lsymbols [inst_X_Y : <inner dicts> -> <outer dict>], stored in [te_pidict]. A unified [resolve_witness] handles all four witness shapes (abstract `Var/`Abs, monomorphic instance, polymorphic instance) and is shared between [compute_op_dicts] (call-site dict-passing) and [try_dict_proj] (Phase D class-op projection). For [TCIConcrete] pointing at a polymorphic instance, [resolve_witness] recursively resolves each inner witness in [etyargs] (walking ITS lift via [walk_dict_lift] since the constructor's argument types are at the inner classes), then applies the constructor. No bridges or axioms-hold yet for polymorphic instances — the constructor is opaque, so [comring_<op> (inst_poly_X di) xs] is type-correct but unconstrained. This is the minimum needed to unblock [create_op] dict-passing of op bodies whose tparams bind a polymorphic carrier (the TcPoly:470 type-mismatch we hit earlier). tcalgebra: 6/10 unchanged (TcMonoid TcRing TcInt TcReal TcBigop TcNumber); 4 fail unchanged (TcBigalg:198 TcBinomial:14 TcPoly:683 TcZModP:141). No regressions.
create_op now prepends one dict-typed parameter per (tparam, tc) bound to the lsymbol's domain for non-class ops. Body translation uses an [le_tdict]-enriched lenv so class-op Fops in op bodies resolve via Phase D's dict-projection rather than emitting opaque [Top_<class>_<op>] symbols. apply_wop accepts ~dict_args; the Fop case in trans_app calls compute_op_dicts to compute them from the call-site etyargs. The lsymbol signature is [dict_doms @ textra @ wdom -> wcodom]; both new and old shapes co-exist (ops without TC bounds produce empty dict_doms and behave exactly as before). w3op_ta now returns [(dict_doms, textra, targs, tres)] at the instantiated types. All non-trivial w3op constructors updated. For ops where EC's elaboration omits class witnesses at the call site (subtype generators like to_poly / of_poly), compute_op_dicts emits typed placeholder dicts so the lsymbol's arity is matched; these placeholders are unconstrained but type-check. tcalgebra: 6/10 pass clean (TcMonoid TcRing TcInt TcReal TcBigop TcNumber); 4 fail at same lines as baseline (TcBigalg:198, TcBinomial:14, TcPoly:683, TcZModP:141). No regressions. Soundness check: [lemma false : false. by smt()] at [t::comring] correctly fails.
Two fixes that compose: 1. Chain-projection spec axioms now match parent/child fields by leaf-name (post-edge-rename) instead of (wcf_origin, wcf_orig_name). The origin-keyed lookup collides at diamond ancestors: at [comring], monoid's [idm] is reached via BOTH legs (renamed to [zero] / [oner]); last-write-wins picked the wrong one and emitted [mulmonoid_oner (comring_to_mulmonoid_1 d) = comring_zero d]. Now correctly emits [... = comring_oner d]. 2. [resolve_witness] for [TCIConcrete] walks [lift] through [tci_parents] first (analogous to [ecEnv.ml]'s [resolve_lifted]) so chain-walked witnesses resolve to the registered SYNTH chain instance's dict directly (e.g. [inst_int_comring_mulmonoid_monoid]) rather than building [mulmonoid_to_monoid_0 inst_int_comring_mulmonoid] via chain projections. The two are semantically equal but only the direct-instance form matches the [bridge_inst_X_<op>] axioms that relate dict projections to concrete realisations. Falls back to chain projections for parents missing from [tci_parents]. tcalgebra: 6/10 pass + TcBinomial advanced from fail-at-line-14 to fail-at-line-35 (now passes fact0 and many subsequent lemmas before hitting size_bin1's [/#]). TcBigalg, TcPoly, TcZModP failing at same lines as baseline. No regressions.
in-progress chain is NOT yet registered
Bug: [add_generic_instance] used to register every chain entry as a
[Th_instance] BEFORE [check_tci_axioms]. The env at obligation-
discharge time therefore exposed the in-progress instance (and every
synthesised chain ancestor) to the resolver, matcher, conversion /
[tc_reduce], and SMT translation. An obligation like
instance idomain with real ... proof unitout by smt().
would close via [instax_inst_real_idomain_unitout : forall x:real,
!real_unit x -> inv x = x] (emitted by the SMT translator for the
not-yet-discharged instance) matching the goal verbatim — circular.
The same hole let user tactics close an obligation by appealing to a
polymorphic lemma over the in-progress class.
Fix: process the chain entries in topological order over
[tci_parents] for the PURPOSE of pre-reducing each obligation form.
When pre-reducing entry X's obligations, X and all chain entries
already processed (ie all of X's strict ancestors in the chain) are
registered in a TEMPORARY scope. [delta_tc] simplification then
rewrites every class-op [Fop] reference whose witness points at a
chain path to the user-provided concrete realisation from the
instance's symbol map. After pre-reduction, X's obligation forms
mention only concrete ops — no class-op [Fop], no chain-path
witness.
[check_tci_axioms] runs against the ORIGINAL scope (no chain entry
registered). The user's proof tactic gets a fully-concrete goal and
has no way to invoke the in-progress instance. After every obligation
discharges, the chain entries are registered permanently — exactly
the post-condition we promise downstream.
The semantics now match what would happen if the user wrote each
chain ancestor as a separate [instance …] declaration in dependency
order: every instance's obligations get discharged against an env
that has all its ancestors registered but not itself or its
descendants. The chain mechanism keeps the one-block syntactic
convenience without the loss of soundness that came from registering
everything up front.
Verified: [lemma false : false by smt()] inside an instance proof at
[t::comring] correctly fails. Soundness probes that previously
derived [1 = 0] inside an in-progress idomain instance no longer
close.
tcalgebra: TcMonoid TcRing TcInt TcBigop pass clean. TcReal,
TcNumber, TcBigalg, TcBinomial, TcPoly, TcZModP now fail at the
obligations / SMT calls that previously closed via circular self-
reference; each is now an honest proof debt — the encoding no
longer fakes it.
Two orthogonal changes:
1. **smt(L<:T1, T2>) syntax**. [pdbmap1] gains [pht_tvi : ptyannot option],
propagated through [ecScope.Prover.process_dbhint] (now returns both
the path-set hints and a [path → ty list Mp.t] map of type
instantiations) into [EcProvers.prover_infos.pr_tvi]. [EcSmt] reads
[tenv.te_tvi], populated from [pi.pr_tvi] in [check]: when a lemma
path has type instantiations, [trans_axiom] substitutes the tparams
to those types, [delta_tc]-reduces the result, and emits a single
concrete-op axiom — bypassing the polymorphic dict-passing emission.
2. **EC_TC_MINIMAL=1 env var**. When set:
- Phase B is disabled (no per-instance dicts/bridges/axhold for
reducible instances).
- [lenv_of_hyps] skips [emit_tparam_dicts] / [emit_abstract_type_dicts]
(no per-tparam dicts or projected ancestor axioms).
- [trans_axiom] for lemmas with TC tparams and no [pr_tvi] entry
emits nothing (a warning instead). The user must explicitly write
[smt(L<:T>)] to bring such a lemma in.
The intent: send NO abstract TC machinery to the SMT prover; let the
user pre-instantiate the lemmas they need with [<:T>] so each enters
the task as a concrete-op axiom. Goal: avoid the task-pollution that
buries fast obligations in unrelated axioms (the Phase-B noise that
Z3 / CVC5 can't filter), and force explicit instantiation discipline
in proofs.
Verified on TcInt: with line 60's [smt(opprK mulrNz opprK)] rewritten
to [smt(opprK<:int> mulrNz<:int>)], the whole file passes under
[EC_TC_MINIMAL=1].
Default behavior unchanged (flag off).
Drop the [real_unit] op wrapper — the instance form accepts an inline lambda for [op unit]. unitout now uses [smt(invr0)] (the [inv 0%r = 0%r] rule), removing the previous reliance on the circular [instax_inst_real_idomain_unitout] axiom.
[opprK] and [mulrNz] are TC-polymorphic; in minimal-mode SMT we have to point them at [int] explicitly. Also drops the duplicate [opprK].
In TC-minimal mode, two issues blocked section-abstract lemmas from
applying to goals at the same abstract carrier:
- [placeholder_dict] emitted a fresh [missing_dict<N>] for every
TC-op call site, so the goal and the user-hinted lemma used
distinct dicts for the same [(*)]. Cached on
(carrier_w3_ty, tc_name) so calls at the same abstract carrier +
class share one constant.
- [trans_class] emitted chain-projection spec axioms describing
[parent_field(proj d) = child_field(d)]. Skipped in minimal mode:
we send class operators but not TC axioms.
Also:
- Track [pi.pr_wanted] in [tenv.te_wanted]. A TC-polymorphic lemma
explicitly requested via [smt(L)] without a [<:T>] instantiation
is now a hard error (not a silent skip).
- Arity-check [<:T1, …>] against the lemma's [ax_tparams] in
[process_dbhint]; mismatched counts raise [hierror] at scope
time instead of being dropped silently in [trans_axiom].
- TcNumber line 747: instantiate [mul0r<:t>] (the only TC-poly
lemma in that hint set; the rest are section-local).
In TC-minimal mode the dict-projection encoding was emitting one-step
projections at the witness's class (e.g. [tcrealdomain_times d]) while
operator bodies that internally project via chain projections produced
multi-hop forms (e.g. [monoid_mop (mulmonoid_to_monoid_0 (...)) x y]).
The two never matched without chain-projection spec axioms — and even
with them, the noise drowned Z3/CVC5.
This commit:
- [try_dict_proj] now canonicalizes class-op Fops in minimal mode:
walk the dict all the way to the OP's class via [lift] and project
using the op's local name there. Both lemma and operator-body refs
converge at the SAME (carrier, op_class, lift) key.
- Pre-emit one flat-constant logic-definition per
(carrier, reachable-ancestor-class, lift-of-edges) at init time.
The body is the explicit chain composition; references to the
constant unfold to the same chain expression when needed. Both
[try_dict_proj] and [compute_op_dicts] route through this cache —
every body term becomes a flat [<class>_<op> d_t_<class>_<lift> …]
rather than a 4-deep nested [proj1 (proj2 (...))] expression.
- [trans_class] in minimal mode skips emitting chain-proj spec axioms
(canonicalization makes them redundant) AND emits projection
lsymbols only for the natively-declared ops of each class
(inherited ops are reached via origin canonicalization, not via
leaf-class field clones).
- [lenv_of_tparams_for_hyp] strips the leading tick from EC tparam
tysymbol names ([ec_tv_a] instead of ['a]) and [trans_hyp] uses
[preid_lid] for lsymbol names so the dump's [.why] companion is
valid Why3 source. [str_p_raw] sanitises operator/punctuation
chars in path-derived names.
- [emit_one_dict] gains [?emit_axioms:bool]; minimal-mode dict
emission passes [~emit_axioms:false] (no [axhold] / no
[tcaxiom_] decls).
- Lemma instantiation in [trans_axiom] uses
[EcUnify.UniEnv.opentvi] to resolve witnesses for [smt(L<:T>)]
hints — the same path as proof-term elaboration. Handles
section-abstract carriers correctly, replacing the hand-rolled
[List.find_opt] lookup.
- [process_dbhint] now arity-checks [<:T1,…>] against
[ax_tparams] at scope time (mismatched count is a hard
[hierror], not a silent skip in [trans_axiom]).
Status: Alt-Ergo proves the TcBigalg:291 task in 0.02s. Z3 and CVC5
still struggle (Unknown / Timeout) despite identical SMT-symbol
matching across lemma / hypotheses / goal — investigation continues
(possibly per-call-site specialisation à la option C).
…e 1)
In TC-minimal mode, [try_dict_proj] now emits a CONCRETE-TYPED lsymbol
per (carrier, op_class, lift) instead of a dict-passing projection.
This mimics what clone-based theories produce: one fresh first-order
function symbol per (concrete instantiation, leg), with no polymorphism
or dict argument visible to the SMT prover.
- Cache keyed by (carrier_w3_ty, op_class_path, local_name) in
[te_carrier_ops]. Each entry is a fresh lsymbol whose
[ls_args]/[ls_value] come from substituting the op's self-tparam
with the carrier in the EC signature.
- Lemma side (after [opentvi]) and operator-body side at the same
(carrier, leg) hit the same cache entry — bytewise-identical SMT
terms across the task. Z3 and CVC5 pattern-match without needing
to instantiate polymorphic types or unfold dict projections.
- Partial / over-application paths now branch on whether we
resolved to [`Concrete ls] (minimal mode) or [`Field (d, w3cd, f)]
(dict-passing mode); HO wrappers for the concrete form reuse
[mk_highorder_func] from regular-op translation.
Sweep at this point (regular ops with TC tparams still polymorphic,
i.e. [bigM] keeps a dict argument — Phase 2 will specialize those
per call site too):
PASS: TcMonoid, TcRing, TcInt, TcReal, TcNumber, TcBigop, TcBigalg,
TcPolySmokeTest, TcZModPSmokeTest
FAIL: TcBinomial:14, TcPoly, TcZModP:294
…nches
- Remove the [tc_minimal_mode] env-var flag and all
[if (not) (tc_minimal_mode ()) then …] conditionals — keep the
minimal-mode body, drop the polymorphic-dict-passing branches.
- Drop chain-projection spec axiom emission from [trans_class]
(replaced by origin canonicalization in [try_dict_proj]).
- Drop the polymorphic-dict-passing axiom encoding in [trans_axiom]
plus its [_at_<carrier>_<class>] instance specialization
(replaced by [do_instantiated] via [smt(L<:T>)] hints).
- Drop the ancestor-class flattening in [trans_class] (only emit
fields for natively-declared ops of the current class).
- Drop the [Field] case of [try_dict_proj]'s [resolved] disjunction
— class-op references always resolve to the concrete-typed
[`Concrete] lsymbol now.
- [emit_one_dict] no longer takes an [?emit_axioms] parameter; the
axhold / tcaxiom emission paths are gone. It always emits
dict-const + flat-constant logic-defs for ancestors.
- [init] simplifies — no Phase B branch, just direct emission of
tparam + abstract-type dicts.
Sweep unchanged from previous commit: 9 PASS, 3 FAIL (TcBinomial:14,
TcPoly, TcZModP:294).
…rrier Three call sites of [smt(ge0_deg)] and two of [smt(oner_neq0)] in sections declaring [c :: comring] / [c :: idomain]. Both lemmas are TC-polymorphic; the minimal-mode encoding requires explicit [<:c>] instantiation.
- TcZModP:unitE — replace [smt(zmod_mulrC zmod_mul1r choicebP)]
with [apply: (unitr0<:zmod>)] (analogue of main's
[apply: ZModpRing.unitr0]).
- TcZModP:zmod_mulf_eq0 — port main's case-analysis proof
using [mul0r] / [mulr0] / [mulrI] / [unitE].
- TcBinomial:fact0 — replace [rewrite /fact /bigiM /bigM
range_geq /#] with [rewrite /fact big_geq // ler_naddl]
(main's proof).
- TcBinomial:size_bin1 — replace the [/#] tail with main's
[subz0 ler_maxr ?size_ge0] rewrite chain.
All four had been rewritten with [smt(...)] / [/#] tails that
relied on auto-relevance to pull in lemmas the minimal-mode
encoding doesn't surface. Backporting main's proofs verbatim
closes them.
…rier [pmulr_gt0] is TC-polymorphic; the minimal-mode SMT encoding requires explicit [<:t>] instantiation (section's [t :: tcrealdomain]). [prodr_ge0_seq] is section-local with 0 tparams — left bare.
Conflicts resolved in 6 files, all from origin/main's [ac42e2a subtype: generalize over section-declared free types at section close]. That commit's subtype-tracking change had already been applied to HEAD's [module Ty.add_subtype]/[Ty.add] independently (tyd_subtype field threaded through, carrier+pred stored on the tydecl), so the conflict resolutions all KEEP HEAD's structure: - [tydecl] keeps HEAD's [tyd_resolve] field on top of the [tyd_subtype] field both branches added. - Type-body constructors stay as polymorphic variants ([`Abstract], [`Concrete]) — TC needs the typeclass-list payload on [`Abstract tc] that main's plain constructor form doesn't carry. - Subtype-related tydecl construction sites all carry the [tyd_resolve = …] field. - [generalize_tydecl] in [ecSection] keeps the destructuring [fun (id, _) -> …] for HEAD's tparam-with-tcs tuple shape. - [ecScope.ml]'s conflict was a structural duplicate (origin/main's [module Ty] block was being pasted before HEAD's [module Search]; both branches already have [module Ty] independently) — dropped the duplicated insertion. Verified: [dune build] clean, tcalgebra sweep 12/12 PASS after merge.
Commit [0b2f706 TC: matcher recognizes ops with same canonical origin] left this line as a broken split [rewrite ... addrAC. rewrite !addzA. ler_subr_addl (...).] — apparent WIP that didn't get re-joined. Restoring main's single-line form [rewrite ... addrAC !addrA ler_subr_addl (IntID.addrC 1).].
Commit [5e04bf6 TC: drain pending TC-constraints before [try_delta]'s tc_reduce check] added [flush_tc_problems] + [norm f1] / [norm f2] at the entrance of [try_delta]. The flush is needed; the [norm] calls are not — they re-substitute ev/tu bindings that may have been pinned during earlier sibling-argument matches, which can change which heads appear after [destr_app] and silently steer the case dispatch away from the [Op.reducible] branch that would otherwise apply. Concrete regression: [theories/algebra/IntDiv.ec:1234]'s [rewrite -(big_mapT _ idfun)] failed with [nothing to rewrite] because the pattern's [idfun \o ?h] couldn't unfold past the norm- substituted form. Dropping the [norm] calls restores the match (IntDiv.ec passes again; tcalgebra 12/12 still PASS). [flush_tc_problems] alone is enough to make the queued [TcCtt] problems get resolved so [tc_reducible] can fire on the now-pinned witnesses.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.