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;

Nockma Runnable Implementation¶

This module implements the Runnable trait for Nockma, allowing it to be used as an executor in the Anoma system.

Types¶

type NockmaProgramState :=
  mk@{
    current_noun : Noun;
    storage : Storage Nat Noun;
    gas_limit : Nat;
  };

Runnable Instance¶

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;
      };
  };

This implementation:

1. Defines a NockmaProgramState type that tracks:

   • The current Noun being evaluated
   • The storage interface for reading/writing Nouns
   • The remaining gas limit

2. Implements executeStep to:

   • Convert input key-value pair to a Noun (using direct Noun.Atom construction since KVSDatum is Nat)
   • Construct the Nock subject: [state [key val]]
   • Construct the full input for Nock evaluation: [subject formula]
   • Run one step of Nockma evaluation
   • Parse the result which should be of the form (Noun.Atom new_state output_requests)
   • Parse the output_requests which is a linked list of requests
   • Each request is either:
     • (Noun.Atom key) for read requests
     • (Noun.Atom key value) for write requests
   • Update program state with new state and remaining gas
   • Return new state and parsed requests

3. Implements halted to check if program has run out of gas or is in designated halting state

4. Provides startingState with initial values