perf/inline blake3 round

Ix/Aiur/Compiler/Check.lean

@@ -780,14 +780,14 @@ def inferTerm (t : Term) : CheckM Typed.Term := match t with
     let a' ← checkNoEscape a .u8
     let b' ← checkNoEscape b .u8
     pure (Typed.Term.u8Mul (.tuple #[.u8, .u8]) false a' b')
-  | .u8ChainRotr7 a b => do
+  | .u8XorSplit7 a b => do
     let a' ← checkNoEscape a .u8
     let b' ← checkNoEscape b .u8
-    pure (Typed.Term.u8ChainRotr7 (.tuple #[.u8, .u8, .u8]) false a' b')
-  | .u8ChainRotr4 a b => do
+    pure (Typed.Term.u8XorSplit7 (.tuple #[.u8, .u8]) false a' b')
+  | .u8XorSplit4 a b => do
     let a' ← checkNoEscape a .u8
     let b' ← checkNoEscape b .u8
-    pure (Typed.Term.u8ChainRotr4 (.tuple #[.u8, .u8, .u8]) false a' b')
+    pure (Typed.Term.u8XorSplit4 (.tuple #[.u8, .u8]) false a' b')
   | .u8Sub a b => do
     -- Low byte and the 0/1 borrow are both `u8` (same range argument as add).
     let a' ← checkNoEscape a .u8
@@ -1007,8 +1007,8 @@ def zonkTypedTerm (t : Typed.Term) : CheckM Typed.Term := match t with
   | .u8Xor τ e a b => do pure (.u8Xor (← zonkTyp τ) e (← zonkTypedTerm a) (← zonkTypedTerm b))
   | .u8Add τ e a b => do pure (.u8Add (← zonkTyp τ) e (← zonkTypedTerm a) (← zonkTypedTerm b))
   | .u8Mul τ e a b => do pure (.u8Mul (← zonkTyp τ) e (← zonkTypedTerm a) (← zonkTypedTerm b))
-  | .u8ChainRotr7 τ e a b => do pure (.u8ChainRotr7 (← zonkTyp τ) e (← zonkTypedTerm a) (← zonkTypedTerm b))
-  | .u8ChainRotr4 τ e a b => do pure (.u8ChainRotr4 (← zonkTyp τ) e (← zonkTypedTerm a) (← zonkTypedTerm b))
+  | .u8XorSplit7 τ e a b => do pure (.u8XorSplit7 (← zonkTyp τ) e (← zonkTypedTerm a) (← zonkTypedTerm b))
+  | .u8XorSplit4 τ e a b => do pure (.u8XorSplit4 (← zonkTyp τ) e (← zonkTypedTerm a) (← zonkTypedTerm b))
   | .u8Sub τ e a b => do pure (.u8Sub (← zonkTyp τ) e (← zonkTypedTerm a) (← zonkTypedTerm b))
   | .u8And τ e a b => do pure (.u8And (← zonkTyp τ) e (← zonkTypedTerm a) (← zonkTypedTerm b))
   | .u8Or τ e a b => do pure (.u8Or (← zonkTyp τ) e (← zonkTypedTerm a) (← zonkTypedTerm b))

Ix/Aiur/Compiler/Concretize.lean

@@ -340,11 +340,11 @@ def termToConcrete
   | .u8Mul τ e a b => do
       pure (.u8Mul (← typToConcrete mono τ) e
                    (← termToConcrete mono a) (← termToConcrete mono b))
-  | .u8ChainRotr7 τ e a b => do
-      pure (.u8ChainRotr7 (← typToConcrete mono τ) e
+  | .u8XorSplit7 τ e a b => do
+      pure (.u8XorSplit7 (← typToConcrete mono τ) e
                    (← termToConcrete mono a) (← termToConcrete mono b))
-  | .u8ChainRotr4 τ e a b => do
-      pure (.u8ChainRotr4 (← typToConcrete mono τ) e
+  | .u8XorSplit4 τ e a b => do
+      pure (.u8XorSplit4 (← typToConcrete mono τ) e
                    (← termToConcrete mono a) (← termToConcrete mono b))
   | .u8Sub τ e a b => do
       pure (.u8Sub (← typToConcrete mono τ) e
@@ -570,9 +570,9 @@ def rewriteTypedTerm (decls : Typed.Decls)
       (rewriteTypedTerm decls subst mono a) (rewriteTypedTerm decls subst mono b)
   | .u8Mul τ e a b => .u8Mul (rewriteTyp subst mono τ) e
       (rewriteTypedTerm decls subst mono a) (rewriteTypedTerm decls subst mono b)
-  | .u8ChainRotr7 τ e a b => .u8ChainRotr7 (rewriteTyp subst mono τ) e
+  | .u8XorSplit7 τ e a b => .u8XorSplit7 (rewriteTyp subst mono τ) e
       (rewriteTypedTerm decls subst mono a) (rewriteTypedTerm decls subst mono b)
-  | .u8ChainRotr4 τ e a b => .u8ChainRotr4 (rewriteTyp subst mono τ) e
+  | .u8XorSplit4 τ e a b => .u8XorSplit4 (rewriteTyp subst mono τ) e
       (rewriteTypedTerm decls subst mono a) (rewriteTypedTerm decls subst mono b)
   | .u8Sub τ e a b => .u8Sub (rewriteTyp subst mono τ) e
       (rewriteTypedTerm decls subst mono a) (rewriteTypedTerm decls subst mono b)
@@ -670,7 +670,7 @@ def collectInTypedTerm (seen : Std.HashSet (Global × Array Typ)) :
     args.attach.foldl (fun s ⟨a, _⟩ => collectInTypedTerm s a) seen
   | .add τ _ a b | .sub τ _ a b | .mul τ _ a b
   | .u8Xor τ _ a b | .u8Add τ _ a b | .u8Mul τ _ a b | .u8Sub τ _ a b
-  | .u8ChainRotr7 τ _ a b | .u8ChainRotr4 τ _ a b | .u8RangeCheck τ _ a b
+  | .u8XorSplit7 τ _ a b | .u8XorSplit4 τ _ a b | .u8RangeCheck τ _ a b
   | .unconstrainedBigUintDivMod τ _ a b
   | .u8And τ _ a b | .u8Or τ _ a b
   | .u8LessThan τ _ a b | .u32LessThan τ _ a b | .unconstrainedU32Add τ _ a b =>
@@ -745,7 +745,7 @@ def collectCalls (decls : Typed.Decls)
     bs.attach.foldl (fun s ⟨(_, b), _⟩ => collectCalls decls s b) seen
   | .add _ _ a b | .sub _ _ a b | .mul _ _ a b
   | .u8Xor _ _ a b | .u8Add _ _ a b | .u8Mul _ _ a b | .u8Sub _ _ a b
-  | .u8ChainRotr7 _ _ a b | .u8ChainRotr4 _ _ a b | .u8RangeCheck _ _ a b
+  | .u8XorSplit7 _ _ a b | .u8XorSplit4 _ _ a b | .u8RangeCheck _ _ a b
   | .unconstrainedBigUintDivMod _ _ a b
   | .u8And _ _ a b | .u8Or _ _ a b
   | .u8LessThan _ _ a b | .u32LessThan _ _ a b | .unconstrainedU32Add _ _ a b =>
@@ -853,9 +853,9 @@ def substInTypedTerm (subst : Global → Option Typ) : Typed.Term → Typed.Term
       (substInTypedTerm subst a) (substInTypedTerm subst b)
   | .u8Mul τ e a b => .u8Mul (Typ.instantiate subst τ) e
       (substInTypedTerm subst a) (substInTypedTerm subst b)
-  | .u8ChainRotr7 τ e a b => .u8ChainRotr7 (Typ.instantiate subst τ) e
+  | .u8XorSplit7 τ e a b => .u8XorSplit7 (Typ.instantiate subst τ) e
       (substInTypedTerm subst a) (substInTypedTerm subst b)
-  | .u8ChainRotr4 τ e a b => .u8ChainRotr4 (Typ.instantiate subst τ) e
+  | .u8XorSplit4 τ e a b => .u8XorSplit4 (Typ.instantiate subst τ) e
       (substInTypedTerm subst a) (substInTypedTerm subst b)
   | .u8Sub τ e a b => .u8Sub (Typ.instantiate subst τ) e
       (substInTypedTerm subst a) (substInTypedTerm subst b)

Ix/Aiur/Compiler/Layout.lean

@@ -198,7 +198,7 @@ def opLayout : Bytecode.Op → LayoutM Unit
     pushDegree ((aDegree.max bDegree).max 1)
     bumpAuxiliaries; bumpLookups
   | .u8Mul .. => do pushDegrees #[1, 1]; bumpAuxiliaries 2; bumpLookups
-  | .u8ChainRotr7 .. | .u8ChainRotr4 .. => do pushDegrees #[1, 1, 1]; bumpAuxiliaries 3; bumpLookups
+  | .u8XorSplit7 .. | .u8XorSplit4 .. => do pushDegrees #[1, 1]; bumpAuxiliaries 2; bumpLookups
   | .u8LessThan .. => do pushDegree 1; bumpAuxiliaries; bumpLookups
   | .u32LessThan .. => do pushDegree 1; bumpAuxiliaries 12; bumpLookups 6
   | .unconstrainedU32Add a b => do

Ix/Aiur/Compiler/Lower.lean

@@ -306,12 +306,12 @@ def toIndex
   | .u8Mul _ _ i j => do
     let i ← expectIdx layoutMap bindings i; let j ← expectIdx layoutMap bindings j
     pushOp (.u8Mul i j) 2
-  | .u8ChainRotr7 _ _ i j => do
+  | .u8XorSplit7 _ _ i j => do
     let i ← expectIdx layoutMap bindings i; let j ← expectIdx layoutMap bindings j
-    pushOp (.u8ChainRotr7 i j) 3
-  | .u8ChainRotr4 _ _ i j => do
+    pushOp (.u8XorSplit7 i j) 2
+  | .u8XorSplit4 _ _ i j => do
     let i ← expectIdx layoutMap bindings i; let j ← expectIdx layoutMap bindings j
-    pushOp (.u8ChainRotr4 i j) 3
+    pushOp (.u8XorSplit4 i j) 2
   | .u8Sub _ _ i j => do
     let i ← expectIdx layoutMap bindings i; let j ← expectIdx layoutMap bindings j
     pushOp (.u8Sub i j) 2

Ix/Aiur/Compiler/Match.lean

@@ -383,8 +383,8 @@ def typedToSimple : Term → Simple.Term
   | .u8Xor τ e a b => .u8Xor τ e (typedToSimple a) (typedToSimple b)
   | .u8Add τ e a b => .u8Add τ e (typedToSimple a) (typedToSimple b)
   | .u8Mul τ e a b => .u8Mul τ e (typedToSimple a) (typedToSimple b)
-  | .u8ChainRotr7 τ e a b => .u8ChainRotr7 τ e (typedToSimple a) (typedToSimple b)
-  | .u8ChainRotr4 τ e a b => .u8ChainRotr4 τ e (typedToSimple a) (typedToSimple b)
+  | .u8XorSplit7 τ e a b => .u8XorSplit7 τ e (typedToSimple a) (typedToSimple b)
+  | .u8XorSplit4 τ e a b => .u8XorSplit4 τ e (typedToSimple a) (typedToSimple b)
   | .u8Sub τ e a b => .u8Sub τ e (typedToSimple a) (typedToSimple b)
   | .u8And τ e a b => .u8And τ e (typedToSimple a) (typedToSimple b)
   | .u8Or τ e a b => .u8Or τ e (typedToSimple a) (typedToSimple b)

Ix/Aiur/Compiler/Simple.lean

@@ -124,6 +124,8 @@ def simplifyTypedTerm (decls : Source.Decls) : Term → Except CheckError Term
       let a' ← simplifyTypedTerm decls a
       let b' ← simplifyTypedTerm decls b
       pure (.u8LessThan τ e a' b')
+  | .u8XorSplit7 τ e a b => do pure (.u8XorSplit7 τ e (← simplifyTypedTerm decls a) (← simplifyTypedTerm decls b))
+  | .u8XorSplit4 τ e a b => do pure (.u8XorSplit4 τ e (← simplifyTypedTerm decls a) (← simplifyTypedTerm decls b))
   | .u32LessThan τ e a b => do
       let a' ← simplifyTypedTerm decls a
       let b' ← simplifyTypedTerm decls b

Ix/Aiur/Goldilocks.lean

@@ -72,16 +72,6 @@ def G.u8Mul (a b : G) : G × G :=
 def G.u8Sub (a b : G) : G × G :=
   (G.ofNat ((a.n + 256 - b.n) % 256), if a.n < b.n then 1 else 0)
 
-/-- Chainable partial for a right-rotation by 7 bits over little-endian bytes.
-Returns `(a>>7 + b<<1, b>>7, a<<1)` (shifts mod 256). -/
-def G.u8ChainRotr7 (a b : G) : G × G × G :=
-  (G.ofNat (a.n / 128 + (b.n * 2) % 256), G.ofNat (b.n / 128), G.ofNat ((a.n * 2) % 256))
-
-/-- Chainable partial for a right-rotation by 4 bits over little-endian bytes.
-Returns `(a>>4 + b<<4, b>>4, a<<4)` (shifts mod 256). -/
-def G.u8ChainRotr4 (a b : G) : G × G × G :=
-  (G.ofNat (a.n / 16 + (b.n * 16) % 256), G.ofNat (b.n / 16), G.ofNat ((a.n * 16) % 256))
-
 def G.u8ShiftLeft  (a : G) : G := G.ofNat ((a.n * 2) % 256)
 def G.u8ShiftRight (a : G) : G := G.ofNat (a.n / 2)
 

Ix/Aiur/Interpret.lean

@@ -427,24 +427,18 @@ partial def interp (decls : Decls) (bindings : Bindings) : Term → InterpM Valu
           let hi : Value := .field (G.ofUInt8 (x / 256).toUInt8)
           return .tuple #[lo, hi]
       | _, _ => throwErr "u8Mul: expected field values"
-  | .u8ChainRotr7 t1 t2 => do
+  | .u8XorSplit7 t1 t2 => do
       match (← interp decls bindings t1), (← interp decls bindings t2) with
       | .field a, .field b =>
-          let i := a.val.toUInt8
-          let j := b.val.toUInt8
-          return .tuple #[.field (G.ofUInt8 ((i >>> 7) + (j <<< 1))),
-                          .field (G.ofUInt8 (j >>> 7)),
-                          .field (G.ofUInt8 (i <<< 1))]
-      | _, _ => throwErr "u8ChainRotr7: expected field values"
-  | .u8ChainRotr4 t1 t2 => do
+          let x := a.val.toUInt8 ^^^ b.val.toUInt8
+          return .tuple #[.field (G.ofUInt8 (x >>> 7)), .field (G.ofUInt8 (x <<< 1))]
+      | _, _ => throwErr "u8XorSplit7: expected field values"
+  | .u8XorSplit4 t1 t2 => do
       match (← interp decls bindings t1), (← interp decls bindings t2) with
       | .field a, .field b =>
-          let i := a.val.toUInt8
-          let j := b.val.toUInt8
-          return .tuple #[.field (G.ofUInt8 ((i >>> 4) + (j <<< 4))),
-                          .field (G.ofUInt8 (j >>> 4)),
-                          .field (G.ofUInt8 (i <<< 4))]
-      | _, _ => throwErr "u8ChainRotr4: expected field values"
+          let x := a.val.toUInt8 ^^^ b.val.toUInt8
+          return .tuple #[.field (G.ofUInt8 (x >>> 4)), .field (G.ofUInt8 (x <<< 4))]
+      | _, _ => throwErr "u8XorSplit4: expected field values"
   | .u8Sub t1 t2 => do
       match (← interp decls bindings t1), (← interp decls bindings t2) with
       | .field a, .field b =>

Ix/Aiur/Meta.lean

@@ -196,8 +196,8 @@ syntax "u8_shift_right" "(" aiur_trm ")"                                     : a
 syntax "u8_xor" "(" aiur_trm ", " aiur_trm ")"                              : aiur_trm
 syntax "u8_add" "(" aiur_trm ", " aiur_trm ")"                              : aiur_trm
 syntax "u8_mul" "(" aiur_trm ", " aiur_trm ")"                              : aiur_trm
-syntax "u8_chain_rotr7" "(" aiur_trm ", " aiur_trm ")"                      : aiur_trm
-syntax "u8_chain_rotr4" "(" aiur_trm ", " aiur_trm ")"                      : aiur_trm
+syntax "u8_xor_split7" "(" aiur_trm ", " aiur_trm ")"                       : aiur_trm
+syntax "u8_xor_split4" "(" aiur_trm ", " aiur_trm ")"                       : aiur_trm
 syntax "u8_sub" "(" aiur_trm ", " aiur_trm ")"                              : aiur_trm
 syntax "u8_and" "(" aiur_trm ", " aiur_trm ")"                              : aiur_trm
 syntax "u8_or" "(" aiur_trm ", " aiur_trm ")"                               : aiur_trm
@@ -341,10 +341,10 @@ partial def elabTrm : ElabStxCat `aiur_trm
     mkAppM ``Source.Term.u8Add #[← elabTrm i, ← elabTrm j]
   | `(aiur_trm| u8_mul($i:aiur_trm, $j:aiur_trm)) => do
     mkAppM ``Source.Term.u8Mul #[← elabTrm i, ← elabTrm j]
-  | `(aiur_trm| u8_chain_rotr7($i:aiur_trm, $j:aiur_trm)) => do
-    mkAppM ``Source.Term.u8ChainRotr7 #[← elabTrm i, ← elabTrm j]
-  | `(aiur_trm| u8_chain_rotr4($i:aiur_trm, $j:aiur_trm)) => do
-    mkAppM ``Source.Term.u8ChainRotr4 #[← elabTrm i, ← elabTrm j]
+  | `(aiur_trm| u8_xor_split7($i:aiur_trm, $j:aiur_trm)) => do
+    mkAppM ``Source.Term.u8XorSplit7 #[← elabTrm i, ← elabTrm j]
+  | `(aiur_trm| u8_xor_split4($i:aiur_trm, $j:aiur_trm)) => do
+    mkAppM ``Source.Term.u8XorSplit4 #[← elabTrm i, ← elabTrm j]
   | `(aiur_trm| u8_sub($i:aiur_trm, $j:aiur_trm)) => do
     mkAppM ``Source.Term.u8Sub #[← elabTrm i, ← elabTrm j]
   | `(aiur_trm| u8_and($i:aiur_trm, $j:aiur_trm)) => do
@@ -561,14 +561,14 @@ where
       let i ← replaceToken old new i
       let j ← replaceToken old new j
       `(aiur_trm| u8_mul($i, $j))
-    | `(aiur_trm| u8_chain_rotr7($i:aiur_trm, $j:aiur_trm)) => do
+    | `(aiur_trm| u8_xor_split7($i:aiur_trm, $j:aiur_trm)) => do
       let i ← replaceToken old new i
       let j ← replaceToken old new j
-      `(aiur_trm| u8_chain_rotr7($i, $j))
-    | `(aiur_trm| u8_chain_rotr4($i:aiur_trm, $j:aiur_trm)) => do
+      `(aiur_trm| u8_xor_split7($i, $j))
+    | `(aiur_trm| u8_xor_split4($i:aiur_trm, $j:aiur_trm)) => do
       let i ← replaceToken old new i
       let j ← replaceToken old new j
-      `(aiur_trm| u8_chain_rotr4($i, $j))
+      `(aiur_trm| u8_xor_split4($i, $j))
     | `(aiur_trm| u8_sub($i:aiur_trm, $j:aiur_trm)) => do
       let i ← replaceToken old new i
       let j ← replaceToken old new j

Ix/Aiur/Semantics/BytecodeEval.lean

@@ -313,18 +313,12 @@ def evalOp (t : Bytecode.Toplevel) (fuel : Nat) (op : Op) (st : EvalState) :
     let prod := x.val.toUInt8.toNat * y.val.toUInt8.toNat
     let st1 := pushMap st (G.ofUInt8 prod.toUInt8)
     pure (pushMap st1 (G.ofUInt8 (prod / 256).toUInt8))
-  | .u8ChainRotr7 a b => do
-    let x ← readIdx st a; let y ← readIdx st b
-    let i := x.val.toUInt8; let j := y.val.toUInt8
-    let st1 := pushMap st (G.ofUInt8 ((i >>> 7) + (j <<< 1)))
-    let st2 := pushMap st1 (G.ofUInt8 (j >>> 7))
-    pure (pushMap st2 (G.ofUInt8 (i <<< 1)))
-  | .u8ChainRotr4 a b => do
-    let x ← readIdx st a; let y ← readIdx st b
-    let i := x.val.toUInt8; let j := y.val.toUInt8
-    let st1 := pushMap st (G.ofUInt8 ((i >>> 4) + (j <<< 4)))
-    let st2 := pushMap st1 (G.ofUInt8 (j >>> 4))
-    pure (pushMap st2 (G.ofUInt8 (i <<< 4)))
+  | .u8XorSplit7 a b => do
+    let x ← readIdx st a; let y ← readIdx st b; let z := x.val.toUInt8 ^^^ y.val.toUInt8
+    pure (pushMap (pushMap st (G.ofUInt8 (z >>> 7))) (G.ofUInt8 (z <<< 1)))
+  | .u8XorSplit4 a b => do
+    let x ← readIdx st a; let y ← readIdx st b; let z := x.val.toUInt8 ^^^ y.val.toUInt8
+    pure (pushMap (pushMap st (G.ofUInt8 (z >>> 4))) (G.ofUInt8 (z <<< 4)))
   | .u8Sub a b => do
     let x ← readIdx st a; let y ← readIdx st b
     let i := x.val.toUInt8; let j := y.val.toUInt8

Ix/Aiur/Semantics/SourceEval.lean

@@ -510,22 +510,18 @@ def interp (decls : Decls) (fuel : Nat) (bindings : Bindings)
                    .field (G.ofUInt8 (x / 256).toUInt8)])
         (interp decls fuel bindings t1 st)
         (fun st1 => interp decls fuel bindings t2 st1)
-  | .u8ChainRotr7 t1 t2 =>
+  | .u8XorSplit7 t1 t2 =>
       combineFieldsResult
         (fun a b =>
-          let i := a.val.toUInt8; let j := b.val.toUInt8
-          .tuple #[.field (G.ofUInt8 ((i >>> 7) + (j <<< 1))),
-                   .field (G.ofUInt8 (j >>> 7)),
-                   .field (G.ofUInt8 (i <<< 1))])
+          let x := a.val.toUInt8 ^^^ b.val.toUInt8
+          .tuple #[.field (G.ofUInt8 (x >>> 7)), .field (G.ofUInt8 (x <<< 1))])
         (interp decls fuel bindings t1 st)
         (fun st1 => interp decls fuel bindings t2 st1)
-  | .u8ChainRotr4 t1 t2 =>
+  | .u8XorSplit4 t1 t2 =>
       combineFieldsResult
         (fun a b =>
-          let i := a.val.toUInt8; let j := b.val.toUInt8
-          .tuple #[.field (G.ofUInt8 ((i >>> 4) + (j <<< 4))),
-                   .field (G.ofUInt8 (j >>> 4)),
-                   .field (G.ofUInt8 (i <<< 4))])
+          let x := a.val.toUInt8 ^^^ b.val.toUInt8
+          .tuple #[.field (G.ofUInt8 (x >>> 4)), .field (G.ofUInt8 (x <<< 4))])
         (interp decls fuel bindings t1 st)
         (fun st1 => interp decls fuel bindings t2 st1)
   | .u8Sub t1 t2 =>

Ix/Aiur/Stages/Bytecode.lean

@@ -43,8 +43,8 @@ inductive Op
   | u8Or : ValIdx → ValIdx → Op
   | u8LessThan : ValIdx → ValIdx → Op
   | u32LessThan : ValIdx → ValIdx → Op
-  | u8ChainRotr7 : ValIdx → ValIdx → Op
-  | u8ChainRotr4 : ValIdx → ValIdx → Op
+  | u8XorSplit7 : ValIdx → ValIdx → Op
+  | u8XorSplit4 : ValIdx → ValIdx → Op
   | debug : String → Option (Array ValIdx) → Op
   /-- Range-check the two values into `[0, 256)` via the byte chip. Produces no
   new values: it is a pure side-effect (lookup), and its `u8` results alias the

Ix/Aiur/Stages/Codegen.lean

@@ -348,7 +348,7 @@ def Op.outputCount : Op → Nat
   | .u8Xor _ _ | .u8And _ _ | .u8Or _ _ | .u8LessThan _ _ => 1
   | .u8Mul _ _ => 2
   | .u8Add _ _ | .u8Sub _ _ => 2
-  | .u8ChainRotr7 _ _ | .u8ChainRotr4 _ _ => 3
+  | .u8XorSplit7 _ _ | .u8XorSplit4 _ _ => 2
   | .u32LessThan _ _ => 1
   | .u8RangeCheck _ _ => 0
   | .unconstrainedBigUintDivMod _ _ => 2
@@ -562,7 +562,7 @@ private def emitU8Bytes2 (out : Nat) (valueHelper : String)
       s!" else \{ {valueHelper}(__v_{i}, __v_{j}, record) }"
     return #[.letStmt false s!"__v_{out}" (some "G") (.lit blockExpr)]
   else
-    -- 2-tuple outputs (Mul) or 3-tuple (ChainRotr7/4).
+    -- Multi-output byte operations.
     let blockExpr : String :=
       s!"if unconstrained \{ Bytes2::{unconShortcut}(&__v_{i}, &__v_{j}) }" ++
       s!" else \{ {valueHelper}(__v_{i}, __v_{j}, record) }"
@@ -723,8 +723,8 @@ def emitOp (out : Nat) (op : Op) : Array RustStmt :=
   | .u8And i j => emitU8Bytes2 out "bytes2_and_value" "and" i j 1
   | .u8Or i j => emitU8Bytes2 out "bytes2_or_value" "or" i j 1
   | .u8LessThan i j => emitU8Bytes2 out "bytes2_less_than_value" "less_than" i j 1
-  | .u8ChainRotr7 i j => emitU8Bytes2 out "bytes2_chain_rotr7_value" "chain_rotr7" i j 3
-  | .u8ChainRotr4 i j => emitU8Bytes2 out "bytes2_chain_rotr4_value" "chain_rotr4" i j 3
+  | .u8XorSplit7 i j => emitU8Bytes2 out "bytes2_xor_split7_value" "xor_split7" i j 2
+  | .u8XorSplit4 i j => emitU8Bytes2 out "bytes2_xor_split4_value" "xor_split4" i j 2
   | .u8Add i j => emitU8Add out i j
   | .u8Sub i j => emitU8Sub out i j
   | .u32LessThan a b => emitU32LessThan out a b
@@ -984,8 +984,8 @@ def optionalExecuteUses : Array (String × String) := #[
   ("bytes2_mul_value", "bytes2_mul_value"),
   ("bytes2_add_value", "bytes2_add_value"),
   ("bytes2_sub_value", "bytes2_sub_value"),
-  ("bytes2_chain_rotr7_value", "bytes2_chain_rotr7_value"),
-  ("bytes2_chain_rotr4_value", "bytes2_chain_rotr4_value"),
+  ("bytes2_xor_split7_value", "bytes2_xor_split7_value"),
+  ("bytes2_xor_split4_value", "bytes2_xor_split4_value"),
   ("unconstrained_big_uint_div_mod_helper", "unconstrained_big_uint_div_mod_helper"),
   ("g_inverse_value", "g_inverse_value"),
   ("CodegenBytes1 as Bytes1", "Bytes1::"),