datalog

Cargo.toml

@@ -29,6 +29,11 @@ ahash = "0.7"
 good_lp = { version = "1.1", features = ["lp-solvers", "coin_cbc"], default-features = false }
 lp-solvers = "0.0.4"
 serde_json = "1.0"
+pest = "2.1"
+pest_derive = "2.1"
+pest-ast = "0.3"
+from-pest = "0.3"
+clap = "2"
 
 [dev-dependencies]
 quickcheck = "1"

Makefile

@@ -4,7 +4,7 @@ build: init
 	cargo build --release --example circ && ./scripts/build_mpc_zokrates_test.zsh && ./scripts/build_aby.zsh
 
 test:
-	cargo test && ./scripts/zokrates_test.zsh && python3 ./scripts/test_aby.py && ./scripts/test_zok_to_ilp.zsh
+	cargo test && ./scripts/zokrates_test.zsh && ./scripts/test_datalog.zsh && python3 ./scripts/test_aby.py && ./scripts/test_zok_to_ilp.zsh
 
 init:
 	git submodule update --init

examples/circ.rs

@@ -2,16 +2,20 @@
 use bellman::gadgets::test::TestConstraintSystem;
 use bellman::Circuit;
 use bls12_381::Scalar;
-use circ::front::zokrates::{Inputs, Mode, Zokrates};
+use circ::front::datalog::{self, Datalog};
+use circ::front::zokrates::{self, Mode, Zokrates};
 use circ::front::FrontEnd;
 use circ::ir::opt::{opt, Opt};
 use circ::target::aby::output::write_aby_exec;
 use circ::target::aby::trans::to_aby;
 use circ::target::ilp::trans::to_ilp;
 use circ::target::r1cs::opt::reduce_linearities;
 use circ::target::r1cs::trans::to_r1cs;
+use clap::arg_enum;
 use env_logger;
 use good_lp::default_solver;
+use std::fs::File;
+use std::io::Read;
 use std::path::PathBuf;
 use structopt::StructOpt;
 
@@ -30,9 +34,25 @@ struct Options {
     #[structopt(short, long, name = "PARTIES")]
     parties: Option<u8>,
 
+    /// Input language
+    #[structopt(short, long, name = "LANG", default_value = "zokrates")]
+    lang: InputLang,
+
     /// Whether to maximize the output
     #[structopt(short, long)]
     maximize: bool,
+
+    /// How many recursions to allow (datalog)
+    #[structopt(short, long, name = "N", default_value = "5")]
+    rec_limit: usize,
+}
+
+arg_enum! {
+    #[derive(PartialEq, Debug)]
+    pub enum InputLang {
+        Zokrates,
+        Datalog,
+    }
 }
 
 fn main() {
@@ -51,12 +71,23 @@ fn main() {
             None => Mode::Proof,
         }
     };
-    let inputs = Inputs {
-        file: options.zokrates_path,
-        inputs: options.inputs,
-        mode: mode.clone(),
+    let cs = match options.lang {
+        InputLang::Zokrates => {
+            let inputs = zokrates::Inputs {
+                file: options.zokrates_path,
+                inputs: options.inputs,
+                mode: mode.clone(),
+            };
+            Zokrates::gen(inputs)
+        }
+        InputLang::Datalog => {
+            let inputs = datalog::Inputs {
+                file: options.zokrates_path,
+                rec_limit: options.rec_limit,
+            };
+            Datalog::gen(inputs)
+        }
     };
-    let cs = Zokrates::gen(inputs);
     let cs = match mode {
         Mode::Opt => opt(cs, vec![Opt::ConstantFold]),
         Mode::Mpc(_) => opt(

examples/datalog/arr.pl

@@ -0,0 +1,3 @@
+main(X: public field[2], Y: public field[2], Z: public field[2]) :-
+    X[0] * Y[0] = Z[0],
+    X[1] * Y[1] = Z[1].

examples/datalog/bits8.pl

@@ -0,0 +1 @@
+has_bits(X: field, Y: u8) :- X = to_field(Y).

examples/datalog/call.pl

@@ -0,0 +1,3 @@
+main(X: field, Y: field, Z: u4) :- non_zero(X), non_zero(Y), to_field(Z) = Y.
+
+non_zero(X: field) :- exists I: field. X * I = 1.

examples/datalog/dec.pl

@@ -0,0 +1,12 @@
+hash(X: u8[5], Y: u8[5], decreasing n: u8) :-
+    n = 0, X = Y;
+  exists Z: u8[5].
+    !(n = 0),
+    X[0] + X[1] = Z[0],
+    X[1] - X[2] = Z[1],
+    X[2] | X[3] = Z[2],
+    X[3] ^ X[4] = Z[3],
+    hash(Z, Y, n-1).
+
+main(X: private u8[5], Y: public u8[5]) :-
+  hash(X, Y, 5).

examples/datalog/dumb_hash.pl

@@ -0,0 +1,12 @@
+hash(X: u8[5], Y: u8[5], n: u8) :-
+    n = 0, X = Y;
+  exists Z: u8[5].
+    !(n = 0),
+    X[0] + X[1] = Z[0],
+    X[1] - X[2] = Z[1],
+    X[2] | X[3] = Z[2],
+    X[3] ^ X[4] = Z[3],
+    hash(Z, Y, n-1).
+
+main(X: private u8[5], Y: public u8[5]) :-
+  hash(X, Y, 5).

examples/datalog/err.pl

@@ -0,0 +1,12 @@
+hash(X: u8[5], Y: u8[5], n: u8) :-
+    n = 0, X = Y;
+  exists Z: u8[5], B: bool.
+    !(n = 0),
+    X[0] + X[1] = Z[0] + B,
+    X[1] - X[2] = Z[1],
+    X[2] | X[3] = Z[2],
+    X[3] ^ X[4] = Z[3],
+    hash(Z, Y, n-1).
+
+main(X: private u8[5], Y: public u8[5]) :-
+  hash(X, Y, 5).

examples/datalog/inv.pl

@@ -0,0 +1 @@
+main(X: field) :- exists I: field. X * I = 1.

examples/datalog/parse_test/one_rule.pl

@@ -0,0 +1,4 @@
+non_zero(Z: field) :- ((Z + Y) + Y) + ~!-Y + to_field(Y);
+                      Z;
+                      exists A: field. A * Z = 1;
+                      exists B: field, C: bool. B * C * Z = 4.

examples/datalog/unbound_rec.pl

@@ -0,0 +1,3 @@
+bad_nz(X: field) :- exists I: field. X * I = 1, bad_nz(I).
+
+main(X: field) :- bad_nz(X).

scripts/test_datalog.zsh

@@ -0,0 +1,21 @@
+#!/usr/bin/env zsh
+
+set -ex
+
+disable -r time
+
+cargo build --example circ
+
+BIN=./target/debug/examples/circ
+
+$BIN --lang datalog ./examples/datalog/parse_test/one_rule.pl || true
+$BIN --lang datalog ./examples/datalog/inv.pl || true
+$BIN --lang datalog ./examples/datalog/call.pl || true
+$BIN --lang datalog ./examples/datalog/arr.pl || true
+# Small R1cs b/c too little recursion.
+size=$(($BIN --lang datalog ./examples/datalog/dumb_hash.pl -r 4 || true) | egrep "Final R1cs size:" | egrep -o "\\b[0-9]+")
+[ "$size" -lt 10 ]
+# Big R1cs b/c enough recursion
+($BIN --lang datalog ./examples/datalog/dumb_hash.pl -r 5 || true) | egrep "Final R1cs size: 306"
+($BIN --lang datalog ./examples/datalog/dumb_hash.pl -r 10 || true) | egrep "Final R1cs size: 306"
+($BIN --lang datalog ./examples/datalog/dec.pl -r 2 || true) | egrep "Final R1cs size: 306"

src/front/datalog/error.rs

@@ -0,0 +1,86 @@
+//! Error implementation for datalog frontend
+
+use thiserror::Error;
+
+use super::term::T;
+use super::parser::ast::Span;
+
+use std::fmt::{Display, Formatter, self};
+use std::convert::From;
+
+#[derive(Error, Debug)]
+/// An error in circuit translation
+pub enum ErrorKind {
+    #[error("Cannot apply operator '{0}' to '{1}'")]
+    /// Cannot apply this operator to this term
+    InvalidUnOp(String, T),
+    #[error("Cannot apply operator '{0}' to\n\t{1}\nand\n\t{2}")]
+    /// Cannot apply this operator to these terms
+    InvalidBinOp(String, T, T),
+    #[error("Could not find entry rule '{0}'")]
+    /// Could not find the entry rule
+    MissingEntry(String),
+    #[error("Circify error: {0}")]
+    /// Could not find the entry rule
+    Circify(crate::circify::CircError),
+}
+
+#[derive(Debug)]
+/// An error with an optional span
+pub struct Error<'ast> {
+    /// The error
+    pub kind: ErrorKind,
+    /// The span
+    pub span: Option<Span<'ast>>,
+}
+
+impl<'ast> Display for Error<'ast> {
+    fn fmt(&self, f: &mut Formatter) -> fmt::Result {
+        writeln!(f, "Error: {}", self.kind)?;
+        if let Some(s) = &self.span {
+            writeln!(f, "\nLocation:")?;
+            for l in s.lines() {
+                writeln!(f, "  {}", l)?;
+            }
+        }
+        Ok(())
+    }
+}
+
+impl<'ast> From<ErrorKind> for Error<'ast> {
+    fn from(error_kind: ErrorKind) -> Self {
+        Error {
+            kind: error_kind,
+            span: None,
+        }
+    }
+}
+
+impl<'ast> From<crate::circify::CircError> for Error<'ast> {
+    fn from(circ: crate::circify::CircError) -> Self {
+        Error {
+            kind: ErrorKind::Circify(circ),
+            span: None,
+        }
+    }
+}
+
+impl<'ast> Error<'ast> {
+    /// Attach span to error
+    pub fn with_span(self, span: Span<'ast>) -> Self {
+        Error {
+            kind: self.kind,
+            span: Some(span),
+        }
+    }
+    /// New error, with span
+    pub fn new(kind: ErrorKind, span: Span<'ast>) -> Self {
+        Error {
+            kind,
+            span: Some(span),
+        }
+    }
+}
+
+/// Fallible value
+pub type Result<'ast, T> = std::result::Result<T, Error<'ast>>;

src/front/datalog/grammar.pest

@@ -0,0 +1,70 @@
+literal = { hex_literal | decimal_literal | boolean_literal }
+decimal_literal = @{ "0" | ASCII_NONZERO_DIGIT ~ ASCII_DIGIT* }
+boolean_literal = @{ "true" | "false" }
+hex_literal = @{ "0x" ~ ASCII_HEX_DIGIT+ }
+bin_literal = @{ "0b" ~ ("0" | "1")+ }
+
+bin_op = _{ add | sub | mul | div | shl | shr | bitand | bitor | bitxor | or | and | urem | eq }
+    add      = { "+" }
+    sub      = { "-" }
+    mul      = { "*" }
+    div      = { "/" }
+    eq       = { "=" }
+    urem     = { "%" }
+    shl      = { "<<" }
+    lt       = { "<" }
+    gt       = { ">" }
+    lte      = { "<=" }
+    gte      = { ">=" }
+    shr      = { ">>" }
+    bitxor   = { "^" }
+    bitand   = { "&" }
+    bitor    = { "|" }
+    or       = { "||" }
+    and      = { "&&" }
+
+un_op = { neg | bitnot | not }
+    neg = { "-" }
+    bitnot = { "~" }
+    not = { "!" }
+
+call_expr = { identifier ~ "(" ~ expr_list ~ ")" }
+expr = { term ~ (bin_op ~ term)* }
+paren_expr = { "(" ~ expr ~ ")" }
+term = { call_expr | literal | access_expr | identifier | paren_expr | unary_expression }
+unary_expression = { un_op ~ term }
+expr_list = _{ expr ~ ("," ~ expr)* }
+access = _{ "[" ~ expr ~ "]" }
+access_expr = { identifier ~ access+ }
+
+identifier = @{ (ASCII_ALPHANUMERIC | "_") ~ (ASCII_ALPHANUMERIC | "_")* }
+
+decl_list = _{ decl ~ ("," ~ decl)* }
+decl = { identifier ~ ":" ~ qual_ty }
+fn_arg_decl = { dec? ~ identifier ~ ":" ~ qual_ty }
+fn_arg_decl_list = _{ fn_arg_decl ~ ("," ~ fn_arg_decl)* }
+exist_prefix = { "exists" ~ decl_list ~ "." }
+condition = { exist_prefix? ~ expr_list }
+rule_cases = _{ condition ~ (";" ~ condition)* ~ "." }
+rule = { identifier ~ "(" ~ fn_arg_decl_list ~ ")" ~ ":-" ~ rule_cases }
+
+program = { SOI ~ rule* ~ EOI }
+
+WHITESPACE = _{ " " | "\t" | "\n" }
+
+// basic types (ZoKrates)
+ty_field = {"field"}
+ty_uint = @{"u" ~ ASCII_NONZERO_DIGIT ~ ASCII_DIGIT* }
+ty_bool = {"bool"}
+base_ty = { ty_field | ty_uint | ty_bool }
+array_size = _{ "[" ~ decimal_literal ~ "]" }
+array_sizes = _{ array_size* }
+ty = { base_ty ~ array_sizes }
+
+vis_private = {"private"}
+vis_public = {"public"}
+vis = { vis_private | vis_public }
+
+dec = { "decreasing" }
+
+qual_ty = { vis? ~ ty }