proof/AES_TagCompareProof.bend checks

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

4 imports

import Base
import ../libs/AES256GCM.bend as AES
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/subtle/word.bend as SW
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/logic.bend as Logic

Definitions

def diff_same source · line 6 · raw

@+a:List<&2, U32> -> @+acc:U32 -> @acc_zero:{U32.is_eq(acc, 0) == True{} : Bool} -> {U32.is_eq(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_difference.go(a, a, acc), 0) == True{} : Bool}

def equal_same source · line 23 · raw

@+a:List<&2, U32> -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_equal_full_scan(a, a) == True{} : Bool}

def equal_of_equal source · line 27 · raw

@+a:List<&2, U32> -> @+b:List<&2, U32> -> @same:{a == b : List<&2, U32>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_equal_full_scan(a, b) == True{} : Bool}

def diff_acc_zero source · line 36 · raw

@+a:List<&2, U32> -> @+b:List<&2, U32> -> @+acc:U32 -> @zero:{U32.is_eq(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_difference.go(a, b, acc), 0) == True{} : Bool} -> {U32.is_eq(acc, 0) == True{} : Bool}

def diff_list_sound source · line 61 · raw

@+a:List<&2, U32> -> @+b:List<&2, U32> -> @+acc:U32 -> @+zero:{U32.is_eq(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_difference.go(a, b, acc), 0) == True{} : Bool} -> {a == b : List<&2, U32>}

def equal_sound source · line 98 · raw

@+a:List<&2, U32> -> @+b:List<&2, U32> -> @accepted:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_equal_full_scan(a, b) == True{} : Bool} -> {a == b : List<&2, U32>}

def unequal_from_bool source · line 103 · raw

@+a:List<&2, U32> -> @+b:List<&2, U32> -> @compared:Bool -> @link:{compared == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_equal_full_scan(a, b) : Bool} -> @unequal:(@_:{a == b : List<&2, U32>} -> Empty) -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_equal_full_scan(a, b) == False{} : Bool}

def unequal_is_false source · line 118 · raw

@+a:List<&2, U32> -> @+b:List<&2, U32> -> @unequal:(@_:{a == b : List<&2, U32>} -> Empty) -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_equal_full_scan(a, b) == False{} : Bool}