diff options
Diffstat (limited to 'src/lem_interp/interp_interface.lem')
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index 40c34480..84e28470 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -95,6 +95,16 @@ type i_state_or_error = (*Function to decode an instruction and build the state to run it*) val decode_to_istate : context -> value -> i_state_or_error +(* Augment an address by the given value *) +val add_to_address : value -> nat -> value + +(* Slice a value into a smaller vector, starting at first number and going to second according to order + For bytevectors, assumes you are slicing at the byte level, not the bit level *) +val slice_value : value -> nat -> nat -> value + +(*append two vectors (bit x byte -> bit) *) +val append_value : value -> value -> value + (* Big step of the interpreter, to the next request for an external action *) (* When interp_mode has eager_eval false, interpreter is (close to) small step *) val interp : interp_mode -> instruction_state -> outcome |