Version 1 Boole feature requests

[kondylidou]

Issue #, if available:

Description of changes:

Summary

This PR brings the Boole feature-request suite, working examples, and documentation back into sync with the current state of the Boole pipeline.
It updates both the implementation and the example/backlog story so the repo more accurately reflects what is supported today versus what is still an open request.

Main changes

• Implemented and documented Boole extensional equality for direct Map types via =~=, lowering it to an explicit quantified formula during translation.
• Fixed nested for lowering end to end by:
  • generating fresh Core block labels for lowered for loops
  • changing loop elimination so it havocs only loop-carried variables, not block-local inner-loop indices
• Moved examples into more accurate categories:
  • square_matrix_multiply is now a main working Boole example
  • string_operators is now a main working Boole example
  • horner_poly_eval remains a feature-request seed
  • binary_search was removed
• Refreshed Boole examples and feature-request seeds to use the current Boole style more consistently:
  • newer quantifier style
  • clearer per-file request/status comments
  • #guard_msgs snapshots
  • smtVCsCorrect proofs where appropriate
• Reworked docs/BooleFeatureRequests.md so it now:
  • records current priorities
  • has an implemented-features section
  • tracks the curated Boole seeds with current status
  • includes a Source column showing where each seed came from
• Added direct Verus source links to the relevant feature-request files so the local Boole seeds are easier to trace back to upstream examples.

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