proof/AES_CertificateProof.bend source

proof/AES_CertificateProof.bend on the hub · documented module

import Base# Decidable equality makes certificates for Bool and Nat unique. These lemmas# compare proofs without evaluating the computation that produced each proof.def bool_code(a: Bool, b: Bool) -> Data:    match a b:        case False{} False{}: Unit        case True{} True{}: Unit        case _ _: Emptydef bool_code_refl(a: Bool) -> bool_code(a, a):    match a:        case False{}: Unit{}        case True{}: Unit{}def bool_encode(+a: Bool, +b: Bool, proof: {a == b : Bool}) -> bool_code(a, b):    %proof : bool_code(a, _)    bool_code_refl(a)def bool_decode(+a: Bool, +b: Bool, code: bool_code(a, b)) -> {a == b : Bool}:    match a b:        case False{} False{}: {==}        case True{} True{}: {==}        case False{} True{}: Empty.absurd({a == b : Bool}, code)        case True{} False{}: Empty.absurd({a == b : Bool}, code)def bool_decode_refl(+a: Bool) ->    {bool_decode(a, a, bool_code_refl(a)) == {==} : {a == a : Bool}}:    match a:        case False{}: {==}        case True{}: {==}def bool_decode_encode(+a: Bool, +b: Bool, +proof: {a == b : Bool}) ->    {bool_decode(a, b, bool_encode(a, b, proof)) == proof : {a == b : Bool}}:    %path@proof : {bool_decode(a, _, bool_encode(a, _, path)) == path :        {a == _ : Bool}}    bool_decode_refl(a)def bool_code_unique(+a: Bool, +b: Bool,    +first: bool_code(a, b), second: bool_code(a, b)) ->    {first == second : bool_code(a, b)}:    match a b:        case False{} False{}:            match first second:                case Unit{} Unit{}: {==}        case True{} True{}:            match first second:                case Unit{} Unit{}: {==}        case False{} True{}:            Empty.absurd({first == second : bool_code(a, b)}, first)        case True{} False{}:            Empty.absurd({first == second : bool_code(a, b)}, first)def bool_unique(+a: Bool, +b: Bool,    +first: {a == b : Bool}, +second: {a == b : Bool}) ->    {first == second : {a == b : Bool}}:    +first_code = bool_encode(a, b, first)    +second_code = bool_encode(a, b, second)    codes_same = bool_code_unique(a, b, first_code, second_code)    decoded_same = Equal.cong(bool_code(a, b), {a == b : Bool},        code => bool_decode(a, b, code), first_code, second_code, codes_same)    Equal.trans({a == b : Bool}, first, bool_decode(a, b, first_code), second,        Equal.sym({a == b : Bool}, bool_decode(a, b, first_code), first,            bool_decode_encode(a, b, first)),        Equal.trans({a == b : Bool}, bool_decode(a, b, first_code),            bool_decode(a, b, second_code), second, decoded_same,            bool_decode_encode(a, b, second)))def nat_code(a: Nat, b: Nat) -> Data:    match a b:        case 0n 0n: Unit        case 1n+p 1n+q: nat_code(p, q)        case _ _: Emptydef nat_code_refl(a: Nat) -> nat_code(a, a):    match a:        case 0n: Unit{}        case 1n+p: nat_code_refl(p)def nat_encode(+a: Nat, +b: Nat, proof: {a == b : Nat}) -> nat_code(a, b):    %proof : nat_code(a, _)    nat_code_refl(a)def nat_decode(+a: Nat, +b: Nat, code: nat_code(a, b)) -> {a == b : Nat}:    match a b:        case 0n 0n: {==}        case 0n 1n+q: Empty.absurd({a == b : Nat}, code)        case 1n+p 0n: Empty.absurd({a == b : Nat}, code)        case 1n+p 1n+q:            Equal.cong(Nat, Nat, value => 1n+value, p, q,                nat_decode(p, q, code))def nat_decode_refl(+a: Nat) ->    {nat_decode(a, a, nat_code_refl(a)) == {==} : {a == a : Nat}}:    match a:        case 0n: {==}        case 1n+p:            %Equal.sym({p == p : Nat},                nat_decode(p, p, nat_code_refl(p)), {==},                nat_decode_refl(p)) :                {Equal.cong(Nat, Nat, value => 1n+value, p, p, _) == {==} :                    {1n+p == 1n+p : Nat}}            {==}def nat_decode_encode(+a: Nat, +b: Nat, +proof: {a == b : Nat}) ->    {nat_decode(a, b, nat_encode(a, b, proof)) == proof : {a == b : Nat}}:    %path@proof : {nat_decode(a, _, nat_encode(a, _, path)) == path :        {a == _ : Nat}}    nat_decode_refl(a)def nat_code_unique(+a: Nat, +b: Nat,    +first: nat_code(a, b), second: nat_code(a, b)) ->    {first == second : nat_code(a, b)}:    match a b:        case 0n 0n:            match first second:                case Unit{} Unit{}: {==}        case 0n 1n+q:            Empty.absurd({first == second : nat_code(a, b)}, first)        case 1n+p 0n:            Empty.absurd({first == second : nat_code(a, b)}, first)        case 1n+p 1n+q: nat_code_unique(p, q, first, second)def nat_unique(+a: Nat, +b: Nat,    +first: {a == b : Nat}, +second: {a == b : Nat}) ->    {first == second : {a == b : Nat}}:    +first_code = nat_encode(a, b, first)    +second_code = nat_encode(a, b, second)    codes_same = nat_code_unique(a, b, first_code, second_code)    decoded_same = Equal.cong(nat_code(a, b), {a == b : Nat},        code => nat_decode(a, b, code), first_code, second_code, codes_same)    Equal.trans({a == b : Nat}, first, nat_decode(a, b, first_code), second,        Equal.sym({a == b : Nat}, nat_decode(a, b, first_code), first,            nat_decode_encode(a, b, first)),        Equal.trans({a == b : Nat}, nat_decode(a, b, first_code),            nat_decode(a, b, second_code), second, decoded_same,            nat_decode_encode(a, b, second)))