proof/AES_CanonicalProof.bend checks

raw source on the hub · import qasim-bend-kit@0.1.0.2/proof/AES_CanonicalProof.bend as AES_CanonicalProof

3 imports

import Base
import ../libs/AES256GCM.bend as AES
import ./AES_StringEqProof.bend as StringEq

Definitions

def encoding_or source · line 5 · raw

@text:String -> @result:Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope> -> String

def canonical_sound_done source · line 11 · raw

@+text:String -> @+found:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @canonical:Bool -> @link:{canonical == String.eq(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encode(found), text) : Bool} -> @accepted:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.parse_canonical_decision(text, found, canonical) == Done{envelope} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encode(envelope) == text : String}

def canonical_sound source · line 40 · raw

@+text:String -> @result:Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope> -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @accepted:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.parse_canonical(text, result) == Done{envelope} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encode(envelope) == text : String}

def canonical_law source · line 58 · raw

@+text:String -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @+parsed:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.parse(text) == Done{envelope} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>} -> {Result.map(&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope, String, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encode, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.parse(text)) == Done{text} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, String>}

def map_done_text source · line 78 · raw

@+text:String -> @result:Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, String> -> String

def canonical_map_from_encoded source · line 84 · raw

@+text:String -> @result:Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope> -> @encoded:{Result.map(&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope, String, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encode, result) == Done{text} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, String>} -> {Result.map(&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope, String, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encode, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.parse_canonical(text, result)) == Done{text} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, String>}