move src/Experiments/NewPipeline/ to src/

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
diff --git a/Makefile b/Makefile
index 6e9ccbb4d..56cbed38a 100644
--- a/Makefile
+++ b/Makefile
@@ -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)
diff --git a/README.md b/README.md
index 3411f047d..0215e2e2c 100644
--- a/README.md
+++ b/README.md
@@ -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