package jasmin

You can search for identifiers within the package.

in-package search v0.2.0

Compiler for High-Assurance and High-Speed Cryptography

Install

dune-project

Dependency

github.com Readme Edit opam file Versions (19)

Authors

J

Jasmin authors and contributors

Maintainers

J

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

Sources

jasmin-compiler-v2025.06.3.tar.bz2

sha256=e7aafd891eb54e89d41d9d7d1bbda9ddb1cddc5fdf0359d88c2b7b417ae4a39b

doc/jasmin.jasmin/Jasmin/Syscall/index.html

Module `Jasmin.Syscall`

val syscall_t_tag : BinNums.positive Syscall_t.syscall_t -> BinNums.positive

type box_syscall_t_RandomBytes = BinNums.positive

type syscall_t_fields_t = box_syscall_t_RandomBytes

val syscall_t_fields : 
  BinNums.positive Syscall_t.syscall_t ->
  syscall_t_fields_t

val syscall_t_eqb_fields : 
  (BinNums.positive Syscall_t.syscall_t ->
    BinNums.positive Syscall_t.syscall_t ->
    bool) ->
  BinNums.positive ->
  box_syscall_t_RandomBytes ->
  box_syscall_t_RandomBytes ->
  bool

val syscall_t_eqb : 
  BinNums.positive Syscall_t.syscall_t ->
  BinNums.positive Syscall_t.syscall_t ->
  bool

val syscall_t_eqb_OK : 
  BinNums.positive Syscall_t.syscall_t ->
  BinNums.positive Syscall_t.syscall_t ->
  Bool.reflect

val coq_HB_unnamed_factory_1 : 
  BinNums.positive Syscall_t.syscall_t Eqtype.Coq_hasDecEq.axioms_

val syscall_syscall_t__canonical__eqtype_Equality : Eqtype.Equality.coq_type

type syscall_sig_t = {

scs_tin : Type.stype list;
scs_tout : Type.stype list;

}

val syscall_sig_u : BinNums.positive Syscall_t.syscall_t -> syscall_sig_t

val syscall_sig_s : 
  Wsize.coq_PointerData ->
  BinNums.positive Syscall_t.syscall_t ->
  syscall_sig_t

type 'syscall_state syscall_sem =
  'syscall_state ->
  BinNums.coq_Z ->
  'syscall_state * Ssralg.GRing.ComRing.sort list

type 'syscall_state syscall_state_t = 'syscall_state