Laurel cannot prove two sequences equal; extensionality needs its own trigger (Sequence.equal)

[keyboardDrummer]

Problem

Laurel cannot prove that two sequences are equal, except when one is syntactically the other.

Sequence lowers to an uninterpreted SMT sort, and its Core axioms (Strata/Languages/Core/Factory.lean) are all pointwise: they state how long a result is and what sits at a given index. Nothing relates two separately-constructed sequences. So goals like these are all unprovable today:

procedure takeOfBuildIsOriginal(s: Sequence<int>, v: int) {
  assert seqTake(seqBuild(s, v), seqLength(s)) == s   // not provable
}

procedure updateToSameValue(s: Sequence<int>, i: int)
  requires 0 <= i requires i < seqLength(s) {
  assert seqUpdate(s, i, seqSelect(s, i)) == s        // not provable
}

This is a routine shape in specifications — "removing what I just appended gives me back the original" — so the gap is felt quickly by anyone writing sequence specs.

What's needed

1. An extensionality axiom

Two sequences of equal length that agree at every index in [0, length) are equal:

∀ s t. length(s) == length(t)
       ∧ (∀ i. 0 <= i < length(s) → select(s, i) == select(t, i))
       → s == t

The inner ∀ belongs in the antecedent, so it skolemises to a single witness index rather than being instantiated — the Dafny/Boogie formulation.

This is consistent under the current uninterpreted-sort encoding, and List.ext_getElem discharges it against the List model in Strata/Languages/Core/SeqModel.lean.

It must be mirrored over Sequence.select!. A Laurel spec lowers seqSelect to the unsafe selector, and Sequence.select / Sequence.select! are separate uninterpreted functions with nothing relating them. Without the mirror (withSelectBang), no pointwise hypothesis written in a Laurel requires can ever discharge the antecedent — verified empirically: the direct-use test fails without it and passes with it.

2. A way for the axiom to actually fire — the harder half

An extensionality axiom alone is not enough, and this is the substance of this issue.

Attaching it to seqLengthFunc with the trigger {length(s), length(t)} makes direct use work: if a spec states seqLength(s) == seqLength(t) plus pointwise equality, assert s == t is proved. But the motivating case above is still not proved, because the trigger can only bind sequences whose length is a ground term in the goal, and Sequence.length(Sequence.take!(Sequence.build(s, v), Sequence.length(s))) never appears there.

Measured with the axiom in place:

configuration	seqTake(seqBuild(s, v), seqLength(s)) == s
cvc5 1.3.4, Strata's default flags	unknown
cvc5 1.3.4 --enum-inst	proved
z3 4.12.6, default	proved

Diagnostics establishing that the trigger, not the axiom, is the blocker:

• Stripping the :pattern entirely does not help — cvc5 infers the same length patterns and still returns unknown.
• Adding the missing length term as an explicit assume makes it pass under default cvc5.
• A proved assert is not carried forward as an assumption in Strata, so an assert-shaped hint does not work as a user-level workaround.

The instantiation cost of the axiom itself is negligible (6 e-matching instantiations on the direct case), so this is not a performance trade-off — the axiom simply never fires where it is needed.

Proposed fix, following Dafny: introduce a Sequence.equal(s, t) function, state extensionality with {Sequence.equal(s, t)} as the trigger, and rewrite == at type Sequence τ to Sequence.equal in the front end / encoder. Triggering on the equality predicate rather than on length means the axiom fires exactly when a sequence equality is being decided, with no dependence on which length terms happen to appear. This requires:

• a new factory function and its axiom in Core.Factory
• encoder awareness of Sequence.equal
• rewriting sequence equality at the Laurel and/or Core surface
• the corresponding SeqModel soundness theorem

3. Constraint on any future datatype encoding of Sequence

If Sequence τ is ever encoded as a freely generated datatype — e.g. a constructor pairing a length with an Array Int τ — then the extensionality axiom above becomes inconsistent, because mkSeq(-1, arr) is a legitimate value of such a sort and the selector law makes the axiom false there. Confirmed directly:

(declare-datatypes (($Seq.int 0)) ((($mkSeq.int ($seqLen.int Int) ($seqElems.int (Array Int Int))))))
(assert (forall ((s $Seq.int)) (>= ($seqLen.int s) 0)))
(check-sat)   ; unsat

The same reasoning applies to any global ∀ s over such a datatype, including a length >= 0 axiom. Such an encoding therefore needs a validity predicate — valid(s) holding when the length is non-negative and elements outside [0, length) are the element default — with the global axioms guarded by it, validity asserted where sequences enter the problem and shown preserved by each operation, and the guard applied to every user-written quantifier over a Sequence.

Acceptance criteria

• seqUpdate(s, i, seqSelect(s, i)) == s is proved under the default solver configuration
• seqTake(seqBuild(s, v), seqLength(s)) == s is proved under the default solver configuration
• Must-fail twins still fail: equal lengths alone do not give equality; pointwise agreement over a shorter range with different lengths does not give equality
• The axiom is mirrored so Laurel specs written with seqSelect can discharge the antecedent
• A SeqModel theorem shows the axiom holds of the List model
• No regression in instantiation counts on sequence-heavy VCs