[kondylidou]

Fixes #1482

Problem

Sequence.select!, update!, take! and drop! are the total variants of Sequence.select, update, take and drop: the same function without the bounds precondition. The SMT encoder emitted each pair as two unrelated uninterpreted functions, so the solver could not conclude that they agree, even for an index that is in bounds:

program Core;

const g : Sequence int;

procedure P()
{
  assume [g_len]: Sequence.length(g) == 2;
  assert [select_pair]: Sequence.select(g, 0) == Sequence.select!(g, 0);
};

select_pair came back unknown, and the same held for the other three pairs.

A program therefore could not use both forms on one sequence: a fact stated with one did not apply to the other. This matters for front ends whose source language distinguishes them. In Verus, a spec-level read is total and an exec-level read is checked, and both denote the same element.

Change

The encoder now emits the solver symbol of the total twin for both forms. The change is confined to the point in SMTEncoder.lean where a factory function becomes an uninterpreted function.

• The bounds precondition is discharged as a separate obligation before encoding, so it is unaffected.
• No axiom is added. The axioms already mirrored onto the total variants become identical terms and are deduplicated by the encoder's axiom set.

Testing

A new test in StrataTest/Languages/Core/Examples/Seq.lean asserts the four equalities. All eight obligations (four bounds checks, four equalities) pass. The existing sequence tests are unchanged.

[shigoel]

Could this use factory function names instead of brittle strings?

[shigoel]

Could you add one out-of-range case, e.g. assert Sequence.select(g, 5) == Sequence.select!(g, 5) with length(g) == 2?

[shigoel]

(a) This runs on every function the encoder sees and takes the full name apart each time. toSMTOp already has the short name (baseName) a few lines up. Checking that first would skip the work for every op that isn't one of these four. Also, the tys.isEmpty case can't happen, so it could go.

(b) This only works because each ! op has the same axioms as its checked twin. Now that they share one solver symbol, only the axioms of whichever form appears first get loaded. If someone later adds an axiom to just one of them, it would be lost or applied to both. Could you add a short note on the four ! definitions in Factory.lean saying their axioms must stay the same as the checked versions?

[shigoel]

@kondylidou Thanks for this PR! Can we consider another design here, where functions like Sequence.select are rewritten to Sequence.select! before we even reach the SMT encoder? This way, we won't have to manually make sure they both lower to the same SMT function.

This came up during an internal discussion with @aqjune-aws. Also, CC: @joscoh for thoughts.