.github/workflows/build.yml

@@ -10,34 +10,47 @@ jobs:
     runs-on: ubuntu-latest  # container actions require GNU/Linux
     strategy:
       matrix:
-        coq_version:
-          - '8.12.2'
-#          - '8.14.0'
-        ocaml_version:
-          - '4.07-flambda'
+        coq_container:
+#        - coqorg/coq:8.12.2
+#        - coqorg/coq:8.16.1-ocaml-4.13.1-flambda
+        - coqorg/coq:8.18.0-ocaml-4.13.1-flambda
+    container:
+      image: ${{ matrix.coq_container }}
+      options: --user root
     steps:
-      - uses: actions/checkout@v2
-        with:
-          persist-credentials: false
-      - uses: coq-community/docker-coq-action@v1
-        with:
-          opam_file: 'Formal_ML.opam'
-          coq_version: ${{ matrix.coq_version }}
-          ocaml_version: ${{ matrix.ocaml_version }}
-#          export: 'OPAMWITHTEST OPAMWITHDOC'
-          export: 'OPAMWITHDOC'
-          after_script: |
-            sudo cp -a $(opam config var Formal_ML:build)/documentation .
-        env:
-          OPAMWITHDOC: 'true'
+    - uses: actions/checkout@v4
+      with:
+        persist-credentials: false
+    - name: Fix permissions
+      run: chown -R 1000 .
+    - name: ls
+      run: ls -la .
+    - name: Install Opam dependencies
+      run: su coq -c 'eval $(opam env) && opam install --deps-only --with-test --with-doc -y -j 2 ./Formal_ML.opam'
+    - name: Build using Make
+      run: su coq -c 'eval $(opam env) && make -kj 2'
+    - name: Build documentation
+      run: su coq -c 'eval $(opam env) && make -kj 2 doc'
+
+#       - uses: coq-community/docker-coq-action@v1
+#         with:
+#           opam_file: 'Formal_ML.opam'
+#           coq_version: ${{ matrix.coq_version }}
+#           ocaml_version: ${{ matrix.ocaml_version }}
+# #          export: 'OPAMWITHTEST OPAMWITHDOC'
+#           export: 'OPAMWITHDOC'
+#           after_script: |
+#             sudo cp -a $(opam config var Formal_ML:build)/documentation .
+#         env:
+#           OPAMWITHDOC: 'true'
 #          OPAMWITHTEST: 'true'
-      - if: ${{ github.event_name == 'push' && github.ref == 'refs/heads/master' }}
-        name: deploy documentation
-        uses: JamesIves/github-pages-deploy-action@3.7.1
-        with:
-          ACCESS_TOKEN: ${{ secrets.ACCESS_TOKEN }}
-          REPOSITORY_NAME: FormalML/FormalML.github.io # the target repository
-          TARGET_FOLDER: main/documentation # target directory
-          BRANCH: main # The branch the action should deploy to.
-          FOLDER: documentation # The folder the action should deploy.
-          CLEAN: true # Automatically remove deleted files from the deploy branch
+      # - if: ${{ github.event_name == 'push' && github.ref == 'refs/heads/master' }}
+      #   name: deploy documentation
+      #   uses: JamesIves/github-pages-deploy-action@3.7.1
+      #   with:
+      #     ACCESS_TOKEN: ${{ secrets.ACCESS_TOKEN }}
+      #     REPOSITORY_NAME: FormalML/FormalML.github.io # the target repository
+      #     TARGET_FOLDER: main/documentation # target directory
+      #     BRANCH: main # The branch the action should deploy to.
+      #     FOLDER: documentation # The folder the action should deploy.
+      #     CLEAN: true # Automatically remove deleted files from the deploy branch

Dockerfile

@@ -1,4 +1,4 @@
-ARG coq_image="coqorg/coq:8.11.2"
+ARG coq_image="coqorg/coq:8.12.2"
 FROM ${coq_image}
 
 MAINTAINER Avi Shinnar "shinnar@us.ibm.com"

Formal_ML.opam

@@ -4,16 +4,21 @@ version: "~dev"
 synopsis: "Exploring formal verification for symbolic neural networks"
 maintainer: "Avi Shinnar <shinnar@us.ibm.com>"
 authors: "Avi Shinnar <shinnar@us.ibm.com>"
+license: "Apache-2.0"
 homepage: "https://github.com/ibm/formalml"
 bug-reports: "https://github.com/ibm/formalml/issues"
 depends: [
   "ocaml" {>= "4.07.0"}
   "coq" {>= "8.12.1"}
   "coq-mathcomp-ssreflect"
-  "coq-coquelicot"
+  "coq-mathcomp-algebra"
+  "coq-mathcomp-algebra-tactics"
+  "coq-mathcomp-real-closed"
+  "coq-mathcomp-analysis" {< "1.0.0"}
+  "coq-coquelicot" {= "3.3.1" }
   "coq-flocq" {>= "4.0.0" }
-  "coq-interval"
-  "coq-ext-lib"
+  "coq-interval" {>= "4.8.0"}
+  "coq-ext-lib" {<= "1.0.0"}
   "ocamlbuild"
   "base64"
   "menhir"

Makefile.coq_modules

@@ -27,13 +27,15 @@ ELFIC_UTILS	= R_compl check_sub_structure compatible continuous_linear_map fixed
 
 UTILS = BasicUtils \
 	Assoc \
+	ClassicUtils \
 	CoquelicotAdd \
 	ELim_Seq \
 	ExtrFloatishIEEE \
 	improper_integrals \
 	Isomorphism \
 	ListAdd \
-	Finite \
+	FiniteType \
+	FiniteTypeVector \
 	NumberIso \
 	PairEncoding \
 	Quotient \
@@ -68,14 +70,16 @@ CERTRL = pmf_monad \
 	mdp \
 	mdp_turtle \
 	finite_time \
-	cond_expt
+	cond_expt \
+	pmf_prob
 
 PROB_THEORY = \
 	Almost \
 	BorelSigmaAlgebra \
 	DiscreteProbSpace \
 	Dynkin \
 	Event \
+	Independence \
 	ProbSpace \
 	FunctionsToReal \
 	Measures \
@@ -96,19 +100,34 @@ PROB_THEORY = \
 	SigmaAlgebras \
 	VectorRandomVariable \
 	Martingale \
+	MartingaleConvergence \
+	MartingaleStopped \
 	Gaussian \
 	ProductSpace \
 	ProductSpaceDep
 
 
 QLEARN = \
 	Dvoretzky \
+	Bellman \
+	qlearn_aux \
 	qlearn \
-    infprod \
+	qlearn_redux \
+	infprod \
 	sumtest \
    	slln \
-	vecslln
+	vecslln \
+	uniform_converge \
+	lim_add \
+	Tsitsiklis \
+	jaakkola_vector
 
+FHE = \
+      nth_root \
+      encode \
+      encrypt \
+      zp_prim_root \
+      arith
 
 MODULES =  $(addprefix lib_utils/,$(QCERT_LIB_UTILS)) \
 	$(addprefix CertRL/LM/,$(ELFIC_UTILS)) \
@@ -117,5 +136,6 @@ MODULES =  $(addprefix lib_utils/,$(QCERT_LIB_UTILS)) \
 	$(addprefix ProbTheory/,$(PROB_THEORY)) \
 	$(addprefix CertRL/,$(CERTRL)) \
 	$(addprefix QLearn/,$(QLEARN)) \
+	$(addprefix FHE/,$(FHE)) \
 	API
 

README.md

@@ -4,6 +4,7 @@
  This repository contains
   - a partial formalization of key results from https://arxiv.org/abs/1804.07795
   - The CertRL library as reported in https://arxiv.org/abs/2009.11403
+  - a formalization of Dvoretzky's stochastic approximation theorem as reported in https://arxiv.org/abs/2202.05959
 
  ## Getting Started
 

_CoqProject

@@ -1 +1 @@
--R coq FormalML -arg -set -arg "Warnings=+default,-ambiguous-path,-typechecker,-ssr-search-moved,-deprecated"
+-R coq FormalML -arg -set -arg "Warnings=+default,-ambiguous-path,-coercions,-hiding-delimiting-key,-overwriting-delimiting-key,-redundant-canonical-projection,-typechecker,-ssr-search-moved,-deprecated,-notation-overridden"

coq/CertRL/LM/README.md

@@ -1,5 +1,10 @@
 This subdirectory contains the [`elfic`](https://www.lri.fr/~sboldo/elfic/) library, which provided a [formal proof of the Lax-Milgram theorem](https://hal.inria.fr/hal-01391578/document). 
 
-We use this library as a dependency for our project, with permission from the authors. 
 In particular, we use the Banach Fixed Point theorem as proven in the file `fixed_point.v`. 
 
+We use this library as a dependency for our project.  For historical
+reasons, it is currently copied into this repository.  Now that an
+official gitlab repository is available at
+https://depot.lipn.univ-paris13.fr/mayero/coq-num-analysis/ and there
+are plans on an OPAM release, this code will likely be replaced with
+a normal dependency in the future.

coq/CertRL/LM/lax_milgram.v

@@ -1005,12 +1005,11 @@ intro x; field.
 repeat (rewrite Hx1 in HU0).
 rewrite Rmult_comm.
 trivial.
-absurd (norm u0 = 0).
+try revert HU0.
 apply Rgt_not_eq.
 apply Rlt_gt.
 apply norm_gt_0.
 trivial.
-trivial.
 apply norm_ge_0.
 simpl.
 apply is_finite_correct in Hfin.

coq/CertRL/finite_time.v

@@ -1,5 +1,5 @@
 Require Import Reals Coq.Lists.List Coquelicot.Series Coquelicot.Hierarchy Coquelicot.SF_seq.
-Require Import pmf_monad mdp Permutation fixed_point Finite LibUtils. 
+Require Import pmf_monad mdp Permutation fixed_point FiniteType LibUtils. 
 Require Import Sums Coq.Reals.ROrderedType.
 Require Import micromega.Lra.
 Require Import micromega.Lia.
@@ -323,7 +323,7 @@ Qed.
 
 Theorem Rmax_list_dec_rule_split n p :
   (n > 0)%nat ->
-  let l' := all_lists_upto (@elms _ (dec_rule_finite M)) n in
+  let l' := all_lists_upto (@fin_elms _ (dec_rule_finite M)) n in
   Max_{ l' } (fun '(h,t) => ltv_fin p (h::t)) =
   Max_{ map fst l' } (fun h => Max_{map snd l'} (fun t => ltv_fin p (h::t)))  
 .
@@ -333,19 +333,19 @@ Proof.
   - apply all_lists_upto_non_nil; trivial.
     destruct (dec_rule_finite M); simpl.
     generalize (nonempty_dec_rule M); intros e.
-    destruct elms; [| congruence].
-    elim (finite e).
+    destruct fin_elms; [| congruence].
+    elim (fin_finite e).
   - apply all_lists_upto_prod.
 Qed.
 
 (* Optimal value function for a time n MDP. *)
 Definition max_ltv_fin (n:nat) p :=
-  let l' := all_lists_upto (@elms _ (dec_rule_finite M)) n in
+  let l' := all_lists_upto (@fin_elms _ (dec_rule_finite M)) n in
   Max_{ l' } (fun '(h,t) => ltv_fin p (h::t)).
 
 Theorem max_ltv_corec p n:
   max_ltv_fin (S (S n)) p =
-  Max_{(@elms _ (dec_rule_finite M))}
+  Max_{(@fin_elms _ (dec_rule_finite M))}
       (fun h => expt_value p (step_expt_reward h) +
              γ * max_ltv_fin (S n) (Pmf_bind p (fun s0 => (t s0 (h s0))))).
 Proof.
@@ -359,7 +359,7 @@ Proof.
   rewrite all_lists_upto_snds.
   rewrite map_map.
   transitivity (
-  (Max_{ all_lists_upto elms (S n)}
+  (Max_{ all_lists_upto fin_elms (S n)}
    (fun '(h, tl) => expt_value p (step_expt_reward a) +
                 γ * ltv_fin (Pmf_bind p (fun s0 : state M => t s0 (a s0))) (h :: tl)))).
   - f_equal.
@@ -376,20 +376,20 @@ Proof.
                                  | pair h tl =>
                                    ltv_fin (@Pmf_bind (state M) (state M) p (fun s0 : state M => @t M s0 (a s0)))
                                            (@cons (dec_rule M) h tl)
-                                 end) (@all_lists_upto (dec_rule M) (@elms (dec_rule M) (dec_rule_finite M)) (S n)))
+                                 end) (@all_lists_upto (dec_rule M) (@fin_elms (dec_rule M) (dec_rule_finite M)) (S n)))
                   (expt_value p (step_expt_reward a))); intros HH2.
 
     case_eq ( map
             (fun a0 : dec_rule M * list (dec_rule M) =>
              γ * (let (h, tl) := a0 in ltv_fin (Pmf_bind p (fun s0 : state M => t s0 (a s0))) (h :: tl)))
-            (all_lists_upto elms (S n))); intros.
-    + generalize (all_lists_upto_non_nil (@elms _ (dec_rule_finite M)) (S n)); intros HH3.
-      destruct ((all_lists_upto (@elms _ (dec_rule_finite M)) (S n))).
+            (all_lists_upto fin_elms (S n))); intros.
+    + generalize (all_lists_upto_non_nil (@fin_elms _ (dec_rule_finite M)) (S n)); intros HH3.
+      destruct ((all_lists_upto (@fin_elms _ (dec_rule_finite M)) (S n))).
       * elim HH3; trivial.
         destruct (dec_rule_finite M); simpl.
         generalize (nonempty_dec_rule M); intros e.
-        destruct elms; [| congruence].
-        elim (finite e).
+        destruct fin_elms; [| congruence].
+        elim (fin_finite e).
         lia.
       * simpl in H; congruence.
     + rewrite H in HH2.