Commit 9fe06d71 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

update paths

parent 53cb0298
......@@ -2,7 +2,7 @@ Require Import Tweetnacl.Libs.Export.
Require Import Tweetnacl.ListsOp.Export.
Require Import Tweetnacl.Car.Reduce.
Require Import Tweetnacl.Car.Carry_n.
Require Import Tweetnacl.Op.M.
Require Import Tweetnacl.Mid.M.
Require Import stdpp.prelude.
......
Require Import Tweetnacl.Libs.Export.
Require Import Tweetnacl.ListsOp.Export.
Require Import Tweetnacl.Car.Reduce.
Require Import Tweetnacl.Op.M.
Require Import Tweetnacl.Mid.M.
Require Import stdpp.prelude.
......
From Coqprime Require Import PocklingtonRefl.
From Tweetnacl.Montgomery Require Import curve25519_prime_cert.
From mathcomp Require Import ssreflect ssrbool prime.
From Tweetnacl.Montgomery Require Import prime_ssrprime.
From Tweetnacl.High Require Import curve25519_prime_cert prime_ssrprime.
Local Open Scope positive_scope.
Require Import Znat.
......
......@@ -3,9 +3,8 @@ From mathcomp Require Import ssreflect ssrnat ssrbool eqtype fintype.
From mathcomp Require Import tuple seq fintype bigop ssralg finalg.
From mathcomp Require Import ssrfun choice zmodp fingroup.
From SsrMultinomials Require Import mpoly.
From SsrEllipticCurves Require Import polyall polydec ssrring ecgroup.
From SsrEllipticCurves Require Export ec.
From Tweetnacl.Montgomery Require Import mc.
From SsrEllipticCurves Require Import polyall polydec ssrring ecgroup ec.
From Tweetnacl.High Require Import mc.
Import GRing.Theory.
......
......@@ -5,7 +5,7 @@ From mathcomp Require Import choice zmodp fingroup.
From SsrMultinomials Require Import mpoly.
From SsrEllipticCurves Require Import polyall polydec ssrring.
From SsrEllipticCurves Require Export ec.
From Tweetnacl.Montgomery Require Import mc.
From Tweetnacl.High Require Import mc.
Import GRing.Theory.
......
Set Warnings "-notation-overridden,-parsing".
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat div ssralg.
From Tweetnacl.Montgomery Require Import mc.
From Tweetnacl.Montgomery Require Import mcgroup.
From Tweetnacl.Montgomery Require Import ladder.
From Tweetnacl.Montgomery Require Import montgomery.
From Tweetnacl.High Require Import mc.
From Tweetnacl.High Require Import mcgroup.
From Tweetnacl.High Require Import ladder.
From Tweetnacl.High Require Import montgomery.
Import GRing.Theory.
......
default_target: .loadpath Libs ListsOp Op Car Sel Montgomery Unpack
default_target: .loadpath Libs ListsOp Mid Low Car Sel Unpack
all: default_target High
#Note3: for SSReflect, one solution is to install MathComp 1.6
# somewhere add this line to a CONFIGURE file
......@@ -10,36 +12,9 @@ SHOW := $(if $(VERBOSE),@true "",@echo "")
HIDE := $(if $(VERBOSE),,@)
DIRS= Libs ListsOp Op Car Sel Montgomery Unpack
DIRS= Libs ListsOp Mid Car Sel High Unpack
INCLUDE= $(foreach a,$(DIRS),$(if $(wildcard $(a)), -Q $(a) $(a)))
COQSTDPP = ../coq-stdpp/theories
COQPRIME = Coqprime
# for Coq-stdpp
ifdef COQSTDPP
EXTFLAGS:=$(EXTFLAGS) -R $(COQSTDPP) stdpp
endif
# for Coq-stdpp
ifdef COQPRIME
EXTFLAGS:=$(EXTFLAGS) -R $(COQPRIME)/Tactic Coqprime
EXTFLAGS:=$(EXTFLAGS) -R $(COQPRIME)/N Coqprime
EXTFLAGS:=$(EXTFLAGS) -R $(COQPRIME)/Z Coqprime
EXTFLAGS:=$(EXTFLAGS) -R $(COQPRIME)/List Coqprime
EXTFLAGS:=$(EXTFLAGS) -R $(COQPRIME)/PrimalityTest Coqprime
EXTFLAGS:=$(EXTFLAGS) -R $(COQPRIME)/elliptic Coqprime
EXTFLAGS:=$(EXTFLAGS) -R $(COQPRIME)/num Coqprime
EXTFLAGS:=$(EXTFLAGS) -R $(COQPRIME)/examples Coqprime
endif
# for SSReflect
ifdef MATHCOMP
EXTFLAGS:=$(EXTFLAGS) -R $(MATHCOMP) mathcomp
endif
COQFLAGS=$(foreach d, $(DIRS), $(if $(wildcard $(d)), -Q $(d) $(d))) $(EXTFLAGS)
LIBPREFIX=Tweetnacl
......@@ -53,44 +28,25 @@ COQTOP=$(COQBIN)coqtop
COQDEP=$(COQBIN)coqdep $(DEPFLAGS)
COQDOC=$(COQBIN)coqdoc -d doc -g -utf8 $(DEPFLAGS)
COQVERSION= 8.6.1 or-else 8.7.0
COQVERSION= 8.7.0
COQV=$(shell $(COQC) -v)
ifeq ("$(filter $(COQVERSION),$(COQV))","")
$(error FAILURE: You need Coq $(COQVERSION) but you have this version: $(COQV))
endif
define clean_files
$($(1):%.v=$(2)/%.v.d) \
$($(1):%.v=$(2)/%.vio) \
$($(1):%.v=$(2)/%.vo) \
$($(1):%.v=$(2)/.%.aux) \
$($(1):%.v=$(2)/.%.vo.aux) \
$($(1):%.v=$(2)/%.glob) \
$($(1):%.v=$(2)/%.v.crashcoqide)
endef
LIBS_FILES = $(wildcard Libs/*.v)
LISTSOP_FILES = $(wildcard ListsOp/*.v)
MID_FILES = $(wildcard Mid/*.v)
CAR_FILES = $(wildcard Car/*.v)
SEL_FILES = $(wildcard Sel/*.v)
UNPACK_FILES = $(wildcard Unpack/*.v)
HIGH_FILES = $(wildcard High/*.v)
COUNTFILES = $(LIBS_FILES) $(LISTSOP_FILES) $(MID_FILES) $(CAR_FILES) \
$(SEL_FILES) $(UNPACK_FILES)
LIBS_FILES = $(notdir $(wildcard Libs/*.v))
LISTSOP_FILES = $(notdir $(wildcard ListsOp/*.v))
OP_FILES = $(notdir $(wildcard Op/*.v))
CAR_FILES = $(notdir $(wildcard Car/*.v))
SEL_FILES = $(notdir $(wildcard Sel/*.v))
UNPACK_FILES = $(notdir $(wildcard Unpack/*.v))
MONTGOMERY_FILES = $(notdir $(wildcard Montgomery/*.v))
COUNTFILES = \
$(LIBS_FILES:%=Libs/%) \
$(LISTSOP_FILES:%=ListsOp/%) \
$(OP_FILES:%=Op/%) \
$(CAR_FILES:%=Car/%) \
$(SEL_FILES:%=Sel/%) \
$(UNPACK_FILES:%=Unpack/%) \
FILES = \
$(COUNTFILES) \
$(MONTGOMERY_FILES:%=Montgomery/%) \
FILES = $(COUNTFILES) $(HIGH_FILES)
ifneq ($(filter-out archclean clean cleanall printenv count,$(MAKECMDGOALS)),)
-include $(addsuffix .d,$(FILES))
......@@ -100,15 +56,6 @@ ifeq ($(MAKECMDGOALS),)
endif
endif
CLEANFILES = \
$(call clean_files,LIBS_FILES,Libs) \
$(call clean_files,LISTSOP_FILES,ListsOp) \
$(call clean_files,OP_FILES,Op) \
$(call clean_files,CAR_FILES,Car) \
$(call clean_files,SEL_FILES,Sel) \
$(call clean_files,UNPACK_FILES,Unpack) \
$(call clean_files,MONTGOMERY_FILES,Montgomery)
%_stripped.v: %.v
# e.g., 'make progs/verif_reverse_stripped.v will remove the tutorial comments
# from progs/verif_reverse.v
......@@ -137,13 +84,13 @@ endif
all: .loadpath $(FILES:.v=.vo)
quick: .loadpath $(FILES:.v=.vio)
Libs: .loadpath $(LIBS_FILES:%.v=Libs/%.vo)
ListsOp: .loadpath $(LISTSOP_FILES:%.v=ListsOp/%.vo)
Op: .loadpath $(OP_FILES:%.v=Op/%.vo)
Car: .loadpath $(CAR_FILES:%.v=Car/%.vo)
Sel: .loadpath $(SEL_FILES:%.v=Sel/%.vo)
Unpack: .loadpath $(UNPACK_FILES:%.v=Unpack/%.vo)
Montgomery: .loadpath $(MONTGOMERY_FILES:%.v=Montgomery/%.vo)
Libs: .loadpath $(LIBS_FILES:%.v=%.vo)
ListsOp: .loadpath $(LISTSOP_FILES:%.v=%.vo)
Mid: .loadpath $(MID_FILES:%.v=%.vo)
Car: .loadpath $(CAR_FILES:%.v=%.vo)
Sel: .loadpath $(SEL_FILES:%.v=%.vo)
Unpack: .loadpath $(UNPACK_FILES:%.v=%.vo)
High: .loadpath $(HIGH_FILES:%.v=%.vo)
_CoqProject: Makefile
$(SHOW)Generate _CoqProject
......@@ -164,7 +111,7 @@ $(addsuffix .d,$(FILES)): %.v.d: %.v
clean:
$(SHOW)cleaning files...
$(HIDE)rm -f $(CLEANFILES) .loadpath _CoqProject .depend .nia.cache .lia.cache
$(HIDE)rm -f $(wildcard */*.d) $(wildcard */*.vo) $(wildcard */*.glob) $(wildcard */.*.aux) .loadpath _CoqProject .depend .nia.cache .lia.cache
# check: quick
# coqtop -schedule-vio2vo
......
Require Import Tweetnacl.Libs.Export.
Require Import Tweetnacl.ListsOp.Export.
Require Export Tweetnacl.Op.SumList.
Require Export Tweetnacl.Mid.SumList.
Require Import stdpp.prelude.
Open Scope Z.
......
Require Export Tweetnacl.Mid.SumList.
Require Export Tweetnacl.Mid.SubList.
Require Export Tweetnacl.Mid.MinusList.
Require Export Tweetnacl.Mid.ScalarMult.
Require Export Tweetnacl.Mid.A.
Require Export Tweetnacl.Mid.M.
Require Export Tweetnacl.Mid.Inner_M1.
Require Export Tweetnacl.Mid.Outer_M1.
Require Export Tweetnacl.Mid.M_low_level.
Require Export Tweetnacl.Mid.M_low_level_compute.
\ No newline at end of file
Require Import Tweetnacl.Libs.Export.
Require Import Tweetnacl.ListsOp.Export.
Require Import Tweetnacl.Op.ScalarMult.
Require Import Tweetnacl.Op.A.
Require Import Tweetnacl.Mid.ScalarMult.
Require Import Tweetnacl.Mid.A.
Require Import stdpp.prelude.
Local Open Scope Z.
......
Require Import Tweetnacl.Libs.Export.
Require Import Tweetnacl.ListsOp.Export.
Require Import Tweetnacl.Op.Inner_M1.
Require Import Tweetnacl.Op.Outer_M1.
Require Import Tweetnacl.Op.M.
Require Import Tweetnacl.Mid.Inner_M1.
Require Import Tweetnacl.Mid.Outer_M1.
Require Import Tweetnacl.Mid.M.
Require Import stdpp.prelude.
Require Import Recdef.
......
Require Import Tweetnacl.Libs.Export.
Require Import stdpp.prelude.
Require Import Tweetnacl.Op.Inner_M1.
Require Import Tweetnacl.Op.Outer_M1.
Require Import Tweetnacl.Mid.Inner_M1.
Require Import Tweetnacl.Mid.Outer_M1.
Local Open Scope Z.
......
Require Import Tweetnacl.Libs.Export.
Require Import Tweetnacl.Op.Inner_M1.
Require Import Tweetnacl.Mid.Inner_M1.
Require Import stdpp.prelude.
Require Import Recdef.
......
Require Import Tweetnacl.Libs.Export.
Require Import Tweetnacl.ListsOp.Export.
Require Import Tweetnacl.Op.MinusList.
Require Import Tweetnacl.Mid.MinusList.
Require Import stdpp.prelude.
Import ListNotations.
......
Require Import Tweetnacl.Libs.Export.
Require Import Tweetnacl.ListsOp.Export.
Require Export Tweetnacl.Op.SubList.
Require Import Tweetnacl.Op.MinusList.
Require Export Tweetnacl.Mid.SubList.
Require Import Tweetnacl.Mid.MinusList.
Require Import stdpp.prelude.
Open Scope Z.
......
Require Export Tweetnacl.Op.SumList.
Require Export Tweetnacl.Op.SubList.
Require Export Tweetnacl.Op.MinusList.
Require Export Tweetnacl.Op.ScalarMult.
Require Export Tweetnacl.Op.A.
Require Export Tweetnacl.Op.M.
Require Export Tweetnacl.Op.Inner_M1.
Require Export Tweetnacl.Op.Outer_M1.
Require Export Tweetnacl.Op.M_low_level.
Require Export Tweetnacl.Op.M_low_level_compute.
\ No newline at end of file
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment