From b8f567cb62e98ce1ce6e7e5163be3b06126ec7d1 Mon Sep 17 00:00:00 2001 From: mike dupont Date: Fri, 2 Aug 2024 07:55:39 -0400 Subject: [PATCH 1/3] compiles --- examples/zkapps/09-recursion/src/dune | 2 ++ examples/zkapps/09-recursion/src/dune-project | 2 ++ 2 files changed, 4 insertions(+) create mode 100644 examples/zkapps/09-recursion/src/dune create mode 100644 examples/zkapps/09-recursion/src/dune-project diff --git a/examples/zkapps/09-recursion/src/dune b/examples/zkapps/09-recursion/src/dune new file mode 100644 index 000000000..1df8786dd --- /dev/null +++ b/examples/zkapps/09-recursion/src/dune @@ -0,0 +1,2 @@ +(coq.theory + (name Add)) \ No newline at end of file diff --git a/examples/zkapps/09-recursion/src/dune-project b/examples/zkapps/09-recursion/src/dune-project new file mode 100644 index 000000000..b1a38abe0 --- /dev/null +++ b/examples/zkapps/09-recursion/src/dune-project @@ -0,0 +1,2 @@ +(lang dune 3.7) +(using coq 0.7) \ No newline at end of file From f948eaa6ffcb7b9ddb3e09c857501892f26ff04b Mon Sep 17 00:00:00 2001 From: mike dupont Date: Fri, 2 Aug 2024 07:55:49 -0400 Subject: [PATCH 2/3] compiles --- examples/zkapps/09-recursion/src/Add.v | 67 ++++++++++++++++++++++++++ 1 file changed, 67 insertions(+) create mode 100644 examples/zkapps/09-recursion/src/Add.v diff --git a/examples/zkapps/09-recursion/src/Add.v b/examples/zkapps/09-recursion/src/Add.v new file mode 100644 index 000000000..43f886c13 --- /dev/null +++ b/examples/zkapps/09-recursion/src/Add.v @@ -0,0 +1,67 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.Lists.List. +Require Import Coq.Strings.String. + +Import ListNotations. +Open Scope string_scope. + +(* SelfProof is represented as a record *) +Record SelfProof := { + sp_publicInput : nat; +}. + +(* ZkProgram is represented as a module type *) +Module Type ZkProgram. + Parameter name : string. + Parameter publicInput : nat. + + Parameter init : nat -> Prop. + Parameter addNumber : nat -> SelfProof -> nat -> Prop. + Parameter add : nat -> SelfProof -> SelfProof -> Prop. +End ZkProgram. + + +Definition name1 := "add-example". +(* Defining our Add program *) +Module Add <: ZkProgram. + + Definition name := "add-example". + Definition publicInput := 0. + + Definition init (state : nat) : Prop := state = 0. + + Definition addNumber (newState : nat) (earlierProof : SelfProof) (numberToAdd : nat) : Prop := + newState = (sp_publicInput earlierProof) + numberToAdd. + + Definition add (newState : nat) (earlierProof1 : SelfProof) (earlierProof2 : SelfProof) : Prop := + newState = (sp_publicInput earlierProof1) + (sp_publicInput earlierProof2). +End Add. + +(* Helper function to create a SelfProof *) +Definition makeSelfProof (input : nat) : SelfProof := {| + sp_publicInput := input; +|}. + +(* Main function *) +Definition main : Prop := + exists proof0 proof1 proof2, + (* Compilation step - we just assume it's done *) + True /\ + (* Making proof 0 *) + Add.init (sp_publicInput proof0) /\ + (* Making proof 1 *) + Add.addNumber (sp_publicInput proof1) proof0 4 /\ + (* Making proof 2 *) + Add.add (sp_publicInput proof2) proof1 proof0 /\ + (* Verification step - we just assume it's done *) + True. + +(* Theorem to prove that our main proposition holds *) +Theorem main_holds : main. +Proof. + unfold main. + exists (makeSelfProof 0). + exists (makeSelfProof 4). + exists (makeSelfProof 4). + repeat split. +Qed. From b0fd66164e200856096552a4b130e9115a17c58d Mon Sep 17 00:00:00 2001 From: mike dupont Date: Fri, 2 Aug 2024 12:17:17 -0400 Subject: [PATCH 3/3] adding coq extraction --- .gitignore | 49 ++++++++++++++++ examples/zkapps/09-recursion/src/Add.v | 15 ++++- examples/zkapps/09-recursion/src/dune-project | 2 +- .../09-recursion/src/extraction/example.ml | 58 +++++++++++++++++++ .../09-recursion/src/extraction/example.mli | 34 +++++++++++ 5 files changed, 154 insertions(+), 4 deletions(-) create mode 100644 examples/zkapps/09-recursion/src/extraction/example.ml create mode 100644 examples/zkapps/09-recursion/src/extraction/example.mli diff --git a/.gitignore b/.gitignore index 10101d590..aeb8b13be 100644 --- a/.gitignore +++ b/.gitignore @@ -29,3 +29,52 @@ yarn-error.log* *.swp .vscode/ +# -*- mode: gitignore; -*- +*~ +\#*\# +/.emacs.desktop +/.emacs.desktop.lock +*.elc +auto-save-list +tramp +.\#* + +# Org-mode +.org-id-locations +*_archive + +# flymake-mode +*_flymake.* + +# eshell files +/eshell/history +/eshell/lastdir + +# elpa packages +/elpa/ + +# reftex files +*.rel + +# AUCTeX auto folder +/auto/ + +# cask packages +.cask/ +dist/ + +# Flycheck +flycheck_*.el + +# server auth directory +/server/ + +# projectiles files +.projectile + +# directory configuration +.dir-locals.el + +# network security +/network-security.data + diff --git a/examples/zkapps/09-recursion/src/Add.v b/examples/zkapps/09-recursion/src/Add.v index 43f886c13..786b52b00 100644 --- a/examples/zkapps/09-recursion/src/Add.v +++ b/examples/zkapps/09-recursion/src/Add.v @@ -1,6 +1,10 @@ +Require Extraction. +Extraction Language OCaml. Require Import Coq.ZArith.ZArith. Require Import Coq.Lists.List. Require Import Coq.Strings.String. +Require Import MetaCoq.Template.All. +Require Import MetaCoq.Template.Checker. Import ListNotations. Open Scope string_scope. @@ -12,7 +16,7 @@ Record SelfProof := { (* ZkProgram is represented as a module type *) Module Type ZkProgram. - Parameter name : string. + Parameter name : String.string. Parameter publicInput : nat. Parameter init : nat -> Prop. @@ -21,8 +25,6 @@ Module Type ZkProgram. End ZkProgram. -Definition name1 := "add-example". -(* Defining our Add program *) Module Add <: ZkProgram. Definition name := "add-example". @@ -65,3 +67,10 @@ Proof. exists (makeSelfProof 4). repeat split. Qed. + +Set Extraction Output Directory "../../extraction". +Extraction "example.ml" main main_holds makeSelfProof Add.Add.Add . + + +(*Redirect "extraction/add.rs" Rust Extract main_holds.*) + diff --git a/examples/zkapps/09-recursion/src/dune-project b/examples/zkapps/09-recursion/src/dune-project index b1a38abe0..98d5258f3 100644 --- a/examples/zkapps/09-recursion/src/dune-project +++ b/examples/zkapps/09-recursion/src/dune-project @@ -1,2 +1,2 @@ (lang dune 3.7) -(using coq 0.7) \ No newline at end of file +(using coq 0.7) diff --git a/examples/zkapps/09-recursion/src/extraction/example.ml b/examples/zkapps/09-recursion/src/extraction/example.ml new file mode 100644 index 000000000..09c7aa95e --- /dev/null +++ b/examples/zkapps/09-recursion/src/extraction/example.ml @@ -0,0 +1,58 @@ + +type __ = Obj.t +let __ = let rec f _ = Obj.repr f in Obj.repr f + +type bool = +| True +| False + +type nat = +| O +| S of nat + +type ascii = +| Ascii of bool * bool * bool * bool * bool * bool * bool * bool + +type string = +| EmptyString +| String of ascii * string + +type selfProof = + nat + (* singleton inductive, whose constructor was Build_SelfProof *) + +module Add = + struct + (** val name : string **) + + let name = + String ((Ascii (True, False, False, False, False, True, True, False)), + (String ((Ascii (False, False, True, False, False, True, True, False)), + (String ((Ascii (False, False, True, False, False, True, True, False)), + (String ((Ascii (True, False, True, True, False, True, False, False)), + (String ((Ascii (True, False, True, False, False, True, True, False)), + (String ((Ascii (False, False, False, True, True, True, True, False)), + (String ((Ascii (True, False, False, False, False, True, True, False)), + (String ((Ascii (True, False, True, True, False, True, True, False)), + (String ((Ascii (False, False, False, False, True, True, True, False)), + (String ((Ascii (False, False, True, True, False, True, True, False)), + (String ((Ascii (True, False, True, False, False, True, True, False)), + EmptyString))))))))))))))))))))) + + (** val publicInput : nat **) + + let publicInput = + O + end + +(** val makeSelfProof : nat -> selfProof **) + +let makeSelfProof input = + input + +type main = __ + +(** val main_holds : __ **) + +let main_holds = + __ diff --git a/examples/zkapps/09-recursion/src/extraction/example.mli b/examples/zkapps/09-recursion/src/extraction/example.mli new file mode 100644 index 000000000..c131d58fa --- /dev/null +++ b/examples/zkapps/09-recursion/src/extraction/example.mli @@ -0,0 +1,34 @@ + +type __ = Obj.t + +type bool = +| True +| False + +type nat = +| O +| S of nat + +type ascii = +| Ascii of bool * bool * bool * bool * bool * bool * bool * bool + +type string = +| EmptyString +| String of ascii * string + +type selfProof = + nat + (* singleton inductive, whose constructor was Build_SelfProof *) + +module Add : + sig + val name : string + + val publicInput : nat + end + +val makeSelfProof : nat -> selfProof + +type main = __ + +val main_holds : __