Trunc.lean🔗

Tier 2 · definitions used by the symbolic proof 13 headline theorems depend on it 25 of 67 lines trusted source ↗

Read the definitions shown. Only the declarations that the headline statements use are shown, with the namespace, section, open and variable commands needed to read them. The collapsed runs are theorems, which Lean checks, and definitions that no headline statement uses.

Declarations on this page (11)

8-Byte MAC Truncation

DyLean term constructor and attacker deduction rule for 8-byte tag truncation (MAC_LENGTH = 8).

namespace DY.Trunc

class CanTrunc8L24–26 ↗#

public
class CanTrunc8 (Bytes: Type u) where
  trunc8: (x: Bytes) → Bytes

export CanTrunc8 (trunc8)

def trunc8LengthL30–31 ↗#

@[expose] public
def trunc8Length := 8

namespace Trunc8

structure SubFL35–37 ↗#

public
structure SubF (Bytes: Type) where
  input: Bytes

instanceL39 ↗#

public instance: ALaCarte.FunctorSizeOf SubF := .unary SubF.input

instanceL40 ↗#

public instance: SubBytesFunctor SubF := .unary SubF.input SubF.mk

def SubF.lengthL42–44 ↗#

@[expose] public
def SubF.length [BytesFunctor]: Bytes.PartialLength SubF :=
  fun ⟨input⟩ rec => Nat.min (rec input) trunc8Length

end Trunc8

#combineL48–49 ↗#

#combine into BytesFunctor, BytesLength from
  Trunc8,

variable [BytesFunctor] [BytesFunctor.Has SubF]

abbrev Trunc8.SubF.packL53–54 ↗#

public
abbrev Trunc8.SubF.pack (x: Trunc8.SubF Bytes) := BytesView.pack x

instanceL56–58 ↗#

public
instance: CanTrunc8 Bytes where
  trunc8 input := ({input}: Trunc8.SubF Bytes).pack

def trunc8.attackerKnowledgeL60–62 ↗#

@[expose] public
def trunc8.attackerKnowledge: SubAttackerKnowledge SubF where
  pred p out := ∃ inp, out = trunc8 inp ∧ p inp

#combineL64–68 ↗#

#combine [BytesFunctor.Has SubF] into attackerKnowledge' from
  trunc8,

end DY.Trunc