Boole language extensions for dalek-lite benchmarks

[kondylidou]

Summary

Extends the Boole language pipeline with new language features, curated benchmark
targets anchored to dalek-lite (Curve25519/Ed25519), and a testing infrastructure
upgrade across all Boole seeds.

Language features

Sequence T type and slicing ops

• toCoreMonoType handles .Sequence _ elem → .tcons "Sequence" [elem]
• All 8 Core inherited ops wired up in Verify.lean
• Three Boole-specific wrappers: Sequence.skip, Sequence.dropFirst,
  Sequence.subrange
• Typed empty-sequence constants: Sequence.empty_bv8/bv16/bv32/bv64/int — each
  needs a distinct token since 0-ary polymorphic Sequence.empty has no arguments
  to infer the type from

Bitvector loop variables (for i : bvN := init to limit)

• for_to_by and for_downto_by dispatch guard/step/increment to
  Bv{N}.ULe/Add/Sub when the loop variable is a bitvector type

decreases annotations

• for v := init to/downto limit accepts an optional decreases e clause;
  forwarded to the Core while-loop measure field and actively verified by cvc5
• Functions and procedures accept an optional decreases e clause using Core's
  existing Measure category — no new grammar category introduced
• All three forms reuse Core's single measure_mk op; no duplicate constructs
• Function termination is verified by Add termination checking for recursive functions #1092; procedure-level decreases is
  silently dropped with a dbg_trace warning pending int-based termination support

Lambda abstraction and application

• fun x : T => body lowers to nested Core .abs nodes
• (f)(x) lowers to .app () f x

Inline let-block postconditions

• let v := e in body in spec/ensures positions lowers via withBVarExprs

choose assignment

• w := choose z : T :: pred(z) lowers to havoc w; assume pred[z/w]

Bitvector comparisons

• Unsigned (<, <=, >, >=) default to Bv{N}.ULt/ULe/UGt/UGe via
  toBvCmpOp
• Signed (<s, <=s, >s, >=s) lower to Bv{N}.SLt/SLe/SGt/SGe

New seeds

• embedded_postcondition.lean — inline let-block in ensures
• montgomery_loop_invariant.lean — relational while-loop invariant; linear
  arithmetic case verifies via cvc5 and smtVCsCorrect
• scalar_reduce.lean — B2 reduce() axiom with abstract types
• sha256_compact_indexed.lean — SHA-256 compact port (indexed Sequence
  encoding); all 19 VCs pass; loop counters use int (faithful to Rust's usize
  semantics, avoids uninterpreted cast to Sequence index); remaining gaps:
  iterator protocol (Improve Strata DDM documentation #27), fixed-size array syntax (Add bv1 type to Strata.Boogie #25), slice types (Update copyright headers to reference both MIT and Apache 2.0 licenses. #26)

Fully implemented seeds graduated from FeatureRequests/ to the main Boole test
folder: early_return.lean, choose_operator.lean, bitvector_ops.lean,
embedded_postcondition.lean.

Seed test infrastructure

Replaced #guard_msgs (drop info) in with explicit /-- info: ... -/ +
#guard_msgs in across all Boole seeds. Added (options := .quiet) uniformly.

Documentation

• New docs/BooleBenchmarks.md: five real-world benchmark targets from dalek-lite
• Updated docs/BooleFeatureRequests.md: all new seeds in inventory table,
  implemented features extended

By submitting this pull request, I confirm that you can use, modify, copy, and
redistribute this contribution, under the terms of your choice.

[joscoh]

Can you change the PR to target main2 and remove the comments about things being upstreamed to main?

[kondylidou]

Can you change the PR to target main2 and remove the comments about things being upstreamed to main?

done:)

[shigoel]

LGTM, modulo the partial functions -- won't block on that right now though