Integer-indexed types - #1065
Draft
strub wants to merge 73 commits into
Draft
Conversation
Mechanical migration of every call site to the new
ty_params = {idxvars; tyvars} record and targs = {indices; types}
record introduced in b15e335. Repairs the broken gen_op/mk_op
bodies in ecDecl and the syntax error in ecInductive (c413f37 WIP).
No semantic change: indices are uniformly empty, tyvars carry the
existing behaviour. Phase-0 design choices and the rest of the
roadmap are documented in memory.md.
tindex equality and hashing now go through a canonical sum-of-monomials normalisation, so n+1 and 1+n (and (n+m)^2 and n^2+2nm+m^2) are recognised as equal. Coefficients are EcBigInt with the natural-number invariant; canonical_const refuses negative TIConst. ecUnify now compares indices (with the previous polarity bug fixed) and ecReduction.for_targs no longer skips them. Memory.md updated with the Phase-1 deliverables and what was deferred (no TIUnivar / UF participation yet — gated on Phase 3 needs).
tindex_subst is no longer a no-op. It consults fs_loc / sb_flocal (indices share the formula-locals namespace), reinterprets the bound formula as a polynomial via the new tindex_of_form recogniser, and panics if the binding is non-polynomial. targs_fv (and so ty_fv on Tconstr) now folds over indices, so the per-formula short-circuits in Fsubst correctly fire for types with TIVar occurrences. is_ty_subst_id now also checks fs_loc emptiness — a formula substitution that touches an int-typed local can affect any type whose Tconstr carries a TIVar of that local. Cost is a wider substitution walk; correctness comes first here. memory.md updated with deliverables, design choices (no eager re-canonicalisation, fs_eloc not consulted), and the remaining risk (audit f_bind_local callers for the polynomial invariant).
Tydecls, operators, predicates and axioms can now declare integer
index parameters; type-constructor applications can supply index
arguments.
type [n m] ('a, 'b) vec.
op f [n 'a] (xs : 'a vec<:n>) : 'a vec<:n+1>.
pred p [n 'a] : 'a vec<:n>.
axiom A [n 'a] : true.
Index binders use plain (no apostrophe) identifiers in `[...]`. Index
applications are framed by `<:...>` rather than `[...]` to avoid a
shift/reduce conflict with codepos brackets in module-update
syntax. Index expressions inside the framing are restricted to the
polynomial fragment (`+`, `*`, non-negative literals, identifiers).
Datatype/record indexed types and cloning of indexed declarations
are refused with clean errors — useful index-instantiation at op
call sites still requires the deferred TIUnivar / polynomial-with-
univars unification work, also flagged in memory.md.
A regression test lives at tests/indexed-types.ec.
Adds the TIUnivar machinery Phase 3 deferred. Indexed ops can now be
called: each idxvar of the op being applied is freshened to a TIUnivar
and unified against the call site via polynomial-normal-form equality.
op concat [n m 'a] (xs : 'a vec<:n>) (ys : 'a vec<:m>) : 'a vec<:n+m>.
op cons [n 'a] (x : 'a) (xs : 'a vec<:n>) : 'a vec<:n+1>.
op test [n m 'a] (x : 'a) (ys : 'a vec<:n>) (zs : 'a vec<:m>)
: 'a vec<:n+(1+m)> (* canonically equal to (n+1)+m *)
= concat (cons x ys) zs.
The typecheck of `test` works because `cons`'s `?u` unifies with `n`,
`concat`'s `?u_n` unifies with `(n+1)`, `?u_m` with `m`, and the
inferred return type `(n+1)+m` is canonically equal to the annotated
`n+(1+m)`.
MVP scope: handles "naked TIUnivar = arbitrary polynomial" (with
occurs check) and canonical equality after resolution. Refuses
genuine polynomial unification (e.g. `?u + 1 = n` would need
subtraction-inversion) with a clean IndexMismatch error.
Also fixes a lurking bug in `ty_subst` where the `Tconstr` case fell
through to `ty_map`, which preserves indices verbatim — silently
dropping op-application index substitution.
clone T as T2 with type [k] 'a vec = body The optional [k] mirrors the tydecl binder syntax. body may reference both k and the type binders; when vec<:e> appears in T, the substitution binds k to e in body. ty_override_def is widened to (idxvars, tyvars, body); subst gains sb_idxvar; subst_ty's Tconstr-with-tydef branch binds both source binder lists to the call-site indices/types before substituting through body. The previous CE_IndexedNotYetSupported is replaced with CE_IdxArgMism so the user gets a precise arity message. Three clone cases land in the regression: drop the index (= int), propagate (= 'a coll<:k>), and a polynomial of the binder (= 'a coll<:k+1>). 77 declarations now compile. Two gaps are flagged in memory.md but kept out of scope: reaching into a cloned theory's ops whose signature got touched (looks orthogonal to indexed types), and explicit index-instantiation syntax at op call sites.
The two assert (List.is_empty *.indices) panics in ecSmt.ml become
raise CanNotTranslate, and check / execute_task catch the exception
to skip the goal cleanly. The user now sees a warning
("SMT: skipped goal containing constructs not yet exported to Why3
(e.g. indexed types)") followed by "cannot prove goal", instead of
an anomaly crash.
Translating indexed types to Why3 stays out of scope per the
original Phase-0 punt.
Errors and transcripts now print 'a vec<:n> instead of 'a vec; pp_tindex handles variables, univars (?#N), constants, and the polynomial *- and +-forms with standard precedence. Two vestigial Phase-0 asserts become clean failures: - ecReduction: indexed-op heads in a user rewrite rule raise NotReducible instead of crashing (they just don't match). - ecMatching: Fop vs Fop in pattern matching uses tindex_equal plus a length check, failing cleanly rather than asserting. The two asserts in ecInductive's positivity check are intentional "should never happen" guards — Phase-3 Slice-A already refuses indexed binders on datatype/record, so they aren't reachable. Closes the roadmap in memory.md. Remaining gaps are documented (op call-site index instantiation syntax, SMT translation of indexed types, indexed datatypes) but out of scope.
E — extend index-binder support to abbreviations and notations. Both rules now accept mixed_tyvars_decl (the bracket binder list that splits into idxvars and tyvars). pabbrev / pnotation gain *_idx fields; ecHiNotations threads them via the new ~idxparams parameter on transtyvars. abbrev my_alias [n 'a] : 'a vec<:n+1> = ... . notation %"..."% [n 'a] (...) = ... . D — investigation of the Phase-4 "T2.make_vec unknown" report showed it was a misuse of the alias `=` operator instead of the inline `<-` operator (alias creates a new name; inline propagates the body). Both modes work correctly. While tracing, fresh_tparams was discovered to freshen tyvars but not idxvars — fix this so op_tparams alpha-renaming includes both.
op count [n 'a] : int. op test : int = count[:5]<:int>. New lexer token LBRACKETCOLON (matches `[:` glued). Grammar adds `f[:idx]`, `f[:idx]<:ty>`, alongside existing `f<:ty>`. Parsetree TVIunamed and ecUnify tvar_inst.TVIunamed are widened to (indices, types). Producers updated mechanically (PFrecord, PTHO_*, inductive constructors, scope's tycinstance loop, printer's op_symb resolution, transtvi). EcUnify.openidx now consumes user- supplied indices when given, falling back to fresh TIUnivars otherwise. select_op's filter validates either side independently when non-empty. Useful when an op's idxvar is unreachable by argument-type inference. Phase-3.5 inference still handles the common case where the index can be derived from an argument's type. The test file gets three new cases (size[:5] xs, count[:5]<:int>, inferred-only baseline). 91 declarations now compile.
Document the plan and effort estimates for the three documented-but- unscheduled gaps from the original A-F plan. Order: B (polynomial unification beyond naked TIUnivar) -> C (non-refining indexed datatypes/records) -> F (SMT translation via per-index monomorphize).
Generalise the index unifier so [?u + k = poly] is solved when ?u
appears with net coefficient ±1 and the residual stays non-negative.
Previously only the naked-univar special case [?u = poly] worked, so
e.g. [tail xs : 'a vec<:n>] (where tail expects [vec<:n+1>]) failed
to unify against a caller-supplied [vec<:5>].
The new tindex_solve_for_univar walks the signed difference of the
two canonical polynomials, accepting only equations where:
- exactly one TIUnivar has non-zero net coefficient,
- that coefficient is ±1,
- every monomial mixing univars with other variables (or with a
univar at degree > 1) cancels to zero on net,
- the resulting value of ?u has non-negative coefficient on every
remaining monomial and constant.
The MVP scope deliberately excludes multi-univar Diophantine and
cases like [?u + 1 = n] for free n (no symbolic guarantee n >= 1).
Lift the Phase-3 Slice-A refusal that blocked index binders on datatype/record declarations. trans_datatype and trans_record now take an optional ~idxparams; ecScope's tydecl path threads it through the existing ~idxparams plumbing of transtyvars. Constructor and projector signature construction in ecEnv builds the result type via tconstr ~indices ~tyargs so e.g. INil is registered as 'a vec<:n>, not 'a vec. The positivity checker drops its assert (List.is_empty args.indices); indices play no role in positivity since the recursion is on the type and indices carry no embedded type information. Match elaboration in trans_branch (ecTyping) and the matchfix twin in ecHiInductive previously broke for 0-field constructors of indexed datatypes: opentys would allocate fresh index univars that appeared in no unified type, leaving them dangling at closed-check time. Fix: prepend a hand-built result type to the opened list so the freshly allocated univars are anchored to a type that participates in the subsequent unification against the scrutinee. Index refinement on match is deliberately out of scope: a vec<:0> scrutinee still admits an ICons-shaped pattern at the type level. Matches OCaml/Haskell parametric ADT semantics. Test file grows to 139 declarations covering constructor application, plain match, matchfix, indexed records, and field projection. Non-indexed datatypes/records continue to work unchanged.
Constructors of an indexed datatype are universally quantified over the index just like over type variables: INil has type forall n 'a. 'a ivec<:n>. Per-constructor result indices (GADT style) require both per-ctor result-type syntax AND index refinement on match, the latter being a much bigger dependent-typing feature.
…phization Replace the two CanNotTranslate raise sites in ecSmt for indexed Tconstr / Fop with a monomorphisation path. New helper EcAst.tindex_to_int reduces a tindex to a closed integer when possible (no free vars, no leftover univars); the SMT pipeline uses it to key two new caches (te_ty_idx, te_op_idx) by "path<:i,j,...>". trans_pty_idx / trans_tydecl_idx substitute idxvars by TIConst via EcCoreSubst.f_subst_init ~idx and emit fresh Why3 sorts named <path>_<i>_<j>... For indexed datatypes / records, all per-index constructor and projector variants are populated as a side-effect. trans_op_idx checks op_kind first: constructors / projectors / record-makers force their carrying type's monomorphisation (which populates te_op_idx); plain indexed operators get a fresh abstract Why3 symbol via create_op_idx. Bodies of plain indexed ops are dropped in this MVP — sound (treats the op opaquely) but limits SMT's unfolding across index instances. Goals with free index variables (e.g. an axiom binding [n]) still hit CanNotTranslate, preserving the per-goal skip behaviour: the existing try/catch around init / make_task emits the warning and the lemma falls through to "no provers" without a crash. Verified via 4 new SMT-discharge lemmas (160 declarations total in tests/indexed-types.ec) and a smoke test confirming non-indexed SMT goals are unaffected.
Lock in that lemma headers accept index params via the existing [n 'a] mixed_tyvars_decl syntax (shared with op binders). Discovered no fix was needed — the original "lemma binders don't accept index params" finding was a syntax confusion: separate brackets ['a] [n] are not supported (only the combined ['a n] form), and <:n> is the type-application framing while [:n] is the op-call framing. Two new lemmas exercise: a parametric proof using [trivial], and a quantified form using [move => ; trivial]. SMT discharge of goals with bound (non-closed) indices remains correctly skipped.
The printers for type declarations, operators, predicates, abbreviations, axioms and added-ops only emitted [tparams.tyvars], silently dropping the index binders. So [type [n] word.] would print as [type word.], hiding the index parameter from the user. New helper [pp_paramsannot ppe fmt (idxvars, tyvars)] prints the combined-bracket form [n 'a] matching the input syntax. All five printers now consult both lists; the per-kind operator printers (pp_opdecl_op / _pr / _nt) take a [ty_params] record instead of a bare tyvars list, and the dispatch in pp_opdecl passes op.op_tparams. Verified against /tmp/print_idx.ec: [type [n] word.], [type [n m] 'a vec.], [op cons [n 'a] : ...], [pred ix_pr [n 'a]], and [axiom ix_ax [n 'a]] all print their index binders.
The op grammar accepts an optional bracket-before-name for the opacity tags (opaque, smt_opaque). When users write [op [n] "_.[_]" (w : word<:n>) : bool] hoping to bind an idxvar [n], the parser greedily consumed the [n] as tags and silently discarded it, leaving [n] unbound in the type signature. Add a [disambiguate_op_brackets] helper invoked from both operator rule alternatives. If every entry in the leading bracket is in the known-tag whitelist, treat as tags (existing behaviour preserved for [op [opaque] foo], [op [opaque smt_opaque] foo], etc.). Otherwise reinterpret the bracket as a pure idxvar binder; if both the leading bracket and an after-name binder are present, raise a clear parse error rather than guessing. This fixes the canonical infix-style indexed-op declaration: type [n] word. op [n] "_.[_]" (w : word<:n>) : bool. which now parses with [n] correctly bound as an idxvar. Verified: full regression (182 decls), the original report case, and theories/datatypes/FMap.ec (heavy [opaque] tag user) still compile unchanged.
Indices and type variables now use distinct bracket families:
- {n m} for index binders
- ['a 'b] for type-variable binders
Indices come first when both are present.
Why: the previous mixed bracket [n 'a] was overloaded with the
op-leading [opaque] tags bracket, requiring a content-based
disambiguation that confused users when an unrecognised tag was
silently rewritten as a binder. With braces vs. brackets, the parser
disambiguates lexically and there is no overlap with op tags.
Parser:
- idxvars_decl now matches LBRACE lident+ RBRACE.
- mixed_tyvars_decl and bucket_mixed are gone, replaced by a single
ix_ty_binder rule that takes idxvars_decl? then tyvars_decl? and
returns (idxvars, tyvars_opt).
- The Gap-fix disambiguate_op_brackets helper is removed; the op
rules now read tags from the leading [...] and the binder from
the after-name {...} [...] pair without any reinterpretation.
- All consumers (operator x2, pred x2, inductive, notation, abbrev,
lemma_decl) switched to ix_ty_binder.
Pretty-printer:
- pp_paramsannot emits {idx} for indices and ['a] for tyvars,
separated by a single space when both are non-empty.
- pp_typedecl uses curly braces for the leading idx binder.
Tests: tests/indexed-types.ec (159 declarations) migrated to the new
syntax. Round-trip print produces text that re-parses unchanged.
FMap.ec (heavy [opaque] tag user) still compiles.
When an axiom / lemma / op / pred / abbreviation / notation binds
an idxvar [n] via {n}, the same ident now also resolves as an
int-typed local in the body of that declaration. Previously [n]
was only reachable in tindex positions like vec<:n>; using it as
an integer term (e.g. mkseq f n) failed with "unknown variable n".
This realises the Phase-2 design choice that idxvars and
formula-locals share a namespace: an idxvar is exactly an integer
binding, and the indexer / formula machinery agree on the ident.
New helper EcTyping.bind_idx_locals env ue pulls the idxvars out
of the unienv's tparams and binds each as a (id, tint) local in
env. Called immediately after every transtyvars ~idxparams site:
ecScope.add_r (axiom/lemma), ecScope op processing,
ecHiPredicates.trans_preddecl_r, ecHiNotations.trans_notation_r,
and ecHiNotations.trans_abbrev_r.
Verified with the original report case and a new regression in
tests/indexed-types.ec exercising [size (id_bits[:n] v) = n + 0].
Two related fixes that together let `rewrite L` and `apply L` work on lemmas declared over indexed types. 1. PTGlobal carries indices. The proof-term head `PTGlobal of EcPath.path * (ty list)` becomes `PTGlobal of EcPath.path * (tindex list) * (ty list)`. The constructor `ptglobal` and the alias `paglobal` gain an optional `?idxs` argument (default `[]`, so non-indexed call sites are source-compatible). `EcEnv.Ax.instantiate` also gains `?idxs`, substituting the lemma's idxvars in the spec. Without this, the proof checker re-instantiated only tyvars and the residual idxvars in the body broke conversion against the goal. 2. Closing a unienv now substitutes index-univars too. New helper `EcUnify.UniEnv.close_subst : unienv -> f_subst` builds a complete `f_subst` carrying both `~tu` (type-univars, as before) and `~iu` (index-univars). Used at the axiom-saving and op-saving sites in ecScope. Previously `Tuni.subst (close ue)` left every `TIUnivar` in the saved AST untouched, so even after the unifier resolved `?u_n := n_lem` the operator-type signatures inside the axiom's body still carried `?u_n`. Two `bits w` nodes that printed identically had different fresh univars and failed `is_conv`. Supporting infra: - `EcUnify.UniEnv.openidx` is exposed in the .mli (was private). Both `pt_of_uglobal_r` and `process_named_pterm` in ecProofTerm now open the lemma's idxvars to fresh `TIUnivar`s alongside its tyvars and thread both maps through `f_subst_init` to substitute the spec. - `EcMatching.MEV.assubst` adds `~iu:(iu_assubst ue)` so concretize resolves index-univars in the proof term and its formula together. - `EcMatching` `Fop` matching uses `unify_idx` for index lists (exposed in `EcUnify`) instead of structural `tindex_equal`. Verified: the user's `bits_cat` rewrite, `exact (test_eq w)` apply, and a new regression in tests/indexed-types.ec all work; full regression (184 decls) passes; non-indexed lemmas/rewrites unchanged.
…p targs
Three intertwined fixes for the user's [bits_cat] case:
lemma catE {m n} (wm : word<:m>) (wn : word<:n>) (i : int) :
0 <= i < m + n
=> (wm ++ wn).[i] = if i < m then wm.[i] else wn.[i-m].
proof.
move=> rgi @/"_.[_]".
rewrite bits_cat.
1. Op application records call-site indices in Fop targs.
`EcUnify.openty_r` now returns `(subst, ixs, tvs)` (was
`(subst, tvs)`); `select_op` returns
`(path, idxs, tys) * top * subue * sbody` (was `(path, tys)`);
`EcTyping.OpSelect.opsel.\`Op` and `opmatch.\`Op` carry
`path * tindex list * ty list`. `form_of_opselect` builds
`f_op p ~indices:ixs ~tyargs:tys ty`. Without this the call-
site indices were lost on Fop nodes — every `Fop` carried
`targs.indices = []` regardless of how the op was applied.
2. Op unfolding substitutes both tyvars and idxvars in the body.
`EcEnv.Op.reduce` was substituting only `tparams.tyvars`; now
it builds an `f_subst` with both `~tv` and `~idx` maps so that
every nested `Fop` in the unfolded body has its `targs.indices`
and `f_ty` rewritten to use the call-site indices.
3. Matcher does not unify Fop indices on the head.
The polynomial-against-polynomial `bits` head match
(`?u_m + ?u_n` against `m + n`) is genuinely ambiguous when
considered in isolation — multiple multi-univar Diophantine
solutions. The Fop matcher now only unifies type arguments and
trusts the surrounding `Fapp` arg matching to constrain indices
via per-arg f_ty unification (matching `(++) wm wn` first sets
`?u_m := m, ?u_n := n` individually, then `bits`'s polynomial
head trivially matches by reduction).
Every consumer of the new triple form was updated: ecHiInductive,
ecPrinting, ecScope (3 sites), ecTyping (4 sites), ecUserMessages.
Verified: full regression (202 decls) + new `unfold_then_rewrite`
test exercising the bug pattern.
…apply
When a lemma or op binds [{n}] and uses [n] both as a tindex AND as
an int term in its body (e.g. [size_bits {n} (w : word<:n>) :
size (bits w) = n]), substitution must reach BOTH namespaces:
- the tindex side ([TIVar n_lem] in [bits]'s targs), and
- the formula-local side ([Flocal n_lem] on the RHS).
Without the second part, opening the lemma at index [m] leaves a
dangling [Flocal n_lem] in the rewrite RHS, the goal becomes
[size (bits wm) = Flocal n_lem] (printed misleadingly as [... = n]
since both n_lem and m_caller share the name "n"), and the proof
cannot close. Same issue for [Op.reduce] when an op's body uses an
idxvar as int.
Fixes:
1. New [EcCoreFol.f_of_tindex : tindex -> form] projects a tindex
into the int-formula world. [TIVar id -> Flocal id : int],
[TIConst k -> f_int k], [TIAdd/TIMul -> f_int_add / f_int_mul].
Asserts on residual [TIUnivar].
2. [EcEnv.Op.reduce] (op-unfolding) and [EcEnv.Ax.instantiate]
(lemma application) now also bind [n_lem -> f_of_tindex idx] in
[fs_loc] alongside the existing [fs_idx] binding.
3. [EcProofTerm.pt_env] gains a [pte_idx_link] field recording each
lemma's [(idxvar ident, fresh tindex univar uid)] pairs;
[concretize_env] uses it to bridge the two namespaces during
proof-term concretization (when [?u_pat] resolves to [TIVar
m_caller], the corresponding [Flocal n_lem] in the body gets
bound to [Flocal m_caller]).
Verified: the user's [size_bits] / [bits_cat] / [catE] proof works,
plus a new regression case in tests/indexed-types.ec covering the
"idxvar used as int term in lemma RHS" pattern (214 decls total).
The previous fix for [pt_of_uglobal_r] (the no-instantiation lemma opener) wasn't carried over to [process_named_pterm] (the explicit [lemma[:idx]] / [lemma<:ty>] opener). Result: [have := mkK[:m + n]] on a lemma whose body uses [n] as an int term left a dangling [Flocal n_lem], breaking the proof checker with InvalidGoalShape. [process_named_pterm] now mirrors [pt_of_uglobal_r]: - For idxvars whose [openidx] returned a concrete [tindex] (because the user supplied [[:idx]]), bind [Flocal n_lem -> f_of_tindex idx] in [fs_loc] directly. The substitution flows into the formula immediately. - For idxvars whose [openidx] returned a fresh [TIUnivar] (the no-instantiation case), record [(n_lem, ?u)] in [pte_idx_link] so [concretize_env] can synthesise the form binding once unification resolves the univar. Same mechanism as [pt_of_uglobal_r]. Verified with the user's [have := mkK[:m + n]] case, plus a new regression in tests/indexed-types.ec exercising the explicit-index [have :=] pattern (227 decls total).
The previous fix made the matcher's Fop case skip index unification entirely, since polynomial-against-polynomial unification with multiple univars (e.g. [bits[:?u_m + ?u_n]] vs [bits[:m + n]]) is genuinely ambiguous in isolation. But that broke the simpler single-univar case: [rewrite mkK] (where mkK has one bound idxvar) no longer constrains [?u_pat] from the [mk[:?u_pat]] head, so the univar stays unresolved and the matcher concludes "nothing to rewrite". Make the index unification best-effort: try to unify each pair, and if a particular pair fails (multi-univar case), silently continue and let arg matching constrain the residual univars later. The single-univar case (handled by Gap-B's naked-univar fast path) goes through normally. Type unification on Fop heads stays mandatory. Verified: the user's [rewrite mkK] case now works, alongside the earlier [bits_cat] / [catE] cases (240 decls).
…ivars [Ax.instantiate], [Op.reduce], and [process_named_pterm] all bind [Flocal n_lem -> f_of_tindex idx] alongside the [TIVar n_lem -> idx] tindex substitution. But the call site can supply an [idx] that still contains an unresolved [TIUnivar] — happens when the matcher invokes [Ax.instantiate] before the surrounding unification has pinned the univar (e.g. on a chain like [apply: inj_bits; rewrite bits_cat. rewrite bits_cat]). The asserting [f_of_tindex] then crashes with the Phase-2 assert. New [EcCoreFol.f_of_tindex_opt : tindex -> form option] returns [None] when [ti] still contains [TIUnivar]. The three substitution sites use it to silently skip the form-side binding in that case; the form-side then gets resolved later by [pte_idx_link] at [concretize_env] time, once the univar is pinned. The asserting variant [f_of_tindex] stays for callers that have proven all univars are resolved. Verified: the user's [catA] / [apply: inj_bits; rewrite bits_cat] proof works (255 decls in tests/indexed-types.ec).
[h_tvar] is a [ty_params] record carrying both [tyvars] and
[idxvars], but the goal/hyps printers only displayed the type
variables. Lemmas with index binders (e.g. [{m n}]) showed an empty
"Type variables: <none>" line and no clue that [m, n] were in scope
as int-typed indices.
[pp_goal1] and [pp_hyps] now register the idxvars in the printer
env (via [PPEnv.add_locals]) and emit an "Index variables: m, n"
line above the existing "Type variables:" line whenever there is
at least one idxvar. The line is omitted entirely when no idxvars
are bound, so non-indexed lemmas look unchanged.
Verified: full regression (255 decls) passes; the line appears
during interactive proofs of any lemma with [{...}] binders.
Idxvars are non-negative integers by Phase-2 design. Expose this in
proofs by wrapping the goal — at proof-start time, not at lemma-save
time — with one [0 <= n_i =>] implication per idxvar. The user
introduces them on demand via [move=> Hn_i].
The wrapping is pushed INSIDE the lemma's [pa_vars] forall (not at
the very top) so the existing auto-introduction of [pa_vars] still
fires. So [lemma foo {n} (xs : T<:n>) : P] still auto-intros [xs];
the [0 <= n =>] hypothesis appears next, available via [move=>].
The implications never leak into the saved [ax_spec]: only the
proof goal sees them. Lemma application by other lemmas does not
require discharging [0 <= n] — the indexed-type discipline
guarantees it.
Also extend [EcSmt.lenv_of_tparams_for_hyp] to register each idxvar
as a top-level int constant in [te_lc], so [smt()] can talk about
the bound idxvars (else [trans_app]'s [Flocal] case would hit
[oget None]).
Verified: full regression (271 decls) plus three new test cases —
[idx_ge0_simple] (no [pa_vars]), [idx_ge0_smt] (multi-idxvar,
discharged via [smt()]), and [idx_with_args] ([pa_vars] auto-intro
still works alongside the new implications).
# Conflicts: # src/ecProofTerm.ml # src/ecProofTerm.mli # src/ecScope.ml # src/ecSubst.ml # src/ecTheoryReplay.ml # src/ecTyping.ml
- adapt main's new sty_subst call sites to record-shaped ty_params (.tyvars/.types), missed from the merge commit - drop now-unused 'open EcTypes' in ecHiPredicates (fatal under --profile=ci)
Allow naming index arguments at instantiation sites, independently of
the positional/named choice made for type arguments:
op f {n m} ['a, 'b] : 'a -> 'b -> bool.
op g = f[:n = 3, m = 4]<:'a = int, 'b = real>.
- parsetree/unify: the index side of an instantiation becomes its own
positional/named sum (IXunamed/IXnamed), carried by both TVIunamed
and TVInamed; the parser's 'cannot mix explicit indices with
named-tyvar syntax' restriction is gone (all four combinations are
legal).
- named index instantiation may be partial: unnamed idxvars fall back
to fresh index univars and are inferred (positional instantiation
still requires the full arity).
- unknown names now error instead of being silently ignored:
opentvi/openidx raise on a name binding no formal (safety net;
surface paths validate earlier), op selection filters candidates by
index-name subset, and pf_check_tvi checks lemma instantiations
('unknown index variable', 'wrong number of index parameters') the
same way it already checked type variables.
Requested by Alley Stoughton in #1065 (comment 1); the partial form
also gives a principled route around the confusing partial-positional
error (comment 4).
Tests: tests/named-index-instantiation.ec (all four combinations,
out-of-order names, partial op/lemma inference, five expect-fail
diagnostics). No regression: unit + prelude + stdlib green; ci
profile (warnings-as-errors) clean.
Member
Author
Done in 9460bc0: index and type instantiation can each be positional or named, in any combination. Named indices may be partial ( |
Explicit index instantiations were dropped when printing operator references: `op g = f[:3, 4]<:int, real>` printed back as `f<:int, real>` (PR #1065, Alley's comment 2). - pp_opname_with_tvi gains an index component: prints `f[:3, 4]<:int, real>`. - pp_opapp threads the Fop/Eop indices (callers pass the full targs record instead of .types). - suppression mirrors the type-argument policy: a new ixs_dominated (over a free-idxvar-of-type collector) hides indices inferable from the printed arguments' types; the showtvi pragma forces them. Everything prints through pp_form -> pp_opapp (pp_expr converts to a form), so goals, bodies, print and search output are all covered. Declaration printing (print f / added-operator messages) already showed {n m} binders. Tests: expect-by-print assertions in tests/named-index-instantiation.ec (shown / suppressed-inferable / printed-non-inferable). No regression: unit + prelude + stdlib green (incl. the print-asserting tests expect.ec / print-proc.ec / clone-type-inline.ec); ci profile clean.
Member
Author
Yes — fixed in 4908019: |
PR #1065, Alley's comments 3 and 4. An explicit instantiation incompatible with an operator produced "unknown variable or constant: `f'" (the tvi check ran as a silent candidate pre-filter, so the failed-application classifier never saw the candidate), and omitted indices died at declaration close as "this operator type contains free type variables". - ecUnify.select_op_outcomes: the tvi compatibility check moves from the EcEnv.Op.all pre-filter into the selection loop; an incompatible candidate now yields a classified KO (new op_failure variants OF_idx_arity / OF_idx_unknown / OF_tv_arity / OF_tv_unknown) before open/unify (openidx's arity fallback would otherwise let a wrong-arity candidate unify). Selection semantics unchanged. - op_instance becomes {oi_tys; oi_ixs}: application failures now report "where the index parameters were inferred as: n = 3" alongside the type parameters; failure-report types resolve BOTH univar kinds and normalize indices (display independent of constraint-solve order). pp_tindex joins the PrinterAPI. - uninferred indices are reported as such: UniEnv.closed splits into closed_tv/closed_iu; the close-check sites (op/pred/formula in ecScope, clone overrides in ecTheoryReplay, tyerror sites in ecProofTyping via new FreeIndexVariables) say "cannot infer all index parameters ...; supply them explicitly (e.g. `f[:n = 3]')" when only the index side is open. Tests: 6 new expect-fail assertions (omitted / partial-positional / unknown-named index, unknown-named / wrong-count tyargs, inferred-index report); the unknown-named-index assertion updates from the old "unknown variable or constant" text. No regression: unit + prelude + stdlib green (op-application-errors.ec byte-identical); ci profile clean.
tests/op-application-errors.ec is the file dedicated to asserting operator-application diagnostics; move the five UnappliedOp assertions from the named-index feature test there (own ixop/ivcat fixtures). named-index-instantiation.ec keeps the feature tests and the non-application diagnostics (duplicate named index, lemma-path pf_check_tvi checks, uninferred-indices close error). Also drop the index-normalization pass from resolve_ty_for_report: it was inert — ty hashconsing compares indices canonically, so a rebuilt vec<:8> IS the interned vec<:3+5> node and the display spelling is whichever got interned first (deterministic per file). Keep the real part (index univars resolved so reports never show ?#N) and document the hashconsing behaviour.
Member
Author
Both fixed in f2074ba. Omitted indices now report and an incompatible instantiation is classified per candidate instead of degenerating to "unknown variable or constant" — (same treatment for unknown named arguments and wrong type-argument counts). Application failures also list inferred indices alongside inferred type parameters. |
PR #1065, Alley's comment 5. Operator and predicate override clauses in `clone with' now accept index binders, in both alias and inline modes: clone U as U' with type {n} 'a foo = 'a vec<:n>, op f {n} ['a] (x : 'a) (xs : 'a vec<:n>) = cons[:n] x xs, pred p {n} ['a] (xs : 'a vec<:n>) = nonempty xs. Surface plumbing: idxvars_decl on the OP/PRED override productions (nonneg markers rejected), opov_idxvars/prov_idxvars parsetree fields, replay via transtyvars ~idxparams + bind_idx_locals, and a NotSameNumberOfIdxParam incompatibility (index arity of an override must match the overridden declaration). The work exposed three latent index bugs in shared infrastructure, all fixed: - EcEnv.Ty.unfold substituted only type parameters: unfolding an indexed type alias leaked its formal index variable, so `foo<:3>' failed to unify with its own unfolding `vec<:3>' (independent of cloning). - Compatible.for_ty renamed only the reference declaration's tyvars onto the override's; it now renames idxvars too. - EcSubst.open_oper (and get_open_oper/get_open_pred) opened operators at type arguments only; it now takes ~indices. Tests: tests/clone-indexed-override.ec (type-only, type+op+pred alias with conversion/print checks, inline mode with axiom-inlining assertion, index-arity-mismatch rejection) and tests/indexed-type-alias.ec (alias unfolding at concrete/symbolic indices, index arithmetic through the alias). No regression: unit + prelude + stdlib green; ci profile clean.
IWord.ec's msbE closed with smt(to_uint_cmp half_modulus) under the local z3 but not under the CI prover set (deterministic failure on every CI stdlib run; CI's cvc5 answers are unparsed by why3, and its z3 rejects the exponential goal). Rework the proof so no prover ever sees an exponential: discharge the 2^(n-1) facts with half_modulus/gt0_half while concrete, generalize the power to an opaque constant, and close the remaining linear-plus-division goals with explicit IntDiv hints (divz_ge0, ltz_divLR).
Member
Author
Right: the general problem (univars on both sides) subsumes solving polynomial systems over ℕ, so we do not attempt it. What is implemented is a small deterministic fragment, and the split matters. Checking index equality is complete: indices are compared by canonical polynomial normal form, which is decidable. Solving is restricted to (a) naked-univar assignment with an occurs-check, and (b) single-univar affine equations with net coefficient ±1 whose solution has non-negative coefficients, e.g. |
… sort
Review findings 11 and 3 (both with confirmed derivations of false).
The Why3 translation erases indices at the sort level; the old
justification ('a cross-width equation is ill-typed in EC') is
insufficient: an axiom quantifying over ONE width, e.g.
forall (c : bool array<:0>), size (ofarr c) = 0, loses its width
restriction and constrains the whole erased sort — collapsing
array<:1> and deriving false. Independently, lemma idxvars were
quantified as an unguarded forall n:int, asserting more than EC
proved (smt(ge0_index) proved 0 <= n for every integer).
Make the index recoverable at the term level for VALUES, as it
already is for operations:
- per-family width observers size_k : ('a,..) t -> int (one per index
position, polymorphic, declared on first use);
- quantifiers over head-indexed types are relativized:
forall (x : t<:i>), P ==> forall x, size_k x = i => P
(conjunct for exists; lambdas assert nothing). Guards are exact.
Where an indexed constructor occurs where observers cannot reach
(nested under another constructor / tuple / arrow, or as a type
argument of an indexed head) the binder raises CanNotTranslate and
takes the existing sound trans_gen fallback;
- lemma idxvars get 0 <= n premises (at the EC level, riding the
normal translation); goal idxvars get 0 <= n facts;
- goal locals at head-indexed types carry size_k x = i facts;
- every indexed operator gets a typing-justified result-width axiom
forall i xs, 0 <= i => size_k (f i xs) = e_k(i) — this is what keeps
guarded lemmas usable, not just sound (the 0 <= i premises keep the
union-of-widths model satisfiable at out-of-range indices; EC types
are inhabited so every natural-width carrier is non-empty).
Soundness: interpret the erased sort as the disjoint union of the
per-width carriers and size_k as the width tag; every EC model
extends, so Why3 proofs under guards are EC-valid.
Tests: tests/indexed-smt-guards.ec turns both reviewer exploits into
fail-smt regressions and checks the positive direction (width-0
lemmas prove width-0 goals through the guards; symbolic-width smt
still fires). No regression: unit + prelude + stdlib + examples all
green; ci profile clean.
Review findings 5, 6, 10 shared one root cause: the branch introduced a second univar kind (index univars, ue_iuf) and a combined closing substitution (close_subst), but left the legacy type-only close/assubst : unienv -> ty Muid.t exported — so ~30 call sites each chose independently, and the wrongly-chosen ones silently dropped resolved indices at persistence boundaries (dangling TIUnivar in proc bodies, have-hypotheses, abbrev bodies). Make the wrong choice inexpressible: close/assubst leave the public UniEnv API (they remain internals); the exported closing API is exactly close_subst (raising) and the new as_subst (non-raising), both returning the f_subst that resolves BOTH univar kinds. iu_assubst stays exported solely for the proof-term idx-link bridge. The compiler then enumerated every consumer (~30 sites, 13 files): ecProofTyping (finding 6: process_form/stmt/type/exp/poe, tc1_process_stmt), ecHiNotations (finding 10: abbrev), ecTyping (Pst_fun family, PSmatch, op-selection error paths — which now also DISPLAY resolved indices), ecTheoryReplay (clone-override op/pred closes — latent, unreported), ecScope (axiom close, subtype predicate, ring/field instance carriers), ecMatching (f_match's second component becomes the combined f_subst; its only caller ignored the map), ecReduction (user rewrite-rule instantiation), ecHiInductive, ecTypesafeFol, ecUserMessages, phl/ecPhlRwEquiv, phl/ecPhlRwPrgm. Most sites get simpler (no Tuni.subst wrapping). Tests: tests/indexed-univar-close.ec pins the three repaired behaviors (abbrev body linked to its binder instead of a frozen ?#N, proc bodies persisting resolved indices, have-hypotheses usable). No regression: unit + prelude + stdlib + examples green; ci profile clean.
Review finding 4 (confirmed derivation of false). Match-fix iota-reduction substituted only the operator's TYPE parameters into the body: the idxvar stayed dangling in both its namespaces (TIVar positions and its int-formula occurrences, e.g. a branch body that returns n), so f[:5] ... and f[:7] ... reduced to the SAME term and 'by cbv' proved their equality. New EcFol.f_subst_tparams instantiates an operator body at explicit targs the way EcEnv.Op.reduce already did correctly: tyvars via the type substitution, idxvars via the ~idx map AND via f_bind_local on their int-typed formula-local occurrences. Migrated four sites: - ecReduction iota (the reported one), - ecCallbyValue iota (its twin), - both rewrite-/op delta-unfold sites in ecHiGoal, whose destructuring tuple discarded the indices at construction (same bug shape, found by sweeping for the pattern; the tuple now carries the full targs and ty_params). Tests: tests/indexed-iota.ec — iota lands on the call-site index (cbv and simplify paths), the old collapse is REFUTED (f[:5] ... <> f[:7] ... by reduction), and rewrite /g on an indexed plain op unfolds correctly. No regression: unit + prelude + stdlib + examples green; ci profile clean.
…inks Review findings 7, 8, 9 (all with confirmed repros). LvMap (7): translvalue discarded the selected map-set operator's inferred indices ((path * ty list) payload); i_asgn_lv then rebuilt an index-erased op node whose arity contradicts the declaration. The lvmap payload now carries the full targs and the rebuild passes ~indices. Records + match desugar (8): trans_record opened the record type with the types-only openty and Tvar.init, so PFrecord built ctor/projection Fop nodes without indices, field/default types leaked formal idxvars, and the proc-match desugar built the projection without the scrutinee's indices. trans_record now opens via openty_r (combined substitution), threads the instance indices to both builders, and the match desugar reads the indices off the scrutinee's type. SMT side: there is no sound erased encoding of indexed datatypes/records yet (a width-erased nullary constructor plus the size axioms would be inconsistent), so trans_tydecl raises CanNotTranslate for them: goals degrade to the sound fallbacks instead of crashing with Why3 arity errors. Full index-threaded constructor encoding is left as documented follow-up. The 0 <= n guards also move to the Why3 level (w3_ge0 via the known-ops table): they no longer require the EC int theory to be in the file's scope. Proof-term links (9): propagate_idx_link / concretize_env resolved a link's univar with a single-hop map lookup, but ue_iuf is a chain map (?u := ?a, ?a := 7 read as unresolved), and concretize_env only handled literal TIVar/TIConst. Export UniEnv.repr_tindex (chain resolution) and use it at both sites; the link binding generalizes to any f_of_tindex-expressible index, so chains grounding in compound indices (m+1) concretize. Tests: tests/indexed-node-instantiation.ec (map-update wp proof, record node conversion, fail-smt degradation, chained and compound-chained proof-term application). No regression: unit + prelude + stdlib + examples green; ci profile clean.
…splay
Review findings 12 and 13.
Reachable arithmetic ring (12): both word ring structures registered
anonymously on word<:n+1>; instance lookup returned the first, so the
ℤ/2ⁿ structure was unreachable by the ring tactic. Fix = a NAMED
index-parametric instance, which required four machinery gaps to
close:
- instance declarations accept index binders
(instance ring [warith] with {n} word<:n+1> ...);
- instance operators are selected AGAINST THE REQUIRED TYPE at the
carrier (was: name-only selection + a tyvars-only type check, which
could not resolve index-parametric operators and mis-resolved
overloads);
- obligation lemmas carry the instance's ty_params (was: hardcoded
empty, leaving the instance's idxvars unregistered in the
obligation proof env);
- the registered Ring/Field environment items carry the instance's
ty_params (was: hardcoded empty, so an index-parametric direct
instance could never match a goal carrier);
- bare ring/field selection is two-pass, ANONYMOUS INSTANCES FIRST
(a named instance is deliberately addressable and must not capture
bare calls by registration recency).
The type-polymorphism prohibition on direct instances stays; only the
index side is opened up.
IWord: family-wide zeroa/onea constants, the [warith] instance with
obligations discharged from the generalized WRingA lemmas (explicit
[:n] instantiation -- obligations whose ops appear un-applied give
inference no anchor).
Honest index display (13): ixs_dominated suppressed [:...] whenever
an idxvar occurred anywhere in the argument types, collapsing e.g.
g[:3,4] v = g[:2,5] v to g v = g v in goal output. An idxvar now
counts as displayed only when an argument index DETERMINES it
(normalized affine in exactly that variable with unit coefficient),
matching the unifier's invertible fragment.
Tests: iword_ring.ec proves via ring [warith] at concrete and
symbolic widths and pins bare-ring-still-boolean;
named-index-instantiation.ec pins the compound-index display. No
regression: unit + prelude + stdlib + examples green; ci profile
clean.
Review findings 1 and 2 (both confirmed derivations of false), fixed
under the ENFORCE design: only index variables (and naturals, and
their sums/products) may instantiate an index.
Finding 1: propagate_idx_link resolved a lemma idxvar to ANY int
local the matcher bound it to -- matching [plus {n+} : 0 <= n]
against [0 <= k] for an arbitrary int local k bound n := k, proving
0 <= k for every k, hence false. The bridge (the single trust
boundary where matcher bindings enter the index world) now requires
every free variable of a candidate index to be a declared index
variable of the goal. A refused binding leaves the linked univar
unresolved, closed_iu fails, and the apply reports 'does not apply'.
Every other entry point already policed the discipline: the surface
grammar has no negative literals, index arithmetic is closed over
the naturals, the affine solver refuses possibly-negative solutions.
Finding 2: with the last entry point closed, every reachable
instantiation of a saved lemma satisfies 0 <= n, so stripping the
injected premise from the saved ax_spec is a JUSTIFIED proof-local
convenience, not a soundness hole. The stripping site now documents
the invariant and its supporting facts.
Tests: tests/indexed-nonneg.ec -- both exploit shapes as fail cases
(arbitrary local via a +-marked lemma; via an idxvar-premised axiom)
and positive controls (idxvar instantiation, and index arithmetic
n := k + 1). All four reviewer exploit files now die at the unsound
apply. No regression: unit + prelude + stdlib + examples green; ci
profile clean.
…aths Re-review finding (confirmed derivation of false). The applied-operator fast path in conversion compared Fop heads by path equality alone, discarding targs: f[:3] 0 and f[:5] 0 were convertible and trivial proved their equality. The bare-Fop conversion case one arm above already required for_targs; the Fapp fast path predates indices and was missed. The heads now count as equal only at the same instantiation (indices canonically, type arguments too — stricter than the old path-only test on the type side as well, with the full stdlib + examples suite unaffected). Distinct instantiations fall through to full conversion, which reduces or fails soundly. Tests: tests/indexed-iota.ec — canonically-equal indices still convert (h[:3] vs h[:2+1]); distinct indices refuse (fail by trivial). No regression: unit + prelude + stdlib + examples green; ci profile clean.
Medium-findings triage batch (review M4/M14/M15/M21 + the two re-review siblings). Freshening trio: axiomatized_op, the refinement-axiom builder, and fresh_idxparam all freshened tyvars only, leaving an idxvar's OTHER namespace dangling (tindex positions vs int-typed formula-locals) — generated/cloned indexed axioms were born unusable. New shared EcCoreSubst.f_freshen_tparams renames both kinds in both namespaces; fresh_idxparam also binds sb_flocal. Probing exposed a fourth member of the index-erased-node family: both builders constructed their generated op APPLICATIONS without indices (f_op ~tyargs only), so the axiomatized axiom crashed the SMT translation with a Why3 arity error; both now pass ~indices. Record let-patterns (M15): the LPRecord path built reccty without indices and re-opened the record params per field (each field got its own fresh index univars, then assert-false on unification). Build reccty with its indices, open ONCE via openty_r, share the instantiation across field types. Kernel index arity (M21): Ax.instantiate accepted an empty index list for an idxvar axiom and silently proceeded with an empty map, producing a dangling-idxvar statement. The index instantiation must now cover the axiom's idxvars exactly. Also re-probed M7/M22 from the original review: closed by the earlier univar-close/chain-link and CanNotTranslate-punt commits. Tests: tests/indexed-idxvar-freshening.ec (axiomatized-by op usable via smt with the axiom shape pinned by expect-print — and now displaying its index argument; indexed-rewrite control; clone-freshened indexed lemma). No regression: unit + prelude + stdlib + examples green; ci profile clean.
The sound conversion guard (97ff8ba) exposed that the warith instance's expr/ofint obligations were ill-indexed from birth: WRingA.exp's own index parameter is the carrier's PREDECESSOR (exp {n} : word<:n+1> -> ...), the instance machinery applies every operator at the carrier's indices, and exp[:wsz] vs exp[:wsz+1] had been 'convertible' only because the old fast path ignored index arguments. (The prior sweep that was believed to validate 97ff8ba had aborted at the unit scenario and never ran stdlib.) r_exp/r_ofint are optional slots with default tactic encodings: supplying predecessor-shaped operators was simply incorrect. Drop them; document the family-shape constraint at the instance (it has now bitten twice: zeroa's first declaration, then exp/ofint). This also explains and retires the previously shelved InvalidGoalShape-in-obligation anomaly -- same ill-indexed obligations, different choke point. ring [warith] still proves the arithmetic test goals (exponent- and literal-free encodings via the defaults). Full sweep genuinely green this time: unit + prelude + stdlib + examples all ran; ci profile clean.
Follow-up to be23c4c, which removed IWord's ill-shaped expr/ofint slots but left the MACHINERY hole: the instance layer (rapp / inject_indices / ring_axioms) applies every registered operator at the carrier's indices, yet operator selection accepted any operator whose type merely unified with the required one -- a predecessor-shaped operator (exp {n} : word<:n+1> -> ..., whose own index parameter resolves to the carrier's predecessor) slipped through and produced ILL-TYPED obligation formulas downstream (anomalies or unprovable goals; previously masked by the unsound conversion fast path). check_tci_operators now compares the selected operator's resolved, normalized index instantiation against the carrier's indices and rejects mismatches with a real diagnostic: operator ... is not parameterized by the carrier's indices (instance operators are applied at the carrier's own index arguments) This covers ring, field, and general instances, and also catches zero-idxvar operators supplied for an indexed carrier. Tests: tests/instance-family-shape.ec (predecessor-shaped rzero rejected; message documented in-comment -- hierror embeds locations, so only failure is asserted). IWord's family-shaped warith instance unaffected. No regression: unit + prelude + stdlib + examples all ran and are green; ci profile clean.
Development notes; superseded by the commit history and the PR description. The design decisions it recorded live in the code comments at their enforcement sites (the naturals discipline at ecScope.start_lemma / ecProofTerm.propagate_idx_link, the family-shape constraint in IWord.ec / ecScope.check_tci_operators).
Medium findings M19 and M18.
Elimination (M19): case/elim on indexed datatypes, records, and
inductive predicates failed ('cannot recognize elimination
principle') or anomalied. Two layers:
- the scheme GENERATORS built every self-type and constructor
occurrence without indices (indsc_of_datatype x3, indsc_of_record
x2, indsc_of_prind, introsc_of_prind, datatype_projectors), so the
generated ivec_case/r_ind/intro schemes were ill-shaped from birth
and the elimT recognizer rightly refused them; all generators now
emit properly indexed statements;
- the application plumbing dropped indices: t_apply_s/tt_apply_s gain
?idxs (threaded to ptglobal), scheme_of_ty returns the full targs,
and t_elimT_ind / t_elim_prind_r pass the instance indices.
Matching (M18): f_match's index unification on Fop heads tolerated
ALL failures, letting GROUND index mismatches through to
InvalidGoalShape anomalies downstream. The tolerance is now split by
groundness: univar-free unequal indices fail the match immediately;
univar-containing ones keep the defer-to-arg-matching behavior.
Tests: tests/indexed-elim.ec (auto and explicit case/elim on an
indexed datatype at symbolic width, record induction, prind case
analysis, ground-mismatch rewrite refusal, univar index inference).
No regression: unit + prelude + stdlib + examples all ran and are
green; ci profile clean.
…sserts Medium findings M16, M17, M20 + rider cleanups. Transactional unification (M16): unify_core mutated the unienv in place, leaking partial type/index assignments through failure into non-restoring paths (the matcher's MatchFailure handlers). Failure now restores the entry state by default. The failure-CLASSIFICATION path opts out (~transactional:false) on its throwaway unienv: the rich UnappliedOp diagnostics -- 'inferred as' sections and resolved expected types -- are precisely the partial assignments of a failed unification, read back deliberately (the exact-text error suite caught that dependency). Link consistency (M20): propagate_idx_link now reports when the matcher's evar binding and the unifier's index resolution CONFLICT; can_concretize refuses instead of concretize_env silently preferring the unifier's value. openidx contract (M17): the positional-arity inference fallback is documented as select-loop-only; all other callers validate arity beforehand. Riders: duplicate UniEnv-internal resolve_tindex removed (one definition; repr_tindex aliases it); dead 'ignore before' dropped; Ty.unfold asserts index arity (corrupt applications fail loudly); Op.reduce restored to asserting on arity mismatch instead of silently skipping the substitution; dead CE_IndexedNotYetSupported removed. No regression: unit + prelude + stdlib + examples all ran and are green; ci profile clean.
- IndexMismatch resolves both sides through the unienv before
reporting; the renderer distinguishes a ground mismatch
("incompatible index arguments: `5' vs `3'") from a genuinely
unsolvable unification (fragment named explicitly)
- negative index literals get a dedicated error instead of an
unbound-variable message; subtraction in index position gets a
parse error with a naturals hint (grammar stays conflict-free)
- f_of_tindex univar-free contract documented; the assert in the
SMT translation is the invariant check (forms reaching SMT are
closed by construction since the closing-API consolidation)
- drop a stale comment describing the abandoned per-index
monomorphisation design in ecSmt
…rrors
- section-declared indices no longer inject an automatic [0 <= n]
premise into proof goals: the goal now matches the stated lemma and
proofs needing the fact obtain it explicitly from the new
Int.ge0_index {k+} lemma; IArray/IWord migrated (only 6 of ~100
proofs actually needed it -- int2bs/nseq size side conditions and
exprS); the opt-in `+' binder marker is unchanged, and IArray's
array-taking ge0_index is subsumed and removed
- duplicate `declare index' (across declares or within one) is
rejected with a located error; first direct test coverage for
declare-index sections
- nested `<:...>' applications ending in `>>' get a dedicated parse
hint (the token is a single operator; write `> >'); a lexer-level
split is not safely possible (context-free lexer, `>>'/`>>>' are
legitimate operator tokens)
- gt0_pow2 / dvd2_pow2 / modz_cmp / divz_cmp / bound_abs move from IWord's numeric section to IntDiv (they are pure-integer facts; Jasmin's JUtils exports the same statements, which can now defer to the stdlib); gt0_pow2 proved directly instead of via smt - name the model backing the IArray/IWord axioms (length-n lists / bool arrays) as the consistency argument - pack_mult regression closes with its real proof instead of admit
`t<:n = 3, m = 5>' now mirrors the op-site `f[:n = 3]' form: any
order, partial (missing indices are inferred, like the `_' hole).
PTapp carries a pidxannot instead of a bare pindex list; the grammar
reuses idx_byname1 and stays conflict-free. Unknown names ("type `t'
has no index parameter named ...") and duplicates error with
locations.
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.
Adds integer-indexed types to EasyCrypt: type constructors parameterised by both type variables and natural-number indices, with a small index language and decidable index equality. This lets you express size-carrying types like
'a vec<:n>and track index arithmetic through operators, lemmas, and cloning.