Skeleton of SMT Language support

[lekko-jonathan]

Opening this so that people can look at it in case people are interested.

There are systems out there that symbolically prove series of math statements. I've been playing around with cvc5, which supports a number of languages. If we were actually shipping things, their built in language might be better, since it has a few more data structures, but I initially targeted SMT2-LIB, since it runs on most solvers, like Microsoft's Z3.

I've been running it online at https://cvc5.github.io/

I've been manually putting in the header and footer like:

(set-logic ALL)
(set-option :produce-models true)

(declare-datatype OAuthDeviceConfig
  ((mkOAuthDeviceConfig 
    (VerificationUri String)
    (PollingIntervalSeconds Int)
  ))
)
(define-fun getDeviceOauth ((env String)) OAuthDeviceConfig
  (ite (= env "staging") (mkOAuthDeviceConfig "https://app-staging.lekko.com/login/device" 5) (ite (= env "development") (mkOAuthDeviceConfig "http://localhost:8080/login/device" 5) (mkOAuthDeviceConfig "https://app.lekko.com/login/device" 5)))
)
(assert (= (= (VerificationUri (getDeviceOauth "staging")) "https://app-staging.lekko.com/login/device") true))

(check-sat)
(get-model)

This PR isn't completely done. I took a lot of short cuts to get things running and vet the ideas that I had. There are a lot of things that aren't implemented.

The ideas I was exploring were:

• Can something like SMT provide a pleasant way to run validators?
• Is it easier to write a generator from a nice encoding instead of the proto encoding?
• Is it easier to go from the proto into the struct encoding than directly to strings?

To me, the answer of all three is YES.

Another thing that I started looking into was "would executing from the struct encoding be significantly faster than our proto walking approach?" - but I didn't bother going all the way there, so I think.. likely?

I think that this kind of points towards something Sergey was talking about a while ago, about the benefits of having an intermediary language that could do more things, that then compiled down into what was run in the SDK. I added things like numeric operators and validation, to start exploring that too.