feat: add automation support for pairwise memory separation

[bollu]

This is stacked on top of #123 , since we want to state this, for a given ms : List MemoryRegion, ms.pairwise MemoryRegion.Separate. This, of course, needs us to have the MemoryRegion abstraction in the first place.

[shigoel]

@bollu Conflicts here.

[bollu]

@shigoel conflicts addressed!

[shigoel]

Left some comments, looks good in general.

We need more tests for the new pairwise construct (in a PR in the very near future is okay!) -- let's start with changing theorems in the SHA512 example to use pairwise, and then we'll go from there?

[bollu]

@shigoel all comments addressed.

[shigoel]

@bollu I see that a couple comments weren't addressed. Tagged you there.

[bollu]

@shigoel All comments (hopefully) addressed.

[shigoel]

Suggested change

	let mut simpTheorems : Array SimpTheorems := #[]
	for a in #[`minimal_theory, `bitvec_rules] do
	let some ext ← (getSimpExtension? a)
	| throwError m!"[simp_mem] Internal error: simp attribute {a} not found!"
	simpTheorems := simpTheorems.push (← ext.getTheorems)
	-- unfold `state_value.
	simpTheorems := simpTheorems.push <| ← ({} : SimpTheorems).addDeclToUnfold `state_value
	let simpCtx : Simp.Context := {
	simpTheorems,
	config := { decide := true, failIfUnchanged := false },
	congrTheorems := (← Meta.getSimpCongrTheorems)
	}
	LNSymSimpContext
	(config := { decide := false, failIfUnchanged := false })
	(simp_attrs := #[`minimal_theory, `bitvec_rules])
	(decls_to_unfold := #[state_value])

@bollu I believe LNSymSimpContext can work here. Fair warning: haven't tried out the suggestion, excuse typos, etc.

[shigoel]

Also, open to making LNSymSimpContext nicer (separate issue).

[bollu]

@shigoel I think I would prefer to keep it as-is, because it's hard to see what LNSymSimpContext builds unless one goes and reads its code. Since this code is meant to be performant, I would rather have the building of the simp-set inline, so it's easy to audit.

[shigoel]

Weren't you using LNSymSimpContext before though?
dd24b6d

Not a big deal, but I want to make sure I understand what the reasons are.

[bollu]

Indeed, I was reusing LNSymSimpContext to make sure that if LNSymSimpContext got more powerful, I would get the same power for free :) But thinking this through, I found your argument for why this should not be expensive to be compelling. Therefore, I'd prefer to build a custom simp-set that's tuned down, and to add power to it as necessary.

From an engineering perspective, I'm advocating for [WET / write everything twice] (https://en.wikipedia.org/wiki/Rule_of_three_(computer_programming)) instead of DRY. 😉

[shigoel]

Gotcha, though I would note that the particular invocation of LNSymSimpContext is equivalent to what you wrote inline.

[bollu]

@shigoel happy to have this merged, as I prefer keeping the current around to build the SimpContext around.