From 00eb69b4754a48c65bb8374641e5a4a18f14376d Mon Sep 17 00:00:00 2001 From: rossberg Date: Tue, 24 Oct 2017 13:19:19 +0200 Subject: [PATCH] [spec] Add size_{table,mem} to embedder interface --- document/core/appendix/embedding.rst | 36 ++++++++++++++++++++++++++++ 1 file changed, 36 insertions(+) diff --git a/document/core/appendix/embedding.rst b/document/core/appendix/embedding.rst index 44f89c8737..2625178809 100644 --- a/document/core/appendix/embedding.rst +++ b/document/core/appendix/embedding.rst @@ -370,6 +370,24 @@ Tables \end{array} +.. _embed-size-table: + +:math:`\F{size\_table}(\store, \tableaddr) : \i32` +.................................................. + +1. Assert: :math:`\store.\STABLES[\tableaddr]` exists. + +2. Return the length of :math:`\store.\STABLES[\tableaddr].\TIELEM`. + +.. math:: + ~ \\ + \begin{array}{lclll} + \F{size\_table}(S, a) &=& n && + (\iff |S.\STABLES[a].\TIELEM| = n) \\ + \end{array} + + + .. _embed-grow-table: :math:`\F{grow\_table}(\store, \tableaddr, n) : \store ~|~ \error` @@ -478,6 +496,24 @@ Memories \end{array} +.. _embed-size-mem: + +:math:`\F{size\_mem}(\store, \memaddr) : \i32` +.............................................. + +1. Assert: :math:`\store.\SMEMS[\memaddr]` exists. + +2. Return the length of :math:`\store.\SMEMS[\memaddr].\MIDATA` divided by the :ref:`page size `. + +.. math:: + ~ \\ + \begin{array}{lclll} + \F{size\_mem}(S, a) &=& n && + (\iff |S.\SMEMS[a].\MIDATA| = n \cdot 64\,\F{Ki}) \\ + \end{array} + + + .. _embed-grow-mem: :math:`\F{grow\_mem}(\store, \memaddr, n) : \store ~|~ \error`