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

Authors

J

Jasmin authors and contributors

Maintainers

J

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

Sources

jasmin-compiler-v2026.03.1.tar.bz2

sha256=78e9f92963403f1ed9f95326f26725532c43956f10fcc47d11ac94c66a236f52

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

Module `Jasmin.Syscall`

val syscall_t_tag : 
  (Wsize.wsize * BinNums.positive) 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.positive;

}

type syscall_t_fields_t = box_syscall_t_RandomBytes

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

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

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

val syscall_t_eqb_OK : 
  (Wsize.wsize * BinNums.positive) Syscall_t.syscall_t ->
  (Wsize.wsize * BinNums.positive) Syscall_t.syscall_t ->
  Bool.reflect

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

}

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

val syscall_sig_s : 
  Wsize.coq_PointerData ->
  (Wsize.wsize * BinNums.positive) 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