Validate isSafe trait invariants during parsing

[fallintoplace]

This tightens isSafe parsing so malformed trait invariants fail before codegen.

Root cause:
TraitAnnealBlock::parse_from_attrs only checked that an isSafe clause existed on unsafe traits. The validation loop was effectively a no-op, so forms like isSafe or other malformed headers could make it through parsing and only blow up later as Lean syntax junk.

What changed:

• reject multiple isSafe sections on a single trait
• require isSafe to be declared as isSafe : <Proposition> or isSafe := <Proposition>
• reject empty isSafe : / isSafe := declarations with no proposition
• update parser tests to cover the accepted forms and the new rejection cases

Impact:

• bad isSafe syntax now fails at parse time with a targeted error
• trait invariants have a narrower, explicit surface instead of silently accepting junk
• duplicate isSafe declarations stop before generation instead of producing ambiguous downstream behavior

Validation:

• cargo fmt --manifest-path /Users/hoangvu/Code/OSS/zerocopy/anneal/Cargo.toml --check
• cargo test --manifest-path /Users/hoangvu/Code/OSS/zerocopy/anneal/Cargo.toml parse::attr

[codecov-commenter]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 91.85%. Comparing base (ed09d09) to head (88c9bc7).

Additional details and impacted files

@@           Coverage Diff           @@
##             main    #3477   +/-   ##
=======================================
  Coverage   91.85%   91.85%           
=======================================
  Files          20       20           
  Lines        6093     6093           
=======================================
  Hits         5597     5597           
  Misses        496      496           

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.