Skip to content
Permalink

Comparing changes

Choose two branches to see what’s changed or to start a new pull request. If you need to, you can also or learn more about diff comparisons.

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also . Learn more about diff comparisons here.
base repository: IBM/FormalML
Failed to load repositories. Confirm that selected base ref is valid, then try again.
Loading
base: ITP2022
Choose a base ref
...
head repository: IBM/FormalML
Failed to load repositories. Confirm that selected head ref is valid, then try again.
Loading
compare: master
Choose a head ref
Loading
Showing with 80,912 additions and 3,825 deletions.
  1. +42 −29 .github/workflows/build.yml
  2. +1 −1 Dockerfile
  3. +8 −3 Formal_ML.opam
  4. +24 −4 Makefile.coq_modules
  5. +1 −0 README.md
  6. +1 −1 _CoqProject
  7. +6 −1 coq/CertRL/LM/README.md
  8. +1 −2 coq/CertRL/LM/lax_milgram.v
  9. +13 −13 coq/CertRL/finite_time.v
  10. +52 −31 coq/CertRL/mdp.v
  11. +5 −5 coq/CertRL/mdp_turtle.v
  12. +15 −2 coq/CertRL/pmf_monad.v
  13. +58 −30 coq/CertRL/pmf_prob.v
  14. +164 −11 coq/CertRL/qvalues.v
  15. +3,455 −0 coq/FHE/arith.v
  16. +5,286 −0 coq/FHE/encode.v
  17. +764 −0 coq/FHE/encrypt.v
  18. +885 −0 coq/FHE/nth_root.v
  19. +3,325 −0 coq/FHE/polyinterp.v
  20. +3,070 −0 coq/FHE/zp_prim_root.v
  21. +4 −4 coq/NeuralNetworks/DefinedFunctions.v
  22. +85 −53 coq/NeuralNetworks/derivlemmas.v
  23. +280 −8 coq/ProbTheory/Almost.v
  24. +48 −48 coq/ProbTheory/BorelSigmaAlgebra.v
  25. +2,595 −282 coq/ProbTheory/ConditionalExpectation.v
  26. +258 −109 coq/ProbTheory/DiscreteProbSpace.v
  27. +278 −17 coq/ProbTheory/Dynkin.v
  28. +134 −4 coq/ProbTheory/Event.v
  29. +547 −39 coq/ProbTheory/Expectation.v
  30. +138 −0 coq/ProbTheory/FunctionsToReal.v
  31. +2 −2 coq/ProbTheory/Gaussian.v
  32. +326 −0 coq/ProbTheory/Independence.v
  33. +118 −658 coq/ProbTheory/Martingale.v
  34. +3,763 −0 coq/ProbTheory/MartingaleConvergence.v
  35. +1,523 −0 coq/ProbTheory/MartingaleStopped.v
  36. +596 −33 coq/ProbTheory/Measures.v
  37. +481 −50 coq/ProbTheory/ProbSpace.v
  38. +8,254 −14 coq/ProbTheory/ProductSpace.v
  39. +2 −2 coq/ProbTheory/ProductSpaceDep.v
  40. +1,001 −151 coq/ProbTheory/RandomVariable.v
  41. +373 −13 coq/ProbTheory/RandomVariableFinite.v
  42. +156 −6 coq/ProbTheory/RandomVariableL2.v
  43. +3 −3 coq/ProbTheory/RandomVariableLinf.v
  44. +17 −17 coq/ProbTheory/RandomVariableLpNat.v
  45. +24 −29 coq/ProbTheory/RandomVariableLpR.v
  46. +611 −36 coq/ProbTheory/RbarExpectation.v
  47. +1,140 −135 coq/ProbTheory/RealRandomVariable.v
  48. +472 −2 coq/ProbTheory/RealVectorHilbert.v
  49. +1,109 −40 coq/ProbTheory/SigmaAlgebras.v
  50. +516 −27 coq/ProbTheory/SimpleExpectation.v
  51. +3 −3 coq/ProbTheory/VectorConditionalExpectation.v
  52. +674 −6 coq/ProbTheory/VectorRandomVariable.v
  53. +909 −0 coq/QLearn/Bellman.v
  54. +1,723 −194 coq/QLearn/Dvoretzky.v
  55. +11,973 −0 coq/QLearn/Tsitsiklis.v
  56. +362 −36 coq/QLearn/infprod.v
  57. +7,583 −0 coq/QLearn/jaakkola_vector.v
  58. +343 −0 coq/QLearn/lim_add.v
  59. +279 −433 coq/QLearn/qlearn.v
  60. +593 −0 coq/QLearn/qlearn_aux.v
  61. +3,768 −0 coq/QLearn/qlearn_redux.v
  62. +3,802 −258 coq/QLearn/slln.v
  63. +297 −50 coq/QLearn/sumtest.v
  64. +424 −0 coq/QLearn/uniform_converge.v
  65. +1,201 −380 coq/QLearn/vecslln.v
  66. +2 −2 coq/lib_utils/LibUtilsAssoc.v
  67. +3 −3 coq/lib_utils/LibUtilsDigits.v
  68. +1 −1 coq/lib_utils/LibUtilsGroupByDomain.v
  69. +11 −18 coq/lib_utils/LibUtilsStringAdd.v
  70. +26 −2 coq/utils/BasicUtils.v
  71. +139 −0 coq/utils/ClassicUtils.v
  72. +1 −1 coq/utils/CoquelicotAdd.v
  73. +1,014 −3 coq/utils/DVector.v
  74. +26 −0 coq/utils/ELim_Seq.v
  75. +0 −403 coq/utils/Finite.v
  76. +819 −0 coq/utils/FiniteType.v
  77. +475 −0 coq/utils/FiniteTypeVector.v
  78. +7 −0 coq/utils/Isomorphism.v
  79. +124 −3 coq/utils/ListAdd.v
  80. +2 −3 coq/utils/PairEncoding.v
  81. +1 −1 coq/utils/Quotient.v
  82. +887 −30 coq/utils/RbarAdd.v
  83. +1,401 −58 coq/utils/RealAdd.v
  84. +4 −9 coq/utils/Sums.v
  85. +2 −0 coq/utils/Utils.v
  86. +2 −12 coq/utils/Vector.v
  87. +1 −1 coq/utils/nvector.v
71 changes: 42 additions & 29 deletions .github/workflows/build.yml
Original file line number Diff line number Diff line change
@@ -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
2 changes: 1 addition & 1 deletion Dockerfile
Original file line number Diff line number Diff line change
@@ -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"
11 changes: 8 additions & 3 deletions Formal_ML.opam
Original file line number Diff line number Diff line change
@@ -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"
28 changes: 24 additions & 4 deletions Makefile.coq_modules
Original file line number Diff line number Diff line change
@@ -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

1 change: 1 addition & 0 deletions README.md
Original file line number Diff line number Diff line change
@@ -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

2 changes: 1 addition & 1 deletion _CoqProject
Original file line number Diff line number Diff line change
@@ -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"
7 changes: 6 additions & 1 deletion coq/CertRL/LM/README.md
Original file line number Diff line number Diff line change
@@ -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.
3 changes: 1 addition & 2 deletions coq/CertRL/LM/lax_milgram.v
Original file line number Diff line number Diff line change
@@ -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.
26 changes: 13 additions & 13 deletions coq/CertRL/finite_time.v
Original file line number Diff line number Diff line change
@@ -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.
Loading