nala

Embeddable OCaml and C toolkit for deterministic polymorphic bytecode execution. It's bytecode has a stable logical instruction set, while physical opcode numbers can be permuted across mutation epochs. Mutated programs keep the same observable behaviour and traces still show both the logical instruction and the physical opcode that reached it

Build

make build

Start

Build/run the factorial

dune exec -- nala build examples/factorial.nala.asm -o examples/factorial.nala
dune exec -- nala verify examples/factorial.nala
dune exec -- nala run examples/factorial.nala

Mutate the physical opcode mapping with a reproducible seed

dune exec -- nala mutate examples/factorial.nala --seed 42 -o examples/factorial.mut.nala
dune exec -- nala run examples/factorial.mut.nala
dune exec -- nala inspect examples/factorial.mut.nala

Trace the mutated package

dune exec -- nala trace examples/factorial.mut.nala

pc=0000 epoch=43 physical=011 logical=const   stack=[]->[6]
pc=0001 epoch=43 physical=019 logical=call    stack=[6]->[]

CLI

nala build <source> -o program.nala
nala run program.nala
nala verify program.nala
nala disasm program.nala
nala mutate program.nala --seed <n> -o mutated.nala
nala trace program.nala
nala inspect program.nala
nala repl

Assembly

.meta name answer
.func main 0 0
  const 40
  const 2
  add
  out
  halt

Functions declare argument count and local count

.func main 0 0
  const 6
  call fact
  out
  halt

.func fact 1 1
  load 0
  const 2
  lt
  jz recur
  const 1
  ret
recur:
  load 0
  load 0
  const 1
  sub
  call fact
  mul
  ret

Host imports are explicit and arity checked

.import double 1
.func main 0 0
  const 21
  import double
  out
  halt

OCaml API

let fail diags =
  List.iter (fun d -> prerr_endline (Nala.Verifier.pp_diagnostic d)) diags;
  exit 1

let () =
  match Nala.Assembler.assemble_file "examples/factorial.nala.asm" with
  | Error e -> fail e
  | Ok program ->
      begin match Nala.Verifier.verify program with
      | Error e -> fail e
      | Ok () -> ()
      end;
      let mutated = Nala.Mutator.mutate ~seed:42 program in
      match Nala.Vm.run mutated with
      | Ok result -> print_string result.output
      | Error e -> fail e

Read/write packages

let program =
  match Nala.Package.read_file "program.nala" with
  | Ok p -> p
  | Error e -> fail e

let () =
  match Nala.Package.write_file "copy.nala" program with
  | Ok () -> ()
  | Error e -> fail e

C API

#include "nala.h"

Register a deterministic import

static nala_status_t doublefn(void *user, const int32_t *args, size_t argc,
                              int32_t *result, nala_error_t *error) {
  (void)user;
  (void)error;
  if (argc != 1) return NALA_ERR_HOST;
  *result = args[0] * 2;
  return NALA_OK;
}

Create a context, load a package, and run

nala_error_t error;
nala_context_t *ctx = nala_context_new(NULL);
nala_program_t *program = NULL;
nala_vm_t *vm = NULL;

nala_program_load(bytes, len, &program, &error);
nala_context_register_import(ctx, "double", 1, doublefn, NULL, &error);
nala_vm_new(ctx, program, &vm, &error);
nala_vm_run(vm, NULL, NULL, &error);

size_t outlen = 0;
const uint8_t *out = nala_vm_output(vm, &outlen);
fwrite(out, 1, outlen, stdout);

nala_vm_free(vm);
nala_program_free(program);
nala_context_free(ctx);