diff --git a/Tactics/Attr.lean b/Tactics/Attr.lean
index e6b682e8..d73ecddd 100644
--- a/Tactics/Attr.lean
+++ b/Tactics/Attr.lean
@@ -15,6 +15,9 @@ initialize
   -- enable tracing for heartbeat usage of `sym_n`
   registerTraceClass `Tactic.sym.heartbeats
 
+  -- Matchgoal tactic's tracing.
+  registerTraceClass `Tactic.matchgoal
+
   -- enable extra checks for debugging `sym_n`,
   -- see `AxEffects.validate` for more detail on what is being type-checked
   registerOption `Tactic.sym.debug {
diff --git a/Tactics/CSE.lean b/Tactics/CSE.lean
index 6ce67914..612f1559 100644
--- a/Tactics/CSE.lean
+++ b/Tactics/CSE.lean
@@ -7,6 +7,7 @@ This file contains an experimental implementation of a common subexpression elim
 used to simplify goal states.
 -/
 import Lean
+import Std
 import Tactics.Attr
 import Lean.Meta.Tactic.Generalize
 open Lean Elab Tactic Expr Meta
@@ -132,7 +133,7 @@ structure State where
   /--
   A mapping from expression to its canonical index.
   -/
-  canon2data : HashMap Expr ExprData := {}
+  canon2data : Std.HashMap Expr ExprData := {}
   /--
   a counter to generate new names.
   -/
@@ -238,7 +239,7 @@ partial def CSEM.tryAddExpr (e : Expr) : CSEM (Option ExprData) := do
     -- the current argument itself was irrelevant, so don't bother adding it.
     if !relevant? then return .none
     let s ← getState
-    match s.canon2data.find? e with
+    match s.canon2data[e]? with
     | .some data => do
       let data := data.incrRef
       traceLargeMsg m!"updated expr (...) with info ({repr data})" m!"{e}"
@@ -324,7 +325,7 @@ def CSEM.cseImpl : CSEM Unit := do
         for hyp in (← getLocalHyps) do
           let _ ← tryAddExpr (← inferType hyp)
 
-    let newCanon2Data : HashMap Expr ExprData ←
+    let newCanon2Data : Std.HashMap Expr ExprData ←
       withTraceNode m!"⏭️ CSE eliminiating unprofitable expressions (#expressions:{(← getState).canon2data.size}):" do
         let mut newCanon2Data := {}
         for (e, data) in (← getState).canon2data.toArray.qsort (fun kv kv' => kv.2.occs > kv'.2.occs) do
diff --git a/Tactics/Matchgoal/Matchgoal.lean b/Tactics/Matchgoal/Matchgoal.lean
new file mode 100644
index 00000000..6168ca26
--- /dev/null
+++ b/Tactics/Matchgoal/Matchgoal.lean
@@ -0,0 +1,329 @@
+import Lean.Meta.Tactic.Rewrite
+import Lean.Meta.Tactic.Refl
+import Lean.Meta.Tactic.Simp
+import Lean.Meta.Tactic.Replace
+import Lean.Elab.Tactic.Basic
+import Lean.Elab.Tactic.Rewrite
+import Lean.Elab.Tactic.ElabTerm
+import Lean.Elab.Tactic.Location
+import Lean.Elab.Tactic.Config
+import Lean.PrettyPrinter
+import Lean.PrettyPrinter.Delaborator
+import Lean.Data.Json
+import Tactics.Attr
+-- import Matchgoal.Trace
+-- import Matchgoal.LogicT
+
+namespace MatchGoal
+
+open Lean Elab Meta Tactic Term Std RBMap
+
+/-- pattern of the hypothesis -/
+declare_syntax_cat pattern_hyp
+
+/-- pattern of 'term' variable #v -/
+declare_syntax_cat pattern_term_var
+
+/-- pattern of hypothesis variable '^H' -/
+declare_syntax_cat pattern_hyp_var -- pattern_term_ident maybe?
+
+/-- pattern of expressions -/
+declare_syntax_cat pattern_expr
+
+scoped syntax (name := term_var) "#" noWs ident : pattern_term_var
+scoped syntax (name := term_var_blank) "#_" : pattern_term_var
+scoped syntax (name := hyp_var) "^" noWs ident : pattern_hyp_var
+-- scoped syntax (name := hyp_var_blank) "^_" : pattern_term_var
+
+
+/- Names that are created from `#<name>` syntax. -/
+@[reducible]
+def PatternName := Name
+
+open Lean Elab in
+
+/-- every unification variable is a term. -/
+scoped elab (name := termvar2term) t:pattern_term_var : term => do
+  let s : Syntax ←
+    match t with
+    | `(pattern_term_var| #$i:ident) => pure i
+    | _ => throwUnsupportedSyntax
+  elabTerm s (expectedType? := .none)
+
+
+/-- every hypothesis variable is an ident. -/
+scoped elab (name := hypvar2ident) t:pattern_hyp_var : term => do
+  let s : Syntax ←
+    match t with
+    | `(pattern_hyp_var| ^$i:ident) => pure i
+    | _ => throwUnsupportedSyntax
+  elabTerm s (expectedType? := .none)
+
+
+/--  var -var2term-> term -term2expr-> expr -/
+scoped syntax (name := term2expr) (priority := 0)
+  term : pattern_expr
+
+scoped syntax (name := hyp)
+  "(" pattern_hyp_var ws ":" ws pattern_expr ")" : pattern_hyp
+
+scoped syntax (name := elabUnificationExpr)
+  "[pattern_expr|" pattern_expr "]" : term
+macro_rules
+| `([pattern_expr| $e:term]) => return e
+
+syntax hyps := sepBy(pattern_hyp, "; ")
+
+structure Depth where
+  depth : Nat := 0
+
+def Depth.increment (d: Depth) : Depth where
+  depth := d.depth + 1
+
+instance : ToString Depth where
+  toString d := Id.run do
+    let rec go (s : String) : Nat → String 
+    | 0 => s
+    | n' + 1 =>  go (s ++ " |") n'
+    go "" d.depth
+
+instance : ToMessageData Depth where
+  toMessageData d := toString d
+
+
+structure PatternHyp where
+  /-- for position information. TODO: pull position out of the raw Tsyntax? -/
+  nameStx : Syntax.Ident
+  rhs : TSyntax `pattern_expr
+
+-- @[computed_field] TODO: figure out how to use computed fields.
+def PatternHyp.name (p : PatternHyp) : Name  := p.nameStx.getId
+
+instance : ToMessageData PatternHyp where
+  toMessageData h := m!"{h.nameStx} : {h.rhs}"
+def PatternHyp.parse : TSyntax `pattern_hyp →  TacticM PatternHyp
+| `(pattern_hyp| (^$i: ident : $e:pattern_expr)) =>
+   return { nameStx := i, rhs := e }
+| stx => do
+  logErrorAt stx <| MessageData.tagged `Tactic.Matchgoal <| m! "unknown hypothesis pattern '{stx}'"
+  throwUnsupportedSyntax
+
+structure PatternCtx where
+  mvars : Std.HashMap PatternName Syntax := {}
+  /-- match hypothesis pattern names to their FVarIds in the local context --/
+  hyps : Std.HashMap PatternName (PatternHyp × FVarId) := {}
+deriving Inhabited
+
+instance : ToMessageData PatternCtx where
+  toMessageData pctx := Id.run do
+    let mvars := MessageData.ofList <| pctx.mvars.toList.map (fun (k, v) =>  m!"{k} ↦ {v}")
+    let hyps := MessageData.ofList <| pctx.hyps.toList.map fun (k, v) => m!"{k} ↦ {(v.snd.name)}"
+    m!"PatternCtx({mvars}, {hyps})"
+
+-- Match the syntax 's' against the syntax 't', where 's' is allowed to have patterns.
+partial def stxMatcher (depth : Depth) (pctx : PatternCtx) (s : Syntax) (t : Syntax): TacticM (Option PatternCtx) := do
+  trace[Tactic.matchgoal] "{depth}stxMatcher: '{s}' =?= '{t}'"
+  match s with 
+  | `(pattern_expr| $s':term) =>  do
+    trace[Tactic.matchgoal] "{depth}stxMatcher: SUCCESS pattern_expr unwrap."
+    stxMatcher depth pctx s' t
+  | `(pattern_term_var| #$i:ident) | `(term| #$i:ident) => do
+      match pctx.mvars.find? i.getId with
+      | .none => 
+        trace[Tactic.matchgoal] "{depth}stxMatcher: SUCCESS assigned #{i} := 't'"
+        return .some { pctx with mvars := pctx.mvars.insert i.getId t }
+      | .some mvarStx =>
+        match (← stxMatcher depth.increment pctx mvarStx t) with
+        | .none => 
+          trace[Tactic.matchgoal] "{depth}stxMatcher: FAILURE"
+          return .none
+        | .some pctx' =>
+          trace[Tactic.matchgoal] "{depth}stxMatcher: SUCCESS"
+          return .some pctx'
+  | _ =>
+    match s, t with
+    | Syntax.missing, Syntax.missing => do 
+      trace[Tactic.matchgoal] "{depth}stxMatcher: SUCCESS"
+      return .some pctx
+    | Syntax.atom  (val := sval) ..  , Syntax.atom (val := tval) .. =>
+      let sval := sval.trim
+      let tval := tval.trim
+      if sval = tval then
+        trace[Tactic.matchgoal] "{depth}stxMatcher: SUCCESS atom '{sval}' = '{tval}'"
+        return .some pctx
+      else
+        trace[Tactic.matchgoal] "{depth}stxMatcher: FAILURE atom '{sval}' /= '{tval}'"
+        return .none
+    | Syntax.ident (val := sval) .., .ident (val := tval) .. =>
+      if sval = tval then
+        trace[Tactic.matchgoal] "{depth}stxMatcher: SUCCESS ident '{sval}' = '{tval}'"
+        return .some pctx
+      else 
+        trace[Tactic.matchgoal] "{depth}stxMatcher: FAILURE ident '{sval}' /= '{tval}'"
+        return .none
+    | .node (kind := skind) (args := sargs) .., .node (kind := tkind) (args := targs) .. => do
+        if skind != tkind then
+          trace[Tactic.matchgoal] "{depth}stxMatcher: FAILURE node '{skind}' /= '{tkind}'"
+          return .none
+        else
+          let mut pctx := pctx
+          for (sarg, targ) in sargs.zip targs do
+            match ← stxMatcher depth.increment pctx sarg targ with
+            | .none => return .none
+            | .some pctx' => pctx := pctx'
+          return .some pctx
+    | _, _ => return .none
+
+open Lean Elab Macro Tactic in
+/--
+Replace holes in the Syntax given by `pattern_var` with the values in ctx
+TODO: We need to know if we should replace `MVars` or
+`Name`s. In the hypothesis manipulation, we should replace MVarIds.
+For the final proof production, we should replace `Names` ? -/
+-- TODO: replace with 'replacer'?
+partial def replace (pctx : PatternCtx) (s : Syntax) : TacticM (Option Syntax) := do
+  -- trace[Tactic.matchgoal] "replace s:'{toString s}'"
+  match s with
+  | `(pattern_term_var| #$i:ident) | `(term| #$i:ident) => do
+     trace[Tactic.matchgoal] "replace in ident '{i}'"
+      match pctx.mvars.find? i.getId with
+      | .none => do
+          -- TODO: this can be verified statically?
+         trace[Tactic.matchgoal.search] m!"Matchgoal variable {i} has not been unified when replacing syntax '{s}'. This is an error."
+         logErrorAt s <|
+           MessageData.tagged `Tactic.Matchgoal <|
+           m!"Matchgoal variable {i} has not been unified when replacing syntax '{s}'. This is an error."
+         return .none
+      | .some stx => return stx
+  | `(pattern_hyp_var| ^$i:ident) | `(term| ^$i:ident) => do
+      match pctx.hyps.find? i.getId with
+      | .none => do
+         trace[Tactic.matchgoal.search] m!"Matchgoal hypothesis variable {i} has not been unified when replacing syntax '{s}'. This is an error."
+         return .none
+      | .some (hypPat, _) => do return hypPat.nameStx
+  | _ =>
+    match s with
+    | Syntax.node info kind args => do
+        let mut args' := #[]
+        for a in args do
+           match ← replace pctx a with
+           | .some a' => args' := args'.push a'
+           | .none => return .none
+        return Syntax.node info kind args'
+    | Syntax.missing | Syntax.atom .. | Syntax.ident .. => return s
+
+
+
+open Lean Core Elab Meta Macro Tactic PrettyPrinter in
+def PatternHyp.matcher (depth : Depth) ( pctx: PatternCtx)
+  (hpat : PatternHyp)
+  (ldecl: LocalDecl) : TacticM (Option PatternCtx) := do
+    let mut pctx := pctx
+    let ldeclType : Expr := ldecl.type
+    let ldeclStx : Syntax ← delab ldeclType
+    match (← stxMatcher depth.increment pctx hpat.rhs.raw ldeclStx) with 
+    | .none => 
+      trace[Tactic.matchgoal.matcher] "FAILURE: PatternHyp.matcher {pctx} : {hpat} =!= {ldeclStx}"
+      return .none
+    | .some pctx' => 
+      trace[Tactic.matchgoal.matcher] "SUCCESS: PatternHyp.matcher {pctx} : {hpat} === {ldeclStx}"
+      pctx := pctx'
+        -- Convert the given goal `Ctx |- target` into `Ctx |- type -> target`.
+        -- let newgoal ← (← getMainGoal).assert hpat.name ldeclType hpatexpr
+        let newgoal ← (← getMainGoal).assert hpat.name ldeclType ldecl.toExpr
+        -- `intros` the arrow.
+        let (hypFVar, newgoal) ← newgoal.intro1P
+        replaceMainGoal [newgoal]
+        return (.some { pctx with hyps := pctx.hyps.insert hpat.name (hpat, hypFVar) })
+
+
+
+open Lean Core Meta Elab Macro Tactic PrettyPrinter in
+/-- The search state of the backtracking depth first search. -/
+def depthFirstSearchHyps
+  (depth : Depth)
+  (tac : TSyntax `tactic)
+  (hyppats : List PatternHyp)
+  (pctx : PatternCtx)
+  (gpat? : Option (TSyntax `pattern_expr)): TacticM Bool :=  do
+  trace[Tactic.matchgoal.search] m!"==={depth.depth}==="
+  trace[Tactic.matchgoal.search] m!"{depth}STEP: depthFirstSearchHyps {hyppats}"
+  match hyppats with
+  | [] => do
+     let stateBeforeMatcher ← Tactic.saveState
+     let mut pctx := pctx
+     if let .some gpat := gpat? then
+       -- Do not do this in two steps: do the matching and the elaboration in the same step.
+       let mainTargetStx ← delab (← getMainTarget)
+       trace[Tactic.matchgoal.search] m!"{depth}STEP: '{gpat}' =?= '{mainTargetStx}'"
+       match ← stxMatcher depth pctx gpat mainTargetStx with 
+       | .none =>  
+          trace[Tactic.matchgoal.search] m!"{depth}FAILED '{gpat} =/= '{mainTargetStx}'"
+          logErrorAt gpat
+            <| MessageData.tagged `Tactic.Matchgoal <|
+              m! "unable to match '{gpat}' =?= '{mainTargetStx}'"
+          restoreState stateBeforeMatcher
+          return False
+       | .some pctx' =>
+          pctx := pctx'
+          trace[Tactic.matchgoal.search] m!"{depth}SUCCESS '{gpat} === '{mainTargetStx}'"
+     trace[Tactic.matchgoal.search] m!"{depth}STEP: preparing to run tactic '{tac}'."
+     trace[Tactic.matchgoal.search] m!"{depth}replacing '{tac}' with context {pctx}" -- TODO: make {ctx} nested
+     let tac ← match ← replace pctx tac with
+        | .some t => 
+          trace[Tactic.matchgoal.search] m!"{depth}SUCCESS: replaced with {t}"
+          pure t
+        | .none =>
+          trace[Tactic.matchgoal.search] m!"{depth}FAILED: no replacement generated"
+          restoreState stateBeforeMatcher
+          return False
+
+     trace[Tactic.matchgoal.search] m!"{depth}STEP: running tactic '{tac}'."
+     if ← tryTactic (evalTactic tac) then
+        trace[Tactic.matchgoal.search] m!"{depth}SUCCESS running '{tac}'."
+        return true
+     else
+        trace[Tactic.matchgoal.search] m!"FAILURE running '{tac}'."
+        restoreState stateBeforeMatcher
+        return false
+  | hyppat :: hyppats' =>
+     let stateBeforeMatcher ← Tactic.saveState
+     for hyp in (← getMainDecl).lctx do
+       if hyp.isImplementationDetail then continue
+       stateBeforeMatcher.restore -- Paranoia. This should ideally not be necessary.
+       if let .some ctx'  ← hyppat.matcher depth.increment pctx hyp then
+         if  (← depthFirstSearchHyps depth.increment tac hyppats' ctx' gpat?) then
+          return true
+     stateBeforeMatcher.restore -- Paranoia. This should ideally not be necessary.
+     return False
+
+/-- match goal tactic -/
+-- local syntax (name := matchgoal)
+scoped syntax (name := matchgoal)
+  "matchgoal" ws
+  (hyps ws)?
+  "⊢" ws (( pattern_expr ws)?) "=>" ws tactic : tactic
+
+-- foobar [[ ident ]] : tactic
+open Lean Core Meta Elab Macro Tactic in
+@[tactic MatchGoal.matchgoal]
+def evalMatchgoal : Tactic := fun stx => -- (stx -> TacticM Unit)
+  -- if stx.kind == node and stx[0] == "matchgoal and stx[1] == ....
+  match stx with
+  | `(tactic| matchgoal
+      $[ $[ $hpatstxs? ];* ]?
+      ⊢ $[ $gpat?:pattern_expr ]? => $tac:tactic ) => do
+    trace[Tactic.matchgoal] m!"{toString gpat?}"
+    let mut pctx : PatternCtx := default
+    let hpats : List PatternHyp ← match hpatstxs? with
+         | .none => pure []
+         | .some stxs => stxs.toList.mapM PatternHyp.parse
+    let success ← depthFirstSearchHyps (depth := Depth.mk 0) tac hpats pctx gpat?
+    match success with
+    | true => return ()
+    | false => throwError m!"matchgoal backtracking search exhaustively failed. Giving up up on '{stx}'."
+    -- then logErrorAt stx <| MessageData.tagged `Tactic.Matchgoal m!"matchgoal failed to find any match"
+  | _ => throwUnsupportedSyntax
+
+end MatchGoal
+
diff --git a/Tactics/Reflect/ProgramInfo.lean b/Tactics/Reflect/ProgramInfo.lean
index 99e3cc71..d7903a1b 100644
--- a/Tactics/Reflect/ProgramInfo.lean
+++ b/Tactics/Reflect/ProgramInfo.lean
@@ -5,6 +5,7 @@ Author(s): Alex Keizer
 -/
 import Arm.Map
 import Tactics.Common
+import Std
 
 /-!
 # ProgramInfo
@@ -61,7 +62,7 @@ structure InstInfo where
 
 structure ProgramInfo where
   name : Name
-  instructions : HashMap (BitVec 64) InstInfo
+  instructions : Std.HashMap (BitVec 64) InstInfo
 
 --------------------------------------------------------------------------------
 
@@ -115,14 +116,14 @@ def expr (pi : ProgramInfo) : Expr := mkConst pi.name
 
 def getInstInfoAt? (pi : ProgramInfo) (addr : BitVec 64) :
     Option InstInfo :=
-  pi.instructions.find? addr
+  pi.instructions[addr]?
 
 def getRawInstAt? (pi : ProgramInfo) (addr : BitVec 64) :
     Option (BitVec 32) :=
   (·.rawInst) <$> pi.getInstInfoAt? addr
 
 -- TODO: this instance could be upstreamed (after cleaning it up)
-instance [BEq α] [Hashable α] : ForIn m (HashMap α β) (α × β) where
+instance [BEq α] [Hashable α] : ForIn m (Std.HashMap α β) (α × β) where
   forIn map acc f := do
     let f := fun (acc : ForInStep _) key val => do
       match acc with
@@ -141,7 +142,7 @@ partial def generateFromExpr (name : Name) (e : Expr) : MetaM ProgramInfo := do
   if !(←isDefEq type (mkConst ``Program)) then
     throwError "type mismatch: {e} {← mkHasTypeButIsExpectedMsg type (mkConst ``Program)}"
 
-  let rec go (instructions : HashMap _ _) (e : Expr) : MetaM (HashMap _ _) := do
+  let rec go (instructions : Std.HashMap _ _) (e : Expr) : MetaM (Std.HashMap _ _) := do
     let e ← whnfD e
     match_expr e with
     | List.cons _ hd tl => do
diff --git a/Tests/Tactics/CSE.lean b/Tests/Tactics/CSE.lean
index f0893580..ce4222d1 100644
--- a/Tests/Tactics/CSE.lean
+++ b/Tests/Tactics/CSE.lean
@@ -134,14 +134,14 @@ info: [Tactic.cse.summary] CSE collecting hypotheses:
     [Tactic.cse.summary] expr: y
   [Tactic.cse.summary] ⏭️ Unprofitable { occs := 2, size := 1 } . (NOTE: can be large)
     [Tactic.cse.summary] expr: x
-  [Tactic.cse.summary] ⏭️ Unprofitable { occs := 1, size := 23 } . (NOTE: can be large)
-    [Tactic.cse.summary] expr: y + y + (y + y) + (y + y + (y + y)) + (y + y + (y + y))
   [Tactic.cse.summary] ⏭️ Unprofitable { occs := 1, size := 3 } . (NOTE: can be large)
     [Tactic.cse.summary] expr: x + x
-  [Tactic.cse.summary] ⏭️ Unprofitable { occs := 1, size := 15 } . (NOTE: can be large)
-    [Tactic.cse.summary] expr: y + y + (y + y) + (y + y + (y + y))
+  [Tactic.cse.summary] ⏭️ Unprofitable { occs := 1, size := 23 } . (NOTE: can be large)
+    [Tactic.cse.summary] expr: y + y + (y + y) + (y + y + (y + y)) + (y + y + (y + y))
   [Tactic.cse.summary] ⏭️ Unprofitable { occs := 1, size := 11 } . (NOTE: can be large)
     [Tactic.cse.summary] expr: x + x + (y + y + (y + y))
+  [Tactic.cse.summary] ⏭️ Unprofitable { occs := 1, size := 15 } . (NOTE: can be large)
+    [Tactic.cse.summary] expr: y + y + (y + y) + (y + y + (y + y))
 [Tactic.cse.summary] CSE summary of profitable expressions (#expressions:2):
   [Tactic.cse.summary] 1) { occs := 8, size := 3 } (NOTE: can be large)
     [Tactic.cse.summary] y + y
@@ -269,80 +269,81 @@ hx2 : x9 + x3 = x2
 x10 x11 : BitVec 128
 hx4 : x10 ||| x11 = x4
 x12 : BitVec 128
-hx11 : x12 <<< 64 = x11
+hx10 : x12 &&& 18446744073709551615#128 = x10
 x13 : BitVec 128
-hx10 : x13 &&& 18446744073709551615#128 = x10
+hx11 : x13 <<< 64 = x11
 x14 : BitVec 64
-hx13 : BitVec.zeroExtend 128 x14 = x13
+hx12 : BitVec.zeroExtend 128 x14 = x12
 x15 : BitVec 64
-hx12 : BitVec.zeroExtend 128 x15 = x12
-x16 : BitVec (127 - 64 + 1)
-x17 : BitVec (63 - 0 + 1)
+hx13 : BitVec.zeroExtend 128 x15 = x13
+x16 : BitVec (63 - 0 + 1)
+x17 : BitVec (127 - 64 + 1)
 x18 : BitVec 128
-hx16 : BitVec.extractLsb 127 64 x18 = x16
-hx17 : BitVec.extractLsb 63 0 x18 = x17
+hx16 : BitVec.extractLsb 63 0 x18 = x16
+hx17 : BitVec.extractLsb 127 64 x18 = x17
 x19 x20 : BitVec 64
 hx8 : x19 + x20 = x8
 x21 : BitVec 64
 hx9 : x20 + x21 = x9
-x22 x23 : BitVec 128
-hx18 : x22 ||| x23 = x18
-x24 x25 : BitVec 64
+x22 : BitVec 128
+x23 : BitVec 64
+x24 : BitVec 128
+hx18 : x22 ||| x24 = x18
+x25 : BitVec 64
 x26 : BitVec 128
-hx23 : x26 <<< 64 = x23
+hx22 : x26 &&& 18446744073709551615#128 = x22
 x27 : BitVec 128
-hx22 : x27 &&& 18446744073709551615#128 = x22
+hx24 : x27 <<< 64 = x24
 x28 : BitVec 64
 hx27 : BitVec.zeroExtend 128 x28 = x27
 x29 : BitVec 64
-hx26 : BitVec.zeroExtend 128 x29 = x26
+hx20 : x29 ^^^ x25 = x20
 x30 : BitVec 64
-hx20 : x30 ^^^ x25 = x20
-x31 : BitVec 64
-hx21 : x24 ^^^ x31 = x21
-x32 x33 : BitVec 64
-hx24 : x33 ^^^ x32 = x24
-x34 : BitVec 64
-x35 : BitVec (63 - 0 + 1)
-hx35 : BitVec.extractLsb 63 0 d = x35
+hx26 : BitVec.zeroExtend 128 x30 = x26
+x31 x32 : BitVec 64
+hx23 : x31 ^^^ x32 = x23
+x33 x34 : BitVec 64
+hx21 : x23 ^^^ x34 = x21
+x35 : BitVec (127 - 64 + 1)
+hx35 : BitVec.extractLsb 127 64 d = x35
+hx7 : x8 + x35 = x7
 x36 : BitVec (63 - 0 + 1)
-hx36 : BitVec.extractLsb 63 0 c = x36
-hx28 : x36 + x35 = x28
-x37 : BitVec (127 - 64 + 1)
-hx37 : BitVec.extractLsb 127 64 c = x37
-hx19 : x37 + x21 = x19
-x38 : BitVec (63 - 0 + 1)
-hx38 : BitVec.extractLsb 63 0 a = x38
-x39 : BitVec (63 - 0 + 1)
-hx39 : BitVec.extractLsb 63 0 b = x39
-hx1 : x2 + x39 = x1
-hx5 : x39 + x6 = x5
-x40 : BitVec (127 - 64 + 1)
-hx40 : BitVec.extractLsb 127 64 b = x40
-hx31 : x40.rotateRight 41 = x31
-hx32 : x40.rotateRight 18 = x32
-hx33 : x40.rotateRight 14 = x33
-hx34 : ~~~x40 = x34
-hx30 : x40 &&& x38 = x30
-x41 : BitVec (127 - 64 + 1)
-hx41 : BitVec.extractLsb 127 64 a = x41
-hx25 : x34 &&& x41 = x25
+hx36 : BitVec.extractLsb 63 0 a = x36
+x37 : BitVec (63 - 0 + 1)
+hx37 : BitVec.extractLsb 63 0 c = x37
+x38 : BitVec (127 - 64 + 1)
+hx38 : BitVec.extractLsb 127 64 c = x38
+hx19 : x38 + x21 = x19
+hx28 : x38 + x35 = x28
+x39 : BitVec (127 - 64 + 1)
+hx39 : BitVec.extractLsb 127 64 e = x39
+hx6 : x7 + x39 = x6
+hx15 : x17 + x39 = x15
+x40 : BitVec (63 - 0 + 1)
+hx40 : BitVec.extractLsb 63 0 b = x40
+hx1 : x2 + x40 = x1
+hx5 : x40 + x6 = x5
+x41 : BitVec (63 - 0 + 1)
+hx41 : BitVec.extractLsb 63 0 d = x41
+hx30 : x37 + x41 = x30
 x42 : BitVec (127 - 64 + 1)
-hx42 : BitVec.extractLsb 127 64 e = x42
-hx6 : x7 + x42 = x6
-hx15 : x16 + x42 = x15
+hx42 : BitVec.extractLsb 127 64 a = x42
+hx25 : x33 &&& x42 = x25
 x43 : BitVec (127 - 64 + 1)
-hx43 : BitVec.extractLsb 127 64 d = x43
-hx7 : x8 + x43 = x7
-hx29 : x37 + x43 = x29
+hx43 : BitVec.extractLsb 127 64 b = x43
+hx31 : x43.rotateRight 14 = x31
+hx32 : x43.rotateRight 18 = x32
+hx33 : ~~~x43 = x33
+hx34 : x43.rotateRight 41 = x34
+hx29 : x43 &&& x36 = x29
 x44 : BitVec (63 - 0 + 1)
 hx44 : BitVec.extractLsb 63 0 e = x44
-hx14 : x17 + x44 = x14
+hx14 : x16 + x44 = x14
 ⊢ x2 ++
-      ((x1 &&& x40 ^^^ ~~~x1 &&& x38) + (x1.rotateRight 14 ^^^ x1.rotateRight 18 ^^^ x1.rotateRight 41) +
+      ((x1 &&& x43 ^^^ ~~~x1 &&& x36) + (x1.rotateRight 14 ^^^ x1.rotateRight 18 ^^^ x1.rotateRight 41) +
         BitVec.extractLsb 63 0 x4) =
     x6 ++
-      (x36 + (x5.rotateRight 14 ^^^ x5.rotateRight 18 ^^^ x5.rotateRight 41) + (x5 &&& x40 ^^^ ~~~x5 &&& x38) + x35 +
+      (x37 + (x5.rotateRight 14 ^^^ x5.rotateRight 18 ^^^ x5.rotateRight 41) + (x5 &&& x43 ^^^ ~~~x5 &&& x36) + x41 +
         x44)
 -/
 #guard_msgs in theorem sha512h_rule_1 (a b c d e : BitVec 128) :
@@ -390,9 +391,9 @@ x4 : BitVec 128
 hx3 : BitVec.extractLsb 127 64 x4 = x3
 x5 : BitVec 64
 x6 x7 : BitVec 128
-hx6 : x7 <<< 64 = x6
+hx4 : x7 ||| x6 = x4
 x8 : BitVec 128
-hx4 : x8 ||| x6 = x4
+hx6 : x8 <<< 64 = x6
 x9 : BitVec 64
 hx7 : BitVec.zeroExtend 128 x9 = x7
 x10 : BitVec 64
@@ -400,12 +401,12 @@ hx8 : BitVec.zeroExtend 128 x10 = x8
 x11 : BitVec 64
 x12 : BitVec (127 - 64 + 1)
 x13 : BitVec (63 - 0 + 1)
-x14 : BitVec (191 - 64 + 1)
-hx12 : BitVec.extractLsb 127 64 x14 = x12
-hx13 : BitVec.extractLsb 63 0 x14 = x13
-x15 : BitVec 64
+x14 : BitVec 64
+x15 : BitVec (191 - 64 + 1)
+hx12 : BitVec.extractLsb 127 64 x15 = x12
+hx13 : BitVec.extractLsb 63 0 x15 = x13
 x16 : BitVec 256
-hx14 : BitVec.extractLsb 191 64 x16 = x14
+hx15 : BitVec.extractLsb 191 64 x16 = x15
 x17 x18 : BitVec 64
 hx2 : x18 + x3 = x2
 x19 : BitVec 128
@@ -414,62 +415,63 @@ x20 x21 : BitVec 64
 hx17 : x20 + x21 = x17
 x22 : BitVec 64
 hx18 : x21 + x22 = x18
-x23 : BitVec 64
-x24 x25 : BitVec 128
-hx19 : x25 ||| x24 = x19
+x23 : BitVec 128
+x24 : BitVec 64
+x25 : BitVec 128
+hx19 : x25 ||| x23 = x19
 x26 : BitVec 128
-hx24 : x26 <<< 64 = x24
+hx23 : x26 <<< 64 = x23
 x27 x28 : BitVec 64
-hx21 : x28 ^^^ x27 = x21
+hx25 : BitVec.zeroExtend 128 x28 = x25
 x29 : BitVec 64
 hx26 : BitVec.zeroExtend 128 x29 = x26
 x30 : BitVec 64
-hx25 : BitVec.zeroExtend 128 x30 = x25
-x31 x32 : BitVec 64
-hx23 : x31 ^^^ x32 = x23
-x33 x34 : BitVec 64
-hx22 : x23 ^^^ x34 = x22
-x35 : BitVec (127 - 64 + 1)
-hx35 : BitVec.extractLsb 127 64 d = x35
-x36 : BitVec (127 - 64 + 1)
-hx36 : BitVec.extractLsb 127 64 e = x36
-hx29 : x35 + x36 = x29
+hx21 : x30 ^^^ x27 = x21
+x31 : BitVec 64
+hx22 : x24 ^^^ x31 = x22
+x32 x33 x34 : BitVec 64
+hx24 : x33 ^^^ x34 = x24
+x35 : BitVec (63 - 0 + 1)
+hx35 : BitVec.extractLsb 63 0 b = x35
+hx1 : x2 + x35 = x1
+hx5 : x35 + x11 = x5
+x36 : BitVec (63 - 0 + 1)
+hx36 : BitVec.extractLsb 63 0 a = x36
 x37 : BitVec (127 - 64 + 1)
 hx37 : BitVec.extractLsb 127 64 b = x37
-hx31 : x37.rotateRight 14 = x31
-hx32 : x37.rotateRight 18 = x32
-hx33 : ~~~x37 = x33
-hx34 : x37.rotateRight 41 = x34
-x38 : BitVec (63 - 0 + 1)
-hx38 : BitVec.extractLsb 63 0 d = x38
-hx15 : x17 + x38 = x15
-x39 : BitVec (63 - 0 + 1)
-hx39 : BitVec.extractLsb 63 0 b = x39
-hx1 : x2 + x39 = x1
-hx5 : x39 + x11 = x5
-x40 : BitVec (127 - 64 + 1)
-hx40 : BitVec.extractLsb 127 64 a = x40
-hx27 : x33 &&& x40 = x27
-x41 : BitVec (63 - 0 + 1)
-hx41 : BitVec.extractLsb 63 0 e = x41
-hx11 : x15 + x41 = x11
-hx30 : x38 + x41 = x30
+hx31 : x37.rotateRight 41 = x31
+hx32 : ~~~x37 = x32
+hx33 : x37.rotateRight 14 = x33
+hx34 : x37.rotateRight 18 = x34
+hx30 : x37 &&& x36 = x30
+x38 : BitVec (127 - 64 + 1)
+hx38 : BitVec.extractLsb 127 64 a = x38
+hx27 : x32 &&& x38 = x27
+x39 : BitVec (127 - 64 + 1)
+hx39 : BitVec.extractLsb 127 64 e = x39
+x40 : BitVec (63 - 0 + 1)
+hx40 : BitVec.extractLsb 63 0 c = x40
+hx9 : x40 + x13 = x9
+x41 : BitVec (127 - 64 + 1)
+hx41 : BitVec.extractLsb 127 64 d = x41
+hx29 : x41 + x39 = x29
 x42 : BitVec (63 - 0 + 1)
-hx42 : BitVec.extractLsb 63 0 a = x42
-hx28 : x37 &&& x42 = x28
-x43 : BitVec (63 - 0 + 1)
-hx43 : BitVec.extractLsb 63 0 c = x43
-hx10 : x43 + x13 = x10
-x44 : BitVec (127 - 64 + 1)
-hx44 : BitVec.extractLsb 127 64 c = x44
-hx9 : x44 + x12 = x9
-hx20 : x44 + x22 = x20
+hx42 : BitVec.extractLsb 63 0 e = x42
+hx11 : x14 + x42 = x11
+x43 : BitVec (127 - 64 + 1)
+hx43 : BitVec.extractLsb 127 64 c = x43
+hx10 : x43 + x12 = x10
+hx20 : x43 + x22 = x20
+x44 : BitVec (63 - 0 + 1)
+hx44 : BitVec.extractLsb 63 0 d = x44
+hx14 : x17 + x44 = x14
+hx28 : x44 + x42 = x28
 ⊢ x2 ++
-      ((x1 &&& x37 ^^^ ~~~x1 &&& x42) + (x1.rotateRight 14 ^^^ x1.rotateRight 18 ^^^ x1.rotateRight 41) +
+      ((x1 &&& x37 ^^^ ~~~x1 &&& x36) + (x1.rotateRight 14 ^^^ x1.rotateRight 18 ^^^ x1.rotateRight 41) +
         BitVec.extractLsb 63 0 x4) =
     x11 ++
-      (x43 + (x5.rotateRight 14 ^^^ x5.rotateRight 18 ^^^ x5.rotateRight 41) + (x5 &&& x37 ^^^ ~~~x5 &&& x42) + x35 +
-        x36)
+      (x40 + (x5.rotateRight 14 ^^^ x5.rotateRight 18 ^^^ x5.rotateRight 41) + (x5 &&& x37 ^^^ ~~~x5 &&& x36) + x41 +
+        x39)
 -/
 #guard_msgs in theorem sha512h_rule_2 (a b c d e : BitVec 128) :
   let a0 := extractLsb 63 0   a