feat: Add fine grained control over mem_omega rewriting [7/?]

[bollu]

Description:

We increase the ITPness of simp_mem by making it less of a proof hammer, and more of a user-controllable rewrite engine. Description of the new design follows:

---

The simp_mem tactic allows simplifying expressions of the form Memory.read_bytes rbase rn (mem').
simp_mem attempts to discover the result of the expression by various heuristics,
which can be controlled by the end user:

• (a) If mem' = Memory.write_bytes wbase wn mem and we know that (rbase, rn) ⟂ (wbase, wn), then we simplify to mem.read (rbase, rn).
• (b) If mem' = Memory.write_bytes wbase wn wval mem and we kow that (rbase, rn) ⊆ (wbase, wn), then we simplify to wval.extract (rbase, rn) (wbase, wn).
• (c) If we have a hypothesis hr' : mem'.read_bytes rbase' rn' = rval, and we know that (rbase, rn) ⊆ (rbase', rn'), then we simplify to rval.extract (rbase, rn) (rbase', rn').

These simplifications are performed by reducing the problem to a problem that can be solved by a decision procedure (omega) to establish
which hypotheses are at play. simp_mem can be controlled along multiple axes:

1. The hypotheses that simp_mem will pass along to the decision procedure to discover overlapping reads (like hr'),
   and hypotheses to establish memory (non-)interference, such as (rbase, rn) ⟂ (wbase, wn).

• simp_mem using []: try to perform the rewrite using no hypotheses.
• simp_mem using [h₁, h₂]: try to perform the rewrite using h₁, h₂, as hypotheses.

2. The kind of rewrite that simp_mem should apply. By default, it explores all possible choices, which might be expensive due to repeated calls to the decision
   procedure. The user can describe which of (a), (b), (c) above happen:

   • simp_mem ⟂ : Only simplify when read is disjoint from write.
   • simp_mem ⊂w : Only simplify when read overlaps the write.
   • simp_mem ⊂r hr : Simplify when read overlaps with a known read hr : mem.read_bytes baseaddr' n' = val.
     This is useful for static information such as lookup tables that are at a fixed location and never modified.
   • simp_mem ⊂r : Simplify when read overlaps with known read from hypothesis list.

3. The targets where the rewrite must be applied. (This needs some thought: does this even make sense?)

   • simp_mem at ⊢
   • simp_mem at h₁, h₂, ⊢

---

• add simp_mem using []
• add simp_mem ⟂/⊂w/⊂r hr/⊂r

Stacked on top of #237

@shilgoel the branch shows appreciable speedups, by controlling the lemmas we pass to mem_omega: In total, it goes from 34s to 13s

Batch mode use, measured by lake build :

* before: `lake build Proofs.Experiments.Memcpy.MemCpyVCG 33.39s user 0.89s system 99% cpu 34.512 total`
* after: `lake build Proofs.Experiments.Memcpy.MemCpyVCG 12.33s user 0.56s system 97% cpu 13.206 total`

Individual breakdown during Interactive use, measured by #time

MemCpyVCG:

• theorem Memcpy.extracted_2 (s0 si : ArmState) : ~ 11 seconds to 1.6 seconds(:tada: !)
  • before mem_omega filtering: 11214 ms .
  • after mem_omega filtering: 1576 ms.
• theorem Memcpy.extracted_0 : ~ 12 seconds to 3.2 seconds
  • before mem_omega filtering: 12023 ms
  • after mem_omega filtering: 3128ms
• theorem partial_correctness : 7.6 s to 6.6 seconds
  • before mem_omega filtering: 7598
  • after mem_omega filtering: 6580ms (this only has a single call to mem_omega)

I feel that this, plus if we get the instantiateMVars fix, will help quite a bit with scaling 🙂

Testing:

What tests have been run? Did make all succeed for your changes? Was
conformance testing successful on an Aarch64 machine?

No semantics were changed, conformance succeeds.

License:

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