sir: allocator policy parameter

[Eduardogbg]

mallocUninit picks its allocation nondeterministically, and the semantics now carries a Generic.MemoryPolicy that says which choices are permitted.

What changed

• SmallStep, Steps, EvalFn, the Runs* family and the observation predicates each take the policy explicitly; the hard-wired sirMemoryPolicy is deleted. Operation.Admissible intersects policy.Allows with validity and the size match, so a policy can narrow what an allocation step may return, never widen it.
• Two policies ship. permissive is the previously hard-wired behaviour verbatim, and permissive_not_deterministic exhibits two allocations it permits at one state. bump puts the allocation at the watermark and rejects requests past the address space: bump_deterministic, bump_sound, bump_satisfiable.
• The determinism side condition is Program.AllocationDeterministic policy = policy.Deterministic ∨ program.AllocationFree. AllocationFree is MemOracleFree renamed, so .inr at permissive recovers every previous statement; .inl bump_deterministic gives determinism under bump for programs that allocate, which zeroSizeStore_deterministic_bump uses. zeroSizeStore_not_deterministic separates the same program under permissive.
• progress_reachable_nonIcall_of_satisfiable derives the allocation obligation from policy.Sound and policy.Satisfiable, and the bump progress theorem is its instantiation. initializedLoad_deterministic proves a program deterministic under permissive through a reachability invariant that absorbs the allocator choice, with neither disjunct available.

[Eduardogbg]

superseded by #26