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