chore: update to lean4.25

[RSoulatIOHK]

Bump to lean 4.25

Description

This pull request adds support for optimizing the String.take operation in the string optimization pipeline and updates the codebase to use String.Pos.Raw.get for character access, ensuring compatibility with the latest Lean version. It also bumps the Lean toolchain to v4.25.0.

Type of Change

•  Lean dependency update
• Bug fix (non-breaking change fixing an issue)
• New feature (non-breaking change adding functionality)
• Breaking change (fix or feature causing existing functionality to change)
• Documentation update
• Performance improvement
• Code refactoring
• Test updates

Related Issue

• Fixes #(issue number)
• Closes #(issue number)

Changes Made

• Added an optimizeStrTake function to handle simplification and normalization of fully applied String.take operations, including constant folding when possible. (Blaster/Optimize/Rewriting/OptimizeString.lean, [1] [2]
• Registered String.take in the set of opaque functions for optimization. (Blaster/Optimize/Opaque.lean, Blaster/Optimize/Opaque.leanL66-R67)
• Updated usages of character access from str.get/line.get! to String.Pos.Raw.get/String.Pos.Raw.get! for improved correctness and compatibility with Lean 4.25.0. (Blaster/Smt/Syntax.lean, [1]; Blaster/Smt/Env.lean, [2]
• Upgraded the Lean toolchain from v4.24.0 to v4.25.0. (lean-toolchain, lean-toolchainL1-R1)

Testing

Test Coverage

• Added new tests for new functionality
• Updated existing tests
• All tests pass locally
• For bug fixes: Added example to Tests/Issues/ folder

Documentation

• README updated (if applicable)
• Code comments added/updated
• Doc comments added for new optimization/rewritting rules

• My code follows the project's style guidelines
• I have performed a self-review of my code
• I have commented my code, particularly in hard-to-understand areas
• I have made corresponding changes to the documentation
• I have added tests that prove my fix is effective or that my feature works
• New and existing unit tests pass locally with my changes using make check_all
• For bug fixes: Original failing example added to Tests/Issues/ folder with reference to issue number

Additional Notes