From 246e1bc62c9f104d155e84488297e55f7c6836ac Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Mon, 13 Jun 2022 06:02:33 -0700
Subject: [PATCH 01/13] added the Eithers type as a multi-way sum, along with
 the eithers multi-way eliminator for Eithers

---
 saw-core/prelude/Prelude.sawcore | 120 +++++++++++++++++++++++--------
 1 file changed, 92 insertions(+), 28 deletions(-)

diff --git a/saw-core/prelude/Prelude.sawcore b/saw-core/prelude/Prelude.sawcore
index 95f573818e..8797542903 100644
--- a/saw-core/prelude/Prelude.sawcore
+++ b/saw-core/prelude/Prelude.sawcore
@@ -1549,6 +1549,98 @@ listSortDrop = ListSort__rec (\ (_:ListSort) -> Nat -> ListSort)
      Nat_cases ListSort Ds (\ (n:Nat) (_ : ListSort) -> rec n));
 
 
+--------------------------------------------------------------------------------
+-- Nested Either types
+
+-- The false proposition
+FalseProp : Prop;
+FalseProp = Eq Bool True False;
+
+-- Ex Falso Quodlibet: if True = False then anything is possible
+efq : (a : sort 0) -> FalseProp -> a;
+efq a contra =
+  coerce
+    #() a
+    (trans
+     (sort 0) #() (ite (sort 0) True #() a) a
+     (sym (sort 0) (ite (sort 0) True #() a) #()
+           (ite_true (sort 0) #() a))
+     (trans
+      (sort 0) (ite (sort 0) True #() a) (ite (sort 0) False #() a) a
+      (eq_cong Bool True False contra (sort 0)
+               (\ (b:Bool) -> ite (sort 0) b #() a))
+      (ite_false (sort 0) #() a)
+      ))
+    ();
+
+-- Ex Falso Quodlibet at sort 1
+efq1 : (a : sort 1) -> Eq Bool True False -> a;
+efq1 a contra =
+  Eq__rec Bit Bit1
+          (\ (b:Bit) (_:Eq Bit Bit1 b) -> Bit#rec (\ (_:Bit) -> sort 1) #() a b)
+          () Bit0 (efq (Eq Bit Bit1 Bit0) contra);
+
+-- An if-then-else that tests if a ListSort is nil
+ifLSNil : (a : sort 1) -> ListSort -> a -> a -> a;
+ifLSNil a l x y =
+  ListSort__rec (\ (_:ListSort) -> a) x (\ (_:sort 0) (_:ListSort) (_:a) -> y) l;
+
+-- A right-nested sequence of Eithers, defined as
+--   Eithers [] = FalseProp
+--   Eithers [tp] = tp
+--   Eithers (tp:tps) = Either tp (Eithers tps)
+Eithers : ListSort -> sort 0;
+Eithers = ListSort__rec
+            (\ (_:ListSort) -> sort 0)
+            FalseProp
+            (\ (tp:sort 0) (tail:ListSort) (rec:sort 0) ->
+               ifLSNil (sort 0) tail tp (Either tp rec));
+
+-- Eliminate the outermost either of an Eithers of cons shape
+eithers1 : (tp:sort 0) -> (tps:ListSort) -> (a:sort 0) ->
+           Eithers (LS_Cons tp tps) -> (tp -> a) -> (Eithers tps -> a) -> a;
+eithers1 tp tps_in a =
+  ListSort__rec
+    (\ (tps:ListSort) ->
+       Eithers (LS_Cons tp tps) -> (tp -> a) -> (Eithers tps -> a) -> a)
+    (\ (eiths:tp) (f:tp -> a) (_:FalseProp -> a) -> f eiths)
+    (\ (tp2:sort 0) (tail:ListSort)
+       (_:Eithers (LS_Cons tp tail) -> (tp -> a) -> (Eithers tail -> a) -> a)
+       (eiths:Either tp (Eithers (LS_Cons tp2 tail)))
+       (f1:tp -> a) (f2:Eithers (LS_Cons tp2 tail) -> a) ->
+       either tp (Eithers (LS_Cons tp2 tail)) a f1 f2 eiths)
+    tps_in;
+
+-- The type of the eliminator for Eithers tp, which maps [tp1,...,tpn] a to
+-- (tp1 -> a) -> ... -> (tpn -> a) -> a
+eithersType : ListSort -> sort 0 -> sort 0;
+eithersType tps a =
+  ListSort__rec (\ (_:ListSort) -> sort 0)
+                a
+                (\ (tp:sort 0) (_:ListSort) (rec:sort 0) -> (tp -> a) -> rec)
+                tps;
+
+-- Lift an a to an eithersType tps a by building a constant function
+liftEithersType : (a:sort 0) -> (tps:ListSort) -> a -> eithersType tps a;
+liftEithersType a =
+  ListSort__rec (\ (tps:ListSort) -> a -> eithersType tps a)
+                (\ (x:a) -> x)
+                (\ (tp:sort 0) (tps:ListSort) (rec:a -> eithersType tps a)
+                   (x:a) (_:tp -> a) -> rec x);
+
+-- An eliminator for the Eithers type
+eithers : (tps:ListSort) -> (a:sort 0) -> Eithers tps -> eithersType tps a;
+eithers tps_top a =
+  ListSort__rec
+    (\ (tps:ListSort) -> Eithers tps -> eithersType tps a)
+    (\ (contra:FalseProp) -> efq a contra)
+    (\ (tp:sort 0) (tps:ListSort) (rec:Eithers tps -> eithersType tps a)
+       (eiths:Eithers (LS_Cons tp tps)) (f:tp -> a) ->
+       eithers1 tp tps (eithersType tps a) eiths
+                       (\ (x:tp) -> liftEithersType a tps (f x)) rec)
+    tps_top;
+
+
 --------------------------------------------------------------------------------
 -- Lists of 64-bit words (for testing Heapster)
 
@@ -1710,34 +1802,6 @@ genFromBVVec : (n : Nat) -> (len : Vec n Bool) -> (a : sort 0) ->
 genFromBVVec n len a v def m =
   gen m a (\ (i:Nat) -> atWithDefault (bvToNat n len) a def v i);
 
--- The false proposition
-FalseProp : Prop;
-FalseProp = Eq Bool True False;
-
--- Ex Falso Quodlibet: if True = False then anything is possible
-efq : (a : sort 0) -> FalseProp -> a;
-efq a contra =
-  coerce
-    #() a
-    (trans
-     (sort 0) #() (ite (sort 0) True #() a) a
-     (sym (sort 0) (ite (sort 0) True #() a) #()
-           (ite_true (sort 0) #() a))
-     (trans
-      (sort 0) (ite (sort 0) True #() a) (ite (sort 0) False #() a) a
-      (eq_cong Bool True False contra (sort 0)
-               (\ (b:Bool) -> ite (sort 0) b #() a))
-      (ite_false (sort 0) #() a)
-      ))
-    ();
-
--- Ex Falso Quodlibet at sort 1
-efq1 : (a : sort 1) -> Eq Bool True False -> a;
-efq1 a contra =
-  Eq__rec Bit Bit1
-          (\ (b:Bit) (_:Eq Bit Bit1 b) -> Bit#rec (\ (_:Bit) -> sort 1) #() a b)
-          () Bit0 (efq (Eq Bit Bit1 Bit0) contra);
-
 -- Generate an empty BVVec
 emptyBVVec : (n : Nat) -> (a : sort 0) -> BVVec n (bvNat n 0) a;
 emptyBVVec n a =

From c7af0a16a64d3dafce2bbb4e3a68b37a1f58a133 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Mon, 13 Jun 2022 06:03:05 -0700
Subject: [PATCH 02/13] changed Heapster disjunctive elimination to a multi-way
 elimination

---
 .../src/Verifier/SAW/Heapster/Implication.hs  | 116 +++++++++++++-----
 1 file changed, 87 insertions(+), 29 deletions(-)

diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
index 20ac85ab50..a789f4e31d 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
@@ -1399,12 +1399,11 @@ data PermImpl1 ps_in ps_outs where
   Impl1_Pop :: ExprVar a -> ValuePerm a ->
                PermImpl1 (ps :> a) (RNil :> '(RNil, ps))
 
-  -- | Eliminate a disjunction on the top of the stack:
+  -- | Eliminate a sequence of right-nested disjunctions:
   --
-  -- > ps * x:(p1 \/ p2) -o (ps * x:p1) \/ (ps * x:p2)
-  Impl1_ElimOr :: ExprVar a -> ValuePerm a -> ValuePerm a ->
-                  PermImpl1 (ps :> a)
-                  (RNil :> '(RNil, ps :> a) :> '(RNil, ps :> a))
+  -- > ps * x:(p1 \/ (p2 \/ (... \/ pn)))
+  -- >   -o (ps * x:p1) \/ ... \/ (ps * x:pn)
+  Impl1_ElimOrs :: ExprVar a -> OrList ps a disjs -> PermImpl1 (ps :> a) disjs
 
   -- | Eliminate an existential on the top of the stack:
   --
@@ -1537,6 +1536,16 @@ data PermImpl1 ps_in ps_outs where
     String -> PermImpl1 ps (RNil :> '(RNil, ps :> LLVMPointerType w))
 
 
+-- | A single disjunct of type @a@ being eliminated, with permissions @ps@ on
+-- the stack below the disjunction
+data OrListDisj (ps :: RList CrucibleType) a
+     (disj :: (RList CrucibleType, RList CrucibleType)) where
+  OrListDisj :: ValuePerm a -> OrListDisj ps a '(RNil, ps :> a)
+
+-- | A sequence of disjuncts being eliminated, with permissions @ps@ on the
+-- stack below the disjunction
+type OrList ps a = RAssign (OrListDisj ps a)
+
 -- | A @'PermImpl' r ps@ is a proof tree of the judgment
 --
 -- > Gamma | Pl * P |- (Gamma1 | Pl1 * P1) \/ ... \/ (Gamman | Pln * Pn)
@@ -1591,6 +1600,9 @@ instance NuMatchingAny1 EqPerm where
 instance NuMatchingAny1 (LocalImplRet ps) where
   nuMatchingAny1Proof = nuMatchingProof
 
+instance NuMatchingAny1 (OrListDisj ps a) where
+  nuMatchingAny1Proof = nuMatchingProof
+
 -- Many of these types are mutually recursive. Moreover, Template Haskell
 -- declaration splices strictly separate top-level groups, so if we were to
 -- write each $(mkNuMatching [t| ... |]) splice individually, the splices
@@ -1603,6 +1615,7 @@ $(concatMapM mkNuMatching
   , [t| forall ps a. NuMatching a => EqProof ps a |]
   , [t| forall ps_in ps_out. SimplImpl ps_in ps_out |]
   , [t| forall ps_in ps_outs. PermImpl1 ps_in ps_outs |]
+  , [t| forall ps a disj. OrListDisj ps a disj |]
   , [t| forall r bs_pss. NuMatchingAny1 r => MbPermImpls r bs_pss |]
   , [t| forall r ps. NuMatchingAny1 r => PermImpl r ps |]
   , [t| forall ps_in ps_out. LocalPermImpl ps_in ps_out |]
@@ -1619,12 +1632,12 @@ data DistPermsSplit ps where
 
 $(mkNuMatching [t| forall ps. DistPermsSplit ps |])
 
-
+-- FIXME: delete all of this?
+{-
 -- | Compile-time flag for whether to prune failure branches in 'implCatchM'
 pruneFailingBranches :: Bool
 pruneFailingBranches = False
 
-
 -- | Apply the 'PermImpl_Step' constructor to a 'PermImpl1' rule and its
 -- sub-proofs, performing the following simplifications (some of which are
 -- performed by the helper function 'permImplCatch'), where @unary impl@
@@ -1671,10 +1684,10 @@ permImplStep impl1@(Impl1_TryProveBVProp _ _ _) mb_impls =
   permImplStepUnary impl1 mb_impls
 
 -- An or elimination fails if both branches fail
-permImplStep (Impl1_ElimOr _ _ _) (MbPermImpls_Cons _
-                                   (MbPermImpls_Cons _ MbPermImpls_Nil
-                                    (matchMbImplFail -> Just msg1))
-                                   (matchMbImplFail -> Just msg2)) =
+permImplStep (Impl1_ElimOrs _ _ _) (MbPermImpls_Cons _
+                                    (MbPermImpls_Cons _ MbPermImpls_Nil
+                                     (matchMbImplFail -> Just msg1))
+                                    (matchMbImplFail -> Just msg2)) =
   PermImpl_Step (Impl1_Fail
                  (msg1 ++ "\n\n--------------------\n\n" ++ msg2))
   MbPermImpls_Nil
@@ -1710,7 +1723,6 @@ permImplStepUnary impl1 (MbPermImpls_Cons MbPermImpls_Nil
 -- Default case: just apply PermImpl_Step
 permImplStepUnary impl1 mb_impls = PermImpl_Step impl1 mb_impls
 
-
 -- | Pattern-match an implication inside a binding to see if it is just a
 -- failure, and if so, return the failure message, all without requiring a
 -- 'NuMatchingAny1' constraint on the @r@ variable
@@ -1756,6 +1768,7 @@ permImplCatch pimpl1 pimpl2 =
   PermImpl_Step Impl1_Catch $
   MbPermImpls_Cons knownRepr (MbPermImpls_Cons knownRepr MbPermImpls_Nil $ emptyMb pimpl1) $
   emptyMb pimpl2
+-}
 
 
 -- | Test if a 'PermImpl' "succeeds", meaning there is at least one non-failing
@@ -1774,10 +1787,18 @@ permImplSucceeds (PermImpl_Step (Impl1_Push _ _) (MbPermImpls_Cons _ _ mb_impl))
   mbLift $ fmap permImplSucceeds mb_impl
 permImplSucceeds (PermImpl_Step (Impl1_Pop _ _) (MbPermImpls_Cons _ _ mb_impl)) =
   mbLift $ fmap permImplSucceeds mb_impl
+permImplSucceeds (PermImpl_Step (Impl1_ElimOrs _ _ ) mb_impls) =
+  mbImplsSucc mb_impls where
+  mbImplsSucc :: MbPermImpls r ps_outs -> Int
+  mbImplsSucc MbPermImpls_Nil = 0
+  mbImplsSucc (MbPermImpls_Cons _ mb_impls' mb_impl) =
+    max (mbImplsSucc mb_impls') (mbLift $ fmap permImplSucceeds mb_impl)
+{-
 permImplSucceeds (PermImpl_Step (Impl1_ElimOr _ _ _)
                   (MbPermImpls_Cons _ (MbPermImpls_Cons _ _ mb_impl1) mb_impl2)) =
   max (mbLift (fmap permImplSucceeds mb_impl1))
   (mbLift (fmap permImplSucceeds mb_impl2))
+-}
 permImplSucceeds (PermImpl_Step (Impl1_ElimExists _ _)
                   (MbPermImpls_Cons _ _ mb_impl)) =
   mbLift $ fmap permImplSucceeds mb_impl
@@ -2616,6 +2637,27 @@ mbPermSets2 :: (KnownRepr CruCtx bs1, KnownRepr CruCtx bs2) =>
 mbPermSets2 ps1 ps2 =
   MbPermSets_Cons (MbPermSets_Cons MbPermSets_Nil knownRepr ps1) knownRepr ps2
 
+-- | Extract the permission in an or elimination disjunct
+orListDisjPerm :: OrListDisj ps a disj -> ValuePerm a
+orListDisjPerm (OrListDisj p) = p
+
+-- | Extract the disjuncts of an or elimination list
+orListDisjs :: OrList ps a disjs -> [ValuePerm a]
+orListDisjs = RL.mapToList orListDisjPerm
+
+-- | Compute the permission eliminated by an 'OrList'
+orListPerm :: OrList ps a disjs -> ValuePerm a
+orListPerm MNil = error "orListPerm: empty disjunct list!"
+orListPerm or_list = foldr1 ValPerm_Or $ orListDisjs or_list
+
+-- | Build an 'MbPermSets' 
+orListMbPermSets :: PermSet (ps :> a) -> ExprVar a -> OrList ps a disjs ->
+                    MbPermSets disjs
+orListMbPermSets _ _ MNil = MbPermSets_Nil
+orListMbPermSets ps x (or_list :>: OrListDisj p) =
+  MbPermSets_Cons (orListMbPermSets ps x or_list) CruCtxNil $
+  emptyMb $ set (topDistPerm x) p ps
+
 -- | Apply a single permission implication step to a permission set
 applyImpl1 :: HasCallStack => PPInfo -> PermImpl1 ps_in ps_outs ->
               PermSet ps_in -> MbPermSets ps_outs
@@ -2644,12 +2686,11 @@ applyImpl1 pp_info (Impl1_Pop x p) ps =
       vsep [pretty "applyImpl1: Impl1_Pop: non-empty permissions for variable"
             <+> permPretty pp_info x <> pretty ":",
             permPretty pp_info (ps ^. varPerm x)]
-applyImpl1 _ (Impl1_ElimOr x p1 p2) ps =
-  if ps ^. topDistPerm x == ValPerm_Or p1 p2 then
-    mbPermSets2 (emptyMb $ set (topDistPerm x) p1 ps)
-    (emptyMb $ set (topDistPerm x) p2 ps)
+applyImpl1 _ (Impl1_ElimOrs x or_list) ps =
+  if ps ^. topDistPerm x == orListPerm or_list then
+    orListMbPermSets ps x or_list
   else
-    error "applyImpl1: Impl1_ElimOr: unexpected permission"
+    error "applyImpl1: Impl1_ElimOrs: unexpected permission"
 applyImpl1 _ (Impl1_ElimExists x p_body) ps =
   if ps ^. topDistPerm x == ValPerm_Exists p_body then
     mbPermSets1 (fmap (\p -> set (topDistPerm x) p ps) p_body)
@@ -3116,8 +3157,8 @@ instance SubstVar PermVarSubst m =>
       Impl1_Push <$> genSubst s x <*> genSubst s p
     [nuMP| Impl1_Pop x p |] ->
       Impl1_Pop <$> genSubst s x <*> genSubst s p
-    [nuMP| Impl1_ElimOr x p1 p2 |] ->
-      Impl1_ElimOr <$> genSubst s x <*> genSubst s p1 <*> genSubst s p2
+    [nuMP| Impl1_ElimOrs x or_list |] ->
+      Impl1_ElimOrs <$> genSubst s x <*> genSubst s or_list
     [nuMP| Impl1_ElimExists x p_body |] ->
       Impl1_ElimExists <$> genSubst s x <*> genSubst s p_body
     [nuMP| Impl1_ElimFalse x |] ->
@@ -3166,6 +3207,13 @@ instance (NuMatchingAny1 r, SubstVar PermVarSubst m,
       let px = mbLift mpx in
       MbPermImpls_Cons px <$> genSubst s mb_impl <*> genSubstMb (cruCtxProxies px) s mb_impls'
 
+instance SubstVar s m => Substable s (OrListDisj ps a disj) m where
+  genSubst s (mbMatch -> [nuMP| OrListDisj mb_p |]) =
+    OrListDisj <$> genSubst s mb_p
+
+instance SubstVar s m => Substable1 s (OrListDisj ps a) m where
+  genSubst1 = genSubst
+
 -- FIXME: shouldn't need the SubstVar PermVarSubst m assumption...
 instance SubstVar PermVarSubst m =>
          Substable PermVarSubst (LocalPermImpl ps_in ps_out) m where
@@ -3891,15 +3939,25 @@ implPopM x p =
                         permPretty i x <> colon <> permPretty i p]) >>>
   implApplyImpl1 (Impl1_Pop x p) (MNil :>: Impl1Cont (const $ pure ()))
 
--- | Eliminate a disjunctive permission @x:(p1 \/ p2)@, building proof trees
--- that proceed with both @x:p1@ and @x:p2@
-implElimOrM :: NuMatchingAny1 r => ExprVar a -> ValuePerm a -> ValuePerm a ->
-               ImplM vars s r (ps :> a) (ps :> a) ()
-implElimOrM x p1 p2 =
+-- | Pattern-match a permission as a sequence of 1 or more disjuncts
+matchOrList :: ValuePerm a -> Maybe (Some (OrList ps a))
+matchOrList p_top@(ValPerm_Or _ _) = Just (helper MNil p_top) where
+  helper :: OrList ps a disjs -> ValuePerm a -> Some (OrList ps a)
+  helper or_list (ValPerm_Or p1 p2) =
+    helper (or_list :>: OrListDisj p1) p2
+  helper or_list p = Some (or_list :>: OrListDisj p)
+matchOrList _ = Nothing
+
+-- | Eliminate a right-nested disjunction @x:(p1 \/ (p2 \/ (... \/ pn)))@,
+-- building proof trees that proceed with all the @pi@
+implElimOrsM :: NuMatchingAny1 r => ExprVar a -> ValuePerm a ->
+                ImplM vars s r (ps :> a) (ps :> a) ()
+implElimOrsM x p@(matchOrList -> Just (Some or_list)) =
   implTraceM (\pp_info -> pretty "Eliminating or:" <+>
-                          permPretty pp_info (ValPerm_Or p1 p2)) >>>
-  implApplyImpl1 (Impl1_ElimOr x p1 p2)
-  (MNil :>: Impl1Cont (const $ pure ()) :>: Impl1Cont (const $ pure ()))
+                          permPretty pp_info p) >>>
+  implApplyImpl1 (Impl1_ElimOrs x or_list)
+  (RL.map (\(OrListDisj _) -> Impl1Cont (const $ pure ())) or_list)
+implElimOrsM _ _ = error "implElimOrsM: malformed input permission"
 
 -- | Eliminate an existential permission @x:(exists (y:tp).p)@ in the current
 -- permission set
@@ -4255,7 +4313,7 @@ elimOrsExistsM :: NuMatchingAny1 r => ExprVar a ->
                   ImplM vars s r (ps :> a) (ps :> a) (ValuePerm a)
 elimOrsExistsM x =
   getTopDistPerm x >>= \case
-    ValPerm_Or p1 p2 -> implElimOrM x p1 p2 >>> elimOrsExistsM x
+    p@(ValPerm_Or _ _) -> implElimOrsM x p >>> elimOrsExistsM x
     ValPerm_Exists mb_p ->
       implElimExistsM x mb_p >>> elimOrsExistsM x
     p -> pure p
@@ -4266,7 +4324,7 @@ elimOrsExistsNamesM :: NuMatchingAny1 r => ExprVar a ->
                        ImplM vars s r (ps :> a) (ps :> a) (ValuePerm a)
 elimOrsExistsNamesM x =
   getTopDistPerm x >>= \case
-    ValPerm_Or p1 p2 -> implElimOrM x p1 p2 >>> elimOrsExistsNamesM x
+    p@(ValPerm_Or _ _) -> implElimOrsM x p >>> elimOrsExistsNamesM x
     ValPerm_Exists mb_p ->
       implElimExistsM x mb_p >>> elimOrsExistsNamesM x
     ValPerm_Named npn args off

From 2b20530b946940c5f8ffcd5e539e104571a3c2c4 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Mon, 13 Jun 2022 11:19:31 -0700
Subject: [PATCH 03/13] made CompM and associated definitions universe
 polymorphic

---
 saw-core-coq/coq/handwritten/CryptolToCoq/CompM.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/CompM.v b/saw-core-coq/coq/handwritten/CryptolToCoq/CompM.v
index 2830372fdf..813f5e3601 100644
--- a/saw-core-coq/coq/handwritten/CryptolToCoq/CompM.v
+++ b/saw-core-coq/coq/handwritten/CryptolToCoq/CompM.v
@@ -93,7 +93,7 @@ Class MonadFix M `{Monad M} `{MonadLeqOp M} `{MonadFixOp M} : Prop :=
  ***)
 
 (* The set monad = the sets over a given type *)
-Definition SetM (A:Type) : Type := A -> Prop.
+Polymorphic Definition SetM (A:Type) : Type := A -> Prop.
 
 (* Equivalence of two sets = they contain the same elements *)
 Instance MonadEqOp_SetM : MonadEqOp SetM :=
@@ -191,7 +191,7 @@ Qed.
  ***)
 
 (* The option transformer just adds "option" around the type A *)
-Definition OptionT (M:Type -> Type) (A:Type) : Type := M (option A).
+Polymorphic Definition OptionT (M:Type -> Type) (A:Type) : Type := M (option A).
 
 (* Equivalence in OptionT is just the underlying equivlence *)
 Instance MonadEqOp_OptionT M `{MonadEqOp M} : MonadEqOp (OptionT M) :=
@@ -410,7 +410,7 @@ Proof.
  *** The Computation Monad = the Option-Set Monad
  ***)
 
-Definition CompM : Type -> Type := OptionT SetM.
+Polymorphic Definition CompM : Type -> Type := OptionT SetM.
 
 
 (***

From 1b3bfe42d4378819866f0725dcfe41bf7ae64a6f Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Mon, 13 Jun 2022 11:20:02 -0700
Subject: [PATCH 04/13] updated SAW translation to handle the new multi-way or
 elimination rule

---
 .../Verifier/SAW/Heapster/IRTTranslation.hs   |  7 --
 .../src/Verifier/SAW/Heapster/Implication.hs  | 31 ++++++++
 .../Verifier/SAW/Heapster/SAWTranslation.hs   | 74 +++++++++++--------
 3 files changed, 75 insertions(+), 37 deletions(-)

diff --git a/heapster-saw/src/Verifier/SAW/Heapster/IRTTranslation.hs b/heapster-saw/src/Verifier/SAW/Heapster/IRTTranslation.hs
index 94b18ac804..33f65f3a83 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/IRTTranslation.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/IRTTranslation.hs
@@ -61,13 +61,6 @@ completeOpenTermTyped sc (OpenTerm termM) =
   either (fail . show) return =<<
   runTCM termM sc Nothing []
 
--- | Build an element of type ListSort from a list of types
--- TODO Move this to OpenTerm.hs?
-listSortOpenTerm :: [OpenTerm] -> OpenTerm
-listSortOpenTerm [] = ctorOpenTerm "Prelude.LS_Nil" []
-listSortOpenTerm (tp:tps) =
-  ctorOpenTerm "Prelude.LS_Cons" [tp, listSortOpenTerm tps]
-
 -- | Get the result of applying 'exprCtxToTerms' to the current expression
 -- translation context
 -- TODO Move this to SAWTranslation.hs?
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
index a789f4e31d..0f33cf91e3 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
@@ -2645,11 +2645,19 @@ orListDisjPerm (OrListDisj p) = p
 orListDisjs :: OrList ps a disjs -> [ValuePerm a]
 orListDisjs = RL.mapToList orListDisjPerm
 
+-- | Extract the disjuncts of an or elimination list in a binding
+mbOrListDisjs :: Mb ctx (OrList ps a disjs) -> [Mb ctx (ValuePerm a)]
+mbOrListDisjs = mbList . mbMapCl $(mkClosed [| orListDisjs |])
+
 -- | Compute the permission eliminated by an 'OrList'
 orListPerm :: OrList ps a disjs -> ValuePerm a
 orListPerm MNil = error "orListPerm: empty disjunct list!"
 orListPerm or_list = foldr1 ValPerm_Or $ orListDisjs or_list
 
+-- | Compute the permission-in-binding eliminated by an 'OrList' in a binding
+mbOrListPerm :: Mb ctx (OrList ps a disj) -> Mb ctx (ValuePerm a)
+mbOrListPerm = mbMapCl $(mkClosed [| orListPerm |])
+
 -- | Build an 'MbPermSets' 
 orListMbPermSets :: PermSet (ps :> a) -> ExprVar a -> OrList ps a disjs ->
                     MbPermSets disjs
@@ -2658,6 +2666,29 @@ orListMbPermSets ps x (or_list :>: OrListDisj p) =
   MbPermSets_Cons (orListMbPermSets ps x or_list) CruCtxNil $
   emptyMb $ set (topDistPerm x) p ps
 
+-- | If we have an 'MbPermImpls' list associated with a multi-way or
+-- elimination, extract out the list of 'PermImpl's it carries
+orListPermImpls :: OrList ps a disjs -> MbPermImpls r disjs ->
+                   [PermImpl r (ps :> a)]
+orListPermImpls MNil MbPermImpls_Nil = []
+orListPermImpls (or_list :>: OrListDisj _) (MbPermImpls_Cons
+                                            _ mb_impls mb_impl) =
+  orListPermImpls or_list mb_impls ++ [elimEmptyMb mb_impl]
+
+-- | Extract the 'PermImpl's-in-bindings from an 'MbPermImpls'-in-binding
+-- associated with a multi-way or elimination
+mbOrListPermImpls :: NuMatchingAny1 r => Mb ctx (OrList ps a disjs) ->
+                     Mb ctx (MbPermImpls r disjs) ->
+                     [Mb ctx (PermImpl r (ps :> a))]
+mbOrListPermImpls (mbMatch ->
+                   [nuMP| MNil |]) (mbMatch -> [nuMP| MbPermImpls_Nil |]) = []
+mbOrListPermImpls
+  (mbMatch -> [nuMP| mb_or_list :>: OrListDisj _ |])
+  (mbMatch -> [nuMP| MbPermImpls_Cons _ mb_impls mb_impl |])
+  = mbOrListPermImpls mb_or_list mb_impls ++ [mbMapCl
+                                              $(mkClosed [| elimEmptyMb |])
+                                              mb_impl]
+
 -- | Apply a single permission implication step to a permission set
 applyImpl1 :: HasCallStack => PPInfo -> PermImpl1 ps_in ps_outs ->
               PermSet ps_in -> MbPermSets ps_outs
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
index 1d227e8594..f3c8316efe 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
@@ -84,6 +84,12 @@ suffixMembers _ MNil = MNil
 suffixMembers ctx1 (ctx2 :>: _) =
   RL.map Member_Step (suffixMembers ctx1 ctx2) :>: Member_Base
 
+-- | Build a SAW core term of type @ListSort@ from a list of types
+listSortOpenTerm :: [OpenTerm] -> OpenTerm
+listSortOpenTerm =
+  foldr (\x y -> ctorOpenTerm "Prelude.LS_Cons" [x,y])
+  (ctorOpenTerm "Prelude.LS_Nil" [])
+
 
 ----------------------------------------------------------------------
 -- * Translation Monads
@@ -499,6 +505,20 @@ eitherElimTransM tp_l tp_r tp_ret fl fr eith =
        [ typeTransTupleType tp_l, typeTransTupleType tp_r,
          typeTransTupleType tp_ret, fl_trans, fr_trans, eith ]
 
+-- | Eliminate a multi-way SAW @Eithers@ type, taking in: a list of the
+-- translations of the types in the @Eithers@ type; the translation of the
+-- output type; a list of functions for the branches of the @Eithers@
+-- elimination; and the term of @Eithers@ type being eliminated
+eithersElimTransM :: [TypeTrans tr_in] -> TypeTrans tr_out ->
+                     [tr_in -> TransM info ctx OpenTerm] -> OpenTerm ->
+                     TransM info ctx OpenTerm
+eithersElimTransM tps tp_ret fs eith =
+  do fs_transs <-
+       zipWithM (\tp f -> lambdaTupleTransM "x_eith_elim" tp f) tps fs
+     let tps_list = listSortOpenTerm $ map typeTransTupleType tps
+     return $ applyOpenTermMulti (globalOpenTerm "Prelude.eithers")
+       ([tps_list, typeTransTupleType tp_ret, eith] ++ fs_transs)
+
 -- | Build the dependent pair type whose first projection type is the
 -- 'typeTransTupleType' of the supplied 'TypeTrans' and whose second projection
 -- is the 'typeTransTupleType' of the supplied monadic function. As a special
@@ -3514,36 +3534,30 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl
        ptrans <- getTopPermM
        setVarPermM x ptrans (withPermStackM RL.tail RL.tail m)
 
-  -- If both branches of an or elimination fail, the whole thing fails; otherwise,
-  -- an or elimination performs a pattern-match on an Either
-  ([nuMP| Impl1_ElimOr x mb_p1 mb_p2 |],
-   [nuMP| (MbPermImpls_Cons _ (MbPermImpls_Cons _ _ mb_impl1) mb_impl2) |]) ->
-    pitmCatching (translatePermImpl prx $
-                  mbCombine RL.typeCtxProxies mb_impl1) >>= \(mtrans1,hasf1) ->
-    pitmCatching (translatePermImpl prx $
-                  mbCombine RL.typeCtxProxies mb_impl2) >>= \(mtrans2,hasf2) ->
-    tell ([],hasf1 <> hasf2) >>
-    case (mtrans1, mtrans2) of
-      (Nothing, Nothing) -> mzero
-      _ ->
-        return $ \k ->
-        do let mb_p1_or_p2 =
-                 mbMapCl $(mkClosed
-                           [| \(Impl1_ElimOr _ p1 p2) -> ValPerm_Or p1 p2 |])
-                 mb_impl
-           () <- assertTopPermM "Impl1_ElimOr" x mb_p1_or_p2
-           tp1 <- translate mb_p1
-           tp2 <- translate mb_p2
-           tp_ret <- compReturnTypeTransM
-           top_ptrans <- getTopPermM
-           eitherElimTransM tp1 tp2 tp_ret
-             (\ptrans ->
-               withPermStackM id ((:>: ptrans) . RL.tail) $
-               forceImplTrans mtrans1 k)
-             (\ptrans ->
-               withPermStackM id ((:>: ptrans) . RL.tail) $
-               forceImplTrans mtrans2 k)
-             (transTupleTerm top_ptrans)
+  -- If all branches of an or elimination fail, the whole thing fails; otherwise,
+  -- an or elimination performs a multi way Eithers elimination
+  ([nuMP| Impl1_ElimOrs x mb_or_list |], _) ->
+    -- First, translate all the PermImpls in mb_impls, using pitmCatching to
+    -- isolate failures to each particular branch, but still reporting failures
+    -- in any branch
+    mapM (pitmCatching . translatePermImpl prx)
+         (mbOrListPermImpls mb_or_list mb_impls) >>= \transs ->
+    let (mtranss, hasfs) = unzip transs in
+    tell ([], mconcat hasfs) >>
+    -- As a special case, if all branches fail (representing as translating to
+    -- Nothing), then the entire or elimination fails
+    if all isNothing mtranss then mzero else
+      return $ \k ->
+      do let mb_or_p = mbOrListPerm mb_or_list
+         () <- assertTopPermM "Impl1_ElimOrs" x mb_or_p
+         tps <- mapM translate $ mbOrListDisjs mb_or_list
+         tp_ret <- compReturnTypeTransM
+         top_ptrans <- getTopPermM
+         eithersElimTransM tps tp_ret
+           (flip map mtranss $ \mtrans ptrans ->
+             withPermStackM id ((:>: ptrans) . RL.tail) $
+             forceImplTrans mtrans k)
+           (transTupleTerm top_ptrans)
 
   -- An existential elimination performs a pattern-match on a Sigma
   ([nuMP| Impl1_ElimExists x p |], _) ->

From 2c7e195dae6a8da182c62b1413611c5f8e5ed808 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Mon, 13 Jun 2022 15:58:44 -0700
Subject: [PATCH 05/13] rewrote the multi-way eithers eliminator to take in an
 inductive list of eliminators, which should hopefully be better for
 automation...

---
 .../Verifier/SAW/Heapster/SAWTranslation.hs   |  16 ++-
 .../coq/handwritten/CryptolToCoq/CompMExtra.v | 129 +++++++++++++++++-
 saw-core/prelude/Prelude.sawcore              |  53 +++----
 3 files changed, 163 insertions(+), 35 deletions(-)

diff --git a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
index f3c8316efe..cb87f38c86 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
@@ -513,11 +513,17 @@ eithersElimTransM :: [TypeTrans tr_in] -> TypeTrans tr_out ->
                      [tr_in -> TransM info ctx OpenTerm] -> OpenTerm ->
                      TransM info ctx OpenTerm
 eithersElimTransM tps tp_ret fs eith =
-  do fs_transs <-
-       zipWithM (\tp f -> lambdaTupleTransM "x_eith_elim" tp f) tps fs
-     let tps_list = listSortOpenTerm $ map typeTransTupleType tps
-     return $ applyOpenTermMulti (globalOpenTerm "Prelude.eithers")
-       ([tps_list, typeTransTupleType tp_ret, eith] ++ fs_transs)
+  foldr (\(tp,f) restM ->
+          do f_trans <- lambdaTupleTransM "x_eith_elim" tp f
+             rest <- restM
+             return (ctorOpenTerm "Prelude.FunsTo_Cons"
+                     [typeTransTupleType tp_ret,
+                      typeTransTupleType tp, f_trans, rest]))
+  (return $ ctorOpenTerm "Prelude.FunsTo_Nil" [typeTransTupleType tp_ret])
+  (zip tps fs)
+  >>= \elims_trans ->
+  return (applyOpenTermMulti (globalOpenTerm "Prelude.eithers")
+          [typeTransTupleType tp_ret, elims_trans, eith])
 
 -- | Build the dependent pair type whose first projection type is the
 -- 'typeTransTupleType' of the supplied 'TypeTrans' and whose second projection
diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/CompMExtra.v b/saw-core-coq/coq/handwritten/CryptolToCoq/CompMExtra.v
index dd0c1516b4..254761d7a3 100644
--- a/saw-core-coq/coq/handwritten/CryptolToCoq/CompMExtra.v
+++ b/saw-core-coq/coq/handwritten/CryptolToCoq/CompMExtra.v
@@ -77,6 +77,74 @@ Proof.
   - apply H0; reflexivity.
 Qed.
 
+Lemma refinesM_eithers_nil_l {A} P eith :
+  SAWCorePrelude.eithers (CompM A) (SAWCorePrelude.FunsTo_Nil _) eith |= P.
+Proof.
+  apply SAWCorePrelude.efq; assumption.
+Qed.
+
+Lemma refinesM_eithers_nil_r {A} P eith :
+  P |= SAWCorePrelude.eithers (CompM A) (SAWCorePrelude.FunsTo_Nil _) eith.
+Proof.
+  apply SAWCorePrelude.efq; assumption.
+Qed.
+
+Lemma refinesM_eithers_one_l {A B} (f:A -> CompM B) eith P :
+  f eith |= P ->
+  SAWCorePrelude.eithers
+    (CompM B)
+    (SAWCorePrelude.FunsTo_Cons _ _ f (SAWCorePrelude.FunsTo_Nil _))
+    eith
+    |= P.
+Proof.
+  intro r; apply r.
+Qed.
+
+Lemma refinesM_eithers_one_r {A B} (f:A -> CompM B) eith P :
+  P |= f eith ->
+  P |=
+    SAWCorePrelude.eithers
+    (CompM B)
+    (SAWCorePrelude.FunsTo_Cons _ _ f (SAWCorePrelude.FunsTo_Nil _))
+    eith.
+Proof.
+  intro r; apply r.
+Qed.
+
+Lemma refinesM_eithers_cons_l
+      {A B C} (f:A -> CompM C) (g:B -> CompM C) elims eith P :
+  (forall a, eith = SAWCorePrelude.Left _ _ a -> f a |= P) ->
+  (forall eith',
+      eith = SAWCorePrelude.Right _ _ eith' ->
+      SAWCorePrelude.eithers _ (SAWCorePrelude.FunsTo_Cons _ _ g elims) eith' |= P) ->
+  SAWCorePrelude.eithers
+    (CompM C)
+    (SAWCorePrelude.FunsTo_Cons _ _ f (SAWCorePrelude.FunsTo_Cons _ _ g elims))
+    eith
+    |= P.
+Proof.
+  destruct eith; intros; simpl.
+  - apply H; reflexivity.
+  - apply H0; reflexivity.
+Qed.
+
+Lemma refinesM_eithers_cons_r
+      {A B C} (f:A -> CompM C) (g:B -> CompM C) elims eith P :
+  (forall a, eith = SAWCorePrelude.Left _ _ a -> P |= f a) ->
+  (forall eith',
+      eith = SAWCorePrelude.Right _ _ eith' ->
+      P |= SAWCorePrelude.eithers _ (SAWCorePrelude.FunsTo_Cons _ _ g elims) eith') ->
+  P |=
+  SAWCorePrelude.eithers
+    (CompM C)
+    (SAWCorePrelude.FunsTo_Cons _ _ f (SAWCorePrelude.FunsTo_Cons _ _ g elims))
+    eith.
+Proof.
+  destruct eith; intros; simpl.
+  - apply H; reflexivity.
+  - apply H0; reflexivity.
+Qed.
+
 Lemma refinesM_maybe_l {A B} (x : CompM B) (f : A -> CompM B) mb P :
   (mb = SAWCorePrelude.Nothing _ -> x |= P) ->
   (forall a, mb = SAWCorePrelude.Just _ a -> f a |= P) ->
@@ -114,11 +182,9 @@ Proof. rewrite returnM_if. trivial. Qed.
 Lemma returnM_injective : forall (A : Type) (x y : A),
     returnM (M:=CompM) x ~= returnM y -> x = y.
 Proof.
-  intros. unfold returnM in H. unfold MonadReturnOp_OptionT in H.
-  unfold eqM in H. unfold MonadEqOp_OptionT in H. unfold eqM in H. unfold MonadEqOp_SetM in H.
-  assert (Some x = Some y) as Hxy.
-  { rewrite H. reflexivity. }
-  inversion Hxy; subst. reflexivity.
+  intros. destruct (H (Some x)).
+  assert (Some y = Some x); [ apply H0; reflexivity | ].
+  inversion H2. reflexivity.
 Qed.
 
 
@@ -353,6 +419,59 @@ Hint Extern 1 (SAWCorePrelude.either _ _ _ _ _ _ |= _) =>
 Hint Extern 1 (_ |= SAWCorePrelude.either _ _ _ _ _ _) =>
   simple apply refinesM_either_r_IntroArg : refinesM.
 
+
+Definition refinesM_eithers_cons_l_IntroArg
+           {A B C} (f:A -> CompM C) (g:B -> CompM C) elims eith P :
+  (FreshIntroArg Any _ (fun a =>
+    FreshIntroArg Either (eith = SAWCorePrelude.Left _ _ a) (fun _ => f a |= P))) ->
+  (FreshIntroArg Any _ (fun eith' =>
+    FreshIntroArg Either (eith = SAWCorePrelude.Right _ _ eith')
+      (fun _ => SAWCorePrelude.eithers _ (SAWCorePrelude.FunsTo_Cons _ _ g elims) eith' |= P))) ->
+  SAWCorePrelude.eithers
+    (CompM C)
+    (SAWCorePrelude.FunsTo_Cons _ _ f (SAWCorePrelude.FunsTo_Cons _ _ g elims))
+    eith
+    |= P :=
+  refinesM_eithers_cons_l f g elims eith P.
+
+Definition refinesM_eithers_cons_r_IntroArg
+           {A B C} (f:A -> CompM C) (g:B -> CompM C) elims eith P :
+  (FreshIntroArg Any _ (fun a =>
+    FreshIntroArg Either (eith = SAWCorePrelude.Left _ _ a) (fun _ => P |= f a))) ->
+  (FreshIntroArg Any _ (fun eith' =>
+    FreshIntroArg Either (eith = SAWCorePrelude.Right _ _ eith')
+      (fun _ => P |= SAWCorePrelude.eithers _ (SAWCorePrelude.FunsTo_Cons _ _ g elims) eith'))) ->
+  P |=
+    SAWCorePrelude.eithers
+    (CompM C)
+    (SAWCorePrelude.FunsTo_Cons _ _ f (SAWCorePrelude.FunsTo_Cons _ _ g elims))
+    eith :=
+  refinesM_eithers_cons_r f g elims eith P.
+
+Hint Extern 1 (SAWCorePrelude.eithers _ (SAWCorePrelude.FunsTo_Nil _) |= _) =>
+  simple apply refinesM_eithers_nil_l : refinesM.
+Hint Extern 1 (_ |= SAWCorePrelude.eithers _ (SAWCorePrelude.FunsTo_Nil _)) =>
+  simple apply refinesM_eithers_nil_r : refinesM.
+Hint Extern 1 (SAWCorePrelude.eithers
+                 _ (SAWCorePrelude.FunsTo_Cons
+                      _ _ _ (SAWCorePrelude.FunsTo_Nil _)) |= _) =>
+  simple apply refinesM_eithers_one_l : refinesM.
+Hint Extern 1 (_ |= SAWCorePrelude.eithers
+                      _ (SAWCorePrelude.FunsTo_Cons
+                           _ _ _ (SAWCorePrelude.FunsTo_Nil _))) =>
+  simple apply refinesM_eithers_one_r : refinesM.
+Hint Extern 1 (SAWCorePrelude.eithers
+                 _ (SAWCorePrelude.FunsTo_Cons
+                      _ _ _ (SAWCorePrelude.FunsTo_Cons
+                               _ _ _ SAWCorePrelude.FunsTo_Nil _)) |= _) =>
+  simple apply refinesM_eithers_cons_l_IntroArg : refinesM.
+Hint Extern 1 (_ |= SAWCorePrelude.eithers
+                      _ (SAWCorePrelude.FunsTo_Cons
+                           _ _ _ (SAWCorePrelude.FunsTo_Cons
+                                    _ _ _ (SAWCorePrelude.FunsTo_Nil _)))) =>
+  simple apply refinesM_eithers_cons_r_IntroArg : refinesM.
+
+
 Definition refinesM_maybe_l_IntroArg {A B} (x : CompM B) (f : A -> CompM B) mb P :
   (FreshIntroArg Maybe (mb = SAWCorePrelude.Nothing _) (fun _ => x |= P)) ->
   (FreshIntroArg Any _ (fun a =>
diff --git a/saw-core/prelude/Prelude.sawcore b/saw-core/prelude/Prelude.sawcore
index 8797542903..d4639aeea4 100644
--- a/saw-core/prelude/Prelude.sawcore
+++ b/saw-core/prelude/Prelude.sawcore
@@ -1611,34 +1611,37 @@ eithers1 tp tps_in a =
        either tp (Eithers (LS_Cons tp2 tail)) a f1 f2 eiths)
     tps_in;
 
--- The type of the eliminator for Eithers tp, which maps [tp1,...,tpn] a to
--- (tp1 -> a) -> ... -> (tpn -> a) -> a
-eithersType : ListSort -> sort 0 -> sort 0;
-eithersType tps a =
-  ListSort__rec (\ (_:ListSort) -> sort 0)
-                a
-                (\ (tp:sort 0) (_:ListSort) (rec:sort 0) -> (tp -> a) -> rec)
-                tps;
-
--- Lift an a to an eithersType tps a by building a constant function
-liftEithersType : (a:sort 0) -> (tps:ListSort) -> a -> eithersType tps a;
-liftEithersType a =
-  ListSort__rec (\ (tps:ListSort) -> a -> eithersType tps a)
-                (\ (x:a) -> x)
-                (\ (tp:sort 0) (tps:ListSort) (rec:a -> eithersType tps a)
-                   (x:a) (_:tp -> a) -> rec x);
+-- The type of a list of functions to a particular output type a
+data FunsTo (a:sort 0) : sort 1 where {
+  FunsTo_Nil : FunsTo a;
+  FunsTo_Cons : (tp:sort 0) -> (tp -> a) -> FunsTo a -> FunsTo a;
+}
+
+-- The recursor for FunsTo
+FunsTo__rec : (a:sort 0) -> (P : FunsTo a -> sort 1) -> P (FunsTo_Nil a) ->
+              ((tp:sort 0) -> (f:tp -> a) -> (es:FunsTo a) ->
+               P es -> P (FunsTo_Cons a tp f es)) ->
+              (es:FunsTo a) -> P es;
+FunsTo__rec a P f1 f2 es = FunsTo#rec a P f1 f2 es;
+
+-- Extract the input types of the functions in a FunsTo list
+FunsToIns : (a:sort 0) -> FunsTo a -> ListSort;
+FunsToIns a =
+  FunsTo__rec
+    a (\ (_:FunsTo a) -> ListSort) LS_Nil
+    (\ (tp:sort 0) (_:tp -> a) (_:FunsTo a) (rec:ListSort) -> LS_Cons tp rec);
 
 -- An eliminator for the Eithers type
-eithers : (tps:ListSort) -> (a:sort 0) -> Eithers tps -> eithersType tps a;
-eithers tps_top a =
-  ListSort__rec
-    (\ (tps:ListSort) -> Eithers tps -> eithersType tps a)
+eithers : (a:sort 0) -> (elims:FunsTo a) -> Eithers (FunsToIns a elims) -> a;
+eithers a =
+  FunsTo__rec
+    a
+    (\ (elims:FunsTo a) -> Eithers (FunsToIns a elims) -> a)
     (\ (contra:FalseProp) -> efq a contra)
-    (\ (tp:sort 0) (tps:ListSort) (rec:Eithers tps -> eithersType tps a)
-       (eiths:Eithers (LS_Cons tp tps)) (f:tp -> a) ->
-       eithers1 tp tps (eithersType tps a) eiths
-                       (\ (x:tp) -> liftEithersType a tps (f x)) rec)
-    tps_top;
+    (\ (tp:sort 0) (f:tp -> a) (elims:FunsTo a)
+       (rec:Eithers (FunsToIns a elims) -> a)
+       (eiths:Eithers (LS_Cons tp (FunsToIns a elims))) ->
+       eithers1 tp (FunsToIns a elims) a eiths f rec);
 
 
 --------------------------------------------------------------------------------

From e4baec2618400741e06f6db97953e4f88bfba9b3 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Mon, 13 Jun 2022 17:39:41 -0700
Subject: [PATCH 06/13] whoops, fixed my extern hints for the eithers
 elimination

---
 .../coq/handwritten/CryptolToCoq/CompMExtra.v        | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/CompMExtra.v b/saw-core-coq/coq/handwritten/CryptolToCoq/CompMExtra.v
index 254761d7a3..b6e63f4e08 100644
--- a/saw-core-coq/coq/handwritten/CryptolToCoq/CompMExtra.v
+++ b/saw-core-coq/coq/handwritten/CryptolToCoq/CompMExtra.v
@@ -448,27 +448,27 @@ Definition refinesM_eithers_cons_r_IntroArg
     eith :=
   refinesM_eithers_cons_r f g elims eith P.
 
-Hint Extern 1 (SAWCorePrelude.eithers _ (SAWCorePrelude.FunsTo_Nil _) |= _) =>
+Hint Extern 1 (SAWCorePrelude.eithers _ (SAWCorePrelude.FunsTo_Nil _) _ |= _) =>
   simple apply refinesM_eithers_nil_l : refinesM.
-Hint Extern 1 (_ |= SAWCorePrelude.eithers _ (SAWCorePrelude.FunsTo_Nil _)) =>
+Hint Extern 1 (_ |= SAWCorePrelude.eithers _ (SAWCorePrelude.FunsTo_Nil _) _) =>
   simple apply refinesM_eithers_nil_r : refinesM.
 Hint Extern 1 (SAWCorePrelude.eithers
                  _ (SAWCorePrelude.FunsTo_Cons
-                      _ _ _ (SAWCorePrelude.FunsTo_Nil _)) |= _) =>
+                      _ _ _ (SAWCorePrelude.FunsTo_Nil _)) _ |= _) =>
   simple apply refinesM_eithers_one_l : refinesM.
 Hint Extern 1 (_ |= SAWCorePrelude.eithers
                       _ (SAWCorePrelude.FunsTo_Cons
-                           _ _ _ (SAWCorePrelude.FunsTo_Nil _))) =>
+                           _ _ _ (SAWCorePrelude.FunsTo_Nil _)) _) =>
   simple apply refinesM_eithers_one_r : refinesM.
 Hint Extern 1 (SAWCorePrelude.eithers
                  _ (SAWCorePrelude.FunsTo_Cons
                       _ _ _ (SAWCorePrelude.FunsTo_Cons
-                               _ _ _ SAWCorePrelude.FunsTo_Nil _)) |= _) =>
+                               _ _ _ (SAWCorePrelude.FunsTo_Nil _))) _ |= _) =>
   simple apply refinesM_eithers_cons_l_IntroArg : refinesM.
 Hint Extern 1 (_ |= SAWCorePrelude.eithers
                       _ (SAWCorePrelude.FunsTo_Cons
                            _ _ _ (SAWCorePrelude.FunsTo_Cons
-                                    _ _ _ (SAWCorePrelude.FunsTo_Nil _)))) =>
+                                    _ _ _ (SAWCorePrelude.FunsTo_Nil _))) _) =>
   simple apply refinesM_eithers_cons_r_IntroArg : refinesM.
 
 

From 34ff61c647740be9e508c18cedb09eb6c4cfe3c3 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Mon, 13 Jun 2022 17:40:57 -0700
Subject: [PATCH 07/13] small tweak to get is_elem_fun_ref_manual to work with
 the new eithers elim

---
 heapster-saw/examples/linked_list_proofs.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/heapster-saw/examples/linked_list_proofs.v b/heapster-saw/examples/linked_list_proofs.v
index b1f366d81d..2ea2a67131 100644
--- a/heapster-saw/examples/linked_list_proofs.v
+++ b/heapster-saw/examples/linked_list_proofs.v
@@ -64,7 +64,7 @@ Lemma is_elem_fun_ref_manual : refinesFun is_elem is_elem_fun.
 Proof.
   unfold is_elem, is_elem__tuple_fun, is_elem_fun, sawLet_def.
   apply refinesFun_multiFixM_fst; intros x l.
-  apply refinesM_letRecM_Nil_l.
+  apply refinesM_letRecM_Nil_l. simpl.
   apply refinesM_either_l; intros [] e_either.
   all: destruct l; cbn [ unfoldList list_rect ] in *.
   all: try (injection e_either; intros; subst); try discriminate e_either.

From 88d624f47cb3e5c4f68cc31c2f386582e54aead6 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Tue, 14 Jun 2022 09:28:06 -0700
Subject: [PATCH 08/13] made the new rules for the eithers eliminator have
 higher priority in the Coq automation

---
 .../coq/handwritten/CryptolToCoq/CompMExtra.v | 34 +++++++++----------
 1 file changed, 17 insertions(+), 17 deletions(-)

diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/CompMExtra.v b/saw-core-coq/coq/handwritten/CryptolToCoq/CompMExtra.v
index b6e63f4e08..a0d793057a 100644
--- a/saw-core-coq/coq/handwritten/CryptolToCoq/CompMExtra.v
+++ b/saw-core-coq/coq/handwritten/CryptolToCoq/CompMExtra.v
@@ -460,12 +460,12 @@ Hint Extern 1 (_ |= SAWCorePrelude.eithers
                       _ (SAWCorePrelude.FunsTo_Cons
                            _ _ _ (SAWCorePrelude.FunsTo_Nil _)) _) =>
   simple apply refinesM_eithers_one_r : refinesM.
-Hint Extern 1 (SAWCorePrelude.eithers
+Hint Extern 2 (SAWCorePrelude.eithers
                  _ (SAWCorePrelude.FunsTo_Cons
                       _ _ _ (SAWCorePrelude.FunsTo_Cons
                                _ _ _ (SAWCorePrelude.FunsTo_Nil _))) _ |= _) =>
   simple apply refinesM_eithers_cons_l_IntroArg : refinesM.
-Hint Extern 1 (_ |= SAWCorePrelude.eithers
+Hint Extern 2 (_ |= SAWCorePrelude.eithers
                       _ (SAWCorePrelude.FunsTo_Cons
                            _ _ _ (SAWCorePrelude.FunsTo_Cons
                                     _ _ _ (SAWCorePrelude.FunsTo_Nil _))) _) =>
@@ -483,9 +483,9 @@ Definition refinesM_maybe_r_IntroArg {A B} (x : CompM B) (f : A -> CompM B) mb P
     FreshIntroArg Maybe (mb = SAWCorePrelude.Just _ a) (fun _ => P |= f a))) ->
   P |= SAWCorePrelude.maybe _ _ x f mb := refinesM_maybe_r x f mb P.
 
-Hint Extern 1 (SAWCorePrelude.maybe _ _ _ _ _ |= _) =>
+Hint Extern 2 (SAWCorePrelude.maybe _ _ _ _ _ |= _) =>
   simple apply refinesM_maybe_l_IntroArg : refinesM.
-Hint Extern 1 (_ |= SAWCorePrelude.maybe _ _ _ _ _) =>
+Hint Extern 2 (_ |= SAWCorePrelude.maybe _ _ _ _ _) =>
   simple apply refinesM_maybe_r_IntroArg : refinesM.
 
 Definition refinesM_sigT_rect_l_IntroArg {A1 A2 B} F P (s: {x:A1 & A2 x}) :
@@ -498,9 +498,9 @@ Definition refinesM_sigT_rect_r_IntroArg {A1 A2 B} F P (s: {x:A1 & A2 x}) :
     FreshIntroArg SigT (s = existT _ a1 a2) (fun _ => P |= F a1 a2)))) ->
   P |= sigT_rect (fun _ => CompM B) F s := refinesM_sigT_rect_r F P s.
 
-Hint Extern 1 (sigT_rect (fun _ => CompM _) _ _ |= _) =>
+Hint Extern 2 (sigT_rect (fun _ => CompM _) _ _ |= _) =>
   simple apply refinesM_sigT_rect_l_IntroArg : refinesM.
-Hint Extern 1 (_ |= sigT_rect (fun _ => CompM _) _ _) =>
+Hint Extern 2 (_ |= sigT_rect (fun _ => CompM _) _ _) =>
   simple apply refinesM_sigT_rect_r_IntroArg : refinesM.
 
 Definition refinesM_if_l_IntroArg {A} (m1 m2:CompM A) b P :
@@ -512,9 +512,9 @@ Definition refinesM_if_r_IntroArg {A} (m1 m2:CompM A) b P :
   (FreshIntroArg If (b = false) (fun _ => P |= m2)) ->
   P |= (if b then m1 else m2) := refinesM_if_r m1 m2 b P.
 
-Hint Extern 1 ((if _ then _ else _) |= _) =>
+Hint Extern 2 ((if _ then _ else _) |= _) =>
   apply refinesM_if_l_IntroArg : refinesM.
-Hint Extern 1 (_ |= (if _ then _ else _)) =>
+Hint Extern 2 (_ |= (if _ then _ else _)) =>
   apply refinesM_if_r_IntroArg : refinesM.
 
 Hint Extern 1 (returnM (if _ then _ else _) |= _) =>
@@ -534,9 +534,9 @@ Hint Extern 1 (assertM _ >> _ |= _) =>
 Hint Extern 1 (_ |= assumingM _ _) =>
   simple eapply refinesM_assumingM_r_IntroArg : refinesM.
 
-Hint Extern 2 (_ |= assertM _ >> _) =>
+Hint Extern 3 (_ |= assertM _ >> _) =>
   simple eapply refinesM_bindM_assertM_r; shelve : refinesM.
-Hint Extern 2 (assumingM _ _ |= _) =>
+Hint Extern 3 (assumingM _ _ |= _) =>
   simple eapply refinesM_assumingM_l; shelve : refinesM.
 
 Definition refinesM_existsM_l_IntroArg A B (P: A -> CompM B) Q :
@@ -546,21 +546,21 @@ Definition refinesM_forallM_r_IntroArg {A B} P (Q: A -> CompM B) :
   (FreshIntroArg Forall _ (fun a => P |= (Q a))) -> P |= (forallM Q) :=
   refinesM_forallM_r P Q.
 
-Hint Extern 2 (existsM _ |= _) =>
+Hint Extern 3 (existsM _ |= _) =>
   simple apply refinesM_existsM_l_IntroArg : refinesM.
-Hint Extern 2 (_ |= forallM _) =>
+Hint Extern 3 (_ |= forallM _) =>
   simple apply refinesM_forallM_r_IntroArg : refinesM.
 
-Hint Extern 3 (_ |= existsM _) =>
+Hint Extern 4 (_ |= existsM _) =>
   simple eapply refinesM_existsM_r; shelve : refinesM.
-Hint Extern 3 (forallM _ |= _) =>
+Hint Extern 4 (forallM _ |= _) =>
   simple eapply refinesM_forallM_l; shelve : refinesM.
 
-Hint Extern 3 (returnM _ |= returnM _) =>
+Hint Extern 4 (returnM _ |= returnM _) =>
   apply refinesM_returnM; (reflexivity || shelve) : refinesM.
 
-Hint Extern 1 (orM _ _ |= _) => simple apply refinesM_orM_l : refinesM.
-Hint Extern 1 (_ |= andM _ _) => simple apply refinesM_andM_r : refinesM.
+Hint Extern 2 (orM _ _ |= _) => simple apply refinesM_orM_l : refinesM.
+Hint Extern 2 (_ |= andM _ _) => simple apply refinesM_andM_r : refinesM.
 (* Note: For the moment, we don't automatically apply refinesM_orM_r or
    refinesM_andM_l - use continue_prove_refinement_left and
    continue_prove_refinement_right. *)

From abf226caa5e7c8a83b20037efbf9a1dbddeb21cd Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Tue, 14 Jun 2022 17:16:14 -0700
Subject: [PATCH 09/13] updated Mr Solver to handle the new multi-way eithers
 eliminator

---
 src/SAWScript/Prover/MRSolver/Monad.hs  |  8 +++
 src/SAWScript/Prover/MRSolver/Solver.hs | 86 ++++++++++++++++++-------
 src/SAWScript/Prover/MRSolver/Term.hs   | 15 +++--
 3 files changed, 78 insertions(+), 31 deletions(-)

diff --git a/src/SAWScript/Prover/MRSolver/Monad.hs b/src/SAWScript/Prover/MRSolver/Monad.hs
index c7755839ea..4c16112756 100644
--- a/src/SAWScript/Prover/MRSolver/Monad.hs
+++ b/src/SAWScript/Prover/MRSolver/Monad.hs
@@ -589,6 +589,14 @@ mrApplyAll f args = liftSC2 scApplyAllBeta f args
 mrApply :: Term -> Term -> MRM Term
 mrApply f arg = mrApplyAll f [arg]
 
+-- | Build a constructor application in Mr. Monad
+mrCtorApp :: Ident -> [Term] -> MRM Term
+mrCtorApp = liftSC2 scCtorApp
+
+-- | Build a 'Term' for a global in Mr. Monad
+mrGlobalTerm :: Ident -> MRM Term
+mrGlobalTerm = liftSC1 scGlobalDef
+
 -- | Like 'scBvNat', but if given a bitvector literal it is converted to a
 -- natural number literal
 mrBvToNat :: Term -> Term -> MRM Term
diff --git a/src/SAWScript/Prover/MRSolver/Solver.hs b/src/SAWScript/Prover/MRSolver/Solver.hs
index 15915e1271..315df6e2e2 100644
--- a/src/SAWScript/Prover/MRSolver/Solver.hs
+++ b/src/SAWScript/Prover/MRSolver/Solver.hs
@@ -224,7 +224,11 @@ normComp (CompTerm t) =
     (isGlobalDef "Prelude.ite" -> Just (), [_, cond, then_tm, else_tm]) ->
       return $ Ite cond (CompTerm then_tm) (CompTerm else_tm)
     (isGlobalDef "Prelude.either" -> Just (), [ltp, rtp, _, f, g, eith]) ->
-      return $ Either (Type ltp) (Type rtp) (CompFunTerm f) (CompFunTerm g) eith
+      return $ Eithers [(Type ltp, CompFunTerm f),
+                        (Type rtp, CompFunTerm g)] eith
+    (isGlobalDef "Prelude.eithers" -> Just (),
+     [_, matchEitherElims -> Just elims, eith]) ->
+      return $ Eithers elims eith
     (isGlobalDef "Prelude.maybe" -> Just (), [tp, _, m, f, mayb]) ->
       do tp' <- case asApplyAll tp of
                   -- Always unfold: is_bvult, is_bvule
@@ -369,8 +373,8 @@ normBind (ReturnM t) k = applyNormCompFun k t
 normBind (ErrorM msg) _ = return (ErrorM msg)
 normBind (Ite cond comp1 comp2) k =
   return $ Ite cond (CompBind comp1 k) (CompBind comp2 k)
-normBind (Either ltp rtp f g t) k =
-  return $ Either ltp rtp (compFunComp f k) (compFunComp g k) t
+normBind (Eithers elims t) k =
+  return $ Eithers (map (\(tp,f) -> (tp, compFunComp f k)) elims) t
 normBind (MaybeElim tp m f t) k =
   return $ MaybeElim tp (CompBind m k) (compFunComp f k) t
 normBind (OrM comp1 comp2) k =
@@ -458,7 +462,29 @@ compToTerm (CompBind m f) =
 applyNormCompFun :: CompFun -> Term -> MRM NormComp
 applyNormCompFun f arg = applyCompFun f arg >>= normComp
 
--- | Apply a 'Comp
+-- | Match a term as a static list of eliminators for an Eithers type
+matchEitherElims :: Term -> Maybe [EitherElim]
+matchEitherElims (asCtor ->
+                  Just (primName -> "Prelude.FunsTo_Nil", [_])) = Just []
+matchEitherElims (asCtor -> Just (primName -> "Prelude.FunsTo_Cons",
+                                  [_, tp, f, rest])) =
+  ((Type tp, CompFunTerm f):) <$>
+  matchEitherElims rest
+matchEitherElims _ = Nothing
+
+-- | Construct the type @Eithers tps@ eliminated by a list of 'EitherElim's
+elimsEithersType :: [EitherElim] -> MRM Type
+elimsEithersType elims =
+  Type <$>
+  (do f <- mrGlobalTerm "Prelude.Eithers"
+      tps <-
+        foldr
+        (\(Type tp,_) restM ->
+          restM >>= \rest -> mrCtorApp "Prelude.LS_Cons" [tp,rest])
+        (mrCtorApp "Prelude.LS_Nil" [])
+        elims
+      mrApply f tps)
+
 
 {- FIXME: do these go away?
 -- | Lookup the definition of a function or throw a 'CannotLookupFunDef' if this is
@@ -785,38 +811,50 @@ mrRefines' m1 (Ite cond2 m2 m2') =
     _ -> withAssumption cond2 (mrRefines m1 m2) >>
          withAssumption not_cond2 (mrRefines m1 m2')
 
-mrRefines' (Either ltp1 rtp1 f1 g1 t1) m2 =
+mrRefines' (Eithers [] _) _ = return ()
+mrRefines' _ (Eithers [] _) = return ()
+mrRefines' (Eithers [(_,f)] t1) m2 =
+  applyNormCompFun f t1 >>= \m1 ->
+  mrRefines m1 m2
+mrRefines' m1 (Eithers [(_,f)] t2) =
+  applyNormCompFun f t2 >>= \m2 ->
+  mrRefines m1 m2
+
+mrRefines' (Eithers ((tp,f1):elims) t1) m2 =
   mrNormOpenTerm t1 >>= \t1' ->
   mrGetDataTypeAssump t1' >>= \mb_assump ->
   case (mb_assump, asEither t1') of
     (_, Just (Left  x)) -> applyNormCompFun f1 x >>= flip mrRefines m2
-    (_, Just (Right x)) -> applyNormCompFun g1 x >>= flip mrRefines m2
+    (_, Just (Right x)) -> mrRefines (Eithers elims x) m2
     (Just (IsLeft  x), _) -> applyNormCompFun f1 x >>= flip mrRefines m2
-    (Just (IsRight x), _) -> applyNormCompFun g1 x >>= flip mrRefines m2
+    (Just (IsRight x), _) -> mrRefines (Eithers elims x) m2
     _ -> let lnm = maybe "x_left" id (compFunVarName f1)
-             rnm = maybe "x_right" id (compFunVarName g1)
-         in withUVarLift lnm ltp1 (f1, t1', m2) (\x (f1', t1'', m2') ->
-             applyNormCompFun f1' x >>= withDataTypeAssump t1'' (IsLeft x)
-                                        . flip mrRefines m2') >>
-            withUVarLift rnm rtp1 (g1, t1', m2) (\x (g1', t1'', m2') ->
-             applyNormCompFun g1' x >>= withDataTypeAssump t1'' (IsRight x)
-                                        . flip mrRefines m2')
-mrRefines' m1 (Either ltp2 rtp2 f2 g2 t2) =
+             rnm = "x_right" in
+         elimsEithersType elims >>= \elims_tp ->
+         withUVarLift lnm tp (f1, t1', m2) (\x (f1', t1'', m2') ->
+           applyNormCompFun f1' x >>= withDataTypeAssump t1'' (IsLeft x)
+                                      . flip mrRefines m2') >>
+         withUVarLift rnm elims_tp (elims, t1', m2)
+           (\x (elims', t1'', m2') ->
+             withDataTypeAssump t1'' (IsRight x) (mrRefines (Eithers elims' x) m2'))
+
+mrRefines' m1 (Eithers ((tp,f2):elims) t2) =
   mrNormOpenTerm t2 >>= \t2' ->
   mrGetDataTypeAssump t2' >>= \mb_assump ->
   case (mb_assump, asEither t2') of
     (_, Just (Left  x)) -> applyNormCompFun f2 x >>= mrRefines m1
-    (_, Just (Right x)) -> applyNormCompFun g2 x >>= mrRefines m1
+    (_, Just (Right x)) -> mrRefines m1 (Eithers elims x)
     (Just (IsLeft  x), _) -> applyNormCompFun f2 x >>= mrRefines m1
-    (Just (IsRight x), _) -> applyNormCompFun g2 x >>= mrRefines m1
+    (Just (IsRight x), _) -> mrRefines m1 (Eithers elims x)
     _ -> let lnm = maybe "x_left" id (compFunVarName f2)
-             rnm = maybe "x_right" id (compFunVarName g2)
-         in withUVarLift lnm ltp2 (f2, t2', m1) (\x (f2', t2'', m1') ->
-             applyNormCompFun f2' x >>= withDataTypeAssump t2'' (IsLeft x)
-                                        . mrRefines m1') >>
-            withUVarLift rnm rtp2 (g2, t2', m1) (\x (g2', t2'', m1') ->
-             applyNormCompFun g2' x >>= withDataTypeAssump t2'' (IsRight x)
-                                        . mrRefines m1')
+             rnm = "x_right" in
+         elimsEithersType elims >>= \elims_tp ->
+         withUVarLift lnm tp (f2, t2', m1) (\x (f2', t2'', m1') ->
+           applyNormCompFun f2' x >>= withDataTypeAssump t2'' (IsLeft x)
+                                      . mrRefines m1') >>
+         withUVarLift rnm elims_tp (elims, t2', m1)
+           (\x (elims', t2'', m1') ->
+             withDataTypeAssump t2'' (IsRight x) (mrRefines m1' (Eithers elims' x)))
 
 mrRefines' m1 (AssumingM cond2 m2) =
   withAssumption cond2 $ mrRefines m1 m2
diff --git a/src/SAWScript/Prover/MRSolver/Term.hs b/src/SAWScript/Prover/MRSolver/Term.hs
index 5ce92c0cb6..b29373b064 100644
--- a/src/SAWScript/Prover/MRSolver/Term.hs
+++ b/src/SAWScript/Prover/MRSolver/Term.hs
@@ -115,7 +115,7 @@ data NormComp
   = ReturnM Term -- ^ A term @returnM a x@
   | ErrorM Term -- ^ A term @errorM a str@
   | Ite Term Comp Comp -- ^ If-then-else computation
-  | Either Type Type CompFun CompFun Term -- ^ A sum elimination
+  | Eithers [EitherElim] Term -- ^ A multi-way sum elimination
   | MaybeElim Type Comp CompFun Term -- ^ A maybe elimination
   | OrM Comp Comp -- ^ an @orM@ computation
   | AssertingM Term Comp -- ^ an @assertingM@ computation
@@ -126,6 +126,10 @@ data NormComp
     -- ^ Bind a monadic function with @N@ arguments in an @a -> CompM b@ term
   deriving (Generic, Show)
 
+-- | An eliminator for an @Eithers@ type is a pair of the type of the disjunct
+-- and a function from that type to the output type
+type EitherElim = (Type,CompFun)
+
 -- | A computation function of type @a -> CompM b@ for some @a@ and @b@
 data CompFun
      -- | An arbitrary term
@@ -499,12 +503,9 @@ instance PrettyInCtx NormComp where
   prettyInCtx (Ite cond t1 t2) =
     prettyAppList [return "ite", return "_", parens <$> prettyInCtx cond,
                    parens <$> prettyInCtx t1, parens <$> prettyInCtx t2]
-  prettyInCtx (Either ltp rtp f g eith) =
-    prettyAppList [return "either",
-                   parens <$> prettyInCtx ltp, parens <$> prettyInCtx rtp,
-                   return (parens "CompM _"),
-                   parens <$> prettyInCtx f, parens <$> prettyInCtx g,
-                   parens <$> prettyInCtx eith]
+  prettyInCtx (Eithers elims eith) =
+    prettyAppList [return "eithers", return (parens "CompM _"),
+                   prettyInCtx (map snd elims), parens <$> prettyInCtx eith]
   prettyInCtx (MaybeElim tp m f mayb) =
     prettyAppList [return "maybe", parens <$> prettyInCtx tp,
                    return (parens "CompM _"), parens <$> prettyInCtx m,

From 925ae3515db585873413ce03f6e49fd7fa6c34e7 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Wed, 15 Jun 2022 15:28:24 -0700
Subject: [PATCH 10/13] changed the SImpl_ElimLLVMBlockOr to eliminate nested
 or shapes to or permissions, rather than just the top one

---
 .../src/Verifier/SAW/Heapster/Implication.hs  | 38 +++++++++++--------
 1 file changed, 22 insertions(+), 16 deletions(-)

diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
index 0f33cf91e3..824f032cab 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
@@ -1192,14 +1192,16 @@ data SimplImpl ps_in ps_out where
     LLVMBlockPerm w -> PermExpr (LLVMShapeType w) ->
     SimplImpl (RNil :> LLVMPointerType w) (RNil :> LLVMPointerType w)
 
-  -- | Eliminate a block of shape @sh1 orsh sh2@ to a disjunction, where the
-  -- supplied 'LLVMBlockPerm' gives @sh1@ and the additional argument is @sh2@::
+  -- | Eliminate a block of shape @sh1 orsh (sh2 orsh (... orsh shn))@ to an
+  -- n-way disjunctive permission, where the shape of the supplied
+  -- 'LLVMBlockPerm' is ignored, and is replaced by the list of shapes, which
+  -- must be non-empty:
   --
-  -- > x:memblock(rw,l,off,len,sh1 orsh sh2)
-  -- >   -o x:memblock(rw,l,off,len,sh1) or memblock(rw,l,off,len,sh2)
+  -- > x:memblock(rw,l,off,len,sh1 orsh (... orsh shn))
+  -- >   -o x:memblock(rw,l,off,len,sh1) or (... or memblock(rw,l,off,len,shn))
   SImpl_ElimLLVMBlockOr ::
     (1 <= w, KnownNat w) => ExprVar (LLVMPointerType w) ->
-    LLVMBlockPerm w -> PermExpr (LLVMShapeType w) ->
+    LLVMBlockPerm w -> [PermExpr (LLVMShapeType w)] ->
     SimplImpl (RNil :> LLVMPointerType w) (RNil :> LLVMPointerType w)
 
   -- | Prove a block of shape @exsh z:A.sh@ from an existential:
@@ -2145,10 +2147,9 @@ simplImplIn (SImpl_IntroLLVMBlockOr x bp1 sh2) =
   distPerms1 x (ValPerm_Or
                 (ValPerm_Conj1 $ Perm_LLVMBlock bp1)
                 (ValPerm_Conj1 $ Perm_LLVMBlock $ bp1 { llvmBlockShape = sh2 }))
-simplImplIn (SImpl_ElimLLVMBlockOr x bp1 sh2) =
-  let sh1 = llvmBlockShape bp1 in
+simplImplIn (SImpl_ElimLLVMBlockOr x bp shs) =
   distPerms1 x (ValPerm_Conj1 $ Perm_LLVMBlock $
-                bp1 { llvmBlockShape = PExpr_OrShape sh1 sh2 })
+                bp { llvmBlockShape = foldr1 PExpr_OrShape shs })
 simplImplIn (SImpl_IntroLLVMBlockEx x bp) =
   case llvmBlockShape bp of
     PExpr_ExShape mb_sh ->
@@ -2544,10 +2545,10 @@ simplImplOut (SImpl_IntroLLVMBlockOr x bp1 sh2) =
   let sh1 = llvmBlockShape bp1 in
   distPerms1 x (ValPerm_Conj1 $ Perm_LLVMBlock $
                 bp1 { llvmBlockShape = PExpr_OrShape sh1 sh2 })
-simplImplOut (SImpl_ElimLLVMBlockOr x bp1 sh2) =
-  distPerms1 x (ValPerm_Or
-                (ValPerm_Conj1 $ Perm_LLVMBlock bp1)
-                (ValPerm_Conj1 $ Perm_LLVMBlock $ bp1 { llvmBlockShape = sh2 }))
+simplImplOut (SImpl_ElimLLVMBlockOr x bp shs) =
+  distPerms1 x $
+  foldr1 ValPerm_Or $
+  map (\sh -> ValPerm_Conj1 $ Perm_LLVMBlock $ bp { llvmBlockShape = sh }) shs
 simplImplOut (SImpl_IntroLLVMBlockEx x bp) =
   distPerms1 x (ValPerm_LLVMBlock bp)
 simplImplOut (SImpl_ElimLLVMBlockEx x bp) =
@@ -3130,8 +3131,8 @@ instance SubstVar PermVarSubst m =>
     [nuMP| SImpl_IntroLLVMBlockOr x bp1 sh2 |] ->
       SImpl_IntroLLVMBlockOr <$> genSubst s x <*> genSubst s bp1
                              <*> genSubst s sh2
-    [nuMP| SImpl_ElimLLVMBlockOr x bp1 sh2 |] ->
-      SImpl_ElimLLVMBlockOr <$> genSubst s x <*> genSubst s bp1 <*> genSubst s sh2
+    [nuMP| SImpl_ElimLLVMBlockOr x bp shs |] ->
+      SImpl_ElimLLVMBlockOr <$> genSubst s x <*> genSubst s bp <*> genSubst s shs
     [nuMP| SImpl_IntroLLVMBlockEx x bp |] ->
       SImpl_IntroLLVMBlockEx <$> genSubst s x <*> genSubst s bp
     [nuMP| SImpl_ElimLLVMBlockEx x bp |] ->
@@ -5442,8 +5443,8 @@ implElimLLVMBlock x bp@(LLVMBlockPerm { llvmBlockShape =
 
 -- For an or shape, eliminate to a disjunctive permisison
 implElimLLVMBlock x bp@(LLVMBlockPerm { llvmBlockShape =
-                                        PExpr_OrShape sh1 sh2 }) =
-  implSimplM Proxy (SImpl_ElimLLVMBlockOr x (bp { llvmBlockShape = sh1 }) sh2)
+                                        PExpr_OrShape sh1 (matchOrShapes -> shs) }) =
+  implSimplM Proxy (SImpl_ElimLLVMBlockOr x bp (sh1:shs))
 
 -- For an existential shape, eliminate to an existential permisison
 implElimLLVMBlock x bp@(LLVMBlockPerm { llvmBlockShape =
@@ -5460,6 +5461,11 @@ implElimLLVMBlock _ bp =
                     permPretty i (Perm_LLVMBlock bp)) >>>=
   implFailM
 
+-- | Destruct a shape @sh1 orsh (sh2 orsh (... orsh shn))@ that is a
+-- right-nested disjunctive shape into the list @[sh1,...,shn]@ of disjuncts
+matchOrShapes :: PermExpr (LLVMShapeType w) -> [PermExpr (LLVMShapeType w)]
+matchOrShapes (PExpr_OrShape sh1 (matchOrShapes -> shs)) = sh1 : shs
+matchOrShapes sh = [sh]
 
 -- | Assume the top of the stack contains @x:ps@, which are all the permissions
 -- for @x@. Extract the @i@th conjuct from @ps@, which should be a @memblock@

From 32170ef2d131ba7e0320bd59aaee5edc47b4ac2b Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Thu, 16 Jun 2022 13:53:03 -0700
Subject: [PATCH 11/13] some small tweaks to the priorities of the
 prove_refinement rules

---
 saw-core-coq/coq/handwritten/CryptolToCoq/CompMExtra.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/CompMExtra.v b/saw-core-coq/coq/handwritten/CryptolToCoq/CompMExtra.v
index a0d793057a..ce8aece388 100644
--- a/saw-core-coq/coq/handwritten/CryptolToCoq/CompMExtra.v
+++ b/saw-core-coq/coq/handwritten/CryptolToCoq/CompMExtra.v
@@ -460,12 +460,12 @@ Hint Extern 1 (_ |= SAWCorePrelude.eithers
                       _ (SAWCorePrelude.FunsTo_Cons
                            _ _ _ (SAWCorePrelude.FunsTo_Nil _)) _) =>
   simple apply refinesM_eithers_one_r : refinesM.
-Hint Extern 2 (SAWCorePrelude.eithers
+Hint Extern 3 (SAWCorePrelude.eithers
                  _ (SAWCorePrelude.FunsTo_Cons
                       _ _ _ (SAWCorePrelude.FunsTo_Cons
                                _ _ _ (SAWCorePrelude.FunsTo_Nil _))) _ |= _) =>
   simple apply refinesM_eithers_cons_l_IntroArg : refinesM.
-Hint Extern 2 (_ |= SAWCorePrelude.eithers
+Hint Extern 3 (_ |= SAWCorePrelude.eithers
                       _ (SAWCorePrelude.FunsTo_Cons
                            _ _ _ (SAWCorePrelude.FunsTo_Cons
                                     _ _ _ (SAWCorePrelude.FunsTo_Nil _))) _) =>

From e052daeb10c14936dc094b20c9feb92ee8ae4b0e Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Thu, 16 Jun 2022 13:53:15 -0700
Subject: [PATCH 12/13] added two more bitvector lemmas

---
 .../coq/handwritten/CryptolToCoq/SAWCoreBitvectors.v        | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreBitvectors.v b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreBitvectors.v
index 70afd55686..4a5dad9cf1 100644
--- a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreBitvectors.v
+++ b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreBitvectors.v
@@ -243,6 +243,12 @@ Proof. holds_for_bits_up_to_3. Qed.
 
 (** Other lemmas about bitvector inequalities **)
 
+Definition not_isBvslt_bvsmin w a : ~ isBvslt w a (bvsmin w).
+Proof. holds_for_bits_up_to_3. Qed.
+
+Definition not_isBvslt_bvsmax w a : ~ isBvslt w (bvsmax w) a.
+Proof. holds_for_bits_up_to_3. Qed.
+
 Definition isBvslt_pred_l w a : isBvslt w (bvsmin w) a ->
                                 isBvslt w (bvSub w a (intToBv w 1)) a.
 Proof. holds_for_bits_up_to_3. Qed.

From 1d1d2a90263c748702fbeff57ead92a6ac9bb7c0 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Thu, 16 Jun 2022 13:53:32 -0700
Subject: [PATCH 13/13] got the mbox proofs working again after the multi-way
 eithers change

---
 heapster-saw/examples/mbox_proofs.v | 123 +++++++++++++++++++++-------
 1 file changed, 94 insertions(+), 29 deletions(-)

diff --git a/heapster-saw/examples/mbox_proofs.v b/heapster-saw/examples/mbox_proofs.v
index 21adb254ed..1d7e19a1e5 100644
--- a/heapster-saw/examples/mbox_proofs.v
+++ b/heapster-saw/examples/mbox_proofs.v
@@ -132,6 +132,11 @@ Proof.
     vm_compute in e_if0; discriminate e_if0.
   - rewrite e_assuming2, e_assuming3 in e_if0.
     vm_compute in e_if0; discriminate e_if0.
+  - destruct a; inversion e_either. destruct e_assuming; assumption.
+  - destruct a; inversion e_either. destruct e_assuming as [ Ha1 [ Ha2 Ha3 ]].
+    assumption.
+  - destruct a; inversion e_either. destruct e_assuming as [ Ha1 [ Ha2 Ha3 ]].
+    assumption.
 Qed.
 
 (*
@@ -216,6 +221,15 @@ Proof.
     prove_refinement.
     + exact a3.
     + prove_refinement.
+  - destruct a; try discriminate. reflexivity.
+  - destruct a; inversion e_either.
+    destruct e_assuming as [ Ha1 [ Ha2 Ha3 ]]. assumption.
+  - destruct a; inversion e_either.
+    destruct e_assuming as [ Ha1 [ Ha2 Ha3 ]]. assumption.
+  - destruct a; inversion e_either.
+    destruct e_assuming as [ Ha1 [ Ha2 Ha3 ]]. assumption.
+  - destruct a; inversion e_either. simpl. rewrite transMbox_Mbox_nil_r.
+    reflexivity.
 Qed.
 
 
@@ -241,6 +255,17 @@ Proof.
   (* Set Ltac Profiling. *)
   time "mbox_drop_spec_ref" prove_refinement.
   (* Show Ltac Profile. Reset Ltac Profile. *)
+  - simpl. destruct a; try discriminate e_either. reflexivity.
+  - simpl. destruct a; try discriminate e_either.
+    inversion e_either. simpl. rewrite <- H0 in e_if. simpl in e_if.
+    unfold isBvule in e_if. rewrite e_if. simpl.
+    repeat rewrite transMbox_Mbox_nil_r.
+    reflexivity.
+  - destruct a; simpl in e_either; inversion e_either.
+    rewrite <- H0 in e_if. simpl in e_if. simpl.
+    assert (bvule 64 v0 a0 = false); [ apply isBvult_def_opp; assumption | ].
+    rewrite H. simpl. rewrite transMbox_Mbox_nil_r.
+    reflexivity.
 Time Qed.
 
 
@@ -283,6 +308,9 @@ Proof.
   (* Set Ltac Profiling. *)
   time "mbox_concat_spec_ref" prove_refinement.
   (* Show Ltac Profile. Reset Ltac Profile. *)
+  - destruct a; simpl in e_either; try discriminate e_either. reflexivity.
+  - destruct a; simpl in e_either; inversion e_either.
+    rewrite transMbox_Mbox_nil_r. reflexivity.
 Time Qed.
 
 (* Add `mbox_concat_spec_ref` to the hint database. Unfortunately, Coq will not unfold refinesFun
@@ -319,7 +347,17 @@ Proof.
     exact (returnM (transMbox x (Mbox_cons strt len (transMbox next y) d))).
   unfold mbox_concat_chains_spec.
   time "mbox_concat_chains_spec_ref" prove_refinement.
-  simpl; repeat rewrite transMbox_Mbox_nil_r; reflexivity.
+  - destruct a5; simpl in e_either; inversion e_either.
+    repeat rewrite transMbox_Mbox_nil_r; reflexivity.
+  - destruct a5; simpl in e_either; inversion e_either.
+    repeat rewrite transMbox_Mbox_nil_r; reflexivity.
+  - destruct a; simpl in e_either; inversion e_either. reflexivity.
+  - destruct a; simpl in e_either; inversion e_either.
+    destruct a0; simpl in e_either0; inversion e_either0.
+    rewrite transMbox_Mbox_nil_r; reflexivity.
+  - destruct a; simpl in e_either; inversion e_either.
+    destruct a0; simpl in e_either0; inversion e_either0.
+    simpl; repeat rewrite transMbox_Mbox_nil_r; reflexivity.
 Time Qed.
 
 
@@ -343,6 +381,9 @@ Proof.
   (* Set Ltac Profiling. *)
   time "mbox_detach_spec_ref" prove_refinement.
   (* Show Ltac Profile. Reset Ltac Profile. *)
+  - destruct a; simpl in e_either; inversion e_either. reflexivity.
+  - destruct a; simpl in e_either; inversion e_either.
+    rewrite transMbox_Mbox_nil_r; reflexivity.
 Time Qed.
 
 (* Add `mbox_detach_spec_ref` to the hint database. Unfortunately, Coq will not unfold refinesFun
@@ -379,11 +420,13 @@ Proof.
   (* Set Ltac Profiling. *)
   time "mbox_len_spec_ref" prove_refinement.
   (* Show Ltac Profile. Reset Ltac Profile. *)
-  (* Most of the remaining cases are taken care of with just bvAdd_id_l and bvAdd_id_r *)
   all: try rewrite bvAdd_id_r; try rewrite bvAdd_id_l; try reflexivity.
-  (* The remaining case just needs a few more rewrites *)
-  - simpl. f_equal. rewrite bvAdd_assoc. f_equal. rewrite bvAdd_comm. f_equal.
-    simpl. rewrite transMbox_Mbox_nil_r. reflexivity.
+  - destruct a2; simpl in e_either; inversion e_either.
+    repeat rewrite transMbox_Mbox_nil_r. rewrite bvAdd_id_r. reflexivity.
+  - destruct a2; simpl in e_either; inversion e_either.
+    repeat rewrite transMbox_Mbox_nil_r. simpl.
+    rewrite bvAdd_assoc. rewrite (bvAdd_comm _ v0). reflexivity.
+  - repeat rewrite transMbox_Mbox_nil_r. reflexivity.
 Time Qed.
 
 
@@ -447,6 +490,13 @@ Definition mbox_copy_spec : Mbox -> CompM (Mbox * Mbox) :=
   Mbox__rec (fun _ => CompM  (Mbox * Mbox)) (returnM (Mbox_nil, Mbox_nil))
           (fun strt len m _ d => mbox_copy_spec_cons strt len m d).
 
+Lemma eithers2_either {A B C} (f: A -> C) (g: B -> C) e :
+  eithers _ (FunsTo_Cons _ _ f (FunsTo_Cons _ _ g (FunsTo_Nil _))) e =
+  either _ _ _ f g e.
+Proof.
+  destruct e; reflexivity.
+Qed.
+
 Lemma mbox_copy_spec_ref : refinesFun mbox_copy mbox_copy_spec.
 Proof.
   unfold mbox_copy, mbox_copy__tuple_fun, mboxNewSpec.
@@ -462,30 +512,45 @@ Proof.
   time "mbox_copy_spec_ref" prove_refinement with NoRewrite.
   (* Show Ltac Profile. Reset Ltac Profile. *)
   all: try discriminate e_either.
-  - rewrite e_forall in e_maybe.
-    discriminate e_maybe.
-  - rewrite e_forall0 in e_maybe0.
-    discriminate e_maybe0.
-  (* TODO Add the sort of reasoning in the next two cases back into the automation? *)
-
-  - rewrite a in e_maybe1.
-    discriminate e_maybe1.
-  - rewrite a1 in e_maybe2.
-    discriminate e_maybe2.
-  - rewrite transMbox_Mbox_nil_r. (* <- this would go away if we removed "NoRewrite" *)
-    replace a2 with e_forall; [ replace a3 with e_forall0 | ].
-    unfold conjSliceBVVec.
-    reflexivity.
-  - apply BoolDecidableEqDepSet.UIP.
-  - apply BoolDecidableEqDepSet.UIP.
-  - rewrite <- e_assuming in e_if.
-    vm_compute in e_if; discriminate e_if.
-  - rewrite <- isBvult_to_isBvslt_pos in e_if.
-    + rewrite e_forall in e_if.
-      vm_compute in e_if; discriminate e_if.
-    + reflexivity.
-    + apply isBvslt_to_isBvsle.
-      assumption.
+  - destruct a; simpl in e_either; inversion e_either. reflexivity.
+  - simpl in e_either0. discriminate e_either0.
+  - destruct a; simpl in e_either; inversion e_either. simpl.
+    apply refinesM_assumingM_r; intro.
+    apply refinesM_forallM_r; intro.
+    unfold isBvule in a2.
+    rewrite <- H0 in e_maybe; simpl in e_maybe.
+    rewrite a2 in e_maybe. simpl in e_maybe. discriminate e_maybe.
+  - destruct a; simpl in e_either; inversion e_either. simpl.
+    apply refinesM_assumingM_r; intro.
+    apply refinesM_forallM_r; intro.
+    apply refinesM_forallM_r; intro.
+    rewrite <- H0 in e_maybe0. simpl in e_maybe0.
+    unfold isBvule in a4; rewrite a4 in e_maybe0.
+    simpl in e_maybe0. discriminate e_maybe0.
+  - destruct a; simpl in e_either; inversion e_either. simpl.
+    apply refinesM_assumingM_r; intro.
+    apply refinesM_forallM_r; intro.
+    apply refinesM_forallM_r; intro.
+    rewrite <- H0 in e_maybe1. simpl in e_maybe1.
+    unfold isBvule in a4. rewrite a4 in e_maybe1.
+    simpl in e_maybe1. discriminate e_maybe1.
+  - destruct a; simpl in e_either; inversion e_either. simpl.
+    apply refinesM_assumingM_r; intro.
+    apply refinesM_forallM_r; intro.
+    apply refinesM_forallM_r; intro.
+    rewrite <- H0 in e_maybe2. simpl in e_maybe2.
+    unfold isBvule in a6. rewrite a6 in e_maybe2.
+    simpl in e_maybe2. discriminate e_maybe2.
+  - destruct a; simpl in e_either; inversion e_either. simpl.
+    prove_refinement with NoRewrite.
+    subst a0. simpl. repeat rewrite transMbox_Mbox_nil_r.
+    destruct a1; simpl in e_either0; inversion e_either0.
+    simpl. unfold conjSliceBVVec.
+    replace a4 with e_forall; [ replace a5 with e_forall0;
+                                [ reflexivity | ] | ];
+    apply BoolDecidableEqDepSet.UIP.
+  - elimtype False; apply (not_isBvslt_bvsmin _ _ e_if).
+  - elimtype False; apply (not_isBvslt_bvsmax _ _ e_if).
 Time Qed.
 
 Lemma no_errors_mbox_copy