Feature/coq

.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
+

examples/zkapps/09-recursion/src/Add.v

@@ -0,0 +1,76 @@
+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.
+
+(* SelfProof is represented as a record *)
+Record SelfProof := {
+  sp_publicInput : nat;
+}.
+
+(* ZkProgram is represented as a module type *)
+Module Type ZkProgram.
+  Parameter name : String.string.
+  Parameter publicInput : nat.
+
+  Parameter init : nat -> Prop.
+  Parameter addNumber : nat -> SelfProof -> nat -> Prop.
+  Parameter add : nat -> SelfProof -> SelfProof -> Prop.
+End ZkProgram.
+
+
+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.
+
+Set Extraction Output Directory "../../extraction".
+Extraction "example.ml" main main_holds makeSelfProof Add.Add.Add .
+
+
+(*Redirect "extraction/add.rs" Rust Extract main_holds.*)
+

examples/zkapps/09-recursion/src/dune

@@ -0,0 +1,2 @@
+(coq.theory
+ (name Add))

examples/zkapps/09-recursion/src/dune-project

@@ -0,0 +1,2 @@
+(lang dune 3.7)
+(using coq 0.7)

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 =
+  __

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 : __