feat: Switch to using bv_decide to decide memory goals instead of bv_omega

[bollu]

Description:

In facing scaling issues with omega, we've taken a step back, and are considering using a SAT solver via bv_omega to discharge our memory goals. This branch will try an experiment, where we will replace the core definitions of mem_legal', mem_subset', mem_separate' to be SAT solver friendly, and will rewrite the surrounding tactics to use these theorems instead.

Testing:

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

License:

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

[bollu]

  -- @bollu: we need 'hSHA2_k512_length' to allow omega to reason about
  -- SHA2.k_512.length, which is otherwise treated as an unintepreted constant.
  have hSHA2_k512_length : SHA2.k_512.length = 80 := rfl
  -- rw [hSHA2_k512_length] at h_s1_ktbl -- motive is not type-correct:(
  -- TODO: discuss with @shigoel.
  -- We need SMT to reason about what `length = 80` means inside the solver.
  -- Alternatively, we write a preprocessor that uses such information
  -- to massage the proof state.
  try simp_mem -- It should fail if it makes no progress. Also, make small examples that demonstrate such failures.
  sorry