…/bedrock2 into regalloc-metrics

…ntics not updated yet

…/bedrock2 into regalloc-metrics

…ec to fix build error

…etrics

Conflicts:
	compiler/src/compiler/FlatImp.v
	compiler/src/compiler/FlatToRiscvMetric.v
	compiler/src/compiler/FlattenExpr.v
	compiler/src/compiler/RegAlloc.v
	compiler/src/compiler/Spilling.v

side effects:
- breaks useimmediate
- fixes spilling

it seems i am trying to do too many things at once so i am committing
the shared things so that i do not have to worry about missing
dependencies due to commit order

The spilling phase adds some boilerplate inside functions and around
function calls, so we need to account for it by making things
artificially more expensive before the spilling phase.

In an effort to avoid monolithic commits, this is a partial commit, so
the code definitely doesn't compile in the current state since lots of
things changed as a side effect.

There are a few comments that say "cost_something constraint:", which
document the various constraints on the magic numbers chosen as upper
bounds for the costs (100, 95, 50). These should probably change to
better numbers at some point.

The pipeline now knows that metrics are preserved throughout.

Many further changes are needed in RegAlloc.v and UseImmediate.v, so
changes to theorems in those files are not included in this commit (and
it will therefore not compile by itself as a result).

This is now 2/5 compiler stages fully verified with metrics.

It's nicer to work with this way, since all the exec judgments have the
same starting metrics then.

Largely rewritten from scratch except for the SSeq part. There are now
3/5 compiler phases fully verified with metrics!

A new compiler stage dead code elimination was added. There were minor
changes in the stage itself due to other updates, and the compiler stage
was commented because the proof is not yet metrics-aware.

Also introduce MetricTactics, which I expect will be very useful
elsewhere.

I now realize why the rest of the codebase uses this style; it's just
easier to work with as a user.

This seemed too easy, so I'm suspicious something's wrong, but
everything seems to work. The definition of riscv_call now incurs a
penalty equal to cost_SCall_L. I don't fully understand why, but
presumably there's some boilerplate added somewhere.

Only one file left with admits! (FlattenExpr)

Also update bedrock2 semantics for new metrics, which fixes
FlattenExpr.v. All the other pipeline stages are now broken and need to
be patched.

it's messy and can use improvements

the compiler has zero admits :D

fix MetricWeakestPrecondition and ...Properties

This reverts commit 44380e0.

This reverts commit b389899.

This reverts commit e5ba50c.

metriclit and most of s should go somewhere else eventually

to be restored later