Verify atomic types and intrinsic wrappers for Challenge 7

[jellllly420]

This proposes an independent solution to the required safety scope of Challenge 7. It verifies the pinned library's from_ptr methods and unsafe operation wrappers with VeriFast, without changing the runtime implementation in library/.

The proof package requires coverage of all 14 from_ptr bodies (including both 128-bit types and the extra pointer-sized types), all 15 current operation wrappers, and all 91 legal intrinsic ordering combinations. It supports conversion of initialized ordinary storage and reuse of existing atomic shares, preserves the boolean 0/1 invariant, and checks actual panic paths with atomic permissions retained on unwind. Concrete callers and rejection controls exercise ownership, initialization, operand domains, invariant closure, and ordering identity.

VeriFast is already an approved tool, but this solution needs an unreleased update to 26.01. The PR includes the explicit release-relative patch and a clean build from pinned archives, compiler, decoder revision, and Cargo locks. The update handles const-generic atomic orders, impl Self, repeated macro contracts, compiler-derived alignment, and the primitive contracts. These tool changes and trusted primitive semantics require review; this PR does not represent them as an accepted release.

The source generator checks digests of the current atomic implementation and intrinsic declarations. To check the complete module beside the compiler's core dependency, it changes duplicate rustc_diagnostic_item attributes to documentation attributes in both inputs. Whole-module refinement compares those prepared inputs. The source preparation, permission interpretation, and trusted boundary are documented in verifast-proofs/core/sync/atomic.rs/README.md.

Validation: a fresh native ARM64 macOS build passes the complete source proof, fourteen fresh/shared callers, three conversion rejection controls, eleven compiler/ownership controls, twenty-nine operation controls, four refinement controls, and twenty-five isolated malformed-MIR decoder controls. The new ARM macOS workflow enforces the 128-bit cases and uploads generated sources, per-function coverage, control results, and build evidence. Hosted CI is pending; this is initially a draft.

Optional panic-avoidance contracts for every public safe atomic method are not included. The proof does not claim general concurrent functional correctness or a hardware memory-model theorem.

Resolves #83.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

Generated by Codex on behalf of @jellllly420