Documentation

Examples.MerkleTree.Proof

source
def DY.Example.MerkleTree.IsHashCollision {Bytes : Type} [Hash.CanHash Bytes] (x : Bytes × Bytes) :
Prop
Equations
Instances For
    source
    @[irreducible]
    def DY.Example.MerkleTree.merkleTreeHash_reduceCollision {Bytes : Type} [Comparse.BytesLike Bytes] [Hash.CanHash Bytes] {α : Type} (mf : Comparse.ExtensibleMessageFormat Bytes α) [DecidableEq Bytes] [DecidableEq α] (l1 l2 : List α) :
    Bytes × Bytes
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem DY.Example.MerkleTree.merkleTreeHash_reduceCollision_correct {Bytes : Type} [Comparse.BytesLike Bytes] [Hash.CanHash Bytes] {α : Type} (mf : Comparse.ExtensibleMessageFormat Bytes α) [DecidableEq Bytes] [DecidableEq α] [mf.IsNonAmbiguous] (l1 l2 : List α) (h : merkleTreeHash mf l1 = merkleTreeHash mf l2) :
      l1 = l2 ∨ IsHashCollision (merkleTreeHash_reduceCollision mf l1 l2)
      source
      def DY.Example.MerkleTree.checkInclusionProof_reduceHashCollision {Bytes : Type} [Comparse.BytesLike Bytes] [Hash.CanHash Bytes] {α : Type} (mf : Comparse.ExtensibleMessageFormat Bytes α) [DecidableEq Bytes] [DecidableEq α] (proof : List Bytes) (leaf : α) (i : Nat) (l : List α) :
      Bytes × Bytes
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem DY.Example.MerkleTree.checkInclusionProof_reduceHashCollision_correct {Bytes : Type} [Comparse.BytesLike Bytes] [Hash.CanHash Bytes] {α : Type} (mf : Comparse.ExtensibleMessageFormat Bytes α) [DecidableEq Bytes] [DecidableEq α] [mf.IsNonAmbiguous] (proof : List Bytes) (leaf : α) (i : Nat) (l : List α) (h : checkInclusionProof mf proof leaf i (merkleTreeHash mf l) l.length) :
        l[i]? = some leaf ∨ IsHashCollision (checkInclusionProof_reduceHashCollision mf proof leaf i l)
        source
        class DY.Example.MerkleTree.HasProofTrace extends DY.Example.MerkleTree.HasExecTrace :
        Type 1
        Instances
          source
          structure DY.Example.MerkleTree.LongTermKeyUsage :
          Type
          Instances For
            source
            @[instance_reducible]
            instance DY.Example.MerkleTree.instParseableSerializeableLongTermKeyUsage [HasProofTrace] :
            Comparse.ParseableSerializeable LongTermKeyUsage
            Equations
            • One or more equations did not get rendered due to their size.
            source
            def DY.Example.MerkleTree.mkLongTermKeyUsage [HasProofTrace] (me : Participant) :
            Usage
            Equations
            Instances For
              source
              @[instance_reducible]
              instance DY.Example.MerkleTree.MerkleTreeSignPred [HasProofTrace] :
              Signature.SignPred
              Equations
              • One or more equations did not get rendered due to their size.
              source
              instance DY.Example.MerkleTree.instSignPredProof_examples [HasProofTrace] [BytesInvariants] :
              Signature.SignPredProof
              source
              class DY.Example.MerkleTree.HasBytesInvariants extends DY.Example.MerkleTree.HasProofTrace :
              Type 1
              Instances
                source
                @[instance_reducible]
                instance DY.Example.MerkleTree.TheEvent.invariant [HasProofTrace] :
                ProtocolEvent.EventInv TheEvent
                Equations
                • One or more equations did not get rendered due to their size.
                source
                @[instance_reducible]
                instance DY.Example.MerkleTree.instProofConfigMkLongTermKeyUsageLabel [HasBytesInvariants] :
                LongTermKeys.ProofConfig "MerkleTree PKI" mkLongTermKeyUsage (LongTermKeys.label "MerkleTree PKI")
                Equations
                • One or more equations did not get rendered due to their size.
                source
                @[instance_reducible]
                instance DY.Example.MerkleTree.ServerStateInv [HasBytesInvariants] :
                PersistentLocalState.CompromisableLocalStateInv ServerState
                Equations
                • One or more equations did not get rendered due to their size.
                source
                class DY.Example.MerkleTree.HasTraceInvariant extends DY.Example.MerkleTree.HasBytesInvariants :
                Type 1
                Instances
                  source
                  instance DY.Example.MerkleTree.instReachableImpliesInvariantReachability [HasTraceInvariant] :
                  ReachableImpliesInvariant Server.authenticate.reachability
                  source
                  instance DY.Example.MerkleTree.instReachableImpliesInvariantReachability_1 [HasTraceInvariant] :
                  ReachableImpliesInvariant Server.proveInclusion.reachability
                  source
                  instance DY.Example.MerkleTree.instReachableImpliesInvariantReachability_2 [HasTraceInvariant] :
                  ReachableImpliesInvariant Client.checkInclusion.reachability
                  source
                  instance DY.Example.MerkleTree.instReachableImpliesInvariantReachability_3 [HasTraceInvariant] :
                  ReachableImpliesInvariant ServerState.compromise.reachability