Guard choose axioms and support sequence extensional equality

[yashmehta00]

Fixes two issues opened about Boole’s verification semantics (#18 and #19):

1. Guard choice-function axioms with predicate existence, preventing unsatisfiable predicates from introducing contradictions. Functions remain total, with predicate guarantees available once existence is established, matching Verus semantics.
2. Support =~= for Sequence T as equal lengths and pointwise equality within bounds, preserving bound-variable scoping.

Seed tests are written as general specifications wherever possible: they characterize sequence equality, establish the guarded choice law, and use cover to exhibit a countermodel to the old unconditional axiom.

Result

• The unsatisfiable-choice reproduction no longer verifies ensures false.
• Satisfiable choice functions retain their guarantees given existence.
• The guarded-law spec passes; the old-law countermodel cover changes from fail to pass.
• Sequence equality supports matching elements and requires matching lengths.
• docs/BooleFeatureRequests.md and related comments updated.
• lake test passes.

[kondylidou]

Thanks for this. Could you split it into two PRs? The two halves are in different states.

PR 1, choose: ready once split out. The guarded axiom is the right fix, and I checked the de Bruijn indices through both binders. The tests are well chosen, in particular the no-precondition case moving from pass to unknown, and the cover test showing the old law has a countermodel.

PR 2, sequence =~=: on hold for now. Two concerns:

The new test asserts (a =~= b) <==> (equal length && in-bounds pointwise equality), but =~= is lowered to exactly that formula, so the solver is checking X <==> X. It cannot fail.
The lowering does not connect to ==. On this branch, requires a =~= b; ensures a == b returns unknown, because Sequence is an uninterpreted sort with no extensionality. The operator can be stated but not used to conclude two sequences are equal.
Whether to address that with a native Seq encoding (as useArrayTheory does for Maps) is being discussed on Zulip, and the outcome may make this lowering unnecessary. Please keep this part as a draft PR until that is settled.

Docs, for PR 1: please limit the docs change to the choose entry. The current diff renumbers the gap list per section, which breaks the cross-references that use the old global numbers (Gap #1, #6, #8, #13, #15), and it moves the backticks in all 29 seed-table links so they render as literal text. Both look like formatter side effects.

[yashmehta00]

Thanks, I'll split them up so you can close this one.

PR1, I resubmitted this here #22 , making sure the docs links match the original and global numbering stays. Just noting that though choose is mentioned again outside the Implemented Feature Requests, in number 18, I'm leaving it there and updating the wording.

PR2, for sequences, I understand that for Maps == and =~= align because with useArrayTheory, pointwise equality automatically establishes ==. The scope in issue #18 seems limited to lowering =~= to equal length and bounded pointwise equality, and from Zulip it sounds like Abdal is going to address == with a native Seq encoding, so I will leave that out of PR2.
On that note, my understanding was that the test should check the Boole-to-Strata lowering of =~=, so the test I wrote ensures (a =~= b) <==> (Sequence.length(a) == Sequence.length(b) && (∀ i: int . 0 <= i && i < Sequence.length(a) ==> Sequence.select!(a, i) == Sequence.select!(b, i))); would fail if the lowering is not done correctly, and the solver checking X <==> X would mean the expression was lowered as intended. (I used the unsafe .select! to avoid a redundant bounds check). Clark seemed to say that the spec should be as general as possible, but I can add another test too.

[kondylidou]

Thanks, I'll split them up so you can close this one.

PR1, I resubmitted this here #22 , making sure the docs links match the original and global numbering stays. Just noting that though choose is mentioned again outside the Implemented Feature Requests, in number 18, I'm leaving it there and updating the wording.

PR2, for sequences, I understand that for Maps == and =~= align because with useArrayTheory, pointwise equality automatically establishes ==. The scope in issue #18 seems limited to lowering =~= to equal length and bounded pointwise equality, and from Zulip it sounds like Abdal is going to address == with a native Seq encoding, so I will leave that out of PR2. On that note, my understanding was that the test should check the Boole-to-Strata lowering of =~=, so the test I wrote ensures (a =~= b) <==> (Sequence.length(a) == Sequence.length(b) && (∀ i: int . 0 <= i && i < Sequence.length(a) ==> Sequence.select!(a, i) == Sequence.select!(b, i))); would fail if the lowering is not done correctly, and the solver checking X <==> X would mean the expression was lowered as intended. (I used the unsafe .select! to avoid a redundant bounds check). Clark seemed to say that the spec should be as general as possible, but I can add another test too.

You're right on scope. Issue #18 asks for exactly this lowering and not for ==. That part is being handled separately, so leaving it out is correct.

You're also right that your test checks the lowering: it fails if the lowered formula is not equivalent to the one stated. I put that too strongly before.

What I'd still ask for are the two cases in #18's acceptance criteria, since they show the operator working in a program, not only how it is lowered:

1. Sequences with equal length and equal elements: assert a =~= b verifies.
2. Sequences of different lengths: assert a =~= b fails.

Keep your current test as well. One more option, if you want it: map_extensionality.lean checks the Map lowering structurally with a #guard on the lowered Core expression. A matching #guard for sequences would pin the exact shape, including the select!.