gistfile1.txt

find . -name '*.v' | grep -v coqutil | grep -v xamples | xargs grep 'LittleEndian\.' | tee /tmp/LittleEndian.txt | less

./src/Bedrock/Field/Synthesis/Generic/Bignum.v:      (fun c => word.of_Z (LittleEndian.combine _ (HList.tuple.of_list c))).
./src/Bedrock/Field/Synthesis/Generic/Bignum.v:      (fun w => HList.tuple.to_list (LittleEndian.split (Z.to_nat k) (word.unsigned w))).
./src/Bedrock/Field/Synthesis/Generic/Bignum.v:        rewrite ?LittleEndian.combine_split; try exact eq_refl;
./src/Bedrock/Field/Common/Util.v:             (LittleEndian.split (Z.to_nat bytes_per_word)
./src/Bedrock/Field/Common/Util.v:                                (LittleEndian.combine
./src/Bedrock/Field/Common/Util.v:      |- context [word.wrap (LittleEndian.combine ?n ?t)] =>
./src/Bedrock/Field/Common/Util.v:      pose proof LittleEndian.combine_bound t as H;
./src/Bedrock/Field/Common/Util.v:    rewrite LittleEndian.split_combine.
./rupicola/bedrock2/end2end/src/end2end/End2EndPipeline.v:Require Import coqutil.Word.LittleEndian.
./rupicola/bedrock2/compiler/src/compiler/FlatToRiscvCommon.v:      rewrite LittleEndian.combine_split.
./rupicola/bedrock2/compiler/src/compiler/FlatToRiscvCommon.v:    rewrite bitSlice_all_nonneg. 2: cbv; discriminate. 2: apply (@LittleEndian.combine_bound 4).
./rupicola/bedrock2/compiler/src/compiler/FlatToRiscvCommon.v:    rewrite LittleEndian.split_combine.
./rupicola/bedrock2/compiler/src/compiler/FlatToRiscvCommon.v:    apply (@LittleEndian.combine_bound 4).
./rupicola/bedrock2/compiler/src/compiler/Softmul.v:    rewrite LittleEndian.combine_split. rewrite word.unsigned_of_Z_nowrap. 2: apply encode_range.
./rupicola/bedrock2/compiler/src/compiler/RunInstruction.v:                  (word.of_Z (opt_sign_extender (LittleEndian.combine n v))) /\
./rupicola/bedrock2/compiler/src/compiler/RunInstruction.v:         ptsto_bytes n addr (LittleEndian.split n (word.unsigned v_new)) * R)%sep
./rupicola/bedrock2/compiler/src/compiler/SpillingUniqueSepLog.v:                               (LittleEndian.split (@Memory.bytes_per width sz) (word.unsigned value))
./rupicola/bedrock2/compiler/src/compiler/CompilerInvariant.v:      HList.tuple.to_list (LittleEndian.split 4 (encode instr)) ++ instrencode instrs.
./rupicola/bedrock2/compiler/src/compiler/SeparationLogic.v:       HList.tuple.to_list (LittleEndian.split (Z.to_nat bytes_per_word) (word.unsigned x)))
./rupicola/bedrock2/compiler/src/compiler/SeparationLogic.v:    1: unshelve setoid_rewrite LittleEndian.split_combine.
./rupicola/bedrock2/compiler/src/compiler/SeparationLogic.v:    match goal with |- context[LittleEndian.combine _ ?xs] => generalize xs end.
./rupicola/bedrock2/compiler/src/compiler/SeparationLogic.v:    pose proof (LittleEndian.combine_bound t).
./rupicola/bedrock2/compiler/src/compiler/GoFlatToRiscv.v:    - rewrite LittleEndian.combine_split.
./rupicola/bedrock2/compiler/src/compiler/UniqueSepLog.v:    bytes addr (LittleEndian.split (@Memory.bytes_per width sz) (word.unsigned value)).
./rupicola/bedrock2/compiler/src/compiler/LowerPipeline.v:        exists (List.flat_map (fun x => HList.tuple.to_list (LittleEndian.split (Z.to_nat bytes_per_word) (word.unsigned x))) stack_trash).
./rupicola/bedrock2/compiler/src/compiler/Pipeline.v:    List.flat_map (fun inst => HList.tuple.to_list (LittleEndian.split 4 (encode inst))) p.
./rupicola/bedrock2/compiler/src/compiler/FlatToRiscvDef.v:    InvalidInstruction (LittleEndian.combine 4 (HList.tuple.of_list [
./rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricRiscvMachine.v:Require Import coqutil.Word.LittleEndian.
./rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricMinimalMMIO.v:  Arguments LittleEndian.combine: simpl never.
./rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalMMIO.v:    word.of_Z (BitOps.signExtend (8 * Z.of_nat n) (LittleEndian.combine n v)).
./rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/LogInstructionTrace.v:               | Some i => LittleEndian.combine 4 i
./rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalMMIO_Post.v:    word.of_Z (BitOps.signExtend (8 * Z.of_nat n) (LittleEndian.combine n v)).
./rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/RiscvMachine.v:Require Import coqutil.Word.LittleEndian.
./rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/RiscvMachine.v:      List.flat_map (fun z => HList.tuple.to_list (LittleEndian.split 4 z)) l.
./rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/Run.v:Require Import coqutil.Word.LittleEndian.
./rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/MkMachineWidth.v:Require Import coqutil.Word.LittleEndian.
./rupicola/bedrock2/bedrock2/src/bedrock2/Scalars.v:Require Import coqutil.Map.Interface bedrock2.Map.Separation bedrock2.Map.SeparationLogic bedrock2.Lift1Prop bedrock2.Array coqutil.Word.LittleEndian.
./rupicola/bedrock2/bedrock2/src/bedrock2/Scalars.v:    ptsto_bytes n addr (LittleEndian.split n value).
./rupicola/bedrock2/bedrock2/src/bedrock2/Scalars.v:    rewrite LittleEndian.combine_split.
./rupicola/bedrock2/bedrock2/src/bedrock2/Scalars.v:    cbv [LittleEndian.combine PrimitivePair.pair._1].
./rupicola/bedrock2/bedrock2/src/bedrock2/Scalars.v:    cbv [LittleEndian.split].
./rupicola/bedrock2/bedrock2/src/bedrock2/Scalars.v:                   (scalar16 a (word.of_Z (LittleEndian.combine _ (HList.tuple.of_list l)))).
./rupicola/bedrock2/bedrock2/src/bedrock2/Scalars.v:    { erewrite LittleEndian.split_combine; exact eq_refl. }
./rupicola/bedrock2/bedrock2/src/bedrock2/Scalars.v:    erewrite <-(LittleEndian.split_combine _ (HList.tuple.of_list (x :: x0 :: nil)%list)).
./rupicola/bedrock2/bedrock2/src/bedrock2/Scalars.v:    erewrite LittleEndian.combine_split.
./rupicola/bedrock2/bedrock2/src/bedrock2/Scalars.v:                   (scalar32 a (word.of_Z (LittleEndian.combine _ (HList.tuple.of_list l)))).
./rupicola/bedrock2/bedrock2/src/bedrock2/Scalars.v:    { erewrite LittleEndian.split_combine; exact eq_refl. }
./rupicola/bedrock2/bedrock2/src/bedrock2/Scalars.v:    erewrite <-(LittleEndian.split_combine _ (HList.tuple.of_list (x :: x0 :: x1 :: x2 :: nil)%list)).
./rupicola/bedrock2/bedrock2/src/bedrock2/Scalars.v:    erewrite LittleEndian.combine_split.
./rupicola/bedrock2/bedrock2/src/bedrock2/Scalars.v:                   (scalar a (word.of_Z (LittleEndian.combine _ (HList.tuple.of_list l)))).
./rupicola/bedrock2/bedrock2/src/bedrock2/Scalars.v:    { erewrite LittleEndian.split_combine.
./rupicola/bedrock2/bedrock2/src/bedrock2/Scalars.v:    apply LittleEndian.combine_bound.
./rupicola/bedrock2/bedrock2/src/bedrock2/Scalars.v:    load access_size.four m a = Some (word.of_Z (LittleEndian.combine _ (HList.tuple.of_list bs))).
./rupicola/bedrock2/bedrock2/src/bedrock2/Scalars.v:    rewrite (Z.mod_small (LittleEndian.combine (length bs) (tuple.of_list bs)) (2 ^ width)). 2: {
./rupicola/bedrock2/bedrock2/src/bedrock2/Scalars.v:      - eapply LittleEndian.combine_bound.
./rupicola/bedrock2/bedrock2/src/bedrock2/Scalars.v:    - eapply LittleEndian.combine_bound.
./rupicola/bedrock2/bedrock2/src/bedrock2/Scalars.v:    load access_size.four m a = Some (word.of_Z (LittleEndian.combine _ (HList.tuple.of_list bs))).
./rupicola/bedrock2/bedrock2/src/bedrock2/Scalars.v:    load access_size.four m a = Some (word.of_Z (LittleEndian.combine _ (HList.tuple.of_list bs))).
./rupicola/bedrock2/bedrock2/src/bedrock2/Memory.v:Require Import BinIntDef coqutil.Word.Interface coqutil.Word.LittleEndian.
./rupicola/bedrock2/bedrock2/src/bedrock2/Memory.v:    | Some bs => Some (LittleEndian.combine _ bs)
./rupicola/bedrock2/bedrock2/src/bedrock2/Memory.v:    store_bytes (bytes_per sz) m a (LittleEndian.split _ v).
./rupicola/bedrock2/processor/src/processor/KamiRiscv.v:Require Import coqutil.Word.LittleEndian.
./rupicola/bedrock2/processor/src/processor/Consistency.v:Require Import coqutil.Word.LittleEndian.
./rupicola/bedrock2/processor/src/processor/KamiRiscvStep.v:Require Import coqutil.Word.LittleEndian.
./rupicola/bedrock2/processor/src/processor/KamiRiscvStep.v:    word.of_Z (BitOps.signExtend (8 * Z.of_nat n) (LittleEndian.combine n v)).