Documentation

DY.EquationalTheory.KdfExtract

source
class DY.KdfExtract.CanKdfExtract (Bytes : Type u) :
Type u
  • kdfExtract (salt ikm : Bytes) : Bytes
Instances
    source
    structure DY.KdfExtract.KdfExtract.SubF (Bytes : Type) :
    Type
    • salt : Bytes
    • ikm : Bytes
    Instances For
      source
      @[instance_reducible]
      instance DY.KdfExtract.KdfExtract.instFunctorSizeOfSubF :
      ALaCarte.FunctorSizeOf SubF
      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[instance_reducible]
      instance DY.KdfExtract.KdfExtract.instRepresentableSubF :
      ALaCarte.Representable SubF
      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[instance_reducible]
      instance DY.KdfExtract.KdfExtract.instRepresentableDecidableEqSubF :
      ALaCarte.RepresentableDecidableEq SubF
      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[instance_reducible]
      instance DY.KdfExtract.KdfExtract.instRepresentableOrdSubF :
      ALaCarte.RepresentableOrd SubF
      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[instance_reducible]
      instance DY.KdfExtract.KdfExtract.instSubBytesFunctorSubF :
      SubBytesFunctor SubF
      Equations
      • One or more equations did not get rendered due to their size.
      source
      def DY.KdfExtract.KdfExtract.SubF.length [BytesFunctor] :
      Bytes.PartialLength SubF
      Equations
      Instances For
        source
        def DY.KdfExtract.SubF.length.internal [BytesFunctor] (id✝ : Fin 1) :
        Bytes.PartialLength (SubF.internal id✝)
        Equations
        Instances For
          source
          @[instance_reducible]
          def DY.KdfExtract.SubF.length [BytesFunctor] :
          Bytes.PartialLength SubF
          Equations
          Instances For
            source
            @[instance_reducible]
            def DY.KdfExtract.SubF :
            Type → Type
            Equations
            Instances For
              source
              def DY.KdfExtract.SubF.internal :
              Fin 1 → Type → Type
              Equations
              Instances For
                source
                @[reducible, inline]
                abbrev DY.KdfExtract.KdfExtract.SubF.pack [BytesFunctor] [BytesFunctor.Has SubF] (x : SubF Bytes) :
                Bytes
                Equations
                Instances For
                  source
                  @[instance_reducible]
                  instance DY.KdfExtract.instCanKdfExtractBytes [BytesFunctor] [BytesFunctor.Has SubF] :
                  CanKdfExtract Bytes
                  Equations
                  source
                  def DY.KdfExtract.kdfExtract.attackerKnowledge [BytesFunctor] [BytesFunctor.Has SubF] :
                  SubAttackerKnowledge SubF
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def DY.KdfExtract.attackerKnowledge.internal [BytesFunctor] [BytesFunctor.Has SubF] :
                    Fin 1 → SubAttackerKnowledge SubF
                    Equations
                    Instances For
                      source
                      @[instance_reducible]
                      def DY.KdfExtract.attackerKnowledge [BytesFunctor] [BytesFunctor.Has SubF] :
                      SubAttackerKnowledge SubF
                      Equations
                      Instances For
                        source
                        theorem DY.KdfExtract.attacker_knows_kdfExtract [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes] [BaseAttackerKnowledge] [AttackerKnowledge] [AttackerKnowledge.Has attackerKnowledge] (salt ikm : Bytes) (tr : ExecTrace) :
                        salt.AttackerKnows tr → ikm.AttackerKnows tr → (kdfExtract salt ikm).AttackerKnows tr
                        source
                        def DY.KdfExtract.KdfExtract.invariants [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] :
                        Bytes.PartialInvariants SubF
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          theorem DY.KdfExtract.KdfExtract.invariantsProofs [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesInvariants] :
                          Bytes.PartialInvariantsProofs invariants
                          source
                          def DY.KdfExtract.invariants.internal [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] (id✝ : Fin 1) :
                          Bytes.PartialInvariants (SubF.internal id✝)
                          Equations
                          Instances For
                            source
                            theorem DY.KdfExtract.invariantsProofs [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] :
                            Bytes.PartialInvariantsProofs invariants
                            source
                            theorem DY.KdfExtract.invariantsProofs.internal [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] (id✝ : Fin 1) :
                            Bytes.PartialInvariantsProofs (invariants.internal id✝)
                            source
                            @[instance_reducible]
                            def DY.KdfExtract.invariants [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] :
                            Bytes.PartialInvariants SubF
                            Equations
                            Instances For
                              source
                              @[simp]
                              theorem DY.KdfExtract.kdfExtract.WellFormed [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [BytesWellFormed] [BytesWellFormed.Has KdfExtract.invariants.well_formed] (salt ikm : Bytes) (tr : ProofTrace) :
                              (kdfExtract salt ikm).WellFormed tr = (salt.WellFormed tr ∧ ikm.WellFormed tr)
                              source
                              @[simp]
                              theorem DY.KdfExtract.kdfExtract.label [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [BytesInvariants] [BytesInvariants.Has invariants] (salt ikm : Bytes) (tr : ProofTrace) :
                              (kdfExtract salt ikm).label tr = (salt.label tr).meet (ikm.label tr)
                              source
                              @[simp]
                              theorem DY.KdfExtract.kdfExtract.Invariant [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [BytesInvariants] [BytesInvariants.Has invariants] (salt ikm : Bytes) (tr : ProofTrace) :
                              (kdfExtract salt ikm).Invariant tr = (salt.Invariant tr ∧ ikm.Invariant tr)
                              source
                              instance DY.KdfExtract.instHoareTriplePureBytesKdfExtractAndInvariantEqLabelLabelMeet [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] [BytesInvariants.Has invariants] (salt ikm : Bytes) :
                              HoareTriplePure (kdfExtract salt ikm) (fun (tr : ProofTrace) => salt.Invariant tr ∧ ikm.Invariant tr) fun (res : Bytes) (tr : ProofTrace) => res.Invariant tr ∧ res.label tr = (salt.label tr).meet (ikm.label tr)
                              source
                              instance DY.KdfExtract.instSubAttackerKnowledgeTheoremSubFAttackerKnowledge [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesFunctor] [BytesInvariants] [BytesFunctor.Has SubF] [BytesInvariants.Has invariants] :
                              SubAttackerKnowledgeTheorem kdfExtract.attackerKnowledge