From eb36492e2ba0dc6522bd59731f25de0031742888 Mon Sep 17 00:00:00 2001 From: Guillaume Claret Date: Sun, 22 Dec 2024 15:29:38 +0100 Subject: [PATCH] ci: add Circom as third-party and CI file --- .github/workflows/coq.yml | 53 ++++ .gitignore | 45 ---- .gitmodules | 6 + Garden/.gitignore | 11 + Garden/Circom/Example/binsum.v | 83 ++++++ Garden/Garden.v | 117 +++++++++ Garden/Makefile | 31 +++ Garden/RecordUpdate.v | 135 ++++++++++ Garden/_CoqProject | 5 + Garden/blacklist.txt | 1 + Garden/coq-garden.opam | 23 ++ README.md | 6 + scripts/coq_of_circom.py | 446 +++++++++++++++++++++++++++++++++ third-party/circom | 1 + third-party/circomlib | 1 + 15 files changed, 919 insertions(+), 45 deletions(-) create mode 100644 .github/workflows/coq.yml delete mode 100644 .gitignore create mode 100644 .gitmodules create mode 100644 Garden/.gitignore create mode 100644 Garden/Circom/Example/binsum.v create mode 100644 Garden/Garden.v create mode 100644 Garden/Makefile create mode 100644 Garden/RecordUpdate.v create mode 100644 Garden/_CoqProject create mode 100644 Garden/blacklist.txt create mode 100644 Garden/coq-garden.opam create mode 100644 scripts/coq_of_circom.py create mode 160000 third-party/circom create mode 160000 third-party/circomlib diff --git a/.github/workflows/coq.yml b/.github/workflows/coq.yml new file mode 100644 index 0000000..1e6a9d4 --- /dev/null +++ b/.github/workflows/coq.yml @@ -0,0 +1,53 @@ +name: Coq + +on: + push: + branches: [ "main" ] + pull_request: + branches: [ "main" ] + +env: + CARGO_TERM_COLOR: always + +jobs: + build: + + runs-on: ubuntu-latest + + steps: + - uses: actions/checkout@v3 + - name: Download Git submodules + run: git submodule update --init --recursive + - uses: coq-community/docker-coq-action@v1 + with: + custom_image: coqorg/coq:8.20-ocaml-4.14-flambda + custom_script: | + startGroup "Install dependencies" + curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y + source "$HOME/.cargo/env" + cargo --version + sudo ln -s `which python3` /usr/bin/python + opam install -y --deps-only Garden/coq-garden.opam + endGroup + startGroup "Set the rights" + sudo chown -R $(whoami) . + endGroup + startGroup "Install Circom" + cd third-party/circom + cargo install --path circom + cd ../.. + endGroup + startGroup "Translate Circom library" + cd third-party/circomlib/test/circuits + circom greaterthan.circom + cd ../../../.. + python scripts/coq_of_circom.py third-party/circomlib/circuits/binsum.json > Garden/Circom/Example/binsum.v + endGroup + startGroup "Check that the diff is empty (excluding submodules)" + git -c color.ui=always diff --exit-code --ignore-submodules=dirty + endGroup + startGroup "Compile Coq project" + cd Garden + make + cd .. + endGroup diff --git a/.gitignore b/.gitignore deleted file mode 100644 index 66596b2..0000000 --- a/.gitignore +++ /dev/null @@ -1,45 +0,0 @@ -.*.aux -.*.d -*.a -*.cma -*.cmi -*.cmo -*.cmx -*.cmxa -*.cmxs -*.glob -*.ml.d -*.ml4.d -*.mlg.d -*.mli.d -*.mllib.d -*.mlpack.d -*.native -*.o -*.v.d -*.vio -*.vo -*.vok -*.vos -.coq-native -.csdp.cache -.lia.cache -.nia.cache -.nlia.cache -.nra.cache -csdp.cache -lia.cache -nia.cache -nlia.cache -nra.cache -native_compute_profile_*.data - -# generated timing files -*.timing.diff -*.v.after-timing -*.v.before-timing -*.v.timing -time-of-build-after.log -time-of-build-before.log -time-of-build-both.log -time-of-build-pretty.log diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 0000000..45b032e --- /dev/null +++ b/.gitmodules @@ -0,0 +1,6 @@ +[submodule "third-parties/circom"] + path = third-party/circom + url = https://github.com/formal-land/circom.git +[submodule "third-party/circomlib"] + path = third-party/circomlib + url = https://github.com/iden3/circomlib.git diff --git a/Garden/.gitignore b/Garden/.gitignore new file mode 100644 index 0000000..94ab08e --- /dev/null +++ b/Garden/.gitignore @@ -0,0 +1,11 @@ +.lia.cache +.nia.cache +.CoqMakefile.d +_CoqProject +CoqMakefile +CoqMakefile.conf +*.vo +*.vok +*.vos +*.glob +.*.aux diff --git a/Garden/Circom/Example/binsum.v b/Garden/Circom/Example/binsum.v new file mode 100644 index 0000000..0e14f5e --- /dev/null +++ b/Garden/Circom/Example/binsum.v @@ -0,0 +1,83 @@ + +(* Generated by Garden *) +Require Import Garden.Garden. + +(* Function *) +Definition nbits (a : F.t) : M.t F.t := + M.function_body ( + (* Var *) + do~ M.declare_var "n" [[ [] ]] in + do~ M.substitute "n" [[ 1 ]] in + (* Var *) + do~ M.declare_var "r" [[ [] ]] in + do~ M.substitute "r" [[ 0 ]] in + do~ M.while [[ InfixOp.Lesser ~(| InfixOp.Sub ~(| M.var ~(| "n" |), 1 |), M.var ~(| "a" |) |)]] + do~ M.substitute "r" [[ InfixOp.Add ~(| M.var ~(| "r" |), 1 |) ]] in + do~ M.substitute "n" [[ InfixOp.Mul ~(| M.var ~(| "n" |), 1 |) ]] in + M.pure tt + in + do~ M.return [[ M.var ~(| "r" |) ]] in + M.pure tt + ). + +(* Template *) +Definition BinSum (n ops : F.t) : Template.t F.t := + (* Var *) + do~ M.declare_var "nout" [[ [] ]] in + do~ M.substitute "nout" [[ nbits ~(| InfixOp.Mul ~(| InfixOp.Sub ~(| InfixOp.Pow ~(| 1, M.var ~(| "n" |) |), 1 |), M.var ~(| "ops" |) |) |) ]] in + (* Signal Input *) + do~ M.declare_signal "in" [[ [M.var ~(| "ops" |); M.var ~(| "n" |)] ]] in + (* Signal Output *) + do~ M.declare_signal "out" [[ [M.var ~(| "nout" |)] ]] in + (* Var *) + do~ M.declare_var "lin" [[ [] ]] in + do~ M.substitute "lin" [[ 0 ]] in + (* Var *) + do~ M.declare_var "lout" [[ [] ]] in + do~ M.substitute "lout" [[ 0 ]] in + (* Var *) + do~ M.declare_var "k" [[ [] ]] in + do~ M.substitute "k" [[ 0 ]] in + (* Var *) + do~ M.declare_var "j" [[ [] ]] in + do~ M.substitute "j" [[ 0 ]] in + (* Var *) + do~ M.declare_var "e2" [[ [] ]] in + do~ M.substitute "e2" [[ 0 ]] in + do~ M.substitute "e2" [[ 1 ]] in + do~ M.substitute "k" [[ 0 ]] in + do~ M.while [[ InfixOp.Lesser ~(| M.var ~(| "k" |), M.var ~(| "n" |) |)]] + do~ M.substitute "j" [[ 0 ]] in + do~ M.while [[ InfixOp.Lesser ~(| M.var ~(| "j" |), M.var ~(| "ops" |) |)]] + do~ M.substitute "lin" [[ InfixOp.Add ~(| M.var ~(| "lin" |), InfixOp.Mul ~(| M.var_access ~(| "in", [Access.Array M.var ~(| "j" |); Access.Array M.var ~(| "k" |)] |), M.var ~(| "e2" |) |) |) ]] in + M.pure tt + do~ M.substitute "j" [[ InfixOp.Add ~(| M.var ~(| "j" |), 1 |) ]] in + M.pure tt + in + M.pure tt + do~ M.substitute "e2" [[ InfixOp.Add ~(| M.var ~(| "e2" |), M.var ~(| "e2" |) |) ]] in + M.pure tt + do~ M.substitute "k" [[ InfixOp.Add ~(| M.var ~(| "k" |), 1 |) ]] in + M.pure tt + in + M.pure tt + do~ M.substitute "e2" [[ 1 ]] in + do~ M.substitute "k" [[ 0 ]] in + do~ M.while [[ InfixOp.Lesser ~(| M.var ~(| "k" |), M.var ~(| "nout" |) |)]] + do~ M.substitute "out" [[ InfixOp.BitAnd ~(| InfixOp.ShiftR ~(| M.var ~(| "lin" |), M.var ~(| "k" |) |), 1 |) ]] in + do~ M.equality_constraint + [[ InfixOp.Mul ~(| M.var_access ~(| "out", [Access.Array M.var ~(| "k" |)] |), InfixOp.Sub ~(| M.var_access ~(| "out", [Access.Array M.var ~(| "k" |)] |), 1 |) |) ]] + [[ 0 ]] + in + do~ M.substitute "lout" [[ InfixOp.Add ~(| M.var ~(| "lout" |), InfixOp.Mul ~(| M.var_access ~(| "out", [Access.Array M.var ~(| "k" |)] |), M.var ~(| "e2" |) |) |) ]] in + do~ M.substitute "e2" [[ InfixOp.Add ~(| M.var ~(| "e2" |), M.var ~(| "e2" |) |) ]] in + M.pure tt + do~ M.substitute "k" [[ InfixOp.Add ~(| M.var ~(| "k" |), 1 |) ]] in + M.pure tt + in + M.pure tt + do~ M.equality_constraint + [[ M.var ~(| "lin" |) ]] + [[ M.var ~(| "lout" |) ]] + in + M.pure tt. diff --git a/Garden/Garden.v b/Garden/Garden.v new file mode 100644 index 0000000..3bbc1a9 --- /dev/null +++ b/Garden/Garden.v @@ -0,0 +1,117 @@ +Require Export Coq.Strings.Ascii. +Require Coq.Strings.HexString. +Require Export Coq.Strings.String. +Require Export Coq.ZArith.ZArith. +From Ltac2 Require Ltac2. +Require Export RecordUpdate. + +Require Export Lia. +From Hammer Require Export Tactics. + +(* Activate the modulo arithmetic in [lia] *) +Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations. + +Global Set Primitive Projections. +Global Set Printing Projections. +Global Open Scope char_scope. +Global Open Scope string_scope. +Global Open Scope list_scope. +Global Open Scope type_scope. +Global Open Scope Z_scope. +Global Open Scope bool_scope. + +Export List.ListNotations. + +Inductive sigS {A : Type} (P : A -> Set) : Set := +| existS : forall (x : A), P x -> sigS P. +Arguments existS {_ _}. + +Reserved Notation "{ x @ P }" (at level 0, x at level 99). +Reserved Notation "{ x : A @ P }" (at level 0, x at level 99). +Reserved Notation "{ ' pat : A @ P }" + (at level 0, pat strict pattern, format "{ ' pat : A @ P }"). + +Notation "{ x @ P }" := (sigS (fun x => P)) : type_scope. +Notation "{ x : A @ P }" := (sigS (A := A) (fun x => P)) : type_scope. +Notation "{ ' pat : A @ P }" := (sigS (A := A) (fun pat => P)) : type_scope. + +Module F. + Definition t := Z. +End F. + +Module BlockUnit. + (** The return value of a code block. *) + Inductive t : Set := + (** The default value *) + | Tt + (** The instruction `return` was called *) + | Return (value : F.t). +End BlockUnit. + +Module Primitive. + (** We group together primitives that share being impure functions operating over the state. *) + Inductive t : Set -> Set := + | OpenScope : t unit + | CloseScope : t unit + | DeclareVar (names : list string) (values : list F.t) : t unit + | AssignVar (names : list string) (values : list F.t) : t unit + | GetVar (name : string) : t F.t. +End Primitive. + +Module M. + Inductive t (A : Set) : Set := + | Pure + (output : A) + | Primitive {B : Set} + (primitive : Primitive.t B) + (k : B -> t A) + | Loop {In Out : Set} + (init : In) + (body : In -> t Out) + (** The final value to return if we decide to break of the loop, otherwise what to continue + with. *) + (break_with : Out -> In + Out) + (k : Out -> t A) + (** Explicit cut in the monadic expressions, to provide better composition for the proofs. *) + | Let {B : Set} (e1 : t B) (k : B -> t A) + (** Similar to [Let], a marker to help for the proofs. *) + | Call {B : Set} (e : t B) (k : B -> t A) + | Impossible (message : string). + Arguments Pure {_}. + Arguments Primitive {_ _}. + Arguments Loop {_ _ _}. + Arguments Let {_ _}. + Arguments Call {_ _}. + Arguments Impossible {_}. + + Fixpoint let_ {A B : Set} (e1 : t A) (e2 : A -> t B) : t B := + match e1 with + | Pure (output) => + e2 output + | Primitive primitive k => + Primitive primitive (fun result => let_ (k result) e2) + | Loop input body break_with k => + Loop input body break_with (fun result => let_ (k result) e2) + | Let e1 k => + Let e1 (fun result => let_ (k result) e2) + | Call e k => + Call e (fun result => let_ (k result) e2) + | Impossible message => Impossible message + end. + + Definition do (block1 block2 : t BlockUnit.t) : t BlockUnit.t := + Let block1 (fun (result : BlockUnit.t) => + match result with + | BlockUnit.Tt => block2 + | BlockUnit.Return _ => block1 + end). + + Definition function_body (block : t BlockUnit.t) : t F.t := + Primitive Primitive.OpenScope (fun _ => + Let block (fun (result : BlockUnit.t) => + Primitive Primitive.CloseScope (fun _ => + match result with + | BlockUnit.Tt => Impossible "Expected a return in the function body" + | BlockUnit.Return value => Pure value + end))). +End M. diff --git a/Garden/Makefile b/Garden/Makefile new file mode 100644 index 0000000..8d75540 --- /dev/null +++ b/Garden/Makefile @@ -0,0 +1,31 @@ +.PHONY: all clean clean-util distclean default + +VFILES := $(shell find -L . -name "*.v" | grep -v -f blacklist.txt | sort) + +default: all + +CoqMakefile: $(VFILES) blacklist.txt + echo "-R . Garden" > _CoqProject + echo "-arg -impredicative-set -arg -w -arg -stdlib-vector" >> _CoqProject + # We copy & paste the command to find files as this variable is too long on command line + find -L . -name "*.v" | grep -v -f blacklist.txt | sort >> _CoqProject + coq_makefile -f _CoqProject -o $@ + +MAKECOQ := +$(MAKE) -f CoqMakefile + +%.vo: CoqMakefile %.v + $(MAKECOQ) $@ + +all: CoqMakefile + $(MAKECOQ) all + +clean-coq: CoqMakefile + $(MAKECOQ) clean + +clean-util: + rm -f *CoqMakefile* + +clean: clean-coq + $(MAKE) clean-util # done separately to enforce order + +distclean: clean diff --git a/Garden/RecordUpdate.v b/Garden/RecordUpdate.v new file mode 100644 index 0000000..3e68181 --- /dev/null +++ b/Garden/RecordUpdate.v @@ -0,0 +1,135 @@ +(** This file adds syntax for update of record fields, in the presence of primitive projections. *) +(* Modifed from: https://github.com/mit-plv/riscv-coq/blob/3a4ddc56fce50c0167fbe887987086fcc157153c/src/riscv/Utility/RecordSetters.v *) + +Require Import Coq.Program.Basics. +Require Import Ltac2.Ltac2. +Require Ltac2.Option. +Require Import Ltac2.Bool. +Set Default Proof Mode "Classic". + +Ltac2 rec strip_foralls (t : constr) := + match Constr.Unsafe.kind t with + | Constr.Unsafe.Prod b u => let (bs, body) := strip_foralls u in (b :: bs, body) + | _ => ([], t) + end. + +Ltac2 app_arg_count (t : constr) := + match Constr.Unsafe.kind t with + | Constr.Unsafe.App _ args => Array.length args + | _ => 0 + end. + +Ltac2 binder_to_field (qualification : ident list) (b : binder) := + Option.get (Env.get (List.append qualification [Option.get (Constr.Binder.name b)])). + +Ltac2 field_names (ctor_ref : Std.reference) := + let ctor_type := Constr.type (Env.instantiate ctor_ref) in + let (binders, result) := strip_foralls ctor_type in + let n_type_args := app_arg_count result in + let field_name_binders := List.skipn n_type_args binders in + List.map (binder_to_field (List.removelast (Env.path ctor_ref))) field_name_binders. + +Ltac2 constructor_of_record (t : constr) := + match Constr.Unsafe.kind t with + | Constr.Unsafe.Ind ind _ => + Std.ConstructRef (Constr.Unsafe.constructor ind 0) + | _ => Control.throw (Invalid_argument (Some (Message.of_constr t))) + end. + +Ltac2 mkApp (f : constr) (args : constr array) := + Constr.Unsafe.make (Constr.Unsafe.App f args). + +Ltac2 record_with_set_val (ty : constr) (record : constr) + (field : constr) (val : constr) : constr := + let (h, args) := + match Constr.Unsafe.kind ty with + | Constr.Unsafe.App h args => (h, args) + | _ => (ty, Array.empty) + end in + let ctor := constructor_of_record h in + let getters := List.map (fun getterRef => + mkApp (Env.instantiate getterRef) args) (field_names ctor) in + let fields := List.map (fun getter => + if Constr.equal getter field then val else '($getter $record) + ) getters in + let res := + mkApp (mkApp (Env.instantiate ctor) args) (Array.of_list fields) in + res. + +Ltac2 setter (ty : constr) (field : constr) : constr := '( + fun v r => ltac2:( + let res := record_with_set_val ty &r field &v in exact $res) + ). + +Ltac exact_setter := + ltac2:(ty field |- + let t := Option.get (Ltac1.to_constr ty) in + let f := Option.get (Ltac1.to_constr field) in + let res := setter t f + in exact $res). + +Class Setter{R E: Type}(getter: R -> E): Type := + set : E -> R -> R. + +Arguments set {R E} (getter) {Setter} (fieldUpdater) (r). + +Global Hint Extern 1 (@Setter ?R ?E ?getter) => + exact_setter R getter : typeclass_instances. + +Module Export RecordSetNotations1. + Declare Scope record_set. + Delimit Scope record_set with rs. + Open Scope rs. + Notation "record <| field := v |>" := (set field v record) + (at level 8, v at level 99, left associativity, + format "record <| field := v |>") + : record_set. +End RecordSetNotations1. + +Module RecordSetterTests. + Module PrimProjTests. + Local Set Primitive Projections. + + Record Test (X : Type) := { + f1 : X; + f2 : X * X; + }. + + Arguments f1 {_}. + Arguments f2 {_}. + + Goal forall X (t : Test X) (x : X), + t <| f1 := x |>.(f1) = x. + Proof. + intros; reflexivity. + Qed. + + Goal forall X (t : Test X) (x : X), + t <| f1 := x |>.(f2) = t.(f2). + Proof. + intros; reflexivity. + Qed. + End PrimProjTests. + + Module NonPrimProjTests. + Record Test (X : Type) := { + f1 : X; + f2 : X * X; + }. + + Arguments f1 {_}. + Arguments f2 {_}. + + Goal forall X (t : Test X) (x : X), + t <| f1 := x |>.(f1) = x. + Proof. + intros; reflexivity. + Qed. + + Goal forall X (t : Test X) (x : X), + t <| f1 := x |>.(f2) = t.(f2). + Proof. + intros; reflexivity. + Qed. + End NonPrimProjTests. +End RecordSetterTests. diff --git a/Garden/_CoqProject b/Garden/_CoqProject new file mode 100644 index 0000000..202d6e7 --- /dev/null +++ b/Garden/_CoqProject @@ -0,0 +1,5 @@ +-R . Garden +-arg -impredicative-set -arg -w -arg -stdlib-vector +./Circom/Example/binsum.v +./Garden.v +./RecordUpdate.v diff --git a/Garden/blacklist.txt b/Garden/blacklist.txt new file mode 100644 index 0000000..8c4944a --- /dev/null +++ b/Garden/blacklist.txt @@ -0,0 +1 @@ +Circom/Example/binsum.v \ No newline at end of file diff --git a/Garden/coq-garden.opam b/Garden/coq-garden.opam new file mode 100644 index 0000000..26a7fe5 --- /dev/null +++ b/Garden/coq-garden.opam @@ -0,0 +1,23 @@ +opam-version: "2.0" +name: "coq-garden" +version: "0.1.0" +synopsis: "Garden" +description: """ +Formal verification for zero-knowledge circuits +""" +maintainer: "Guillaume Claret " +authors: [ + "Formal Land " +] +license: "MIT" +homepage: "https://github.com/formal-land/garden" +bug-reports: "https://github.com/formal-land/garden/issues" +dev-repo: "git+https://github.com/formal-land/garden.git" +depends: [ + "coq" {>= "8.20.0" } + "coq-coqutil" {>= "0.0.5"} + "coq-hammer" +] +build: [ + [make] +] diff --git a/README.md b/README.md index c8826f5..3a5873b 100644 --- a/README.md +++ b/README.md @@ -1,5 +1,11 @@ # Garden +> Make your zero-knowledge applications safe with formal verification! +

logo

+ +## Overview + +We first target the formal verification of [Circom](https://github.com/iden3/circom) circuits using the [🐓 Coq](https://coq.inria.fr/) proof assistant. diff --git a/scripts/coq_of_circom.py b/scripts/coq_of_circom.py new file mode 100644 index 0000000..8b795dd --- /dev/null +++ b/scripts/coq_of_circom.py @@ -0,0 +1,446 @@ +""" +Translate Circom circuits to Coq code. +""" +import json +import sys + +def indent(text: str) -> str: + return "\n".join(" " + line for line in text.split("\n")) + +""" +pub type TagList = Vec; +""" +def to_coq_tag_list(node) -> str: + return "[" + ", ".join(f"\"{tag}\"" for tag in node) + "]" + +""" +pub enum SignalType { + Output, + Input, + Intermediate, +} +""" +def signal_type_to_coq(node) -> str: + if "Output" in node: + return "Output" + if "Input" in node: + return "Input" + if "Intermediate" in node: + return "Intermediate" + return f"Unknown signal type: {node}" + +""" +pub enum VariableType { + Var, + Signal(SignalType, TagList), + Component, + AnonymousComponent, + Bus(String, SignalType, TagList), +} +""" +def to_coq_variable_type(node) -> str: + if "Var" in node: + return "Var" + if "Signal" in node: + signal = node["Signal"] + return \ + "Signal " + signal_type_to_coq(signal[0]) + if "Component" in node: + return "Component" + if "AnonymousComponent" in node: + return "AnonymousComponent" + if "Bus" in node: + bus = node["Bus"] + return "Bus " + bus["String"] + " " + bus["SignalType"] + " " + bus["TagList"] + return f"Unknown variable type: {node}" + +""" +pub enum LogArgument { + LogStr(String), + LogExp(Expression), +} +""" +def to_coq_log_argument(node) -> str: + if "LogStr" in node: + return f"LogStr {node['LogStr']}" + if "LogExp" in node: + return f"LogExp {to_coq_expression(node['LogExp'])}" + return f"Unknown log argument: {node}" + +""" +pub enum Access { + ComponentAccess(String), + ArrayAccess(Expression), +} +""" +def to_coq_access(node) -> str: + if "ComponentAccess" in node: + return f"Access.Component {node['ComponentAccess']}" + if "ArrayAccess" in node: + return f"Access.Array {to_coq_expression(node['ArrayAccess'])}" + return f"Unknown access: {node}" + +""" +pub enum Expression { + InfixOp { + meta: Meta, + lhe: Box, + infix_op: ExpressionInfixOpcode, + rhe: Box, + }, + PrefixOp { + meta: Meta, + prefix_op: ExpressionPrefixOpcode, + rhe: Box, + }, + InlineSwitchOp { + meta: Meta, + cond: Box, + if_true: Box, + if_false: Box, + }, + ParallelOp { + meta: Meta, + rhe: Box, + }, + Variable { + meta: Meta, + name: String, + access: Vec, + }, + Number(Meta, BigInt), + Call { + meta: Meta, + id: String, + args: Vec, + }, + BusCall { + meta: Meta, + id: String, + args: Vec, + }, + AnonymousComp{ + meta: Meta, + id: String, + is_parallel: bool, + params: Vec, + signals: Vec, + names: Option>, + }, + ArrayInLine { + meta: Meta, + values: Vec, + }, + Tuple { + meta: Meta, + values: Vec, + }, + UniformArray { + meta: Meta, + value: Box, + dimension: Box, + }, +} +""" +def to_coq_expression(node) -> str: + if "InfixOp" in node: + infix_op = node["InfixOp"] + return \ + "InfixOp." + infix_op["infix_op"] + " ~(| " + \ + to_coq_expression(infix_op["lhe"]) + ", " + \ + to_coq_expression(infix_op["rhe"]) + \ + " |)" + if "PrefixOp" in node: + prefix_op = node["PrefixOp"] + return \ + "PrefixOp." + prefix_op["prefix_op"] + " ~(| " + \ + to_coq_expression(prefix_op["rhe"]) + \ + " |)" + if "InlineSwitchOp" in node: + inline_switch_op = node["InlineSwitchOp"] + return \ + "(" + to_coq_expression(inline_switch_op["cond"]) + " ? " + to_coq_expression(inline_switch_op["if_true"]) + " : " + to_coq_expression(inline_switch_op["if_false"]) + ")" + if "ParallelOp" in node: + parallel_op = node["ParallelOp"] + return "ParallelOp " + to_coq_expression(parallel_op["rhe"]) + if "Variable" in node: + variable = node["Variable"] + if len(variable["access"]) == 0: + return \ + "M.var ~(| " + \ + "\"" + variable["name"] + "\"" + \ + " |)" + return \ + "M.var_access ~(| " + \ + "\"" + variable["name"] + "\"" + ", " + \ + "[" + "; ".join(to_coq_access(access) for access in variable["access"]) + "]" + \ + " |)" + if "Number" in node: + number = node["Number"] + return str(number[1][0]) + if "Call" in node: + call = node["Call"] + return \ + call["id"] + " ~(| " + \ + ", ".join(to_coq_expression(arg) for arg in call["args"]) + \ + " |)" + if "BusCall" in node: + bus_call = node["BusCall"] + return bus_call["id"] + "(" + ", ".join(to_coq_expression(arg) for arg in bus_call["args"]) + ")" + if "AnonymousComp" in node: + anonymous_comp = node["AnonymousComp"] + return \ + "AnonymousComp " + anonymous_comp["id"] + " " + str(anonymous_comp["is_parallel"]) + " " + \ + ", ".join(to_coq_expression(param) for param in anonymous_comp["params"]) + " " + \ + ", ".join(to_coq_expression(signal) for signal in anonymous_comp["signals"]) + if "ArrayInLine" in node: + array_in_line = node["ArrayInLine"] + return \ + "ArrayInLine {" + ", ".join(to_coq_expression(value) for value in array_in_line["values"]) + "}" + if "Tuple" in node: + tuple = node["Tuple"] + return \ + "Tuple {" + ", ".join(to_coq_expression(value) for value in tuple["values"]) + "}" + if "UniformArray" in node: + uniform_array = node["UniformArray"] + return \ + "UniformArray " + to_coq_expression(uniform_array["value"]) + " " + to_coq_expression(uniform_array["dimension"]) + return f"Unknown expression: {node}" + +""" +pub enum Statement { + IfThenElse { + meta: Meta, + cond: Expression, + if_case: Box, + else_case: Option>, + }, + While { + meta: Meta, + cond: Expression, + stmt: Box, + }, + Return { + meta: Meta, + value: Expression, + }, + InitializationBlock { + meta: Meta, + xtype: VariableType, + initializations: Vec, + }, + Declaration { + meta: Meta, + xtype: VariableType, + name: String, + dimensions: Vec, + is_constant: bool, + }, + Substitution { + meta: Meta, + var: String, + access: Vec, + op: AssignOp, + rhe: Expression, + }, + MultSubstitution { + meta: Meta, + lhe: Expression, + op: AssignOp, + rhe: Expression, + }, + UnderscoreSubstitution{ + meta: Meta, + op: AssignOp, + rhe: Expression, + }, + ConstraintEquality { + meta: Meta, + lhe: Expression, + rhe: Expression, + }, + LogCall { + meta: Meta, + args: Vec, + }, + Block { + meta: Meta, + stmts: Vec, + }, + Assert { + meta: Meta, + arg: Expression, + }, +} +""" +def to_coq_statement(node) -> str: + if "IfThenElse" in node: + if_then_else = node["IfThenElse"] + return \ + "if " + to_coq_expression(if_then_else["cond"]) + " then\n" + \ + indent(to_coq_statement(if_then_else["if_case"])) + "\n" + \ + "else\n" + \ + indent(to_coq_statement(if_then_else["else_case"])) + "\n" + \ + "end" + if "While" in node: + while_stmt = node["While"] + return \ + "do~ M.while [[ " + to_coq_expression(while_stmt["cond"]) + "]]\n" + \ + indent(to_coq_statement(while_stmt["stmt"])) + "\n" + \ + "in" + if "Return" in node: + return "do~ M.return [[ " + to_coq_expression(node["Return"]["value"]) + " ]] in" + if "InitializationBlock" in node: + init_block = node["InitializationBlock"] + return \ + "(* " + to_coq_variable_type(init_block["xtype"]) + " *)\n" + \ + "\n".join(to_coq_statement(stmt) for stmt in init_block["initializations"]) + if "Declaration" in node: + declaration = node["Declaration"] + xtype = declaration["xtype"] + if xtype == "Var": + declare_function = "M.declare_var" + elif xtype == "Component": + declare_function = "M.declare_component" + elif xtype == "AnonymousComponent": + declare_function = "M.declare_anonymous_component" + elif "Signal" in xtype: + declare_function = "M.declare_signal" + elif xtype == "Bus": + declare_function = "M.declare_bus" + else: + declare_function = f"Unknown xtype {xtype}" + return \ + "do~ " + declare_function + " \"" + declaration["name"] + "\" " + \ + "[[ [" + \ + "; ".join(to_coq_expression(dim) for dim in declaration["dimensions"]) + \ + "] ]] in" + if "Substitution" in node: + substitution = node["Substitution"] + return \ + "do~ M.substitute \"" + substitution["var"] + "\" " + \ + "[[ " + to_coq_expression(substitution["rhe"]) + " ]] in" + if "MultSubstitution" in node: + mult_substitution = node["MultSubstitution"] + return \ + "MultSubstitution " + to_coq_expression(mult_substitution["lhe"]) + " = " + \ + to_coq_expression(mult_substitution["rhe"]) + if "UnderscoreSubstitution" in node: + underscore_substitution = node["UnderscoreSubstitution"] + return \ + "UnderscoreSubstitution = " + to_coq_expression(underscore_substitution["rhe"]) + if "ConstraintEquality" in node: + constraint_equality = node["ConstraintEquality"] + return \ + "do~ M.equality_constraint\n" + \ + indent( + "[[ " + to_coq_expression(constraint_equality["lhe"]) + " ]]\n" + \ + "[[ " + to_coq_expression(constraint_equality["rhe"]) + " ]]" + ) + "\n" + \ + "in" + if "LogCall" in node: + log_call = node["LogCall"] + return \ + "LogCall " + ", ".join(to_coq_log_argument(arg) for arg in log_call["args"]) + if "Block" in node: + block = node["Block"] + return \ + "\n".join(to_coq_statement(stmt) for stmt in block["stmts"]) + "\n" + \ + "M.pure tt" + if "Assert" in node: + return "assert " + to_coq_expression(node["Assert"]["arg"]) + return f"Unknown statement: {node}" + +def to_coq_definition_args(args: list[str]) -> str: + if len(args) == 0: + return "" + return " (" + " ".join(args) + " : F.t)" + +""" +pub enum Definition { + Template { + meta: Meta, + name: String, + args: Vec, + arg_location: FileLocation, + body: Statement, + parallel: bool, + is_custom_gate: bool, + }, + Function { + meta: Meta, + name: String, + args: Vec, + arg_location: FileLocation, + body: Statement, + }, + Bus { + meta: Meta, + name: String, + args: Vec, + arg_location: FileLocation, + body: Statement, + }, +} +""" +def to_coq_definition(node) -> str: + if "Template" in node: + template = node["Template"] + return \ + "(* Template *)\n" + \ + "Definition " + template["name"] + to_coq_definition_args(template["args"]) + \ + " : Template.t F.t :=\n" + \ + indent( + to_coq_statement(template["body"]) + "." + ) + if "Function" in node: + function = node["Function"] + return \ + "(* Function *)\n" + \ + "Definition " + function["name"] + to_coq_definition_args(function["args"]) + \ + " : M.t F.t :=\n" + \ + indent( + "M.function_body (\n" + \ + indent( + to_coq_statement(function["body"]) + ) + "\n" + + ")." + ) + if "Bus" in node: + bus = node["Bus"] + return \ + "(* Bus *)\n" + \ + "Definition " + bus["name"] + to_coq_definition_args(bus["args"]) + \ + " : Bus.t F.t :=\n" + \ + indent( + to_coq_statement(bus["body"]) + "." + ) + return f"Unknown definition: {node}" + +""" +pub struct AST { + pub meta: Meta, + pub compiler_version: Option, + pub custom_gates: bool, + pub custom_gates_declared: bool, + pub includes: Vec, + pub definitions: Vec, + pub main_component: Option, +} +""" +def to_coq_ast(node) -> str: + header = """ +(* Generated by Garden *) +Require Import Garden.Garden. + +""" + return \ + header + \ + "\n\n".join(to_coq_definition(definition) for definition in node["definitions"]) + +# Load the first command line parameter +with open(sys.argv[1], "r") as f: + json_data = f.read() + +# Print the Coq code +print(to_coq_ast(json.loads(json_data))) diff --git a/third-party/circom b/third-party/circom new file mode 160000 index 0000000..159fe5c --- /dev/null +++ b/third-party/circom @@ -0,0 +1 @@ +Subproject commit 159fe5c853272ca82616a2fe9bd6cf80ad42d3b6 diff --git a/third-party/circomlib b/third-party/circomlib new file mode 160000 index 0000000..0a045ae --- /dev/null +++ b/third-party/circomlib @@ -0,0 +1 @@ +Subproject commit 0a045aec50d51396fcd86a568981a5a0afb99e95