Syscall (p.jasmin.2026.03.0.doc.jasmin.jasmin.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