Juvix imports
module arch.system.state.resource_machine.notes.function_formats.nockma;
import prelude open;
import Stdlib.Data.Nat open;
import Stdlib.Data.List open;
import arch.system.state.resource_machine.notes.function_formats.transactionfunction open;
Nockma ImplementationΒΆ
type Noun :=
| Atom : Nat -> Noun
| Cell : Noun -> Noun -> Noun;
terminating
nounEq (n1 n2 : Noun) : Bool :=
case mkPair n1 n2 of
| mkPair (Atom x) (Atom y) := x == y
| mkPair (Cell a b) (Cell c d) := nounEq a c && nounEq b d
| _ := false;
instance
EqNoun : Eq Noun :=
mkEq@{
eq := nounEq;
};
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;
};
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]
[
Slash;
Constant;
Apply;
CellTest;
Increment;
EqualOp;
IfThenElse;
Compose;
Extend;
Invoke;
Pound;
Match;
Scry;
]);
type GasState A :=
mkGasState@{
runGasState : Nat -> Result String (Pair A Nat);
};
instance
GasStateMonad : Monad GasState :=
mkMonad@{
applicative :=
mkApplicative@{
functor :=
mkFunctor@{
map :=
\{f s :=
mkGasState
\{gas :=
case GasState.runGasState s gas of
| ok (mkPair x remaining) := ok (mkPair (f x) remaining)
| error e := error e}};
};
pure := \{x := mkGasState \{gas := ok (mkPair x gas)}};
ap :=
\{sf sa :=
mkGasState
\{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 :=
mkGasState
\{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 := mkGasState \{_ := error str};
getGasCost (cost : NockOp) : Nat :=
case cost of
| Slash := 1
| CellTest := 1
| Increment := 1
| EqualOp := 2
| IfThenElse := 3
| Compose := 2
| Extend := 2
| Invoke := 3
| Pound := 1
| Scry := 10
| _ := 0;
consume (op : NockOp) : GasState Unit :=
mkGasState
\{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
| Direct :=
case Storage.readDirect stor addr of {
| some val := ok (convertToNoun val)
| none := error "Direct storage read failed"
}
| 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";
terminating
slash
{val : Type}
(stor : Storage Nat val)
(n : Noun)
(subject : Noun)
: GasState Noun :=
case n of
| Atom x :=
case x == 1 of {
| true := pure subject
| false :=
case x == 2 of {
| true :=
case subject of {
| Cell a _ := pure a
| _ := err "Cannot take slash of atom"
}
| false :=
case x == 3 of {
| true :=
case subject of {
| Cell _ b := pure b
| _ := err "Cannot take slash of atom"
}
| false :=
case mod x 2 == 0 of {
| true :=
consume Slash
>>= \{_ :=
slash stor (Atom (div x 2)) subject
>>= \{res :=
consume Slash
>>= \{_ := slash stor (Atom 2) res}}}
| false :=
consume Slash
>>= \{_ :=
slash stor (Atom (div x 2)) subject
>>= \{res :=
consume Slash
>>= \{_ := slash stor (Atom 3) res}}}
}
}
}
}
| _ := err "Slash must be atom";
terminating
pound
{val : Type}
(stor : Storage Nat val)
(n : Noun)
(b : Noun)
(c : Noun)
: GasState Noun :=
case n of
| Atom x :=
case x == 1 of {
| true := pure b
| false :=
case mod x 2 == 0 of {
| true :=
case c of {
| Cell _ _ :=
consume Slash
>>= \{_ :=
slash stor (Atom (2 * div x 2 + 1)) c
>>= \{slashResult :=
consume Pound
>>= \{_ :=
pound
stor
(Atom (div x 2))
(Cell b slashResult)
c}}}
| _ := err "Invalid pound target"
}
| false :=
case c of {
| Cell _ _ :=
consume Slash
>>= \{_ :=
slash stor (Atom (2 * div x 2)) c
>>= \{slashResult :=
consume Pound
>>= \{_ :=
pound
stor
(Atom (div x 2))
(Cell slashResult b)
c}}}
| _ := err "Invalid pound target"
}
}
}
| _ := err "Pound must be atom";
terminating
evalOp
{val : Type}
(stor : Storage Nat val)
(op : NockOp)
(a : Noun)
(args : Noun)
: GasState Noun :=
case op of
| Slash := slash stor args a
| Constant := pure args
| Apply :=
case args of {
| Cell b c :=
nock stor (Cell a b)
>>= \{r1 :=
nock stor (Cell a c) >>= \{r2 := nock stor (Cell r1 r2)}}
| _ := err "Invalid apply args"
}
| CellTest :=
case args of {
| Cell b _ :=
nock stor (Cell a b)
>>= \{res :=
case res of
| Cell _ _ := pure (Atom 0)
| _ := pure (Atom 1)}
| _ := err "Invalid cell test args"
}
| Increment :=
case args of {
| Cell b _ :=
nock stor (Cell a b)
>>= \{res :=
case res of
| Atom n := pure (Atom (suc n))
| x := pure x}
| _ := err "Invalid increment args"
}
| EqualOp :=
case args of {
| Cell b c :=
nock stor (Cell a b)
>>= \{r1 :=
nock stor (Cell a c)
>>= \{r2 :=
pure
(Atom
case nounEq r1 r2 of {
| true := 0
| false := 1
})}}
| _ := err "Invalid equality args"
}
| IfThenElse :=
case args of {
| Cell b (Cell c d) :=
nock stor (Cell a (Cell (Atom 4) (Cell (Atom 4) b)))
>>= \{r1 :=
nock stor (Cell (Cell (Atom 2) (Atom 3)) (Cell (Atom 0) r1))
>>= \{r2 :=
nock stor (Cell (Cell c d) (Cell (Atom 0) r2))
>>= \{r3 := nock stor (Cell a r3)}}}
| _ := err "Invalid if-then-else args"
}
| Compose :=
case args of {
| Cell b c := nock stor (Cell a b) >>= \{r := nock stor (Cell r c)}
| _ := err "Invalid compose args"
}
| Extend :=
case args of {
| Cell b c :=
nock stor (Cell a b) >>= \{r := nock stor (Cell (Cell r a) c)}
| _ := err "Invalid extend args"
}
| Invoke :=
case args of {
| Cell b c :=
nock stor (Cell a c)
>>= \{core :=
let
formula :=
Cell
(Atom 2)
(Cell (Cell (Atom 0) (Atom 1)) (Cell (Atom 0) b));
in nock stor (Cell core formula)}
| _ := err "Invalid invoke args"
}
| Pound :=
case args of {
| Cell (Cell b c) d :=
nock stor (Cell a c)
>>= \{r1 := nock stor (Cell a d) >>= \{r2 := pound stor b r1 r2}}
| _ := err "Invalid pound args"
}
| Match :=
case args of {
| Cell (Cell b c) d :=
nock stor (Cell a c)
>>= \{r1 :=
nock stor (Cell a d)
>>= \{r2 :=
nock stor (Cell (Cell r1 r2) (Cell (Atom 0) (Atom 3)))}}
| Cell _ c := nock stor (Cell a c)
| _ := err "Invalid pure pound args"
}
| Scry :=
case args of
| Cell b (Cell c d) :=
nock stor b
>>= \{opcode :=
case opcode of
| Atom opval :=
nock stor c
>>= \{addr :=
case addr of
| Atom addrVal :=
let
scryType :=
case opval == 0 of
| true := Direct
| false := Index;
in mkGasState
\{gas :=
scry stor scryType addrVal
>>= \{scryResult :=
GasState.runGasState
(nock stor (Cell a (Cell scryResult d)))
gas}}
| _ := err "Scry address must be atom"}
| _ := err "Scry type must be atom"}
| _ := err "Invalid scry args";
terminating
nock {val : Type} (stor : Storage Nat val) (input : Noun) : GasState Noun :=
case input of
| Atom _ := pure input
| Cell a b :=
case b of
| Cell first rest :=
case first of {
| Cell b c :=
nock stor (Cell a (Cell b c))
>>= \{r1 :=
nock stor (Cell a rest) >>= \{r2 := pure (Cell r1 r2)}}
| Atom n :=
case parseOp n of {
| some opcode :=
consume opcode >>= \{_ := evalOp stor opcode a rest}
| none := err "Invalid operation"
}
}
| _ := err "Invalid Nock expression";
Nockma instances for transaction function functionality;
instance
NockmaTransactionFunction
: TransactionFunction Noun Nat (Option Noun) Nat Noun Noun :=
mkTransactionFunction@{
readStorage :=
\{addr := Cell (Atom 12) (Cell (Atom 0) (Cell (Atom addr) (Atom 1)))};
readByIndex :=
\{prog := Cell (Atom 12) (Cell (Atom 1) (Cell prog (Atom 1)))};
cost :=
\{prog :=
let
terminating
countNodes (n : Noun) : Nat :=
case n of
| Atom a :=
case parseOp a of {
| some op := getGasCost op
| none := 0
}
| Cell a b := countNodes a + countNodes b;
in countNodes prog};
};
instance
NockmaVM : TransactionVM Noun Nat (Option Noun) Nat Noun Noun :=
mkTransactionVM@{
txFunc := NockmaTransactionFunction;
eval :=
\{prog gas :=
case
GasState.runGasState (nock (externalStorage {Nat} {Nat}) prog) gas
of
| ok result := ok (fst result)
| error msg := error msg};
};