Componolit/libsparkcrypto

Proof absence-of-runtime errors

senier opened this issue · 0 comments

senier commented

A couple of VCs remain unproved (or get only proved with Isabelle). The goal is to prove absence of runtime errors using SPARKprove and leave functional properties to Isabelle.

  • src/shared/generic/lsc-types.ads
  • src/shared/generic/lsc.ads
  • src/shared/generic/lsc-aes.ads
  • src/shared/generic/lsc-aes-cbc.ads
  • src/shared/generic/lsc-sha2.ads
  • src/shared/generic/lsc-sha2-hmac.ads
  • src/shared/generic/lsc-sha1.ads
  • src/shared/generic/lsc-sha1-hmac.ads
  • src/shared/generic/lsc-ripemd160.ads
  • src/shared/generic/lsc-ripemd160-hmac.ads
  • src/shared/generic/lsc-internal-io.ads
  • src/shared/generic/lsc-internal.ads
  • src/shared/generic/lsc-internal-types.ads
  • src/shared/generic/lsc-internal-aes.ads
  • src/shared/generic/lsc-internal-aes-cbc.ads
  • src/shared/generic/lsc-internal-aes-print.ads
  • src/shared/generic/lsc-internal-aes-tables.ads
  • src/shared/generic/lsc-internal-byteorder32.ads
  • src/shared/generic/lsc-internal-byteorder64.ads
  • src/shared/generic/lsc-internal-byteswap32.ads
  • src/shared/generic/lsc-internal-byteswap64.ads
  • src/shared/generic/lsc-internal-convert.ads
  • src/shared/generic/lsc-internal-convert_hash.ads
  • src/shared/generic/lsc-internal-convert_hmac.ads
  • src/shared/generic/lsc-internal-hmac_ripemd160.ads
  • src/shared/generic/lsc-internal-hmac_sha1.ads
  • src/shared/generic/lsc-internal-hmac_sha256.ads
  • src/shared/generic/lsc-internal-hmac_sha384.ads
  • src/shared/generic/lsc-internal-hmac_sha512.ads
  • src/shared/generic/lsc-internal-sha256.ads
  • src/shared/generic/lsc-internal-sha256-tables.ads
  • src/shared/generic/lsc-internal-sha512.ads
  • src/shared/generic/lsc-internal-sha512-tables.ads
  • src/shared/generic/lsc-internal-ops32.ads
  • src/shared/generic/lsc-internal-ops64.ads
  • src/shared/generic/lsc-internal-pad32.ads
  • src/shared/generic/lsc-internal-pad64.ads
  • src/shared/generic/lsc-internal-ripemd160.ads
  • src/shared/generic/lsc-internal-ripemd160-print.ads
  • src/shared/generic/lsc-internal-sha1.ads
  • src/shared/generic/lsc-internal-math_int.ads
  • src/shared/generic/lsc-internal-ec.ads
  • src/shared/generic/lsc-internal-ec_signature.ads
  • src/shared/generic/lsc-internal-bignum.ads