Add Kani harness for address arithmetic in mem-core #16

Context: Kani does bounded model checking. Address arithmetic (overflow, alignment) in PhysicalAddress / VirtualAddress is a high-value target — bugs here are kernel exploits.

Scope:

• Add #[cfg(kani)] harnesses in lib/mem-core/src/ covering: add/sub with overflow, alignment rounding, range-containment.
• Add CI job kani that runs cargo kani on host.
• Document the harness pattern in CONTRIBUTING.md for others to copy.

Acceptance: kani CI job runs and passes.