module arch.system.state.resource_machine.notes.nockma;

import prelude open;
import Stdlib.Data.Nat open;
import Stdlib.Data.List open;
import Stdlib.Trait.Show open;

Nockma Implementation¶

Core Data Types¶

The fundamental data structures for Nockma implementation, including the Noun type that represents all data in Nock, along with equality and display instances.

type Noun :=
  | Atom : Nat -> Noun
  | Cell : Noun -> Noun -> Noun;

terminating
nounEq (n1 n2 : Noun) : Bool :=
  case mkPair n1 n2 of
    | mkPair (Noun.Atom x) (Noun.Atom y) := x == y
    | mkPair (Noun.Cell a b) (Noun.Cell c d) := nounEq a c && nounEq b d
    | _ := false;

instance
EqNoun : Eq Noun :=
  Eq.mk@{
    isEqual := nounEq;
  };

Pretty-printer for Noun¶

terminating
showNoun (n : Noun) : String :=
  case n of
    | Noun.Atom a := natToString a
    | Noun.Cell l r := "[" ++str showNoun l ++str " " ++str showNoun r ++str "]";

instance
ShowNoun : Show Noun :=
  Show.mk@{
    show := showNoun;
  };

Storage System and Operation Types¶

Storage abstraction for scrying operations and the enumeration of all Nock operations with their corresponding opcodes.

axiom convertToNoun : {val : Type} -> val -> Noun;

axiom convertFromNoun : {val : Type} -> Noun -> Option val;

type ScryOp :=
  | Direct
  | Index;

type Storage addr val :=
  mkStorage@{
    readDirect : addr -> Option val;
    readIndex : val -> Option val;
  };

emptyStorage {addr val : Type} : Storage addr val :=
  Storage.mkStorage@{
    readDirect := \{_ := none};
    readIndex := \{_ := none};
  };

axiom externalStorage : {addr val : Type} -> Storage addr val;

type NockOp :=
  | Slash
  | Constant
  | Apply
  | CellTest
  | Increment
  | EqualOp
  | IfThenElse
  | Compose
  | Extend
  | Invoke
  | Pound
  | Match
  | Scry;

opOr {A : Type} (n m : Option A) : Option A :=
  case n of
    | none := m
    | some n := some n;

parseOp (n : Nat) : Option NockOp :=
  let
    test :=
      \{m op :=
        case n == m of
          | true := some op
          | false := none};
  in foldr
    opOr
    none
    (zipWith
      test
      [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12]
      [
        NockOp.Slash;
        NockOp.Constant;
        NockOp.Apply;
        NockOp.CellTest;
        NockOp.Increment;
        NockOp.EqualOp;
        NockOp.IfThenElse;
        NockOp.Compose;
        NockOp.Extend;
        NockOp.Invoke;
        NockOp.Pound;
        NockOp.Match;
        NockOp.Scry;
      ]);

Gas State Monad¶

A monadic framework for tracking gas consumption and handling errors during Nock evaluation. This ensures computations can be bounded and failures can be properly handled.

type GasState A :=
  mk@{
    runGasState : Nat -> Result String (Pair A Nat);
  };

instance
GasStateMonad : Monad GasState :=
  Monad.mk@{
    applicative :=
      Applicative.mk@{
        functor :=
          Functor.mk@{
            map :=
              \{f s :=
                GasState.mk
                  \{gas :=
                    case GasState.runGasState s gas of
                      | ok (mkPair x remaining) := ok (mkPair (f x) remaining)
                      | error e := error e}};
          };
        pure := \{x := GasState.mk \{gas := ok (mkPair x gas)}};
        ap :=
          \{sf sa :=
            GasState.mk
              \{gas :=
                case GasState.runGasState sf gas of
                  | ok (mkPair f remaining) :=
                    case GasState.runGasState sa remaining of {
                      | ok (mkPair x final) := ok (mkPair (f x) final)
                      | error e := error e
                    }
                  | error e := error e}};
      };
    bind :=
      \{ma f :=
        GasState.mk
          \{gas :=
            case GasState.runGasState ma gas of
              | ok (mkPair a remaining) := GasState.runGasState (f a) remaining
              | error e := error e}};
  };

err {A : Type} (str : String) : GasState A := GasState.mk \{_ := error str};

Gas Management and Storage Operations¶

Functions for managing computational costs and implementing storage read operations (scrying) that allow Nock programs to interact with external data.

getGasCost (cost : NockOp) : Nat :=
  case cost of
    | NockOp.Slash := 1
    | NockOp.CellTest := 1
    | NockOp.Increment := 1
    | NockOp.EqualOp := 2
    | NockOp.IfThenElse := 3
    | NockOp.Compose := 2
    | NockOp.Extend := 2
    | NockOp.Invoke := 3
    | NockOp.Pound := 1
    | NockOp.Scry := 10
    | _ := 0;

consume (op : NockOp) : GasState Unit :=
  GasState.mk
    \{gas :=
      let
        cost := getGasCost op;
      in case cost > gas of
           | true := error "Out of gas"
           | false := ok (mkPair unit (sub gas cost))};

scry
  {val : Type}
  (stor : Storage Nat val)
  (op : ScryOp)
  (addr : Nat)
  : Result String Noun :=
  case op of
    | ScryOp.Direct :=
      case Storage.readDirect stor addr of {
        | some val := ok (convertToNoun val)
        | none := error "Direct storage read failed"
      }
    | ScryOp.Index :=
      case Storage.readDirect stor addr of
        | some indexFn :=
          case Storage.readIndex stor indexFn of {
            | some val := ok (convertToNoun val)
            | none := error "Index computation failed"
          }
        | none := error "Index function not found";

Helper Operations¶

Implementation of the fundamental slash (/) and pound (#) operations that provide tree navigation and editing capabilities respectively.

terminating
slash
  {val : Type}
  (stor : Storage Nat val)
  (n : Noun)
  (subject : Noun)
  : GasState Noun :=
  case n of
    | Noun.Atom x :=
      case x == 1 of {
        | true := pure subject
        | false :=
          case x == 2 of {
            | true :=
              case subject of {
                | Noun.Cell a _ := pure a
                | _ :=
                  err
                    ("Cannot take slash (/2) of atom: " ++str showNoun subject)
              }
            | false :=
              case x == 3 of {
                | true :=
                  case subject of {
                    | Noun.Cell _ b := pure b
                    | _ :=
                      err
                        ("Cannot take slash (/3) of atom: "
                          ++str showNoun subject)
                  }
                | false :=
                  case mod x 2 == 0 of {
                    | true :=
                      consume NockOp.Slash
                        >>= \{_ :=
                          slash stor (Noun.Atom (div x 2)) subject
                            >>= \{res :=
                              consume NockOp.Slash
                                >>= \{_ := slash stor (Noun.Atom 2) res}}}
                    | false :=
                      consume NockOp.Slash
                        >>= \{_ :=
                          slash stor (Noun.Atom (div x 2)) subject
                            >>= \{res :=
                              consume NockOp.Slash
                                >>= \{_ := slash stor (Noun.Atom 3) res}}}
                  }
              }
          }
      }
    | _ := err ("Slash axis must be atom, got: " ++str showNoun n);

terminating
pound
  {val : Type}
  (stor : Storage Nat val)
  (n : Noun)
  (b : Noun)
  (c : Noun)
  : GasState Noun :=
  case n of
    | Noun.Atom x :=
      case x == 1 of {
        | true := pure b
        | false :=
          case mod x 2 == 0 of {
            | true :=
              case c of {
                | Noun.Cell _ _ :=
                  consume NockOp.Slash
                    >>= \{_ :=
                      slash stor (Noun.Atom (2 * div x 2 + 1)) c
                        >>= \{slashResult :=
                          consume NockOp.Pound
                            >>= \{_ :=
                              pound
                                stor
                                (Noun.Atom (div x 2))
                                (Noun.Cell b slashResult)
                                c}}}
                | _ :=
                  err ("Invalid pound target (must be cell): " ++str showNoun c)
              }
            | false :=
              case c of {
                | Noun.Cell _ _ :=
                  consume NockOp.Slash
                    >>= \{_ :=
                      slash stor (Noun.Atom (2 * div x 2)) c
                        >>= \{slashResult :=
                          consume NockOp.Pound
                            >>= \{_ :=
                              pound
                                stor
                                (Noun.Atom (div x 2))
                                (Noun.Cell slashResult b)
                                c}}}
                | _ :=
                  err ("Invalid pound target (must be cell): " ++str showNoun c)
              }
          }
      }
    | _ := err ("Pound axis must be atom, got: " ++str showNoun n);

Operation Evaluator¶

The main dispatcher that handles evaluation of each Nock operation according to the Nock specification. Each case implements one of the 13 fundamental Nock operations.

terminating
evalOp
  {val : Type}
  (stor : Storage Nat val)
  (op : NockOp)
  (a : Noun)
  (args : Noun)
  : GasState Noun :=
  case op of
    | NockOp.Slash := slash stor args a
    | NockOp.Constant := pure args
    | NockOp.Apply :=
      case args of {
        | Noun.Cell b c :=
          nock stor (Noun.Cell a b)
            >>= \{r1 :=
              nock stor (Noun.Cell a c)
                >>= \{r2 := nock stor (Noun.Cell r1 r2)}}
        | _ :=
          err ("Invalid apply (2) args (must be cell): " ++str showNoun args)
      }
    | NockOp.CellTest :=
      case args of {
        | Noun.Cell b _ :=
          nock stor (Noun.Cell a b)
            >>= \{res :=
              case res of
                | Noun.Cell _ _ := pure (Noun.Atom 0)
                | _ := pure (Noun.Atom 1)}
        | _ :=
          err
            ("Invalid cell test (3) args (must be cell): " ++str showNoun args)
      }
    | NockOp.Increment :=
      nock stor (Noun.Cell a args)
        >>= \{res :=
          case res of
            | Noun.Atom n := pure (Noun.Atom (suc n))
            | x :=
              err ("Increment (4) target must be atom, got: " ++str showNoun x)}
    | NockOp.EqualOp :=
      case args of {
        | Noun.Cell b c :=
          nock stor (Noun.Cell a b)
            >>= \{r1 :=
              nock stor (Noun.Cell a c)
                >>= \{r2 :=
                  pure
                    (Noun.Atom
                      case nounEq r1 r2 of {
                        | true := 0
                        | false := 1
                      })}}
        | _ :=
          err ("Invalid equality (5) args (must be cell): " ++str showNoun args)
      }
    | NockOp.IfThenElse :=
      case args of {
        | Noun.Cell b (Noun.Cell c d) :=
          nock
              stor
              (Noun.Cell
                a
                (Noun.Cell (Noun.Atom 4) (Noun.Cell (Noun.Atom 4) b)))
            >>= \{r1 :=
              nock
                  stor
                  (Noun.Cell
                    (Noun.Cell (Noun.Atom 2) (Noun.Atom 3))
                    (Noun.Cell (Noun.Atom 0) r1))
                >>= \{r2 :=
                  nock
                      stor
                      (Noun.Cell (Noun.Cell c d) (Noun.Cell (Noun.Atom 0) r2))
                    >>= \{r3 := nock stor (Noun.Cell a r3)}}}
        | _ :=
          err
            ("Invalid if-then-else (6) args (must be [b [c d]]): "
              ++str showNoun args)
      }
    | NockOp.Compose :=
      case args of {
        | Noun.Cell b c :=
          nock stor (Noun.Cell a b) >>= \{r := nock stor (Noun.Cell r c)}
        | _ :=
          err ("Invalid compose (7) args (must be cell): " ++str showNoun args)
      }
    | NockOp.Extend :=
      case args of {
        | Noun.Cell b c :=
          nock stor (Noun.Cell a b)
            >>= \{r := nock stor (Noun.Cell (Noun.Cell r a) c)}
        | _ :=
          err ("Invalid extend (8) args (must be cell): " ++str showNoun args)
      }
    | NockOp.Invoke :=
      case args of {
        | Noun.Cell b c :=
          nock stor (Noun.Cell a c)
            >>= \{core :=
              let
                formula :=
                  Noun.Cell
                    (Noun.Atom 2)
                    (Noun.Cell
                      (Noun.Cell (Noun.Atom 0) (Noun.Atom 1))
                      (Noun.Cell (Noun.Atom 0) b));
              in nock stor (Noun.Cell core formula)}
        | _ :=
          err ("Invalid invoke (9) args (must be cell): " ++str showNoun args)
      }
    | NockOp.Pound :=
      case args of {
        | Noun.Cell (Noun.Cell b c) d :=
          nock stor (Noun.Cell a c)
            >>= \{r1 :=
              nock stor (Noun.Cell a d) >>= \{r2 := pound stor b r1 r2}}
        | _ :=
          err
            ("Invalid pound (10) args (must be [[b c] d]): "
              ++str showNoun args)
      }
    | NockOp.Match :=
      case args of {
        | Noun.Cell (Noun.Cell b c) d :=
          nock stor (Noun.Cell a c)
            >>= \{r1 :=
              nock stor (Noun.Cell a d)
                >>= \{r2 :=
                  nock
                    stor
                    (Noun.Cell
                      (Noun.Cell r1 r2)
                      (Noun.Cell (Noun.Atom 0) (Noun.Atom 3)))}}
        | Noun.Cell b c := nock stor (Noun.Cell a c)
        | _ :=
          err ("Invalid match (11) args (must be cell): " ++str showNoun args)
      }
    | Scry :=
      case args of
        | Noun.Cell b (Noun.Cell c d) :=
          nock stor b
            >>= \{opcode :=
              case opcode of
                | Noun.Atom opval :=
                  nock stor c
                    >>= \{addr :=
                      case addr of
                        | Noun.Atom addrVal :=
                          let
                            scryType :=
                              case opval == 0 of
                                | true := ScryOp.Direct
                                | false := ScryOp.Index;
                          in GasState.mk
                            \{gas :=
                              scry stor scryType addrVal
                                >>= \{scryResult :=
                                  GasState.runGasState
                                    (nock
                                      stor
                                      (Noun.Cell a (Noun.Cell scryResult d)))
                                    gas}}
                        | _ :=
                          err
                            ("Scry address must be atom, got: "
                              ++str showNoun addr)}
                | _ :=
                  err ("Scry type must be atom, got: " ++str showNoun opcode)}
        | _ :=
          err
            ("Invalid scry (12) args (must be [b [c d]]): " ++str showNoun args);

Core Nockma Evaluator¶

The main entry point for Nock evaluation. This function handles the parsing of Nock expressions and dispatches to the appropriate operation evaluators.

terminating
nock {val : Type} (stor : Storage Nat val) (input : Noun) : GasState Noun :=
  case input of
    | Noun.Atom n :=
      err ("Cannot evaluate atom as program: " ++str showNoun (Noun.Atom n))
    | Noun.Cell a b :=
      case b of
        | Noun.Cell first rest :=
          case first of {
            | Noun.Cell b c :=
              nock stor (Noun.Cell a (Noun.Cell b c))
                >>= \{r1 :=
                  nock stor (Noun.Cell a rest)
                    >>= \{r2 := pure (Noun.Cell r1 r2)}}
            | Noun.Atom n :=
              case parseOp n of {
                | some opcode :=
                  consume opcode >>= \{_ := evalOp stor opcode a rest}
                | none :=
                  err
                    ("Invalid operation code: "
                      ++str natToString n
                      ++str " in formula: "
                      ++str showNoun b)
              }
          }
        | Noun.Atom bn :=
          err
            ("Formula cannot be an atom: "
              ++str showNoun (Noun.Atom bn)
              ++str " in input: "
              ++str showNoun input);