~/bend-docscommunity

proof/AES_StringEqProof.bend checks

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

2 imports
import Base
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/proofs/string_compare.bend as Compare

Definitions

def false_type source · line 4 · raw

@b:Bool -> Data

def false_true source · line 9 · raw

@e:{False{} == True{} : Bool} -> Empty

def cmp_eq_of_true source · line 13 · raw

@c:Cmp -> @accepted:{Cmp.is_eq(c) == True{} : Bool} -> {c == EQ{} : Cmp}

def tag_is_snd source · line 20 · raw

@r:Pair(Pair(String, String), Cmp) -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/proofs/string_compare.comparison_tag(String, r) == Pair.snd(Pair(String, String), Cmp, r) : Cmp}

def string_eq_sound source · line 26 · raw

@+a:String -> @+b:String -> @accepted:{String.eq(a, b) == True{} : Bool} -> {a == b : String}

def string_eq_self source · line 35 · raw

@+s:String -> {String.eq(s, s) == True{} : Bool}