#272 Adds Frama-C WP proofs

Summary by cubic

Adds Frama-C WP proofs gated in CI for ELF parsing, GDB RSP hex/checksum, and guest address math, and switches ELF relocation to a checked elf_window_t window. Tightens safety checks across exec, GDB, guest memory, and FUSE, and hardens the Infer workflow.

• New Features

  • CI verify runs Frama-C on ELF, RSP, and GVA math; proofs gate merges with a pinned toolchain; scripts/check-wp-result.py and scripts/check-acsl-coverage.py enforce success and coverage; proof timeout set to 120s.
  • Extracted guest address arithmetic to src/core/gva-math.h and proved it; relocation uses elf_window_t (va_base/target_base); tightened ELF helpers and added ELF_PHDR_TABLE_MAX; AT_PHDR derived from the covering PT_LOAD and guarded by phdr_valid.
  • Suppress Infer PULSE_UNINITIALIZED_VALUE in .inferconfig; add make infer-uninit to re-run with the check enabled and report the count.

• Bug Fixes

  • ELF: validate PHDR geometry at both parse sites; reject wrapping/extreme extents early; avoid misaligned reads; stop re-parsing files; ignore zero-memsz segments; compute AT_PHDR correctly; zero-initialize PHDR scratch; bound interpreter and executable extents before the point of no return.
  • GDB RSP: bound reads to NUL; require enough hex digits; validate checksum nibbles; handle empty H; require bufsz >= 2; return an error on malformed vCont.
  • Guest memory: clamp available bytes to the end of the primary buffer; require full 4 KiB page tables before indexing.
  • FUSE: clamp read replies to the requested size; added an over-reply test.
  • Infer: fix make infer-uninit to create the build dir, honor Infer exit status (treat exit 2 as expected), and fail on an empty/missing report.