From 06018b7af3bbc1479e98b60a71def624882f1ef5 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Fri, 8 Apr 2022 11:26:09 -0400 Subject: [PATCH] try out SepCallsand ZnWords in lightbulb.v (#244) --- bedrock2/src/bedrock2/SepAuto.v | 32 ++--- bedrock2/src/bedrock2/SepAutoArray.v | 11 +- bedrock2/src/bedrock2/SepAutoExports.v | 17 +++ bedrock2/src/bedrock2/SepCalls.v | 32 +++-- bedrock2/src/bedrock2/SepCallsExports.v | 16 +++ .../bedrock2Examples/LiveVerif/LiveVerif.v | 2 +- .../src/bedrock2Examples/LiveVerif/swap.v | 2 +- .../src/bedrock2Examples/SepAutoArrayTests.v | 13 +- bedrock2/src/bedrock2Examples/lightbulb.v | 111 +++++++----------- compiler/src/compilerExamples/Softmul.v | 2 +- .../src/compilerExamples/SoftmulBedrock2.v | 2 +- .../src/compilerExamples/SoftmulCompile.v | 2 +- 12 files changed, 124 insertions(+), 118 deletions(-) create mode 100644 bedrock2/src/bedrock2/SepAutoExports.v create mode 100644 bedrock2/src/bedrock2/SepCallsExports.v diff --git a/bedrock2/src/bedrock2/SepAuto.v b/bedrock2/src/bedrock2/SepAuto.v index 7ba5553f7..150803f94 100644 --- a/bedrock2/src/bedrock2/SepAuto.v +++ b/bedrock2/src/bedrock2/SepAuto.v @@ -6,22 +6,22 @@ undo the `Ltac fwd_rewrites ::= fwd_rewrite_db_in_star.` patching, so `fwd` and tactics using `fwd` will do fewer simplifications than intended *) -Require Export Coq.ZArith.ZArith. Open Scope Z_scope. (* TODO remove *) -Require Export coqutil.Byte. -Require Export coqutil.Datatypes.Inhabited. -Require Export coqutil.Tactics.Tactics. -Require Export coqutil.Tactics.autoforward. -Require Export coqutil.Map.Interface coqutil.Map.Properties coqutil.Map.OfListWord. -Require Export coqutil.Word.Interface coqutil.Word.Properties. -Require Export coqutil.Tactics.fwd. -Require Export bedrock2.Lift1Prop. -Require Export bedrock2.Map.Separation bedrock2.Map.SeparationLogic. +Require Import Coq.ZArith.ZArith. Open Scope Z_scope. (* TODO remove *) +Require Import coqutil.Byte. +Require Import coqutil.Datatypes.Inhabited. +Require Import coqutil.Tactics.Tactics. +Require Import coqutil.Tactics.autoforward. +Require Import coqutil.Map.Interface coqutil.Map.Properties coqutil.Map.OfListWord. +Require Import coqutil.Word.Interface coqutil.Word.Properties. +Require Import coqutil.Tactics.fwd. +Require Import bedrock2.Lift1Prop. +Require Import bedrock2.Map.Separation bedrock2.Map.SeparationLogic. Require Import bedrock2.Array. -Require Export bedrock2.ZnWords. -Require Export bedrock2.WordSimpl. -Export List.ListNotations. Open Scope list_scope. (* TODO remove *) -Require Export bedrock2.SepCalls. -Require Export bedrock2.TransferSepsOrder. +Require Import bedrock2.ZnWords. +Require Import bedrock2.WordSimpl. +Import List.ListNotations. Open Scope list_scope. (* TODO remove *) +Require Import bedrock2.SepCalls. +Require Import bedrock2.TransferSepsOrder. Ltac fwd_rewrites ::= fwd_rewrite_db_in_star. @@ -37,6 +37,6 @@ but if t2 is a match and not prefixed with idtac, it's evaluated too early *) Ltac after_mem_modifying_lemma := scancel_asm; match goal with - | _: tactic_error _ |- _ => idtac + | _: bedrock2.TacticError.tactic_error _ |- _ => idtac | |- _ => intro_new_mem; transfer_sep_order end. diff --git a/bedrock2/src/bedrock2/SepAutoArray.v b/bedrock2/src/bedrock2/SepAutoArray.v index d30fed794..47d62fd36 100644 --- a/bedrock2/src/bedrock2/SepAutoArray.v +++ b/bedrock2/src/bedrock2/SepAutoArray.v @@ -1,10 +1,13 @@ -Require Import Coq.Logic.FunctionalExtensionality. -Require Import Coq.Logic.PropExtensionality. +Require Import Coq.ZArith.BinInt. +Require Import Coq.Init.Byte. +Require Import coqutil.Word.Bitwidth. +Require Import coqutil.Tactics.rewr. +Require Import coqutil.Map.Interface. Require Import bedrock2.SepAuto. Require Import bedrock2.Array. Require Import bedrock2.groundcbv. -Require Import coqutil.Word.Bitwidth. -Require Import coqutil.Tactics.rewr. +Require Import bedrock2.TransferSepsOrder. +Require Import bedrock2.SepCalls. Section SepLog. Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word byte}. diff --git a/bedrock2/src/bedrock2/SepAutoExports.v b/bedrock2/src/bedrock2/SepAutoExports.v new file mode 100644 index 000000000..47a56524c --- /dev/null +++ b/bedrock2/src/bedrock2/SepAutoExports.v @@ -0,0 +1,17 @@ +Require Export Coq.ZArith.ZArith. Open Scope Z_scope. (* TODO remove *) +Require Export coqutil.Byte. +Require Export coqutil.Datatypes.Inhabited. +Require Export coqutil.Tactics.Tactics. +Require Export coqutil.Tactics.autoforward. +Require Export coqutil.Map.Interface coqutil.Map.Properties coqutil.Map.OfListWord. +Require Export coqutil.Word.Interface coqutil.Word.Properties. +Require Export coqutil.Tactics.fwd. +Require Export bedrock2.Lift1Prop. +Require Export bedrock2.Map.Separation bedrock2.Map.SeparationLogic. +Require Export bedrock2.ZnWords. +Require Export bedrock2.WordSimpl. +Export List.ListNotations. Open Scope list_scope. (* TODO remove *) +Require Export bedrock2.SepCallsExports. +Require Export bedrock2.TransferSepsOrder. + +Require Export bedrock2.SepAuto. diff --git a/bedrock2/src/bedrock2/SepCalls.v b/bedrock2/src/bedrock2/SepCalls.v index 13fd862b3..7cf10386d 100644 --- a/bedrock2/src/bedrock2/SepCalls.v +++ b/bedrock2/src/bedrock2/SepCalls.v @@ -7,34 +7,32 @@ Applying the call lemma is not handled by this file, but solving the above conjunction (except for solving finalPost) is. *) -Require Export Coq.ZArith.ZArith. Open Scope Z_scope. +Require Import Coq.ZArith.ZArith. Open Scope Z_scope. Require Import coqutil.Z.Lia. -Require Export coqutil.Byte. +Require Import coqutil.Byte. Require Import coqutil.Datatypes.HList. Require Import coqutil.Datatypes.PropSet. -Require Export coqutil.Datatypes.Inhabited. +Require Import coqutil.Datatypes.Inhabited. Require Import coqutil.Tactics.rewr coqutil.Tactics.rdelta. Require Import Coq.Program.Tactics. Require Import coqutil.Macros.symmetry. -Require Export coqutil.Tactics.Tactics. -Require Export coqutil.Tactics.autoforward. -Require Export coqutil.Map.Interface coqutil.Map.Properties coqutil.Map.OfListWord. -Require Export coqutil.Word.Interface coqutil.Word.Properties. +Require Import coqutil.Tactics.Tactics. +Require Import coqutil.Tactics.autoforward. +Require Import coqutil.Map.Interface coqutil.Map.Properties coqutil.Map.OfListWord. +Require Import coqutil.Word.Interface coqutil.Word.Properties. Require Import coqutil.Sorting.OrderToPermutation. -Require Export coqutil.Tactics.fwd. +Require Import coqutil.Tactics.fwd. Require Import coqutil.Tactics.ltac_list_ops. -Require Export bedrock2.Lift1Prop. -Require Export bedrock2.Map.Separation bedrock2.Map.SeparationLogic. +Require Import bedrock2.Lift1Prop. +Require Import bedrock2.Map.Separation bedrock2.Map.SeparationLogic. Require Import bedrock2.Array. -Require Export bedrock2.ZnWords. +Require Import bedrock2.ZnWords. Require Import bedrock2.ptsto_bytes bedrock2.Scalars. Require Import bedrock2.groundcbv. -Require Export bedrock2.TacticError. +Require Import bedrock2.TacticError. Require Import bedrock2.ident_to_string. -Require Export Coq.Strings.String. Open Scope string_scope. -(* exporting String because otherwise error messages will be displayed as - (String.String (Ascii.Ascii false false true false true false true false) ...) *) -Require Export Coq.Lists.List. (* to make sure `length` refers to list rather than 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 *) Import List.ListNotations. Open Scope list_scope. Section SepLog. @@ -238,7 +236,7 @@ Ltac use_sep_asm := end. Ltac impl_ecancel := - repeat (impl_ecancel_step_without_splitting || impl_ecancel_step_with_splitting). + repeat (impl_ecancel_step_with_splitting || impl_ecancel_step_without_splitting ). Ltac finish_impl_ecancel := lazymatch goal with diff --git a/bedrock2/src/bedrock2/SepCallsExports.v b/bedrock2/src/bedrock2/SepCallsExports.v new file mode 100644 index 000000000..9394ed865 --- /dev/null +++ b/bedrock2/src/bedrock2/SepCallsExports.v @@ -0,0 +1,16 @@ +Require Export Coq.ZArith.ZArith. Open Scope Z_scope. +Require Export coqutil.Byte. +Require Export coqutil.Datatypes.Inhabited. +Require Export coqutil.Tactics.Tactics. +Require Export coqutil.Tactics.autoforward. +Require Export coqutil.Map.Interface coqutil.Map.Properties coqutil.Map.OfListWord. +Require Export coqutil.Word.Interface coqutil.Word.Properties. +Require Export coqutil.Tactics.fwd. +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 *) + +Require Export bedrock2.SepCalls. diff --git a/bedrock2/src/bedrock2Examples/LiveVerif/LiveVerif.v b/bedrock2/src/bedrock2Examples/LiveVerif/LiveVerif.v index 1015f722d..d2efca116 100644 --- a/bedrock2/src/bedrock2Examples/LiveVerif/LiveVerif.v +++ b/bedrock2/src/bedrock2Examples/LiveVerif/LiveVerif.v @@ -20,7 +20,7 @@ Require coqutil.Datatypes.String coqutil.Map.SortedList coqutil.Map.SortedListSt Require Import bedrock2Examples.LiveVerif.string_to_ident. Require Import bedrock2.ident_to_string. Require Import bedrock2.SepBulletPoints. -Require Import bedrock2.SepAutoArray bedrock2.SepAuto. +Require Import bedrock2.SepAutoArray bedrock2.SepAutoExports. Require Import bedrock2.OperatorOverloading. Notation "/[ x ]" := (word.of_Z x) (* squeeze a Z into a word (beat it with a / to make it smaller) *) diff --git a/bedrock2/src/bedrock2Examples/LiveVerif/swap.v b/bedrock2/src/bedrock2Examples/LiveVerif/swap.v index 082cc6c68..c257a59db 100644 --- a/bedrock2/src/bedrock2Examples/LiveVerif/swap.v +++ b/bedrock2/src/bedrock2Examples/LiveVerif/swap.v @@ -23,7 +23,7 @@ Require Import Coq.Strings.String. Require Import bedrock2.TacticError. Require Import bedrock2Examples.LiveVerif.string_to_ident. Require Import bedrock2.ident_to_string. -Require Import bedrock2.SepAutoArray bedrock2.SepAuto. +Require Import bedrock2.SepAutoArray bedrock2.SepAutoExports. Require Import bedrock2.OperatorOverloading. Local Open Scope oo_scope. Close Scope sepcl_scope. diff --git a/bedrock2/src/bedrock2Examples/SepAutoArrayTests.v b/bedrock2/src/bedrock2Examples/SepAutoArrayTests.v index 867aee616..196b72da2 100644 --- a/bedrock2/src/bedrock2Examples/SepAutoArrayTests.v +++ b/bedrock2/src/bedrock2Examples/SepAutoArrayTests.v @@ -1,9 +1,12 @@ +Require Import Coq.ZArith.ZArith. Require Import Coq.micromega.Lia. Require Import coqutil.Word.Bitwidth32. Require Import bedrock2.Array. -Require Import bedrock2.SepAutoArray bedrock2.SepAuto. +Require Import bedrock2.SepCalls bedrock2.SepAutoArray bedrock2.SepAuto. Close Scope list_scope. Close Scope Z_scope. (* TODO *) -Require Import bedrock2.OperatorOverloading. Local Open Scope oo_scope. +Require Import bedrock2.TransferSepsOrder. +Require Import coqutil.Map.Interface. +Require Import coqutil.Datatypes.OperatorOverloading bedrock2.OperatorOverloading. Local Open Scope oo_scope. Require Import bedrock2.ListIndexNotations. Local Open Scope list_index_scope. Require Import bedrock2.SepBulletPoints. Local Open Scope sep_bullets_scope. @@ -76,11 +79,11 @@ Section WithParameters. Context (sample_call: word -> word -> cmd). - Hypothesis sample_call_correct: forall m a1 n (vs: list word) R (post: mem -> Prop), + Hypothesis sample_call_correct: forall (m : mem) (a1 n : word) (vs: list word) (R post: mem -> Prop), sep (a1 :-> vs : word_array) R m /\ List.length vs = Z.to_nat (word.unsigned n) /\ - (forall m', - sep (a1 :-> vs[5 := vs[5] * (word.of_Z (word := word) 2)] : word_array) R m' -> + (forall m':mem, + sep (a1 :-> vs[5 := vs[5%nat] * (word.of_Z (word := word) 2)] : word_array) R m' -> post m') -> wp (sample_call a1 n) m post. diff --git a/bedrock2/src/bedrock2Examples/lightbulb.v b/bedrock2/src/bedrock2Examples/lightbulb.v index acaecc872..ede90b351 100644 --- a/bedrock2/src/bedrock2Examples/lightbulb.v +++ b/bedrock2/src/bedrock2Examples/lightbulb.v @@ -376,12 +376,14 @@ Section WithParameters. morphism (Properties.word.ring_morph (word := word)), constants [Properties.word_cst]). + Require Import bedrock2.ZnWords. + Require Import bedrock2.SepAutoArray bedrock2.SepCalls. + Lemma recvEthernet_ok : program_logic_goal_for_function! recvEthernet. Proof. straightline. rename H into Hcall; clear H0 H1. rename H2 into H. rename H3 into H0. - repeat (straightline || split_if || straightline_call || eauto 99 || prove_ext_spec). - 1, 3: rewrite word.unsigned_of_Z; cbv - [Z.le Z.lt]; clear; blia. + repeat (straightline || split_if || straightline_call || eauto 99 || prove_ext_spec || ZnWords). 3: { @@ -391,7 +393,7 @@ Section WithParameters. (fun v scratch R t m buf num_bytes_loop i read err => PrimitivePair.pair.mk ( word.unsigned err = 0 /\ word.unsigned i <= word.unsigned num_bytes /\ v = word.unsigned i /\ (bytes (word.add buf i) scratch * R) m /\ - Z.of_nat (List.length scratch) = word.unsigned (word.sub num_bytes i) /\ + List.length scratch = Z.to_nat (word.unsigned (word.sub num_bytes i)) /\ word.unsigned i mod 4 = word.unsigned num_bytes mod 4 /\ num_bytes_loop = num_bytes) (fun T M BUF NUM_BYTES I READ ERR => @@ -411,26 +413,18 @@ Section WithParameters. List.repeat Datatypes.length HList.polymorphic_list.repeat HList.polymorphic_list.length PrimitivePair.pair._1 PrimitivePair.pair._2] in *; - repeat (straightline || split_if || eapply interact_nomem || eauto 99). + [ repeat (straightline || split_if || eapply interact_nomem || eauto 99) .. | ]. { exact (Z.gt_wf (word.unsigned num_bytes)). } - 1: repeat (refine (conj _ _)); eauto. - { subst i. rewrite word.unsigned_of_Z. - eapply Properties.word.unsigned_range. } - 1: zify_unsigned. - 1: replace (word.add p_addr i) with p_addr by (subst i; ring). - 1: rewrite <- (List.firstn_skipn (Z.to_nat (word.unsigned (word.sub num_bytes i) ) ) _) in H. - 1: SeparationLogic.seprewrite_in (symmetry! @bytearray_index_merge) H; [|ecancel_assumption]. - 1,2,3: - repeat match goal with - | |- ?x = ?x => exact (eq_refl x) - | _ => progress trans_ltu - | _ => progress zify_unsigned - | _ => progress rewrite ?Znat.Z2Nat.id by blia - | H: _ |- _ => progress (rewrite ?Znat.Z2Nat.id in H by blia) - | _ => rewrite List.length_firstn_inbounds by blia - | _ => progress rewrite ?Z.sub_0_r - end; repeat straightline. - { repeat match goal with x:= _ |- context[?x] => subst x end. clear. Z.div_mod_to_equations. blia. } + + { + repeat (split; [trivial||ZnWords|]). + replace (word.add p_addr i) with p_addr by (subst i; ring). + progress trans_ltu. + + scancel_asm. + Tactics.ssplit. + all : trivial; try listZnWords. + } { straightline_call; repeat straightline. { rewrite word.unsigned_of_Z. cbv; clear. intuition congruence. } @@ -492,34 +486,11 @@ Section WithParameters. { replace (word.add x9 i) with (word.add (word.add x9 x11) (word.of_Z 4)) by (subst i; ring). ecancel_assumption. } - { repeat match goal with x1 := _ |- _ => subst x1; rewrite List.length_skipn; rewrite Znat.Nat2Z.inj_sub end. - { repeat match goal with H5:_|-_=>rewrite H5 end; subst i. - progress replace (word.sub num_bytes (word.add x11 (word.of_Z 4))) - with (word.sub (word.sub num_bytes x11) (word.of_Z 4)) by ring. - rewrite (word.unsigned_sub _ (word.of_Z 4)). - unfold word.wrap. rewrite Z.mod_small. - all: replace (word.unsigned (word.of_Z 4)) with 4 by (rewrite word.unsigned_of_Z; exact eq_refl). - all: change (Z.of_nat 4) with 4. - all : Z.div_mod_to_equations; blia. } - Z.div_mod_to_equations; blia. } - { subst i. - rewrite word.unsigned_add. unfold word.wrap. rewrite (Z.mod_small _ (2 ^ 32)). - { revert dependent x11. clear -word_ok. - replace (word.unsigned (word.of_Z 4)) with 4 by (rewrite word.unsigned_of_Z; exact eq_refl). - intros. - Z.div_mod_to_equations. blia. } - replace (word.unsigned (word.of_Z 4)) with 4 by (rewrite word.unsigned_of_Z; exact eq_refl). - Z.div_mod_to_equations. - blia. } - { repeat match goal with |- context [?x] => is_var x; subst x end. - rewrite word.unsigned_add. unfold word.wrap. rewrite Z.mod_small. - { replace (word.unsigned (word.of_Z 4)) with 4 by (rewrite word.unsigned_of_Z; exact eq_refl). blia. } - replace (word.unsigned (word.of_Z 4)) with 4 by (rewrite word.unsigned_of_Z; exact eq_refl). - Z.div_mod_to_equations. blia. } - { subst v'. subst i. - rewrite word.unsigned_add. - replace (word.unsigned (word.of_Z 4)) with 4 by (rewrite word.unsigned_of_Z; exact eq_refl). - unfold word.wrap. rewrite (Z.mod_small _ (2 ^ 32)); Z.div_mod_to_equations; blia. } + { match goal with x1 := _ |- _ => subst x1; rewrite List.length_skipn end. + ZnWords. } + { ZnWords. } + { ZnWords. } + { ZnWords. } { letexists; repeat split. { repeat match goal with x := _ |- _ => is_var x; subst x end; subst. @@ -556,13 +527,10 @@ Section WithParameters. rewrite H13. subst br. rewrite word.unsigned_ltu in H11. - destruct (word.unsigned x11 rewrite H; intro HX; solve[inversion HX] end. } { trans_ltu; replace (word.unsigned (word.of_Z 1521)) with 1521 in * by (rewrite word.unsigned_of_Z; exact eq_refl). + replace (Z.to_nat (word.unsigned (word.sub p_addr p_addr) / 1)) with O in * by ZnWords. + all : cbn [seps array List.firstn List.skipn] in *. eexists _; split; eauto; repeat split; try blia. { SeparationLogic.seprewrite_in @bytearray_index_merge H10. - { rewrite H11. - 1: replace (word.sub num_bytes (word.of_Z 0)) with num_bytes by ring. - rewrite List.length_firstn_inbounds, ?Znat.Z2Nat.id. - 1:exact eq_refl. - 1:eapply word.unsigned_range. - rewrite ?Znat.Z2Nat.id by eapply word.unsigned_range. - blia. } + { rewrite H11, List.firstn_length. ZnWords. } eassumption. } { 1:rewrite List.app_length, List.length_skipn, H11, List.firstn_length. replace (word.sub num_bytes (word.of_Z 0)) with num_bytes by ring. - enough (Z.to_nat (word.unsigned num_bytes) <= length buf)%nat by blia. + enough (Z.to_nat (word.unsigned num_bytes) <= length buf)%nat by ZnWords. rewrite ?Znat.Z2Nat.id by eapply word.unsigned_range; blia. } right. right. split; eauto using TracePredicate.any_app_more. } } @@ -648,7 +616,8 @@ Section WithParameters. 1:eapply TracePredicate.concat_app; try intuition eassumption. subst v0. rewrite word.unsigned_ltu in H6. - destruct (word.unsigned num_bytes match type of x with _ => subst x end end. diff --git a/compiler/src/compilerExamples/Softmul.v b/compiler/src/compilerExamples/Softmul.v index feadee4ca..e190efdc1 100644 --- a/compiler/src/compilerExamples/Softmul.v +++ b/compiler/src/compilerExamples/Softmul.v @@ -36,7 +36,7 @@ Require Import riscv.Platform.MaterializeRiscvProgram. Require Import compiler.regs_initialized. Require Import compilerExamples.SoftmulBedrock2. Require Import compilerExamples.SoftmulCompile. -Require Import bedrock2.SepAutoArray bedrock2.SepAuto. +Require Import bedrock2.SepAutoArray bedrock2.SepAutoExports. Require Import bedrock2.SepBulletPoints. Local Open Scope sep_bullets_scope. Undelimit Scope sep_scope. diff --git a/compiler/src/compilerExamples/SoftmulBedrock2.v b/compiler/src/compilerExamples/SoftmulBedrock2.v index 32eb413a6..a86e6ae57 100644 --- a/compiler/src/compilerExamples/SoftmulBedrock2.v +++ b/compiler/src/compilerExamples/SoftmulBedrock2.v @@ -22,7 +22,7 @@ Definition softmul := From bedrock2 Require Import Semantics BasicC32Semantics WeakestPrecondition ProgramLogic. From coqutil Require Import Word.Properties Word.Interface Tactics.letexists. Require Import riscv.Spec.Decode riscv.Utility.Utility. -Require Import bedrock2.SepAutoArray bedrock2.SepAuto. +Require Import bedrock2.SepAutoArray bedrock2.SepAutoExports. Open Scope bool_scope. (* like (decode RV32I), but additionally also accepts the Mul instruction diff --git a/compiler/src/compilerExamples/SoftmulCompile.v b/compiler/src/compilerExamples/SoftmulCompile.v index 7cbbe552c..bb3af21a5 100644 --- a/compiler/src/compilerExamples/SoftmulCompile.v +++ b/compiler/src/compilerExamples/SoftmulCompile.v @@ -35,7 +35,7 @@ Require Import compilerExamples.SoftmulBedrock2. Require compiler.Pipeline. Require Import bedrock2.BasicC32Semantics. Require Import bedrock2.SepBulletPoints. Local Open Scope sep_bullets_scope. -Require Import bedrock2.SepAutoArray bedrock2.SepAuto. +Require Import bedrock2.SepAutoArray bedrock2.SepAutoExports. (* TODO might need slight change to Naive.word to make these hold (shifts ignore high bits) *)