package fstar

You can search for identifiers within the package.

in-package search v0.2.0

Legend:
Library
Module
Module type
Parameter
Class
Class type

type 'n nbytes = FStar_Bytes.bytes

type tag = Prims.unit nbytes

val sha1 : FStar_Bytes.bytes -> tag

type hmac_key = Prims.unit nbytes

val hmac_sha1_keygen : Prims.unit -> hmac_key

val hmac_sha1 : hmac_key -> FStar_Bytes.bytes -> tag

val hmac_sha1_verify : hmac_key -> FStar_Bytes.bytes -> tag -> Prims.bool

type block = Prims.unit nbytes

type cipher = Prims.unit nbytes

type aes_key = Prims.unit nbytes

type aes_iv = Prims.unit nbytes

val aes_128_keygen : Prims.unit -> aes_key

val aes_128_decrypt : aes_key -> cipher -> block

val aes_128_encrypt : aes_key -> block -> cipher

val aes_128_ivgen : Prims.unit -> aes_iv

val aes_128_cbc_decrypt : 
  aes_key ->
  aes_iv ->
  FStar_Bytes.bytes ->
  FStar_Bytes.bytes

val aes_128_cbc_encrypt : 
  aes_key ->
  aes_iv ->
  FStar_Bytes.bytes ->
  FStar_Bytes.bytes

type rsa_pkey = {

}

val __proj__Mkrsa_pkey__item__modulus : rsa_pkey -> FStar_Bytes.bytes

val __proj__Mkrsa_pkey__item__exponent : rsa_pkey -> FStar_Bytes.bytes

type rsa_skey = rsa_pkey * FStar_Bytes.bytes

val rsa_keygen : Prims.unit -> rsa_skey

val rsa_pk : rsa_skey -> rsa_pkey

val rsa_pkcs1_encrypt : rsa_pkey -> FStar_Bytes.bytes -> FStar_Bytes.bytes

val rsa_pkcs1_decrypt : rsa_skey -> FStar_Bytes.bytes -> FStar_Bytes.bytes

type sigv = FStar_Bytes.bytes

val rsa_sha1 : rsa_skey -> FStar_Bytes.bytes -> sigv

val rsa_sha1_verify : rsa_pkey -> FStar_Bytes.bytes -> sigv -> Prims.bool