diff --git a/Makefile.coq b/Makefile.coq new file mode 100644 index 0000000..ff2715a --- /dev/null +++ b/Makefile.coq @@ -0,0 +1,989 @@ +########################################################################## +## # The Coq Proof Assistant / The Coq Development Team ## +## v # Copyright INRIA, CNRS and contributors ## +## /dev/null 2>/dev/null; echo $$?)) +STDTIME?=command time -f $(TIMEFMT) +else +ifeq (0,$(shell gtime -f "" true >/dev/null 2>/dev/null; echo $$?)) +STDTIME?=gtime -f $(TIMEFMT) +else +STDTIME?=command time +endif +endif +else +STDTIME?=command time -f $(TIMEFMT) +endif + +COQBIN?= +ifneq (,$(COQBIN)) +# add an ending / +COQBIN:=$(COQBIN)/ +endif + +# Coq binaries +COQC ?= "$(COQBIN)coqc" +COQTOP ?= "$(COQBIN)coqtop" +COQCHK ?= "$(COQBIN)coqchk" +COQNATIVE ?= "$(COQBIN)coqnative" +COQDEP ?= "$(COQBIN)coqdep" +COQDOC ?= "$(COQBIN)coqdoc" +COQPP ?= "$(COQBIN)coqpp" +COQMKFILE ?= "$(COQBIN)coq_makefile" +OCAMLLIBDEP ?= "$(COQBIN)ocamllibdep" + +# Timing scripts +COQMAKE_ONE_TIME_FILE ?= "$(COQCORELIB)/tools/make-one-time-file.py" +COQMAKE_BOTH_TIME_FILES ?= "$(COQCORELIB)/tools/make-both-time-files.py" +COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQCORELIB)/tools/make-both-single-timing-files.py" +BEFORE ?= +AFTER ?= + +# OCaml binaries +CAMLC ?= "$(OCAMLFIND)" ocamlc -c +CAMLOPTC ?= "$(OCAMLFIND)" opt -c +CAMLLINK ?= "$(OCAMLFIND)" ocamlc -linkall +CAMLOPTLINK ?= "$(OCAMLFIND)" opt -linkall +CAMLDOC ?= "$(OCAMLFIND)" ocamldoc +CAMLDEP ?= "$(OCAMLFIND)" ocamldep -slash -ml-synonym .mlpack + +# DESTDIR is prepended to all installation paths +DESTDIR ?= + +# Debug builds, typically -g to OCaml, -debug to Coq. +CAMLDEBUG ?= +COQDEBUG ?= + +# Extra packages to be linked in (as in findlib -package) +CAMLPKGS ?= +FINDLIBPKGS = -package coq-core.plugins.ltac $(CAMLPKGS) + +# Option for making timing files +TIMING?= +# Option for changing sorting of timing output file +TIMING_SORT_BY ?= auto +# Option for changing the fuzz parameter on the output file +TIMING_FUZZ ?= 0 +# Option for changing whether to use real or user time for timing tables +TIMING_REAL?= +# Option for including the memory column(s) +TIMING_INCLUDE_MEM?= +# Option for sorting by the memory column +TIMING_SORT_BY_MEM?= +# Output file names for timed builds +TIME_OF_BUILD_FILE ?= time-of-build.log +TIME_OF_BUILD_BEFORE_FILE ?= time-of-build-before.log +TIME_OF_BUILD_AFTER_FILE ?= time-of-build-after.log +TIME_OF_PRETTY_BUILD_FILE ?= time-of-build-pretty.log +TIME_OF_PRETTY_BOTH_BUILD_FILE ?= time-of-build-both.log +TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line + +TGTS ?= + +# Retro compatibility (DESTDIR is standard on Unix, DSTROOT is not) +ifdef DSTROOT +DESTDIR := $(DSTROOT) +endif + +# Substitution of the path by appending $(DESTDIR) if needed. +# The variable $(COQMF_WINDRIVE) can be needed for Cygwin environments. +windrive_path = $(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(1)),$(1)) +destination_path = $(if $(DESTDIR),$(DESTDIR)/$(call windrive_path,$(1)),$(1)) + +# Installation paths of libraries and documentation. +COQLIBINSTALL ?= $(call destination_path,$(COQLIB)/user-contrib) +COQDOCINSTALL ?= $(call destination_path,$(DOCDIR)/coq/user-contrib) +COQPLUGININSTALL ?= $(call destination_path,$(COQCORELIB)/..) +COQTOPINSTALL ?= $(call destination_path,$(COQLIB)/toploop) # FIXME: Unused variable? + +# findlib files installation +FINDLIBPREINST= mkdir -p "$(COQPLUGININSTALL)/" +FINDLIBDESTDIR= -destdir "$(COQPLUGININSTALL)/" + +# we need to move out of sight $(METAFILE) otherwise findlib thinks the +# package is already installed +findlib_install = \ + $(HIDE)if [ "$(METAFILE)" ]; then \ + $(FINDLIBPREINST) && \ + mv "$(METAFILE)" "$(METAFILE).skip" ; \ + "$(OCAMLFIND)" install $(2) $(FINDLIBDESTDIR) $(FINDLIBPACKAGE) $(1); \ + rc=$$?; \ + mv "$(METAFILE).skip" "$(METAFILE)"; \ + exit $$rc; \ + fi +findlib_remove = \ + $(HIDE)if [ ! -z "$(METAFILE)" ]; then\ + "$(OCAMLFIND)" remove $(FINDLIBDESTDIR) $(FINDLIBPACKAGE); \ + fi + + +########## End of parameters ################################################## +# What follows may be relevant to you only if you need to +# extend this Makefile. If so, look for 'Extension point' here and +# put in Makefile.coq.local double colon rules accordingly. +# E.g. to perform some work after the all target completes you can write +# +# post-all:: +# echo "All done!" +# +# in Makefile.coq.local +# +############################################################################### + + + + +# Flags ####################################################################### +# +# We define a bunch of variables combining the parameters. +# To add additional flags to coq, coqchk or coqdoc, set the +# {COQ,COQCHK,COQDOC}EXTRAFLAGS variable to whatever you want to add. +# To overwrite the default choice and set your own flags entirely, set the +# {COQ,COQCHK,COQDOC}FLAGS variable. + +SHOW := $(if $(VERBOSE),@true "",@echo "") +HIDE := $(if $(VERBOSE),,@) + +TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) + +OPT?= + +# The DYNOBJ and DYNLIB variables are used by "coqdep -dyndep var" in .v.d +ifeq '$(OPT)' '-byte' +USEBYTE:=true +DYNOBJ:=.cma +DYNLIB:=.cma +else +USEBYTE:= +DYNOBJ:=.cmxs +DYNLIB:=.cmxs +endif + +# these variables are meant to be overridden if you want to add *extra* flags +COQEXTRAFLAGS?= +COQCHKEXTRAFLAGS?= +COQDOCEXTRAFLAGS?= + +# Find the last argument of the form "-native-compiler FLAG" +COQUSERNATIVEFLAG:=$(strip \ +$(subst -native-compiler-,,\ +$(lastword \ +$(filter -native-compiler-%,\ +$(subst -native-compiler ,-native-compiler-,\ +$(strip $(COQEXTRAFLAGS))))))) + +COQFILTEREDEXTRAFLAGS:=$(strip \ +$(filter-out -native-compiler-%,\ +$(subst -native-compiler ,-native-compiler-,\ +$(strip $(COQEXTRAFLAGS))))) + +COQACTUALNATIVEFLAG:=$(lastword $(COQMF_COQ_NATIVE_COMPILER_DEFAULT) $(COQMF_COQPROJECTNATIVEFLAG) $(COQUSERNATIVEFLAG)) + +ifeq '$(COQACTUALNATIVEFLAG)' 'yes' + COQNATIVEFLAG="-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" + COQDONATIVE="yes" +else +ifeq '$(COQACTUALNATIVEFLAG)' 'ondemand' + COQNATIVEFLAG="-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" + COQDONATIVE="no" +else + COQNATIVEFLAG="-w" "-deprecated-native-compiler-option" "-native-compiler" "no" + COQDONATIVE="no" +endif +endif + +# these flags do NOT contain the libraries, to make them easier to overwrite +COQFLAGS?=-q $(OTHERFLAGS) $(COQFILTEREDEXTRAFLAGS) $(COQNATIVEFLAG) +COQCHKFLAGS?=-silent -o $(COQCHKEXTRAFLAGS) +COQDOCFLAGS?=-interpolate -utf8 $(COQDOCEXTRAFLAGS) + +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.18.0 + +# COQ_SRC_SUBDIRS is for user-overriding, usually to add +# `user-contrib/Foo` to the includes, we keep COQCORE_SRC_SUBDIRS for +# Coq's own core libraries, which should be replaced by ocamlfind +# options at some point. +COQ_SRC_SUBDIRS?= +COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)/$(d)") + +CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) +# ocamldoc fails with unknown argument otherwise +CAMLDOCFLAGS:=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS))) +CAMLFLAGS+=$(OCAMLWARN) + +ifneq (,$(TIMING)) + ifeq (after,$(TIMING)) + TIMING_EXT=after-timing + else + ifeq (before,$(TIMING)) + TIMING_EXT=before-timing + else + TIMING_EXT=timing + endif + endif + TIMING_ARG=-time-file $<.$(TIMING_EXT) +else + TIMING_ARG= +endif + +# Files ####################################################################### +# +# We here define a bunch of variables about the files being part of the +# Coq project in order to ease the writing of build target and build rules + +VDFILE := .Makefile.coq.d + +ALLSRCFILES := \ + $(MLGFILES) \ + $(MLFILES) \ + $(MLPACKFILES) \ + $(MLLIBFILES) \ + $(MLIFILES) + +# helpers +vo_to_obj = $(addsuffix .o,\ + $(filter-out Warning: Error:,\ + $(shell $(COQTOP) -q -noinit -batch -quiet -print-mod-uid $(1)))) +strip_dotslash = $(patsubst ./%,%,$(1)) + +# without this we get undefined variables in the expansion for the +# targets of the [deprecated,use-mllib-or-mlpack] rule +with_undef = $(if $(filter-out undefined, $(origin $(1))),$($(1))) + +VO = vo +VOS = vos + +VOFILES = $(VFILES:.v=.$(VO)) +GLOBFILES = $(VFILES:.v=.glob) +HTMLFILES = $(VFILES:.v=.html) +GHTMLFILES = $(VFILES:.v=.g.html) +BEAUTYFILES = $(addsuffix .beautified,$(VFILES)) +TEXFILES = $(VFILES:.v=.tex) +GTEXFILES = $(VFILES:.v=.g.tex) +CMOFILES = \ + $(MLGFILES:.mlg=.cmo) \ + $(MLFILES:.ml=.cmo) \ + $(MLPACKFILES:.mlpack=.cmo) +CMXFILES = $(CMOFILES:.cmo=.cmx) +OFILES = $(CMXFILES:.cmx=.o) +CMAFILES = $(MLLIBFILES:.mllib=.cma) $(MLPACKFILES:.mlpack=.cma) +CMXAFILES = $(CMAFILES:.cma=.cmxa) +CMIFILES = \ + $(CMOFILES:.cmo=.cmi) \ + $(MLIFILES:.mli=.cmi) +# the /if/ is because old _CoqProject did not list a .ml(pack|lib) but just +# a .mlg file +CMXSFILES = \ + $(MLPACKFILES:.mlpack=.cmxs) \ + $(CMXAFILES:.cmxa=.cmxs) \ + $(if $(MLPACKFILES)$(CMXAFILES),,\ + $(MLGFILES:.mlg=.cmxs) $(MLFILES:.ml=.cmxs)) + +# files that are packed into a plugin (no extension) +PACKEDFILES = \ + $(call strip_dotslash, \ + $(foreach lib, \ + $(call strip_dotslash, \ + $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES)),$(call with_undef,$(lib)))) +# files that are archived into a .cma (mllib) +LIBEDFILES = \ + $(call strip_dotslash, \ + $(foreach lib, \ + $(call strip_dotslash, \ + $(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES)),$(call with_undef,$(lib)))) +CMIFILESTOINSTALL = $(filter-out $(addsuffix .cmi,$(PACKEDFILES)),$(CMIFILES)) +CMOFILESTOINSTALL = $(filter-out $(addsuffix .cmo,$(PACKEDFILES)),$(CMOFILES)) +OBJFILES = $(call vo_to_obj,$(VOFILES)) +ALLNATIVEFILES = \ + $(OBJFILES:.o=.cmi) \ + $(OBJFILES:.o=.cmx) \ + $(OBJFILES:.o=.cmxs) +FINDLIBPACKAGE=$(patsubst .%,%,$(suffix $(METAFILE))) + +# trick: wildcard filters out non-existing files, so that `install` doesn't show +# warnings and `clean` doesn't pass to rm a list of files that is too long for +# the shell. +NATIVEFILES = $(wildcard $(ALLNATIVEFILES)) +FILESTOINSTALL = \ + $(VOFILES) \ + $(VFILES) \ + $(GLOBFILES) \ + $(NATIVEFILES) \ + $(CMXSFILES) # to be removed when we remove legacy loading +FINDLIBFILESTOINSTALL = \ + $(CMIFILESTOINSTALL) +ifeq '$(HASNATDYNLINK)' 'true' +DO_NATDYNLINK = yes +FINDLIBFILESTOINSTALL += $(CMXSFILES) $(CMXAFILES) $(CMOFILESTOINSTALL:.cmo=.cmx) +else +DO_NATDYNLINK = +endif + +ALLDFILES = $(addsuffix .d,$(ALLSRCFILES)) $(VDFILE) + +# Compilation targets ######################################################### + +all: + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all +.PHONY: all + +all.timing.diff: + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all.timing.diff TIME_OF_PRETTY_BUILD_EXTRA_FILES="" + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all +.PHONY: all.timing.diff + +ifeq (0,$(TIMING_REAL)) +TIMING_REAL_ARG := +TIMING_USER_ARG := --user +else +ifeq (1,$(TIMING_REAL)) +TIMING_REAL_ARG := --real +TIMING_USER_ARG := +else +TIMING_REAL_ARG := +TIMING_USER_ARG := +endif +endif + +ifeq (0,$(TIMING_INCLUDE_MEM)) +TIMING_INCLUDE_MEM_ARG := --no-include-mem +else +TIMING_INCLUDE_MEM_ARG := +endif + +ifeq (1,$(TIMING_SORT_BY_MEM)) +TIMING_SORT_BY_MEM_ARG := --sort-by-mem +else +TIMING_SORT_BY_MEM_ARG := +endif + +make-pretty-timed-before:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_BEFORE_FILE) +make-pretty-timed-after:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_AFTER_FILE) +make-pretty-timed make-pretty-timed-before make-pretty-timed-after:: + $(HIDE)rm -f pretty-timed-success.ok + $(HIDE)($(MAKE) --no-print-directory -f "$(PARENT)" $(TGTS) TIMED=1 2>&1 && touch pretty-timed-success.ok) | tee -a $(TIME_OF_BUILD_FILE) + $(HIDE)rm pretty-timed-success.ok # must not be -f; must fail if the touch failed +print-pretty-timed:: + $(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIMING_INCLUDE_MEM_ARG) $(TIMING_SORT_BY_MEM_ARG) $(TIMING_REAL_ARG) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) +print-pretty-timed-diff:: + $(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIMING_INCLUDE_MEM_ARG) $(TIMING_SORT_BY_MEM_ARG) $(TIMING_REAL_ARG) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) +ifeq (,$(BEFORE)) +print-pretty-single-time-diff:: + @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing' + $(HIDE)false +else +ifeq (,$(AFTER)) +print-pretty-single-time-diff:: + @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing' + $(HIDE)false +else +print-pretty-single-time-diff:: + $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --fuzz=$(TIMING_FUZZ) --sort-by=$(TIMING_SORT_BY) $(TIMING_USER_ARG) $(AFTER) $(BEFORE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) +endif +endif +pretty-timed: + $(HIDE)$(MAKE) --no-print-directory -f "$(PARENT)" make-pretty-timed + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-timed +.PHONY: pretty-timed make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff + +# Extension points for actions to be performed before/after the all target +pre-all:: + @# Extension point + $(HIDE)if [ "$(COQMAKEFILE_VERSION)" != "$(COQ_VERSION)" ]; then\ + echo "W: This Makefile was generated by Coq $(COQMAKEFILE_VERSION)";\ + echo "W: while the current Coq version is $(COQ_VERSION)";\ + fi +.PHONY: pre-all + +post-all:: + @# Extension point +.PHONY: post-all + +real-all: $(VOFILES) $(if $(USEBYTE),bytefiles,optfiles) +.PHONY: real-all + +real-all.timing.diff: $(VOFILES:.vo=.v.timing.diff) +.PHONY: real-all.timing.diff + +bytefiles: $(CMOFILES) $(CMAFILES) +.PHONY: bytefiles + +optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES)) +.PHONY: optfiles + +# FIXME, see Ralf's bugreport +# quick is deprecated, now renamed vio +vio: $(VOFILES:.vo=.vio) +.PHONY: vio +quick: vio + $(warning "'make quick' is deprecated, use 'make vio' or consider using 'vos' files") +.PHONY: quick + +vio2vo: + $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \ + -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio) +.PHONY: vio2vo + +# quick2vo is undocumented +quick2vo: + $(HIDE)make -j $(J) vio + $(HIDE)VIOFILES=$$(for vofile in $(VOFILES); do \ + viofile="$$(echo "$$vofile" | sed "s/\.vo$$/.vio/")"; \ + if [ "$$vofile" -ot "$$viofile" -o ! -e "$$vofile" ]; then printf "$$viofile "; fi; \ + done); \ + echo "VIO2VO: $$VIOFILES"; \ + if [ -n "$$VIOFILES" ]; then \ + $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -schedule-vio2vo $(J) $$VIOFILES; \ + fi +.PHONY: quick2vo + +checkproofs: + $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \ + -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio) +.PHONY: checkproofs + +vos: $(VOFILES:%.vo=%.vos) +.PHONY: vos + +vok: $(VOFILES:%.vo=%.vok) +.PHONY: vok + +validate: $(VOFILES) + $(TIMER) $(COQCHK) $(COQCHKFLAGS) $(COQLIBS_NOML) $^ +.PHONY: validate + +only: $(TGTS) +.PHONY: only + +# Documentation targets ####################################################### + +html: $(GLOBFILES) $(VFILES) + $(SHOW)'COQDOC -d html $(GAL)' + $(HIDE)mkdir -p html + $(HIDE)$(COQDOC) \ + -toc $(COQDOCFLAGS) -html $(GAL) $(COQDOCLIBS) -d html $(VFILES) + +mlihtml: $(MLIFILES:.mli=.cmi) + $(SHOW)'CAMLDOC -d $@' + $(HIDE)mkdir $@ || rm -rf $@/* + $(HIDE)$(CAMLDOC) -html \ + -d $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES) $(FINDLIBPKGS) + +all-mli.tex: $(MLIFILES:.mli=.cmi) + $(SHOW)'CAMLDOC -latex $@' + $(HIDE)$(CAMLDOC) -latex \ + -o $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES) $(FINDLIBPKGS) + +all.ps: $(VFILES) + $(SHOW)'COQDOC -ps $(GAL)' + $(HIDE)$(COQDOC) \ + -toc $(COQDOCFLAGS) -ps $(GAL) $(COQDOCLIBS) \ + -o $@ `$(COQDEP) -sort $(VFILES)` + +all.pdf: $(VFILES) + $(SHOW)'COQDOC -pdf $(GAL)' + $(HIDE)$(COQDOC) \ + -toc $(COQDOCFLAGS) -pdf $(GAL) $(COQDOCLIBS) \ + -o $@ `$(COQDEP) -sort $(VFILES)` + +# FIXME: not quite right, since the output name is different +gallinahtml: GAL=-g +gallinahtml: html + +all-gal.ps: GAL=-g +all-gal.ps: all.ps + +all-gal.pdf: GAL=-g +all-gal.pdf: all.pdf + +# ? +beautify: $(BEAUTYFILES) + for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done + @echo 'Do not do "make clean" until you are sure that everything went well!' + @echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/' +.PHONY: beautify + +# Installation targets ######################################################## +# +# There rules can be extended in Makefile.coq.local +# Extensions can't assume when they run. + +# We use $(file) to avoid generating a very long command string to pass to the shell +# (cf https://coq.zulipchat.com/#narrow/stream/250632-Coq-Platform-devs-.26-users/topic/Strange.20command.20length.20limit.20on.20Linux) +# However Apple ships old make which doesn't have $(file) so we need a fallback +$(file >.hasfile,1) +HASFILE:=$(shell if [ -e .hasfile ]; then echo 1; rm .hasfile; fi) + +MKFILESTOINSTALL= $(if $(HASFILE),$(file >.filestoinstall,$(FILESTOINSTALL)),\ + $(shell rm -f .filestoinstall) \ + $(foreach x,$(FILESTOINSTALL),$(shell printf '%s\n' "$x" >> .filestoinstall))) + +# findlib needs the package to not be installed, so we remove it before +# installing it (see the call to findlib_remove) +install: META + @$(MKFILESTOINSTALL) + $(HIDE)code=0; for f in $$(cat .filestoinstall); do\ + if ! [ -f "$$f" ]; then >&2 echo $$f does not exist; code=1; fi \ + done; exit $$code + $(HIDE)for f in $$(cat .filestoinstall); do\ + df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\ + if [ "$$?" != "0" -o -z "$$df" ]; then\ + echo SKIP "$$f" since it has no logical path;\ + else\ + install -d "$(COQLIBINSTALL)/$$df" &&\ + install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\ + echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\ + fi;\ + done + $(call findlib_remove) + $(call findlib_install, META $(FINDLIBFILESTOINSTALL)) + $(HIDE)$(MAKE) install-extra -f "$(SELF)" + @rm -f .filestoinstall +install-extra:: + @# Extension point +.PHONY: install install-extra + +META: $(METAFILE) + $(HIDE)if [ "$(METAFILE)" ]; then \ + cat "$(METAFILE)" | grep -v 'directory.*=.*' > META; \ + fi + +install-byte: + $(call findlib_install, $(CMAFILES) $(CMOFILESTOINSTALL), -add) + +install-doc:: html mlihtml + @# Extension point + $(HIDE)install -d "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html" + $(HIDE)for i in html/*; do \ + dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\ + install -m 0644 "$$i" "$$dest";\ + echo INSTALL "$$i" "$$dest";\ + done + $(HIDE)install -d \ + "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml" + $(HIDE)for i in mlihtml/*; do \ + dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\ + install -m 0644 "$$i" "$$dest";\ + echo INSTALL "$$i" "$$dest";\ + done +.PHONY: install-doc + +uninstall:: + @# Extension point + @$(MKFILESTOINSTALL) + $(call findlib_remove) + $(HIDE)for f in $$(cat .filestoinstall); do \ + df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\ + instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\ + rm -f "$$instf" &&\ + echo RM "$$instf" ;\ + done + $(HIDE)for f in $$(cat .filestoinstall); do \ + df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\ + echo RMDIR "$(COQLIBINSTALL)/$$df/" &&\ + (rmdir "$(COQLIBINSTALL)/$$df/" 2>/dev/null || true); \ + done + @rm -f .filestoinstall + +.PHONY: uninstall + +uninstall-doc:: + @# Extension point + $(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html' + $(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html" + $(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml' + $(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml" + $(HIDE) rmdir "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/" || true +.PHONY: uninstall-doc + +# Cleaning #################################################################### +# +# There rules can be extended in Makefile.coq.local +# Extensions can't assume when they run. + +clean:: + @# Extension point + $(SHOW)'CLEAN' + $(HIDE)rm -f $(CMOFILES) + $(HIDE)rm -f $(CMIFILES) + $(HIDE)rm -f $(CMAFILES) + $(HIDE)rm -f $(CMXFILES) + $(HIDE)rm -f $(CMXAFILES) + $(HIDE)rm -f $(CMXSFILES) + $(HIDE)rm -f $(OFILES) + $(HIDE)rm -f $(CMXAFILES:.cmxa=.a) + $(HIDE)rm -f $(MLGFILES:.mlg=.ml) + $(HIDE)rm -f $(CMXFILES:.cmx=.cmt) + $(HIDE)rm -f $(MLIFILES:.mli=.cmti) + $(HIDE)rm -f $(ALLDFILES) + $(HIDE)rm -f $(NATIVEFILES) + $(HIDE)find . -name .coq-native -type d -empty -delete + $(HIDE)rm -f $(VOFILES) + $(HIDE)rm -f $(VOFILES:.vo=.vio) + $(HIDE)rm -f $(VOFILES:.vo=.vos) + $(HIDE)rm -f $(VOFILES:.vo=.vok) + $(HIDE)rm -f $(BEAUTYFILES) $(VFILES:=.old) + $(HIDE)rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob all-mli.tex + $(HIDE)rm -f $(VFILES:.v=.glob) + $(HIDE)rm -f $(VFILES:.v=.tex) + $(HIDE)rm -f $(VFILES:.v=.g.tex) + $(HIDE)rm -f pretty-timed-success.ok + $(HIDE)rm -f META + $(HIDE)rm -rf html mlihtml +.PHONY: clean + +cleanall:: clean + @# Extension point + $(SHOW)'CLEAN *.aux *.timing' + $(HIDE)rm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux) + $(HIDE)rm -f $(TIME_OF_BUILD_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) + $(HIDE)rm -f $(VOFILES:.vo=.v.timing) + $(HIDE)rm -f $(VOFILES:.vo=.v.before-timing) + $(HIDE)rm -f $(VOFILES:.vo=.v.after-timing) + $(HIDE)rm -f $(VOFILES:.vo=.v.timing.diff) + $(HIDE)rm -f .lia.cache .nia.cache +.PHONY: cleanall + +archclean:: + @# Extension point + $(SHOW)'CLEAN *.cmx *.o' + $(HIDE)rm -f $(NATIVEFILES) + $(HIDE)rm -f $(CMOFILES:%.cmo=%.cmx) +.PHONY: archclean + + +# Compilation rules ########################################################### + +$(MLIFILES:.mli=.cmi): %.cmi: %.mli + $(SHOW)'CAMLC -c $<' + $(HIDE)$(TIMER) $(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) $< + +$(MLGFILES:.mlg=.ml): %.ml: %.mlg + $(SHOW)'COQPP $<' + $(HIDE)$(COQPP) $< + +# Stupid hack around a deficient syntax: we cannot concatenate two expansions +$(filter %.cmo, $(MLFILES:.ml=.cmo) $(MLGFILES:.mlg=.cmo)): %.cmo: %.ml + $(SHOW)'CAMLC -c $<' + $(HIDE)$(TIMER) $(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) $< + +# Same hack +$(filter %.cmx, $(MLFILES:.ml=.cmx) $(MLGFILES:.mlg=.cmx)): %.cmx: %.ml + $(SHOW)'CAMLOPT -c $(FOR_PACK) $<' + $(HIDE)$(TIMER) $(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) $(FOR_PACK) $< + + +$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa + $(SHOW)'CAMLOPT -shared -o $@' + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) \ + -shared -o $@ $< + +$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib + $(SHOW)'CAMLC -a -o $@' + $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $^ + +$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib + $(SHOW)'CAMLOPT -a -o $@' + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $^ + + +$(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmxa + $(SHOW)'CAMLOPT -shared -o $@' + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) \ + -shared -o $@ $< + +$(MLPACKFILES:.mlpack=.cmxa): %.cmxa: %.cmx | %.mlpack + $(SHOW)'CAMLOPT -a -o $@' + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $< + +$(MLPACKFILES:.mlpack=.cma): %.cma: %.cmo | %.mlpack + $(SHOW)'CAMLC -a -o $@' + $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $^ + +$(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack + $(SHOW)'CAMLC -pack -o $@' + $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -pack -o $@ $^ + +$(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack + $(SHOW)'CAMLOPT -pack -o $@' + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -pack -o $@ $^ + +# This rule is for _CoqProject with no .mllib nor .mlpack +$(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(MLGFILES:.mlg=.cmxs)): %.cmxs: %.cmx + $(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@' + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) \ + -shared -o $@ $< + +# can't make +# https://www.gnu.org/software/make/manual/make.html#Static-Pattern +# work with multiple target rules +# so use eval in a loop instead +# with grouped targets https://www.gnu.org/software/make/manual/make.html#Multiple-Targets +# if available (GNU Make >= 4.3) +ifneq (,$(filter grouped-target,$(.FEATURES))) +define globvorule= + +# take care to $$ variables using $< etc + $(1).vo $(1).glob &: $(1).v | $(VDFILE) + $(SHOW)COQC $(1).v + $(HIDE)$$(TIMER) $(COQC) $(COQDEBUG) $$(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $(1).v +ifeq ($(COQDONATIVE), "yes") + $(SHOW)COQNATIVE $(1).vo + $(HIDE)$(call TIMER,$(1).vo.native) $(COQNATIVE) $(COQLIBS) $(1).vo +endif + +endef +else + +$(VOFILES): %.vo: %.v | $(VDFILE) + $(SHOW)COQC $< + $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $< +ifeq ($(COQDONATIVE), "yes") + $(SHOW)COQNATIVE $@ + $(HIDE)$(call TIMER,$@.native) $(COQNATIVE) $(COQLIBS) $@ +endif + +# this is broken :( todo fix if we ever find a solution that doesn't need grouped targets +$(GLOBFILES): %.glob: %.v + $(SHOW)'COQC $< (for .glob)' + $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< + +endif + +$(foreach vfile,$(VFILES:.v=),$(eval $(call globvorule,$(vfile)))) + +$(VFILES:.v=.vio): %.vio: %.v + $(SHOW)COQC -vio $< + $(HIDE)$(TIMER) $(COQC) -vio $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< + +$(VFILES:.v=.vos): %.vos: %.v + $(SHOW)COQC -vos $< + $(HIDE)$(TIMER) $(COQC) -vos $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< + +$(VFILES:.v=.vok): %.vok: %.v + $(SHOW)COQC -vok $< + $(HIDE)$(TIMER) $(COQC) -vok $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< + +$(addsuffix .timing.diff,$(VFILES)): %.timing.diff : %.before-timing %.after-timing + $(SHOW)PYTHON TIMING-DIFF $*.{before,after}-timing + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-single-time-diff BEFORE=$*.before-timing AFTER=$*.after-timing TIME_OF_PRETTY_BUILD_FILE="$@" + +$(BEAUTYFILES): %.v.beautified: %.v + $(SHOW)'BEAUTIFY $<' + $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -beautify $< + +$(TEXFILES): %.tex: %.v + $(SHOW)'COQDOC -latex $<' + $(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@ + +$(GTEXFILES): %.g.tex: %.v + $(SHOW)'COQDOC -latex -g $<' + $(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@ + +$(HTMLFILES): %.html: %.v %.glob + $(SHOW)'COQDOC -html $<' + $(HIDE)$(COQDOC) $(COQDOCFLAGS) -html $< -o $@ + +$(GHTMLFILES): %.g.html: %.v %.glob + $(SHOW)'COQDOC -html -g $<' + $(HIDE)$(COQDOC) $(COQDOCFLAGS) -html -g $< -o $@ + +# Dependency files ############################################################ + +ifndef MAKECMDGOALS + -include $(ALLDFILES) +else + ifneq ($(filter-out archclean clean cleanall printenv make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff,$(MAKECMDGOALS)),) + -include $(ALLDFILES) + endif +endif + +.SECONDARY: $(ALLDFILES) + +redir_if_ok = > "$@" || ( RV=$$?; rm -f "$@"; exit $$RV ) + +GENMLFILES:=$(MLGFILES:.mlg=.ml) +$(addsuffix .d,$(ALLSRCFILES)): $(GENMLFILES) + +$(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli + $(SHOW)'CAMLDEP $<' + $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) + +$(addsuffix .d,$(MLGFILES)): %.mlg.d: %.ml + $(SHOW)'CAMLDEP $<' + $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) + +$(addsuffix .d,$(MLFILES)): %.ml.d: %.ml + $(SHOW)'CAMLDEP $<' + $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) + +$(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib + $(SHOW)'OCAMLLIBDEP $<' + $(HIDE)$(OCAMLLIBDEP) -c $(OCAMLLIBS) "$<" $(redir_if_ok) + +$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack + $(SHOW)'OCAMLLIBDEP $<' + $(HIDE)$(OCAMLLIBDEP) -c $(OCAMLLIBS) "$<" $(redir_if_ok) + +# If this makefile is created using a _CoqProject we have coqdep get +# options from it. This avoids argument length limits for pathological +# projects. Note that extra options might be on the command line. +VDFILE_FLAGS:=$(if _CoqProject,-f _CoqProject,) $(CMDLINE_COQLIBS) $(CMDLINE_VFILES) + +$(VDFILE): _CoqProject $(VFILES) + $(SHOW)'COQDEP VFILES' + $(HIDE)$(COQDEP) $(if $(strip $(METAFILE)),-m "$(METAFILE)") -vos -dyndep var $(VDFILE_FLAGS) $(redir_if_ok) + +# Misc ######################################################################## + +byte: + $(HIDE)$(MAKE) all "OPT:=-byte" -f "$(SELF)" +.PHONY: byte + +opt: + $(HIDE)$(MAKE) all "OPT:=-opt" -f "$(SELF)" +.PHONY: opt + +# This is deprecated. To extend this makefile use +# extension points and Makefile.coq.local +printenv:: + $(warning printenv is deprecated) + $(warning write extensions in Makefile.coq.local or include Makefile.coq.conf) + @echo 'COQLIB = $(COQLIB)' + @echo 'COQCORELIB = $(COQCORELIB)' + @echo 'DOCDIR = $(DOCDIR)' + @echo 'OCAMLFIND = $(OCAMLFIND)' + @echo 'HASNATDYNLINK = $(HASNATDYNLINK)' + @echo 'SRC_SUBDIRS = $(SRC_SUBDIRS)' + @echo 'COQ_SRC_SUBDIRS = $(COQ_SRC_SUBDIRS)' + @echo 'COQCORE_SRC_SUBDIRS = $(COQCORE_SRC_SUBDIRS)' + @echo 'OCAMLFIND = $(OCAMLFIND)' + @echo 'PP = $(PP)' + @echo 'COQFLAGS = $(COQFLAGS)' + @echo 'COQLIB = $(COQLIBS)' + @echo 'COQLIBINSTALL = $(COQLIBINSTALL)' + @echo 'COQDOCINSTALL = $(COQDOCINSTALL)' +.PHONY: printenv + +# Generate a .merlin file. If you need to append directives to this +# file you can extend the merlin-hook target in Makefile.coq.local +.merlin: + $(SHOW)'FILL .merlin' + $(HIDE)echo 'FLG $(COQMF_CAMLFLAGS)' > .merlin + $(HIDE)echo 'B $(COQCORELIB)' >> .merlin + $(HIDE)echo 'S $(COQCORELIB)' >> .merlin + $(HIDE)$(foreach d,$(COQCORE_SRC_SUBDIRS), \ + echo 'B $(COQCORELIB)$(d)' >> .merlin;) + $(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \ + echo 'S $(COQLIB)$(d)' >> .merlin;) + $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'B $(d)' >> .merlin;) + $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'S $(d)' >> .merlin;) + $(HIDE)$(MAKE) merlin-hook -f "$(SELF)" +.PHONY: merlin + +merlin-hook:: + @# Extension point +.PHONY: merlin-hook + +# prints all variables +debug: + $(foreach v,\ + $(sort $(filter-out $(INITIAL_VARS) INITIAL_VARS,\ + $(.VARIABLES))),\ + $(info $(v) = $($(v)))) +.PHONY: debug + +.DEFAULT_GOAL := all + +# Users can create Makefile.coq.local-late to hook into double-colon rules +# or add other needed Makefile code, using defined +# variables if necessary. +-include Makefile.coq.local-late + +# Local Variables: +# mode: makefile-gmake +# End: diff --git a/Makefile.coq.conf b/Makefile.coq.conf new file mode 100644 index 0000000..ca4c561 --- /dev/null +++ b/Makefile.coq.conf @@ -0,0 +1,71 @@ +# This configuration file was generated by running: +# coq_makefile -f _CoqProject -o Makefile.coq + +COQBIN?= +ifneq (,$(COQBIN)) +# add an ending / +COQBIN:=$(COQBIN)/ +endif +COQMKFILE ?= "$(COQBIN)coq_makefile" + +############################################################################### +# # +# Project files. # +# # +############################################################################### + +COQMF_CMDLINE_VFILES := +COQMF_SOURCES := $(shell $(COQMKFILE) -sources-of -f _CoqProject $(COQMF_CMDLINE_VFILES)) +COQMF_VFILES := $(filter %.v, $(COQMF_SOURCES)) +COQMF_MLIFILES := $(filter %.mli, $(COQMF_SOURCES)) +COQMF_MLFILES := $(filter %.ml, $(COQMF_SOURCES)) +COQMF_MLGFILES := $(filter %.mlg, $(COQMF_SOURCES)) +COQMF_MLPACKFILES := $(filter %.mlpack, $(COQMF_SOURCES)) +COQMF_MLLIBFILES := $(filter %.mllib, $(COQMF_SOURCES)) +COQMF_METAFILE = + +############################################################################### +# # +# Path directives (-I, -R, -Q). # +# # +############################################################################### + +COQMF_OCAMLLIBS = +COQMF_SRC_SUBDIRS = +COQMF_COQLIBS = -Q theories vRATLS +COQMF_COQLIBS_NOML = -Q theories vRATLS +COQMF_CMDLINE_COQLIBS = + +############################################################################### +# # +# Coq configuration. # +# # +############################################################################### + +COQMF_COQLIB=/nix/store/51fqh0dc78ggqqy0vp6hhkq242jprpqf-coq-8.18.0/lib/coq/ +COQMF_COQCORELIB=/nix/store/51fqh0dc78ggqqy0vp6hhkq242jprpqf-coq-8.18.0/lib/coq/../coq-core/ +COQMF_DOCDIR=/nix/store/51fqh0dc78ggqqy0vp6hhkq242jprpqf-coq-8.18.0/share/doc/ +COQMF_OCAMLFIND=/nix/store/jfhjb6dlfsyvybzrcr432d7hlvpqngvv-ocaml4.14.2-findlib-1.9.6/bin/ocamlfind +COQMF_CAMLFLAGS=-thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 +COQMF_WARN=-warn-error +a-3 +COQMF_HASNATDYNLINK=true +COQMF_COQ_SRC_SUBDIRS=boot config lib clib kernel library engine pretyping interp gramlib parsing proofs tactics toplevel printing ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/funind plugins/ltac plugins/ltac2 plugins/micromega plugins/nsatz plugins/ring plugins/rtauto plugins/ssr plugins/ssrmatching plugins/syntax +COQMF_COQ_NATIVE_COMPILER_DEFAULT=no +COQMF_WINDRIVE= + +############################################################################### +# # +# Native compiler. # +# # +############################################################################### + +COQMF_COQPROJECTNATIVEFLAG = + +############################################################################### +# # +# Extra variables. # +# # +############################################################################### + +COQMF_OTHERFLAGS = +COQMF_INSTALLCOQDOCROOT = vRATLS diff --git a/theories/examples/Conversions.v b/theories/examples/Conversions.v index b6c4cfc..f1e7091 100644 --- a/theories/examples/Conversions.v +++ b/theories/examples/Conversions.v @@ -54,7 +54,6 @@ Proof. rewrite /intoZp'/fromZp => x. rewrite /eq_rect_r/eq_rect //=. case: x => m m_lt_p //=. - Check Zp_cast. case: (Zp_cast (p:=p) p_gt1); rewrite /Zp_trunc => Zp_eq_p //=. Fail rewrite Zp_eq_p. Abort. @@ -73,10 +72,6 @@ Definition intoZp'' (q:nat) : 'I_q.+2 -> 'Z_q.+2 := fun x => x. Definition z (q:nat) : 'Z_q -> 'Z_q.-2.+2 := fun x => x. Definition y (q:nat) : 'Z_q -> 'I_q.-2.+2 := fun x => x. -Check False_rect. -Check False_rec. -Check Bool.diff_false_true. - (* This fails because it requires a rewrite of [H]. *) Fail Definition into (q:nat) (H: (1 < q)%N) : 'I_q -> 'I_q.-2.+2 := match q with @@ -90,16 +85,12 @@ Definition into {q:nat} : (1 < q)%N -> 'I_q -> 'I_q.-2.+2 := | _ => fun H => False_rect _ (Bool.diff_false_true H) end. -Print into. - Definition into' {q:nat} : (1 < q)%N -> 'I_q -> 'I_q.-2.+2. Proof. case: q => //=. case => //=. Defined. -Print into'. - Definition into'' {q:nat} : (1 < q)%N -> 'I_q -> 'I_q.-2.+2. Proof. case: q. @@ -109,8 +100,6 @@ Proof. + move => n H. exact id. Defined. -Print into''. - (** Lesson learned Creating functions with tactics results in really complex terms. Those are hard to handle when using these functions in lemmas. diff --git a/theories/examples/More_props.v b/theories/examples/More_props.v new file mode 100644 index 0000000..c0124bf --- /dev/null +++ b/theories/examples/More_props.v @@ -0,0 +1,132 @@ +From Relational Require Import OrderEnrichedCategory GenericRulesSimple. + +Set Warnings "-notation-overridden,-ambiguous-paths". +From mathcomp Require Import all_ssreflect all_algebra reals distr realsum + fingroup.fingroup solvable.cyclic prime ssrnat ssreflect ssrfun ssrbool ssrnum + eqtype choice seq. +Set Warnings "notation-overridden,ambiguous-paths". + +From Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings + UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb UniformStateProb + pkg_core_definition choice_type pkg_composition pkg_rhl + Package Prelude RandomOracle. + +From Coq Require Import Utf8. +From extructures Require Import ord fset fmap. + +From Equations Require Import Equations. +Require Equations.Prop.DepElim. +Require Import Coq.Init.Logic. +Require Import List. + +Set Equations With UIP. + +(* +The paper: +https://web.archive.org/web/20220121005133id_/https://eprint.iacr.org/2019/779.pdf +*) + +(* + This is needed to make definitions with Equations transparent. + Otherwise they are opaque and code simplifications in the + proofs with [ssprove_code_simpl] does not resolve properly. + *) +Set Equations Transparent. + +Set Bullet Behavior "Strict Subproofs". +Set Default Goal Selector "!". +Set Primitive Projections. + +Import Num.Def. +Import Num.Theory. +Import Order.POrderTheory. + +From vRATLS Require Import examples.Signature. + +Import PackageNotation. + +Obligation Tactic := idtac. + + +Print Run_aux. + +(* TODO new run function needed: [evalState] *) +Fail Theorem CEO seed : + forall pk sk, + Some (pk,sk) = Run sampler KeyGen seed -> + forall msg sig, + Some sig = Run_aux sampler (Sign msg) (λ l, if l == sk_loc then Some sk else Some NSUnit) -> + forall pk', + Some true = Run_aux sampler (Verify sig msg) (λ l, if l == pk_loc then Some pk' else Some NSUnit) -> + pk = pk'. + +Fail Definition Sign_me : package Sig_locs_real Sig_ifce Sig_prot_ifce + := [package + #def #[sign_me] (msg : 'message) : 'pubkey × 'signature + { + #import {sig #[get_pk] : 'unit → 'pubkey } as get_pk ;; + #import {sig #[sign] : 'message → 'signature } as sign ;; + + pk ← get_pk tt ;; + sig ← sign msg ;; + + ret (pk, sig) + } + ]. + +Fail Definition Verify_me : package Sig_locs_real Sig_ifce Sig_prot_ifce + := [package + #def #[verify_me] (sig : 'signature) (msg : 'message) : 'pubkey × 'bool + { + #import {sig #[get_pk] : 'unit → 'pubkey } as get_pk ;; + #import {sig #[sign] : 'message → 'signature } as sign ;; + + pk ← get_pk tt ;; + b ← verify msg sig ;; + ret (pk, b) + } + ]. + + +Fail Theorem CEO seed seed': + forall pk pk' msg sig, + Some (pk , sig ) = Run sampler (Sign_me msg) seed -> + Some (pk', true) = Run sampler (Verify_me sig msg) seed -> + pk = pk'. + +(* The below version holds for [KeyGen] implementations + that dependent on the seed. + That is, we need an additional property for [KeyGen]: + [ + Some pk = Run sampler KeyGen seed -> + Some pk' = Run sampler KeyGen seed' -> + seed = seed' -> + pk = pk' + ] + *) +Fail Theorem CEO' seed seed': + forall pk pk' msg sig, + Some (pk , sig ) = Run sampler (Sign_me msg) seed -> + Some (pk', true) = Run sampler (Verify_me sig msg) seed' -> + pk = pk' -> + seed = seed'. +(* + The proof is by case on [seed == seed']. + The [true] case is straight-forward. + The [false] case leads to a contradiction in the hypotheses because + then [pk = pk'] does not hold anymore. + *) + + +Fail Theorem DEO seed seed': + forall pk pk' msg msg' sig, + Some (pk, sig ) = Run sampler (Sign_me msg) seed -> + Some (pk, true) = Run sampler (Verify_me sig msg') seed' -> + seed != seed' -> + pk = pk' ∧ msg = msg'. + +Theorem Consistency_verify: + forall pk seed sig msg r r', + Some (pk, r ) = Run sampler (Verify_me sig msg) seed' -> + Some (pk, r') = Run sampler (Verify_me sig msg) seed' -> + r = r'. diff --git a/theories/examples/RA.v b/theories/examples/RA.v index 847d08c..bab28aa 100644 --- a/theories/examples/RA.v +++ b/theories/examples/RA.v @@ -7,9 +7,9 @@ cryptography. It is like the version used on the RATLS paper. VERIFIER PROVER Generates a chal- lenge 'chal' - -----chal-----> + -----chal-----> Attestation - (using TPM) + (using TPM) <-----res------ Validity check of proof @@ -60,7 +60,7 @@ From vRATLS Require Import extructurespp.ord. From vRATLS Require Import extructurespp.fmap. From vRATLS Require Import extructurespp.fset. -Module Type RemoteAttestationParams (π2 : SignatureConstraints). +Module RemoteAttestationParams (π2 : SignatureParams). Import π2. @@ -68,21 +68,18 @@ Module Type RemoteAttestationParams (π2 : SignatureConstraints). Definition Attestation : choice_type := 'fin (mkpos pos_n). Definition chMessage : choice_type := 'fin (mkpos pos_n). - Parameter Challenge : finType. - Parameter Challenge_pos : Positive #|Challenge|. - #[local] Existing Instance Challenge_pos. - Definition chChallenge := 'fin #|Challenge|. End RemoteAttestationParams. Module Type RemoteAttestationAlgorithms (π1 : SignatureParams) (* TBD This is strange. The reason is because our code depends on signature scheme functions. *) - (π2 : SignatureConstraints) - (π3 : RemoteAttestationParams π2) - (KG : KeyGeneration π1 π2) - (Alg : SignatureAlgorithms π1 π2 KG). + (π2 : KeyGenParams π1) + (KGc : KeyGen_code π1 π2) + (* (Alg : SignatureAlgorithms π1 π2 KGc) *). - Import π1 π2 π3 KG Alg. + Module π3 := RemoteAttestationParams π1. + Import π1 π2 π3 KGc (* Alg *). + Import KGc.KGP (* Alg.KG *). Local Open Scope package_scope. @@ -93,7 +90,7 @@ Module Type RemoteAttestationAlgorithms Notation " 'attest " := Attestation (in custom pack_type at level 2). Definition state_loc : Location := ('state ; 9%N). - Definition attest_loc : Location := ('set (Signature × chMessage) ; 10%N). + Definition attest_loc : Location := ('set (chSignature × chMessage) ; 10%N). Definition verify_att : nat := 11. Definition attest : nat := 12. Definition get_pk_att : nat := 13. @@ -104,17 +101,19 @@ Module Type RemoteAttestationAlgorithms End RemoteAttestationAlgorithms. Module Type RemoteAttestationHash - (π1 : SignatureParams) - (π2 : SignatureConstraints) - (π3 : RemoteAttestationParams π2) - (KG : KeyGeneration π1 π2) - (Alg : SignatureAlgorithms π1 π2 KG) - (RAA : RemoteAttestationAlgorithms π1 π2 π3 KG Alg) - (SP : SignaturePrimitives π1 π2 KG Alg). + (π1 : SignatureParams) (* TBD This is strange. The reason is because our code depends on signature scheme functions. *) + (π2 : KeyGenParams π1) + (KGc : KeyGen_code π1 π2) + (Alg : SignatureAlgorithms π1 π2 KGc) + (RAA : RemoteAttestationAlgorithms π1 π2 KGc). + + Module π3 := RemoteAttestationParams π1. + Module SP := SignaturePrimitives π1 π2 KGc Alg. + Import π1 π2 π3 KGc Alg RAA SP. + Import KGc.KGP SP.KG. - Import π1 π2 π3 KG Alg RAA SP. - Definition attest_loc_long : Location := ('set (Signature × chState × chChallenge) ; 2%N). + Definition attest_loc_long : Location := ('set (chSignature × chState × chChallenge) ; 2%N). Definition Attestation_locs_real := fset [:: pk_loc ; sk_loc; state_loc ]. Definition Attestation_locs_ideal := Attestation_locs_real :|: fset [:: attest_loc_long ]. @@ -279,11 +278,32 @@ Module Type RemoteAttestationHash simplify_eq_rel x. all: ssprove_code_simpl. - simplify_linking. - ssprove_sync_eq. - ssprove_sync_eq. - ssprove_sync_eq => pk_loc. - eapply r_ret. - intuition eauto. + ssprove_code_simpl. + rewrite /cast_fun/eq_rect_r/eq_rect. + simplify_linking. + ssprove_code_simpl. + eapply rsame_head_alt_pre. + + -- pose xxx ( t : heap * heap) := match t with | (s₀, s₁) => s₀ = s₁ end. + apply (rpost_weaken_rule _ + (λ '(a₀, s₀) '(a₁, s₁), a₀ = a₁ /\ xxx (s₀, s₁) )). + --- apply (rpre_weaken_rule (λ '(s₀, s₁), xxx (s₀, s₁) )). + ---- eapply r_reflexivity_alt. + ----- instantiate (1:=Key_locs). destruct KeyGen. exact: prog_valid. + ----- move => l. unfold xxx. + rewrite /Key_locs => l_not_in_Key_locs. + unfold get_pre_cond. + intros s0 s1. intros h. rewrite h. reflexivity. + ----- move => l v l_not_in_Key_locs. + unfold xxx. unfold put_pre_cond. + intros s0 s1 h. rewrite h. reflexivity. + ---- unfold xxx. intros s0 s1 h. exact h. + --- intros a0 a1. destruct a0. destruct a1. split. + + destruct H. unfold xxx in H0. exact H0. + + destruct H. exact H. + -- intros a. destruct a. repeat ssprove_sync_eq. intros a1. apply r_ret. intros s0' s1' h. + split. ++ reflexivity. + ++ exact h. - destruct x. ssprove_swap_lhs 0. ssprove_sync_eq => state. @@ -370,7 +390,7 @@ Module Type RemoteAttestationHash Definition Att_ideal_locp_heap := Attestation_locs_ideal. Definition Aux_prim_ideal_heap := Comp_locs. - Definition attest_set := 'set (Signature × chState × chChallenge). + Definition attest_set := 'set (chSignature × chState × chChallenge). Definition sign_set := 'set ('signature × 'message). (* Normally, this would be located in a Functor. @@ -1198,22 +1218,45 @@ Module Type RemoteAttestationHash (λ '(b₀, s₀) '(b₁, s₁), b₀ = b₁ /\ full_heap_eq' (s₀,s₁))). 2:{ case => b₀ s₀; case => b₁ s₁. by [rewrite -/(full_heap_eq' (s₀,s₁))]. } - Fail ssprove_sync. - (* I have to reshape the precondition into: - [λ '(s0, s1), full_heap_eq' (s0, s1)] - *) - rewrite -(reshape_pair_id full_heap_eq'). - - (* TODO: This is simpler than below! Check it! *) - ssprove_sync. 2: apply (@l_in_lSet sk_loc). - 1: rewrite -fset1E fdisjoints1; auto_in_fset. - - ssprove_sync. 2: apply (@l_in_lSet pk_loc). - 1: rewrite -fset1E fdisjoints1; auto_in_fset. - - ssprove_sync. 2: apply (@l_in_lSet pk_loc). - 1: rewrite -fset1E fdisjoints1; auto_in_fset. - - move => a; by [apply r_ret]. + ssprove_code_simpl. + rewrite /cast_fun/eq_rect_r/eq_rect. + simplify_linking. + ssprove_code_simpl. + eapply rsame_head_alt_pre. + -- apply (rpost_weaken_rule _ + (λ '(a₀, s₀) '(a₁, s₁), a₀ = a₁ /\ full_heap_eq' (s₀, s₁) )). + ---- rewrite -(reshape_pair_id full_heap_eq'). + eapply r_reflexivity_alt. + ----- instantiate (1:=Key_locs). destruct KeyGen. exact: prog_valid. + ----- move => l. + rewrite /Key_locs. unfold Key_locs => l_not_in_Key_locs. (* Why does rewrite fail? *) + ssprove_invariant. + rewrite fset_cons. + rewrite fdisjointUl. + apply/andP. + split; + (( try rewrite -fset1E); rewrite fdisjoint1s; auto_in_fset). + ----- move => l v l_not_in_Key_locs. ssprove_invariant. + unfold Key_locs. + ssprove_invariant. + rewrite fset_cons. + rewrite fdisjointUl. + apply/andP. + split; + (( try rewrite -fset1E); rewrite fdisjoint1s; auto_in_fset). + ---- case => a0 s0; case => a1 s1. case => l r. by [split]. + -- intro a. + destruct a. + rewrite -(reshape_pair_id full_heap_eq'). + ssprove_sync. 2: apply (@l_in_lSet sk_loc). + 1: rewrite -fset1E fdisjoints1; auto_in_fset. + + ssprove_sync. 2: apply (@l_in_lSet pk_loc). + 1: rewrite -fset1E fdisjoints1; auto_in_fset. + ssprove_sync. 2: apply (@l_in_lSet pk_loc). + 1: rewrite -fset1E fdisjoints1; auto_in_fset. + + move => a; by [apply r_ret]. - ssprove_swap_rhs 0%N. sync_sig_att. 1: auto_in_fset. move => state. @@ -1221,7 +1264,7 @@ Module Type RemoteAttestationHash + ssprove_invariant. + move => state_loc. - (* I think this is from above and not needed anymore. + (* I think this is from above and not needed anymore. rewrite put_bind. rewrite [in X in ⊢ ⦃ _ ⦄ _ ≈ X ⦃ _ ⦄ ]put_bind. (* The below fails because the post condition is [b₀ = b₁ /\ pre (s₀, s₁)] @@ -1369,140 +1412,139 @@ Module Type RemoteAttestationHash - by []. Qed. - Lemma concat_3 : - fset [:: pk_loc; state_loc] - :|: (fset [:: pk_loc; sk_loc] - :|: fset [:: sign_loc] - :|: fset [:: pk_loc; sk_loc]) - = fset [:: pk_loc; state_loc; pk_loc; sk_loc; sign_loc]. - Proof. - (* LHS *) - repeat rewrite fset_fsetU_norm2. - repeat rewrite -fsetUA. (* base shape *) - - (* stategy: deduplicate by moving same items to the left. *) - (* shift item on index 4 to the right (index starts from 0) *) - do 2! rewrite fsetUA. - rewrite [X in _ :|: X]fsetUC. - repeat rewrite -fsetUA. - rewrite fsetUid. - - rewrite fsetUC. - repeat rewrite -fsetUA. - - rewrite [X in _ :|: X]fsetUC. - repeat rewrite -fsetUA. - rewrite fsetUid. - - do 1! rewrite fsetUA. - rewrite [X in _ :|: X]fsetUC. - repeat rewrite -fsetUA. - rewrite fsetUid. - - (* final order *) - do 1! rewrite fsetUA. - rewrite [X in _ :|: X]fsetUC. - repeat rewrite -fsetUA. - - (* do 0! rewrite fsetUA. *) - rewrite [X in _ :|: X]fsetUC. - repeat rewrite -fsetUA. - - rewrite fsetUC. - repeat rewrite -fsetUA. - - (* collapse into fset *) - repeat rewrite -fset_cat cat1s. - - (* RHS *) - apply esym. - - repeat rewrite fset_fsetU_norm5. (* normalize *) - repeat rewrite -fsetUA. (* base shape *) - - rewrite fsetUC. - repeat rewrite -fsetUA. - - (* do 0! rewrite fsetUA. *) - rewrite [X in _ :|: X]fsetUC. - repeat rewrite -fsetUA. - rewrite fsetUid. - - (* final order *) - - (* do 0! rewrite fsetUA. *) - rewrite [X in _ :|: X]fsetUC. - repeat rewrite -fsetUA. - - (* do 0! rewrite fsetUA. *) - rewrite [X in _ :|: X]fsetUC. - repeat rewrite -fsetUA. - - rewrite fsetUC. - repeat rewrite -fsetUA. - - (* collapse into fset *) - by repeat rewrite -fset_cat cat1s. - Qed. - - - Theorem RA_unforg LA A : - ValidPackage LA Att_interface A_export A → - fdisjoint LA (Sig_real_locp).(locs) → - fdisjoint LA (Sig_ideal_locp).(locs) → - fdisjoint LA Aux_locs → - fdisjoint LA (Att_real_locp).(locs) → - fdisjoint LA (Att_ideal_locp).(locs) → - (AdvantageE (Att_ideal_c) (Att_real_c) A - <= AdvantageE (Aux ∘ Sig_ideal ∘ Key_Gen) (Aux ∘ Sig_real_c) A)%R. - Proof. - move => va H1 H2 H3 H4 H5. - rewrite Advantage_sym. - simpl in *|-. - ssprove triangle (Att_real ∘ Key_Gen) [:: - Aux ∘ Sig_real ∘ Key_Gen ; - Aux ∘ Sig_ideal ∘ Key_Gen - ] (Att_ideal ∘ Key_Gen) A as ineq. - eapply le_trans. - 1: { exact: ineq. } - clear ineq. - rewrite sig_real_vs_att_real. - - 2: exact: H4. - 2: { - rewrite fdisjointUr. - apply/andP; split; assumption. - } - rewrite GRing.add0r. - rewrite [X in (_ + X <= _)%R]Advantage_sym. - - (* Set Typeclasses Debug Verbosity 2. *) - - rewrite sig_ideal_vs_att_ideal. - (* Type class resolution failed because of the [Att_interface_f]. - Both advantages need to be on the same interface! - *) - 2: exact: H5. - 2: { - (* TODO There should be a tactic for discharging such [fdisjoint] goals! *) - rewrite /Comp_locs. - rewrite /Aux_locs in H3. - rewrite /Sig_locs_ideal in H2. - (* This feels like a silly construction. Is there a better way to arrive at this [Prop]? *) - rewrite /is_true in H3; rewrite /is_true in H2. - have prim_aux : true && true by []. - rewrite -[X in X && _]H3 -[X in _ && X]H2 in prim_aux. - - move: prim_aux; rewrite -fdisjointUr (* -/fset_cat *) /=. - - (* TODO move below into extructurespp and extend. *) - rewrite /Sig_locs_real/Key_locs. - - exact: id. - } - rewrite GRing.addr0. - by [rewrite Advantage_sym]. - Qed. + fset [:: pk_loc; state_loc] + :|: (fset [:: pk_loc; sk_loc] + :|: fset [:: sign_loc] + :|: fset [:: pk_loc; sk_loc]) + = fset [:: pk_loc; state_loc; pk_loc; sk_loc; sign_loc]. +Proof. + (* LHS *) + repeat rewrite fset_fsetU_norm2. + repeat rewrite -fsetUA. (* base shape *) + + (* stategy: deduplicate by moving same items to the left. *) + (* shift item on index 4 to the right (index starts from 0) *) + do 2! rewrite fsetUA. + rewrite [X in _ :|: X]fsetUC. + repeat rewrite -fsetUA. + rewrite fsetUid. + + rewrite fsetUC. + repeat rewrite -fsetUA. + + rewrite [X in _ :|: X]fsetUC. + repeat rewrite -fsetUA. + rewrite fsetUid. + + do 1! rewrite fsetUA. + rewrite [X in _ :|: X]fsetUC. + repeat rewrite -fsetUA. + rewrite fsetUid. + + (* final order *) + do 1! rewrite fsetUA. + rewrite [X in _ :|: X]fsetUC. + repeat rewrite -fsetUA. + + (* do 0! rewrite fsetUA. *) + rewrite [X in _ :|: X]fsetUC. + repeat rewrite -fsetUA. + + rewrite fsetUC. + repeat rewrite -fsetUA. + + (* collapse into fset *) + repeat rewrite -fset_cat cat1s. + + (* RHS *) + apply esym. + + repeat rewrite fset_fsetU_norm5. (* normalize *) + repeat rewrite -fsetUA. (* base shape *) + + rewrite fsetUC. + repeat rewrite -fsetUA. + + (* do 0! rewrite fsetUA. *) + rewrite [X in _ :|: X]fsetUC. + repeat rewrite -fsetUA. + rewrite fsetUid. + + (* final order *) + + (* do 0! rewrite fsetUA. *) + rewrite [X in _ :|: X]fsetUC. + repeat rewrite -fsetUA. + + (* do 0! rewrite fsetUA. *) + rewrite [X in _ :|: X]fsetUC. + repeat rewrite -fsetUA. + + rewrite fsetUC. + repeat rewrite -fsetUA. + + (* collapse into fset *) + by repeat rewrite -fset_cat cat1s. +Qed. + + +Theorem RA_unforg LA A : + ValidPackage LA Att_interface A_export A → + fdisjoint LA (Sig_real_locp).(locs) → + fdisjoint LA (Sig_ideal_locp).(locs) → + fdisjoint LA Aux_locs → + fdisjoint LA (Att_real_locp).(locs) → + fdisjoint LA (Att_ideal_locp).(locs) → + (AdvantageE (Att_ideal_c) (Att_real_c) A + <= AdvantageE (Aux ∘ Sig_ideal ∘ Key_Gen) (Aux ∘ Sig_real_c) A)%R. +Proof. + move => va H1 H2 H3 H4 H5. + rewrite Advantage_sym. + simpl in *|-. + ssprove triangle (Att_real ∘ Key_Gen) [:: + Aux ∘ Sig_real ∘ Key_Gen ; + Aux ∘ Sig_ideal ∘ Key_Gen + ] (Att_ideal ∘ Key_Gen) A as ineq. + eapply le_trans. + 1: { exact: ineq. } + clear ineq. + rewrite sig_real_vs_att_real. + + 2: exact: H4. + 2: { + rewrite fdisjointUr. + apply/andP; split; assumption. + } + rewrite GRing.add0r. + rewrite [X in (_ + X <= _)%R]Advantage_sym. + + (* Set Typeclasses Debug Verbosity 2. *) + + rewrite sig_ideal_vs_att_ideal. + (* Type class resolution failed because of the [Att_interface_f]. + Both advantages need to be on the same interface! + *) + 2: exact: H5. + 2: { + (* TODO There should be a tactic for discharging such [fdisjoint] goals! *) + rewrite /Comp_locs. + rewrite /Aux_locs in H3. + rewrite /Sig_locs_ideal in H2. + (* This feels like a silly construction. Is there a better way to arrive at this [Prop]? *) + rewrite /is_true in H3; rewrite /is_true in H2. + have prim_aux : true && true by []. + rewrite -[X in X && _]H3 -[X in _ && X]H2 in prim_aux. + + move: prim_aux; rewrite -fdisjointUr (* -/fset_cat *) /=. + + (* TODO move below into extructurespp and extend. *) + rewrite /Sig_locs_real/Key_locs. + + exact: id. + } + rewrite GRing.addr0. + by [rewrite Advantage_sym]. +Qed. End RemoteAttestationHash. diff --git a/theories/examples/RA_Prot.v b/theories/examples/RA_Prot.v index a87e93c..9bf3654 100644 --- a/theories/examples/RA_Prot.v +++ b/theories/examples/RA_Prot.v @@ -45,33 +45,33 @@ From vRATLS Require Import examples.Signature. From vRATLS Require Import examples.RA. Module Protocol - (π1 : SignatureParams) - (π2 : SignatureConstraints) - (RAP : RemoteAttestationParams π2) - (KG : KeyGeneration π1 π2) - (Alg : SignatureAlgorithms π1 π2 KG) - (RAA : RemoteAttestationAlgorithms π1 π2 RAP KG Alg) - (SP : SignaturePrimitives π1 π2 KG Alg) - (RAH : RemoteAttestationHash π1 π2 RAP KG Alg RAA SP) - . - - Import π1 π2 RAP KG Alg RAA SP RAH. + (π1 : SignatureParams) + (π2 : KeyGenParams π1) + (KGc : KeyGen_code π1 π2) + (Alg : SignatureAlgorithms π1 π2 KGc) + (RAA : RemoteAttestationAlgorithms π1 π2 KGc) + (RAH : RemoteAttestationHash π1 π2 KGc Alg RAA). + + Module π3 := RemoteAttestationParams π1. + Module SP := SignaturePrimitives π1 π2 KGc Alg. + Import π1 π2 π3 KGc Alg RAA SP RAH. + Import KGc.KGP SP.KG. Definition i_chal := #|Challenge|. Definition att : nat := 50. - Definition RA_prot_interface := - [interface #val #[att] : 'unit → 'pubkey × ('attest × 'bool) ]. + Definition RA_prot_interface := + [interface #val #[att] : 'unit → 'pubkey × ('signature × 'bool) ]. - Definition Att_prot : package Attestation_locs_real + Definition Att_prot : package Attestation_locs_real Att_interface RA_prot_interface := [package - #def #[att] ( _ : 'unit) : 'pubkey × ('attest × 'bool) + #def #[att] ( _ : 'unit) : 'pubkey × ('signature × 'bool) { #import {sig #[get_pk_att] : 'unit → 'pubkey } as get_pk_att ;; #import {sig #[attest] : 'challenge → ('signature × 'message) } as attest ;; #import {sig #[verify_att] : ('challenge × 'signature) → 'bool } as verify_att ;; - + (* Protocol *) pk ← get_pk_att tt ;; chal ← sample uniform i_chal ;; @@ -132,8 +132,8 @@ Module Protocol (* This prop is different from the RA prop, because it has much more inputs *) Parameter RA_prop: - ∀ (l: {fmap (Signature * chState * chChallenge ) -> 'unit}) - (s s' s'' : chState) (pk : PubKey) (sk : SecKey) (chal : chChallenge) (h : chMessage), + ∀ (l: {fmap (chSignature * chState * chChallenge ) -> 'unit}) + (s s' s'' : chState) (pk : 'pubkey) (sk : 'seckey) (chal : chChallenge) , Ver_sig pk (Sign sk (Hash s chal)) (Hash s' chal) = ((Sign sk (Hash s chal), s'', chal) \in domm l). @@ -157,26 +157,50 @@ Module Protocol ssprove_code_simpl. ssprove_code_simpl_more. ssprove_code_simpl; simplify_linking. - ssprove_sync. - ssprove_sync. - ssprove_sync => pk. - ssprove_sync => chal. - ssprove_sync => sk. - ssprove_sync => state. - apply r_get_remember_rhs => a. - apply r_get_remember_lhs => pk'. - apply r_get_remember_lhs => state'. - eapply r_put_rhs. - ssprove_restore_mem. - -- ssprove_invariant. - -- eapply r_get_remember_rhs => a'. + rewrite /cast_fun/eq_rect_r/eq_rect. + simplify_linking. + ssprove_code_simpl. + eapply rsame_head_alt_pre. + -- apply (rpost_weaken_rule _ + (λ '(a₀, s₀) '(a₁, s₁), a₀ = a₁ /\ heap_ignore (fset [:: attest_loc_long]) (s₀, s₁))). + --- eapply r_reflexivity_alt. + ---- instantiate (1:=Key_locs). destruct KeyGen. exact: prog_valid. + ---- move => l. + rewrite /Key_locs. unfold Key_locs => l_not_in_Key_locs. (* Why does rewrite fail? *) + ssprove_invariant. + move: l_not_in_Key_locs. + rewrite fset_cons. + apply/fdisjointP. + rewrite fdisjointUl. + apply/andP. + split; + (( try rewrite -fset1E); rewrite fdisjoint1s; auto_in_fset). + ---- move => l v l_not_in_Key_locs. ssprove_invariant. + --- case => a0 s0; case => a1 s1. case => l r. by [split]. + --intro a. + ssprove_code_simpl. + ssprove_code_simpl_more. + destruct a. + ssprove_sync. + ssprove_sync. + ssprove_sync => pk. + ssprove_sync => chal. + ssprove_sync => sk. + ssprove_sync => state. + apply r_get_remember_rhs => a. + apply r_get_remember_lhs => pk'. + apply r_get_remember_lhs => state'. + eapply r_put_rhs. + ssprove_restore_mem. + --- ssprove_invariant. + --- eapply r_get_remember_rhs => a'. apply r_get_remember_rhs => state''. - eapply r_ret => s0 s1 pre //=. + eapply r_ret => s2 s1 pre //=. split. - --- repeat f_equal. - eapply RA_prop. intuition eauto. - ---move: pre. - by repeat case. + ---- repeat f_equal. + eapply RA_prop. + ---- move: pre. + by repeat case. Qed. End Protocol. diff --git a/theories/examples/RSA.v b/theories/examples/RSA.v index f1798b6..3a8c735 100644 --- a/theories/examples/RSA.v +++ b/theories/examples/RSA.v @@ -1,20 +1,23 @@ From Relational Require Import OrderEnrichedCategory GenericRulesSimple. +From mathcomp Require Import all_ssreflect. Set Warnings "-notation-overridden,-ambiguous-paths". + From mathcomp Require Import all_ssreflect all_algebra reals distr realsum fingroup.fingroup solvable.cyclic prime ssrnat ssreflect ssrfun ssrbool ssrnum - eqtype choice seq. + eqtype choice seq fintype zmodp prime finset. + Set Warnings "notation-overridden,ambiguous-paths". From extra Require Import rsa. From Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb UniformStateProb - pkg_core_definition choice_type pkg_composition pkg_rhl + pkg_core_definition choice_type pkg_composition pkg_rhl Casts Package Prelude RandomOracle. From Coq Require Import Utf8. -From extructures Require Import ord fset fmap. +From extructures Require Import ord fset fmap ffun. From Equations Require Import Equations. Require Equations.Prop.DepElim. @@ -22,11 +25,6 @@ Require Import Coq.Init.Logic. Require Import List. Set Equations With UIP. -(* - This is needed to make definitions with Equations transparent. - Otherwise they are opaque and code simplifications in the - proofs with [ssprove_code_simpl] do not resolve properly. - *) Set Equations Transparent. Set Bullet Behavior "Strict Subproofs". @@ -41,90 +39,882 @@ From vRATLS Require Import Signature. Import PackageNotation. -Obligation Tactic := idtac. +Local Open Scope package_scope. + + +Module RSA_params <: SignatureParams. + + (* Message space *) + Variable w : nat. + + (* Sampling space *) + Variable n : nat. + + Definition pos_n : nat := 2^n. + + Definition r₀ : nat := n.+4.+2. + (* We need to have at least two primes [p] and [q]. + Indeed, the conditions for phi_N force us to have + at least prime numbers 2,3 and 5! + *) + Definition R₀ : Type := 'I_r₀. + Definition r : nat := r₀ * r₀. + Definition R : Type := 'I_r. + + (* the set of prime numbers. *) + Definition prime_num : finType := {x: R₀ | prime x + (* & odd x (* --> excludes prime 2 and gives e=7 (smallest) *) *) + }. + Definition P : {set prime_num} := [set : prime_num]. + + Lemma two_ltn_r₀ : 2 < r₀. + Proof. by rewrite /r₀; case: n. Qed. + + Definition two : R₀ := Ordinal two_ltn_r₀. + Lemma prime2ord : prime two. Proof. by []. Qed. + Definition two' : prime_num := exist _ two prime2ord. + + Lemma three_ltn_r₀ : 3 < r₀. + Proof. by rewrite /r₀; case: n. Qed. + + Definition three : R₀ := Ordinal three_ltn_r₀. + Lemma prime3ord : prime three. Proof. by []. Qed. + Definition three' : prime_num := exist _ three prime3ord. + Lemma five_ltn_r₀ : 5 < r₀. + Proof. by rewrite /r₀; case: n. Qed. + + Definition five : R₀ := Ordinal five_ltn_r₀. + Lemma prime5ord : prime five. Proof. by []. Qed. + Definition five' : prime_num := exist _ five prime5ord. + + (* + This definition accounts for two properties: + 1. [p <> q] such that the primes are not equal and + 2. [2 < p.-1 * q.-1] such that we at the very least draw + one number [e] from this space. + Since, in this new space [phi_N = p.-1 * q.-1] we also + require that [e] is coprime to the space itself, i.e., + [coprime e phi_N] we arrive that smallest possible + [e=3] when [p=2] and [q=5] because + [2.-1 * 5.-1 = 1 * 4 = 4]. + *) + Definition P' (y : prime_num) := (* (P :\ y)%SET. *) + let P_no_y := (P :\ y)%SET in + if y == two' then (P_no_y :\ three')%SET + else if y == three' then (P_no_y :\ two')%SET + else P_no_y. + + Lemma notin_m {T:finType} (a b:T) (Q:{set T}): + a \notin Q -> a \notin (Q :\ b)%SET. + Proof. + move => a_notin_Q. + rewrite in_setD. + by apply/nandP; right. + Qed. + + Lemma P_P'_neq : forall y, y \in P -> P :!=: P' y. + Proof. + rewrite /P' => y y_in_P. + rewrite eqtype.eq_sym. + apply proper_neq. + case: (y == two'). + - apply/properP. + split. + * by []. + * exists y => //=. + apply notin_m. + rewrite in_setD. + apply/nandP; left. + rewrite negbK. + exact: set11. + - case: (y == three'). + * apply/properP. + split. + + by []. + + exists y => //=. + apply notin_m. + rewrite in_setD. + apply/nandP; left. + rewrite negbK. + exact: set11. + * by apply properD1. + Qed. + + Lemma p_q_neq p q (p_in_P: p \in P) : + q \in P' p -> p <> q. + Proof. + rewrite /P'. + case: (p == two'). + - rewrite in_setD1; move/andP; case => _. + by rewrite in_setD1; move/andP; case; move/eqP/nesym. + - case: (p == three'); + [rewrite in_setD1; move/andP; case => _|]; + by rewrite in_setD1; move/andP; case; move/eqP/nesym. + Qed. + + Definition i_P := #|P|. + Instance pos_i_P : Positive i_P. + Proof. + apply /card_gt0P. by exists two'. + Qed. + + #[export] Instance positive_P' `(p:prime_num) : Positive #|(P' p)|. + Proof. + apply/card_gt0P. + case H: (p == two'); move/eqP: H. + - move => H; rewrite H; exists five'. + rewrite /P'. + case: (two' == two'); + try repeat rewrite in_setD1 //=. + apply in_setT. + - move => H₂. + rewrite /P'. + rewrite ifF. + + case H₃: (p == three'); move/eqP: H₃ => H₃. + * rewrite H₃. + exists five'. + repeat rewrite in_setD1 //=; apply/andP; split. + * exists two'. + rewrite in_setD1. + apply/andP; split; [by apply/eqP/nesym | apply in_setT]. + + by apply/eqP. + Qed. + + Lemma p_q_neq' (p: 'fin P) (q: 'fin (P' (enum_val p))) : enum_val p != enum_val q. + Proof. + apply/eqP. + apply p_q_neq; try apply/enum_valP. + Qed. + + (* + Definition X (m:nat) : finType := 'I_m.+3. + The above is insufficient. I want to sample an [e] from a space + such that [1 < e < phi_N] where + [phi_N = lcm p.-1 q.-1] for Carmichael's totient function or + [phi_N = p.-1 * q.-1] for Euler's totient function. + That is [phi_N = totient p * totient q] by [totient_prime]. + And [phi_N = totient (p * q)] by [totient coprime] given [coprime p q]. + That is [phi_N = totient n]. + Search "totient". + Search coprime prime. + *) + Definition E' {m:R} (H:2 n0 n0_lt_r //. + move => H. + apply/ltnSE => //. + simpl. (* removes [inZp] *) + rewrite prednK. + - simpl. + rewrite modn_small //. + - rewrite -pred_Sn. + move/ltnSE/ltnW:H. + exact: id. + Qed. + + Lemma m_pred_gt1 (H:{m:R | 2 m m_gt2. + rewrite /sval. + by apply m_pred_gt1'. + Qed. + + Lemma m_pred_coprime' {m:R} (m_gt2: 2 m m_gt2. + by apply m_pred_coprime'. + Qed. + + Lemma m_pred_all {m:R} (m_gt2: 2 (Signature * A * A ) triggert endless loop *) + Lemma eq_dec (p q pq d w: nat) (H: pq = (p * q)%nat) : decrypt'' d pq w = decrypt' d p q w. + Proof. + by rewrite /decrypt''/decrypt' H. + Qed. - (* Final proposition for a signature scheme to be indistinguishable *) - Parameter Signature_prop: - ∀ (l: {fmap (Signature * chMessage ) -> 'unit}) - (s : Signature) (pk : PubKey) (m : chMessage), - Ver_sig pk s m = ((s,m) \in domm l). + Lemma eq_enc (p q pq d w: nat) (H: pq = (p * q)%nat) : encrypt'' d pq w = encrypt' d p q w. + Proof. + by rewrite /encrypt''/encrypt' H. + Qed. + + Theorem rsa_correct'' + {p q pq d e : nat} + (H: pq = (p * q)%nat) + (wf : wf_type p q + (p.-1 * q.-1) (* phi_N based on Euler totien function instead of lcm *) + d e) w : + let r := Build_rsa wf in + decrypt'' e pq (encrypt'' d pq w) = w %[mod pq]. + Proof. + rewrite (eq_dec p q _ _ _ H). + rewrite (eq_enc p q _ _ _ H). + rewrite (enc_eq wf) (dec_eq wf) /=. rewrite [X in _ %% X = _ %% X]H. + apply rsa_correct. + Qed. + + Lemma pq_phi_gt_0 : forall p q, prime p -> prime q -> 0 < p.-1 * q.-1. + Proof. + by case => [] // [] // p1; case => [] // []. + Qed. + +End RSA_func. + + + +Module RSA_KeyGen <: KeyGenParams RSA_params. + + Import RSA_params RSA_func. + + Definition sk0 : SecKey := (exist _ 1%R (ltn0Sn 0), 1)%g. + Definition pk0 : PubKey := (exist _ 1%R (ltn0Sn 0), 1)%g. + Definition sig0 : Signature := 1%g. + Definition m0 : Message := 1%g. + Definition chal0 : Challenge := 1%g. + + #[export] Instance SecKey_pos : Positive #|SecKey|. + Proof. + apply /card_gt0P. exists sk0. auto. + Qed. + + #[export] Instance PubKey_pos : Positive #|PubKey|. + Proof. + apply /card_gt0P. exists pk0. auto. + Qed. + + #[export] Instance Signature_pos : Positive #|Signature|. + Proof. + apply /card_gt0P. exists sig0. auto. + Qed. + + #[export] Instance Message_pos : Positive #|Message|. + Proof. + apply /card_gt0P. exists m0. auto. + Qed. + + #[export] Instance Challenge_pos : Positive #|Challenge|. + Proof. + apply /card_gt0P. exists chal0. auto. + Qed. + + Definition chSecKey : choice_type := 'fin #|SecKey|. + Definition chPubKey : choice_type := 'fin #|PubKey|. + Definition chSignature : choice_type := 'fin #|Signature|. + Definition chMessage : choice_type := 'fin #|Message|. + Definition chChallenge : choice_type := 'fin #|Challenge|. + + Definition i_sk := #|SecKey|. + Definition i_pk := #|PubKey|. + Definition i_sig := #|Signature|. + +End RSA_KeyGen. + + + +Module RSA_KeyGen_code <: KeyGen_code RSA_params RSA_KeyGen. + + Import Padding. + Import RSA_params RSA_KeyGen. + Module KGP := KeyGenParams_extended RSA_params RSA_KeyGen. + Import KGP. + Module π1 := RSA_params. + + Import PackageNotation. + Local Open Scope package_scope. + + Definition cast (p : prime_num ) : R₀ := + match p with + | exist x _ => x + end. + + Lemma n_leq_nn : r₀ <= r. + Proof. + rewrite /r/r₀ -addn1. + apply leq_pmull. + by rewrite addn1. + Qed. + + Lemma mult_prime_gt_0 : forall a b, + prime a -> + prime b -> + 0 < a * b. + Proof. + move => a b ap bp. + rewrite muln_gt0. + apply/andP. + split. + - exact: prime_gt0 ap. + - exact: prime_gt0 bp. + Qed. + + Lemma fold_R3 : (π1.n + (π1.n + (π1.n + π1.n * π1.n.+3).+3).+3).+3 = (π1.n.+3 * π1.n.+3)%nat. + Proof. + rewrite (addnC π1.n (muln _ _)). + repeat rewrite -addSn. + rewrite -[X in (_ + (_ + X))%nat = _]addn3. + rewrite -/Nat.add plusE. + rewrite -[X in (_ + (_ + X))%nat = _]addnA. + rewrite addn3. + by rewrite -mulSnr -mulSn -mulSn. + Qed. + + + Lemma fold_R4 : (π1.n + (π1.n + (π1.n + (π1.n + π1.n * π1.n.+4).+4).+4).+4).+4 = (π1.n.+4 * π1.n.+4)%nat. + Proof. + rewrite (addnC π1.n (muln _ _)). + repeat rewrite -addSn. + rewrite -[X in (_ + (_ + (_ + X)))%nat = _]addn4. + rewrite -/Nat.add plusE. + rewrite -[X in (_ + (_ + (_ + X)))%nat = _]addnA. + rewrite addn4. + by rewrite -mulSnr -mulSn -mulSn -mulSn. + Qed. + + Lemma fold_R6 : + (π1.n + + (π1.n + + (π1.n + + (π1.n + + (π1.n + + (π1.n + π1.n * r₀).+2.+4).+2.+4).+2.+4).+2.+4).+2.+4).+2.+4 = (π1.n.+2.+4 * π1.n.+2.+4)%nat. + Proof. + rewrite /r₀. + rewrite (addnC π1.n (muln _ _)). + repeat rewrite -addSn. + rewrite -[X in + (_ + (_ + (_ + (_ + (_ + X)))))%nat = _]addn4. + rewrite -/Nat.add plusE. + rewrite -[X in + (_ + (_ + (_ + (_ + (_ + X)))))%nat = _]addn2. + rewrite -/Nat.add plusE. + rewrite -[X in + (_ + (_ + (_ + (_ + (_ + X)))))%nat = _]addnA. + rewrite -[X in + (_ + (_ + (_ + (_ + (_ + X)))))%nat = _]addnA. + rewrite (addnC 4 2). + rewrite (addnA _ 2 4). + rewrite addn2. + rewrite addn4. + by rewrite -mulSnr -mulSn -mulSn -mulSn. + Qed. + + Lemma ltn_R : forall (a b: R₀), + a * b < + (π1.n + + (π1.n + + (π1.n + + (π1.n + + (π1.n + + (π1.n + π1.n * r₀).+2.+4).+2.+4).+2.+4).+2.+4).+2.+4).+2.+4. + Proof. + rewrite /R₀/r₀ => a b. + by rewrite fold_R6 ltn_mul. + Qed. + + + Lemma widen_mult_prime_gt_0_R {a b:R₀} (ap: prime a) (bp: prime b) : + 0 < ((widen_ord n_leq_nn a) * (widen_ord n_leq_nn b))%R. + Proof. + rewrite /widen_ord /=. + rewrite -/Nat.mul -/Nat.add. + rewrite plusE multE. + rewrite modn_small. + - by apply mult_prime_gt_0. + - by apply ltn_R. + Qed. + + Lemma widen_mult_prime_gt_0_nat {a b:R₀} (ap: prime a) (bp: prime b) : + 0 < ((widen_ord n_leq_nn a) * (widen_ord n_leq_nn b))%nat. + Proof. + rewrite /widen_ord /=. + by apply mult_prime_gt_0. + Qed. + + Definition mult_cast (a b : prime_num) : R' := + match a,b with + | exist a' ap , exist b' bp => + exist _ + ((widen_ord n_leq_nn a') * (widen_ord n_leq_nn b'))%R (* <-- This [R] is not our [R] but means the Ring. *) + (widen_mult_prime_gt_0_R ap bp) + end. + + Lemma mult_cast_nat_lt_r {a b:R₀} : (a * b)%nat < r. + Proof. + move: a b; rewrite /R₀/r. + case => [a a_ltn]; case => [b b_ltn]. + apply ltn_mul; try apply ltn_ord. + Qed. + + Definition mult_cast_nat (a b : prime_num) : R' := + match a,b with + | exist a' ap , exist b' bp => + exist _ + (Ordinal mult_cast_nat_lt_r) + (widen_mult_prime_gt_0_nat ap bp) + end. + + Definition phi_N (a b : prime_num) : nat := + match a,b with + | exist a' ap , exist b' bp => a'.-1 * b'.-1 + end. + + Lemma sub_r_gt_r {r:R₀} (H:0 < r) : r.-1 < r₀. + Proof. + case: r H; case => r r_lt_r₀ // => H //=. + exact: ltnW. + Qed. + + Definition sub_r {r:R₀} (H:0 < r) : R₀ := + Ordinal (sub_r_gt_r H). + + Lemma phi_N_lt_r (a b : prime_num) : phi_N a b < r. + Proof. + rewrite /phi_N //. + case: a => a a_prim; case: b => b b_prim //. + rewrite /r. + apply ltn_mul; [move: a_prim | move: b_prim]; + move/prime_gt1/ltnW; exact: sub_r_gt_r. + Qed. + + Definition phi_N_ord (a b : prime_num) : R := + Ordinal (phi_N_lt_r a b). + + Equations e_widen {m:R} (H:2 [m m_lt_r] H [e e_gt1] //=. + repeat rewrite prednK. + - exact: (ltnW m_lt_r). + - exact: ltnW (ltnW H). + - rewrite -ltnS prednK. + + exact: ltnW H. + + exact: ltnW (ltnW H). + Defined. + + Equations calc_d (phi: {m:R | 2 p' q'. + rewrite /phi_N_ord/phi_N //=. + + have p_in_P : enum_val p' \in P := enum_valP p'. + have q_in_P' : enum_val q' \in (P' (enum_val p')) := enum_valP q'. + have p_q_neq: enum_val p' \in P -> enum_val q' \in P' (enum_val p') -> enum_val p' <> enum_val q' := (p_q_neq (enum_val p') (enum_val q')). + move:p_q_neq p_in_P q_in_P'. + + case: (enum_val q') => /= => q'' q_prime. + case: (enum_val p') => /= => p'' p_prime. + + case: p'' p_prime => //=; case => //=; case => //=. + case. + - (* [p = 2] *) + case: q'' q_prime => //=; case => //=; case => //=. + case. + + (* [q = 2] => discard by [P'] *) + move => q_lt_r₀ q_prime. + move => p_lt_r₀ p_prime. + move => p_q_neq p_in_P q_in_P'. + + specialize (p_q_neq p_in_P q_in_P'). + + have p_q_eq: Ordinal (n:=r₀) (m:=2) p_lt_r₀ = Ordinal (n:=r₀) (m:=2) q_lt_r₀ by + clear; apply/eqP; exact: eq_refl. (* <- eqType (proof irrelevance) *) + + have prime_p: prime (Ordinal (n:=r₀) (m:=2) p_lt_r₀) by []. + have prime_q: prime (Ordinal (n:=r₀) (m:=2) q_lt_r₀) by []. + + have p_q_eq': + exist (λ x : 'I_r₀, prime x) (Ordinal (n:=r₀) (m:=2) p_lt_r₀) prime_p + = exist (λ x : 'I_r₀, prime x) (Ordinal (n:=r₀) (m:=2) q_lt_r₀) prime_q := + @boolp.eq_exist _ (λ x : 'I_r₀, prime x) _ _ prime_p prime_q p_q_eq. + + have p_prime_eq : prime_p = p_prime by []. + have q_prime_eq : prime_q = q_prime by []. + + move: p_q_neq p_q_eq'. + + by rewrite p_prime_eq q_prime_eq. + + + (* [q = n.+3] *) + case. + * (* [q = 3] => [2 < 1 * 2] => discard by [P'] *) + + move => q_lt_r₀ q_prime. + move => p_lt_r₀ p_prime. + move => p_q_neq p_in_P. + + rewrite /P'/three'/three //=. + have prime3_eq: q_prime = prime3ord by []. + rewrite prime3_eq. + rewrite in_setD. + move/andP; case. + have three_ltn_r₀_eq : q_lt_r₀ = three_ltn_r₀ by []. + rewrite three_ltn_r₀_eq. + move/negP. + + by rewrite in_set1. + + * (* [q = n.+3] => [2 < 1 * n.+3] => solve *) + by []. + - (* [p = n.+3] *) + (* discard non-prime cases *) + case: q'' q_prime => //=; case => //=; case => //=. + (* now solve *) + case. + + (* [q = 2] => [2 < n.+2 * 1] *) + move => q_lt_r₀ q_prime. + case. + * (* [p = 3] => [2 < 2 * 1] => discard by [P'] *) + move => p_lt_r₀ p_prime. + move => p_q_neq p_in_P. + + rewrite /P'/three'/three/two'/two //=. + have prime2_eq: q_prime = prime2ord by []. + rewrite prime2_eq. + rewrite in_setD. + move/andP; case. + have two_ltn_r₀_eq : q_lt_r₀ = two_ltn_r₀ by []. + rewrite two_ltn_r₀_eq. + move/negP. + + by rewrite in_set1. + + * (* [p = n.+4] => [2 < n.+3 * 1] => solve *) + by []. + + (* solve *) + intros; clear. + elim: n => [|n' iH]. + * by case: n0. + * rewrite mulnS; apply ltn_addl. + exact: iH. + Qed. + + Equations KeyGen : + code Key_locs [interface] (chPubKey × chSecKey) := + KeyGen := + {code + p₀ ← sample uniform P ;; + let p := enum_val p₀ in + q₀ ← sample uniform (P' p) ;; + let q := enum_val q₀ in + assert (p != q) ;; + + let phiN' := phi_N_ord' p₀ q₀ in + let phiN₁ := proj1_sig phiN' in + let phiN₂ := proj2_sig phiN' in + + e ← sample uniform (E phiN₂) ;; + let e := enum_val e in + let d := calc_d phiN' e in + let ed := Zp_mul (proj1_sig e) d in + assert (ed == Zp1) ;; + let e := e_widen phiN₂ (proj1_sig e) in + let d := e_widen phiN₂ d in + + let n := mult_cast_nat p q in + let pub_key := fto (n,e) in + let sec_key := fto (n,d) in + #put pk_loc := pub_key ;; + #put sk_loc := sec_key ;; + ret ( pub_key , sec_key ) + }. + +End RSA_KeyGen_code. + + +Module RSA_SignatureAlgorithms <: SignatureAlgorithms + RSA_params + RSA_KeyGen + RSA_KeyGen_code. - End rsa_alg. +(* - - (* - Definition SecKey' := Datatypes_prod__canonical__choice_Choice. - Definition PubKey' := Datatypes_prod__canonical__choice_Choice. - - Notation " 'pubkey2 " := PubKey' (in custom pack_type at level 2). - Notation " 'pubkey2 " := PubKey' (at level 2): package_scope. - Notation " 'seckey2 " := SecKey' (in custom pack_type at level 2). - Notation " 'seckey2 " := SecKey' (at level 2): package_scope. - - Definition Key_Gen_rsa : package Key_locs [interface] KeyGen_ifce - := [package - #def #[key_gen] (_ : 'unit) : ('seckey × 'pubkey) - { - p ← sample uniform i_sk ;; - q ← sample uniform i_sk ;; - #assert (prime p == true) ;; - #assert (prime q) ;; - ret (p,q) - } - ]. - *) - - Definition SecKey' :choice_type := nat. - Definition PubKey' := nat. - - Notation " 'pubkey2 " := PubKey' (in custom pack_type at level 2). - Notation " 'pubkey2 " := PubKey' (at level 2): package_scope. - Notation " 'seckey2 " := SecKey' (in custom pack_type at level 2). - Notation " 'seckey2 " := SecKey' (at level 2): package_scope. - - Definition Key_Gen_rsa : package Key_locs [interface] KeyGen_ifce - := [package - #def #[key_gen] (_ : 'unit) : ('seckey × 'pubkey) - { - ret (d,e) - } - ]. - -End -*) \ No newline at end of file +Module RSA_SignatureAlgorithms + (π1 : RSA_params) + (π2 : KeyGenParams π1) + (π3 : KeyGen_code π1 π2) +<: + (* FIXME This only gets the abstract definitions and hence creates the correctness + property based on that. + But I need the concrete implementations in order to create the proof! + + I would like to give a dedicated instance to derive from + [SignatureAlgorithms π1 (RSA_KeyGen π1) (RSA_KeyGen_code π1 π2)] + but Coq does not allow me to do so. + + At the same time, Coq does not allow me to make the module parameters + more concrete because appartently only a module type can be a parameter. + (This makes a lot of sense because modules can just be imported.) + *) + SignatureAlgorithms π1 (RSA_KeyGen π1) (RSA_KeyGen_code π1 π2). + + Import π1 π2 π3 π3.KGP. +*) + + Import RSA_params RSA_func RSA_KeyGen RSA_KeyGen_code RSA_KeyGen_code.KGP Padding. + + Module KG := RSA_KeyGen_code. + + + Lemma dec_smaller_n (d s pq : R) (H: 0 < pq) : (decrypt'' d pq s) < pq. + Proof. + by rewrite /decrypt''; apply ltn_pmod. + Qed. + + Lemma enc_smaller_n (e pq : R) (m : 'I_pq) (H: 0 < pq) : (encrypt'' e pq m) < pq. + Proof. + by rewrite /encrypt''; apply ltn_pmod. + Qed. + + Definition dec_to_In (d s pq : R) (H: 0 < pq) : 'I_pq := + Ordinal (dec_smaller_n d s pq H). + Definition enc_to_In (e pq:R) (m:'I_pq) (H: 0 < pq) : 'I_pq := + Ordinal (enc_smaller_n e pq m H). + + Lemma pq_leq_r: + forall (pq:fintype_ordinal__canonical__fintype_Finite r), pq <= r. + Proof. + case => pq pq_ltn_r /=. + exact: (ltnW pq_ltn_r). + Qed. + + Equations Sign (sk : chSecKey) (m : chMessage) : chSignature := + Sign sk m := + match otf sk with + | (exist pq O_ltn_pq, sk') => + (* This may seem unnecessary because we are casting + from [R] to ['I_pq] and back to [R']. + It is important for the proof part though. + *) + fto (widen_ord + (pq_leq_r pq) + (enc_to_In sk' pq (padd pq (otf m)) O_ltn_pq)) + end. + + Equations Ver_sig (pk : chPubKey) (sig : chSignature) (m : chMessage) : 'bool := + Ver_sig pk sig m := + match otf pk with + | (exist pq O_ltn_pq, pk') => + (dec_to_In pk' (otf sig) pq O_ltn_pq) == padd pq (otf m) + end. + + + Theorem Signature_correct pk sk msg seed (* e d p' q'*): + Some (pk,sk) = Run sampler KeyGen seed -> + Ver_sig pk (Sign sk msg) msg == true. + Proof. + rewrite /Run/Run_aux /=. + + (* SSReflect style generalization: *) + move: (pkg_interpreter.sampler_obligation_4 seed {| pos := P; cond_pos := pos_i_P |}) => p₀. + move: (pkg_interpreter.sampler_obligation_4 (seed + 1) {| pos := P' (enum_val p₀); cond_pos := _ |}) => q₀. + + rewrite /assert. + have p_q_neq'' : enum_val p₀ != enum_val q₀. 1: { by apply p_q_neq'. } + rewrite ifT //=. + + move: (pkg_interpreter.sampler_obligation_4 (seed + 1 + 1) {| pos := _; cond_pos := _ |}) => e. (* [sk₁] *) + + rewrite /sval. + case: (enum_val e) => [e']; move/andP; case => [e_gt1 coprime_e_phiN] //. + have ed_mod : Zp_mul e' (Zp_inv e') == Zp1. + 1:{ + apply/eqP. + apply Zp_mulzV. + (* rewrite coprime_sym. *) + clear e. + move: e' e_gt1 coprime_e_phiN; rewrite /phi_N_ord'/phi_N_ord/E' //=. + rewrite Zp_cast. + - move => e' e_gt1 coprime_e_phiN. + exact: coprime_e_phiN. + - apply/ltnW/KG.phi_N_ord'_obligations_obligation_1. + } + rewrite ifT //=. + + case => pk_eq sk_eq. (* injectivity *) + + rewrite /Ver_sig/Sign/dec_to_In/enc_to_In /=. + rewrite sk_eq pk_eq /=. + rewrite !otf_fto /=. + + case H: (mult_cast_nat (enum_val p₀) (enum_val q₀)) => [pq pq_gt_O] /=. + rewrite /widen_ord /=. + rewrite !otf_fto /=. + + apply/eqP/eqP. + (* TODO this step is a bit strange. investigate. *) + case H₁: (Ordinal (n:=pq) (m:=_) _) => [m i]. + case: H₁. + + move: H; rewrite /mult_cast_nat -/Nat.add -/Nat.mul /widen_ord. + clear sk_eq pk_eq. + + have phi_N_ord_gt2 : 2 < phi_N_ord (enum_val p₀) (enum_val q₀) := KG.phi_N_ord'_obligations_obligation_1 p₀ q₀. + + move: e' ed_mod e_gt1 coprime_e_phiN phi_N_ord_gt2. + case Hq: (enum_val q₀) => [q' q'_prime]. + case Hp: (enum_val p₀) => [p' p'_prime]. + move => e' ed_mod e_gt1 coprime_e_phiN phi_N_ord_gt2. + + case. + + case H₂: (Ordinal (n:=r) (m:=p') _) => [p'' p''_ltn_r]. + case: H₂ => p'_eq_p''. + case H₂: (Ordinal (n:=r) (m:=q') _) => [q'' q''_ltn_r]. + case: H₂ => q'_eq_q''. + + case XX: (Ordinal (n:=r) (m:=p'*q') _) => [p_mul_q pr]. + case: XX. move/esym => p_mul_q_eq. + move/esym => pq_spec. + + (* TODO remember this hypothesis for [decrypt] and [ecnrypt]. *) + rewrite -[X in X = _ -> _](@modn_small _ pq). + - rewrite -[X in _ = X -> _](@modn_small _ pq). + + + have eee : nat_of_ord pq = (p' * q')%N by subst. + rewrite (rsa_correct'' eee) /=. + * move => msg_eq. subst. + repeat rewrite modn_small in msg_eq. + ** by apply ord_inj. + ** exact: i. + ** by []. + * rewrite /wf_type. + apply/andP; split; try exact: p'_prime. + apply/andP; split; try exact: q'_prime. + apply/andP; split; [ by move: p_q_neq''; rewrite Hq Hp |]. + apply/andP; split; [ by apply pq_phi_gt_0 |]. + apply/andP; split; [ by apply dvdn_mulr |]. + apply/andP; split; [ by apply dvdn_mull |]. + move: ed_mod; rewrite mulnC. + + (* TODO should be a separate lemma! + [ + Zp_mul e' (Zp_inv e') == Zp1 -> + e' * Zp_inv e' == 1 %[mod p'.-1 * q'.-1] + ] + *) + rewrite /Zp_mul/inZp //=. + move/eqP. + case. + move: e' e_gt1 coprime_e_phiN. + rewrite /Zp_trunc/phi_N_ord/phi_N. + move => e' e_gt1 coprime_e_phiN. + Fail rewrite prednK. (* TODO How do I deal with dependent type errors? *) + move => ed_mod. + apply/eqP. + rewrite -[X in _ = 1 %[mod X]]prednK. + ** rewrite -[X in _ = 1 %[mod X.+1]]prednK. + *** exact: ed_mod. + *** apply ltnSE. + rewrite prednK. + **** apply/ltnW/phi_N_ord_gt2. + **** apply/ltnW/ltnW/phi_N_ord_gt2. + ** apply/ltnW/ltnW/phi_N_ord_gt2. + + by []. + - by rewrite /decrypt''; apply ltn_pmod. + + Unshelve. + 1: { clear ed_mod e phi_N_ord_gt2 p'_prime e' e_gt1 coprime_e_phiN Hp; case: p' => [p' p'_ltn_r₀]; apply (leq_trans p'_ltn_r₀ n_leq_nn). } + clear ed_mod e e' e_gt1 coprime_e_phiN phi_N_ord_gt2 q'_prime Hq; case: q' => [q' q'_ltn_r₀]; apply (leq_trans q'_ltn_r₀ n_leq_nn). + Qed. + +End RSA_SignatureAlgorithms. diff --git a/theories/examples/Sig_Prot.v b/theories/examples/Sig_Prot.v index e5a7c69..6ebf9ba 100644 --- a/theories/examples/Sig_Prot.v +++ b/theories/examples/Sig_Prot.v @@ -58,12 +58,13 @@ Definition tt := Datatypes.tt. Module Type SignatureProt (π1 : SignatureParams) - (π2 : SignatureConstraints) - (KG : KeyGeneration π1 π2) - (Alg : SignatureAlgorithms π1 π2 KG) - (Prim : SignaturePrimitives π1 π2 KG Alg). + (π2 : KeyGenParams π1) + (π3 : KeyGen_code π1 π2) + (π4 : SignatureAlgorithms π1 π2 π3). - Import π1 π2 KG Alg Prim. + Module π5 := SignaturePrimitives π1 π2 π3 π4. + Import π1 π2 π3 π4 π5. + Import π3.KGP π5.KG. Definition protocol := 30. Definition Sig_prot_ifce := @@ -85,7 +86,6 @@ Module Type SignatureProt } ]. - Equations Sig_prot_real : package Sig_locs_real [interface] Sig_prot_ifce := Sig_prot_real := {package Sig_prot ∘ Sig_real_c }. Next Obligation. @@ -143,20 +143,129 @@ Module Type SignatureProt apply fsubsetxx. - simplify_eq_rel m. simplify_linking. - ssprove_sync. ssprove_sync. - ssprove_sync => pk. - ssprove_sync => sk. - eapply r_get_remember_rhs => sig. - eapply r_put_rhs. - ssprove_restore_mem. - -- ssprove_invariant. - -- eapply r_get_remember_rhs => sig'. + rewrite /cast_fun/eq_rect_r/eq_rect. + simplify_linking. + ssprove_code_simpl. + eapply rsame_head_alt_pre. + -- apply (rpost_weaken_rule _ + (λ '(a₀, s₀) '(a₁, s₁), a₀ = a₁ /\ heap_ignore (fset [:: sign_loc]) (s₀, s₁))). + --- eapply r_reflexivity_alt. + ---- instantiate (1:=Key_locs). destruct KeyGen. exact: prog_valid. + ---- move => l. + rewrite /Key_locs. unfold Key_locs => l_not_in_Key_locs. (* Why does rewrite fail? *) + ssprove_invariant. + move: l_not_in_Key_locs. + rewrite fset_cons. + apply/fdisjointP. + rewrite fdisjointUl. + apply/andP. + split; + (( try rewrite -fset1E); rewrite fdisjoint1s; auto_in_fset). + ---- move => l v l_not_in_Key_locs. ssprove_invariant. + --- case => a0 s0; case => a1 s1. case => l r. by [split]. + -- intro a. + (* + ssprove_code_simpl. + ssprove_code_simpl_more. + *) + destruct a. + ssprove_sync. + ssprove_sync. + ssprove_sync => pk. + ssprove_sync => sk. + eapply r_get_remember_rhs => sig. + eapply r_put_rhs. + ssprove_restore_mem. + (* + At this point, the proof looses the information about + what is put into the [sign_loc]. + This is due to the [heap_ignore] invariant. + What are basically saying that we do not care what is + being stored in [sign_loc] for the proof. + *) + --- ssprove_invariant. + --- eapply r_get_remember_rhs => sig'. + eapply r_get_remember_lhs => KG_pk. + eapply r_ret. + intuition eauto. + ---- repeat f_equal. + apply Signature_prop. + ---- by [move: H; rewrite /inv_conj; repeat case]. + Qed. + + (* FIXME + This is still insufficient! + It misses the key generation evidence. + *) + Axiom Signature_correct_fail: forall pk sk msg, Ver_sig pk (Sign sk msg) msg == true. + + Lemma ext_unforge_sig_prot_full: + Sig_prot_real ≈₀ Sig_prot_ideal. + Proof. + eapply (eq_rel_perf_ind_ignore (fset [:: sign_loc])). + - rewrite /Sig_locs_real/Sig_locs_ideal. + apply fsubsetU. + apply/orP. + right. + rewrite !fset_cons. + apply fsubsetU ; apply /orP ; right. + apply fsetUS. + apply fsubsetxx. + - simplify_eq_rel m. + simplify_linking. + rewrite /cast_fun/eq_rect_r/eq_rect. + simplify_linking. + ssprove_code_simpl. + eapply rsame_head_alt_pre. + -- apply (rpost_weaken_rule _ + (λ '(a₀, s₀) '(a₁, s₁), a₀ = a₁ /\ heap_ignore (fset [:: sign_loc]) (s₀, s₁))). + --- eapply r_reflexivity_alt. + ---- instantiate (1:=Key_locs). destruct KeyGen. exact: prog_valid. + ---- move => l. + rewrite /Key_locs. unfold Key_locs => l_not_in_Key_locs. (* Why does rewrite fail? *) + ssprove_invariant. + move: l_not_in_Key_locs. + rewrite fset_cons. + apply/fdisjointP. + rewrite fdisjointUl. + apply/andP. + split; + (( try rewrite -fset1E); rewrite fdisjoint1s; auto_in_fset). + ---- move => l v l_not_in_Key_locs. ssprove_invariant. + --- case => a0 s0; case => a1 s1. case => l r. by [split]. + -- intro a. + (* + ssprove_code_simpl. + ssprove_code_simpl_more. + *) + destruct a. + ssprove_sync. + ssprove_sync. + ssprove_sync => pk. + ssprove_sync => sk. + eapply r_get_remember_rhs => sig. + eapply r_put_rhs. + eapply r_get_remember_rhs => sig'. eapply r_get_remember_lhs => KG_pk. - eapply r_ret => s0 s1 pre //=. - split. - ---- repeat f_equal. - apply Signature_prop. - ---- by [move: pre; rewrite /inv_conj; repeat case]. + eapply r_ret. + intuition eauto; + move:H; do 3! case; move => x; do 2! case; move => h_ignore sign_loc_is_sig set_s1 sign_log_is_sig' _. + --- repeat f_equal. + move: sign_log_is_sig'; rewrite /rem_rhs set_s1. + rewrite get_set_heap_eq. + intros [=<-]. + rewrite mem_domm. + rewrite setmE. + rewrite ifT //=. + apply/eqP. + (* FIXME: even this is not correct. + the correctness property needs evidence that [(pk,sk) = KeyGen] *) + exact: Signature_correct_fail. + --- rewrite set_s1. + rewrite /heap_ignore => l l_notin_sign_loc. + specialize (h_ignore l l_notin_sign_loc). + move: l_notin_sign_loc; rewrite -fset1E in_fset1 => l_neq_sig. + by rewrite get_set_heap_neq. Qed. Module Correctness. @@ -166,7 +275,6 @@ Module Type SignatureProt Definition Prot_res_ifce := [interface #val #[prot_res] : 'message → 'unit ]. - Equations prot_result (msg : 'message) : code Sig_locs_real Sig_prot_ifce 'bool := prot_result msg := {code #import {sig #[protocol] : 'message → 'pubkey × ('signature × 'bool) } as protocol ;; @@ -225,6 +333,12 @@ Module Type SignatureProt all: by [apply: fsubsetxx]. Defined. + Lemma reshape_pair_id {T T0 T1 : Type} (f : T * T0 -> T1) : (fun '(pair x y) => f (pair x y)) = f. + Proof. + apply functional_extensionality; by [case]. + Qed. + (* To DO: Get from RA.v, to import here and in RA.v *) + Lemma fun_correct: prot_result_real ≈₀ prot_result_real'. Proof. @@ -232,15 +346,49 @@ Module Type SignatureProt simplify_eq_rel x. all: simplify_linking; ssprove_code_simpl. repeat ssprove_sync_eq. - move => _. - ssprove_sync_eq => sk. - ssprove_sync_eq => pk. - rewrite /tt_. - rewrite (Signature_correct pk sk x) /=. - apply r_ret => s0 s1 s0_eq_s1 //=. + simplify_linking. + ssprove_code_simpl. + rewrite /cast_fun/eq_rect_r/eq_rect. + simplify_linking. + ssprove_code_simpl. + eapply rsame_head_alt_pre. + - set xxx := fun '(s0,s1) => s0 = s1. + rewrite -(reshape_pair_id xxx). + apply (rpost_weaken_rule _ + (λ '(a₀, s₀) '(a₁, s₁), a₀ = a₁ /\ (xxx (s₀, s₁)) )). + -- eapply r_reflexivity_alt. + --- instantiate (1:=Key_locs). destruct KeyGen. exact: prog_valid. + --- move => l. + rewrite /Key_locs/xxx. + unfold Key_locs => l_not_in_Key_locs. (* Why does rewrite fail? *) + rewrite /get_pre_cond. + by intros s0 s1 [=->]. + --- intros. + rewrite /xxx/put_pre_cond. + by intros s0 s1 [=->]. + + -- intro a. + intro a1. + simplify_linking. + destruct a. destruct a1. intros H. destruct H. + by split. + - intros a. + + ssprove_code_simpl. + ssprove_code_simpl_more. + destruct a. + ssprove_sync_eq. + ssprove_sync_eq. + ssprove_sync_eq => pk. + ssprove_sync_eq => sk. + ssprove_sync_eq => pk2. + rewrite /tt_. + rewrite (Signature_correct_fail pk2 sk x) /=. + apply r_ret => s2 s1 s0_eq_s1 //=. Qed. End Correctness. End SignatureProt. + diff --git a/theories/examples/Signature.v b/theories/examples/Signature.v index 5a8b59e..33c3d1e 100644 --- a/theories/examples/Signature.v +++ b/theories/examples/Signature.v @@ -48,45 +48,42 @@ Notation " 'set t " := (chSet t) (at level 2): package_scope. Definition tt := Datatypes.tt. Module Type SignatureParams. - - Parameter fSecKey : finType. - Parameter SecKey_pos : Positive #|fSecKey|. - #[local] Existing Instance SecKey_pos. - Definition SecKey := 'fin #|fSecKey|. - Definition i_sk := #|fSecKey|. - Lemma pos_i_sk : Positive i_sk. - Proof. - rewrite /i_sk. apply SecKey_pos. - Qed. - - Definition PubKey := SecKey. - Definition Signature : choice_type := chFin(mkpos pos_n). - (* - Definition SecKey : choice_type := chFin(mkpos pos_n). - Definition PubKey : choice_type := chFin(mkpos pos_n). - *) - + Parameter SecKey PubKey Signature Message Challenge : finType. End SignatureParams. -Module Type SignatureConstraints. - Definition chMessage : choice_type := 'fin (mkpos pos_n). -End SignatureConstraints. - (** | KEY | | GENERATION | **) -Module Type KeyGeneration - (π1 : SignatureParams) - (π2 : SignatureConstraints). +Module Type KeyGenParams (π1 : SignatureParams). + Import π1. + + Parameter SecKey_pos : Positive #|SecKey|. + Parameter PubKey_pos : Positive #|PubKey|. + Parameter Signature_pos : Positive #|Signature|. + Parameter Message_pos : Positive #|Message|. + Parameter Challenge_pos : Positive #|Challenge|. + +End KeyGenParams. +Module KeyGenParams_extended (π1 : SignatureParams) (π2 : KeyGenParams π1). Import π1 π2. - Notation " 'pubkey " := PubKey (in custom pack_type at level 2). - Notation " 'pubkey " := PubKey (at level 2): package_scope. - Notation " 'seckey " := SecKey (in custom pack_type at level 2). - Notation " 'seckey " := SecKey (at level 2): package_scope. + #[local] Existing Instance SecKey_pos. + #[local] Existing Instance PubKey_pos. + #[local] Existing Instance Signature_pos. + #[local] Existing Instance Message_pos. + #[local] Existing Instance Challenge_pos. - Parameter KeyGen : (SecKey × PubKey). + Definition chSecKey := 'fin #|SecKey|. + Definition chPubKey := 'fin #|PubKey|. + Definition chSignature := 'fin #|Signature|. + Definition chMessage := 'fin #|Message|. + Definition chChallenge := 'fin #|Challenge|. + + Notation " 'pubkey " := chPubKey (in custom pack_type at level 2). + Notation " 'pubkey " := chPubKey (at level 2): package_scope. + Notation " 'seckey " := chSecKey (in custom pack_type at level 2). + Notation " 'seckey " := chSecKey (at level 2): package_scope. Definition pk_loc : Location := ('pubkey ; 0%N). Definition sk_loc : Location := ('seckey ; 1%N). @@ -95,28 +92,25 @@ Module Type KeyGeneration Definition apply : nat := 3. Definition Key_locs := fset [:: pk_loc ; sk_loc]. - (* - "failed attempt to define apply function as enclave - for secret key" +End KeyGenParams_extended. - Context (T : choice_type). - Notation " 't " := T (in custom pack_type at level 2). - Notation " 't " := T (at level 2): package_scope. +Module Type KeyGen_code (π1 : SignatureParams) (π2 : KeyGenParams π1). + Import π1 π2. + Module KGP := KeyGenParams_extended π1 π2. + Import KGP. - Context (L : {fset Location}). - Definition M L T := code L [interface] T. - Notation " 'm " := M (in custom pack_type at level 2). - Notation " 'm " := M (at level 2): package_scope. + Parameter KeyGen : + code Key_locs [interface] (chPubKey × chSecKey). - Definition Apply := mkopsig apply ('m L 'seckey) ('m L T). +End KeyGen_code. - Definition KeyGen_ifce T := fset (cons - (*(pair key_gen (pair 'unit 'pubkey)) *) +Module KeyGen + (π1 : SignatureParams) + (π2 : KeyGenParams π1) + (π3 : KeyGen_code π1 π2). - (pair apply (pair Apply T)) - (*#val #[apply] : ('m L 'seckey → 'm L 't) → 't *) - nil). - *) + Import π1 π2 π3. + Import π3.KGP. Definition KeyGen_ifce := [interface #val #[key_gen] : 'unit → ('seckey × 'pubkey) @@ -124,56 +118,53 @@ Module Type KeyGeneration Definition Key_Gen : package Key_locs [interface] KeyGen_ifce := [package - #def #[key_gen] (_ : 'unit) : ('seckey × 'pubkey) - { - let (sk, pk) := KeyGen in - #put sk_loc := sk ;; - #put pk_loc := pk ;; + #def #[key_gen] (_ : 'unit) : ('seckey × 'pubkey) + { + '(pk, sk) ← KeyGen ;; + #put sk_loc := sk ;; + #put pk_loc := pk ;; + ret (sk, pk) + } + ]. - ret (sk, pk) - } - ]. - -End KeyGeneration. +End KeyGen. (** | SIGNATURE | | SCHEME | **) Module Type SignatureAlgorithms (π1 : SignatureParams) - (π2 : SignatureConstraints) - (π3 : KeyGeneration π1 π2). + (π2 : KeyGenParams π1) + (π3 : KeyGen_code π1 π2). - Import π1 π2 π3. + Import π3 π3.KGP. - Parameter Sign : ∀ (sk : SecKey) (m : chMessage), Signature. + Parameter Sign : ∀ (sk : chSecKey) (m : chMessage), chSignature. - Parameter Ver_sig : ∀ (pk : PubKey) (sig : Signature) (m : chMessage), + Parameter Ver_sig : ∀ (pk : chPubKey) (sig : chSignature) (m : chMessage), 'bool. - (* TODO: fmap (Signature * A * A ) -> (Signature * A * A ) triggert endless loop *) - - (* Final proposition for a signature scheme to be indistinguishable *) - Parameter Signature_prop: - ∀ (l: {fmap (Signature * chMessage ) -> 'unit}) - (s : Signature) (pk : PubKey) (m : chMessage), - Ver_sig pk s m = ((s,m) \in domm l). - (* Functional correctness property for signatures *) - Parameter Signature_correct: forall pk sk msg, Ver_sig pk (Sign sk msg) msg == true. + Parameter Signature_correct : ∀ pk sk msg seed, + Some (pk,sk) = Run sampler KeyGen seed -> + Ver_sig pk (Sign sk msg) msg == true. End SignatureAlgorithms. -Module Type SignaturePrimitives +Module SignaturePrimitives (π1 : SignatureParams) - (π2 : SignatureConstraints) - (KG : KeyGeneration π1 π2) - (Alg : SignatureAlgorithms π1 π2 KG). + (π2 : KeyGenParams π1) + (π3 : KeyGen_code π1 π2) + (π4 : SignatureAlgorithms π1 π2 π3). - Import π1 π2 KG Alg. + Import π1 π2 π3 π4. + Import π3.KGP. - Notation " 'signature " := Signature (in custom pack_type at level 2). - Notation " 'signature " := Signature (at level 2): package_scope. + Module KG := KeyGen π1 π2 π3. + Import KG. + + Notation " 'signature " := chSignature (in custom pack_type at level 2). + Notation " 'signature " := chSignature (at level 2): package_scope. Notation " 'message " := chMessage (in custom pack_type at level 2). Notation " 'message " := chMessage (at level 2): package_scope. @@ -257,8 +248,8 @@ Module Type SignaturePrimitives rewrite fset_cons. apply fsetUS. apply fsubsetxx. - - rewrite /Key_locs/Sig_locs_real/Key_locs. - rewrite fset_cons. + - rewrite /Sig_locs_real/Key_locs. + rewrite fset_cons. apply fsetUS. rewrite fset_cons. apply fsetUS. @@ -287,6 +278,25 @@ Module Type SignaturePrimitives apply fsub0set. Qed. + + (* + This axiom cannot be instantiated. + The problem is the missing link between [l] and the LHS of the + equality. + Even if [Ver_sig] is instantiated, this axiom remains unprovable. + See [RSA] for reference. + + This is a key finding in our development: + The proof of existential unforgability can only be done on the + protocol itself but __not__ on the library level. + Please see [Sig_prot] for an axiom-free proof of existential + unforgability. + *) + Axiom Signature_prop: + ∀ (l: {fmap (chSignature * chMessage ) -> 'unit}) + (s : chSignature) (pk : chPubKey) (m : chMessage), + Ver_sig pk s m = ((s,m) \in domm l). + Lemma ext_unforge: Sig_real_c ≈₀ Sig_ideal_c. Proof. @@ -300,26 +310,61 @@ Module Type SignaturePrimitives apply fsetUS. apply fsubsetxx. - simplify_eq_rel x. - -- simplify_linking. - ssprove_sync. - ssprove_sync. - ssprove_sync => pk_loc. - eapply r_ret. - intuition eauto. - -- repeat ssprove_sync. - intros. - eapply r_get_remember_rhs => sign_loc. - eapply r_put_rhs. - ssprove_restore_mem. - --- ssprove_invariant. - --- eapply r_ret => s0 s1 pre //=. - -- case x => s m. - eapply r_get_remember_lhs => pk. - eapply r_get_remember_rhs => S. - eapply r_ret => s0 s1 pre //=. - split. - ---- eapply Signature_prop. - ---- by [move: pre; rewrite /inv_conj; repeat case]. + -- simplify_linking. + ssprove_code_simpl. + rewrite /cast_fun/eq_rect_r/eq_rect. + simplify_linking. + ssprove_code_simpl. + eapply rsame_head_alt_pre. + --- Fail eapply r_reflexivity_alt. + (* + This really needs a tactic. + This postcondition has the wrong shape. + It needs [b0 = b1 /\ f (s0, s1)]. + But we have [f (s0, s1) /\ b0 = b1]. + The rewrite is a bit more evolved though because + we would need setoid_rewrite to rewrite under binders. + The SSProvers instead provide the following way: + *) + apply (rpost_weaken_rule _ + (λ '(a₀, s₀) '(a₁, s₁), a₀ = a₁ /\ heap_ignore (fset [:: sign_loc]) (s₀, s₁))). + ---- eapply r_reflexivity_alt. + ----- instantiate (1:=Key_locs). destruct KeyGen. exact: prog_valid. + ----- move => l. + rewrite /Key_locs. unfold Key_locs => l_not_in_Key_locs. (* Why does rewrite fail? *) + ssprove_invariant. + move: l_not_in_Key_locs. + rewrite fset_cons. + apply/fdisjointP. + rewrite fdisjointUl. + apply/andP. + split; + (( try rewrite -fset1E); rewrite fdisjoint1s; auto_in_fset). + ----- move => l v l_not_in_Key_locs. ssprove_invariant. + ---- case => a0 s0; case => a1 s1. case => l r. by [split]. + --- intro a. + ssprove_code_simpl. + ssprove_code_simpl_more. + destruct a. + ssprove_sync. + ssprove_sync. + ssprove_sync => pk_loc. + eapply r_ret. + intuition eauto. + -- repeat ssprove_sync. + intros. + eapply r_get_remember_rhs => sign_loc. + eapply r_put_rhs. + ssprove_restore_mem. + --- ssprove_invariant. + --- eapply r_ret => s0 s1 pre //=. + -- case x => s m. + eapply r_get_remember_lhs => pk. + eapply r_get_remember_rhs => S. + eapply r_ret => s0 s1 pre //=. + split. + --- eapply Signature_prop. + --- by [move: pre; rewrite /inv_conj; repeat case]. Qed. End SignaturePrimitives. diff --git a/theories/extructurespp/fmap.v b/theories/extructurespp/fmap.v index edd6b10..843ba6b 100644 --- a/theories/extructurespp/fmap.v +++ b/theories/extructurespp/fmap.v @@ -235,4 +235,60 @@ Section Facts. by [rewrite (eq_map eid) map_id]. Qed. + Lemma getm_def_seq_step {S T:ordType} {a₀:S*T} {a₁: seq.seq (S*T)} {a₂:S} : + getm_def (fset (a₀ :: a₁)) a₂ = getm_def (a₀ :: (fset a₁)) a₂. + Proof. + Admitted. + + Lemma rem_unit {S T:ordType} {X:eqType} (s:{fmap (S*T) -> X}) (x₁:S) (x₂:T): + (x₁, x₂) \in domm s -> x₁ \in domm (mkfmap (domm s)). + Proof. + move: x₁ x₂. + elim/fmap_ind : s => /=. + - move => x₁ x₂. + by rewrite domm0 in_fset0. + - move => s iH [x₁ x₂] v x_notin_s x₁' x₂'. + rewrite mem_domm mem_domm. + + rewrite setmE. + rewrite domm_set mkfmapE -fset_cons getm_def_seq_step /getm_def. + rewrite -/(getm_def _ x₁') -mkfmapE /=. + + case H: ((x₁',x₂') == (x₁,x₂)). + -- move/eqP:H => H; inversion H. + rewrite ifT //=. + -- rewrite -mem_domm => x'_in_s. + case H_x₁: (x₁' == x₁). + --- by []. + --- specialize (iH x₁' x₂' x'_in_s). + rewrite mem_domm in iH. + exact: iH. + Qed. + + Lemma rem_unit' {S T:ordType} {X:eqType} (s:{fmap (S*T) -> X}) (x₁:S): + x₁ \in domm (mkfmap (domm s)) -> exists (x₂:T), (x₁, x₂) \in domm s. + Proof. + move: x₁. + elim/fmap_ind : s => /=. + - move => x₁. + rewrite mem_domm mkfmapE domm0 //=. + - move => s iH [x₁ x₂] v x_notin_s x₁'. + rewrite mem_domm. + + rewrite domm_set mkfmapE -fset_cons getm_def_seq_step /getm_def -/(getm_def _ x₁') -mkfmapE /=. + + case H_x₁: (x₁' == x₁). + -- move => x_in_s. + exists x₂. + move/eqP:H_x₁ => H_x₁; rewrite H_x₁ //=. + rewrite in_fset. + exact: mem_head. + -- rewrite -mem_domm => x₁'_in_s. + specialize (iH x₁' x₁'_in_s). + case: iH => x₂' iH. + exists x₂'. + rewrite /domm in iH. + by rewrite fset_cons in_fsetU1; apply/orP; right. + Qed. + End Facts.