diff options
-rw-r--r-- | .gitignore | 38 | ||||
-rw-r--r-- | Makefile | 42 | ||||
-rw-r--r-- | README.md | 10 | ||||
-rw-r--r-- | _CoqProject | 76 | ||||
-rw-r--r-- | src/AbstractInterpretation.v (renamed from src/Experiments/NewPipeline/AbstractInterpretation.v) | 4 | ||||
-rw-r--r-- | src/AbstractInterpretationProofs.v (renamed from src/Experiments/NewPipeline/AbstractInterpretationProofs.v) | 16 | ||||
-rw-r--r-- | src/AbstractInterpretationWf.v (renamed from src/Experiments/NewPipeline/AbstractInterpretationWf.v) | 12 | ||||
-rw-r--r-- | src/AbstractInterpretationZRangeProofs.v (renamed from src/Experiments/NewPipeline/AbstractInterpretationZRangeProofs.v) | 4 | ||||
-rw-r--r-- | src/Arithmetic.v (renamed from src/Experiments/NewPipeline/Arithmetic.v) | 0 | ||||
-rw-r--r-- | src/BoundsPipeline.v (renamed from src/Experiments/NewPipeline/BoundsPipeline.v) | 48 | ||||
-rw-r--r-- | src/CLI.v (renamed from src/Experiments/NewPipeline/CLI.v) | 6 | ||||
-rw-r--r-- | src/COperationSpecifications.v (renamed from src/Experiments/NewPipeline/COperationSpecifications.v) | 2 | ||||
-rw-r--r-- | src/CStringification.v (renamed from src/Experiments/NewPipeline/CStringification.v) | 4 | ||||
-rw-r--r-- | src/CompilersTestCases.v (renamed from src/Experiments/NewPipeline/CompilersTestCases.v) | 12 | ||||
-rw-r--r-- | src/ExtractionHaskell/saturated_solinas.v (renamed from src/Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.v) | 2 | ||||
-rw-r--r-- | src/ExtractionHaskell/unsaturated_solinas.v (renamed from src/Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.v) | 2 | ||||
-rw-r--r-- | src/ExtractionHaskell/word_by_word_montgomery.v (renamed from src/Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.v) | 2 | ||||
-rw-r--r-- | src/ExtractionOCaml/saturated_solinas.v (renamed from src/Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.v) | 2 | ||||
-rw-r--r-- | src/ExtractionOCaml/unsaturated_solinas.v (renamed from src/Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.v) | 2 | ||||
-rw-r--r-- | src/ExtractionOCaml/word_by_word_montgomery.v (renamed from src/Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.v) | 2 | ||||
-rw-r--r-- | src/GENERATEDIdentifiersWithoutTypes.v (renamed from src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v) | 4 | ||||
-rw-r--r-- | src/GENERATEDIdentifiersWithoutTypesProofs.v (renamed from src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.v) | 6 | ||||
-rw-r--r-- | src/Language.v (renamed from src/Experiments/NewPipeline/Language.v) | 0 | ||||
-rw-r--r-- | src/LanguageInversion.v (renamed from src/Experiments/NewPipeline/LanguageInversion.v) | 2 | ||||
-rw-r--r-- | src/LanguageWf.v (renamed from src/Experiments/NewPipeline/LanguageWf.v) | 4 | ||||
-rw-r--r-- | src/MiscCompilerPasses.v (renamed from src/Experiments/NewPipeline/MiscCompilerPasses.v) | 2 | ||||
-rw-r--r-- | src/MiscCompilerPassesProofs.v (renamed from src/Experiments/NewPipeline/MiscCompilerPassesProofs.v) | 8 | ||||
-rw-r--r-- | src/PushButtonSynthesis.v (renamed from src/Experiments/NewPipeline/PushButtonSynthesis.v) | 16 | ||||
-rw-r--r-- | src/PushButtonSynthesis/ReificationCache.v (renamed from src/Experiments/NewPipeline/PushButtonSynthesis/ReificationCache.v) | 4 | ||||
-rw-r--r-- | src/README.md (renamed from src/Experiments/NewPipeline/README.md) | 0 | ||||
-rw-r--r-- | src/Rewriter.v (renamed from src/Experiments/NewPipeline/Rewriter.v) | 6 | ||||
-rw-r--r-- | src/RewriterInterpProofs1.v (renamed from src/Experiments/NewPipeline/RewriterInterpProofs1.v) | 14 | ||||
-rw-r--r-- | src/RewriterProofs.v (renamed from src/Experiments/NewPipeline/RewriterProofs.v) | 22 | ||||
-rw-r--r-- | src/RewriterRulesGood.v (renamed from src/Experiments/NewPipeline/RewriterRulesGood.v) | 14 | ||||
-rw-r--r-- | src/RewriterRulesInterpGood.v (renamed from src/Experiments/NewPipeline/RewriterRulesInterpGood.v) | 14 | ||||
-rw-r--r-- | src/RewriterWf1.v (renamed from src/Experiments/NewPipeline/RewriterWf1.v) | 12 | ||||
-rw-r--r-- | src/RewriterWf2.v (renamed from src/Experiments/NewPipeline/RewriterWf2.v) | 14 | ||||
-rw-r--r-- | src/SlowPrimeSynthesisExamples.v (renamed from src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v) | 6 | ||||
-rw-r--r-- | src/StandaloneHaskellMain.v (renamed from src/Experiments/NewPipeline/StandaloneHaskellMain.v) | 4 | ||||
-rw-r--r-- | src/StandaloneOCamlMain.v (renamed from src/Experiments/NewPipeline/StandaloneOCamlMain.v) | 4 | ||||
-rw-r--r-- | src/Toplevel2.v (renamed from src/Experiments/NewPipeline/Toplevel2.v) | 32 | ||||
-rw-r--r-- | src/UnderLets.v (renamed from src/Experiments/NewPipeline/UnderLets.v) | 2 | ||||
-rw-r--r-- | src/UnderLetsProofs.v (renamed from src/Experiments/NewPipeline/UnderLetsProofs.v) | 8 | ||||
-rw-r--r-- | src/arith_rewrite_head.out (renamed from src/Experiments/NewPipeline/arith_rewrite_head.out) | 0 | ||||
-rw-r--r-- | src/arith_with_casts_rewrite_head.out (renamed from src/Experiments/NewPipeline/arith_with_casts_rewrite_head.out) | 0 | ||||
-rw-r--r-- | src/fancy_rewrite_head.out (renamed from src/Experiments/NewPipeline/fancy_rewrite_head.out) | 0 | ||||
-rw-r--r-- | src/fancy_with_casts_rewrite_head.out (renamed from src/Experiments/NewPipeline/fancy_with_casts_rewrite_head.out) | 0 | ||||
-rw-r--r-- | src/haskell.sed (renamed from src/Experiments/NewPipeline/haskell.sed) | 0 | ||||
-rw-r--r-- | src/nbe_rewrite_head.out (renamed from src/Experiments/NewPipeline/nbe_rewrite_head.out) | 0 |
49 files changed, 245 insertions, 239 deletions
diff --git a/.gitignore b/.gitignore index 0a1bc5a54..0a28789cd 100644 --- a/.gitignore +++ b/.gitignore @@ -110,22 +110,22 @@ third_party/openssl-nistz256-adx/measure third_party/openssl-nistz256-amd64/measure third_party/openssl-nistz256/measure third_party/curve25519-donna-c64/measure -src/Experiments/NewPipeline/ExtractionHaskell/saturated_solinas -src/Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas -src/Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery -src/Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.exe -src/Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.exe -src/Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.exe -src/Experiments/NewPipeline/ExtractionHaskell/*.hi -src/Experiments/NewPipeline/ExtractionHaskell/*.hs -src/Experiments/NewPipeline/ExtractionHaskell/*.o -src/Experiments/NewPipeline/ExtractionOCaml/saturated_solinas -src/Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas -src/Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery -src/Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.exe -src/Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.exe -src/Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.exe -src/Experiments/NewPipeline/ExtractionOCaml/*.cmi -src/Experiments/NewPipeline/ExtractionOCaml/*.cmx -src/Experiments/NewPipeline/ExtractionOCaml/*.ml -src/Experiments/NewPipeline/ExtractionOCaml/*.o +src/ExtractionHaskell/saturated_solinas +src/ExtractionHaskell/unsaturated_solinas +src/ExtractionHaskell/word_by_word_montgomery +src/ExtractionHaskell/saturated_solinas.exe +src/ExtractionHaskell/unsaturated_solinas.exe +src/ExtractionHaskell/word_by_word_montgomery.exe +src/ExtractionHaskell/*.hi +src/ExtractionHaskell/*.hs +src/ExtractionHaskell/*.o +src/ExtractionOCaml/saturated_solinas +src/ExtractionOCaml/unsaturated_solinas +src/ExtractionOCaml/word_by_word_montgomery +src/ExtractionOCaml/saturated_solinas.exe +src/ExtractionOCaml/unsaturated_solinas.exe +src/ExtractionOCaml/word_by_word_montgomery.exe +src/ExtractionOCaml/*.cmi +src/ExtractionOCaml/*.cmx +src/ExtractionOCaml/*.ml +src/ExtractionOCaml/*.o @@ -78,12 +78,12 @@ UNMADE_C_FILES := \ # files that are treated specially SPECIAL_VOFILES := \ src/Specific/%Display.vo \ - src/Experiments/NewPipeline/ExtractionOCaml/%.vo \ - src/Experiments/NewPipeline/ExtractionHaskell/%.vo + src/ExtractionOCaml/%.vo \ + src/ExtractionHaskell/%.vo SPECIFIC_GENERATED_VOFILES := src/Specific/solinas%.vo src/Specific/montgomery%.vo # add files to this list to prevent them from being built as final # targets by the "lite" target -NEW_PIPELINE_FILTER := src/Experiments/NewPipeline/% +NEW_PIPELINE_FILTER := src/% LITE_UNMADE_VOFILES := src/Curves/Weierstrass/AffineProofs.vo \ src/Curves/Weierstrass/Jacobian.vo \ src/Curves/Weierstrass/Projective.vo \ @@ -92,12 +92,12 @@ LITE_UNMADE_VOFILES := src/Curves/Weierstrass/AffineProofs.vo \ src/Specific/NISTP256/AMD128/fe%.vo \ src/Specific/X25519/C64/ladderstep.vo \ src/Specific/X25519/C32/fe%.vo \ - src/Experiments/NewPipeline/RewriterWf1.vo \ - src/Experiments/NewPipeline/RewriterWf2.vo \ - src/Experiments/NewPipeline/RewriterRulesGood.vo \ - src/Experiments/NewPipeline/RewriterProofs.vo \ - src/Experiments/NewPipeline/Toplevel2.vo \ - src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo \ + src/RewriterWf1.vo \ + src/RewriterWf2.vo \ + src/RewriterRulesGood.vo \ + src/RewriterProofs.vo \ + src/Toplevel2.vo \ + src/SlowPrimeSynthesisExamples.vo \ src/Experiments/SimplyTypedArithmetic.vo \ $(SPECIFIC_GENERATED_VOFILES) NOBIGMEM_UNMADE_VOFILES := \ @@ -114,12 +114,12 @@ NO_CURVES_PROOFS_UNMADE_VOFILES := src/Curves/Weierstrass/AffineProofs.vo \ NO_CURVES_PROOFS_NON_SPECIFIC_UNMADE_VOFILES := $(filter $(NO_CURVES_PROOFS_UNMADE_VOFILES) src/Specific/%.vo,$(VOFILES)) REAL_SPECIFIC_GENERATED_VOFILES := $(filter $(SPECIFIC_GENERATED_VOFILES),$(VOFILES)) NEW_PIPELINE_PRE_VOFILES := $(filter $(NEW_PIPELINE_FILTER),$(REGULAR_VOFILES)) -PRE_STANDALONE_PRE_VOFILES := $(filter src/Experiments/NewPipeline/Standalone%.vo,$(REGULAR_VOFILES)) +PRE_STANDALONE_PRE_VOFILES := $(filter src/Standalone%.vo,$(REGULAR_VOFILES)) UTIL_PRE_VOFILES := $(filter bbv/%.vo src/Algebra/%.vo src/Tactics/%.vo src/Util/%.vo,$(REGULAR_VOFILES)) COQ_WITHOUT_NEW_PIPELINE_VOFILES := $(filter-out $(NEW_PIPELINE_FILTER),$(REGULAR_VOFILES)) SOME_EARLY_VOFILES := \ - src/Experiments/NewPipeline/Arithmetic.vo \ - src/Experiments/NewPipeline/Rewriter.vo \ + src/Arithmetic.vo \ + src/Rewriter.vo \ src/Experiments/SimplyTypedArithmetic.vo SELECTED_PATTERN := \ @@ -543,33 +543,33 @@ STANDALONE := \ saturated_solinas \ word_by_word_montgomery -$(STANDALONE:%=src/Experiments/NewPipeline/ExtractionOCaml/%.ml) : %.ml : %.v src/Experiments/NewPipeline/StandaloneOCamlMain.vo +$(STANDALONE:%=src/ExtractionOCaml/%.ml) : %.ml : %.v src/StandaloneOCamlMain.vo $(SHOW)'COQC $< > $@' $(HIDE)$(TIMER_FULL) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< > $@.tmp $(HIDE)sed 's/\r\n/\n/g; s/\r//g' $@.tmp > $@ && rm -f $@.tmp -$(STANDALONE:%=src/Experiments/NewPipeline/ExtractionHaskell/%.hs) : %.hs : %.v src/Experiments/NewPipeline/StandaloneHaskellMain.vo src/Experiments/NewPipeline/haskell.sed +$(STANDALONE:%=src/ExtractionHaskell/%.hs) : %.hs : %.v src/StandaloneHaskellMain.vo src/haskell.sed $(SHOW)'COQC $< > $@' $(HIDE)$(TIMER_FULL) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< > $@.tmp - $(HIDE)sed 's/\r\n/\n/g; s/\r//g' $@.tmp | sed -f src/Experiments/NewPipeline/haskell.sed > $@ && rm -f $@.tmp + $(HIDE)sed 's/\r\n/\n/g; s/\r//g' $@.tmp | sed -f src/haskell.sed > $@ && rm -f $@.tmp # pass -w -20 to disable the unused argument warning -$(STANDALONE:%=src/Experiments/NewPipeline/ExtractionOCaml/%) : % : %.ml +$(STANDALONE:%=src/ExtractionOCaml/%) : % : %.ml $(TIMER_FULL) ocamlopt -w -20 -o $@ $< -$(STANDALONE:%=src/Experiments/NewPipeline/ExtractionHaskell/%) : % : %.hs +$(STANDALONE:%=src/ExtractionHaskell/%) : % : %.hs $(TIMER_FULL) $(GHC) $(GHCFLAGS) -o $@ $< standalone: standalone-haskell standalone-ocaml -standalone-haskell: $(STANDALONE:%=src/Experiments/NewPipeline/ExtractionHaskell/%) -standalone-ocaml: $(STANDALONE:%=src/Experiments/NewPipeline/ExtractionOCaml/%) +standalone-haskell: $(STANDALONE:%=src/ExtractionHaskell/%) +standalone-ocaml: $(STANDALONE:%=src/ExtractionOCaml/%) UNSATURATED_SOLINAS_C_FILES := curve25519_64.c curve25519_32.c p521_64.c p521_32.c # p224_solinas_64.c WORD_BY_WORD_MONTGOMERY_C_FILES := p256_64.c p256_32.c p384_64.c p384_32.c secp256k1_64.c secp256k1_32.c p224_64.c p224_32.c FUNCTIONS_FOR_25519 := carry_mul carry_square carry_scmul121666 carry add sub opp selectznz to_bytes from_bytes -UNSATURATED_SOLINAS := src/Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas -WORD_BY_WORD_MONTGOMERY := src/Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery +UNSATURATED_SOLINAS := src/ExtractionOCaml/unsaturated_solinas +WORD_BY_WORD_MONTGOMERY := src/ExtractionOCaml/word_by_word_montgomery ALL_C_FILES := $(UNSATURATED_SOLINAS_C_FILES) $(WORD_BY_WORD_MONTGOMERY_C_FILES) .PHONY: c-files c-files: $(ALL_C_FILES) @@ -1,8 +1,14 @@ -[![Build Status](https://api.travis-ci.org/mit-plv/fiat-crypto.png?branch=master)](https://travis-ci.org/mit-plv/fiat-crypto) - Fiat-Crypto: Synthesizing Correct-by-Construction Code for Cryptographic Primitives ===== +[![Build Status](https://api.travis-ci.org/mit-plv/fiat-crypto.png?branch=master)](https://travis-ci.org/mit-plv/fiat-crypto) + +See [src/README.md](src/README.md). + +OLD PIPELINE README BELOW +========================= + + Build Requirements ----- This repository requires: diff --git a/_CoqProject b/_CoqProject index 77482ceb2..5cb9ea44c 100644 --- a/_CoqProject +++ b/_CoqProject @@ -16,7 +16,38 @@ bbv/theories/Word.v bbv/theories/WordScope.v bbv/theories/ZHints.v bbv/theories/ZLib.v +src/AbstractInterpretation.v +src/AbstractInterpretationProofs.v +src/AbstractInterpretationWf.v +src/AbstractInterpretationZRangeProofs.v +src/Arithmetic.v +src/BoundsPipeline.v +src/CLI.v +src/COperationSpecifications.v +src/CStringification.v +src/CompilersTestCases.v src/Demo.v +src/GENERATEDIdentifiersWithoutTypes.v +src/GENERATEDIdentifiersWithoutTypesProofs.v +src/Language.v +src/LanguageInversion.v +src/LanguageWf.v +src/MiscCompilerPasses.v +src/MiscCompilerPassesProofs.v +src/PushButtonSynthesis.v +src/Rewriter.v +src/RewriterInterpProofs1.v +src/RewriterProofs.v +src/RewriterRulesGood.v +src/RewriterRulesInterpGood.v +src/RewriterWf1.v +src/RewriterWf2.v +src/SlowPrimeSynthesisExamples.v +src/StandaloneHaskellMain.v +src/StandaloneOCamlMain.v +src/Toplevel2.v +src/UnderLets.v +src/UnderLetsProofs.v src/Algebra/Field.v src/Algebra/Field_test.v src/Algebra/Group.v @@ -246,44 +277,12 @@ src/Curves/Weierstrass/Jacobian.v src/Curves/Weierstrass/Projective.v src/Experiments/PartialEvaluationWithLetIn.v src/Experiments/SimplyTypedArithmetic.v -src/Experiments/NewPipeline/AbstractInterpretation.v -src/Experiments/NewPipeline/AbstractInterpretationProofs.v -src/Experiments/NewPipeline/AbstractInterpretationWf.v -src/Experiments/NewPipeline/AbstractInterpretationZRangeProofs.v -src/Experiments/NewPipeline/Arithmetic.v -src/Experiments/NewPipeline/BoundsPipeline.v -src/Experiments/NewPipeline/CLI.v -src/Experiments/NewPipeline/COperationSpecifications.v -src/Experiments/NewPipeline/CStringification.v -src/Experiments/NewPipeline/CompilersTestCases.v -src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v -src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.v -src/Experiments/NewPipeline/Language.v -src/Experiments/NewPipeline/LanguageInversion.v -src/Experiments/NewPipeline/LanguageWf.v -src/Experiments/NewPipeline/MiscCompilerPasses.v -src/Experiments/NewPipeline/MiscCompilerPassesProofs.v -src/Experiments/NewPipeline/PushButtonSynthesis.v -src/Experiments/NewPipeline/Rewriter.v -src/Experiments/NewPipeline/RewriterInterpProofs1.v -src/Experiments/NewPipeline/RewriterProofs.v -src/Experiments/NewPipeline/RewriterRulesGood.v -src/Experiments/NewPipeline/RewriterRulesInterpGood.v -src/Experiments/NewPipeline/RewriterWf1.v -src/Experiments/NewPipeline/RewriterWf2.v -src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v -src/Experiments/NewPipeline/StandaloneHaskellMain.v -src/Experiments/NewPipeline/StandaloneOCamlMain.v -src/Experiments/NewPipeline/Toplevel2.v -src/Experiments/NewPipeline/UnderLets.v -src/Experiments/NewPipeline/UnderLetsProofs.v -src/Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.v -src/Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.v -src/Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.v -src/Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.v -src/Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.v -src/Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.v -src/Experiments/NewPipeline/PushButtonSynthesis/ReificationCache.v +src/ExtractionHaskell/saturated_solinas.v +src/ExtractionHaskell/unsaturated_solinas.v +src/ExtractionHaskell/word_by_word_montgomery.v +src/ExtractionOCaml/saturated_solinas.v +src/ExtractionOCaml/unsaturated_solinas.v +src/ExtractionOCaml/word_by_word_montgomery.v src/LegacyArithmetic/ArchitectureToZLike.v src/LegacyArithmetic/ArchitectureToZLikeProofs.v src/LegacyArithmetic/BarretReduction.v @@ -311,6 +310,7 @@ src/LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v src/LegacyArithmetic/Double/Proofs/SpreadLeftImmediate.v src/Primitives/EdDSARepChange.v src/Primitives/MxDHRepChange.v +src/PushButtonSynthesis/ReificationCache.v src/Spec/CompleteEdwardsCurve.v src/Spec/Ed25519.v src/Spec/EdDSA.v diff --git a/src/Experiments/NewPipeline/AbstractInterpretation.v b/src/AbstractInterpretation.v index 0e5a0e9dd..463cc72cd 100644 --- a/src/Experiments/NewPipeline/AbstractInterpretation.v +++ b/src/AbstractInterpretation.v @@ -6,8 +6,8 @@ Require Import Crypto.Util.Option. Require Import Crypto.Util.OptionList. Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Require Import Crypto.Util.LetIn. -Require Import Crypto.Experiments.NewPipeline.Language. -Require Import Crypto.Experiments.NewPipeline.UnderLets. +Require Import Crypto.Language. +Require Import Crypto.UnderLets. Import ListNotations. Local Open Scope bool_scope. Local Open Scope Z_scope. Module Compilers. diff --git a/src/Experiments/NewPipeline/AbstractInterpretationProofs.v b/src/AbstractInterpretationProofs.v index 0e7d55c7a..6bf479dfe 100644 --- a/src/Experiments/NewPipeline/AbstractInterpretationProofs.v +++ b/src/AbstractInterpretationProofs.v @@ -33,13 +33,13 @@ Require Import Crypto.Util.Tactics.SpecializeBy. Require Import Crypto.Util.Tactics.SpecializeAllWays. Require Import Crypto.Util.Tactics.Head. Require Import Crypto.Util.Tactics.DoWithHyp. -Require Import Crypto.Experiments.NewPipeline.Language. -Require Import Crypto.Experiments.NewPipeline.LanguageInversion. -Require Import Crypto.Experiments.NewPipeline.LanguageWf. -Require Import Crypto.Experiments.NewPipeline.UnderLetsProofs. -Require Import Crypto.Experiments.NewPipeline.AbstractInterpretation. -Require Import Crypto.Experiments.NewPipeline.AbstractInterpretationWf. -Require Import Crypto.Experiments.NewPipeline.AbstractInterpretationZRangeProofs. +Require Import Crypto.Language. +Require Import Crypto.LanguageInversion. +Require Import Crypto.LanguageWf. +Require Import Crypto.UnderLetsProofs. +Require Import Crypto.AbstractInterpretation. +Require Import Crypto.AbstractInterpretationWf. +Require Import Crypto.AbstractInterpretationZRangeProofs. Module Compilers. Import Language.Compilers. @@ -62,7 +62,7 @@ Module Compilers. Module Import partial. Import AbstractInterpretation.Compilers.partial. - Import NewPipeline.UnderLets.Compilers.UnderLets. + Import UnderLets.Compilers.UnderLets. Section with_type. Context {base_type : Type}. Local Notation type := (type base_type). diff --git a/src/Experiments/NewPipeline/AbstractInterpretationWf.v b/src/AbstractInterpretationWf.v index ee69313c3..a2ba63c01 100644 --- a/src/Experiments/NewPipeline/AbstractInterpretationWf.v +++ b/src/AbstractInterpretationWf.v @@ -18,11 +18,11 @@ Require Import Crypto.Util.Tactics.SplitInContext. Require Import Crypto.Util.Tactics.UniquePose. Require Import Crypto.Util.Tactics.SpecializeBy. Require Import Crypto.Util.Tactics.SpecializeAllWays. -Require Import Crypto.Experiments.NewPipeline.Language. -Require Import Crypto.Experiments.NewPipeline.LanguageInversion. -Require Import Crypto.Experiments.NewPipeline.LanguageWf. -Require Import Crypto.Experiments.NewPipeline.UnderLetsProofs. -Require Import Crypto.Experiments.NewPipeline.AbstractInterpretation. +Require Import Crypto.Language. +Require Import Crypto.LanguageInversion. +Require Import Crypto.LanguageWf. +Require Import Crypto.UnderLetsProofs. +Require Import Crypto.AbstractInterpretation. Module Compilers. Import Language.Compilers. @@ -35,7 +35,7 @@ Module Compilers. Module Import partial. Import AbstractInterpretation.Compilers.partial. - Import NewPipeline.UnderLets.Compilers.UnderLets. + Import UnderLets.Compilers.UnderLets. Section with_type. Context {base_type : Type}. Local Notation type := (type base_type). diff --git a/src/Experiments/NewPipeline/AbstractInterpretationZRangeProofs.v b/src/AbstractInterpretationZRangeProofs.v index 32fe5b526..0cafa6dda 100644 --- a/src/Experiments/NewPipeline/AbstractInterpretationZRangeProofs.v +++ b/src/AbstractInterpretationZRangeProofs.v @@ -36,8 +36,8 @@ Require Import Crypto.Util.Tactics.UniquePose. Require Import Crypto.Util.Tactics.SpecializeBy. Require Import Crypto.Util.Tactics.SpecializeAllWays. Require Import Crypto.Util.Tactics.Head. -Require Import Crypto.Experiments.NewPipeline.LanguageWf. -Require Import Crypto.Experiments.NewPipeline.AbstractInterpretation. +Require Import Crypto.LanguageWf. +Require Import Crypto.AbstractInterpretation. Module Compilers. Import LanguageWf.Compilers. diff --git a/src/Experiments/NewPipeline/Arithmetic.v b/src/Arithmetic.v index 5af73875b..5af73875b 100644 --- a/src/Experiments/NewPipeline/Arithmetic.v +++ b/src/Arithmetic.v diff --git a/src/Experiments/NewPipeline/BoundsPipeline.v b/src/BoundsPipeline.v index 7c6fb6b00..2b74545f3 100644 --- a/src/Experiments/NewPipeline/BoundsPipeline.v +++ b/src/BoundsPipeline.v @@ -20,34 +20,34 @@ Require Import Crypto.Util.Tactics.HasBody. Require Import Crypto.Util.Tactics.Head. Require Import Crypto.Util.Tactics.SpecializeBy. Require Import Crypto.Util.Tactics.SplitInContext. -Require Crypto.Experiments.NewPipeline.Language. -Require Crypto.Experiments.NewPipeline.UnderLets. -Require Crypto.Experiments.NewPipeline.AbstractInterpretation. -Require Crypto.Experiments.NewPipeline.Rewriter. -Require Crypto.Experiments.NewPipeline.MiscCompilerPasses. -Require Crypto.Experiments.NewPipeline.CStringification. -Require Crypto.Experiments.NewPipeline.LanguageWf. -Require Crypto.Experiments.NewPipeline.UnderLetsProofs. -Require Crypto.Experiments.NewPipeline.MiscCompilerPassesProofs. -Require Crypto.Experiments.NewPipeline.RewriterProofs. -Require Crypto.Experiments.NewPipeline.AbstractInterpretationWf. -Require Crypto.Experiments.NewPipeline.AbstractInterpretationProofs. +Require Crypto.Language. +Require Crypto.UnderLets. +Require Crypto.AbstractInterpretation. +Require Crypto.Rewriter. +Require Crypto.MiscCompilerPasses. +Require Crypto.CStringification. +Require Crypto.LanguageWf. +Require Crypto.UnderLetsProofs. +Require Crypto.MiscCompilerPassesProofs. +Require Crypto.RewriterProofs. +Require Crypto.AbstractInterpretationWf. +Require Crypto.AbstractInterpretationProofs. Require Import Crypto.Util.Notations. Import ListNotations. Local Open Scope Z_scope. Import - Crypto.Experiments.NewPipeline.LanguageWf - Crypto.Experiments.NewPipeline.UnderLetsProofs - Crypto.Experiments.NewPipeline.MiscCompilerPassesProofs - Crypto.Experiments.NewPipeline.RewriterProofs - Crypto.Experiments.NewPipeline.AbstractInterpretationWf - Crypto.Experiments.NewPipeline.AbstractInterpretationProofs - Crypto.Experiments.NewPipeline.Language - Crypto.Experiments.NewPipeline.UnderLets - Crypto.Experiments.NewPipeline.AbstractInterpretation - Crypto.Experiments.NewPipeline.Rewriter - Crypto.Experiments.NewPipeline.MiscCompilerPasses - Crypto.Experiments.NewPipeline.CStringification. + Crypto.LanguageWf + Crypto.UnderLetsProofs + Crypto.MiscCompilerPassesProofs + Crypto.RewriterProofs + Crypto.AbstractInterpretationWf + Crypto.AbstractInterpretationProofs + Crypto.Language + Crypto.UnderLets + Crypto.AbstractInterpretation + Crypto.Rewriter + Crypto.MiscCompilerPasses + Crypto.CStringification. Import LanguageWf.Compilers diff --git a/src/Experiments/NewPipeline/CLI.v b/src/CLI.v index ecce16e9d..329937fc4 100644 --- a/src/Experiments/NewPipeline/CLI.v +++ b/src/CLI.v @@ -8,9 +8,9 @@ Require Import Crypto.Util.Strings.Decimal. Require Import Crypto.Util.Strings.HexString. Require Import Crypto.Util.Option. Require Import Crypto.Util.Strings.Show. -Require Import Crypto.Experiments.NewPipeline.PushButtonSynthesis. -Require Import Crypto.Experiments.NewPipeline.CStringification. -Require Import Crypto.Experiments.NewPipeline.BoundsPipeline. +Require Import Crypto.PushButtonSynthesis. +Require Import Crypto.CStringification. +Require Import Crypto.BoundsPipeline. Import ListNotations. Local Open Scope Z_scope. Local Open Scope string_scope. Import CStringification.Compilers. diff --git a/src/Experiments/NewPipeline/COperationSpecifications.v b/src/COperationSpecifications.v index 55c0dfb03..e8ae7d11e 100644 --- a/src/Experiments/NewPipeline/COperationSpecifications.v +++ b/src/COperationSpecifications.v @@ -11,7 +11,7 @@ Require Import Crypto.Util.ListUtil.FoldBool. Require Import Crypto.Util.Tactics.SpecializeBy. Require Import Crypto.Util.Tactics.SplitInContext. Require Import Crypto.Util.Tactics.UniquePose. -Require Import Crypto.Experiments.NewPipeline.Arithmetic. +Require Import Crypto.Arithmetic. Local Open Scope Z_scope. Local Open Scope bool_scope. (** These Imports are only needed for the ring proof *) diff --git a/src/Experiments/NewPipeline/CStringification.v b/src/CStringification.v index 3aebb2ec3..45e0c2eb0 100644 --- a/src/Experiments/NewPipeline/CStringification.v +++ b/src/CStringification.v @@ -14,8 +14,8 @@ Require Import Crypto.Util.ZRange.Operations. Require Import Crypto.Util.ZRange.Show. Require Import Crypto.Util.Option. Require Import Crypto.Util.OptionList. -Require Import Crypto.Experiments.NewPipeline.Language. -Require Import Crypto.Experiments.NewPipeline.AbstractInterpretation. +Require Import Crypto.Language. +Require Import Crypto.AbstractInterpretation. Require Import Crypto.Util.Bool.Equality. Require Import Crypto.Util.Notations. Import ListNotations. Local Open Scope zrange_scope. Local Open Scope Z_scope. diff --git a/src/Experiments/NewPipeline/CompilersTestCases.v b/src/CompilersTestCases.v index e48efa72e..c02b4e2fc 100644 --- a/src/Experiments/NewPipeline/CompilersTestCases.v +++ b/src/CompilersTestCases.v @@ -2,12 +2,12 @@ Require Import Coq.ZArith.ZArith. Require Import Coq.Lists.List. Require Import Crypto.Util.ZRange. Require Import Crypto.Util.LetIn. -Require Import Crypto.Experiments.NewPipeline.Language. -Require Import Crypto.Experiments.NewPipeline.UnderLets. -Require Import Crypto.Experiments.NewPipeline.AbstractInterpretation. -Require Import Crypto.Experiments.NewPipeline.Rewriter. -Require Import Crypto.Experiments.NewPipeline.MiscCompilerPasses. -Require Import Crypto.Experiments.NewPipeline.CStringification. +Require Import Crypto.Language. +Require Import Crypto.UnderLets. +Require Import Crypto.AbstractInterpretation. +Require Import Crypto.Rewriter. +Require Import Crypto.MiscCompilerPasses. +Require Import Crypto.CStringification. Import ListNotations. Local Open Scope Z_scope. Import Language.Compilers. diff --git a/src/Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.v b/src/ExtractionHaskell/saturated_solinas.v index fe323d3b7..18d1b9074 100644 --- a/src/Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.v +++ b/src/ExtractionHaskell/saturated_solinas.v @@ -1,4 +1,4 @@ -Require Import Crypto.Experiments.NewPipeline.StandaloneHaskellMain. +Require Import Crypto.StandaloneHaskellMain. (*Redirect "/tmp/saturated_solinas.hs"*) Recursive Extraction SaturatedSolinas.main. (* cat /tmp/solinas.hs.out | sed -f haskell.sed > ../../solinas.hs *) diff --git a/src/Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.v b/src/ExtractionHaskell/unsaturated_solinas.v index 225649b99..d4caf6ec5 100644 --- a/src/Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.v +++ b/src/ExtractionHaskell/unsaturated_solinas.v @@ -1,4 +1,4 @@ -Require Import Crypto.Experiments.NewPipeline.StandaloneHaskellMain. +Require Import Crypto.StandaloneHaskellMain. (*Redirect "/tmp/unsaturated_solinas.hs" *)Recursive Extraction UnsaturatedSolinas.main. (* cat /tmp/solinas.hs.out | sed -f haskell.sed > ../../solinas.hs *) diff --git a/src/Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.v b/src/ExtractionHaskell/word_by_word_montgomery.v index 5ac65a524..366b6d82e 100644 --- a/src/Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.v +++ b/src/ExtractionHaskell/word_by_word_montgomery.v @@ -1,4 +1,4 @@ -Require Import Crypto.Experiments.NewPipeline.StandaloneHaskellMain. +Require Import Crypto.StandaloneHaskellMain. (*Redirect "/tmp/word_by_word_montgomery.hs" *)Recursive Extraction WordByWordMontgomery.main. (* cat /tmp/solinas.hs.out | sed -f haskell.sed > ../../solinas.hs *) diff --git a/src/Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.v b/src/ExtractionOCaml/saturated_solinas.v index ffca16caf..3664b34e3 100644 --- a/src/Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.v +++ b/src/ExtractionOCaml/saturated_solinas.v @@ -1,3 +1,3 @@ -Require Import Crypto.Experiments.NewPipeline.StandaloneOCamlMain. +Require Import Crypto.StandaloneOCamlMain. (*Redirect "/tmp/saturated_solinas.ml"*) Recursive Extraction SaturatedSolinas.main. diff --git a/src/Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.v b/src/ExtractionOCaml/unsaturated_solinas.v index bd37edfe2..50de2615b 100644 --- a/src/Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.v +++ b/src/ExtractionOCaml/unsaturated_solinas.v @@ -1,3 +1,3 @@ -Require Import Crypto.Experiments.NewPipeline.StandaloneOCamlMain. +Require Import Crypto.StandaloneOCamlMain. (*Redirect "/tmp/unsaturated_solinas.ml"*) Recursive Extraction UnsaturatedSolinas.main. diff --git a/src/Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.v b/src/ExtractionOCaml/word_by_word_montgomery.v index 083e53a30..01f8bdcfd 100644 --- a/src/Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.v +++ b/src/ExtractionOCaml/word_by_word_montgomery.v @@ -1,3 +1,3 @@ -Require Import Crypto.Experiments.NewPipeline.StandaloneOCamlMain. +Require Import Crypto.StandaloneOCamlMain. (*Redirect "/tmp/word_by_word_montgomery.ml"*) Recursive Extraction WordByWordMontgomery.main. diff --git a/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v b/src/GENERATEDIdentifiersWithoutTypes.v index 43c8eb813..a682df8a2 100644 --- a/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v +++ b/src/GENERATEDIdentifiersWithoutTypes.v @@ -7,7 +7,7 @@ Require Import Crypto.Util.Option. Require Import Crypto.Util.ZRange. Require Import Crypto.Util.PrimitiveSigma. Require Import Crypto.Util.Notations. -Require Import Crypto.Experiments.NewPipeline.Language. +Require Import Crypto.Language. Import ListNotations. Local Open Scope list_scope. Import PrimitiveSigma.Primitive. @@ -838,7 +838,7 @@ Require Import Crypto.Util.Option. Require Import Crypto.Util.ZRange. Require Import Crypto.Util.PrimitiveSigma. Require Import Crypto.Util.Notations. -Require Import Crypto.Experiments.NewPipeline.Language. +Require Import Crypto.Language. Import ListNotations. Local Open Scope list_scope. Import PrimitiveSigma.Primitive. diff --git a/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.v b/src/GENERATEDIdentifiersWithoutTypesProofs.v index 48ac11ce6..c1b4232d8 100644 --- a/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.v +++ b/src/GENERATEDIdentifiersWithoutTypesProofs.v @@ -9,9 +9,9 @@ Require Import Crypto.Util.Tactics.DestructHead. Require Import Crypto.Util.Option. Require Import Crypto.Util.Decidable. Require Import Crypto.Util.HProp. -Require Import Crypto.Experiments.NewPipeline.Language. -Require Import Crypto.Experiments.NewPipeline.LanguageInversion. -Require Import Crypto.Experiments.NewPipeline.GENERATEDIdentifiersWithoutTypes. +Require Import Crypto.Language. +Require Import Crypto.LanguageInversion. +Require Import Crypto.GENERATEDIdentifiersWithoutTypes. Require Import Crypto.Util.FixCoqMistakes. Import EqNotations. diff --git a/src/Experiments/NewPipeline/Language.v b/src/Language.v index eba5cf85a..eba5cf85a 100644 --- a/src/Experiments/NewPipeline/Language.v +++ b/src/Language.v diff --git a/src/Experiments/NewPipeline/LanguageInversion.v b/src/LanguageInversion.v index bc9ad60be..7bc86d396 100644 --- a/src/Experiments/NewPipeline/LanguageInversion.v +++ b/src/LanguageInversion.v @@ -1,4 +1,4 @@ -Require Import Crypto.Experiments.NewPipeline.Language. +Require Import Crypto.Language. Require Import Crypto.Util.Sigma. Require Import Crypto.Util.Option. Require Import Crypto.Util.Prod. diff --git a/src/Experiments/NewPipeline/LanguageWf.v b/src/LanguageWf.v index d245e1e55..1aa0a775a 100644 --- a/src/Experiments/NewPipeline/LanguageWf.v +++ b/src/LanguageWf.v @@ -4,8 +4,8 @@ Require Import Coq.micromega.Lia. Require Import Coq.FSets.FMapPositive. Require Import Coq.Classes.Morphisms. Require Import Coq.Relations.Relations. -Require Import Crypto.Experiments.NewPipeline.Language. -Require Import Crypto.Experiments.NewPipeline.LanguageInversion. +Require Import Crypto.Language. +Require Import Crypto.LanguageInversion. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.DestructHead. Require Import Crypto.Util.Tactics.UniquePose. diff --git a/src/Experiments/NewPipeline/MiscCompilerPasses.v b/src/MiscCompilerPasses.v index d04d4c742..d810832f0 100644 --- a/src/Experiments/NewPipeline/MiscCompilerPasses.v +++ b/src/MiscCompilerPasses.v @@ -2,7 +2,7 @@ Require Import Coq.ZArith.ZArith. Require Import Coq.MSets.MSetPositive. Require Import Coq.FSets.FMapPositive. Require Import Crypto.Util.ListUtil Coq.Lists.List. -Require Import Crypto.Experiments.NewPipeline.Language. +Require Import Crypto.Language. Require Import Crypto.Util.Notations. Import ListNotations. Local Open Scope Z_scope. diff --git a/src/Experiments/NewPipeline/MiscCompilerPassesProofs.v b/src/MiscCompilerPassesProofs.v index 986bfaaa5..ac3e7babd 100644 --- a/src/Experiments/NewPipeline/MiscCompilerPassesProofs.v +++ b/src/MiscCompilerPassesProofs.v @@ -3,10 +3,10 @@ Require Import Coq.Lists.List. Require Import Coq.Classes.Morphisms. Require Import Coq.MSets.MSetPositive. Require Import Coq.FSets.FMapPositive. -Require Import Crypto.Experiments.NewPipeline.Language. -Require Import Crypto.Experiments.NewPipeline.LanguageInversion. -Require Import Crypto.Experiments.NewPipeline.LanguageWf. -Require Import Crypto.Experiments.NewPipeline.MiscCompilerPasses. +Require Import Crypto.Language. +Require Import Crypto.LanguageInversion. +Require Import Crypto.LanguageWf. +Require Import Crypto.MiscCompilerPasses. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.SplitInContext. Require Import Crypto.Util.Tactics.SpecializeAllWays. diff --git a/src/Experiments/NewPipeline/PushButtonSynthesis.v b/src/PushButtonSynthesis.v index d1b72ae0d..c8e1e97df 100644 --- a/src/Experiments/NewPipeline/PushButtonSynthesis.v +++ b/src/PushButtonSynthesis.v @@ -41,14 +41,14 @@ Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs. (* For MontgomeryRe Require Import Crypto.Util.Tactics.HasBody. Require Import Crypto.Util.Tactics.Head. Require Import Crypto.Util.Tactics.SpecializeBy. -Require Import Crypto.Experiments.NewPipeline.LanguageWf. -Require Import Crypto.Experiments.NewPipeline.Language. -Require Import Crypto.Experiments.NewPipeline.AbstractInterpretation. -Require Import Crypto.Experiments.NewPipeline.CStringification. -Require Import Crypto.Experiments.NewPipeline.Arithmetic. -Require Import Crypto.Experiments.NewPipeline.BoundsPipeline. -Require Import Crypto.Experiments.NewPipeline.COperationSpecifications. -Require Import Crypto.Experiments.NewPipeline.PushButtonSynthesis.ReificationCache. +Require Import Crypto.LanguageWf. +Require Import Crypto.Language. +Require Import Crypto.AbstractInterpretation. +Require Import Crypto.CStringification. +Require Import Crypto.Arithmetic. +Require Import Crypto.BoundsPipeline. +Require Import Crypto.COperationSpecifications. +Require Import Crypto.PushButtonSynthesis.ReificationCache. Import ListNotations. Local Open Scope Z_scope. Local Open Scope list_scope. Local Open Scope bool_scope. diff --git a/src/Experiments/NewPipeline/PushButtonSynthesis/ReificationCache.v b/src/PushButtonSynthesis/ReificationCache.v index 28202a6af..ba8488820 100644 --- a/src/Experiments/NewPipeline/PushButtonSynthesis/ReificationCache.v +++ b/src/PushButtonSynthesis/ReificationCache.v @@ -5,8 +5,8 @@ Require Import Coq.Relations.Relation_Definitions. Require Import Crypto.Util.Tactics.Head. Require Import Crypto.Util.Tactics.SubstEvars. -Require Import Crypto.Experiments.NewPipeline.Language. -Require Import Crypto.Experiments.NewPipeline.LanguageWf. +Require Import Crypto.Language. +Require Import Crypto.LanguageWf. Import Language.Compilers diff --git a/src/Experiments/NewPipeline/README.md b/src/README.md index 400a2e005..400a2e005 100644 --- a/src/Experiments/NewPipeline/README.md +++ b/src/README.md diff --git a/src/Experiments/NewPipeline/Rewriter.v b/src/Rewriter.v index 69349e19d..76071b866 100644 --- a/src/Experiments/NewPipeline/Rewriter.v +++ b/src/Rewriter.v @@ -10,9 +10,9 @@ Require Import Crypto.Util.ZRange.Operations. Require Import Crypto.Util.ZUtil.Definitions. Require Crypto.Util.PrimitiveProd. Require Crypto.Util.PrimitiveHList. -Require Import Crypto.Experiments.NewPipeline.Language. -Require Import Crypto.Experiments.NewPipeline.UnderLets. -Require Import Crypto.Experiments.NewPipeline.GENERATEDIdentifiersWithoutTypes. +Require Import Crypto.Language. +Require Import Crypto.UnderLets. +Require Import Crypto.GENERATEDIdentifiersWithoutTypes. Require Import Crypto.Util.LetIn. Require Import Crypto.Util.Notations. Import ListNotations. Local Open Scope bool_scope. Local Open Scope Z_scope. diff --git a/src/Experiments/NewPipeline/RewriterInterpProofs1.v b/src/RewriterInterpProofs1.v index 450c9ba09..e59591f0c 100644 --- a/src/Experiments/NewPipeline/RewriterInterpProofs1.v +++ b/src/RewriterInterpProofs1.v @@ -6,13 +6,13 @@ Require Import Coq.Classes.Morphisms. Require Import Coq.MSets.MSetPositive. Require Import Coq.FSets.FMapPositive. Require Import Coq.Logic.FunctionalExtensionality. -Require Import Crypto.Experiments.NewPipeline.Language. -Require Import Crypto.Experiments.NewPipeline.LanguageInversion. -Require Import Crypto.Experiments.NewPipeline.LanguageWf. -Require Import Crypto.Experiments.NewPipeline.UnderLetsProofs. -Require Import Crypto.Experiments.NewPipeline.GENERATEDIdentifiersWithoutTypesProofs. -Require Import Crypto.Experiments.NewPipeline.Rewriter. -Require Import Crypto.Experiments.NewPipeline.RewriterWf1. +Require Import Crypto.Language. +Require Import Crypto.LanguageInversion. +Require Import Crypto.LanguageWf. +Require Import Crypto.UnderLetsProofs. +Require Import Crypto.GENERATEDIdentifiersWithoutTypesProofs. +Require Import Crypto.Rewriter. +Require Import Crypto.RewriterWf1. Require Import Crypto.Util.MSetPositive.Facts. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.SplitInContext. diff --git a/src/Experiments/NewPipeline/RewriterProofs.v b/src/RewriterProofs.v index 888e8f8fb..c18527305 100644 --- a/src/Experiments/NewPipeline/RewriterProofs.v +++ b/src/RewriterProofs.v @@ -4,17 +4,17 @@ Require Import Coq.Lists.List. Require Import Coq.Classes.Morphisms. Require Import Coq.MSets.MSetPositive. Require Import Coq.FSets.FMapPositive. -Require Import Crypto.Experiments.NewPipeline.Language. -Require Import Crypto.Experiments.NewPipeline.LanguageInversion. -Require Import Crypto.Experiments.NewPipeline.LanguageWf. -Require Import Crypto.Experiments.NewPipeline.UnderLetsProofs. -Require Import Crypto.Experiments.NewPipeline.GENERATEDIdentifiersWithoutTypesProofs. -Require Import Crypto.Experiments.NewPipeline.Rewriter. -Require Import Crypto.Experiments.NewPipeline.RewriterWf1. -Require Import Crypto.Experiments.NewPipeline.RewriterWf2. -Require Import Crypto.Experiments.NewPipeline.RewriterInterpProofs1. -Require Import Crypto.Experiments.NewPipeline.RewriterRulesGood. -Require Import Crypto.Experiments.NewPipeline.RewriterRulesInterpGood. +Require Import Crypto.Language. +Require Import Crypto.LanguageInversion. +Require Import Crypto.LanguageWf. +Require Import Crypto.UnderLetsProofs. +Require Import Crypto.GENERATEDIdentifiersWithoutTypesProofs. +Require Import Crypto.Rewriter. +Require Import Crypto.RewriterWf1. +Require Import Crypto.RewriterWf2. +Require Import Crypto.RewriterInterpProofs1. +Require Import Crypto.RewriterRulesGood. +Require Import Crypto.RewriterRulesInterpGood. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.SplitInContext. Require Import Crypto.Util.Tactics.SpecializeAllWays. diff --git a/src/Experiments/NewPipeline/RewriterRulesGood.v b/src/RewriterRulesGood.v index f9e20ebb0..3718f04e5 100644 --- a/src/Experiments/NewPipeline/RewriterRulesGood.v +++ b/src/RewriterRulesGood.v @@ -4,13 +4,13 @@ Require Import Coq.Lists.List. Require Import Coq.Classes.Morphisms. Require Import Coq.MSets.MSetPositive. Require Import Coq.FSets.FMapPositive. -Require Import Crypto.Experiments.NewPipeline.Language. -Require Import Crypto.Experiments.NewPipeline.LanguageInversion. -Require Import Crypto.Experiments.NewPipeline.LanguageWf. -Require Import Crypto.Experiments.NewPipeline.UnderLetsProofs. -Require Import Crypto.Experiments.NewPipeline.GENERATEDIdentifiersWithoutTypesProofs. -Require Import Crypto.Experiments.NewPipeline.Rewriter. -Require Import Crypto.Experiments.NewPipeline.RewriterWf1. +Require Import Crypto.Language. +Require Import Crypto.LanguageInversion. +Require Import Crypto.LanguageWf. +Require Import Crypto.UnderLetsProofs. +Require Import Crypto.GENERATEDIdentifiersWithoutTypesProofs. +Require Import Crypto.Rewriter. +Require Import Crypto.RewriterWf1. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.SplitInContext. Require Import Crypto.Util.Tactics.SpecializeAllWays. diff --git a/src/Experiments/NewPipeline/RewriterRulesInterpGood.v b/src/RewriterRulesInterpGood.v index c80e35014..40177e3a0 100644 --- a/src/Experiments/NewPipeline/RewriterRulesInterpGood.v +++ b/src/RewriterRulesInterpGood.v @@ -4,13 +4,13 @@ Require Import Coq.Lists.List. Require Import Coq.Classes.Morphisms. Require Import Coq.MSets.MSetPositive. Require Import Coq.FSets.FMapPositive. -Require Import Crypto.Experiments.NewPipeline.Language. -Require Import Crypto.Experiments.NewPipeline.LanguageInversion. -Require Import Crypto.Experiments.NewPipeline.LanguageWf. -Require Import Crypto.Experiments.NewPipeline.UnderLetsProofs. -Require Import Crypto.Experiments.NewPipeline.GENERATEDIdentifiersWithoutTypesProofs. -Require Import Crypto.Experiments.NewPipeline.Rewriter. -Require Import Crypto.Experiments.NewPipeline.RewriterWf1. +Require Import Crypto.Language. +Require Import Crypto.LanguageInversion. +Require Import Crypto.LanguageWf. +Require Import Crypto.UnderLetsProofs. +Require Import Crypto.GENERATEDIdentifiersWithoutTypesProofs. +Require Import Crypto.Rewriter. +Require Import Crypto.RewriterWf1. Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. diff --git a/src/Experiments/NewPipeline/RewriterWf1.v b/src/RewriterWf1.v index 0536757e8..19ea1e9e7 100644 --- a/src/Experiments/NewPipeline/RewriterWf1.v +++ b/src/RewriterWf1.v @@ -5,12 +5,12 @@ Require Import Coq.Lists.List. Require Import Coq.Classes.Morphisms. Require Import Coq.MSets.MSetPositive. Require Import Coq.FSets.FMapPositive. -Require Import Crypto.Experiments.NewPipeline.Language. -Require Import Crypto.Experiments.NewPipeline.LanguageInversion. -Require Import Crypto.Experiments.NewPipeline.LanguageWf. -Require Import Crypto.Experiments.NewPipeline.UnderLetsProofs. -Require Import Crypto.Experiments.NewPipeline.GENERATEDIdentifiersWithoutTypesProofs. -Require Import Crypto.Experiments.NewPipeline.Rewriter. +Require Import Crypto.Language. +Require Import Crypto.LanguageInversion. +Require Import Crypto.LanguageWf. +Require Import Crypto.UnderLetsProofs. +Require Import Crypto.GENERATEDIdentifiersWithoutTypesProofs. +Require Import Crypto.Rewriter. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.SplitInContext. Require Import Crypto.Util.Tactics.SpecializeAllWays. diff --git a/src/Experiments/NewPipeline/RewriterWf2.v b/src/RewriterWf2.v index 142f953fa..13238361b 100644 --- a/src/Experiments/NewPipeline/RewriterWf2.v +++ b/src/RewriterWf2.v @@ -4,13 +4,13 @@ Require Import Coq.Lists.List. Require Import Coq.Classes.Morphisms. Require Import Coq.MSets.MSetPositive. Require Import Coq.FSets.FMapPositive. -Require Import Crypto.Experiments.NewPipeline.Language. -Require Import Crypto.Experiments.NewPipeline.LanguageInversion. -Require Import Crypto.Experiments.NewPipeline.LanguageWf. -Require Import Crypto.Experiments.NewPipeline.UnderLetsProofs. -Require Import Crypto.Experiments.NewPipeline.GENERATEDIdentifiersWithoutTypesProofs. -Require Import Crypto.Experiments.NewPipeline.Rewriter. -Require Import Crypto.Experiments.NewPipeline.RewriterWf1. +Require Import Crypto.Language. +Require Import Crypto.LanguageInversion. +Require Import Crypto.LanguageWf. +Require Import Crypto.UnderLetsProofs. +Require Import Crypto.GENERATEDIdentifiersWithoutTypesProofs. +Require Import Crypto.Rewriter. +Require Import Crypto.RewriterWf1. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.SplitInContext. Require Import Crypto.Util.Tactics.SpecializeAllWays. diff --git a/src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v b/src/SlowPrimeSynthesisExamples.v index 7d4c82f6b..8da9e8776 100644 --- a/src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v +++ b/src/SlowPrimeSynthesisExamples.v @@ -2,9 +2,9 @@ Require Import Coq.ZArith.ZArith. Require Import Coq.Strings.String. Require Import Coq.derive.Derive. Require Import Coq.Lists.List. -Require Import Crypto.Experiments.NewPipeline.Arithmetic. -Require Import Crypto.Experiments.NewPipeline.PushButtonSynthesis. -Require Import Crypto.Experiments.NewPipeline.CStringification. +Require Import Crypto.Arithmetic. +Require Import Crypto.PushButtonSynthesis. +Require Import Crypto.CStringification. Require Import Crypto.Util.Notations. Import ListNotations. Local Open Scope Z_scope. diff --git a/src/Experiments/NewPipeline/StandaloneHaskellMain.v b/src/StandaloneHaskellMain.v index b7d7fa869..1a07b827f 100644 --- a/src/Experiments/NewPipeline/StandaloneHaskellMain.v +++ b/src/StandaloneHaskellMain.v @@ -6,8 +6,8 @@ Require Import Coq.Strings.String. Require Crypto.Util.Strings.String. Require Import Crypto.Util.Strings.Decimal. Require Import Crypto.Util.Strings.HexString. -Require Import Crypto.Experiments.NewPipeline.PushButtonSynthesis. -Require Import Crypto.Experiments.NewPipeline.CLI. +Require Import Crypto.PushButtonSynthesis. +Require Import Crypto.CLI. Require Import Crypto.Util.Notations. Import ListNotations. Local Open Scope string_scope. diff --git a/src/Experiments/NewPipeline/StandaloneOCamlMain.v b/src/StandaloneOCamlMain.v index a642a1006..cb2a20904 100644 --- a/src/Experiments/NewPipeline/StandaloneOCamlMain.v +++ b/src/StandaloneOCamlMain.v @@ -7,8 +7,8 @@ Require Import Coq.Strings.String. Require Crypto.Util.Strings.String. Require Import Crypto.Util.Strings.Decimal. Require Import Crypto.Util.Strings.HexString. -Require Import Crypto.Experiments.NewPipeline.PushButtonSynthesis. -Require Import Crypto.Experiments.NewPipeline.CLI. +Require Import Crypto.PushButtonSynthesis. +Require Import Crypto.CLI. Require Import Crypto.Util.Notations. Import ListNotations. Local Open Scope string_scope. diff --git a/src/Experiments/NewPipeline/Toplevel2.v b/src/Toplevel2.v index 81c94b1bc..01381380a 100644 --- a/src/Experiments/NewPipeline/Toplevel2.v +++ b/src/Toplevel2.v @@ -47,28 +47,28 @@ Require Import Crypto.Util.Strings.Show. Require Import Crypto.Util.ZRange.Operations. Require Import Crypto.Util.ZRange.BasicLemmas. Require Import Crypto.Util.ZRange.Show. -Require Import Crypto.Experiments.NewPipeline.Arithmetic. -Require Crypto.Experiments.NewPipeline.Language. -Require Crypto.Experiments.NewPipeline.UnderLets. -Require Crypto.Experiments.NewPipeline.AbstractInterpretation. -Require Crypto.Experiments.NewPipeline.AbstractInterpretationProofs. -Require Crypto.Experiments.NewPipeline.Rewriter. -Require Crypto.Experiments.NewPipeline.MiscCompilerPasses. -Require Crypto.Experiments.NewPipeline.CStringification. -Require Export Crypto.Experiments.NewPipeline.PushButtonSynthesis. +Require Import Crypto.Arithmetic. +Require Crypto.Language. +Require Crypto.UnderLets. +Require Crypto.AbstractInterpretation. +Require Crypto.AbstractInterpretationProofs. +Require Crypto.Rewriter. +Require Crypto.MiscCompilerPasses. +Require Crypto.CStringification. +Require Export Crypto.PushButtonSynthesis. Require Import Crypto.Util.Notations. Import ListNotations. Local Open Scope Z_scope. Import Associational Positional. Import - Crypto.Experiments.NewPipeline.Language - Crypto.Experiments.NewPipeline.UnderLets - Crypto.Experiments.NewPipeline.AbstractInterpretation - Crypto.Experiments.NewPipeline.AbstractInterpretationProofs - Crypto.Experiments.NewPipeline.Rewriter - Crypto.Experiments.NewPipeline.MiscCompilerPasses - Crypto.Experiments.NewPipeline.CStringification. + Crypto.Language + Crypto.UnderLets + Crypto.AbstractInterpretation + Crypto.AbstractInterpretationProofs + Crypto.Rewriter + Crypto.MiscCompilerPasses + Crypto.CStringification. Import Language.Compilers diff --git a/src/Experiments/NewPipeline/UnderLets.v b/src/UnderLets.v index dd6019570..522a8c4c7 100644 --- a/src/Experiments/NewPipeline/UnderLets.v +++ b/src/UnderLets.v @@ -1,4 +1,4 @@ -Require Import Crypto.Experiments.NewPipeline.Language. +Require Import Crypto.Language. Require Import Crypto.Util.Notations. Module Compilers. diff --git a/src/Experiments/NewPipeline/UnderLetsProofs.v b/src/UnderLetsProofs.v index 19e79e95b..787fdb7c4 100644 --- a/src/Experiments/NewPipeline/UnderLetsProofs.v +++ b/src/UnderLetsProofs.v @@ -1,10 +1,10 @@ Require Import Coq.Lists.List. Require Import Coq.Classes.Morphisms. Require Import Coq.Lists.SetoidList. -Require Import Crypto.Experiments.NewPipeline.Language. -Require Import Crypto.Experiments.NewPipeline.LanguageInversion. -Require Import Crypto.Experiments.NewPipeline.LanguageWf. -Require Import Crypto.Experiments.NewPipeline.UnderLets. +Require Import Crypto.Language. +Require Import Crypto.LanguageInversion. +Require Import Crypto.LanguageWf. +Require Import Crypto.UnderLets. Require Import Crypto.Util.Prod. Require Import Crypto.Util.Sigma. Require Import Crypto.Util.Option. diff --git a/src/Experiments/NewPipeline/arith_rewrite_head.out b/src/arith_rewrite_head.out index 4a3eb8e80..4a3eb8e80 100644 --- a/src/Experiments/NewPipeline/arith_rewrite_head.out +++ b/src/arith_rewrite_head.out diff --git a/src/Experiments/NewPipeline/arith_with_casts_rewrite_head.out b/src/arith_with_casts_rewrite_head.out index 2baf1c5d2..2baf1c5d2 100644 --- a/src/Experiments/NewPipeline/arith_with_casts_rewrite_head.out +++ b/src/arith_with_casts_rewrite_head.out diff --git a/src/Experiments/NewPipeline/fancy_rewrite_head.out b/src/fancy_rewrite_head.out index 414237570..414237570 100644 --- a/src/Experiments/NewPipeline/fancy_rewrite_head.out +++ b/src/fancy_rewrite_head.out diff --git a/src/Experiments/NewPipeline/fancy_with_casts_rewrite_head.out b/src/fancy_with_casts_rewrite_head.out index c35ff8a01..c35ff8a01 100644 --- a/src/Experiments/NewPipeline/fancy_with_casts_rewrite_head.out +++ b/src/fancy_with_casts_rewrite_head.out diff --git a/src/Experiments/NewPipeline/haskell.sed b/src/haskell.sed index 2ef5dd06d..2ef5dd06d 100644 --- a/src/Experiments/NewPipeline/haskell.sed +++ b/src/haskell.sed diff --git a/src/Experiments/NewPipeline/nbe_rewrite_head.out b/src/nbe_rewrite_head.out index cbd282f50..cbd282f50 100644 --- a/src/Experiments/NewPipeline/nbe_rewrite_head.out +++ b/src/nbe_rewrite_head.out |