Documentation

Cryptlib.Protocols.Sphinx.commands

Sphinx per-hop routing commands #

A routing-info block is a sequence of tag-prefixed commands, read until a null tag or the end of the block. Every command has a constant wire size.

source
inductive Cryptlib.Protocols.Sphinx.Commands.RoutingCommand :
Type

A routing command. null is the terminal marker (tag 0x00, no body).

Instances For
    source
    @[instance_reducible]
    instance Cryptlib.Protocols.Sphinx.Commands.instBEqRoutingCommand :
    BEq RoutingCommand
    Equations
    source
    def Cryptlib.Protocols.Sphinx.Commands.instBEqRoutingCommand.beq :
    RoutingCommand → RoutingCommand → Bool
    Equations
    Instances For
      source
      def Cryptlib.Protocols.Sphinx.Commands.instReprRoutingCommand.repr :
      RoutingCommand → ℕ → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[instance_reducible]
        instance Cryptlib.Protocols.Sphinx.Commands.instReprRoutingCommand :
        Repr RoutingCommand
        Equations
        source
        def Cryptlib.Protocols.Sphinx.Commands.RoutingCommand.toBytes :
        RoutingCommand → ByteArray
        Equations
        Instances For
          source
          @[simp]
          theorem Cryptlib.Protocols.Sphinx.Commands.RoutingCommand.nextNodeHop_toBytes_size (id mac : Vector UInt8 32) :
          (nextNodeHop id mac).toBytes.size = Constants.nextNodeHopLength

          A .nextNodeHop serializes to exactly nextNodeHopLength bytes.

          source
          def Cryptlib.Protocols.Sphinx.Commands.fromBytesOne (b : ByteArray) :
          Except String (Option RoutingCommand × ByteArray)

          Parse one command, returning it and the unconsumed remainder. none means an empty buffer or the null terminal.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Cryptlib.Protocols.Sphinx.Commands.parseAllFuel :
            ℕ → ByteArray → Except String (List RoutingCommand)

            parseAll with explicit fuel, so its behavior is provable.

            Equations
            Instances For
              source
              def Cryptlib.Protocols.Sphinx.Commands.parseAll (b : ByteArray) :
              Except String (List RoutingCommand)

              Parse every command in a routing-info block, stopping at null or the end of the buffer.

              Equations
              Instances For

                parseAll undoes commandsToBytes #

                source
                theorem Cryptlib.Protocols.Sphinx.Commands.parseAllFuel_append_zeros (cmds : List RoutingCommand) (hn : ∀ c ∈ cmds, c ≠ RoutingCommand.null) (zeros : ByteArray) (hzeros : (zeros.data.all fun (x : UInt8) => x == 0) = true) (fuel : ℕ) (hfuel : cmds.length ≤ fuel) :
                parseAllFuel fuel (List.foldl (fun (acc : ByteArray) (c : RoutingCommand) => acc ++ c.toBytes) ByteArray.empty cmds ++ zeros) = Except.ok cmds

                Parsing serialized commands followed by any all-zero padding recovers the commands, given enough fuel and no .null among them.

                source
                theorem Cryptlib.Protocols.Sphinx.Commands.parseAll_append_zeros (cmds : List RoutingCommand) (hn : ∀ c ∈ cmds, c ≠ RoutingCommand.null) (zeros : ByteArray) (hzeros : (zeros.data.all fun (x : UInt8) => x == 0) = true) :
                parseAll (List.foldl (fun (acc : ByteArray) (c : RoutingCommand) => acc ++ c.toBytes) ByteArray.empty cmds ++ zeros) = Except.ok cmds

                parseAll undoes commandsToBytes followed by any all-zero padding.