deps(deps): bump hax-lib from 0.3.7 to 0.4.0

[dependabot]

Bumps hax-lib from 0.3.7 to 0.4.0.

Changelog

Sourced from hax-lib's changelog.

[0.4.0] - 2026-09-04

Changes to the Rust engine:

• Fix diagnostic reporting

Changes to the OCaml engine:

• Don't fail when an item carries a hax attribute pointing to an item that another backend cfg-ed out. Backend-specific item quotes such as #[hax_lib::legacy_lean::before(..)] used to abort extraction to any other backend with Could not find item with UID ... (#2026)
• Drop rustc's internal <cfg_trace>/<cfg_attr_trace> marker attributes, which made the engine print Rust code that could not be parsed back (#2026)

Changes to the frontend:

• Fix all observable issues in the new rust version of the THIR importer
• Add access to representation information of other types than just enums

Changes to cargo-hax:

• Manage aeneas and charon versions with cargo hax tools, pinned via a committed hax.toml, installed from pre-built binaries verified against a shipped manifest
• cargo hax into lean generates a complete, buildable Lean package by default (#2142)
• Publish a pre-built cargo-hax binary per supported platform with every release, so that cargo binstall cargo-hax installs it without building
• Make cargo install cargo-hax build on any recent toolchain, so that the lean backend can be installed on its own and pinned per project with cargo-run-bin; the JSON schema exporter the OCaml engine's build consumes moved behind the new legacy-engine feature
• Add proof scenarios: named extraction configurations committed as [scenario.<name>] tables in hax.toml, run with the new cargo hax extract [NAME]... subcommand into per-scenario proofs/<scenario>/<backend>/ directories
• Add support for specifications written with anodized: #[spec(requires: ..)], #[spec(ensures: ..)] and #[spec(maintains: ..)] now extract as pre- and postconditions, on every backend
• Validate driver reports on cargo's stderr: only haxmeta files of workspace crates under the run's target directory are accepted, and a lost or partial report set fails the run instead of silently producing an incomplete extraction
• Exit with a failing status whenever an error was reported
• Make traits from core with default methods visible to charon so that impls of these traits have the right defaulted implementations (#2172)

Changes to the hax-lib crate:

• Add hax_lib::ensures_ref, an ensures whose closure takes the result by reference, for postconditions over a type that is not Copy
• Remove dependency to proc_macro_error2 (unmaintained) (#2039)
• Keep the generics of a struct in scope in the refinement functions generated by #[hax_lib::attributes], fixing refinements on fields that mention a const generic (#899)
• Allow specifications on the methods of an impl block whose signature mentions an associated type of Self. The cases that remain unsupported (trait declarations, and associated types the block does not define) now fail with an explicit error instead of invalid code (#2089)
• Support quote annotations (before, after, options) on inherent impl blocks and on their items (#1698)
• Support requires, and ensures written behind a cfg_attr in

... (truncated)

Commits

• f8fe693 Merge pull request #2223 from cryspen/release/v0.4.0
• b97bc0b Merge pull request #2215 from cryspen/fo2-reconstruct-asserts-else
• e490157 fix(engine): reconstruct asserts only when there is no else branch
• aeaec2e chore: release v0.4.0
• e17ec42 Merge pull request #2214 from cryspen/gat-impl-bounds-guard-1907
• 122a981 fix(frontend): resolve trait bounds on generic associated types
• f0ea8ec fix(engine): keep the else branch in assert reconstruction
• fd47c62 fix(frontend): guard GAT associated-type bounds against the instantiate_super...
• 15fd124 Merge pull request #2213 from cryspen/fix-standalone-install-merge-queue
• 16bf684 Merge pull request #2212 from cryspen/fstar-quote-callsite-spans-040
• Additional commits viewable in compare view

Dependabot will resolve any conflicts with this PR as long as you don't alter it yourself. You can also trigger a rebase manually by commenting @dependabot rebase.

---

Dependabot commands and options

You can trigger Dependabot actions by commenting on this PR:

• @dependabot rebase will rebase this PR
• @dependabot recreate will recreate this PR, overwriting any edits that have been made to it
• @dependabot show <dependency name> ignore conditions will show all of the ignore conditions of the specified dependency
• @dependabot ignore this major version will close this PR and stop Dependabot creating any more for this major version (unless you reopen the PR or upgrade to it yourself)
• @dependabot ignore this minor version will close this PR and stop Dependabot creating any more for this minor version (unless you reopen the PR or upgrade to it yourself)
• @dependabot ignore this dependency will close this PR and stop Dependabot creating any more for this dependency (unless you reopen the PR or upgrade to it yourself)

[dependabot]

Labels

The following labels could not be found: dependencies, rust, security. Please create them before Dependabot can add them to a pull request.

Please fix the above issues or remove invalid values from dependabot.yml.

[socket-security]

Review the following changes in direct dependencies. Learn more about Socket for GitHub.

Diff	Package	Supply Chain Security	Vulnerability	Quality	Maintenance	License
	cargo/​hax-lib@​0.3.7 ⏵ 0.4.0	+3		+4

View full report

[github-actions]

🔒 Security Validation Report

Generated: Mon Sep 14 10:01:17 UTC 2026

📊 Summary

• NIST compliance: success
• Cryptographic validation: success
• Constant-time operations: success
• Memory safety: success
• Dependency security: success
• WASM security: success

✅ Overall Security Status: PASSED

All critical security validations passed successfully.

🔍 Details

This report covers:

• NIST post-quantum algorithm compliance
• Constant-time operation verification
• Memory safety and zeroization checks
• Dependency vulnerability scanning
• WASM build artifact validation

📋 Next Steps

✅ Security validation passed. Code is ready for deployment.

---

✅ Security validation passed! This code meets all security requirements.

[github-actions]

🔍 Pull Request Summary

Generated: Mon Sep 14 10:29:23 UTC 2026

📋 Validation Results

• Core Validation: success
• Security Validation: success
• Test Coverage: success
• WASM Compatibility: success
• Documentation: success

✅ Overall Status: PASSED

🔒 Security Checklist

• No classical cryptographic algorithms
• Only SHA-3 family hash functions
• Constant-time operations
• Proper memory zeroization
• Input validation
• Error handling

📝 Review Notes

Please review the security implications of this change carefully.
All cryptographic changes require security team review.

---

✅ Automated validation passed! This PR is ready for review.