From 07ad3e7b8d3a69ab72341896c5854c9d4393dede Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sat, 27 Jul 2024 20:09:05 +0200 Subject: [PATCH] Adapt to https://github.com/coq/coq/pull/19530 --- LiveVerif/src/LiveVerif/LiveFwd.v | 2 +- LiveVerif/src/LiveVerif/LiveParsing.v | 6 +- LiveVerif/src/LiveVerif/LiveProgramLogic.v | 6 +- LiveVerif/src/LiveVerif/LiveRules.v | 8 +- LiveVerif/src/LiveVerif/LiveSnippet.v | 2 +- LiveVerif/src/LiveVerif/LiveVerifLib.v | 4 +- LiveVerif/src/LiveVerif/PackageContext.v | 2 +- LiveVerif/src/LiveVerif/string_to_ident.v | 4 +- .../src/LiveVerifExamples/Tests/PrintSmt.v | 4 +- .../LiveVerifExamples/Tests/SampleSideconds.v | 2 +- .../LiveVerifExamples/Tests/SampleSimpls.v | 2 +- LiveVerif/src/LiveVerifExamples/interleave.v | 2 +- LiveVerifEx64/src/LiveVerifExamples/fmalloc.v | 348 +++++++++++++- .../src/LiveVerifExamples/onesize_malloc.v | 346 +++++++++++++- .../src/LiveVerifExamples/tree_set.v | 436 +++++++++++++++++- bedrock2/src/bedrock2/AbsintWordToZ.v | 4 +- bedrock2/src/bedrock2/Array.v | 2 +- bedrock2/src/bedrock2/ArrayCasts.v | 6 +- bedrock2/src/bedrock2/BasicC32Semantics.v | 2 +- bedrock2/src/bedrock2/BasicC64Semantics.v | 2 +- bedrock2/src/bedrock2/ByteListPredicates.v | 8 +- bedrock2/src/bedrock2/FE310CSemantics.v | 2 +- bedrock2/src/bedrock2/FrameRule.v | 4 +- .../src/bedrock2/HeapletwiseAutoSplitMerge.v | 6 +- bedrock2/src/bedrock2/HeapletwiseHyps.v | 4 +- bedrock2/src/bedrock2/Lift1Prop.v | 2 +- bedrock2/src/bedrock2/ListIndexNotations.v | 4 +- bedrock2/src/bedrock2/Loops.v | 2 +- bedrock2/src/bedrock2/Map/DisjointUnion.v | 4 +- bedrock2/src/bedrock2/Map/SeparationLogic.v | 6 +- bedrock2/src/bedrock2/Memory.v | 4 +- bedrock2/src/bedrock2/MetricLogging.v | 2 +- bedrock2/src/bedrock2/MetricSemantics.v | 4 +- bedrock2/src/bedrock2/NetworkPackets.v | 4 +- bedrock2/src/bedrock2/NotationsCustomEntry.v | 4 +- bedrock2/src/bedrock2/OperatorOverloading.v | 2 +- bedrock2/src/bedrock2/PrintListByte.v | 2 +- bedrock2/src/bedrock2/ProgramLogic.v | 4 +- bedrock2/src/bedrock2/PurifyHeapletwise.v | 2 +- bedrock2/src/bedrock2/PurifySep.v | 2 +- bedrock2/src/bedrock2/RecordPredicates.v | 2 +- bedrock2/src/bedrock2/Refinement.v | 2 +- bedrock2/src/bedrock2/Scalars.v | 4 +- bedrock2/src/bedrock2/Semantics.v | 2 +- bedrock2/src/bedrock2/SepAuto.v | 2 +- bedrock2/src/bedrock2/SepAutoArray.v | 4 +- bedrock2/src/bedrock2/SepAutoExports.v | 2 +- bedrock2/src/bedrock2/SepCalls.v | 8 +- bedrock2/src/bedrock2/SepCallsExports.v | 6 +- bedrock2/src/bedrock2/SepClause.v | 2 +- bedrock2/src/bedrock2/SepLib.v | 4 +- bedrock2/src/bedrock2/SepLogAddrArith.v | 4 +- bedrock2/src/bedrock2/SepappBulletPoints.v | 2 +- bedrock2/src/bedrock2/Syntax.v | 4 +- bedrock2/src/bedrock2/TacticError.v | 2 +- bedrock2/src/bedrock2/ToCString.v | 4 +- .../bedrock2/ToCStringExprTypecheckingTest.v | 2 +- bedrock2/src/bedrock2/TraceInspection.v | 4 +- bedrock2/src/bedrock2/TracePredicate.v | 2 +- bedrock2/src/bedrock2/TransferSepsOrder.v | 4 +- bedrock2/src/bedrock2/Variables.v | 2 +- bedrock2/src/bedrock2/WeakestPrecondition.v | 5 +- .../bedrock2/WeakestPreconditionProperties.v | 2 +- bedrock2/src/bedrock2/WordPushDownLemmas.v | 4 +- bedrock2/src/bedrock2/ZListEqProver.v | 7 +- bedrock2/src/bedrock2/ZWordMem.v | 6 +- bedrock2/src/bedrock2/ZnWords.v | 6 +- bedrock2/src/bedrock2/ZnWordsTests.v | 4 +- bedrock2/src/bedrock2/bottom_up_simpl.v | 4 +- bedrock2/src/bedrock2/bottom_up_simpl_ltac1.v | 4 +- bedrock2/src/bedrock2/bottom_up_simpl_perf.v | 2 +- bedrock2/src/bedrock2/cancel_div.v | 2 +- bedrock2/src/bedrock2/cancel_div_ltac1.v | 2 +- bedrock2/src/bedrock2/e1000_packet_trace.v | 4 +- bedrock2/src/bedrock2/e1000_read_write_step.v | 6 +- bedrock2/src/bedrock2/e1000_state.v | 4 +- bedrock2/src/bedrock2/ident_to_string.v | 2 +- .../src/bedrock2/memory_mapped_ext_spec.v | 8 +- .../old_dma/StateMachineBasedExtSpec.v | 4 +- .../old_dma/StateMachineBasedExtSpec_wp.v | 4 +- ...ular_buffer_slice_based_on_list_of_addrs.v | 4 +- bedrock2/src/bedrock2/old_dma/e1000.v | 6 +- .../src/bedrock2/old_dma/e1000_stateless.v | 4 +- bedrock2/src/bedrock2/old_dma/e1000_wp.v | 4 +- .../mmio_read_write_step_based_ext_spec.v | 6 +- bedrock2/src/bedrock2/ptsto_bytes.v | 4 +- bedrock2/src/bedrock2/safe_implication.v | 4 +- bedrock2/src/bedrock2/sepapp.v | 4 +- .../bedrock2/syntactic_f_equal_with_ZnWords.v | 2 +- bedrock2/src/bedrock2/to_from_anybytes.v | 4 +- bedrock2/src/bedrock2/unzify.v | 2 +- .../src/bedrock2Examples/ARPResponderProofs.v | 2 +- bedrock2/src/bedrock2Examples/Demos.v | 2 +- .../src/bedrock2Examples/FE310CompilerDemo.v | 4 +- bedrock2/src/bedrock2Examples/FlatConstMem.v | 3 +- bedrock2/src/bedrock2Examples/LAN9250.v | 2 +- bedrock2/src/bedrock2Examples/SPI.v | 2 +- bedrock2/src/bedrock2Examples/Trace.v | 6 +- bedrock2/src/bedrock2Examples/bsearch.v | 2 +- bedrock2/src/bedrock2Examples/chacha20.v | 2 +- bedrock2/src/bedrock2Examples/ipow.v | 3 +- .../src/bedrock2Examples/lightbulb_spec.v | 2 +- bedrock2/src/bedrock2Examples/swap_by_add.v | 2 +- compiler/src/compiler/DeadCodeElim.v | 2 +- compiler/src/compiler/DeadCodeElimDef.v | 6 +- compiler/src/compiler/DivisibleBy4.v | 2 +- compiler/src/compiler/ElfPrinter.v | 6 +- compiler/src/compiler/ExprImp.v | 6 +- compiler/src/compiler/ExprImpEventLoopSpec.v | 2 +- compiler/src/compiler/FlatImp.v | 6 +- compiler/src/compiler/FlatImpConstraints.v | 2 +- compiler/src/compiler/FlatImpUniqueSepLog.v | 6 +- compiler/src/compiler/FlatToRiscvCommon.v | 8 +- compiler/src/compiler/FlatToRiscvDef.v | 4 +- compiler/src/compiler/FlatToRiscvFunctions.v | 4 +- compiler/src/compiler/FlattenExpr.v | 4 +- compiler/src/compiler/FlattenExprDef.v | 2 +- compiler/src/compiler/ForeverSafe.v | 2 +- compiler/src/compiler/GoFlatToRiscv.v | 2 +- compiler/src/compiler/LowerPipeline.v | 2 +- compiler/src/compiler/MMIO.v | 2 +- compiler/src/compiler/MemoryLayout.v | 2 +- .../src/compiler/NaiveRiscvWordProperties.v | 4 +- compiler/src/compiler/NameGen.v | 2 +- compiler/src/compiler/Pipeline.v | 2 +- compiler/src/compiler/RegAlloc.v | 2 +- compiler/src/compiler/Registers.v | 2 +- compiler/src/compiler/RiscvEventLoop.v | 2 +- compiler/src/compiler/RiscvWordProperties.v | 4 +- compiler/src/compiler/RunInstruction.v | 2 +- compiler/src/compiler/SeparationLogic.v | 8 +- compiler/src/compiler/Spilling.v | 6 +- compiler/src/compiler/StringNameGen.v | 12 +- compiler/src/compiler/Symbols.v | 7 +- compiler/src/compiler/ToplevelLoop.v | 6 +- compiler/src/compiler/UniqueSepLog.v | 6 +- compiler/src/compiler/UseImmediate.v | 2 +- compiler/src/compiler/UseImmediateDef.v | 2 +- compiler/src/compiler/ZLemmas.v | 2 +- compiler/src/compiler/ZNameGen.v | 2 +- .../memory_mapped_ext_calls_compiler.v | 4 +- .../compiler/memory_mapped_ext_calls_riscv.v | 10 +- compiler/src/compiler/mod4_0.v | 2 +- compiler/src/compiler/regs_initialized.v | 2 +- compiler/src/compiler/util/Common.v | 4 +- compiler/src/compilerExamples/AssemblyVerif.v | 4 +- .../src/compilerExamples/EditDistExample.v | 8 +- compiler/src/compilerExamples/FibCompiled.v | 2 +- compiler/src/compilerExamples/Fibonacci.v | 2 +- .../compilerExamples/InlineAssemblyMacro.v | 2 +- compiler/src/compilerExamples/swap.v | 2 +- .../src/end2end/Bedrock2SemanticsForKami.v | 2 +- end2end/src/end2end/End2EndLightbulb.v | 6 +- end2end/src/end2end/End2EndPipeline.v | 8 +- end2end/src/end2end/KamiRiscvWordProperties.v | 2 +- end2end/src/end2end/PrintAdmits.v | 4 +- end2end/src/end2end/RelyNotations.v | 4 +- processor/src/processor/Consistency.v | 4 +- processor/src/processor/KamiProc.v | 4 +- processor/src/processor/KamiRiscv.v | 4 +- processor/src/processor/KamiRiscvStep.v | 4 +- processor/src/processor/KamiWord.v | 3 +- 162 files changed, 1423 insertions(+), 293 deletions(-) mode change 120000 => 100644 LiveVerifEx64/src/LiveVerifExamples/fmalloc.v mode change 120000 => 100644 LiveVerifEx64/src/LiveVerifExamples/onesize_malloc.v mode change 120000 => 100644 LiveVerifEx64/src/LiveVerifExamples/tree_set.v diff --git a/LiveVerif/src/LiveVerif/LiveFwd.v b/LiveVerif/src/LiveVerif/LiveFwd.v index 7cd504f4..f3d27b30 100644 --- a/LiveVerif/src/LiveVerif/LiveFwd.v +++ b/LiveVerif/src/LiveVerif/LiveFwd.v @@ -1,4 +1,4 @@ -Require Import Coq.ZArith.ZArith. Local Open Scope Z_scope. +From Coq Require Import ZArith. Local Open Scope Z_scope. Require Import coqutil.Word.Bitwidth. Require Import coqutil.Tactics.autoforward. Require Import coqutil.Word.Interface coqutil.Word.Properties coqutil.Map.Interface. diff --git a/LiveVerif/src/LiveVerif/LiveParsing.v b/LiveVerif/src/LiveVerif/LiveParsing.v index 27900f50..a13702f6 100644 --- a/LiveVerif/src/LiveVerif/LiveParsing.v +++ b/LiveVerif/src/LiveVerif/LiveParsing.v @@ -1,6 +1,6 @@ -Require Import Coq.setoid_ring.InitialRing. (* for isZcst *) -Require Import Coq.Strings.String. -Require Import Coq.ZArith.ZArith. Local Open Scope Z_scope. +From Coq Require Import InitialRing. (* for isZcst *) +From Coq Require Import String. +From Coq Require Import ZArith. Local Open Scope Z_scope. Require Import bedrock2.Syntax. Require Import LiveVerif.LiveExpr. Require Import LiveVerif.LiveSnippet. diff --git a/LiveVerif/src/LiveVerif/LiveProgramLogic.v b/LiveVerif/src/LiveVerif/LiveProgramLogic.v index 9e16e651..e0c1782d 100644 --- a/LiveVerif/src/LiveVerif/LiveProgramLogic.v +++ b/LiveVerif/src/LiveVerif/LiveProgramLogic.v @@ -1,7 +1,7 @@ -Require Import Coq.ZArith.ZArith. Local Open Scope Z_scope. -Require Import Coq.micromega.Lia. +From Coq Require Import ZArith. Local Open Scope Z_scope. +From Coq Require Import Lia. Require Import coqutil.Z.Lia. -Require Import Coq.Strings.String. +From Coq Require Import String. Require Import coqutil.Tactics.rdelta. Require Import coqutil.Tactics.Tactics. Require Import coqutil.Map.Interface coqutil.Map.Properties. diff --git a/LiveVerif/src/LiveVerif/LiveRules.v b/LiveVerif/src/LiveVerif/LiveRules.v index 62fbb602..5b738829 100644 --- a/LiveVerif/src/LiveVerif/LiveRules.v +++ b/LiveVerif/src/LiveVerif/LiveRules.v @@ -1,7 +1,7 @@ -Require Import Coq.ZArith.ZArith. Local Open Scope Z_scope. -Require Import Coq.micromega.Lia. -Require Import Coq.Init.Byte. -Require Import Coq.Strings.String. +From Coq Require Import ZArith. Local Open Scope Z_scope. +From Coq Require Import Lia. +From Coq.Init Require Import Byte. +From Coq Require Import String. Require Import coqutil.Map.Interface coqutil.Map.Properties. Require coqutil.Map.SortedListString. (* for function env, other maps are kept abstract *) Require Import coqutil.Word.Interface coqutil.Word.Properties coqutil.Word.Bitwidth. diff --git a/LiveVerif/src/LiveVerif/LiveSnippet.v b/LiveVerif/src/LiveVerif/LiveSnippet.v index 270fa02f..f7b7ee8c 100644 --- a/LiveVerif/src/LiveVerif/LiveSnippet.v +++ b/LiveVerif/src/LiveVerif/LiveSnippet.v @@ -1,4 +1,4 @@ -Require Import Coq.Strings.String. +From Coq Require Import String. Require Import bedrock2.Syntax. Inductive assignment_rhs := diff --git a/LiveVerif/src/LiveVerif/LiveVerifLib.v b/LiveVerif/src/LiveVerif/LiveVerifLib.v index 3fd33c48..89f01424 100644 --- a/LiveVerif/src/LiveVerif/LiveVerifLib.v +++ b/LiveVerif/src/LiveVerif/LiveVerifLib.v @@ -1,5 +1,5 @@ -Require Export Coq.ZArith.ZArith. Local Open Scope Z_scope. -Require Export Coq.micromega.Lia. +Require Export ZArith. Local Open Scope Z_scope. +Require Export Lia. Require Export coqutil.Datatypes.Inhabited. Require Export coqutil.Tactics.Tactics. Require Export coqutil.Tactics.safe_auto. diff --git a/LiveVerif/src/LiveVerif/PackageContext.v b/LiveVerif/src/LiveVerif/PackageContext.v index 469e850b..7103faf2 100644 --- a/LiveVerif/src/LiveVerif/PackageContext.v +++ b/LiveVerif/src/LiveVerif/PackageContext.v @@ -1,4 +1,4 @@ -Require Import Coq.ZArith.ZArith. Local Open Scope Z_scope. +From Coq Require Import ZArith. Local Open Scope Z_scope. Require Import Ltac2.Ltac2. Set Default Proof Mode "Classic". Require Import coqutil.Tactics.rdelta. Require Import coqutil.Datatypes.Inhabited. diff --git a/LiveVerif/src/LiveVerif/string_to_ident.v b/LiveVerif/src/LiveVerif/string_to_ident.v index f21ef2c8..173d56db 100644 --- a/LiveVerif/src/LiveVerif/string_to_ident.v +++ b/LiveVerif/src/LiveVerif/string_to_ident.v @@ -1,5 +1,5 @@ -Require Import Coq.Strings.String. -Require Import Coq.Strings.Ascii. +From Coq Require Import String. +From Coq Require Import Ascii. Require Import Ltac2.Ltac2. Require Ltac2.Option. diff --git a/LiveVerif/src/LiveVerifExamples/Tests/PrintSmt.v b/LiveVerif/src/LiveVerifExamples/Tests/PrintSmt.v index 4baf305d..4aa89aee 100644 --- a/LiveVerif/src/LiveVerifExamples/Tests/PrintSmt.v +++ b/LiveVerif/src/LiveVerifExamples/Tests/PrintSmt.v @@ -1,6 +1,6 @@ -Require Import Coq.ZArith.ZArith. +From Coq Require Import ZArith. Require Import coqutil.Word.Interface. -Require Import Coq.Logic.Classical_Prop. +From Coq Require Import Classical_Prop. Require Import coqutil.Tactics.ident_ops. Ltac eval_constant_pows := diff --git a/LiveVerif/src/LiveVerifExamples/Tests/SampleSideconds.v b/LiveVerif/src/LiveVerifExamples/Tests/SampleSideconds.v index bcc9fcb7..fb04b46a 100644 --- a/LiveVerif/src/LiveVerifExamples/Tests/SampleSideconds.v +++ b/LiveVerif/src/LiveVerifExamples/Tests/SampleSideconds.v @@ -26,7 +26,7 @@ Ltac eval_constant_pows := end end. -Require Import Coq.Logic.Classical_Prop. +From Coq Require Import Classical_Prop. Lemma ExistsNot_NotForall: forall AA (P: AA -> Prop), (exists a: AA, ~ P a) <-> ~ forall (a: AA), P a. Proof. diff --git a/LiveVerif/src/LiveVerifExamples/Tests/SampleSimpls.v b/LiveVerif/src/LiveVerifExamples/Tests/SampleSimpls.v index 5c017d9c..fb332685 100644 --- a/LiveVerif/src/LiveVerifExamples/Tests/SampleSimpls.v +++ b/LiveVerif/src/LiveVerifExamples/Tests/SampleSimpls.v @@ -1,4 +1,4 @@ -Require Import Coq.ZArith.ZArith. Local Open Scope Z_scope. +From Coq Require Import ZArith. Local Open Scope Z_scope. Require Import coqutil.Word.Interface coqutil.Word.Properties. Require Import coqutil.Datatypes.ZList. Require bedrock2.WordNotations. diff --git a/LiveVerif/src/LiveVerifExamples/interleave.v b/LiveVerif/src/LiveVerifExamples/interleave.v index 0282c814..9dd00e66 100644 --- a/LiveVerif/src/LiveVerifExamples/interleave.v +++ b/LiveVerif/src/LiveVerifExamples/interleave.v @@ -1,4 +1,4 @@ -Require Import Coq.Lists.List. +From Coq Require Import List. Require Import bedrock2.ReversedListNotations. Local Open Scope list_scope. Section Interleave. diff --git a/LiveVerifEx64/src/LiveVerifExamples/fmalloc.v b/LiveVerifEx64/src/LiveVerifExamples/fmalloc.v deleted file mode 120000 index b74df650..00000000 --- a/LiveVerifEx64/src/LiveVerifExamples/fmalloc.v +++ /dev/null @@ -1 +0,0 @@ -../../../LiveVerif/src/LiveVerifExamples/fmalloc.v \ No newline at end of file diff --git a/LiveVerifEx64/src/LiveVerifExamples/fmalloc.v b/LiveVerifEx64/src/LiveVerifExamples/fmalloc.v new file mode 100644 index 00000000..517476eb --- /dev/null +++ b/LiveVerifEx64/src/LiveVerifExamples/fmalloc.v @@ -0,0 +1,347 @@ +(* -*- eval: (load-file "../LiveVerif/live_verif_setup.el"); -*- *) +(* fmalloc: fixed-size malloc *) +Require Import LiveVerif.LiveVerifLib. + +Load LiveVerif. + +Record fmalloc_state_t := { + block_size: Z; + free_list: word; +}. + +Definition fmalloc_state(s: fmalloc_state_t): word -> mem -> Prop := .**/ + +typedef struct __attribute__ ((__packed__)) { + size_t block_size; + uintptr_t free_list; +} fmalloc_state; + +/**. + +Section WithBlockSize. + Context (block_size: Z). + Fixpoint fixed_size_free_list(n: nat)(p: word): mem -> Prop := + match n with + | O => emp (p = /[0]) + | S n' => EX q, + <{ * emp (p <> /[0]) + * <{ + uintptr q + + anyval (array (uint 8) (block_size - sizeof uintptr)) }> p + * fixed_size_free_list n' q }> + end. +End WithBlockSize. + +Lemma fixed_size_free_list_nil: forall blk_size, + fixed_size_free_list blk_size O /[0] map.empty. +Proof. intros. simpl. split; reflexivity. Qed. + +Lemma fixed_size_free_list_null: forall blk_size n m, + fixed_size_free_list blk_size n /[0] m -> + emp (n = O) m. +Proof. + intros. destruct n; simpl in *. + - unfold emp in *. intuition congruence. + - exfalso. steps. congruence. +Qed. + +Lemma fixed_size_free_list_nonnull: forall blk_size n a m, + a <> /[0] -> + fixed_size_free_list blk_size n a m -> + exists q n', n = S n' /\ + <{ * <{ + uintptr q + + anyval (array (uint 8) (blk_size - sizeof uintptr)) }> a + * fixed_size_free_list blk_size n' q }> m. +Proof. + intros. destruct n; simpl in *. + - unfold emp in H0. exfalso. apply proj2 in H0. congruence. + - steps. +Qed. + +Definition allocator(block_size nRemaining: Z)(outer_addr: word): mem -> Prop := + ex1 (fun addr => <{ + * fmalloc_state {| block_size := block_size; free_list := addr |} outer_addr + * fixed_size_free_list block_size (Z.to_nat nRemaining) addr + * emp (0 <= nRemaining /\ 2 * sizeof uintptr <= block_size < 2 ^ bitwidth) + }>). + +(* Note: size argument is ignored (but other implementations that allow different + sizes might need it) *) +Definition freeable(sz: Z)(a: word): mem -> Prop := + emp (a <> /[0]). (* TODO maybe this should be in array instead? *) + +Local Hint Extern 1 (cannot_purify (fixed_size_free_list _ _ _)) + => constructor : suppressed_warnings. +Local Hint Extern 1 (cannot_purify (allocator _ _ _)) + => constructor : suppressed_warnings. +Local Hint Extern 1 (cannot_purify (freeable _ _)) + => constructor : suppressed_warnings. +Local Hint Extern 1 (PredicateSize_not_found (fixed_size_free_list _ _)) + => constructor : suppressed_warnings. + +Local Hint Unfold + allocator + freeable +: heapletwise_always_unfold. + +Ltac predicates_safe_to_cancel_hook hypPred conclPred ::= + lazymatch conclPred with + | fmalloc_state {| free_list := ?addr2 |} => + lazymatch hypPred with + | fmalloc_state {| free_list := ?addr1 |} => + is_evar addr2; unify addr1 addr2 + end + end. + +#[export] Instance spec_of_fmalloc_init: fnspec := .**/ + +void fmalloc_init(uintptr_t a, uintptr_t buf, uintptr_t blk_size, uintptr_t n) /**# + ghost_args := (R: mem -> Prop); + requires t m := 2 * sizeof uintptr <= \[blk_size] /\ + (* disallow wrap to avoid null pointers in free list: *) + \[buf] <> 0 /\ \[buf] + \[n] * \[blk_size] < 2 ^ bitwidth /\ + <{ * array (uint 8) (sizeof fmalloc_state) ? a + * array (uint 8) (\[blk_size] * \[n]) ? buf + * R }> m; + ensures t' m' := t' = t /\ + <{ * allocator \[blk_size] \[n] a + * R }> m' #**/ /**. +Derive fmalloc_init SuchThat (fun_correct! fmalloc_init) As fmalloc_init_ok. .**/ +{ /**. .**/ + uintptr_t tail = 0; /**. .**/ + uintptr_t head = buf + blk_size * n; /**. + + pose proof (fixed_size_free_list_nil \[blk_size]) as A. + rewrite <- (mmap.du_empty_r m3) in D. + forget (map.empty (map := mem)) as mE. + change (mE |= fixed_size_free_list \[blk_size] 0 /[0]) in A. + swap /[0] with tail in A. + delete #(tail = ??). + let h := find #(?? + ?? < ??) in move h after tail. + let h := find #(?? <= ??) in move h after tail. + pose (nOrig := n). swap n with nOrig in #(?? < 2 ^ ??). + change n with nOrig at 2. + swap O with (Z.to_nat (\[nOrig] - \[n])) in A. + prove (0 <= \[n] <= \[nOrig]). + swap nOrig with n in #(head = ??). + clearbody nOrig. + move n after tail. + loop invariant above tail. + .**/ + while (0 < n) /* decreases n */ { /**. .**/ + head = head - blk_size; /**. .**/ + n = n - 1; /**. + + assert (\[head ^- buf] + sizeof uintptr <= \[blk_size] * \[n']). { + (* TODO can we automate this proof so that the assertion is not needed + any more, because the subrange check that needs it finds it on its own? *) + subst head. + subst head'. + bottom_up_simpl_in_goal. + replace (blk_size ^* n' ^- blk_size) with (blk_size ^* (n' ^- /[1])) by ring. + (* non-linear arithmetic! *) + rewrite word.unsigned_mul_nowrap. + 2: { + eapply Z.le_lt_trans. 2: eassumption. + rewrite Z.mul_comm. + etransitivity. + 1: eapply Z.mul_le_mono_nonneg_r. 1: solve [steps]. + 1: instantiate (1 := \[nOrig]). + all: steps. + } + replace \[n' ^- /[1]] with (\[n'] - 1) by steps. steps. + } .**/ + store(head, tail); /**. .**/ + tail = head; /**. .**/ + } /**. + unfold split_concl_at. + replace (\[blk_size] * \[n]) with \[head ^- buf]. + 2: { + subst head head' n. + bottom_up_simpl_in_goal. + replace (blk_size ^* n' ^- blk_size) with (blk_size ^* (n' ^- /[1])) by ring. + (* non-linear arithmetic! *) + rewrite word.unsigned_mul_nowrap. + 2: { + eapply Z.le_lt_trans. 2: eassumption. + rewrite Z.mul_comm. + etransitivity. + 1: eapply Z.mul_le_mono_nonneg_r. 1: solve [steps]. + 1: instantiate (1 := \[nOrig]). + all: steps. + } + steps. + } + step. step. + replace (Z.to_nat (\[nOrig] - \[n])) with (S (Z.to_nat (\[nOrig] - \[n']))). + 2: { + subst n. steps. + } + simpl fixed_size_free_list. + steps. + + subst tail head head'. + assert (0 < \[buf ^+ blk_size ^* n' ^- blk_size]). + 2: solve [steps]. + eapply Z.lt_le_trans with (m := \[buf]). 1: solve[steps]. + replace (buf ^+ blk_size ^* n' ^- blk_size) + with (buf ^+ blk_size ^* (n' ^- /[1])) by ring. + rewrite word.unsigned_add_nowrap. 1: solve[steps]. + (* non-linear arithmetic! *) + eapply Z.le_lt_trans. + 2: eassumption. + eapply (proj1 (Z.add_le_mono_l _ _ _)). + rewrite Z.mul_comm. + rewrite word.unsigned_mul_nowrap. + 2: { + eapply Z.le_lt_trans. 2: eassumption. + rewrite Z.mul_comm. + etransitivity. + 1: eapply Z.mul_le_mono_nonneg_r. 1: solve [steps]. + 1: instantiate (1 := \[nOrig]). + all: steps. + } + eapply Z.mul_le_mono_nonneg_l; solve [steps]. + + rewrite mmap.du_empty_l. + lazymatch goal with + | H: with_mem ?m (array _ ?n ? _) |- canceling nil (mmap.Def ?m) True => + replace n with 0 in H + end. + prove_emp_in_hyps. steps. + subst head head' tail. + bottom_up_simpl_in_goal. + rewrite word.unsigned_sub_nowrap. + 2: { + rewrite word.unsigned_mul_nowrap by nia. + nia. + } + rewrite word.unsigned_mul_nowrap by nia. + steps. + .**/ + store(a, blk_size); /**. .**/ + store(a+sizeof(uintptr_t), tail); /**. + + assert (n = /[0]) as Hn by steps. + rewrite Hn in *|-. + bottom_up_simpl_in_hyps. + prove_emp_in_hyps. + repeat heapletwise_step. + .**/ +} /**. + unfold fmalloc_state, split_concl_at. + steps. +Qed. + +#[export] Instance spec_of_fmalloc_has_space: fnspec := .**/ + +uintptr_t fmalloc_has_space(uintptr_t al) /**# + ghost_args := blk_size n_remaining (R: mem -> Prop); + requires t m := <{ * allocator blk_size n_remaining al + * R }> m; + ensures t' m' r := t' = t /\ + ((\[r] = 0 /\ n_remaining = 0) \/ (\[r] = 1 /\ 0 < n_remaining)) /\ + <{ * allocator blk_size n_remaining al + * R }> m' #**/ /**. +Derive fmalloc_has_space + SuchThat (fun_correct! fmalloc_has_space) As fmalloc_has_space_ok. .**/ +{ /**. .**/ + uintptr_t l = load(al + sizeof(uintptr_t)); /**. .**/ + return l != 0; /**. + unfold expr.not. (* TODO support boolean operators in non-condition position *) + steps. .**/ +} /**. + destr (word.eqb l /[0]); [left|right]; steps. + - let H := constr:(#(fixed_size_free_list)) in eapply fixed_size_free_list_null in H. + steps. + - let H := constr:(#(fixed_size_free_list)) in eapply fixed_size_free_list_nonnull in H. + 2: assumption. + steps. lia. +Qed. + +#[export] Instance spec_of_fmalloc: fnspec := .**/ + +uintptr_t fmalloc(uintptr_t al) /**# + ghost_args := blk_size n_remaining (R: mem -> Prop); + requires t m := <{ * allocator blk_size n_remaining al + * R }> m; + ensures t' m' p := t' = t /\ + if \[p] =? 0 then + n_remaining = 0 /\ + <{ * allocator blk_size 0 al + * R }> m' + else + <{ * allocator blk_size (n_remaining - 1) al + * array (uint 8) blk_size ? p + * freeable blk_size p + * R }> m' #**/ /**. +Derive fmalloc SuchThat (fun_correct! fmalloc) As fmalloc_ok. .**/ +{ /**. .**/ + uintptr_t l = load(al + sizeof(uintptr_t)); /**. .**/ + if (l) /* split */ { /**. + + let H := constr:(#(fixed_size_free_list ?? ??)) in + eapply fixed_size_free_list_nonnull in H. + 2: assumption. fwd. repeat heapletwise_step. + .**/ + store(al + sizeof(uintptr_t), load(l)); /**. + + let H := constr:(#(array (uint 8))) in rename H into h. + unfold with_mem in h. + eapply cast_to_anybytes in h. + 2: { eauto with contiguous. } + bottom_up_simpl_in_hyp h. + lazymatch type of h with + | ?p ?m => change (with_mem m p) in h + end. + .**/ + return l; /**. .**/ + } /**. + replace (\[l] =? 0) with false; steps. + replace (Z.to_nat (n_remaining - 1)) with n'; steps. .**/ + else { /**. .**/ + return 0; /**. .**/ + } /**. + let H := constr:(#fixed_size_free_list) in eapply fixed_size_free_list_null in H. + steps. + simpl fixed_size_free_list. + let H := constr:(#fixed_size_free_list) in eapply fixed_size_free_list_null in H. + steps. + .**/ +} /**. +Qed. + +#[export] Instance spec_of_fmalloc_free: fnspec := .**/ + +void fmalloc_free (uintptr_t al, uintptr_t p) /**# + ghost_args := blk_size n_remaining (R: mem -> Prop); + requires t m := <{ * allocator blk_size n_remaining al + * array (uint 8) blk_size ? p + * freeable blk_size p + * R }> m; + ensures t' m' := t' = t /\ + <{ * allocator blk_size (n_remaining + 1) al + * R }> m' #**/ /**. +Derive fmalloc_free SuchThat + (fun_correct! fmalloc_free) As fmalloc_free_ok. .**/ +{ /**. .**/ + store(p, load(al+sizeof(uintptr_t))); /**. .**/ + store(al+sizeof(uintptr_t), p); /**. .**/ +} /**. + replace (Z.to_nat (n_remaining + 1)) with (S (Z.to_nat n_remaining)) by lia. + simpl fixed_size_free_list. + prove_emp_in_hyps. + steps. +Qed. + +End LiveVerif. + +#[export] Hint Extern 1 (cannot_purify (freeable _ _)) + => constructor : suppressed_warnings. +#[export] Hint Extern 1 (PredicateSize_not_found (freeable _)) + => constructor : suppressed_warnings. +#[export] Hint Extern 1 (PredicateSize_not_found (allocator _ _)) + => constructor : suppressed_warnings. +#[export] Hint Extern 1 (cannot_purify (allocator _ _ _)) + => constructor : suppressed_warnings. + +Comments .**/ //. diff --git a/LiveVerifEx64/src/LiveVerifExamples/onesize_malloc.v b/LiveVerifEx64/src/LiveVerifExamples/onesize_malloc.v deleted file mode 120000 index 4c23b8a9..00000000 --- a/LiveVerifEx64/src/LiveVerifExamples/onesize_malloc.v +++ /dev/null @@ -1 +0,0 @@ -../../../LiveVerif/src/LiveVerifExamples/onesize_malloc.v \ No newline at end of file diff --git a/LiveVerifEx64/src/LiveVerifExamples/onesize_malloc.v b/LiveVerifEx64/src/LiveVerifExamples/onesize_malloc.v new file mode 100644 index 00000000..de3ff504 --- /dev/null +++ b/LiveVerifEx64/src/LiveVerifExamples/onesize_malloc.v @@ -0,0 +1,345 @@ +(* -*- eval: (load-file "../LiveVerif/live_verif_setup.el"); -*- *) +Require Import LiveVerif.LiveVerifLib. + +Class malloc_constants: Set := { + malloc_state_ptr: Z; + malloc_block_size: Z; +}. + +Load LiveVerif. + +Record malloc_state := { + free_list: word; +}. + +Definition malloc_state_t(s: malloc_state): word -> mem -> Prop := .**/ + +typedef struct __attribute__ ((__packed__)) { + uintptr_t free_list; +} malloc_state_t; + +/**. + +Context {consts: malloc_constants}. + +(* The Inductive conveniently provides the fuel needed for the recursion *) +Inductive fixed_size_free_list(block_size: Z): word -> mem -> Prop := +| fixed_size_free_list_nil p m: + p = /[0] -> + emp True m -> + fixed_size_free_list block_size p m +| fixed_size_free_list_cons p q m: + p <> /[0] -> + <{ * <{ + uintptr q + + anyval (array (uint 8) (block_size - sizeof uintptr)) }> p + * fixed_size_free_list block_size q }> m -> + fixed_size_free_list block_size p m. + +Definition allocator_with_potential_failure(f: option Z): mem -> Prop := + ex1 (fun addr => <{ + * malloc_state_t {| free_list := addr |} /[malloc_state_ptr] + * fixed_size_free_list malloc_block_size addr + * emp (match f with + | Some n => (* empty free list *) + addr = /[0] \/ + (* trying to allocate more than supported *) + malloc_block_size < n + | None => True + end) + * emp (2 * sizeof uintptr <= malloc_block_size < 2 ^ bitwidth) + }>). + +Definition allocator: mem -> Prop := + allocator_with_potential_failure None. +Definition allocator_cannot_allocate(n: Z): mem -> Prop := + allocator_with_potential_failure (Some n). + +Definition allocator_failed_below(n: Z): mem -> Prop := + ex1 (fun amount => <{ * allocator_cannot_allocate amount + * emp (amount <= n) }>). + +Lemma allocator_failed_below_monotone: forall n1 n2 m, + n1 <= n2 -> + allocator_failed_below n1 m -> + allocator_failed_below n2 m. +Proof. + unfold allocator_failed_below, ex1. intros. fwd. eexists. + eapply sep_emp_r. eapply sep_emp_r in H0. destruct H0. split. + - eassumption. + - etransitivity; eassumption. +Qed. + +Definition freeable(sz: Z)(a: word): mem -> Prop := + <{ * emp (a <> /[0]) (* TODO maybe this should be in array instead? *) + * array (uint 8) (malloc_block_size - sz) ? (a ^+ /[sz]) }>. + +Local Hint Extern 1 (cannot_purify (fixed_size_free_list _ _)) + => constructor : suppressed_warnings. +Local Hint Extern 1 (cannot_purify allocator) + => constructor : suppressed_warnings. +Local Hint Extern 1 (cannot_purify (allocator_cannot_allocate _)) + => constructor : suppressed_warnings. +Local Hint Extern 1 (cannot_purify (allocator_with_potential_failure _)) + => constructor : suppressed_warnings. +Local Hint Extern 1 (cannot_purify (freeable _ _)) + => constructor : suppressed_warnings. +Local Hint Extern 1 (PredicateSize_not_found (fixed_size_free_list _)) + => constructor : suppressed_warnings. + +Local Hint Unfold + allocator + allocator_cannot_allocate + allocator_failed_below + allocator_with_potential_failure + freeable +: heapletwise_always_unfold. + +Ltac predicates_safe_to_cancel_hook hypPred conclPred ::= + lazymatch conclPred with + | malloc_state_t {| free_list := ?addr2 |} => + lazymatch hypPred with + | malloc_state_t {| free_list := ?addr1 |} => + is_evar addr2; unify addr1 addr2 + end + end. + +Lemma recover_allocator_cannot_allocate: forall n, + impl1 (allocator_cannot_allocate n) allocator. +Proof. + unfold allocator_cannot_allocate, allocator, allocator_with_potential_failure. + intros n m M. steps. +Qed. + +Lemma recover_allocator_failed_below: forall n m, + allocator_failed_below n m -> allocator m. +Proof. + unfold allocator_failed_below. intros. destruct H as [amount H]. + eapply sep_emp_r in H. eapply recover_allocator_cannot_allocate. eapply H. +Qed. + +Axiom TODO: False. + +#[export] Instance spec_of_Malloc_init: fnspec := .**/ + +void Malloc_init (uintptr_t p, uintptr_t n) /**# + ghost_args := (R: mem -> Prop); + requires t m := 2 * sizeof uintptr <= malloc_block_size < 2 ^ bitwidth /\ + \[n] mod malloc_block_size = 0 /\ + \[p] + \[n] < 2 ^ bitwidth /\ (* <-- no wrap around because otherwise + some pointers in free list might be null *) + <{ * array (uint 8) (sizeof malloc_state_t) ? /[malloc_state_ptr] + * array (uint 8) \[n] ? p + * R }> m; + ensures t' m' := t' = t /\ + <{ * allocator + * R }> m' #**/ /**. +Derive Malloc_init SuchThat (fun_correct! Malloc_init) As Malloc_init_ok. .**/ +{ /**. .**/ + store(malloc_state_ptr, p); /**. .**/ + uintptr_t tail = 0; /**. .**/ + uintptr_t head = p + n; /**. + + assert (\[n] = \[n] / malloc_block_size * malloc_block_size) as NAlt. { + Z.div_mod_to_equations. (* <-- also adds eqs for non-const modulo *) + lia. + } + assert (0 <= \[n] / malloc_block_size). { + zify_goal. + Z.div_mod_to_equations. (* <-- also adds eqs for non-const modulo *) + lia. + } + forget (\[n] / malloc_block_size) as c. + let h := find #(array (uint 8)) in rewrite NAlt in h. + let h := find #(\[p] + \[n]) in rewrite NAlt in h. + let h := find #(head = ??) in replace n with (/[c] ^* /[malloc_block_size]) in Def1 by steps. + pose proof (fixed_size_free_list_nil malloc_block_size tail map.empty + ltac:(assumption) ltac:(unfold emp; auto)) as A. + rewrite <- (mmap.du_empty_r m3) in D0. + forget (map.empty (map := mem)) as m. + change (m |= fixed_size_free_list malloc_block_size tail) in A. + delete #(tail = ??). + let h := find #(?? <= malloc_block_size < ??) in move h after tail. + delete #(?? mod malloc_block_size = 0). + prove (c * malloc_block_size < 2 ^ bitwidth). + delete #(\[n] = ??). (* try to not use n any more *) + loop invariant above tail. + .**/ + while (head != p) /* decreases c */ { /**. .**/ + head = head - malloc_block_size; /**. + + assert (\[head ^- p] + sizeof uintptr <= c * malloc_block_size). { + (* TODO can we automate this proof so that the assertion is not needed + any more, because the subrange check that needs it finds it on its own? *) + subst head. + subst head'. + bottom_up_simpl_in_goal. + zify_hyps. + assert (0 < c) by lia. + replace (/[c]) with (/[c-1] ^+ /[1]). + 2: solve [steps]. + bottom_up_simpl_in_goal. + zify_goal. + lia. + } .**/ + store(head, tail); /**. .**/ + tail = head; /**. .**/ + } /*?. + lazymatch goal with + | H: merge_step _ |- _ => clear H + end. + step. step. step. step. step. step. step. step. step. step. step. step. step. + instantiate (1 := c - 1). solve [step]. + 2: solve [step]. + steps. + + unzify. + case TODO. +(* + assert (\[tail] <> 0). { + subst. + assert (0 < c) by lia. + replace (/[c]) with (/[c-1] ^+ /[1]). + 2: solve [steps]. + bottom_up_simpl_in_goal. + zify_goal. + lia. + + zify_goal. + by steps. + 2: { + clear Error. unfold find_hyp_for_range. + unzify. + + +assert (subrange head 4 p (c * malloc_block_size * 1)). { + unfold subrange. + subst head. + subst head'. + bottom_up_simpl_in_goal. + + clear Error. + assert (0 < c) by lia. + replace (/[c]) with (/[c-1] ^+ /[1]). + 2: solve [steps]. + bottom_up_simpl_in_goal. + + zify_goal. + lia. + +clear Error. +Search p. + +jj +*) + .**/ +} /**. + all: case TODO. + Unshelve. try exact (word.of_Z 0). +Qed. + +#[export] Instance spec_of_Malloc: fnspec := .**/ + +uintptr_t Malloc (uintptr_t n) /**# + ghost_args := (R: mem -> Prop); + requires t m := <{ * allocator + * R }> m; + ensures t' m' p := t' = t /\ + <{ * (if \[p] =? 0 then + allocator_failed_below \[n] + else + <{ * allocator + * array (uint 8) \[n] ? p + * freeable \[n] p }>) + * R }> m' #**/ /**. +Derive Malloc SuchThat (fun_correct! Malloc) As Malloc_ok. .**/ +{ /**. .**/ + uintptr_t l = load(malloc_state_ptr); /**. .**/ + if (l != 0 && n <= malloc_block_size) /* split */ { /**. + + let H := constr:(#(fixed_size_free_list ?? ??)) in inversion H; clear H. + (* TODO better inversion tactic for such use cases *) + 1: congruence. + repeat let lastHypType := lazymatch goal with _: ?t |- _ => t end in + lazymatch lastHypType with + | ?lhs = _ => subst lhs + end. + repeat heapletwise_step. + .**/ + store(malloc_state_ptr, load(l)); /**. + + let H := constr:(#(array (uint 8))) in rename H into h. + unfold with_mem in h. + eapply cast_to_anybytes in h. + 2: { eauto with contiguous. } + bottom_up_simpl_in_hyp h. + lazymatch type of h with + | ?p ?m => change (with_mem m p) in h + end. + .**/ + return l; /**. .**/ + } /**. + replace (\[l] =? 0) with false; steps. .**/ + else { /**. .**/ + return 0; /**. .**/ + } /**. + replace (\[/[0]] =? 0) with true; steps. + instantiate (1 := \[n]). 1-2: steps. + .**/ +} /**. +Qed. + +#[export] Instance spec_of_Free: fnspec := .**/ + +void Free (uintptr_t p) /**# + ghost_args := n (R: mem -> Prop); + requires t m := <{ * allocator + * array (uint 8) \[n] ? p + * freeable \[n] p + * R }> m; + ensures t' m' := t' = t /\ + <{ * allocator + * R }> m' #**/ /**. +Derive Free SuchThat (fun_correct! Free) As Free_ok. .**/ +{ /**. + pose proof merge_anyval_array as M. + specialize M with (addr := p). + start_canceling_in_hyp M. + canceling_step_in_hyp M. + rewrite Z.mul_1_l in M. + rewrite word.of_Z_unsigned in M. + canceling_step_in_hyp M. + eapply canceling_done_in_hyp in M. + destruct M as (?m, (?D, ?H)). + bottom_up_simpl_in_hyp H. + .**/ + store(p, load(malloc_state_ptr)); /**. .**/ + store(malloc_state_ptr, p); /**. + + discard_merge_step. + epose proof (fixed_size_free_list_cons malloc_block_size p) as HL. + lazymatch goal with + | H: p <> /[0] |- _ => specialize HL with (1 := H) + end. + unfold sepapps, List.fold_right, proj_predicate, sepapp_sized_predicates, + sepapp, sized_emp in HL. + cancel_in_hyp HL. + .**/ +} /**. +Qed. + +End LiveVerif. + +#[export] Hint Extern 1 (cannot_purify (freeable _ _)) + => constructor : suppressed_warnings. +#[export] Hint Extern 1 (PredicateSize_not_found (freeable _)) + => constructor : suppressed_warnings. +#[export] Hint Extern 1 (PredicateSize_not_found allocator_failed_below) + => constructor : suppressed_warnings. +#[export] Hint Extern 1 (PredicateSize_not_found (@allocator _ _)) + => constructor : suppressed_warnings. +#[export] Hint Extern 1 (cannot_purify allocator) + => constructor : suppressed_warnings. +#[export] Hint Extern 1 (cannot_purify (allocator_failed_below _)) + => constructor : suppressed_warnings. + +Comments .**/ //. diff --git a/LiveVerifEx64/src/LiveVerifExamples/tree_set.v b/LiveVerifEx64/src/LiveVerifExamples/tree_set.v deleted file mode 120000 index 8a9dc05a..00000000 --- a/LiveVerifEx64/src/LiveVerifExamples/tree_set.v +++ /dev/null @@ -1 +0,0 @@ -../../../LiveVerif/src/LiveVerifExamples/tree_set.v \ No newline at end of file diff --git a/LiveVerifEx64/src/LiveVerifExamples/tree_set.v b/LiveVerifEx64/src/LiveVerifExamples/tree_set.v new file mode 100644 index 00000000..9b2266d5 --- /dev/null +++ b/LiveVerifEx64/src/LiveVerifExamples/tree_set.v @@ -0,0 +1,435 @@ +(* -*- eval: (load-file "../LiveVerif/live_verif_setup.el"); -*- *) +Require Import LiveVerif.LiveVerifLib. +Require Import LiveVerifExamples.onesize_malloc. +Require Import coqutil.Datatypes.PropSet. + +Inductive tree_skeleton: Set := +| Leaf +| Node(leftChild rightChild: tree_skeleton). + +Definition tree_skeleton_lt(sk1 sk2: tree_skeleton): Prop := + match sk2 with + | Node leftChild rightChild => sk1 = leftChild \/ sk1 = rightChild + | Leaf => False + end. + +Lemma tree_skeleton_lt_wf: well_founded tree_skeleton_lt. +Proof. + unfold well_founded. intros sk2. + induction sk2; eapply Acc_intro; intros sk1 Lt; unfold tree_skeleton_lt in Lt. + - contradiction. + - destruct Lt; subst; assumption. +Qed. + +#[local] Hint Resolve tree_skeleton_lt_wf: wf_of_type. + +Lemma tree_skeleton_lt_l: forall sk1 sk2, + safe_implication True (tree_skeleton_lt sk1 (Node sk1 sk2)). +Proof. unfold safe_implication, tree_skeleton_lt. intros. auto. Qed. + +Lemma tree_skeleton_lt_r: forall sk1 sk2, + safe_implication True (tree_skeleton_lt sk2 (Node sk1 sk2)). +Proof. unfold safe_implication, tree_skeleton_lt. intros. auto. Qed. + +#[local] Hint Resolve tree_skeleton_lt_l tree_skeleton_lt_r : safe_implication. + +Definition same_set{A: Type}(s1 s2: set A) := forall x, s1 x <-> s2 x. +Definition is_empty_set{A: Type}(s: set A) := forall x, ~ s x. + +Load LiveVerif. + +Context {consts: malloc_constants}. + +Fixpoint bst'(sk: tree_skeleton)(s: set Z)(addr: word){struct sk}: mem -> Prop := + match sk with + | Leaf => emp (addr = /[0] /\ is_empty_set s) + | Node skL skR => EX (p: word) (v: Z) (q: word), + <{ * emp (addr <> /[0]) + * emp (s v) + * freeable (sizeof uintptr * 2 + 4) addr + * <{ + uintptr p + + uint 32 v + + uintptr q }> addr + * bst' skL (fun x => s x /\ x < v) p + * bst' skR (fun x => s x /\ v < x) q }> + end. + +(* Note: one level of indirection because sometimes we have to change the root + pointer (eg from null (empty) to non-null or vice versa) *) +Definition bst(s: set Z)(addr: word): mem -> Prop := + EX rootp, <{ * uintptr rootp addr + * EX sk: tree_skeleton, bst' sk s rootp }>. + +Local Hint Extern 1 (PredicateSize (bst' ?sk)) => + let r := eval cbv iota in + (match sk with + | Node _ _ => sizeof uintptr * 2 + 4 + | Leaf => 0 + end) in + exact r +: typeclass_instances. + +#[local] Hint Extern 1 (cannot_purify (bst' _ _ _)) + => constructor : suppressed_warnings. +#[local] Hint Extern 1 (cannot_purify (bst _ _)) + => constructor : suppressed_warnings. +#[local] Hint Extern 1 (cannot_purify (freeable _ _)) + => constructor : suppressed_warnings. + +#[local] Hint Unfold bst : heapletwise_always_unfold. + +Lemma invert_bst'_null{sk s p m}: + p = /[0] -> + m |= bst' sk s p -> + sk = Leaf /\ + m |= emp (forall x, ~ s x). +Proof. + unfold with_mem. intros. subst. destruct sk; simpl in *. + - unfold emp in *. intuition auto. + - repeat heapletwise_step. exfalso. apply H1. reflexivity. +Qed. + +Lemma invert_bst'_nonnull{sk s p m}: + p <> /[0] -> + m |= bst' sk s p -> + exists skL skR pL v pR, + sk = Node skL skR /\ + s v /\ + <{ * freeable (sizeof uintptr * 2 + 4) p + * <{ + uintptr pL + + uint 32 v + + uintptr pR }> p + * bst' skL (fun x => s x /\ x < v) pL + * bst' skR (fun x => s x /\ v < x) pR }> m. +Proof. + intros. + destruct sk; simpl in *. + { exfalso. unfold with_mem, emp in *. intuition idtac. } + repeat heapletwise_step. + eexists _, _, p0, v, q. split. 1: reflexivity. + split. 1: eassumption. + repeat heapletwise_step. +Qed. + + (* TODO use and move or delete *) + Lemma after_if_skip' b fs (PThen PElse Post: trace -> mem -> locals -> Prop): + bool_expr_branches b (forall t m l, PThen t m l -> Post t m l) + (forall t m l, PElse t m l -> Post t m l) True -> + @after_if _ _ _ _ _ _ fs b PThen PElse cmd.skip Post. + Proof. + intros. + unfold after_if. + intros ? ? ? [? ? ?]. subst x. + eapply wp_skip. + apply proj1 in H. + destruct b; eauto. + Qed. + +Import FunctionalExtensionality PropExtensionality. + +Lemma bst'_change_set: forall sk a s1 s2, + safe_implication (same_set s1 s2) (impl1 (bst' sk s1 a) (bst' sk s2 a)). +Proof. + unfold safe_implication, same_set. intros. + replace s2 with s1. 1: reflexivity. + extensionality x. + apply propositional_extensionality. + apply H. +Qed. + +#[local] Hint Resolve bst'_change_set : safe_implication. + +(* always unify (set A) with (A -> Prop) *) +#[global] Hint Transparent set : safe_implication. + +Ltac zset_solver := + unfold same_set, is_empty_set; + intros; + lazymatch goal with + | |- _ <-> _ => split + | |- _ => idtac + end; + intuition (lia || congruence || solve [eauto 3]). + +Ltac step_hook ::= + match goal with + | |- _ => progress cbn [bst'] + | |- context C[8 * 2 + 4] => let g := context C[20] in change g (* TODO generalize *) + | |- context C[4 * 2 + 4] => let g := context C[12] in change g (* TODO generalize *) + | sk: tree_skeleton |- _ => progress subst sk + | |- same_set _ _ => reflexivity (* <- might instantiate evars and we're fine with that *) + | |- same_set _ _ => zset_solver + | |- is_empty_set _ => zset_solver + | H: _ |= bst' _ _ ?p, E: ?p = /[0] |- _ => + assert_fails (has_evar H); eapply (invert_bst'_null E) in H + | H: _ |= bst' _ _ ?p, E: \[?p] = 0 |- _ => + eapply invert_bst'_null in H; [ | zify_goal; xlia zchecker ] + | H: _ |= bst' _ _ ?p, N: ?p <> /[0] |- _ => + assert_fails (has_evar H); eapply (invert_bst'_nonnull N) in H + | H: ?addr <> /[0] |- context[bst' ?sk_evar _ ?addr] => + is_evar sk_evar; + let n := open_constr:(Node _ _) in unify sk_evar n + | |- context[bst' ?skEvar ?s /[0]] => is_evar skEvar; unify skEvar Leaf + | s: set Z, H: forall x: Z, ~ _ |- _ => + lazymatch goal with + | |- context[s ?v] => + lazymatch type of H with + | context[s] => unique pose proof (H v) + end + end + | s: set Z |- _ => + match goal with + | H: s ?x1 |- s ?x2 => + assert_fails (idtac; has_evar x2); + assert_fails (idtac; has_evar x1); + replace x2 with x1; [exact H | solve[steps]] + | |- ~ s _ => zset_solver + end + | H: ?res = ?c1 /\ _ \/ ?res = ?c2 /\ _ + |- ?res = ?c1 /\ _ \/ ?res = ?c2 /\ _ => + assert_succeeds (idtac; assert (c1 <> c2) by (zify_goal; xlia zchecker)); + destruct H; [left|right] + | |- ?A \/ ?B => + tryif (assert_succeeds (assert (~ A) by (zify_goal; xlia zchecker))) + then right else + tryif (assert_succeeds (assert (~ B) by (zify_goal; xlia zchecker))) + then left else fail + | H1: ?x <= ?y, H2: ?y <= ?x, C: ?s ?x |- ?s ?y => + (replace y with x by xlia zchecker); exact C + | H: _ \/ _ |- _ => decompose [and or] H; clear H; try (exfalso; xlia zchecker); [] + | |- _ => solve [auto 3 with nocore safe_core] + end. + +Ltac predicates_safe_to_cancel_hook hypPred conclPred ::= + lazymatch conclPred with + | bst' ?sk2 ?s2 => + lazymatch hypPred with + | bst' ?sk1 ?s1 => + (* Note: address has already been checked, and if sk and/or s don't + unify, sidecondition solving steps will make them match later, + so here, we just need to take care of instantiating evars from conclPred *) + try syntactic_unify_only_inst_r s1 s2; + try syntactic_unify_only_inst_r sk1 sk2 + end + end. + +Ltac provide_new_ghosts_hook ::= manual_new_ghosts. + +#[export] Instance spec_of_bst_remove_max: fnspec := .**/ + +uintptr_t bst_remove_max(uintptr_t c) /**# + ghost_args := p s sk (R: mem -> Prop); + requires t m := p <> /[0] /\ + <{ * allocator + * uintptr p c + * bst' sk s p + * R }> m; + ensures t' m' r := t' = t /\ exists sk' q, + s \[r] /\ + (forall x, s x -> x <= \[r]) /\ + <{ * allocator + * uintptr q c + * bst' sk' (fun x => s x /\ x < \[r]) q + * R }> m' #**/ /**. +Derive bst_remove_max SuchThat (fun_correct! bst_remove_max) +As bst_remove_max_ok. .**/ +{ /**. .**/ + uintptr_t p = load(c); /**. .**/ + uintptr_t res = 0; /**. + (* Local Arguments ready : clear implicits. *) + loop invariant above p. + delete #(res = ??). + move skR before t. + .**/ + do /* initial_ghosts(s, c, skR, R); decreases skR */ { /**. .**/ + c = p + sizeof(uintptr_t) + 4; /**. .**/ + p = load(c); /**. .**/ + if (p) /* split */ { /**. .**/ + /* nothing to do */ /**. .**/ + } /**. + instantiate (3 := expr.var "p"). (* <-- need to give loop termination cond + already here... *) + steps. + new_ghosts((fun x => (s x /\ v < x)), c, skR, _). + steps. + { destr (x <=? v). 1: lia. eauto. } + .**/ + else { /**. .**/ + res = load32(c - 4); /**. .**/ + } /**. +Abort. + +#[export] Instance spec_of_bst_init: fnspec := .**/ + +void bst_init(uintptr_t p) /**# + ghost_args := (R: mem -> Prop); + requires t m := <{ * array (uint 8) (sizeof uintptr) ? p + * R }> m; + ensures t' m' := t' = t /\ + <{ * bst (fun _ => False) p + * R }> m' #**/ /**. +Derive bst_init SuchThat (fun_correct! bst_init) As bst_init_ok. .**/ +{ /**. .**/ + store(p, 0); /**. .**/ +} /**. +Qed. + +#[export] Instance spec_of_bst_alloc_node: fnspec := .**/ + +uintptr_t bst_alloc_node( ) /**# + ghost_args := (R: mem -> Prop); + requires t m := <{ * allocator + * R }> m; + ensures t' m' res := t' = t /\ + ((\[res] = 0 /\ <{ * allocator_failed_below (sizeof uintptr * 2 + 4) + * R }> m') \/ + (\[res] <> 0 /\ <{ * allocator + * freeable (sizeof uintptr * 2 + 4) res + * uintptr ? res + * uint 32 ? (res ^+ /[sizeof uintptr]) + * uintptr ? (res ^+ /[sizeof uintptr + 4]) + * R }> m')) #**/ /**. +Derive bst_alloc_node SuchThat (fun_correct! bst_alloc_node) +As bst_alloc_node_ok. .**/ +{ /**. .**/ + uintptr_t res = Malloc(sizeof(uintptr_t) + 4 + sizeof(uintptr_t)); /**. .**/ + return res; /**. .**/ +} /**. + destruct_one_match_hyp; steps. +Qed. + +Ltac provide_new_ghosts_hook ::= guess_new_ghosts. + +#[export] Instance spec_of_bst_add: fnspec := .**/ + +uintptr_t bst_add(uintptr_t p, uintptr_t vAdd) /**# + ghost_args := s (R: mem -> Prop); + requires t m := \[vAdd] < 2 ^ 32 /\ + <{ * allocator + * bst s p + * R }> m; + ensures t' m' r := t' = t /\ + ((\[r] = 0 /\ <{ * allocator_failed_below (sizeof uintptr * 2 + 4) + * bst s p + * R }> m') \/ + (\[r] = 1 /\ <{ * allocator + * bst (fun x => x = \[vAdd] \/ s x) p + * R }> m')) #**/ /**. +Derive bst_add SuchThat (fun_correct! bst_add) As bst_add_ok. .**/ +{ /**. .**/ + uintptr_t a = load(p); /**. + (* invariant: *p = a *) .**/ + uintptr_t found = 0; /**. + + pose (measure := sk). + prove (found = /[0] /\ measure = sk \/ found = /[1] /\ s \[vAdd]) as A. + move A before sk. + clearbody measure. + delete (#(found = /[0])). + move p after t. + move sk before t. + (* Local Arguments ready : clear implicits. *) + loop invariant above a. + (* Ltac log_packaged_context P ::= idtac P. *) + .**/ + while (a && !found) + /* initial_ghosts(p, s, sk, R); decreases(measure) */ + { /**. .**/ + uintptr_t x = load32(a + sizeof(uintptr_t)); /**. .**/ + if (x == vAdd) /* split */ { /**. .**/ + found = 1; /**. .**/ + } /**. + (* arbitrarily pick skL, could also pick skR, just need something smaller *) + eapply tree_skeleton_lt_l. constructor. .**/ + else { /**. .**/ + if (vAdd < x) /* split */ { /**. .**/ + p = a; /**. .**/ + a = load(p); /**. .**/ + } /**. .**/ + else { /**. .**/ + p = a + sizeof(uintptr_t) + 4; /**. .**/ + a = load(p); /**. .**/ + } /**. .**/ + } /**. .**/ + } /**. .**/ + if (found) /* split */ { /**. .**/ + return 1; /**. .**/ + } /**. .**/ + else { /**. .**/ + /* key not found, so we zoomed into the tree until it is empty, and + shrinked the function's postcondition and the context -- there's + no more tree around, and we'll just retrun a singleton tree! */ /**. .**/ + uintptr_t res = bst_alloc_node(); /**. .**/ + if (res) /* split */ { /**. .**/ + store(res, 0); /**. .**/ + store32(res + sizeof(uintptr_t), vAdd); /**. .**/ + store(res + sizeof(uintptr_t) + 4, 0); /**. .**/ + store(p, res); /**. .**/ + return 1; /**. .**/ + } /**. .**/ + else { /**. .**/ + /* malloc failed! */ /**. .**/ + return 0; /**. .**/ + } /**. .**/ + } /**. .**/ +} /**. +Qed. + +#[export] Instance spec_of_bst_contains: fnspec := .**/ + +uintptr_t bst_contains(uintptr_t p, uintptr_t query) /**# + ghost_args := s (R: mem -> Prop); + requires t m := <{ * bst s p + * R }> m; + ensures t' m' b := t' = t /\ + (\[b] = 1 /\ s \[query] \/ \[b] = 0 /\ ~ s \[query]) /\ + <{ * bst s p + * R }> m' #**/ /**. +Derive bst_contains SuchThat (fun_correct! bst_contains) As bst_contains_ok. .**/ +{ /**. .**/ + uintptr_t found = 0; /**. .**/ + uintptr_t a = load(p); /**. + + move sk after found. + pose (measure := sk). + loop invariant above a. + prove (found = /[0] /\ measure = sk \/ found = /[1] /\ s \[query]) as A. + move A before found. + delete #(found = ??). + clearbody measure. + move sk before t. + (* Ltac log_packaged_context P ::= idtac P. *) + .**/ + while (!found && a != 0) + /* initial_ghosts(p, s, sk, R); decreases measure */ + { /**. .**/ + uintptr_t here = load32(a + sizeof(uintptr_t)); /**. .**/ + if (query < here) /* split */ { /**. .**/ + p = a; /**. .**/ + a = load(p); /**. .**/ + } /**. .**/ + else { /**. .**/ + if (here < query) /* split */ { /**. .**/ + p = a + sizeof(uintptr_t) + 4; /**. .**/ + a = load(p); /**. .**/ + } /**. .**/ + else { /**. .**/ + found = 1; /**. .**/ + } /**. + (* arbitrarily pick skL, could also pick skR, just need something smaller *) + eapply tree_skeleton_lt_l. constructor. .**/ + } /**. .**/ + } /**. .**/ + return found; /**. .**/ +} /**. + destr (\[a] =? 0); steps. zset_solver. +Qed. + +(* Note: inability to break out of loop is cumbersome, because it complicates pre: + - it has to incorporate almost all of post for the res=true case + ==> not too bad though, in these examples + - and even if we are done, we still have to decrease the termination measure + ==> trick: separate variable for termination measure, and only link it to sep + clauses in pre if done flag is false *) + +End LiveVerif. Comments .**/ //. diff --git a/bedrock2/src/bedrock2/AbsintWordToZ.v b/bedrock2/src/bedrock2/AbsintWordToZ.v index 36da9b13..5640e8a3 100644 --- a/bedrock2/src/bedrock2/AbsintWordToZ.v +++ b/bedrock2/src/bedrock2/AbsintWordToZ.v @@ -1,4 +1,4 @@ -Require Import Coq.Strings.String Coq.ZArith.ZArith. +From Coq Require Import String ZArith. From coqutil Require Import Word.Interface Word.Properties. From coqutil Require Import Tactics.rdelta Z.div_mod_to_equations. Require Import coqutil.Z.Lia. @@ -43,7 +43,7 @@ Ltac named_pose_asfresh_or_id x n := y. Ltac requireZcst z := - lazymatch Coq.setoid_ring.InitialRing.isZcst z with + lazymatch InitialRing.isZcst z with | true => idtac end. Ltac requireZcstExpr e := diff --git a/bedrock2/src/bedrock2/Array.v b/bedrock2/src/bedrock2/Array.v index 05314357..2df5300a 100644 --- a/bedrock2/src/bedrock2/Array.v +++ b/bedrock2/src/bedrock2/Array.v @@ -1,5 +1,5 @@ Require Import coqutil.Map.Interface bedrock2.Map.Separation bedrock2.Map.SeparationLogic bedrock2.Lift1Prop bedrock2.Memory. -Require Import Coq.Lists.List Coq.ZArith.BinInt. Local Open Scope Z_scope. +From Coq Require Import List BinInt. Local Open Scope Z_scope. Require Import coqutil.Word.Interface coqutil.Word.Properties. Require Import coqutil.Z.Lia. Require Import coqutil.Byte. diff --git a/bedrock2/src/bedrock2/ArrayCasts.v b/bedrock2/src/bedrock2/ArrayCasts.v index 94c7be8b..bcbe4af3 100644 --- a/bedrock2/src/bedrock2/ArrayCasts.v +++ b/bedrock2/src/bedrock2/ArrayCasts.v @@ -1,9 +1,9 @@ Require Import coqutil.Map.Interface bedrock2.Map.Separation bedrock2.Map.SeparationLogic bedrock2.Lift1Prop bedrock2.Memory. -Require Import Coq.Lists.List Coq.ZArith.BinInt. Local Open Scope Z_scope. +From Coq Require Import List BinInt. Local Open Scope Z_scope. Require Import coqutil.Word.Interface coqutil.Word.Properties coqutil.Word.Bitwidth. -Require Import coqutil.Z.Lia Coq.micromega.Lia. +Require Import coqutil.Z.Lia Lia. Require Import coqutil.Byte. -Require Import Coq.Arith.PeanoNat. +Require Import PeanoNat. Require Import coqutil.Word.LittleEndianList. Require Import bedrock2.Array bedrock2.Scalars. diff --git a/bedrock2/src/bedrock2/BasicC32Semantics.v b/bedrock2/src/bedrock2/BasicC32Semantics.v index 752836c3..729072bf 100644 --- a/bedrock2/src/bedrock2/BasicC32Semantics.v +++ b/bedrock2/src/bedrock2/BasicC32Semantics.v @@ -1,4 +1,4 @@ -Require Import Coq.ZArith.ZArith. +From Coq Require Import ZArith. Require Import bedrock2.Syntax bedrock2.Semantics. Require coqutil.Datatypes.String coqutil.Map.SortedList coqutil.Map.SortedListString. Require Import coqutil.Word.Interface coqutil.Map.SortedListWord. diff --git a/bedrock2/src/bedrock2/BasicC64Semantics.v b/bedrock2/src/bedrock2/BasicC64Semantics.v index d7e89cf0..5eed85ed 100644 --- a/bedrock2/src/bedrock2/BasicC64Semantics.v +++ b/bedrock2/src/bedrock2/BasicC64Semantics.v @@ -1,4 +1,4 @@ -Require Import Coq.ZArith.ZArith. +From Coq Require Import ZArith. Require Import bedrock2.Syntax bedrock2.Semantics. Require coqutil.Datatypes.String coqutil.Map.SortedList coqutil.Map.SortedListString. Require Import coqutil.Word.Interface coqutil.Map.SortedListWord. diff --git a/bedrock2/src/bedrock2/ByteListPredicates.v b/bedrock2/src/bedrock2/ByteListPredicates.v index f1bd25b4..f0e9af6a 100644 --- a/bedrock2/src/bedrock2/ByteListPredicates.v +++ b/bedrock2/src/bedrock2/ByteListPredicates.v @@ -19,9 +19,9 @@ + pointer_to (ethernet_header h) }> *) -Require Import Coq.Logic.PropExtensionality. -Require Import Coq.Logic.FunctionalExtensionality. -Require Import Coq.Lists.List. +From Coq Require Import PropExtensionality. +From Coq Require Import FunctionalExtensionality. +From Coq Require Import List. Require Import coqutil.Byte. Lemma bp_ext: forall (P Q: list byte -> Prop), (forall bs, P bs <-> Q bs) -> P = Q. @@ -92,7 +92,7 @@ Proof. - rewrite IHPs. symmetry. apply bp_app_assoc. Qed. -Require Import Coq.ZArith.ZArith. Local Open Scope Z_scope. +From Coq Require Import ZArith. Local Open Scope Z_scope. Section Array. Context [E: Type] (elem: E -> list byte -> Prop). diff --git a/bedrock2/src/bedrock2/FE310CSemantics.v b/bedrock2/src/bedrock2/FE310CSemantics.v index de4b7f84..6f260525 100644 --- a/bedrock2/src/bedrock2/FE310CSemantics.v +++ b/bedrock2/src/bedrock2/FE310CSemantics.v @@ -1,4 +1,4 @@ -Require Import Coq.ZArith.ZArith. +From Coq Require Import ZArith. Require Import bedrock2.Syntax bedrock2.Semantics. Require coqutil.Datatypes.String coqutil.Map.SortedList coqutil.Map.SortedListString. Require Import coqutil.Word.Interface. diff --git a/bedrock2/src/bedrock2/FrameRule.v b/bedrock2/src/bedrock2/FrameRule.v index 7ca6b059..6117d133 100644 --- a/bedrock2/src/bedrock2/FrameRule.v +++ b/bedrock2/src/bedrock2/FrameRule.v @@ -1,4 +1,4 @@ -Require Import Coq.ZArith.ZArith. +From Coq Require Import ZArith. Require Import coqutil.sanity coqutil.Macros.subst coqutil.Macros.unique coqutil.Byte. Require Import coqutil.Datatypes.PrimitivePair coqutil.Datatypes.HList. Require Import coqutil.Decidable. @@ -11,7 +11,7 @@ Require Import bedrock2.Memory bedrock2.ptsto_bytes bedrock2.Map.Separation. Require Import bedrock2.Semantics bedrock2.MetricSemantics. Require Import bedrock2.Map.DisjointUnion bedrock2.Map.split_alt. -Require Import Coq.Lists.List. +From Coq Require Import List. Section semantics. Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word byte}. diff --git a/bedrock2/src/bedrock2/HeapletwiseAutoSplitMerge.v b/bedrock2/src/bedrock2/HeapletwiseAutoSplitMerge.v index 49623867..c6a3dec6 100644 --- a/bedrock2/src/bedrock2/HeapletwiseAutoSplitMerge.v +++ b/bedrock2/src/bedrock2/HeapletwiseAutoSplitMerge.v @@ -1,6 +1,6 @@ -Require Import Coq.ZArith.ZArith. -Require Import Coq.Init.Byte. -Require Import Coq.micromega.Lia. +From Coq Require Import ZArith. +From Coq.Init Require Import Byte. +From Coq Require Import Lia. Require Import coqutil.Word.Bitwidth coqutil.Word.Properties. Require Import coqutil.Map.Interface coqutil.Map.Properties. Require Import coqutil.Datatypes.ZList. diff --git a/bedrock2/src/bedrock2/HeapletwiseHyps.v b/bedrock2/src/bedrock2/HeapletwiseHyps.v index 0b66a4c0..83454a33 100644 --- a/bedrock2/src/bedrock2/HeapletwiseHyps.v +++ b/bedrock2/src/bedrock2/HeapletwiseHyps.v @@ -1,5 +1,5 @@ -Require Import Coq.Logic.PropExtensionality Coq.Logic.FunctionalExtensionality. -Require Import Coq.Lists.List. Import ListNotations. Open Scope list_scope. +From Coq Require Import PropExtensionality FunctionalExtensionality. +From Coq Require Import List. Import ListNotations. Open Scope list_scope. Require Import coqutil.Map.Interface coqutil.Map.Properties. Require Import coqutil.Tactics.fwd. Require Import coqutil.Tactics.Tactics. diff --git a/bedrock2/src/bedrock2/Lift1Prop.v b/bedrock2/src/bedrock2/Lift1Prop.v index 1b5481f6..2621b50b 100644 --- a/bedrock2/src/bedrock2/Lift1Prop.v +++ b/bedrock2/src/bedrock2/Lift1Prop.v @@ -1,4 +1,4 @@ -Require Import Coq.Classes.Morphisms. +From Coq Require Import Morphisms. Section Binary. Context {T: Type} (P Q: T -> Prop). diff --git a/bedrock2/src/bedrock2/ListIndexNotations.v b/bedrock2/src/bedrock2/ListIndexNotations.v index 75ef7720..f1388af5 100644 --- a/bedrock2/src/bedrock2/ListIndexNotations.v +++ b/bedrock2/src/bedrock2/ListIndexNotations.v @@ -1,5 +1,5 @@ -Require Import Coq.Lists.List. -Require Import Coq.micromega.Lia. +From Coq Require Import List. +From Coq Require Import Lia. Require Import coqutil.Tactics.fwd. Require Import coqutil.Datatypes.List. Require Import coqutil.Datatypes.Inhabited. diff --git a/bedrock2/src/bedrock2/Loops.v b/bedrock2/src/bedrock2/Loops.v index e2bc84e9..1ec449ec 100644 --- a/bedrock2/src/bedrock2/Loops.v +++ b/bedrock2/src/bedrock2/Loops.v @@ -1,5 +1,5 @@ Require Import coqutil.Datatypes.PrimitivePair coqutil.Datatypes.HList coqutil.dlet. -Require Import Coq.Classes.Morphisms BinIntDef. +From Coq Require Import Morphisms BinIntDef. Require Import coqutil.Macros.unique coqutil.Map.Interface coqutil.Word.Interface. Import map. Require Import coqutil.Word.Bitwidth. Require Import coqutil.Map.Properties. diff --git a/bedrock2/src/bedrock2/Map/DisjointUnion.v b/bedrock2/src/bedrock2/Map/DisjointUnion.v index 6daa11ff..a539f8af 100644 --- a/bedrock2/src/bedrock2/Map/DisjointUnion.v +++ b/bedrock2/src/bedrock2/Map/DisjointUnion.v @@ -103,8 +103,8 @@ P1 = fun m => all keys in m are < 3 P2 = fun m => all keys in m are < 4 proving any (R * P1) m is as easy as giving all of m to R and giving map.empty to P1 *) -Require Import Coq.Lists.List. Import ListNotations. -Require Import Coq.ZArith.ZArith. +From Coq Require Import List. Import ListNotations. +From Coq Require Import ZArith. Require Import coqutil.Decidable. Require Import coqutil.Map.Interface coqutil.Map.Properties. Require Import coqutil.Tactics.Tactics. diff --git a/bedrock2/src/bedrock2/Map/SeparationLogic.v b/bedrock2/src/bedrock2/Map/SeparationLogic.v index 16b863d3..d1fca76c 100644 --- a/bedrock2/src/bedrock2/Map/SeparationLogic.v +++ b/bedrock2/src/bedrock2/Map/SeparationLogic.v @@ -1,6 +1,6 @@ Require Export bedrock2.Map.Separation. -Require Import Coq.Classes.Morphisms. +From Coq Require Import Morphisms. Require Import bedrock2.Lift1Prop. Require Coq.Lists.List. Require Import coqutil.sanity coqutil.Decidable coqutil.Tactics.destr. @@ -750,8 +750,8 @@ Ltac seprewrite_by Hrw tac := (* a convenient way to turn iff1 into eq, so that it can be used with our own equality-based (rather than Morphism-based) rewriters. *) -Require Import Coq.Logic.PropExtensionality. -Require Import Coq.Logic.FunctionalExtensionality. +From Coq Require Import PropExtensionality. +From Coq Require Import FunctionalExtensionality. Lemma iff1ToEq{T: Type}{P Q: T -> Prop}(H: iff1 P Q): P = Q. Proof. unfold iff1 in *. extensionality x. diff --git a/bedrock2/src/bedrock2/Memory.v b/bedrock2/src/bedrock2/Memory.v index 09a76bf4..0a23bbfa 100644 --- a/bedrock2/src/bedrock2/Memory.v +++ b/bedrock2/src/bedrock2/Memory.v @@ -1,6 +1,6 @@ -Require Import Coq.ZArith.ZArith. +From Coq Require Import ZArith. Require Import coqutil.Z.Lia. -Require Coq.Lists.List. +From Coq Require List. Require Import coqutil.sanity. Require Import coqutil.Decidable. Require Import coqutil.Datatypes.PrimitivePair coqutil.Datatypes.HList coqutil.Datatypes.List. diff --git a/bedrock2/src/bedrock2/MetricLogging.v b/bedrock2/src/bedrock2/MetricLogging.v index 451dacc7..7efcc560 100644 --- a/bedrock2/src/bedrock2/MetricLogging.v +++ b/bedrock2/src/bedrock2/MetricLogging.v @@ -1,4 +1,4 @@ -Require Import Coq.ZArith.BinInt. +From Coq Require Import BinInt. Require Import coqutil.Z.Lia. Section Riscv. diff --git a/bedrock2/src/bedrock2/MetricSemantics.v b/bedrock2/src/bedrock2/MetricSemantics.v index 41936c90..cbee7915 100644 --- a/bedrock2/src/bedrock2/MetricSemantics.v +++ b/bedrock2/src/bedrock2/MetricSemantics.v @@ -5,10 +5,10 @@ Require coqutil.Map.SortedListString. Require Import bedrock2.Syntax coqutil.Map.Interface coqutil.Map.OfListWord. Require Import BinIntDef coqutil.Word.Interface coqutil.Word.Bitwidth. Require Export bedrock2.Memory. -Require Import Coq.Lists.List. +From Coq Require Import List. Require Import bedrock2.MetricLogging. Require Import bedrock2.Semantics. -Require Import Coq.Lists.List. +From Coq Require Import List. Section semantics. Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word byte}. diff --git a/bedrock2/src/bedrock2/NetworkPackets.v b/bedrock2/src/bedrock2/NetworkPackets.v index b1c63e4c..80e31629 100644 --- a/bedrock2/src/bedrock2/NetworkPackets.v +++ b/bedrock2/src/bedrock2/NetworkPackets.v @@ -1,5 +1,5 @@ -Require Import Coq.ZArith.ZArith. Local Open Scope Z_scope. -Require Import Coq.Lists.List. Import ListNotations. +From Coq Require Import ZArith. Local Open Scope Z_scope. +From Coq Require Import List. Import ListNotations. Record ethernet_header_t := { src_mac: list Z; (* 6 *) diff --git a/bedrock2/src/bedrock2/NotationsCustomEntry.v b/bedrock2/src/bedrock2/NotationsCustomEntry.v index 722c2ef4..cef9ce65 100644 --- a/bedrock2/src/bedrock2/NotationsCustomEntry.v +++ b/bedrock2/src/bedrock2/NotationsCustomEntry.v @@ -1,8 +1,8 @@ -Require Import Coq.ZArith.BinIntDef Coq.Strings.String. +From Coq Require Import BinIntDef String. Require Import coqutil.Macros.subst coqutil.Macros.unique bedrock2.Syntax. Require Import coqutil.Macros.ident_to_string. -Export Coq.Strings.String.StringSyntax. +Export String.StringSyntax. Export bedrock2.Syntax.Coercions. Number Notation BinInt.Z BinInt.Z.of_num_int BinInt.Z.to_num_int : Z_scope. diff --git a/bedrock2/src/bedrock2/OperatorOverloading.v b/bedrock2/src/bedrock2/OperatorOverloading.v index fe507eb1..47d8f03c 100644 --- a/bedrock2/src/bedrock2/OperatorOverloading.v +++ b/bedrock2/src/bedrock2/OperatorOverloading.v @@ -1,4 +1,4 @@ -Require Import Coq.ZArith.ZArith. +From Coq Require Import ZArith. Require Import coqutil.Map.Interface. Require Import coqutil.Word.Interface. Require Import bedrock2.Map.SeparationLogic. diff --git a/bedrock2/src/bedrock2/PrintListByte.v b/bedrock2/src/bedrock2/PrintListByte.v index db353d26..12eee52e 100644 --- a/bedrock2/src/bedrock2/PrintListByte.v +++ b/bedrock2/src/bedrock2/PrintListByte.v @@ -7,7 +7,7 @@ Ltac print_list_byte := ltac2:(bs |- print_list_byte (Option.get (Ltac1.to_const Ltac2 Notation "print_bytes" bs(constr) := print_list_byte bs. Tactic Notation "print_bytes" constr(bs) := print_list_byte bs. -Require Import Coq.Lists.List. +From Coq Require Import List. Definition allBytes: list Byte.byte := map (fun nn => match Byte.of_N (BinNat.N.of_nat nn) with | Some b => b diff --git a/bedrock2/src/bedrock2/ProgramLogic.v b/bedrock2/src/bedrock2/ProgramLogic.v index 20714412..fc005096 100644 --- a/bedrock2/src/bedrock2/ProgramLogic.v +++ b/bedrock2/src/bedrock2/ProgramLogic.v @@ -340,7 +340,7 @@ Ltac straightline := | |- False \/ _ => right | |- _ \/ False => left | |- BinInt.Z.modulo ?z (Memory.bytes_per_word _) = BinInt.Z0 /\ _ => - lazymatch Coq.setoid_ring.InitialRing.isZcst z with + lazymatch InitialRing.isZcst z with | true => split; [exact eq_refl|] end | |- _ => straightline_stackalloc @@ -386,7 +386,7 @@ Ltac show_program := Ltac subst_words := repeat match goal with x := _ : coqutil.Word.Interface.word.rep |- _ => subst x end. -Require Import coqutil.Tactics.eplace Coq.setoid_ring.Ring_tac. +Require Import coqutil.Tactics.eplace Ring_tac. Ltac ring_simplify_words := subst_words; repeat match goal with H : context [?w] |- _ => diff --git a/bedrock2/src/bedrock2/PurifyHeapletwise.v b/bedrock2/src/bedrock2/PurifyHeapletwise.v index 7e4643ba..7a2b8563 100644 --- a/bedrock2/src/bedrock2/PurifyHeapletwise.v +++ b/bedrock2/src/bedrock2/PurifyHeapletwise.v @@ -1,5 +1,5 @@ Require Import Ltac2.Ltac2. -Require Import Coq.micromega.Lia. +From Coq Require Import Lia. Require Import coqutil.Map.Interface. Require Import coqutil.Word.Interface. Require Import coqutil.Tactics.fold_hyps coqutil.Tactics.foreach_hyp. diff --git a/bedrock2/src/bedrock2/PurifySep.v b/bedrock2/src/bedrock2/PurifySep.v index 58cad172..32218d02 100644 --- a/bedrock2/src/bedrock2/PurifySep.v +++ b/bedrock2/src/bedrock2/PurifySep.v @@ -1,4 +1,4 @@ -Require Import Coq.Logic.PropExtensionality Coq.Logic.FunctionalExtensionality. +From Coq Require Import PropExtensionality FunctionalExtensionality. Require Import coqutil.Map.Interface coqutil.Map.Properties. Require Import coqutil.Tactics.fwd. Require Import bedrock2.Lift1Prop. diff --git a/bedrock2/src/bedrock2/RecordPredicates.v b/bedrock2/src/bedrock2/RecordPredicates.v index 44d7522a..2f2b1a66 100644 --- a/bedrock2/src/bedrock2/RecordPredicates.v +++ b/bedrock2/src/bedrock2/RecordPredicates.v @@ -1,4 +1,4 @@ -Require Import Coq.ZArith.ZArith. +From Coq Require Import ZArith. Require Import coqutil.Word.Interface coqutil.Word.Bitwidth. Require Import coqutil.Map.Interface. Require Import coqutil.Tactics.ltac_list_ops. diff --git a/bedrock2/src/bedrock2/Refinement.v b/bedrock2/src/bedrock2/Refinement.v index 236866e3..d924ce81 100644 --- a/bedrock2/src/bedrock2/Refinement.v +++ b/bedrock2/src/bedrock2/Refinement.v @@ -1,7 +1,7 @@ (* These lemmas can be useful when proving a refinement and induction over the statement rather than over its exec derivation is preferred *) -Require Import Coq.ZArith.ZArith. +From Coq Require Import ZArith. Require Import coqutil.Word.Bitwidth. Require Import coqutil.Map.Interface. Require Import bedrock2.Syntax bedrock2.Semantics. diff --git a/bedrock2/src/bedrock2/Scalars.v b/bedrock2/src/bedrock2/Scalars.v index 8442f9bb..01caa9f4 100644 --- a/bedrock2/src/bedrock2/Scalars.v +++ b/bedrock2/src/bedrock2/Scalars.v @@ -1,12 +1,12 @@ Require Import coqutil.Map.Interface bedrock2.Map.Separation bedrock2.Map.SeparationLogic bedrock2.Lift1Prop bedrock2.Array coqutil.Word.LittleEndianList. Require Import bedrock2.Memory. -Require Import Coq.Lists.List Coq.ZArith.ZArith. +From Coq Require Import List ZArith. Require Import coqutil.Word.Interface coqutil.Map.Interface. (* coercions word and rep *) Require Import coqutil.Word.Properties. Require Import coqutil.Word.Bitwidth. Require Import coqutil.Z.div_mod_to_equations. Require Import coqutil.Z.bitblast. -Require Import coqutil.Z.Lia Coq.micromega.Lia. +Require Import coqutil.Z.Lia Lia. Require Import coqutil.Byte. Require Import coqutil.Map.OfListWord. Require Import coqutil.Macros.symmetry. diff --git a/bedrock2/src/bedrock2/Semantics.v b/bedrock2/src/bedrock2/Semantics.v index 0fe39044..e4b1fe6c 100644 --- a/bedrock2/src/bedrock2/Semantics.v +++ b/bedrock2/src/bedrock2/Semantics.v @@ -5,7 +5,7 @@ Require coqutil.Map.SortedListString. Require Import bedrock2.Syntax coqutil.Map.Interface coqutil.Map.OfListWord. Require Import BinIntDef coqutil.Word.Interface coqutil.Word.Bitwidth. Require Export bedrock2.Memory. -Require Import Coq.Lists.List. +From Coq Require Import List. (* BW is not needed on the rhs, but helps infer width *) Definition LogItem{width: Z}{BW: Bitwidth width}{word: word.word width}{mem: map.map word byte} := diff --git a/bedrock2/src/bedrock2/SepAuto.v b/bedrock2/src/bedrock2/SepAuto.v index 886a9689..860fdb6b 100644 --- a/bedrock2/src/bedrock2/SepAuto.v +++ b/bedrock2/src/bedrock2/SepAuto.v @@ -6,7 +6,7 @@ undo the `Ltac fwd_rewrites ::= fwd_rewrite_db_in_star.` patching, so `fwd` and tactics using `fwd` will do fewer simplifications than intended *) -Require Import Coq.ZArith.ZArith. Open Scope Z_scope. (* TODO remove *) +From Coq Require Import ZArith. Open Scope Z_scope. (* TODO remove *) Require Import coqutil.Byte. Require Import coqutil.Datatypes.Inhabited. Require Import coqutil.Tactics.Tactics. diff --git a/bedrock2/src/bedrock2/SepAutoArray.v b/bedrock2/src/bedrock2/SepAutoArray.v index 8931b94d..3e298133 100644 --- a/bedrock2/src/bedrock2/SepAutoArray.v +++ b/bedrock2/src/bedrock2/SepAutoArray.v @@ -1,5 +1,5 @@ -Require Import Coq.ZArith.BinInt. -Require Import Coq.Init.Byte. +From Coq Require Import BinInt. +From Coq.Init Require Import Byte. Require Import coqutil.Word.Bitwidth. Require Import coqutil.Tactics.rewr. Require Import coqutil.Map.Interface. diff --git a/bedrock2/src/bedrock2/SepAutoExports.v b/bedrock2/src/bedrock2/SepAutoExports.v index da95b5fd..0b68060f 100644 --- a/bedrock2/src/bedrock2/SepAutoExports.v +++ b/bedrock2/src/bedrock2/SepAutoExports.v @@ -1,4 +1,4 @@ -Require Export Coq.ZArith.ZArith. +From Coq Require Export ZArith. Require Export coqutil.Byte. Require Export coqutil.Datatypes.Inhabited. Require Export coqutil.Tactics.Tactics. diff --git a/bedrock2/src/bedrock2/SepCalls.v b/bedrock2/src/bedrock2/SepCalls.v index 7cf10386..7c6c9010 100644 --- a/bedrock2/src/bedrock2/SepCalls.v +++ b/bedrock2/src/bedrock2/SepCalls.v @@ -7,14 +7,14 @@ Applying the call lemma is not handled by this file, but solving the above conjunction (except for solving finalPost) is. *) -Require Import Coq.ZArith.ZArith. Open Scope Z_scope. +From Coq Require Import ZArith. Open Scope Z_scope. Require Import coqutil.Z.Lia. Require Import coqutil.Byte. Require Import coqutil.Datatypes.HList. Require Import coqutil.Datatypes.PropSet. Require Import coqutil.Datatypes.Inhabited. Require Import coqutil.Tactics.rewr coqutil.Tactics.rdelta. -Require Import Coq.Program.Tactics. +From Coq.Program Require Import Tactics. Require Import coqutil.Macros.symmetry. Require Import coqutil.Tactics.Tactics. Require Import coqutil.Tactics.autoforward. @@ -31,8 +31,8 @@ Require Import bedrock2.ptsto_bytes bedrock2.Scalars. Require Import bedrock2.groundcbv. Require Import bedrock2.TacticError. Require Import bedrock2.ident_to_string. -Require Import Coq.Strings.String. Open Scope string_scope. -Require Import Coq.Lists.List. (* to make sure `length` refers to list rather than string *) +From Coq Require Import String. Open Scope string_scope. +From Coq Require Import List. (* to make sure `length` refers to list rather than string *) Import List.ListNotations. Open Scope list_scope. Section SepLog. diff --git a/bedrock2/src/bedrock2/SepCallsExports.v b/bedrock2/src/bedrock2/SepCallsExports.v index 9394ed86..b004807d 100644 --- a/bedrock2/src/bedrock2/SepCallsExports.v +++ b/bedrock2/src/bedrock2/SepCallsExports.v @@ -1,4 +1,4 @@ -Require Export Coq.ZArith.ZArith. Open Scope Z_scope. +From Coq Require Export ZArith. Open Scope Z_scope. Require Export coqutil.Byte. Require Export coqutil.Datatypes.Inhabited. Require Export coqutil.Tactics.Tactics. @@ -10,7 +10,7 @@ Require Export bedrock2.Lift1Prop. Require Export bedrock2.Map.Separation bedrock2.Map.SeparationLogic. Require Export bedrock2.ZnWords. Require Export bedrock2.TacticError. -Require Export Coq.Strings.String. Open Scope string_scope. -Require Export Coq.Lists.List. (* to make sure `length` refers to list rather than string *) +From Coq Require Export String. Open Scope string_scope. +From Coq Require Export List. (* to make sure `length` refers to list rather than string *) Require Export bedrock2.SepCalls. diff --git a/bedrock2/src/bedrock2/SepClause.v b/bedrock2/src/bedrock2/SepClause.v index a767597b..121ea85c 100644 --- a/bedrock2/src/bedrock2/SepClause.v +++ b/bedrock2/src/bedrock2/SepClause.v @@ -1,4 +1,4 @@ -Require Export Coq.ZArith.ZArith. +From Coq Require Export ZArith. Require Export coqutil.Byte. Require Export coqutil.Map.Interface coqutil.Map.Properties coqutil.Map.OfListWord. Require Export coqutil.Word.Interface coqutil.Word.Properties. diff --git a/bedrock2/src/bedrock2/SepLib.v b/bedrock2/src/bedrock2/SepLib.v index d25a940d..1cc1dc0f 100644 --- a/bedrock2/src/bedrock2/SepLib.v +++ b/bedrock2/src/bedrock2/SepLib.v @@ -1,5 +1,5 @@ -Require Import Coq.ZArith.ZArith. Local Open Scope Z_scope. -Require Import Coq.micromega.Lia. +From Coq Require Import ZArith. Local Open Scope Z_scope. +From Coq Require Import Lia. Require Import coqutil.Word.Interface coqutil.Word.Properties coqutil.Word.Bitwidth. Require Import coqutil.Map.Interface. Require Import coqutil.Datatypes.ZList. Import ZList.List.ZIndexNotations. diff --git a/bedrock2/src/bedrock2/SepLogAddrArith.v b/bedrock2/src/bedrock2/SepLogAddrArith.v index f0a13629..ff8cc5e7 100644 --- a/bedrock2/src/bedrock2/SepLogAddrArith.v +++ b/bedrock2/src/bedrock2/SepLogAddrArith.v @@ -1,5 +1,5 @@ -Require Export Coq.Lists.List. Export ListNotations. -Require Export Coq.ZArith.ZArith. Open Scope Z_scope. +From Coq Require Export List. Export ListNotations. +From Coq Require Export ZArith. Open Scope Z_scope. Require Export coqutil.Word.Interface coqutil.Word.Properties. Require Export coqutil.Map.Interface coqutil.Map.Properties. Require Import coqutil.Tactics.rdelta coqutil.Tactics.destr coqutil.Decidable. diff --git a/bedrock2/src/bedrock2/SepappBulletPoints.v b/bedrock2/src/bedrock2/SepappBulletPoints.v index 7da7ebbd..74cdfbff 100644 --- a/bedrock2/src/bedrock2/SepappBulletPoints.v +++ b/bedrock2/src/bedrock2/SepappBulletPoints.v @@ -1,6 +1,6 @@ (* Notations to display a list of sepapp predicates as a bullet point list *) -Require Import Coq.ZArith.ZArith. +From Coq Require Import ZArith. Require Import coqutil.Map.Interface coqutil.Word.Interface. Require Import bedrock2.Lift1Prop. Require Import bedrock2.Map.Separation bedrock2.Map.SeparationLogic. diff --git a/bedrock2/src/bedrock2/Syntax.v b/bedrock2/src/bedrock2/Syntax.v index a480eaf3..0f40af32 100644 --- a/bedrock2/src/bedrock2/Syntax.v +++ b/bedrock2/src/bedrock2/Syntax.v @@ -1,6 +1,6 @@ Require Import coqutil.sanity coqutil.Macros.subst coqutil.Macros.unique. -Require Coq.Strings.String. -Require Import Coq.Numbers.BinNums. +From Coq Require String. +From Coq Require Import BinNums. Module Import bopname. Inductive bopname: Set := add | sub | mul | mulhuu | divu | remu | and | or | xor | sru | slu | srs | lts | ltu | eq. diff --git a/bedrock2/src/bedrock2/TacticError.v b/bedrock2/src/bedrock2/TacticError.v index 540b3101..92a5ad63 100644 --- a/bedrock2/src/bedrock2/TacticError.v +++ b/bedrock2/src/bedrock2/TacticError.v @@ -1,4 +1,4 @@ -Require Import Coq.Strings.String. +From Coq Require Import String. (* Almost everyone importing this file will need strings in their error messages *) Export Coq.Strings.String.StringSyntax. Require Import coqutil.Datatypes.dlist. diff --git a/bedrock2/src/bedrock2/ToCString.v b/bedrock2/src/bedrock2/ToCString.v index eb76b99e..39e71c30 100644 --- a/bedrock2/src/bedrock2/ToCString.v +++ b/bedrock2/src/bedrock2/ToCString.v @@ -1,7 +1,7 @@ Require Import bedrock2.Syntax bedrock2.Variables. Import bopname. Require Import coqutil.Datatypes.ListSet. -Require Import Coq.ZArith.BinIntDef Coq.Numbers.BinNums Coq.Numbers.DecimalString. -Require Import Coq.Strings.String. Local Open Scope string_scope. +From Coq Require Import BinIntDef BinNums DecimalString. +From Coq Require Import String. Local Open Scope string_scope. Definition prelude := "#include #include diff --git a/bedrock2/src/bedrock2/ToCStringExprTypecheckingTest.v b/bedrock2/src/bedrock2/ToCStringExprTypecheckingTest.v index bb2612a7..63eda455 100644 --- a/bedrock2/src/bedrock2/ToCStringExprTypecheckingTest.v +++ b/bedrock2/src/bedrock2/ToCStringExprTypecheckingTest.v @@ -1,5 +1,5 @@ Require Import Ltac2.Ltac2. -Require Import Coq.ZArith.BinInt Coq.Strings.String. +From Coq Require Import BinInt String. Require Import bedrock2.Syntax bedrock2.ToCString. Import Syntax.Coercions. Local Open Scope Z_scope. Local Open Scope string_scope. diff --git a/bedrock2/src/bedrock2/TraceInspection.v b/bedrock2/src/bedrock2/TraceInspection.v index fec780bc..fa7a192a 100644 --- a/bedrock2/src/bedrock2/TraceInspection.v +++ b/bedrock2/src/bedrock2/TraceInspection.v @@ -1,5 +1,5 @@ -Require Import Coq.Strings.String. -Require Import Coq.ZArith.ZArith. +From Coq Require Import String. +From Coq Require Import ZArith. Require Import coqutil.Tactics.Tactics. Require Import coqutil.Tactics.fwd. Require Import coqutil.Map.Interface coqutil.Map.Properties. diff --git a/bedrock2/src/bedrock2/TracePredicate.v b/bedrock2/src/bedrock2/TracePredicate.v index f81d5ffe..0577df1c 100644 --- a/bedrock2/src/bedrock2/TracePredicate.v +++ b/bedrock2/src/bedrock2/TracePredicate.v @@ -1,4 +1,4 @@ -Require Import Coq.Lists.List. Import ListNotations. +From Coq Require Import List. Import ListNotations. Require Import bedrock2.ReversedListNotations. Section ListPred. diff --git a/bedrock2/src/bedrock2/TransferSepsOrder.v b/bedrock2/src/bedrock2/TransferSepsOrder.v index 5d2c10d2..708d463f 100644 --- a/bedrock2/src/bedrock2/TransferSepsOrder.v +++ b/bedrock2/src/bedrock2/TransferSepsOrder.v @@ -1,13 +1,13 @@ (* Applying the order of sep clauses from an old hypothesis onto a new hypothesis: *) -Require Export Coq.ZArith.ZArith. Open Scope Z_scope. +From Coq Require Export ZArith. Open Scope Z_scope. Require Import coqutil.Z.Lia. Require Export coqutil.Byte. Require Import coqutil.Datatypes.HList. Require Import coqutil.Datatypes.PropSet. Require Export coqutil.Datatypes.Inhabited. Require Import coqutil.Tactics.rewr coqutil.Tactics.rdelta. -Require Import Coq.Program.Tactics. +From Coq.Program Require Import Tactics. Require Export coqutil.Tactics.Tactics. Require Export coqutil.Tactics.autoforward. Require Export coqutil.Map.Interface coqutil.Map.Properties coqutil.Map.OfListWord. diff --git a/bedrock2/src/bedrock2/Variables.v b/bedrock2/src/bedrock2/Variables.v index 0ef6695e..f76a1f0d 100644 --- a/bedrock2/src/bedrock2/Variables.v +++ b/bedrock2/src/bedrock2/Variables.v @@ -1,6 +1,6 @@ Require Import coqutil.Macros.subst coqutil.Macros.unique bedrock2.Syntax. -Require Import Coq.Lists.List. +From Coq Require Import List. Module expr. Import Syntax.expr. Fixpoint vars (e : expr) : list String.string := diff --git a/bedrock2/src/bedrock2/WeakestPrecondition.v b/bedrock2/src/bedrock2/WeakestPrecondition.v index af40307c..62e27e6a 100644 --- a/bedrock2/src/bedrock2/WeakestPrecondition.v +++ b/bedrock2/src/bedrock2/WeakestPrecondition.v @@ -1,5 +1,6 @@ Require Import coqutil.Macros.subst coqutil.Macros.unique coqutil.Map.Interface coqutil.Map.OfListWord. -Require Import Coq.ZArith.BinIntDef coqutil.Word.Interface coqutil.Word.Bitwidth. +From Coq Require Import BinIntDef. +Require Import coqutil.Word.Interface coqutil.Word.Bitwidth. Require Import coqutil.dlet bedrock2.Syntax bedrock2.Semantics. Section WeakestPrecondition. @@ -154,7 +155,7 @@ Ltac unfold1_list_map_goal := let G := unfold1_list_map G in change G. -Import Coq.ZArith.ZArith. +Import ZArith. Notation "'fnspec!' name a0 .. an '/' g0 .. gn '~>' r0 .. rn ',' '{' 'requires' tr mem := pre ';' 'ensures' tr' mem' ':=' post '}'" := (fun functions => diff --git a/bedrock2/src/bedrock2/WeakestPreconditionProperties.v b/bedrock2/src/bedrock2/WeakestPreconditionProperties.v index 166f868c..fe8544bc 100644 --- a/bedrock2/src/bedrock2/WeakestPreconditionProperties.v +++ b/bedrock2/src/bedrock2/WeakestPreconditionProperties.v @@ -2,7 +2,7 @@ Require Import coqutil.Macros.subst coqutil.Macros.unique coqutil.Map.Interface Require Import coqutil.Word.Bitwidth. Require bedrock2.WeakestPrecondition. -Require Import Coq.Classes.Morphisms. +From Coq Require Import Morphisms. Section WeakestPrecondition. Context {width} {BW: Bitwidth width} {word: word.word width} {mem: map.map word Byte.byte}. diff --git a/bedrock2/src/bedrock2/WordPushDownLemmas.v b/bedrock2/src/bedrock2/WordPushDownLemmas.v index 575b2937..13209c17 100644 --- a/bedrock2/src/bedrock2/WordPushDownLemmas.v +++ b/bedrock2/src/bedrock2/WordPushDownLemmas.v @@ -1,5 +1,5 @@ -Require Import Coq.ZArith.ZArith. Local Open Scope Z_scope. -Require Import Coq.micromega.Lia. +From Coq Require Import ZArith. Local Open Scope Z_scope. +From Coq Require Import Lia. Require Import coqutil.Word.Interface coqutil.Word.Properties. Module word. diff --git a/bedrock2/src/bedrock2/ZListEqProver.v b/bedrock2/src/bedrock2/ZListEqProver.v index 95f942d6..f8272b72 100644 --- a/bedrock2/src/bedrock2/ZListEqProver.v +++ b/bedrock2/src/bedrock2/ZListEqProver.v @@ -1,6 +1,7 @@ -Require Import Coq.ZArith.ZArith. Local Open Scope Z_scope. -Require Import Coq.micromega.Lia coqutil.Ltac2Lib.Lia. -Require Import Coq.Lists.List. +From Coq Require Import ZArith. Local Open Scope Z_scope. +From Coq Require Import Lia. +Require Import coqutil.Ltac2Lib.Lia. +From Coq Require Import List. Require Import coqutil.Datatypes.ZList. Require Import coqutil.Datatypes.Inhabited. Import ZList.List.ZIndexNotations. Local Open Scope zlist_scope. diff --git a/bedrock2/src/bedrock2/ZWordMem.v b/bedrock2/src/bedrock2/ZWordMem.v index 7028b1b6..64958b10 100644 --- a/bedrock2/src/bedrock2/ZWordMem.v +++ b/bedrock2/src/bedrock2/ZWordMem.v @@ -1,6 +1,6 @@ -Require Import Coq.ZArith.ZArith. Local Open Scope Z_scope. -Require Import Coq.micromega.Lia. -Require Import Coq.Logic.FunctionalExtensionality. +From Coq Require Import ZArith. Local Open Scope Z_scope. +From Coq Require Import Lia. +From Coq Require Import FunctionalExtensionality. Require Import coqutil.Tactics.fwd coqutil.Tactics.Tactics. Require Import coqutil.Datatypes.ZList. Require Import coqutil.Map.Interface coqutil.Map.Properties. diff --git a/bedrock2/src/bedrock2/ZnWords.v b/bedrock2/src/bedrock2/ZnWords.v index 6a753c5a..457ee947 100644 --- a/bedrock2/src/bedrock2/ZnWords.v +++ b/bedrock2/src/bedrock2/ZnWords.v @@ -8,9 +8,9 @@ The `word` instance can be abstract (more tested) or concrete (less tested), but `width` has to be concrete, because otherwise the Euclidean equations become non-linear and thus are not understood by `lia`. *) -Require Import Coq.Program.Tactics. -Require Import Coq.ZArith.ZArith. -Require Import Coq.ZArith.Zpow_facts. +From Coq.Program Require Import Tactics. +From Coq Require Import ZArith. +From Coq Require Import Zpow_facts. Require Import coqutil.Tactics.rdelta coqutil.Tactics.rewr. Require Import coqutil.Z.Lia. Require Import coqutil.Word.Interface coqutil.Word.Properties. diff --git a/bedrock2/src/bedrock2/ZnWordsTests.v b/bedrock2/src/bedrock2/ZnWordsTests.v index dd1eaed8..12ad463c 100644 --- a/bedrock2/src/bedrock2/ZnWordsTests.v +++ b/bedrock2/src/bedrock2/ZnWordsTests.v @@ -1,7 +1,7 @@ -Require Import Coq.ZArith.ZArith. Local Open Scope Z_scope. +From Coq Require Import ZArith. Local Open Scope Z_scope. Require Import bedrock2.ZnWords. Require Import coqutil.Word.Interface. -Require Import Coq.Lists.List. Import ListNotations. +From Coq Require Import List. Import ListNotations. Require Import coqutil.Datatypes.Inhabited. Require Import bedrock2.WordNotations. Local Open Scope word_scope. diff --git a/bedrock2/src/bedrock2/bottom_up_simpl.v b/bedrock2/src/bedrock2/bottom_up_simpl.v index f8392324..8aabfa26 100644 --- a/bedrock2/src/bedrock2/bottom_up_simpl.v +++ b/bedrock2/src/bedrock2/bottom_up_simpl.v @@ -1,7 +1,7 @@ Require Import coqutil.Ltac2Lib.Ltac2. Require Import coqutil.Ltac2Lib.Failf coqutil.Ltac2Lib.rdelta coqutil.Ltac2Lib.Lia. -Require Import Coq.ZArith.ZArith. Local Open Scope Z_scope. -Require Import Coq.micromega.Lia. +From Coq Require Import ZArith. Local Open Scope Z_scope. +From Coq Require Import Lia. Require Import coqutil.Word.Interface coqutil.Word.Properties. Require Import coqutil.Datatypes.Inhabited. Require Import coqutil.Datatypes.ZList. diff --git a/bedrock2/src/bedrock2/bottom_up_simpl_ltac1.v b/bedrock2/src/bedrock2/bottom_up_simpl_ltac1.v index 3053fead..531e1fd0 100644 --- a/bedrock2/src/bedrock2/bottom_up_simpl_ltac1.v +++ b/bedrock2/src/bedrock2/bottom_up_simpl_ltac1.v @@ -1,5 +1,5 @@ -Require Import Coq.ZArith.ZArith. Local Open Scope Z_scope. -Require Import Coq.micromega.Lia. +From Coq Require Import ZArith. Local Open Scope Z_scope. +From Coq Require Import Lia. Require Import coqutil.Word.Interface coqutil.Word.Properties. Require Import coqutil.Datatypes.ZList. Require Import coqutil.Tactics.Tactics. diff --git a/bedrock2/src/bedrock2/bottom_up_simpl_perf.v b/bedrock2/src/bedrock2/bottom_up_simpl_perf.v index 30d39299..ab9f99d1 100644 --- a/bedrock2/src/bedrock2/bottom_up_simpl_perf.v +++ b/bedrock2/src/bedrock2/bottom_up_simpl_perf.v @@ -1,4 +1,4 @@ -Require Import Coq.ZArith.ZArith. Local Open Scope Z_scope. +From Coq Require Import ZArith. Local Open Scope Z_scope. Require Import Ltac2.Ltac2. Set Default Proof Mode "Classic". Require Import Ltac2.Printf. Require Import coqutil.Tactics.foreach_hyp. diff --git a/bedrock2/src/bedrock2/cancel_div.v b/bedrock2/src/bedrock2/cancel_div.v index ea20bb01..3b88d519 100644 --- a/bedrock2/src/bedrock2/cancel_div.v +++ b/bedrock2/src/bedrock2/cancel_div.v @@ -1,5 +1,5 @@ Require Import coqutil.Ltac2Lib.Ltac2 coqutil.Ltac2Lib.Ring. -Require Import Coq.ZArith.ZArith. Local Open Scope Z_scope. +From Coq Require Import ZArith. Local Open Scope Z_scope. (* For the division canceler, we use statements of the form (a = d * a') instead of (a / d = a'), because the former also states that the remainder of the division is 0. diff --git a/bedrock2/src/bedrock2/cancel_div_ltac1.v b/bedrock2/src/bedrock2/cancel_div_ltac1.v index dfdad979..263f1236 100644 --- a/bedrock2/src/bedrock2/cancel_div_ltac1.v +++ b/bedrock2/src/bedrock2/cancel_div_ltac1.v @@ -1,4 +1,4 @@ -Require Import Coq.ZArith.ZArith. Local Open Scope Z_scope. +From Coq Require Import ZArith. Local Open Scope Z_scope. (* For the division canceler, we use statements of the form (a = d * a') instead of (a / d = a'), because the former also states that the remainder of the division is 0. diff --git a/bedrock2/src/bedrock2/e1000_packet_trace.v b/bedrock2/src/bedrock2/e1000_packet_trace.v index fe936897..396a91d6 100644 --- a/bedrock2/src/bedrock2/e1000_packet_trace.v +++ b/bedrock2/src/bedrock2/e1000_packet_trace.v @@ -1,5 +1,5 @@ -Require Import Coq.ZArith.ZArith. -Require Import Coq.Strings.String. Local Open Scope string_scope. +From Coq Require Import ZArith. +From Coq Require Import String. Local Open Scope string_scope. Require Import coqutil.Word.Bitwidth. Require Import coqutil.Map.Interface. Require Import coqutil.Word.Interface. diff --git a/bedrock2/src/bedrock2/e1000_read_write_step.v b/bedrock2/src/bedrock2/e1000_read_write_step.v index b911a26d..dfd9a302 100644 --- a/bedrock2/src/bedrock2/e1000_read_write_step.v +++ b/bedrock2/src/bedrock2/e1000_read_write_step.v @@ -10,9 +10,9 @@ https://www.intel.com/content/dam/doc/manual/pci-pci-x-family-gbe-controllers-so These network cards were launched in the 2000s and discontinued in the 2010s, but continue to be a popular choice for virtualization, and are often referred to as "e1000". *) -Require Import Coq.Strings.String. -Require Import Coq.ZArith.ZArith. -Require Import Coq.micromega.Lia. +From Coq Require Import String. +From Coq Require Import ZArith. +From Coq Require Import Lia. Require Import coqutil.Tactics.fwd. Require Import coqutil.Map.Interface coqutil.Map.Properties. Require Import coqutil.Word.Interface coqutil.Word.Properties coqutil.Word.Bitwidth. diff --git a/bedrock2/src/bedrock2/e1000_state.v b/bedrock2/src/bedrock2/e1000_state.v index fd826134..70856a2f 100644 --- a/bedrock2/src/bedrock2/e1000_state.v +++ b/bedrock2/src/bedrock2/e1000_state.v @@ -10,8 +10,8 @@ https://www.intel.com/content/dam/doc/manual/pci-pci-x-family-gbe-controllers-so These network cards were launched in the 2000s and discontinued in the 2010s, but continue to be a popular choice for virtualization, and are often referred to as "e1000". *) -Require Import Coq.Strings.String. -Require Import Coq.ZArith.ZArith. +From Coq Require Import String. +From Coq Require Import ZArith. Require Import coqutil.Tactics.fwd. Require Import coqutil.Map.Interface coqutil.Map.Properties. Require Import coqutil.Word.Interface coqutil.Word.Bitwidth. diff --git a/bedrock2/src/bedrock2/ident_to_string.v b/bedrock2/src/bedrock2/ident_to_string.v index 8fe40e7a..90e7ddc5 100644 --- a/bedrock2/src/bedrock2/ident_to_string.v +++ b/bedrock2/src/bedrock2/ident_to_string.v @@ -1,4 +1,4 @@ -Require Import Coq.Strings.String. +From Coq Require Import String. Require Import Ltac2.Ltac2. (* Converts the lower i + 1 bits of an Ltac2 integer into a bool list diff --git a/bedrock2/src/bedrock2/memory_mapped_ext_spec.v b/bedrock2/src/bedrock2/memory_mapped_ext_spec.v index 7e6266c5..7138cf33 100644 --- a/bedrock2/src/bedrock2/memory_mapped_ext_spec.v +++ b/bedrock2/src/bedrock2/memory_mapped_ext_spec.v @@ -1,7 +1,7 @@ -Require Import Coq.Strings.String. Local Open Scope string_scope. -Require Import Coq.ZArith.ZArith. -Require Import Coq.micromega.Lia. -Require Import Coq.Lists.List. Import ListNotations. Local Open Scope list_scope. +From Coq Require Import String. Local Open Scope string_scope. +From Coq Require Import ZArith. +From Coq Require Import Lia. +From Coq Require Import List. Import ListNotations. Local Open Scope list_scope. Require Import coqutil.Datatypes.HList. Require coqutil.Word.LittleEndian. Require Import coqutil.Byte. diff --git a/bedrock2/src/bedrock2/old_dma/StateMachineBasedExtSpec.v b/bedrock2/src/bedrock2/old_dma/StateMachineBasedExtSpec.v index 3b9417de..f2fa0e5e 100644 --- a/bedrock2/src/bedrock2/old_dma/StateMachineBasedExtSpec.v +++ b/bedrock2/src/bedrock2/old_dma/StateMachineBasedExtSpec.v @@ -1,5 +1,5 @@ -Require Import Coq.Strings.String. -Require Import Coq.ZArith.ZArith. +From Coq Require Import String. +From Coq Require Import ZArith. Require Import coqutil.Map.Interface coqutil.Word.Interface coqutil.Word.Bitwidth. Require Import bedrock2.Semantics. diff --git a/bedrock2/src/bedrock2/old_dma/StateMachineBasedExtSpec_wp.v b/bedrock2/src/bedrock2/old_dma/StateMachineBasedExtSpec_wp.v index c050ae42..a0e53432 100644 --- a/bedrock2/src/bedrock2/old_dma/StateMachineBasedExtSpec_wp.v +++ b/bedrock2/src/bedrock2/old_dma/StateMachineBasedExtSpec_wp.v @@ -1,5 +1,5 @@ -Require Import Coq.Strings.String. -Require Import Coq.ZArith.ZArith. +From Coq Require Import String. +From Coq Require Import ZArith. Require Import coqutil.Map.Interface coqutil.Word.Interface coqutil.Word.Bitwidth. Require Import bedrock2.Semantics. diff --git a/bedrock2/src/bedrock2/old_dma/circular_buffer_slice_based_on_list_of_addrs.v b/bedrock2/src/bedrock2/old_dma/circular_buffer_slice_based_on_list_of_addrs.v index 0a2a2e93..04599c3c 100644 --- a/bedrock2/src/bedrock2/old_dma/circular_buffer_slice_based_on_list_of_addrs.v +++ b/bedrock2/src/bedrock2/old_dma/circular_buffer_slice_based_on_list_of_addrs.v @@ -1,5 +1,5 @@ -Require Import Coq.Strings.String. -Require Import Coq.ZArith.ZArith. +From Coq Require Import String. +From Coq Require Import ZArith. Require Import coqutil.Tactics.fwd. Require Import coqutil.Map.Interface coqutil.Map.Properties. Require Import coqutil.Word.Interface coqutil.Word.Bitwidth. diff --git a/bedrock2/src/bedrock2/old_dma/e1000.v b/bedrock2/src/bedrock2/old_dma/e1000.v index a922f179..760eacae 100644 --- a/bedrock2/src/bedrock2/old_dma/e1000.v +++ b/bedrock2/src/bedrock2/old_dma/e1000.v @@ -10,9 +10,9 @@ https://www.intel.com/content/dam/doc/manual/pci-pci-x-family-gbe-controllers-so These network cards were launched in the 2000s and discontinued in the 2010s, but continue to be a popular choice for virtualization, where they are often referred to as "e1000". *) -Require Import Coq.Strings.String. -Require Import Coq.ZArith.ZArith. -Require Import Coq.micromega.Lia. +From Coq Require Import String. +From Coq Require Import ZArith. +From Coq Require Import Lia. Require Import coqutil.Tactics.Tactics. Require Import coqutil.Tactics.fwd. Require Import coqutil.Map.Interface coqutil.Map.Properties. diff --git a/bedrock2/src/bedrock2/old_dma/e1000_stateless.v b/bedrock2/src/bedrock2/old_dma/e1000_stateless.v index 91982c94..3ba1cd40 100644 --- a/bedrock2/src/bedrock2/old_dma/e1000_stateless.v +++ b/bedrock2/src/bedrock2/old_dma/e1000_stateless.v @@ -10,8 +10,8 @@ https://www.intel.com/content/dam/doc/manual/pci-pci-x-family-gbe-controllers-so These network cards were launched in the 2000s and discontinued in the 2010s, but continue to be a popular choice for virtualization, where they are often referred to as "e1000". *) -Require Import Coq.Strings.String. -Require Import Coq.ZArith.ZArith. +From Coq Require Import String. +From Coq Require Import ZArith. Require Import coqutil.Tactics.fwd. Require Import coqutil.Map.Interface coqutil.Map.Properties. Require Import coqutil.Word.Interface coqutil.Word.Properties coqutil.Word.Bitwidth. diff --git a/bedrock2/src/bedrock2/old_dma/e1000_wp.v b/bedrock2/src/bedrock2/old_dma/e1000_wp.v index 13b42b9c..ac8eaf19 100644 --- a/bedrock2/src/bedrock2/old_dma/e1000_wp.v +++ b/bedrock2/src/bedrock2/old_dma/e1000_wp.v @@ -10,8 +10,8 @@ https://www.intel.com/content/dam/doc/manual/pci-pci-x-family-gbe-controllers-so These network cards were launched in the 2000s and discontinued in the 2010s, but continue to be a popular choice for virtualization, where they are often referred to as "e1000". *) -Require Import Coq.Strings.String. -Require Import Coq.ZArith.ZArith. +From Coq Require Import String. +From Coq Require Import ZArith. Require Import coqutil.Tactics.fwd. Require Import coqutil.Map.Interface coqutil.Map.Properties. Require Import coqutil.Word.Interface coqutil.Word.Bitwidth. diff --git a/bedrock2/src/bedrock2/old_dma/mmio_read_write_step_based_ext_spec.v b/bedrock2/src/bedrock2/old_dma/mmio_read_write_step_based_ext_spec.v index ab42fddc..2d33238a 100644 --- a/bedrock2/src/bedrock2/old_dma/mmio_read_write_step_based_ext_spec.v +++ b/bedrock2/src/bedrock2/old_dma/mmio_read_write_step_based_ext_spec.v @@ -1,6 +1,6 @@ -Require Import Coq.Strings.String. Local Open Scope string_scope. -Require Import Coq.ZArith.ZArith. -Require Import Coq.Lists.List. Import ListNotations. Local Open Scope list_scope. +From Coq Require Import String. Local Open Scope string_scope. +From Coq Require Import ZArith. +From Coq Require Import List. Import ListNotations. Local Open Scope list_scope. Require Import coqutil.Tactics.fwd. Require Import coqutil.Map.Interface coqutil.Word.Interface coqutil.Word.Bitwidth. Require Import bedrock2.Semantics. diff --git a/bedrock2/src/bedrock2/ptsto_bytes.v b/bedrock2/src/bedrock2/ptsto_bytes.v index 9d3f393e..59d2edc9 100644 --- a/bedrock2/src/bedrock2/ptsto_bytes.v +++ b/bedrock2/src/bedrock2/ptsto_bytes.v @@ -1,12 +1,12 @@ Require Import coqutil.Map.Interface coqutil.Map.Properties bedrock2.Map.Separation bedrock2.Map.SeparationLogic bedrock2.Lift1Prop bedrock2.Array. Require Import bedrock2.Memory. -Require Import Coq.Lists.List Coq.ZArith.ZArith. +From Coq Require Import List ZArith. Require Import coqutil.Word.Interface coqutil.Word.Properties coqutil.Map.Interface. Require Import coqutil.Z.div_mod_to_equations. Import HList List PrimitivePair. Require Import coqutil.Z.Lia. Require Import coqutil.Byte. -Require Import Coq.ZArith.ZArith. +From Coq Require Import ZArith. Open Scope Z_scope. diff --git a/bedrock2/src/bedrock2/safe_implication.v b/bedrock2/src/bedrock2/safe_implication.v index e0073b6a..91534c1d 100644 --- a/bedrock2/src/bedrock2/safe_implication.v +++ b/bedrock2/src/bedrock2/safe_implication.v @@ -59,7 +59,7 @@ Ltac safe_implication_step := end end. -Require Import Coq.Lists.List. +From Coq Require Import List. Lemma list_app_eq_r: forall [A: Type] (xs ys1 ys2: list A), safe_implication (ys1 = ys2) (xs ++ ys1 = xs ++ ys2). @@ -69,7 +69,7 @@ Lemma list_app_eq_l: forall [A: Type] (xs1 xs2 ys: list A), safe_implication (xs1 = xs2) (xs1 ++ ys = xs2 ++ ys). Proof. unfold safe_implication. intros. subst. reflexivity. Qed. -Require Import Coq.ZArith.ZArith. Local Open Scope Z_scope. +From Coq Require Import ZArith. Local Open Scope Z_scope. Require Import coqutil.Word.Bitwidth coqutil.Word.Interface coqutil.Map.Interface. Require Import bedrock2.Lift1Prop. Require Import bedrock2.SepLib. diff --git a/bedrock2/src/bedrock2/sepapp.v b/bedrock2/src/bedrock2/sepapp.v index 067fbbf7..6049d46d 100644 --- a/bedrock2/src/bedrock2/sepapp.v +++ b/bedrock2/src/bedrock2/sepapp.v @@ -1,6 +1,6 @@ (* The seppapp operator: separating append, useful for contiguous memory regions *) -Require Import Coq.ZArith.ZArith. Local Open Scope Z_scope. -Require Import Coq.Logic.FunctionalExtensionality. +From Coq Require Import ZArith. Local Open Scope Z_scope. +From Coq Require Import FunctionalExtensionality. Require Import coqutil.Tactics.Tactics coqutil.Tactics.fwd. Require Import coqutil.Byte. Require Import coqutil.Word.Interface coqutil.Word.Properties coqutil.Word.Bitwidth. diff --git a/bedrock2/src/bedrock2/syntactic_f_equal_with_ZnWords.v b/bedrock2/src/bedrock2/syntactic_f_equal_with_ZnWords.v index 9c28dfa9..c77dec53 100644 --- a/bedrock2/src/bedrock2/syntactic_f_equal_with_ZnWords.v +++ b/bedrock2/src/bedrock2/syntactic_f_equal_with_ZnWords.v @@ -1,4 +1,4 @@ -Require Import Coq.ZArith.ZArith. +From Coq Require Import ZArith. Require Import coqutil.Word.Interface. Require Import bedrock2.ZnWords. Require Import bedrock2.Lift1Prop. diff --git a/bedrock2/src/bedrock2/to_from_anybytes.v b/bedrock2/src/bedrock2/to_from_anybytes.v index f0c0918e..63bda3aa 100644 --- a/bedrock2/src/bedrock2/to_from_anybytes.v +++ b/bedrock2/src/bedrock2/to_from_anybytes.v @@ -1,5 +1,5 @@ -Require Import Coq.ZArith.ZArith. Local Open Scope Z_scope. -Require Import Coq.micromega.Lia. +From Coq Require Import ZArith. Local Open Scope Z_scope. +From Coq Require Import Lia. Require Import coqutil.Datatypes.Inhabited. Require Import coqutil.Word.Interface coqutil.Word.Properties coqutil.Word.Bitwidth. Require Import coqutil.Map.Interface. diff --git a/bedrock2/src/bedrock2/unzify.v b/bedrock2/src/bedrock2/unzify.v index b45a76b8..11e4894b 100644 --- a/bedrock2/src/bedrock2/unzify.v +++ b/bedrock2/src/bedrock2/unzify.v @@ -1,6 +1,6 @@ (* Z-ify word expressions in an undoable (unzify) way *) -Require Import Coq.ZArith.ZArith Coq.micromega.Lia. +From Coq Require Import ZArith Lia. Require Import coqutil.Word.Interface coqutil.Word.Properties. Require Import coqutil.Z.Lia. Require Import coqutil.Datatypes.ZList. diff --git a/bedrock2/src/bedrock2Examples/ARPResponderProofs.v b/bedrock2/src/bedrock2Examples/ARPResponderProofs.v index d4f52115..6e3ba7a8 100644 --- a/bedrock2/src/bedrock2Examples/ARPResponderProofs.v +++ b/bedrock2/src/bedrock2Examples/ARPResponderProofs.v @@ -1,4 +1,4 @@ -From Coq Require Import Strings.String Lists.List ZArith.BinInt. +From Coq Require Import String List BinInt. From coqutil.Word Require Import Interface. From bedrock2 Require Import Semantics BasicC32Semantics ProgramLogic. Require Import coqutil.Byte. diff --git a/bedrock2/src/bedrock2Examples/Demos.v b/bedrock2/src/bedrock2Examples/Demos.v index cd5667ab..6cc06b39 100644 --- a/bedrock2/src/bedrock2Examples/Demos.v +++ b/bedrock2/src/bedrock2Examples/Demos.v @@ -1,4 +1,4 @@ -Require Import Coq.ZArith.BinInt Coq.Strings.String Coq.Lists.List. Import ListNotations. +From Coq Require Import BinInt String List. Import ListNotations. Require Import coqutil.Macros.subst coqutil.Macros.unique bedrock2.Syntax. Require Import bedrock2.NotationsCustomEntry. Require Import coqutil.sanity. diff --git a/bedrock2/src/bedrock2Examples/FE310CompilerDemo.v b/bedrock2/src/bedrock2Examples/FE310CompilerDemo.v index 08033dc2..5f7543a2 100644 --- a/bedrock2/src/bedrock2Examples/FE310CompilerDemo.v +++ b/bedrock2/src/bedrock2Examples/FE310CompilerDemo.v @@ -1,8 +1,8 @@ From coqutil Require Import sanity. Local Unset Universe Minimization ToSet. -Require Import Coq.Strings.String. +From Coq Require Import String. Require Import coqutil.Z.Lia. -Require Import Coq.ZArith.BinInt. +From Coq Require Import BinInt. Require Import bedrock2.Syntax. Definition MMIOAction: Type := String.string. diff --git a/bedrock2/src/bedrock2Examples/FlatConstMem.v b/bedrock2/src/bedrock2Examples/FlatConstMem.v index ea65a48f..83c55df3 100644 --- a/bedrock2/src/bedrock2Examples/FlatConstMem.v +++ b/bedrock2/src/bedrock2Examples/FlatConstMem.v @@ -15,7 +15,8 @@ Require Import coqutil.Macros.symmetry. Require Import coqutil.Word.Interface coqutil.Word.Properties. Require Import bedrock2.Semantics bedrock2.ProgramLogic bedrock2.Array. Require Import bedrock2.Map.Separation bedrock2.Map.SeparationLogic. -Require Import Coq.Lists.List coqutil.Map.OfListWord. +From Coq Require Import List. +Require Import coqutil.Map.OfListWord. Require Import coqutil.Z.Lia. Require Import coqutil.Tactics.Tactics. Require Import coqutil.Tactics.letexists. diff --git a/bedrock2/src/bedrock2Examples/LAN9250.v b/bedrock2/src/bedrock2Examples/LAN9250.v index 899c2d0c..7ea5b324 100644 --- a/bedrock2/src/bedrock2Examples/LAN9250.v +++ b/bedrock2/src/bedrock2Examples/LAN9250.v @@ -118,7 +118,7 @@ Definition lan9250_tx := func! (p, l) ~> err { Require Import bedrock2.ProgramLogic. Require Import bedrock2.FE310CSemantics. Require Import coqutil.Word.Interface. -Require Import Coq.Lists.List. Import ListNotations. +From Coq Require Import List. Import ListNotations. Require Import bedrock2.TracePredicate. Import TracePredicateNotations. Require bedrock2Examples.lightbulb_spec. Require Import bedrock2.ZnWords. diff --git a/bedrock2/src/bedrock2Examples/SPI.v b/bedrock2/src/bedrock2Examples/SPI.v index 479c1628..b25c2df7 100644 --- a/bedrock2/src/bedrock2Examples/SPI.v +++ b/bedrock2/src/bedrock2Examples/SPI.v @@ -43,7 +43,7 @@ Definition spi_xchg := func! (b) ~> (b, busy) { Require Import bedrock2.ProgramLogic. Require Import bedrock2.FE310CSemantics bedrock2.Semantics. -Require Import Coq.Lists.List. Import ListNotations. +From Coq Require Import List. Import ListNotations. Require Import bedrock2.TracePredicate. Import TracePredicateNotations. Require Import bedrock2.ZnWords. diff --git a/bedrock2/src/bedrock2Examples/Trace.v b/bedrock2/src/bedrock2Examples/Trace.v index d91baee1..a7845980 100644 --- a/bedrock2/src/bedrock2Examples/Trace.v +++ b/bedrock2/src/bedrock2Examples/Trace.v @@ -1,10 +1,10 @@ Require Import coqutil.Z.Lia. -Require Import Coq.ZArith.ZArith. Open Scope Z_scope. -Require Import Coq.Lists.List. Import ListNotations. +From Coq Require Import ZArith. Open Scope Z_scope. +From Coq Require Import List. Import ListNotations. Require Import coqutil.Word.Interface coqutil.Word.Properties coqutil.Word.Bitwidth32. Require Import coqutil.Map.Interface coqutil.Map.Properties. Require Import coqutil.Tactics.Tactics. -Require Import Coq.Strings.String. +From Coq Require Import String. Require Import bedrock2.TracePredicate. Import TracePredicateNotations. Require Import bedrock2.Semantics bedrock2.MetricSemantics. Require Import bedrock2.Syntax. diff --git a/bedrock2/src/bedrock2Examples/bsearch.v b/bedrock2/src/bedrock2Examples/bsearch.v index 2e452db7..b1875881 100644 --- a/bedrock2/src/bedrock2Examples/bsearch.v +++ b/bedrock2/src/bedrock2Examples/bsearch.v @@ -1,4 +1,4 @@ -Require Import Coq.Strings.String Coq.ZArith.ZArith. +From Coq Require Import String ZArith. Require Import coqutil.Z.Lia. From bedrock2 Require Import NotationsCustomEntry ProgramLogic Map.Separation Array Scalars Loops. diff --git a/bedrock2/src/bedrock2Examples/chacha20.v b/bedrock2/src/bedrock2Examples/chacha20.v index 42305292..0f50d2db 100644 --- a/bedrock2/src/bedrock2Examples/chacha20.v +++ b/bedrock2/src/bedrock2Examples/chacha20.v @@ -49,7 +49,7 @@ Section chacha20. End chacha20. (* -Require Import Coq.Strings.String bedrock2.ToCString coqutil.Macros.WithBaseName. +From Coq Require Import String bedrock2.ToCString coqutil.Macros.WithBaseName. Example chacha20_block_c_string := Eval vm_compute in ToCString.c_module &[,chacha20_block; chacha20_quarter]. Print chacha20_block_c_string. diff --git a/bedrock2/src/bedrock2Examples/ipow.v b/bedrock2/src/bedrock2Examples/ipow.v index bdfb950c..9037a55a 100644 --- a/bedrock2/src/bedrock2Examples/ipow.v +++ b/bedrock2/src/bedrock2Examples/ipow.v @@ -1,4 +1,5 @@ -Require Import Coq.ZArith.ZArith coqutil.Z.div_mod_to_equations. +From Coq Require Import ZArith. +Require Import coqutil.Z.div_mod_to_equations. Require Import bedrock2.NotationsCustomEntry. Import Syntax BinInt String List.ListNotations ZArith. Require Import coqutil.Z.Lia. diff --git a/bedrock2/src/bedrock2Examples/lightbulb_spec.v b/bedrock2/src/bedrock2Examples/lightbulb_spec.v index 63a047dc..fe9fdf34 100644 --- a/bedrock2/src/bedrock2Examples/lightbulb_spec.v +++ b/bedrock2/src/bedrock2Examples/lightbulb_spec.v @@ -1,5 +1,5 @@ Require Import bedrock2.TracePredicate. -Require Import Coq.ZArith.BinInt Coq.Strings.String. +From Coq Require Import BinInt String. Require Import coqutil.Word.Interface. Require Import coqutil.Map.Interface. Require Import coqutil.Byte. diff --git a/bedrock2/src/bedrock2Examples/swap_by_add.v b/bedrock2/src/bedrock2Examples/swap_by_add.v index b7ac6491..9ca0263b 100644 --- a/bedrock2/src/bedrock2Examples/swap_by_add.v +++ b/bedrock2/src/bedrock2Examples/swap_by_add.v @@ -22,7 +22,7 @@ Require bedrock2.WeakestPreconditionProperties. From coqutil.Tactics Require Import Tactics letexists eabstract. Require Import bedrock2.ProgramLogic bedrock2.Scalars. Require Import coqutil.Word.Interface coqutil.Word.Properties coqutil.Word.Naive. -Require Import coqutil.Tactics.eplace Coq.setoid_ring.Ring_tac. +Require Import coqutil.Tactics.eplace Ring_tac. Section WithParameters. Context {mem: map.map word32 Byte.byte} {mem_ok: map.ok mem}. diff --git a/compiler/src/compiler/DeadCodeElim.v b/compiler/src/compiler/DeadCodeElim.v index db0ad51e..6d1c8fbc 100644 --- a/compiler/src/compiler/DeadCodeElim.v +++ b/compiler/src/compiler/DeadCodeElim.v @@ -1,5 +1,5 @@ Require Import compiler.FlatImp. -Require Import Coq.Lists.List. Import ListNotations. +From Coq Require Import List. Import ListNotations. Require Import bedrock2.Syntax. Require Import coqutil.Tactics.fwd. Require Import String. diff --git a/compiler/src/compiler/DeadCodeElimDef.v b/compiler/src/compiler/DeadCodeElimDef.v index 7ebf13a8..fcf3ab19 100644 --- a/compiler/src/compiler/DeadCodeElimDef.v +++ b/compiler/src/compiler/DeadCodeElimDef.v @@ -1,5 +1,5 @@ Require Import compiler.FlatImp. -Require Import Coq.Lists.List. Import ListNotations. +From Coq Require Import List. Import ListNotations. Require Import bedrock2.Syntax. Require Import coqutil.Tactics.fwd. Require Import String. @@ -12,8 +12,8 @@ Require Import compiler.util.Common. Require Import bedrock2.MetricLogging. Require Import coqutil.Tactics.fwd. (* below only for of_list_list_diff *) -Require Import Coq.Logic.PropExtensionality. -Require Import Coq.Logic.FunctionalExtensionality. +From Coq Require Import PropExtensionality. +From Coq Require Import FunctionalExtensionality. Section WithArguments1. Context {width: Z}. diff --git a/compiler/src/compiler/DivisibleBy4.v b/compiler/src/compiler/DivisibleBy4.v index da106747..48c359ca 100644 --- a/compiler/src/compiler/DivisibleBy4.v +++ b/compiler/src/compiler/DivisibleBy4.v @@ -1,4 +1,4 @@ -Require Import Coq.ZArith.ZArith. +From Coq Require Import ZArith. Require Import coqutil.Z.Lia. Require Import coqutil.Word.Interface coqutil.Word.Properties. Require Import coqutil.Tactics.Tactics. diff --git a/compiler/src/compiler/ElfPrinter.v b/compiler/src/compiler/ElfPrinter.v index e4fdc929..402d9f19 100644 --- a/compiler/src/compiler/ElfPrinter.v +++ b/compiler/src/compiler/ElfPrinter.v @@ -1,9 +1,9 @@ (* ELF printer for a tiny subset of the spec at https://refspecs.linuxfoundation.org/elf/elf.pdf *) -Require Import Coq.ZArith.ZArith. Local Open Scope Z_scope. -Require Import Coq.Strings.String. -Require Import Coq.Strings.Ascii. +From Coq Require Import ZArith. Local Open Scope Z_scope. +From Coq Require Import String. +From Coq Require Import Ascii. Require Import coqutil.Datatypes.ZList. Require Import coqutil.Word.Interface. Require Import coqutil.Word.LittleEndianList. diff --git a/compiler/src/compiler/ExprImp.v b/compiler/src/compiler/ExprImp.v index 2e02425c..48eed8a2 100644 --- a/compiler/src/compiler/ExprImp.v +++ b/compiler/src/compiler/ExprImp.v @@ -1,6 +1,6 @@ -Require Import Coq.ZArith.ZArith. -Require Import Coq.Lists.List. Import ListNotations. -Require Import Coq.Program.Tactics. +From Coq Require Import ZArith. +From Coq Require Import List. Import ListNotations. +From Coq.Program Require Import Tactics. Require Import riscv.Utility.Utility. Require Export bedrock2.Syntax. Require Export bedrock2.Semantics. diff --git a/compiler/src/compiler/ExprImpEventLoopSpec.v b/compiler/src/compiler/ExprImpEventLoopSpec.v index 9fd05641..287fa2f4 100644 --- a/compiler/src/compiler/ExprImpEventLoopSpec.v +++ b/compiler/src/compiler/ExprImpEventLoopSpec.v @@ -1,4 +1,4 @@ -Require Import Coq.ZArith.ZArith. +From Coq Require Import ZArith. Require Coq.Strings.String. Require Import coqutil.Map.Interface coqutil.Word.Interface. Require Import bedrock2.MetricLogging. diff --git a/compiler/src/compiler/FlatImp.v b/compiler/src/compiler/FlatImp.v index 72914d2a..30a46320 100644 --- a/compiler/src/compiler/FlatImp.v +++ b/compiler/src/compiler/FlatImp.v @@ -1,6 +1,6 @@ -Require Import Coq.Bool.Bool. -Require Import Coq.ZArith.ZArith. -Require Import Coq.Lists.List. Import ListNotations. +From Coq Require Import Bool. +From Coq Require Import ZArith. +From Coq Require Import List. Import ListNotations. Require Import bedrock2.MetricLogging. Require Import coqutil.Macros.unique. Require Import bedrock2.Memory. diff --git a/compiler/src/compiler/FlatImpConstraints.v b/compiler/src/compiler/FlatImpConstraints.v index 58f99b0e..a2691f20 100644 --- a/compiler/src/compiler/FlatImpConstraints.v +++ b/compiler/src/compiler/FlatImpConstraints.v @@ -1,7 +1,7 @@ (* constraints on FlatImp ASTs, referenced by several phases *) Require Import compiler.FlatImp. Require Import compiler.Registers. -Require Import Coq.ZArith.ZArith. +From Coq Require Import ZArith. Fixpoint uses_standard_arg_regs(s: stmt Z): Prop := match s with diff --git a/compiler/src/compiler/FlatImpUniqueSepLog.v b/compiler/src/compiler/FlatImpUniqueSepLog.v index 8cb62cf5..4481c194 100644 --- a/compiler/src/compiler/FlatImpUniqueSepLog.v +++ b/compiler/src/compiler/FlatImpUniqueSepLog.v @@ -1,6 +1,6 @@ -Require Import Coq.Bool.Bool. -Require Import Coq.ZArith.ZArith. -Require Import Coq.Lists.List. Import ListNotations. +From Coq Require Import Bool. +From Coq Require Import ZArith. +From Coq Require Import List. Import ListNotations. Require Import bedrock2.MetricLogging. Require Import coqutil.Macros.unique. Require Import bedrock2.Memory. diff --git a/compiler/src/compiler/FlatToRiscvCommon.v b/compiler/src/compiler/FlatToRiscvCommon.v index 1fca2883..c82c31cf 100644 --- a/compiler/src/compiler/FlatToRiscvCommon.v +++ b/compiler/src/compiler/FlatToRiscvCommon.v @@ -1,9 +1,9 @@ Require Import riscv.Utility.Monads. Require Import riscv.Utility.MonadNotations. Require Import coqutil.Macros.unique. Require Import compiler.FlatImp. -Require Import Coq.Lists.List. +From Coq Require Import List. Import ListNotations. -Require Import Coq.ZArith.ZArith. +From Coq Require Import ZArith. Require Import riscv.Spec.Decode. Require Import riscv.Spec.Machine. Require Import riscv.Spec.PseudoInstructions. @@ -14,9 +14,9 @@ Require Import riscv.Platform.Run. Require Import riscv.Platform.Memory. Require Import riscv.Utility.PowerFunc. Require Import coqutil.Decidable. -Require Import Coq.Program.Tactics. +From Coq.Program Require Import Tactics. Require Import coqutil.Tactics.rewr. -Require Import Coq.Bool.Bool. +From Coq Require Import Bool. Require Import riscv.Utility.InstructionCoercions. Require Import riscv.Spec.Primitives. Require Import riscv.Spec.MetricPrimitives. diff --git a/compiler/src/compiler/FlatToRiscvDef.v b/compiler/src/compiler/FlatToRiscvDef.v index 649c6d2a..0e77fd76 100644 --- a/compiler/src/compiler/FlatToRiscvDef.v +++ b/compiler/src/compiler/FlatToRiscvDef.v @@ -1,9 +1,9 @@ Require Import coqutil.Macros.unique. Require Import coqutil.Decidable. Require Import compiler.FlatImp. -Require Import Coq.Lists.List. +From Coq Require Import List. Import ListNotations. -Require Import Coq.ZArith.ZArith. +From Coq Require Import ZArith. Require Import riscv.Spec.Machine. Require Import riscv.Spec.PseudoInstructions. Require Import riscv.Utility.InstructionCoercions. diff --git a/compiler/src/compiler/FlatToRiscvFunctions.v b/compiler/src/compiler/FlatToRiscvFunctions.v index 5aa6f318..85b87778 100644 --- a/compiler/src/compiler/FlatToRiscvFunctions.v +++ b/compiler/src/compiler/FlatToRiscvFunctions.v @@ -1,8 +1,8 @@ Require Import coqutil.Tactics.rdelta. Require Import coqutil.Tactics.rewr. Require Import coqutil.Datatypes.PropSet. -Require Import Coq.Logic.FunctionalExtensionality. -Require Import Coq.Logic.PropExtensionality. +From Coq Require Import FunctionalExtensionality. +From Coq Require Import PropExtensionality. Require Import riscv.Spec.Decode. Require Import riscv.Spec.Primitives. Require Import riscv.Platform.RiscvMachine. diff --git a/compiler/src/compiler/FlattenExpr.v b/compiler/src/compiler/FlattenExpr.v index f30cf146..f162e0c9 100644 --- a/compiler/src/compiler/FlattenExpr.v +++ b/compiler/src/compiler/FlattenExpr.v @@ -9,10 +9,10 @@ Require Import bedrock2.Syntax. Require Import bedrock2.MetricLogging. Require Import bedrock2.Semantics bedrock2.MetricSemantics. Require Import coqutil.Macros.unique. -Require Import Coq.Bool.Bool. +From Coq Require Import Bool. Require Import coqutil.Datatypes.PropSet. Require Import coqutil.Tactics.Simp. -Require Import Coq.Program.Tactics. +From Coq.Program Require Import Tactics. Require Import coqutil.Datatypes.String. Require Import compiler.FlattenExprDef. Require Export coqutil.Word.SimplWordExpr. diff --git a/compiler/src/compiler/FlattenExprDef.v b/compiler/src/compiler/FlattenExprDef.v index 41ab0ee5..d087365a 100644 --- a/compiler/src/compiler/FlattenExprDef.v +++ b/compiler/src/compiler/FlattenExprDef.v @@ -9,7 +9,7 @@ Require Import riscv.Utility.Utility. Require Import bedrock2.MetricLogging. Require Import bedrock2.Semantics. Require Import coqutil.Macros.unique. -Require Import Coq.Bool.Bool. +From Coq Require Import Bool. Require Import coqutil.Datatypes.PropSet. Require Import coqutil.Tactics.Simp. Require Import coqutil.Datatypes.String. diff --git a/compiler/src/compiler/ForeverSafe.v b/compiler/src/compiler/ForeverSafe.v index 7bf0e073..d02d9701 100644 --- a/compiler/src/compiler/ForeverSafe.v +++ b/compiler/src/compiler/ForeverSafe.v @@ -1,4 +1,4 @@ -Require Import Coq.Lists.List. +From Coq Require Import List. Require Import coqutil.Map.Interface coqutil.Map.Properties. Require Import riscv.Utility.Monads. Require Import riscv.Utility.Utility. diff --git a/compiler/src/compiler/GoFlatToRiscv.v b/compiler/src/compiler/GoFlatToRiscv.v index 92cfd4cb..3c1b47b9 100644 --- a/compiler/src/compiler/GoFlatToRiscv.v +++ b/compiler/src/compiler/GoFlatToRiscv.v @@ -2,7 +2,7 @@ From Coq Require Import ZArith. Require Import coqutil.Z.Lia. Require Import coqutil.Z.Lia. Require Import coqutil.Z.div_mod_to_equations. -Require Import Coq.Lists.List. Import ListNotations. +From Coq Require Import List. Import ListNotations. Require Import coqutil.Map.Interface coqutil.Map.Properties. Require Import coqutil.Word.Interface coqutil.Word.Properties. Require Import riscv.Utility.Monads. diff --git a/compiler/src/compiler/LowerPipeline.v b/compiler/src/compiler/LowerPipeline.v index b76e3afc..5a188042 100644 --- a/compiler/src/compiler/LowerPipeline.v +++ b/compiler/src/compiler/LowerPipeline.v @@ -1,4 +1,4 @@ -Require Import Coq.Logic.FunctionalExtensionality. +From Coq Require Import FunctionalExtensionality. Require Import coqutil.Map.Interface. Require Import coqutil.Map.MapEauto. Require Import coqutil.Tactics.Tactics. diff --git a/compiler/src/compiler/MMIO.v b/compiler/src/compiler/MMIO.v index 52bfedd4..9c48d3ba 100644 --- a/compiler/src/compiler/MMIO.v +++ b/compiler/src/compiler/MMIO.v @@ -1,4 +1,4 @@ -Require Import Coq.ZArith.ZArith. +From Coq Require Import ZArith. Require Import coqutil.Z.Lia. Require Import coqutil.Macros.unique. Require Import compiler.util.Common. diff --git a/compiler/src/compiler/MemoryLayout.v b/compiler/src/compiler/MemoryLayout.v index 1eda987f..1c7d0b49 100644 --- a/compiler/src/compiler/MemoryLayout.v +++ b/compiler/src/compiler/MemoryLayout.v @@ -1,4 +1,4 @@ -Require Import Coq.ZArith.ZArith. +From Coq Require Import ZArith. Require Import coqutil.Word.Interface. Require Import riscv.Utility.Utility. Require Import compiler.SeparationLogic. diff --git a/compiler/src/compiler/NaiveRiscvWordProperties.v b/compiler/src/compiler/NaiveRiscvWordProperties.v index 4849058f..5b0dedcc 100644 --- a/compiler/src/compiler/NaiveRiscvWordProperties.v +++ b/compiler/src/compiler/NaiveRiscvWordProperties.v @@ -1,7 +1,7 @@ -Require Import Coq.ZArith.ZArith. +From Coq Require Import ZArith. Require Import coqutil.Word.Interface coqutil.Word.Properties. Require Import coqutil.Z.BitOps coqutil.Z.ZLib. -Require Import Coq.micromega.Lia. +From Coq Require Import Lia. Require Import coqutil.Tactics.destr. Require Import compiler.RiscvWordProperties. Require coqutil.Word.Naive. diff --git a/compiler/src/compiler/NameGen.v b/compiler/src/compiler/NameGen.v index 81b55099..8e42eb37 100644 --- a/compiler/src/compiler/NameGen.v +++ b/compiler/src/compiler/NameGen.v @@ -1,4 +1,4 @@ -Require Import Coq.Lists.List. +From Coq Require Import List. Require Import coqutil.Datatypes.PropSet. Class NameGen(var st: Type) := mkNameGen { diff --git a/compiler/src/compiler/Pipeline.v b/compiler/src/compiler/Pipeline.v index d57b1767..4d24cad2 100644 --- a/compiler/src/compiler/Pipeline.v +++ b/compiler/src/compiler/Pipeline.v @@ -1,5 +1,5 @@ Require Export Coq.Lists.List. -Require Import Coq.ZArith.ZArith. +From Coq Require Import ZArith. Export ListNotations. Require Export coqutil.Decidable. Require compiler.ExprImp. diff --git a/compiler/src/compiler/RegAlloc.v b/compiler/src/compiler/RegAlloc.v index c5ed8d75..9d904334 100644 --- a/compiler/src/compiler/RegAlloc.v +++ b/compiler/src/compiler/RegAlloc.v @@ -1,7 +1,7 @@ Require Import compiler.util.Common. Require Import compiler.FlatImp. Require Import coqutil.Tactics.simpl_rewrite. -Require Import Coq.Lists.List. Import ListNotations. +From Coq Require Import List. Import ListNotations. Require Import riscv.Utility.Utility. Require Import coqutil.Map.MapEauto. Require Import bedrock2.Syntax. diff --git a/compiler/src/compiler/Registers.v b/compiler/src/compiler/Registers.v index fbed550c..ba549c11 100644 --- a/compiler/src/compiler/Registers.v +++ b/compiler/src/compiler/Registers.v @@ -1,4 +1,4 @@ -Require Import Coq.ZArith.ZArith. Local Open Scope Z_scope. +From Coq Require Import ZArith. Local Open Scope Z_scope. Require Import coqutil.Datatypes.List. (* RISC-V Calling Convention from diff --git a/compiler/src/compiler/RiscvEventLoop.v b/compiler/src/compiler/RiscvEventLoop.v index cd82e5bf..385d486d 100644 --- a/compiler/src/compiler/RiscvEventLoop.v +++ b/compiler/src/compiler/RiscvEventLoop.v @@ -1,6 +1,6 @@ From Coq Require Import ZArith. Require Import coqutil.Z.Lia. -Require Import Coq.Lists.List. Import ListNotations. +From Coq Require Import List. Import ListNotations. Require Import coqutil.Map.Interface coqutil.Map.Properties. Require Import coqutil.Word.Interface coqutil.Word.Properties. Require Import riscv.Utility.Monads. diff --git a/compiler/src/compiler/RiscvWordProperties.v b/compiler/src/compiler/RiscvWordProperties.v index 2e0bf537..83b46594 100644 --- a/compiler/src/compiler/RiscvWordProperties.v +++ b/compiler/src/compiler/RiscvWordProperties.v @@ -1,5 +1,5 @@ -Require Import Coq.ZArith.ZArith. -Require Import Coq.micromega.Lia. +From Coq Require Import ZArith. +From Coq Require Import Lia. Require Import coqutil.Word.Interface coqutil.Word.Properties. Require Import coqutil.Z.BitOps coqutil.Z.ZLib. Require Import coqutil.Tactics.destr. diff --git a/compiler/src/compiler/RunInstruction.v b/compiler/src/compiler/RunInstruction.v index ed2def57..f03b5dd1 100644 --- a/compiler/src/compiler/RunInstruction.v +++ b/compiler/src/compiler/RunInstruction.v @@ -1,7 +1,7 @@ From Coq Require Import ZArith. Require Import coqutil.Z.Lia. Require Import coqutil.Z.Lia. -Require Import Coq.Lists.List. Import ListNotations. +From Coq Require Import List. Import ListNotations. Require Import coqutil.Map.Interface coqutil.Map.Properties. Require Import coqutil.Word.Interface coqutil.Word.Properties. Require Import riscv.Utility.Monads. diff --git a/compiler/src/compiler/SeparationLogic.v b/compiler/src/compiler/SeparationLogic.v index 61c6f788..62c3d783 100644 --- a/compiler/src/compiler/SeparationLogic.v +++ b/compiler/src/compiler/SeparationLogic.v @@ -1,5 +1,5 @@ -Require Export Coq.Lists.List. Export ListNotations. -Require Export Coq.ZArith.ZArith. Open Scope Z_scope. +From Coq Require Export List. Export ListNotations. +From Coq Require Export ZArith. Open Scope Z_scope. Require Export coqutil.Word.Interface coqutil.Word.Properties. Require Export coqutil.Map.Interface coqutil.Map.Properties. Require Import coqutil.Tactics.rdelta coqutil.Tactics.destr coqutil.Decidable. @@ -18,8 +18,8 @@ Require Import coqutil.Tactics.Simp. Require Export riscv.Utility.Utility. Require Import riscv.Utility.Encode. Require Import riscv.Spec.Decode. -Require Import Coq.Logic.FunctionalExtensionality. -Require Import Coq.Logic.PropExtensionality. +From Coq Require Import FunctionalExtensionality. +From Coq Require Import PropExtensionality. Declare Scope sep_scope. diff --git a/compiler/src/compiler/Spilling.v b/compiler/src/compiler/Spilling.v index b91c0beb..5b401c7c 100644 --- a/compiler/src/compiler/Spilling.v +++ b/compiler/src/compiler/Spilling.v @@ -1,9 +1,9 @@ Require Import compiler.util.Common. Require Import bedrock2.Map.SeparationLogic. Require Import compiler.FlatImp. -Require Import Coq.Lists.List. Import ListNotations. -Require Import Coq.Logic.PropExtensionality. -Require Import Coq.Logic.FunctionalExtensionality. +From Coq Require Import List. Import ListNotations. +From Coq Require Import PropExtensionality. +From Coq Require Import FunctionalExtensionality. Require Import riscv.Utility.Utility. Require Import coqutil.Map.MapEauto. Require Import coqutil.Tactics.Simp. diff --git a/compiler/src/compiler/StringNameGen.v b/compiler/src/compiler/StringNameGen.v index cda8d4ce..3337f25b 100644 --- a/compiler/src/compiler/StringNameGen.v +++ b/compiler/src/compiler/StringNameGen.v @@ -1,11 +1,11 @@ -Require Import Coq.Strings.Ascii. -Require Import Coq.Strings.String. -Require Import Coq.Lists.List. +From Coq Require Import Ascii. +From Coq Require Import String. +From Coq Require Import List. Require Import compiler.util.Common. Require Import compiler.NameGen. -Require Import Coq.NArith.NArith. -Require Import Coq.Numbers.DecimalString. -Require Import Coq.Numbers.DecimalN. +From Coq Require Import NArith. +From Coq Require Import DecimalString. +From Coq Require Import DecimalN. Local Open Scope string_scope. Local Open Scope char_scope. diff --git a/compiler/src/compiler/Symbols.v b/compiler/src/compiler/Symbols.v index 580dcfb6..f46ac3df 100644 --- a/compiler/src/compiler/Symbols.v +++ b/compiler/src/compiler/Symbols.v @@ -1,6 +1,7 @@ -Require Import Coq.Strings.String Coq.Strings.HexString. -Require Import Coq.Init.Byte coqutil.Byte. -Require Import Coq.Lists.List. +From Coq Require Import String HexString. +From Coq.Init Require Import Byte. +Require Import coqutil.Byte. +From Coq Require Import List. Require Import coqutil.Map.Interface. Require Import coqutil.Map.Z_keyed_SortedListMap. Local Open Scope string_scope. diff --git a/compiler/src/compiler/ToplevelLoop.v b/compiler/src/compiler/ToplevelLoop.v index 7b82edff..290f4bfd 100644 --- a/compiler/src/compiler/ToplevelLoop.v +++ b/compiler/src/compiler/ToplevelLoop.v @@ -1,9 +1,9 @@ Require Export Coq.Lists.List. -Require Import Coq.ZArith.ZArith. -Require Import Coq.Strings.String. Local Open Scope string_scope. +From Coq Require Import ZArith. +From Coq Require Import String. Local Open Scope string_scope. Export ListNotations. Require Export coqutil.Decidable. -Require Import Coq.Program.Tactics. +From Coq.Program Require Import Tactics. Require Import coqutil.Tactics.rewr. Require compiler.ExprImp. Require Export compiler.FlattenExprDef. diff --git a/compiler/src/compiler/UniqueSepLog.v b/compiler/src/compiler/UniqueSepLog.v index d8c31768..e8ac630b 100644 --- a/compiler/src/compiler/UniqueSepLog.v +++ b/compiler/src/compiler/UniqueSepLog.v @@ -103,9 +103,9 @@ P1 = fun m => all keys in m are < 3 P2 = fun m => all keys in m are < 4 proving any (R * P1) m is as easy as giving all of m to R and giving map.empty to P1 *) -Require Import Coq.Lists.List. Import ListNotations. -Require Import Coq.ZArith.ZArith. -Require Import Coq.Init.Byte. +From Coq Require Import List. Import ListNotations. +From Coq Require Import ZArith. +From Coq.Init Require Import Byte. Require Import coqutil.Decidable. Require Import coqutil.Map.Interface coqutil.Map.Properties. Require Import coqutil.Word.Interface coqutil.Word.Properties. diff --git a/compiler/src/compiler/UseImmediate.v b/compiler/src/compiler/UseImmediate.v index 71f4a7e8..c4e0b5af 100644 --- a/compiler/src/compiler/UseImmediate.v +++ b/compiler/src/compiler/UseImmediate.v @@ -1,6 +1,6 @@ Require Import compiler.util.Common. Require Import compiler.FlatImp. -Require Import Coq.Lists.List. Import ListNotations. +From Coq Require Import List. Import ListNotations. Require Import bedrock2.Syntax. Require Import coqutil.Tactics.fwd. Require Import String. diff --git a/compiler/src/compiler/UseImmediateDef.v b/compiler/src/compiler/UseImmediateDef.v index fdb505f8..fc611235 100644 --- a/compiler/src/compiler/UseImmediateDef.v +++ b/compiler/src/compiler/UseImmediateDef.v @@ -1,6 +1,6 @@ Require Import compiler.util.Common. Require Import compiler.FlatImp. -Require Import Coq.Lists.List. Import ListNotations. +From Coq Require Import List. Import ListNotations. Require Import bedrock2.Syntax. Require Import coqutil.Tactics.fwd. Require Import String. diff --git a/compiler/src/compiler/ZLemmas.v b/compiler/src/compiler/ZLemmas.v index 2a076f74..6606b6fe 100644 --- a/compiler/src/compiler/ZLemmas.v +++ b/compiler/src/compiler/ZLemmas.v @@ -1,4 +1,4 @@ -Require Import Coq.ZArith.ZArith. +From Coq Require Import ZArith. Require Import coqutil.Z.Lia. Require Import coqutil.Z.BitOps. Require Import coqutil.Z.bitblast. diff --git a/compiler/src/compiler/ZNameGen.v b/compiler/src/compiler/ZNameGen.v index fed7f46a..2fcbadbb 100644 --- a/compiler/src/compiler/ZNameGen.v +++ b/compiler/src/compiler/ZNameGen.v @@ -1,4 +1,4 @@ -Require Import Coq.Lists.List. +From Coq Require Import List. Require Import coqutil.Z.Lia. Require Import compiler.util.Common. Require Import compiler.NameGen. diff --git a/compiler/src/compiler/memory_mapped_ext_calls_compiler.v b/compiler/src/compiler/memory_mapped_ext_calls_compiler.v index 5a421ec6..7cbb8d95 100644 --- a/compiler/src/compiler/memory_mapped_ext_calls_compiler.v +++ b/compiler/src/compiler/memory_mapped_ext_calls_compiler.v @@ -1,5 +1,5 @@ -Require Import Coq.ZArith.ZArith. -Require Import Coq.micromega.Lia. +From Coq Require Import ZArith. +From Coq Require Import Lia. Require Import coqutil.Tactics.fwd. Require Import coqutil.Map.Interface coqutil.Map.Properties coqutil.Map.Domain. Require Import compiler.util.Common. diff --git a/compiler/src/compiler/memory_mapped_ext_calls_riscv.v b/compiler/src/compiler/memory_mapped_ext_calls_riscv.v index 35668d7a..90ae8533 100644 --- a/compiler/src/compiler/memory_mapped_ext_calls_riscv.v +++ b/compiler/src/compiler/memory_mapped_ext_calls_riscv.v @@ -1,11 +1,11 @@ (* Based on riscv.Platform.MinimalMMIO and riscv.Platform.MetricMinimalMMIO, but with a different nonmem_load and nonmem_store *) -Require Import Coq.Strings.String. +From Coq Require Import String. Require coqutil.Datatypes.String. -Require Import Coq.ZArith.ZArith. -Require Import Coq.Logic.FunctionalExtensionality. -Require Import Coq.Logic.PropExtensionality. +From Coq Require Import ZArith. +From Coq Require Import FunctionalExtensionality. +From Coq Require Import PropExtensionality. Require Import bedrock2.memory_mapped_ext_spec. (* import this early because bedrock2.Memory.load_bytes vs riscv.Platform.Memory.load_bytes *) Require Import bedrock2.TraceInspection. Require Import riscv.Utility.Monads. @@ -16,7 +16,7 @@ Require Import riscv.Spec.Machine. Require Import riscv.Utility.Utility. Require Import riscv.Spec.Primitives. Require Import riscv.Spec.MetricPrimitives. -Require Import Coq.Lists.List. Import ListNotations. +From Coq Require Import List. Import ListNotations. Require Export riscv.Platform.RiscvMachine. Require Import riscv.Platform.MaterializeRiscvProgram. Require Export riscv.Platform.MetricRiscvMachine. diff --git a/compiler/src/compiler/mod4_0.v b/compiler/src/compiler/mod4_0.v index a23e07dc..9ee27c0f 100644 --- a/compiler/src/compiler/mod4_0.v +++ b/compiler/src/compiler/mod4_0.v @@ -1,5 +1,5 @@ (*the library would generalize over 4, and have good enough automation to not require these specialized lemmas*) -Require Import Coq.ZArith.ZArith. Local Open Scope Z_scope. +From Coq Require Import ZArith. Local Open Scope Z_scope. Require Import coqutil.Z.Lia. Lemma mod4_0_add: forall (x y: Z), diff --git a/compiler/src/compiler/regs_initialized.v b/compiler/src/compiler/regs_initialized.v index ab4c0683..f1d530a4 100644 --- a/compiler/src/compiler/regs_initialized.v +++ b/compiler/src/compiler/regs_initialized.v @@ -1,4 +1,4 @@ -Require Import Coq.ZArith.ZArith. +From Coq Require Import ZArith. Require Import coqutil.Map.Interface coqutil.Map.Properties. Require Import coqutil.Tactics.Tactics. Local Open Scope Z_scope. diff --git a/compiler/src/compiler/util/Common.v b/compiler/src/compiler/util/Common.v index 31a4b13d..c8892983 100644 --- a/compiler/src/compiler/util/Common.v +++ b/compiler/src/compiler/util/Common.v @@ -1,8 +1,8 @@ Require Export coqutil.Z.Lia. Require Export Coq.Strings.String. Require Export coqutil.Datatypes.Result. Export ResultMonadNotations. -Require Export Coq.ZArith.ZArith. -Require Export Coq.Lists.List. +From Coq Require Export ZArith. +From Coq Require Export List. Require Export coqutil.Map.Interface coqutil.Map.Properties coqutil.Map.Solver. Require Export coqutil.Word.Interface coqutil.Word.Properties. Require Export coqutil.Decidable. diff --git a/compiler/src/compilerExamples/AssemblyVerif.v b/compiler/src/compilerExamples/AssemblyVerif.v index 4f7fb99e..fb842565 100644 --- a/compiler/src/compilerExamples/AssemblyVerif.v +++ b/compiler/src/compilerExamples/AssemblyVerif.v @@ -1,4 +1,4 @@ -Require Import Coq.Lists.List. +From Coq Require Import List. Require Import coqutil.Z.Lia. Import ListNotations. Require Import coqutil.Word.Properties. @@ -6,7 +6,7 @@ Require Import riscv.Utility.Monads. Require Import riscv.Spec.Primitives. Require Import riscv.Spec.MetricPrimitives. Require Import riscv.Spec.Machine. -Require Import Coq.ZArith.ZArith. +From Coq Require Import ZArith. Require Import riscv.Utility.Utility. Require Import riscv.Platform.Memory. Require Import riscv.Platform.Run. diff --git a/compiler/src/compilerExamples/EditDistExample.v b/compiler/src/compilerExamples/EditDistExample.v index 014d274c..ba5dea48 100644 --- a/compiler/src/compilerExamples/EditDistExample.v +++ b/compiler/src/compilerExamples/EditDistExample.v @@ -1,8 +1,8 @@ (* -Require Import Coq.ZArith.ZArith. +From Coq Require Import ZArith. Require Import compiler.ExprImp. Require Import compiler.util.Common. -Require Import Coq.Lists.List. +From Coq Require Import List. Import ListNotations. Require Import compiler.util.Common. Require Import compiler.Pipeline. @@ -11,8 +11,8 @@ Require Import riscv.Platform.MinimalLogging. Require Import riscv.Utility.Utility. Require Import riscv.Utility.Encode. Require Import compilerExamples.Fibonacci. -Require Import Coq.Strings.String. -Require Import Coq.Strings.Ascii. +From Coq Require Import String. +From Coq Require Import Ascii. Require Import compiler.NameGen. diff --git a/compiler/src/compilerExamples/FibCompiled.v b/compiler/src/compilerExamples/FibCompiled.v index 7dbc83ab..689ea590 100644 --- a/compiler/src/compilerExamples/FibCompiled.v +++ b/compiler/src/compilerExamples/FibCompiled.v @@ -1,4 +1,4 @@ -Require Import Coq.Arith.Arith. +From Coq Require Import Arith. Require Import bedrock2.Map.SeparationLogic. Require Import bedrock2.ptsto_bytes. Require Import coqutil.Decidable. diff --git a/compiler/src/compilerExamples/Fibonacci.v b/compiler/src/compilerExamples/Fibonacci.v index 94c032f4..fe4d290e 100644 --- a/compiler/src/compilerExamples/Fibonacci.v +++ b/compiler/src/compilerExamples/Fibonacci.v @@ -1,5 +1,5 @@ (* -Require Import Coq.Lists.List. +From Coq Require Import List. Import ListNotations. Require bedrock2Examples.Demos. Require Import coqutil.Decidable. diff --git a/compiler/src/compilerExamples/InlineAssemblyMacro.v b/compiler/src/compilerExamples/InlineAssemblyMacro.v index bf2ccccf..c7f5e7a3 100644 --- a/compiler/src/compilerExamples/InlineAssemblyMacro.v +++ b/compiler/src/compilerExamples/InlineAssemblyMacro.v @@ -1,4 +1,4 @@ -Require Import Coq.ZArith.ZArith. +From Coq Require Import ZArith. Require Import compiler.util.Common. Require Import riscv.Utility.Monads. Require Import coqutil.Map.SortedList. diff --git a/compiler/src/compilerExamples/swap.v b/compiler/src/compilerExamples/swap.v index ae8662f8..9c2ac0e9 100644 --- a/compiler/src/compilerExamples/swap.v +++ b/compiler/src/compilerExamples/swap.v @@ -1,4 +1,4 @@ -Require Import Coq.Lists.List. +From Coq Require Import List. Import ListNotations. Require bedrock2Examples.Demos. Require Import coqutil.Decidable. diff --git a/end2end/src/end2end/Bedrock2SemanticsForKami.v b/end2end/src/end2end/Bedrock2SemanticsForKami.v index 23972350..20e6d04d 100644 --- a/end2end/src/end2end/Bedrock2SemanticsForKami.v +++ b/end2end/src/end2end/Bedrock2SemanticsForKami.v @@ -1,4 +1,4 @@ -Require Import Coq.ZArith.ZArith. +From Coq Require Import ZArith. Require Import bedrock2.Syntax bedrock2.Semantics. Require coqutil.Datatypes.String coqutil.Map.SortedList coqutil.Map.SortedListString. Require Import coqutil.Word.Interface coqutil.Map.SortedListWord. diff --git a/end2end/src/end2end/End2EndLightbulb.v b/end2end/src/end2end/End2EndLightbulb.v index e1437e21..b506707e 100644 --- a/end2end/src/end2end/End2EndLightbulb.v +++ b/end2end/src/end2end/End2EndLightbulb.v @@ -1,6 +1,6 @@ -Require Import Coq.ZArith.ZArith. -Require Import Coq.Strings.String. -Require Import Coq.Lists.List. Import ListNotations. +From Coq Require Import ZArith. +From Coq Require Import String. +From Coq Require Import List. Import ListNotations. Require Import coqutil.Word.Interface coqutil.Word.Bitwidth32. Require Import coqutil.Map.Interface. Require Import coqutil.Tactics.forward. diff --git a/end2end/src/end2end/End2EndPipeline.v b/end2end/src/end2end/End2EndPipeline.v index dcb547d6..aa4cb141 100644 --- a/end2end/src/end2end/End2EndPipeline.v +++ b/end2end/src/end2end/End2EndPipeline.v @@ -1,8 +1,8 @@ Require Import String. -Require Import Coq.ZArith.ZArith. +From Coq Require Import ZArith. Require Import coqutil.Z.Lia. -Require Import Coq.Lists.List. Import ListNotations. -Require Import Coq.Logic.FunctionalExtensionality. +From Coq Require Import List. Import ListNotations. +From Coq Require Import FunctionalExtensionality. Require Import riscv.Utility.Encode. Require Import riscv.Utility.Utility. Require Import coqutil.Word.LittleEndian. @@ -47,7 +47,7 @@ Require Import compiler.ExprImpEventLoopSpec. Local Open Scope Z_scope. -Require Import Coq.Classes.Morphisms. +From Coq Require Import Morphisms. #[global] Instance word_riscv_ok: @RiscvWordProperties.word.riscv_ok 32 KamiWord.wordW. refine (@KamiRiscvWordProperties.kami_word_riscv_ok 5 _ _). diff --git a/end2end/src/end2end/KamiRiscvWordProperties.v b/end2end/src/end2end/KamiRiscvWordProperties.v index 5f18e036..f52ba1fd 100644 --- a/end2end/src/end2end/KamiRiscvWordProperties.v +++ b/end2end/src/end2end/KamiRiscvWordProperties.v @@ -1,4 +1,4 @@ -Require Import Coq.ZArith.ZArith. +From Coq Require Import ZArith. Require Import coqutil.Word.Interface coqutil.Word.Properties. Require Import coqutil.Z.BitOps. Require Import coqutil.Z.Lia. diff --git a/end2end/src/end2end/PrintAdmits.v b/end2end/src/end2end/PrintAdmits.v index c7caca86..cb16653b 100644 --- a/end2end/src/end2end/PrintAdmits.v +++ b/end2end/src/end2end/PrintAdmits.v @@ -1,5 +1,5 @@ -Require Import Coq.ZArith.ZArith. -Require Import Coq.Strings.String. +From Coq Require Import ZArith. +From Coq Require Import String. Require end2end.End2EndLightbulb. Open Scope Z_scope. Open Scope string_scope. diff --git a/end2end/src/end2end/RelyNotations.v b/end2end/src/end2end/RelyNotations.v index 66ab05d8..2a276da7 100644 --- a/end2end/src/end2end/RelyNotations.v +++ b/end2end/src/end2end/RelyNotations.v @@ -1,5 +1,5 @@ -Require Import Coq.Lists.List. -Require Import Coq.ZArith.ZArith. +From Coq Require Import List. +From Coq Require Import ZArith. Require Import coqutil.Word.Naive coqutil.Word.Interface. Require Import coqutil.Datatypes.List. Require Import bedrock2.ReversedListNotations. diff --git a/processor/src/processor/Consistency.v b/processor/src/processor/Consistency.v index 2f812a46..0d82449a 100644 --- a/processor/src/processor/Consistency.v +++ b/processor/src/processor/Consistency.v @@ -1,8 +1,8 @@ Require Import String BinInt. -Require Import Coq.ZArith.ZArith. +From Coq Require Import ZArith. Require Import coqutil.Z.Lia. Require Import coqutil.Byte. -Require Import Coq.Lists.List. Import ListNotations. +From Coq Require Import List. Import ListNotations. Require Import Kami.Lib.Word. Require Import Kami.Syntax Kami.Semantics. Require Import Kami.Ex.IsaRv32. diff --git a/processor/src/processor/KamiProc.v b/processor/src/processor/KamiProc.v index d0706287..6ac471bb 100644 --- a/processor/src/processor/KamiProc.v +++ b/processor/src/processor/KamiProc.v @@ -1,6 +1,6 @@ Require Import String. -Require Import Coq.ZArith.ZArith. -Require Import Coq.Lists.List. Import ListNotations. +From Coq Require Import ZArith. +From Coq Require Import List. Import ListNotations. Require Import coqutil.Z.Lia. diff --git a/processor/src/processor/KamiRiscv.v b/processor/src/processor/KamiRiscv.v index 8b093d50..1485f3b2 100644 --- a/processor/src/processor/KamiRiscv.v +++ b/processor/src/processor/KamiRiscv.v @@ -1,7 +1,7 @@ Require Import String. -Require Import Coq.ZArith.ZArith. +From Coq Require Import ZArith. Require Import coqutil.Z.Lia. -Require Import Coq.Lists.List. Import ListNotations. +From Coq Require Import List. Import ListNotations. Require Import Kami.Lib.Word. Require Import Kami.Ex.IsaRv32 riscv.Spec.Decode. Require Import riscv.Utility.Encode. diff --git a/processor/src/processor/KamiRiscvStep.v b/processor/src/processor/KamiRiscvStep.v index 389946f4..cb59711a 100644 --- a/processor/src/processor/KamiRiscvStep.v +++ b/processor/src/processor/KamiRiscvStep.v @@ -1,7 +1,7 @@ Require Import String. -Require Import Coq.ZArith.ZArith. +From Coq Require Import ZArith. Require Import coqutil.Z.Lia. -Require Import Coq.Lists.List. Import ListNotations. +From Coq Require Import List. Import ListNotations. Require Import Kami.Lib.Word. Require Import Kami.Ex.IsaRv32 riscv.Spec.Decode. Require Import riscv.Utility.Encode. diff --git a/processor/src/processor/KamiWord.v b/processor/src/processor/KamiWord.v index cae6a66f..5aa9c252 100644 --- a/processor/src/processor/KamiWord.v +++ b/processor/src/processor/KamiWord.v @@ -1,4 +1,5 @@ -Require Import Coq.ZArith.ZArith Coq.ZArith.BinIntDef Coq.ZArith.BinInt coqutil.Z.Lia. +From Coq Require Import ZArith BinIntDef BinInt. +Require Import coqutil.Z.Lia. Require Import coqutil.sanity coqutil.Tactics.forward coqutil.Word.Interface. Import word. Require Import Kami.Lib.Word. Require riscv.Utility.Utility.