def unequal_from_bool

qasim-bend-kit@0.1.0.2 · proof/AES_TagCompareProof.bend:103

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES

103def unequal_from_bool(+a: List<&2, U32>, +b: List<&2, U32>,
104    compared: Bool,
105    link: {compared == AES.bytes_equal_full_scan(a, b) : Bool},
106    unequal: {a != b : List<&2, U32>}) ->
107    {AES.bytes_equal_full_scan(a, b) == False{} : Bool}:
108    match compared:
109        case False{}:
110            Equal.sym(Bool, False{}, AES.bytes_equal_full_scan(a, b), link)
111        case True{}:
112            accepted = Equal.sym(Bool, True{},
113                AES.bytes_equal_full_scan(a, b), link)
114            Empty.absurd(
115                {AES.bytes_equal_full_scan(a, b) == False{} : Bool},
116                unequal(equal_sound(a, b, accepted)))