Documentation

DY.EquationalTheory.Concat

source
class DY.Concat.CanConcat (Bytes : Type u) :
Type u
  • concat : Bytes → Bytes → Bytes
  • split : Bytes → Nat → Option (Bytes × Bytes)
Instances
    source
    structure DY.Concat.Concat.SubF (Bytes : Type) :
    Type
    • lhs : Bytes
    • rhs : Bytes
    Instances For
      source
      @[instance_reducible]
      instance DY.Concat.Concat.instFunctorSizeOfSubF :
      ALaCarte.FunctorSizeOf SubF
      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[instance_reducible]
      instance DY.Concat.Concat.instRepresentableSubF :
      ALaCarte.Representable SubF
      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[instance_reducible]
      instance DY.Concat.Concat.instRepresentableDecidableEqSubF :
      ALaCarte.RepresentableDecidableEq SubF
      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[instance_reducible]
      instance DY.Concat.Concat.instRepresentableOrdSubF :
      ALaCarte.RepresentableOrd SubF
      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[instance_reducible]
      instance DY.Concat.Concat.instSubBytesFunctorSubF :
      SubBytesFunctor SubF
      Equations
      • One or more equations did not get rendered due to their size.
      source
      def DY.Concat.Concat.SubF.length [BytesFunctor] :
      Bytes.PartialLength SubF
      Equations
      • { lhs := lhs, rhs := rhs }.length rec_2 = rec_2 lhs ⋯ + rec_2 rhs ⋯
      Instances For
        source
        def DY.Concat.SubF.length.internal [BytesFunctor] (id✝ : Fin 1) :
        Bytes.PartialLength (SubF.internal id✝)
        Equations
        Instances For
          source
          def DY.Concat.SubF.internal :
          Fin 1 → Type → Type
          Equations
          Instances For
            source
            @[instance_reducible]
            def DY.Concat.SubF :
            Type → Type
            Equations
            Instances For
              source
              @[instance_reducible]
              def DY.Concat.SubF.length [BytesFunctor] :
              Bytes.PartialLength SubF
              Equations
              Instances For
                source
                @[reducible, inline]
                abbrev DY.Concat.Concat.SubF.pack [BytesFunctor] [BytesFunctor.Has SubF] (x : SubF Bytes) :
                Bytes
                Equations
                Instances For
                  source
                  @[instance_reducible]
                  instance DY.Concat.instCanConcatBytes [BytesFunctor] [BytesFunctor.Has SubF] [BytesLength] :
                  CanConcat Bytes
                  Equations
                  • One or more equations did not get rendered due to their size.
                  source
                  theorem DY.Concat.split_concat [BytesFunctor] [BytesFunctor.Has SubF] [BytesLength] (lhs rhs : Bytes) :
                  split (concat lhs rhs) lhs.length = some (lhs, rhs)
                  source
                  theorem DY.Concat.concat_split [BytesFunctor] [BytesFunctor.Has SubF] [BytesLength] (buf : Bytes) (i : Nat) (lhs rhs : Bytes) :
                  split buf i = some (lhs, rhs) → concat lhs rhs = buf
                  source
                  @[simp]
                  theorem DY.Concat.length_concat [BytesFunctor] [BytesFunctor.Has SubF] [BytesLength] [BytesLength.Has SubF.length] (lhs rhs : Bytes) :
                  (concat lhs rhs).length = lhs.length + rhs.length
                  source
                  @[simp]
                  theorem DY.Concat.length_split [BytesFunctor] [BytesFunctor.Has SubF] [BytesLength] [BytesLength.Has SubF.length] (buf : Bytes) (i : Nat) (lhs rhs : Bytes) :
                  split buf i = some (lhs, rhs) → lhs.length = i ∧ i + rhs.length = buf.length
                  source
                  def DY.Concat.concat.attackerKnowledge [BytesFunctor] [BytesFunctor.Has SubF] [BytesLength] :
                  SubAttackerKnowledge SubF
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def DY.Concat.splitLeft.attackerKnowledge [BytesFunctor] [BytesFunctor.Has SubF] [BytesLength] :
                    SubAttackerKnowledge SubF
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      def DY.Concat.splitRight.attackerKnowledge [BytesFunctor] [BytesFunctor.Has SubF] [BytesLength] :
                      SubAttackerKnowledge SubF
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        @[instance_reducible]
                        def DY.Concat.attackerKnowledge [BytesFunctor] [BytesFunctor.Has SubF] [BytesLength] :
                        SubAttackerKnowledge SubF
                        Equations
                        Instances For
                          source
                          def DY.Concat.attackerKnowledge.internal [BytesFunctor] [BytesFunctor.Has SubF] [BytesLength] :
                          Fin 3 → SubAttackerKnowledge SubF
                          Equations
                          Instances For
                            source
                            theorem DY.Concat.attacker_knows_concat [BytesFunctor] [BytesFunctor.Has SubF] [BytesLength] [ExecTraceTypes] [BaseAttackerKnowledge] [AttackerKnowledge] [AttackerKnowledge.Has attackerKnowledge] (lhs rhs : Bytes) (tr : ExecTrace) :
                            lhs.AttackerKnows tr → rhs.AttackerKnows tr → (concat lhs rhs).AttackerKnows tr
                            source
                            theorem DY.Concat.attacker_knows_split [BytesFunctor] [BytesFunctor.Has SubF] [BytesLength] [ExecTraceTypes] [BaseAttackerKnowledge] [AttackerKnowledge] [AttackerKnowledge.Has attackerKnowledge] (buf : Bytes) (i : Nat) (tr : ExecTrace) :
                            buf.AttackerKnows tr → match split buf i with | none => True | some (lhs, rhs) => lhs.AttackerKnows tr ∧ rhs.AttackerKnows tr
                            source
                            def DY.Concat.Concat.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.Concat.Concat.invariantsProofs [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesInvariants] :
                              Bytes.PartialInvariantsProofs invariants
                              source
                              theorem DY.Concat.invariantsProofs.internal [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] (id✝ : Fin 1) :
                              Bytes.PartialInvariantsProofs (invariants.internal id✝)
                              source
                              @[instance_reducible]
                              def DY.Concat.invariants [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] :
                              Bytes.PartialInvariants SubF
                              Equations
                              Instances For
                                source
                                def DY.Concat.invariants.internal [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] (id✝ : Fin 1) :
                                Bytes.PartialInvariants (SubF.internal id✝)
                                Equations
                                Instances For
                                  source
                                  theorem DY.Concat.invariantsProofs [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] :
                                  Bytes.PartialInvariantsProofs invariants
                                  source
                                  @[simp]
                                  theorem DY.Concat.concat.WellFormed [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [BytesLength] [BytesWellFormed] [BytesWellFormed.Has Concat.invariants.well_formed] (lhs rhs : Bytes) (tr : ProofTrace) :
                                  (concat lhs rhs).WellFormed tr = (lhs.WellFormed tr ∧ rhs.WellFormed tr)
                                  source
                                  @[simp]
                                  theorem DY.Concat.concat.label [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [BytesLength] [BytesInvariants] [BytesInvariants.Has invariants] (lhs rhs : Bytes) (tr : ProofTrace) :
                                  (concat lhs rhs).label tr = (lhs.label tr).meet (rhs.label tr)
                                  source
                                  @[simp]
                                  theorem DY.Concat.concat.Invariant [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [BytesLength] [BytesInvariants] [BytesInvariants.Has invariants] (lhs rhs : Bytes) (tr : ProofTrace) :
                                  (concat lhs rhs).Invariant tr = (lhs.Invariant tr ∧ rhs.Invariant tr)
                                  source
                                  @[simp]
                                  theorem DY.Concat.split.WellFormed [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [BytesLength] [BytesWellFormed] [BytesWellFormed.Has Concat.invariants.well_formed] (buf : Bytes) (i : Nat) (tr : ProofTrace) :
                                  match split buf i with | none => True | some (lhs, rhs) => buf.WellFormed tr = (lhs.WellFormed tr ∧ rhs.WellFormed tr)
                                  source
                                  @[simp]
                                  theorem DY.Concat.split.label [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [BytesLength] [BytesInvariants] [BytesInvariants.Has invariants] (buf : Bytes) (i : Nat) (tr : ProofTrace) :
                                  match split buf i with | none => True | some (lhs, rhs) => buf.label tr = (lhs.label tr).meet (rhs.label tr)
                                  source
                                  @[simp]
                                  theorem DY.Concat.split.Invariant [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [BytesLength] [BytesInvariants] [BytesInvariants.Has invariants] (buf : Bytes) (i : Nat) (tr : ProofTrace) :
                                  buf.Invariant tr → match split buf i with | none => True | some (lhs, rhs) => lhs.Invariant tr ∧ rhs.Invariant tr
                                  source
                                  instance DY.Concat.instSubAttackerKnowledgeTheoremSubFAttackerKnowledge [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesFunctor] [BytesInvariants] [BytesFunctor.Has SubF] [BytesLength] [BytesInvariants.Has invariants] :
                                  SubAttackerKnowledgeTheorem concat.attackerKnowledge
                                  source
                                  instance DY.Concat.instSubAttackerKnowledgeTheoremSubFAttackerKnowledge_1 [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesFunctor] [BytesInvariants] [BytesFunctor.Has SubF] [BytesLength] [BytesInvariants.Has invariants] :
                                  SubAttackerKnowledgeTheorem splitLeft.attackerKnowledge
                                  source
                                  instance DY.Concat.instSubAttackerKnowledgeTheoremSubFAttackerKnowledge_2 [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesFunctor] [BytesInvariants] [BytesFunctor.Has SubF] [BytesLength] [BytesInvariants.Has invariants] :
                                  SubAttackerKnowledgeTheorem splitRight.attackerKnowledge