Inject extern spec of std functions

[coord-e]

No description provided.

[Copilot]

Pull request overview

This PR introduces automatic injection of extern specifications for standard library functions in Thrust, a verification tool for Rust. Instead of hardcoding specifications for specific functions like Box::new and std::mem::swap, the PR adds a comprehensive std.rs file containing specifications for common std library functions (Option, Result, Box, mem operations, and i32 methods) that gets automatically injected into the user's code during compilation.

Key changes:

• New std.rs file with extern specifications for Option, Result, Box, mem, and i32 methods
• Code injection mechanism in main.rs to parse and inject std.rs into the AST
• Type parameter substitution infrastructure in rty.rs to handle generic specifications correctly

Reviewed changes

Copilot reviewed 8 out of 8 changed files in this pull request and generated 7 comments.

Show a summary per file

File	Description
std.rs	New file containing extern specifications for standard library functions (Option, Result, Box, mem, i32)
src/main.rs	Adds after_crate_root_parsing callback to inject std.rs into the parsed AST
src/rty.rs	Implements type parameter substitution in sorts, formulas, terms, and atoms to support generic extern specs
src/analyze/basic_block.rs	Removes hardcoded handling of Box::new and mem::swap, now handled via injected specs
src/refine/template.rs	Adjusts template building logic for parameter refinements
src/analyze/local_def.rs	Filters extern spec target extraction to only Fn and AssocFn def kinds
src/analyze.rs	Inlines datatype symbol name construction for enum variants
src/chc.rs	Adds args_mut() accessor to DatatypeSort

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.