Salt v1.2.0 — Cross-function chaining, struct field bounds, stdlib bundling

Salt v1.2.0

New Verification Features

• Cross-function contract chaining: callee ensures postconditions flow into the caller's Z3 solver, enabling compositional verification
• Struct field type bounds: field accesses in contracts receive type-domain constraints (u8→[0,255], etc.)
• Nested body scanner: array store detection recurses into function calls and binary ops
• While-loop && auto-inference: invariant inference handles conjunctions
• Expr::Let defensive handling: prevents silent catch-all failures in contract translation

Distribution

• Crate renamed to saltc: cargo install saltc now works
• Stdlib bundled into binary: saltc works without std/ on disk
• Release tarball attached for macOS ARM64

Documentation

• Consolidated verification docs into single canonical reference (z3-contracts.md)
• Updated blog posts with v1.2.0 features
• SPEC.md: grammar consistency fixes, table of contents
• 39 Z3 contract regression tests with evidence lines

Fixes

• Two correctness bugs found and fixed in red-team review (param symbol tracking, field axioms cache)

See VERIFICATION_CAPABILITIES.md → z3-contracts.md for the full capability reference.