module arch.system.state.resource_machine.notes.nockma_runnable;
import prelude open;
import arch.system.state.resource_machine.notes.nockma open;
import arch.system.state.resource_machine.notes.runnable open;
type NockmaProgramState :=
mk@{
current_noun : Noun;
storage : Storage Nat Noun;
gas_limit : Nat;
};
instance
nockmaRunnable : Runnable Nat Nat Noun NockmaProgramState :=
Runnable.mkRunnable@{
executeStep :=
\{executable state input :=
let
input_noun :=
Noun.Cell (Noun.Atom (fst input)) (Noun.Atom (snd input));
subject :=
Noun.Cell (NockmaProgramState.current_noun state) input_noun;
full_input := Noun.Cell subject executable;
result :=
GasState.runGasState
(nock (NockmaProgramState.storage state) full_input)
(NockmaProgramState.gas_limit state);
in case result of
| error err := error err
| ok (mkPair result_noun remaining_gas) :=
case result_noun of
| Noun.Cell (Noun.Atom new_state) requests :=
let
parseRequest
(req : Noun) : Option (Either Nat (Pair Nat Nat)) :=
case req of
| Noun.Atom key := some (left key)
| Noun.Cell (Noun.Atom key) (Noun.Atom value) :=
some (right (mkPair key value))
| _ := none;
terminating
parseRequests
(reqs : Noun) : List (Either Nat (Pair Nat Nat)) :=
case reqs of
| Noun.Atom zero := nil
| Noun.Cell (Noun.Atom req) rest :=
case parseRequest (Noun.Atom req) of {
| none := parseRequests rest
| some parsed := parsed :: parseRequests rest
}
| _ := nil;
parsed_requests := parseRequests requests;
new_state :=
state@NockmaProgramState{
current_noun := Noun.Atom new_state;
gas_limit := remaining_gas;
};
in ok (mkPair new_state parsed_requests)
| _ := error "Invalid result format"};
halted :=
\{state :=
NockmaProgramState.gas_limit
state
== zero
|| case NockmaProgramState.current_noun state of {
| Noun.Atom n := n == 1702390132
| _ := false
}};
startingState :=
NockmaProgramState.mk@{
current_noun := Noun.Atom zero;
storage := emptyStorage;
gas_limit := 1000;
};
};