Combining two schemes

Splitting a concatenated encoding, and running a state action against half of a product state.

def Cryptlib.Util.Combine.sliftL {σ₁ : Type (max u_1 u_2)} {σ₂ : Type u_2} {α : Type (max u_1 u_2)} (x : StateM σ₁ α) : StateM (σ₁ × σ₂) α

Run a total state action against the left half of a product state.

Equations

• Cryptlib.Util.Combine.sliftL x (s₁, s₂) = ((x s₁).fst, (x s₁).snd, s₂)

def Cryptlib.Util.Combine.sliftR {σ₁ : Type u_1} {σ₂ α : Type (max u_2 u_1)} (x : StateM σ₂ α) : StateM (σ₁ × σ₂) α

Run a total state action against the right half of a product state.

Equations

• Cryptlib.Util.Combine.sliftR x (s₁, s₂) = ((x s₂).fst, s₁, (x s₂).snd)

def Cryptlib.Util.Combine.splitL {a b : Nat} (v : Vector UInt8 (a + b)) : Vector UInt8 a

The first a bytes of a concatenation.

Equations

• Cryptlib.Util.Combine.splitL v = Vector.cast ⋯ (v.take a)

def Cryptlib.Util.Combine.splitR {a b : Nat} (v : Vector UInt8 (a + b)) : Vector UInt8 b

The remaining b bytes of a concatenation.

Equations

• Cryptlib.Util.Combine.splitR v = Vector.cast ⋯ (v.drop a)

theorem Cryptlib.Util.Combine.splitL_append {a b : Nat} (v : Vector UInt8 a) (w : Vector UInt8 b) : splitL (v ++ w) = v

theorem Cryptlib.Util.Combine.splitR_append {a b : Nat} (v : Vector UInt8 a) (w : Vector UInt8 b) : splitR (v ++ w) = w