package jasmin

  1. Overview
  2. Docs
Compiler for High-Assurance and High-Speed Cryptography

Install 

dune-project
 Dependency

github.com Readme Edit opam file Versions (17)

Authors

  1. J
    Jasmin authors and contributors

Maintainers

  1. J
    Jean-Christophe Léchenet <jean-christophe.lechenet@inria.fr>

Sources

jasmin-compiler-v2025.06.1.tar.bz2
sha256=e92b42fa69da7c730b0c26dacf842a72b4febcaf4f2157a1dc18b3cce1f859fa

doc/jasmin.jasmin/Jasmin/Ct_checker_forward/index.html

Module Jasmin.Ct_checker_forwardSource

Sourceval is_ct_op1 : Expr.sop1 -> bool
Sourceval is_ct_op2 : Expr.sop2 -> bool
Sourceval is_ct_opN : Expr.opN -> bool
Sourceval is_ct_sopn : ('asm -> bool) -> 'asm Sopn.sopn -> bool
Sourcetype signature

Security type of a function

Sourceval pp_signature : (_, _) Prog.prog -> Format.formatter -> (Prog.funname * signature) -> unit

Human-readable form of a signature

Sourceval ty_prog : ('asm -> bool) -> infer:bool -> (_, 'asm) Prog.prog -> Jasmin.Prog.Name.t list -> (Prog.funname * signature) list * (Jasmin.Prog.L.t * (Format.formatter -> unit)) option

Type-check (for constant-time) a list of functions in the given program (defaults to all functions if the list is empty).

Returns the signature of all functions that have been successfully type-checked and an optional error message in case of failure (type-checking aborts after the first error).

When infer is false, checking of export functions fails unless they are correctly annotated.