proof/AES_CertificateProof.bend checks

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

1 import

import Base

Definitions

def bool_code source · line 5 · raw

@a:Bool -> @b:Bool -> Data

Decidable equality makes certificates for Bool and Nat unique. These lemmas compare proofs without evaluating the computation that produced each proof.

def bool_code_refl source · line 11 · raw

@a:Bool -> bool_code(a, a)

def bool_encode source · line 16 · raw

@+a:Bool -> @+b:Bool -> @proof:{a == b : Bool} -> bool_code(a, b)

def bool_decode source · line 20 · raw

@+a:Bool -> @+b:Bool -> @code:bool_code(a, b) -> {a == b : Bool}

def bool_decode_refl source · line 27 · raw

@+a:Bool -> {bool_decode(a, a, bool_code_refl(a)) == {==} : {a == a : Bool}}

def bool_decode_encode source · line 33 · raw

@+a:Bool -> @+b:Bool -> @+proof:{a == b : Bool} -> {bool_decode(a, b, bool_encode(a, b, proof)) == proof : {a == b : Bool}}

def bool_code_unique source · line 39 · raw

@+a:Bool -> @+b:Bool -> @+first:bool_code(a, b) -> @second:bool_code(a, b) -> {first == second : bool_code(a, b)}

def bool_unique source · line 54 · raw

@+a:Bool -> @+b:Bool -> @+first:{a == b : Bool} -> @+second:{a == b : Bool} -> {first == second : {a == b : Bool}}

def nat_code source · line 69 · raw

@a:Nat -> @b:Nat -> Data

def nat_code_refl source · line 75 · raw

@a:Nat -> nat_code(a, a)

def nat_encode source · line 80 · raw

@+a:Nat -> @+b:Nat -> @proof:{a == b : Nat} -> nat_code(a, b)

def nat_decode source · line 84 · raw

@+a:Nat -> @+b:Nat -> @code:nat_code(a, b) -> {a == b : Nat}

def nat_decode_refl source · line 93 · raw

@+a:Nat -> {nat_decode(a, a, nat_code_refl(a)) == {==} : {a == a : Nat}}

def nat_decode_encode source · line 105 · raw

@+a:Nat -> @+b:Nat -> @+proof:{a == b : Nat} -> {nat_decode(a, b, nat_encode(a, b, proof)) == proof : {a == b : Nat}}

def nat_code_unique source · line 111 · raw

@+a:Nat -> @+b:Nat -> @+first:nat_code(a, b) -> @second:nat_code(a, b) -> {first == second : nat_code(a, b)}

def nat_unique source · line 124 · raw

@+a:Nat -> @+b:Nat -> @+first:{a == b : Nat} -> @+second:{a == b : Nat} -> {first == second : {a == b : Nat}}