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 (23)

Authors

J

Jasmin authors and contributors

Maintainers

J

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

Sources

jasmin-compiler-v2026.09.0.tar.bz2

sha256=11fec571efb9f7b3a47fea324b4e2a68289e0b73b2248d237eccf139b5218190

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

Module `Jasmin.Syscall`

val syscall_t_tag : 
  (Wsize.wsize * BinNums.coq_Z) Syscall_t.syscall_t ->
  BinNums.positive

type box_syscall_t_RandomBytes = {

coq_Box_syscall_t_RandomBytes_0 : Wsize.wsize;
coq_Box_syscall_t_RandomBytes_1 : BinNums.coq_Z;

}

type syscall_t_fields_t = box_syscall_t_RandomBytes

val syscall_t_fields : 
  (Wsize.wsize * BinNums.coq_Z) Syscall_t.syscall_t ->
  syscall_t_fields_t

val syscall_t_eqb_fields : 
  ((Wsize.wsize * BinNums.coq_Z) Syscall_t.syscall_t ->
    (Wsize.wsize * BinNums.coq_Z) Syscall_t.syscall_t ->
    bool) ->
  BinNums.positive ->
  box_syscall_t_RandomBytes ->
  box_syscall_t_RandomBytes ->
  bool

val syscall_t_eqb : 
  (Wsize.wsize * BinNums.coq_Z) Syscall_t.syscall_t ->
  (Wsize.wsize * BinNums.coq_Z) Syscall_t.syscall_t ->
  bool

val syscall_t_eqb_OK : 
  (Wsize.wsize * BinNums.coq_Z) Syscall_t.syscall_t ->
  (Wsize.wsize * BinNums.coq_Z) Syscall_t.syscall_t ->
  Datatypes.reflect

val coq_HB_unnamed_factory_1 : 
  (Wsize.wsize * BinNums.coq_Z) 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.atype list;
scs_tout : Type.atype list;

}

val syscall_sig_u : 
  (Wsize.wsize * BinNums.coq_Z) Syscall_t.syscall_t ->
  syscall_sig_t

val syscall_sig_s : 
  Wsize.coq_PointerData ->
  (Wsize.wsize * BinNums.coq_Z) Syscall_t.syscall_t ->
  syscall_sig_t

type 'syscall_state syscall_sem =
  'syscall_state ->
  BinNums.coq_Z ->
  'syscall_state * Word0.word list

type 'syscall_state syscall_state_t = 'syscall_state