def aes_nat_eq_step_status

qasim-bend-kit@0.1.0.2 · PROOF.bend:393

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

393def aes_nat_eq_step_status(+a: Nat, +b: Nat,
394    result: Maybe<&0, {a == b : Nat}>) ->
395    {Maybe.is_some(&0, {1n+a == 1n+b : Nat},
396        AES.aes_nat_eq_step(a, b, result)) ==
397     Maybe.is_some(&0, {a == b : Nat}, result) : Bool}:
398    match result:
399        case None{}: {==}
400        case Some{proof}: {==}