WebAssembly backend

.github/workflows/build.yml

@@ -4,6 +4,7 @@ on:
   push:
     branches:
       - master
+      - upstream-pr
   pull_request:
     branches:
       - "**"
@@ -36,6 +37,15 @@ jobs:
             #   opam pin -n -y submodules/metacoq
             # endGroup
           before_script: |
+            startGroup "Install more dependencies"
+              sudo apt install --yes wabt curl
+              # Node in debian bookworm is too old, install via nodesource
+              # TODO once version 22 is in the standard debian repo, use that
+              sudo curl -fsSL https://deb.nodesource.com/setup_22.x -o nodesource_setup.sh
+              sudo bash nodesource_setup.sh
+              sudo apt install -y nodejs
+              node --version
+            endGroup
             startGroup "fix permission issues"
               sudo chown -R coq:coq .
             endGroup

_CoqProject

@@ -8,6 +8,7 @@
 -R theories/LambdaBoxLocal      CertiCoq.LambdaBoxLocal
 -R theories/LambdaANF           CertiCoq.LambdaANF
 -R theories/Codegen             CertiCoq.Codegen
+-R theories/CodegenWasm         CertiCoq.CodegenWasm
 -R theories/Runtime             CertiCoq.runtime
 
 -R benchmarks                   CertiCoq.Benchmarks
@@ -21,4 +22,4 @@
 -R bootstrap/certicoqc/theories CertiCoq.CertiCoqC
 -I bootstrap/certicoqc
 -R bootstrap/certicoqchk        CertiCoq.CertiCoqCheck
--I bootstrap/certicoqchk
+-I bootstrap/certicoqchk

benchmarks/.gitignore

@@ -8,6 +8,10 @@ Top.*
 glue.Top.*
 ffi.Top.*
 
+*.wasm
+*.wat
+*.cwasm
+
 m.h
 gc.c
 gc.h

benchmarks/Makefile

@@ -9,7 +9,7 @@ CFILES=$(patsubst %, CertiCoq.Benchmarks.tests.%_cps.c, $(TESTS)) $(patsubst %,
 EXEC=$(TESTS) $(patsubst %, %_cps, $(TESTS)) $(patsubst %, %_cps_opt, $(TESTS)) $(patsubst %, %_opt, $(TESTS))
 INCLUDE=../runtime
 
-all: lib tests exec run
+all: lib tests exec run run_wasm
 default: exec run
 
 .PHONY: all default clean lib cleanlib tests run $(TESTS)
@@ -112,3 +112,9 @@ $(TESTS): $(CFILES)
 
 run: run.sh
 	sh run.sh 10
+
+run_wasm:
+	@echo "\nRunning CertiCoq-Wasm test suite"
+	make -C wasm run_tests
+	@echo "\nRunning CertiCoq-Wasm primitive unit tests"
+	make -C wasm run_primitive_unit_tests

benchmarks/lib/BernsteinYangTermination.v

@@ -0,0 +1,51 @@
+(* Computation needed to show termination of the Bernstein-Yang modular inversion algorithm *)
+(* taken from: https://github.com/AU-COBRA/coq-rust-extraction/blob/master/tests/theories/BernsteinYangTermination.v *)
+
+From Coq Require Import Bool.
+From Coq Require Import ZArith.
+
+Import Z.
+Local Open Scope Z.
+Definition odd := Z.odd.
+Definition steps := Eval vm_compute in 2 ^ 44 : N.
+Definition shiftl a b := Eval cbv in Z.shiftl a b.
+Definition shiftr a b := Eval cbv in Z.shiftr a b.
+Definition divstep d f g :=
+  if (0 <? d) && odd g
+  then (1 - d, g, shiftr (g - f) 1)
+  else (1 + d, f, shiftr (g + (if odd g then 1 else 0) * f) 1 ).
+Fixpoint needs_n_steps (d a b : Z) n :=
+  match n with
+  | 0%nat => true
+  | S n => if (b =? 0)
+          then false
+          else let '(d', a', b') := divstep d a b in needs_n_steps d' a' b' n
+  end.
+Fixpoint min_needs_n_steps_nat (a b : Z) n (acc : Z) fuel :=
+  match fuel with
+  | 0%nat => 0
+  | S fuel =>
+    let a2 := a * a in
+    if acc <? a2
+        then acc
+        else
+          let length := a2 + b * b in
+          if acc <? length
+             then min_needs_n_steps_nat (a + 2) 0 n acc fuel
+             else if needs_n_steps 1 a (shiftr b 1) n || needs_n_steps 1 a (- (shiftr b 1)) n
+                  then min_needs_n_steps_nat (a + 2) 0 n (Z.min length acc) fuel
+                  else min_needs_n_steps_nat a (b + 2) n acc fuel
+  end.
+Definition nat_shiftl := Eval cbv in Nat.shiftl.
+Definition W n := min_needs_n_steps_nat 1 0 n (shiftl 1 62) (nat_shiftl 1 44).
+
+(*
+Extract Constant nat_shiftl => "fn ##name##(&'a self, a: u64, b: u64) -> u64 { a << b }".
+(* Unsound in general, but fine for this program *)
+Extract Constant shiftl => "fn ##name##(&'a self, a: i64, b: i64) -> i64 { a << b }".
+Extract Constant shiftr => "fn ##name##(&'a self, a: i64, b: i64) -> i64 { a >> b }".
+
+From RustExtraction Require Import ExtrRustBasic.
+From RustExtraction Require Import ExtrRustUncheckedArith.
+Redirect "extracted-code/BernsteinYangTermination.rs" Rust Extract W.
+*)

benchmarks/lib/Makefile

@@ -7,7 +7,7 @@
 ##         #     GNU Lesser General Public License Version 2.1          ##
 ##         #     (see LICENSE file for the text of the license)         ##
 ##########################################################################
-## GNUMakefile for Coq 8.19.1
+## GNUMakefile for Coq 8.19.2
 
 # For debugging purposes (must stay here, don't move below)
 INITIAL_VARS := $(.VARIABLES)
@@ -278,7 +278,7 @@ COQDOCLIBS?=$(COQLIBS_NOML)
 # The version of Coq being run and the version of coq_makefile that
 # generated this makefile
 COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1)
-COQMAKEFILE_VERSION:=8.19.1
+COQMAKEFILE_VERSION:=8.19.2
 
 # COQ_SRC_SUBDIRS is for user-overriding, usually to add
 # `user-contrib/Foo` to the includes, we keep COQCORE_SRC_SUBDIRS for

benchmarks/lib/_CoqProject

@@ -7,4 +7,7 @@ vs.v
 sha256.v
 # bignum.v
 # SqlQueries.v
-coind.v
+coind.v
+BernsteinYangTermination.v
+stack_machine.v
+coqprime.v

benchmarks/lib/coqprime.v

@@ -0,0 +1,74 @@
+(* coq prime benchmark *)
+From Coqprime Require Import PocklingtonRefl.
+From MetaCoq.Utils Require Import bytestring MCString.
+
+Local Open Scope positive_scope.
+Open Scope bs.
+
+Definition cert1 := 
+         (Pock_certif 2453592460649055756812450508556009475577084379843351664172069410531995758325371349410079350684102193 5 ((535891737757285083698263, 1)::(22187633823577, 1)::(2,4)::nil) 263365669118842309261237752510635123964) :: 
+        (Pock_certif 535891737757285083698263 3 ((29771763208738060205459, 1)::(2,1)::nil) 1) ::
+         (Pock_certif 29771763208738060205459 2 ((2141, 1)::(1867, 1)::(7, 1)::(2,1)::nil) 17474375) ::
+         (Pock_certif 22187633823577 7 ((13, 2)::(3, 3)::(2,3)::nil) 22167) ::
+         (Proof_certif 2141 prime2141) ::
+         (Proof_certif 1867 prime1867) ::
+         (Proof_certif 13 prime13) ::
+         (Proof_certif 7 prime7) ::
+         (Proof_certif 3 prime3) ::
+         (Proof_certif 2 prime2) ::
+          nil.
+
+Definition check_cert1 := test_Certif cert1.
+(* Eval compute in "Checking primality of 2453592460649055756812450508556009475577084379843351664172069410531995758325371349410079350684102193 (100 digits)". *)
+(* Time Eval vm_compute in check_cert1. *)
+
+
+Definition cert2 :=
+         (Pock_certif 5351956038121333109794470473803140209428240474621443000490827925245658234802043104136048237347232839 7 ((7931077303135578295706501, 1)::(807509, 1)::(23071, 1)::(2,1)::nil) 83825513627931379579640353334701292) ::
+        (Pock_certif 7931077303135578295706501 2 ((94477, 1)::(19, 1)::(5, 2)::(2,2)::nil) 53011245) ::
+         (Pock_certif 807509 2 ((53, 1)::(2,2)::nil) 416) ::
+         (Pock_certif 94477 2 ((7873, 1)::(2,2)::nil) 1) ::
+         (Proof_certif 23071 prime23071) ::
+         (Proof_certif 7873 prime7873) ::
+         (Proof_certif 53 prime53) ::
+         (Proof_certif 19 prime19) ::
+         (Proof_certif 5 prime5) ::
+         (Proof_certif 2 prime2) ::
+          nil.
+
+Definition check_cert2 := test_Certif cert2.
+(* Eval compute in "Checking primality of 5351956038121333109794470473803140209428240474621443000490827925245658234802043104136048237347232839 (100 digits)". *)
+(* Time Eval vm_compute in check_cert2. *)
+
+
+Definition cert3 :=
+         (Pock_certif 5156668690509008564394179574550331202149987474724297759354684344612323405888046576355302595612624991 3 ((1064619103664925607325345484869851719496771558974058884015408678407183477, 1)::(2,1)::nil) 1) ::
+        (Pock_certif 1064619103664925607325345484869851719496771558974058884015408678407183477 2 ((3912194362405668030913307804243, 1)::(2,2)::nil) 26551391883318726506260350984158) ::
+         (Pock_certif 3912194362405668030913307804243 2 ((369180882757, 1)::(2,1)::nil) 949924248164) ::
+         (Pock_certif 369180882757 6 ((3, 7)::(2,2)::nil) 1388) ::
+         (Proof_certif 3 prime3) ::
+         (Proof_certif 2 prime2) ::
+          nil.
+
+Definition check_cert3 := test_Certif cert3.
+(* Eval compute in "Checking primality of 5156668690509008564394179574550331202149987474724297759354684344612323405888046576355302595612624991 (100 digits)". *)
+(* Time Eval vm_compute in check_cert3. *)
+(* Extraction "ocaml_prime3" check_cert3. *)
+
+
+Definition cert4 :=
+         (Pock_certif 4563975913455889091356468710155013974880832493315598107353834542502587892695693300925853265435622357 2 ((616868944230556873267, 1)::(35974457, 1)::(15383, 1)::(2,2)::nil) 2510617228410479161890451128591679) ::
+        (Pock_certif 616868944230556873267 2 ((66797, 1)::(1069, 1)::(2,1)::nil) 242273896) ::
+         (Pock_certif 35974457 3 ((569, 1)::(2,3)::nil) 1) ::
+         (Pock_certif 66797 2 ((16699, 1)::(2,2)::nil) 1) ::
+         (Proof_certif 16699 prime16699) ::
+         (Proof_certif 15383 prime15383) ::
+         (Proof_certif 1069 prime1069) ::
+         (Proof_certif 569 prime569) ::
+         (Proof_certif 2 prime2) ::
+          nil.
+
+
+Definition check_cert4 := test_Certif cert4.
+(* Eval compute in "Checking primality of 4563975913455889091356468710155013974880832493315598107353834542502587892695693300925853265435622357 (100 digits)". *)
+(* Time Eval vm_compute in check_cert4. *)

benchmarks/lib/stack_machine.v

@@ -0,0 +1,175 @@
+(* Occam's razor, program computing with different number representations: N,nat,PrimInt *)
+
+Require Import Nat Arith String List Uint63 BinNat ZArith.
+Import ListNotations.
+
+Inductive id : Type :=
+| Id: string -> id.
+
+Definition beq_id (a b: id) : bool :=
+  match a, b with
+  | Id a', Id b' => if string_dec a' b' then true else false
+  end.
+
+Definition total_map (A: Type) := id -> A.
+
+Definition t_empty {A: Type} (v: A) : total_map A :=
+  fun (_ : id) => v.
+
+Definition t_update {A: Type} (m: total_map A) (k: id) (v: A) : total_map A :=
+  fun (x : id) => if beq_id k x then v else m x.
+
+Class Numeric A : Type :=
+  {
+    plus : A -> A -> A ;
+    minus : A -> A -> A ;
+    mult : A -> A -> A ;
+    zero : A ;
+  }.
+
+#[export] Instance NumericNat : Numeric nat :=
+  {
+    plus := Nat.add ;
+    minus := Nat.sub ;
+    mult := Nat.mul ;
+    zero := 0
+  }.
+
+#[export] Instance NumericBinNat : Numeric N :=
+  {
+    plus := fun x y => (x + y)%N ;
+    minus := fun x y => (x - y)%N ;
+    mult := fun x y => (x * y)%N ;
+    zero := 0%N
+  }.
+
+#[export] Instance NumericPrimInt : Numeric int :=
+  {
+    plus := fun x y => (x + y)%uint63 ;
+    minus := fun x y => (x - y)%uint63 ;
+    mult := fun x y => (x * y)%uint63 ;
+    zero := 0%uint63
+  }.
+
+Definition state {A} `{Numeric A} := total_map A.
+
+Inductive aexp {A} `{Numeric A} : Type :=
+  | ANum : A -> aexp
+  | AId : id -> aexp
+  | APlus : aexp -> aexp -> aexp
+  | AMinus : aexp -> aexp -> aexp
+| AMult : aexp -> aexp -> aexp.
+
+Fixpoint aeval {A} `{Numeric A} (st : state) (a : aexp) : A :=
+  match a with
+  | ANum n => n
+  | AId x => st x
+  | APlus a1 a2 => plus (aeval st a1) (aeval st a2)
+  | AMinus a1 a2  => minus (aeval st a1) (aeval st a2)
+  | AMult a1 a2 => mult (aeval st a1) (aeval st a2)
+  end.
+
+Definition aeval' {A} `{Numeric A} :=
+  aeval (t_empty zero).
+
+
+Inductive sinstr {A} `{Numeric A} : Type :=
+| SPush : A -> sinstr
+| SLoad : id -> sinstr
+| SPlus : sinstr
+| SMinus : sinstr
+| SMult : sinstr.
+
+Fixpoint s_compile {A} `{Numeric A} (e : aexp) : list sinstr :=
+  match e with
+  | ANum x => [SPush x]
+  | AId k => [SLoad k]
+  | APlus a1 a2 => (s_compile a1) ++ (s_compile a2) ++ [SPlus]
+  | AMinus a1 a2 => (s_compile a1) ++ (s_compile a2) ++ [SMinus]
+  | AMult a1 a2 => (s_compile a1) ++ (s_compile a2) ++ [SMult]
+  end.
+
+Fixpoint s_execute {A} `{Numeric A} (st : state) (stack : list A)
+                   (prog : list sinstr)
+                 : list A :=
+  match prog with
+  | [] => stack
+  | (SPush n) :: prog' => s_execute st (n :: stack) prog'
+  | (SLoad k) :: prog' => s_execute st ((st k) :: stack) prog'
+  | SPlus :: prog' => s_execute st ((plus (hd zero (tl stack)) (hd zero stack)) :: (tl (tl stack)))
+                                prog'
+  | SMinus :: prog' => s_execute st ((minus (hd zero (tl stack)) (hd zero stack)) :: (tl (tl stack)))
+                                prog'
+  | SMult :: prog' => s_execute st ((mult (hd zero (tl stack)) (hd zero stack)) :: (tl (tl stack)))
+                                prog'
+  end.
+
+Definition s_execute' {A} `{Numeric A} :=
+  s_execute (t_empty zero) [].
+
+Lemma s_execute_app {A} `{Numeric A}: forall st stack si1 si2,
+  s_execute st stack (si1 ++ si2) =
+  s_execute st (s_execute st stack si1) si2.
+Proof.
+  intros.
+  generalize dependent st.
+  generalize dependent stack.
+  generalize dependent si2.
+  induction si1; intros.
+  - reflexivity.
+  - destruct a; simpl; apply IHsi1.
+Qed.
+
+Lemma s_compile_append {A} `{Numeric A}: forall st stack e,
+  s_execute st stack (s_compile e) =
+  (aeval st e) :: stack.
+Proof.
+  intros.
+  generalize dependent st.
+  generalize dependent stack.
+  induction e; simpl; intros;
+    try reflexivity;
+    repeat rewrite s_execute_app;
+    rewrite IHe1; rewrite IHe2;
+    reflexivity.
+Qed.
+
+Theorem s_compile_correct {A} `{Numeric A} : forall (st : state) (e : aexp),
+  s_execute st [] (s_compile e) = [ aeval st e ].
+Proof.
+  intros.
+  apply s_compile_append.
+Qed.
+
+Fixpoint gauss_sum_aexp_nat n :=
+  match n with
+  | 0 => ANum 0
+  | S n' => APlus (ANum n) (gauss_sum_aexp_nat n')
+  end.
+
+Fixpoint gauss_sum_aexp_N_aux (guard : nat) (n : N) :=
+  match guard with
+  | O => ANum 0%N
+  | S g' => APlus (ANum n) (gauss_sum_aexp_N_aux g' (n - 1)%N)
+  end.
+
+Definition gauss_sum_aexp_N (n : N) :=
+  gauss_sum_aexp_N_aux (N.to_nat n) n.
+
+Fixpoint gauss_sum_aexp_PrimInt_aux (guard : nat) (n : int) :=
+  match guard with
+  | O => ANum 0%uint63
+  | S g' => APlus (ANum n) (gauss_sum_aexp_PrimInt_aux g' (n - 1)%uint63)
+  end.
+
+Definition gauss_sum_aexp_PrimInt (n : int) :=
+  gauss_sum_aexp_PrimInt_aux (Z.to_nat (Uint63.to_Z n)) n.
+
+Definition gauss_sum_sintrs_nat (n : nat) :=
+  s_compile (gauss_sum_aexp_nat n).
+
+Definition gauss_sum_sintrs_N (n : N) :=
+  s_compile (gauss_sum_aexp_N n).
+
+Definition gauss_sum_sintrs_PrimInt (n : int) :=
+  s_compile (gauss_sum_aexp_PrimInt n).