Multisig.new

multisig/.gitignore

@@ -0,0 +1,3 @@
+kompile_tool/k
+kompile_tool/k.old
+bazel-*

multisig/kompile_tool/BUILD

@@ -0,0 +1,63 @@
+sh_binary(
+  name = "kompile_tool",
+  srcs = ["kompile.sh"],
+  deps = [":k_release"],
+  data = [":k_release"],
+  visibility = ["//visibility:public"],
+)
+
+sh_binary(
+  name = "kompile_e_tool",
+  srcs = ["kompile-e.sh"],
+  deps = [":k_release"],
+  data = [":k_release"],
+  visibility = ["//visibility:public"],
+)
+
+sh_binary(
+  name = "kprove_tool",
+  srcs = ["kprove.sh"],
+  deps = [":k_release"],
+  data = [":k_release"],
+  visibility = ["//visibility:public"],
+)
+
+sh_binary(
+  name = "kprove_kompile_tool",
+  srcs = ["kprove-kompile.sh"],
+  deps = [":k_release"],
+  data = [":k_release"],
+  visibility = ["//visibility:public"],
+)
+
+sh_binary(
+  name = "kore_tool",
+  srcs = ["kore.sh"],
+  deps = [":k_release"],
+  data = [":k_release"],
+  visibility = ["//visibility:public"],
+)
+
+sh_binary(
+  name = "ktrusted_tool",
+  srcs = ["make-trusted.py"],
+  visibility = ["//visibility:public"],
+)
+
+sh_binary(
+  name = "kmerge_tool",
+  srcs = ["kmerge.sh"],
+  visibility = ["//visibility:public"],
+)
+
+sh_library(
+  name = "k_release",
+  data = glob(["k/**"]),
+  visibility = ["//visibility:public"],
+)
+
+sh_library(
+  name = "kast_script",
+  srcs = ["kast.kscript"],
+  visibility = ["//visibility:public"],
+)

multisig/kompile_tool/kast.kscript

@@ -0,0 +1,18 @@
+alias kclaim = claim | kast -i kore -o pretty -d . /dev/stdin
+alias kclaim-d x = claim | kast -i kore -o pretty -d x /dev/stdin
+alias kclaim-n x = claim x | kast -i kore -o pretty -d . /dev/stdin
+alias kclaim-nd x y = claim x | kast -i kore -o pretty -d y /dev/stdin
+alias kaxiom x = axiom x | kast -i kore -o pretty -d . /dev/stdin
+alias kaxiom-d x y = axiom x | kast -i kore -o pretty -d y /dev/stdin
+alias konfig = config | kast -i kore -o pretty -d . /dev/stdin
+alias konfig-d x = config | kast -i kore -o pretty -d x /dev/stdin
+alias konfig-n x = config x | kast -i kore -o pretty -d . /dev/stdin
+alias konfig-nd x y = config x | kast -i kore -o pretty -d y /dev/stdin
+alias ktry x = try x | kast -i kore -o pretty -d . /dev/stdin
+alias ktry-d x y = try x | kast -i kore -o pretty -d y /dev/stdin
+alias ktryf x = tryf x | kast -i kore -o pretty -d . /dev/stdin
+alias ktryf-d x y = tryf x | kast -i kore -o pretty -d y /dev/stdin
+alias krule = rule | kast -i kore -o pretty -d . /dev/stdin
+alias krule-d x = rule | kast -i kore -o pretty -d x /dev/stdin
+alias krule-n x = rule x | kast -i kore -o pretty -d . /dev/stdin
+alias krule-nd x y = rule x | kast -i kore -o pretty -d y /dev/stdin

multisig/kompile_tool/kmerge.sh

@@ -0,0 +1,18 @@
+#!/usr/bin/env bash
+
+set -e
+
+OUTPUT=$1
+shift
+
+FIRST=$1
+shift
+
+cat $FIRST | sed 's/^.*\/\/@ Bazel remove\s*$/\/\/ Removed by Bazel + kmerge./' > $OUTPUT
+echo >> $OUTPUT
+
+for f in "$@"
+do
+  cat "$f" | sed 's/^.*\/\/@ Bazel remove\s*$/\/\/ Removed by Bazel + kmerge./' >> $OUTPUT
+  echo >> $OUTPUT
+done

multisig/kompile_tool/kompile-e.sh

@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+set -e
+
+PARENT_DIR=`dirname $0`
+
+KOMPILE=$PARENT_DIR/kompile_e_tool.runfiles/__main__/kompile_tool/k/bin/kompile
+$KOMPILE --backend haskell -I `pwd` -E "$@" > /dev/null

multisig/kompile_tool/kompile.sh

@@ -0,0 +1,12 @@
+#!/usr/bin/env bash
+
+set -e
+
+PARENT_DIR=`dirname $0`
+
+OUTPUT_DIR=`dirname $1`
+OUTPUT_DIR=`dirname $OUTPUT_DIR`
+shift
+
+KOMPILE=$PARENT_DIR/kompile_tool.runfiles/__main__/kompile_tool/k/bin/kompile
+$KOMPILE --backend haskell -I `pwd` --directory $OUTPUT_DIR "$@"

multisig/kompile_tool/kore.sh

@@ -0,0 +1,59 @@
+#!/usr/bin/env bash
+
+set -e
+
+SPEC_MODULE_NAME=$1
+shift
+
+KOMPILE_DIR=`dirname $1`
+shift
+
+DEFINITION=$(realpath $1)
+shift
+
+SPEC=$(realpath $1)
+shift
+
+COMMAND=$1
+shift
+
+OUTPUT=$(realpath $1)
+shift
+
+BREADTH=$1
+shift
+
+MODULE_NAME=$(cat $COMMAND | sed 's/^.*--module \([^ ]*\) .*$/\1/')
+
+# SPEC_MODULE_NAME=$(cat $COMMAND | sed 's/^.*--spec-module \([^ ]*\) .*$/\1/')
+
+KOMPILE_TOOL_DIR=kompile_tool
+
+REPL_SCRIPT=$(realpath $KOMPILE_TOOL_DIR/kast.kscript)
+
+KORE_EXEC="$(realpath $KOMPILE_TOOL_DIR/k/bin/kore-exec) --breadth $BREADTH"
+KORE_REPL="$(realpath $KOMPILE_TOOL_DIR/k/bin/kore-repl) --repl-script $REPL_SCRIPT"
+
+BACKEND_COMMAND=$KORE_EXEC
+if [ $# -eq 0 ]; then
+  BACKEND_COMMAND=$KORE_EXEC
+else
+  if [ "$1" == "--debug" ]; then
+    BACKEND_COMMAND=$KORE_REPL
+  else
+    echo "Unknown argument: '$1'"
+    exit 1
+  fi
+fi
+
+PATH=$(realpath $KOMPILE_TOOL_DIR/k/bin):$PATH
+
+cd $(dirname $KOMPILE_DIR)
+
+$BACKEND_COMMAND \
+    --smt-timeout 4000 \
+    $DEFINITION \
+    --prove $SPEC \
+    --module $MODULE_NAME \
+    --spec-module $SPEC_MODULE_NAME \
+    --output $OUTPUT

multisig/kompile_tool/kprove-kompile.sh

@@ -0,0 +1,61 @@
+#!/usr/bin/env bash
+
+set -e
+
+KOMPILE_DIR=`dirname $1`
+shift
+
+ORIGINAL_FILE=$1
+shift
+
+PROOF_FILE=$(realpath $1)
+shift
+
+SPEC_OUTPUT=$1
+shift
+
+DEFINITION_OUTPUT=$1
+shift
+
+COMMAND_OUTPUT=$1
+shift
+
+KOMPILE_OUTPUT=$(dirname $1)
+shift
+
+MODULE_NAME=$(basename "$ORIGINAL_FILE" | sed 's/\.[^\.]*$//' | tr [:lower:] [:upper:])
+
+KOMPILE_TOOL_DIR=kompile_tool
+
+KPROVE=$(realpath $KOMPILE_TOOL_DIR/k/bin/kprove)
+
+TMP_DIR=$(mktemp -d)
+trap 'rm -rf -- "$TMP_DIR"' EXIT
+
+cp -rL $KOMPILE_DIR $TMP_DIR
+chmod -R a+w $TMP_DIR/*
+
+pushd $TMP_DIR > /dev/null
+
+nice -n 10 \
+$KPROVE \
+  --spec-module "$MODULE_NAME" \
+  --dry-run \
+  "$PROOF_FILE" > output
+
+SPEC_FILE=$(cat output | grep kore-exec | sed 's/^.*--prove \([^ ]*\) .*$/\1/')
+COMMAND=$(cat output | grep kore-exec)
+
+popd > /dev/null
+
+cp $SPEC_FILE $SPEC_OUTPUT
+
+DEFINITION_FILE=$(dirname $SPEC_FILE)/vdefinition.kore
+
+cp $DEFINITION_FILE $DEFINITION_OUTPUT
+
+echo $COMMAND > $COMMAND_OUTPUT
+
+mkdir -p $KOMPILE_OUTPUT
+
+cp $TMP_DIR/$(basename $KOMPILE_DIR)/* $KOMPILE_OUTPUT

multisig/kompile_tool/kprove.sh

@@ -0,0 +1,60 @@
+#!/usr/bin/env bash
+
+set -e
+
+PARENT_DIR=$(dirname $0)
+
+KOMPILE_DIR=$(dirname $1)
+shift
+
+TMP_DIR=$(mktemp -d)
+trap 'rm -rf -- "$TMP_DIR"' EXIT
+
+ORIGINAL_FILE=$1
+shift
+
+PROOF_FILE=$(realpath $1)
+shift
+
+BREADTH=$1
+shift
+
+#KOMPILE_PARENT = $(dirname $KOMPILE_DIR)
+#
+MODULE_NAME=$(basename "$ORIGINAL_FILE" | sed 's/\.[^\.]*$//' | tr [:lower:] [:upper:])
+
+cp -rL $KOMPILE_DIR $TMP_DIR
+chmod -R a+w $TMP_DIR/*
+
+KOMPILE_TOOL_DIR=kompile_tool
+
+KPROVE=$(realpath $KOMPILE_TOOL_DIR/k/bin/kprove)
+REPL_SCRIPT=$(realpath $KOMPILE_TOOL_DIR/kast.kscript)
+
+#PROOF_FILE_PATH=$(realpath $PROOF_FILE)
+#REPL_SCRIPT_PATH=$(realpath $REPL_SCRIPT)
+#
+KORE_EXEC="kore-exec --breadth $BREADTH"
+KORE_REPL="kore-repl --repl-script $REPL_SCRIPT"
+
+BACKEND_COMMAND=$KORE_EXEC
+if [ $# -eq 0 ]; then
+  BACKEND_COMMAND=$KORE_EXEC
+else
+  if [ "$1" == "--debug" ]; then
+    BACKEND_COMMAND=$KORE_REPL
+  else
+    echo "Unknown argument: '$1'"
+    exit 1
+  fi
+fi
+
+cd $TMP_DIR
+echo $TMP_DIR
+
+$KPROVE \
+  --haskell-backend-command "$BACKEND_COMMAND --smt-timeout 4000" \
+  --spec-module "$MODULE_NAME" \
+  "$PROOF_FILE"
+
+#  --directory "$TMP_DIR" \

multisig/kompile_tool/make-trusted.py

@@ -0,0 +1,65 @@
+#!/usr/bin/env python3
+import sys
+
+def naturalNumbers():
+  i = 1
+  while True:
+    yield i
+    i += 1
+
+DEFAULT = 0
+PROOF = 1
+TRUSTED = 2
+
+def makeTrusted(file_name, lines):
+  state = DEFAULT
+  for (line_number, line) in lines:
+    normalized = line.strip()
+    if normalized.startswith('//@'):
+      if state == DEFAULT:
+        if normalized == '//@ proof':
+          state = PROOF
+        else:
+          raise Exception(
+            "Unexpected trusted directive, only '//@ proof' allowed here.\n%s:%d"
+            % (file_name, line_number))
+      elif state == PROOF:
+        if normalized == '//@ trusted':
+          state = TRUSTED
+        else:
+          raise Exception(
+            "Unexpected trusted directive, only '//@ trusted' allowed here.\n%s:%d"
+            % (file_name, line_number))
+      elif state == TRUSTED:
+        if normalized == '//@ end':
+          state = DEFAULT
+        else:
+          raise Exception(
+            "Unexpected trusted directive, only '//@ end' allowed here.\n%s:%d"
+            % (file_name, line_number))
+    else:
+      if state == DEFAULT:
+        pass
+      else:
+        unindented = line.lstrip()
+        indentation = ' ' * (len(line) - len(unindented))
+        if state == PROOF:
+          line = indentation + '// ' + unindented
+        elif state == TRUSTED:
+          if unindented.startswith('// '):
+            line = indentation + unindented[3:]
+          else:
+            raise Exception(
+              "Expected trusted lines to be commented.\n%s:%d"
+              % (file_name, line_number))
+    yield line
+
+def main(argv):
+  if len(argv) != 2:
+    raise Exception('Wrong number of arguments, expected an input and an output file name.')
+  with open(argv[0], 'r') as f:
+    with open(argv[1], 'w') as g:
+      g.writelines(makeTrusted(argv[0], zip(naturalNumbers(), f)))
+
+if __name__ == '__main__':
+  main(sys.argv[1:])

multisig/kompile_tool/prepare-k.sh

@@ -0,0 +1,9 @@
+#!/usr/bin/env bash
+
+KOMPILE=`which kompile`
+BIN=`dirname $KOMPILE`
+RELEASE=`dirname $BIN`
+
+mkdir k
+
+cp -r $RELEASE/* k