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

Authors

J

Jasmin authors and contributors

Maintainers

J

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

Sources

jasmin-compiler-v2025.06.1.tar.bz2

sha256=e92b42fa69da7c730b0c26dacf842a72b4febcaf4f2157a1dc18b3cce1f859fa

doc/jasmin.jasmin/Jasmin/Memory_model/index.html

Module `Jasmin.Memory_model`

type __ = Obj.t

module LE : sig ... end

type pointer_op = {

add : Eqtype.Equality.sort -> BinNums.coq_Z -> Eqtype.Equality.sort;
sub : Eqtype.Equality.sort -> Eqtype.Equality.sort -> BinNums.coq_Z;
p_to_z : Eqtype.Equality.sort -> BinNums.coq_Z;

}

val is_align : 
  Eqtype.Equality.coq_type ->
  pointer_op ->
  Eqtype.Equality.sort ->
  Wsize.wsize ->
  bool

type 'core_mem coreMem = {

get : 'core_mem -> Eqtype.Equality.sort -> Ssralg.GRing.ComRing.sort Utils0.exec;
set : 'core_mem -> Eqtype.Equality.sort -> Ssralg.GRing.ComRing.sort -> 'core_mem Utils0.exec;
valid8 : 'core_mem -> Eqtype.Equality.sort -> bool;
valid8P : 'core_mem -> Eqtype.Equality.sort -> Ssralg.GRing.ComRing.sort -> Bool.reflect;

}

type aligned =

| Unaligned
| Aligned

val aligned_tag : aligned -> BinNums.positive

type box_aligned_Unaligned =

| Box_aligned_Unaligned

type aligned_fields_t = __

val aligned_fields : aligned -> aligned_fields_t

val aligned_eqb_fields : 
  (aligned -> aligned -> bool) ->
  BinNums.positive ->
  aligned_fields_t ->
  aligned_fields_t ->
  bool

val aligned_eqb : aligned -> aligned -> bool

val aligned_eqb_OK : aligned -> aligned -> Bool.reflect

val coq_HB_unnamed_factory_1 : aligned Eqtype.Coq_hasDecEq.axioms_

val memory_model_aligned__canonical__eqtype_Equality : Eqtype.Equality.coq_type

val aligned_le : aligned -> aligned -> bool

module CoreMem : sig ... end

val coq_PointerW : Wsize.coq_PointerData -> pointer_op

val round_ws : Wsize.wsize -> BinNums.coq_Z -> BinNums.coq_Z

type 'mem memory = {

stack_root : 'mem -> Ssralg.GRing.ComRing.sort;
stack_limit : 'mem -> Ssralg.GRing.ComRing.sort;
frames : 'mem -> Ssralg.GRing.ComRing.sort list;
alloc_stack : 'mem -> Wsize.wsize -> BinNums.coq_Z -> BinNums.coq_Z -> BinNums.coq_Z -> 'mem Utils0.exec;
free_stack : 'mem -> 'mem;
init : (Ssralg.GRing.ComRing.sort * BinNums.coq_Z) list -> Ssralg.GRing.ComRing.sort -> 'mem Utils0.exec;

}

module type MemoryT = sig ... end