…record, extension_env, and constraints

…g in terms of AbstractInstruction

* cleaned compiler warnings; ported ADD instruction

* formatting

Co-authored-by: Tannr <tannr@hey.com>

* more concrete instructions; removed prev val from mem op

Made return type for AbstractInstruction abstract.

Because instructions can now return different types, the `InnerInterpreter` trait constrains the set of possible return types from individual instructions.
All existing instructions still return `AbstractExecRecord`. All existing instructions are concrete so they return `ConcreteAbstractExecRecord` which has its constraint type parameter set to the unit type. This allows concrete instructions to not have any generic type for constraints while still using the same `AbstractExecRecord` return type.

Separated AbstractMachine into AbstractMachine, InnerInterpreter, and OuterInterpreter.

AbstractMachine - purely encapsulates the current state of the machine. It does not include constraints as concrete machines do not have constraints.

InnerInterpreter - handles the return value and state update from execution of an individual instruction. We have two example inner interpreters. The concrete inner interpreter maps simply updates the current machine state. The symbolic inner interpreter returns a vec of new machine states and constraints.

OuterInterpreter - handles orchestration of which machine state(s) to run. For the example outer interpreters we implement, we embed the inner interpreter in the outer interpreter struct as a trait object. This allows for some flexibility in choosing different inner interpreters so long as they have a  step function of the right type for the outer interpreter. The concrete outer interpreter just steps the concrete inner interpreter until the machine can’t execute any further. The symbolic outer interpreter performs DFS on the search graph of machine states. Note that this architecture allows us to substitute out an alternative symbolic outer interpreter that performs BFS or any other alternative search strategy.

I temporarily removed the `PathSummary` portion yet where we use the solver to find the reachable paths and return models. The type signature of `ConcreteOuterInterpreter` is already incredibly complex and I'd prefer to not add the additional generics that the solver is going to entail in a separate PR.

…ast;

* remove generic from stack

…ilitate custom types support

* remove memory generic

* lint