+
+
+*WARNING: describing convolution this way makes the actual operation done by the operator much more difficult to understand... In fact, this scheme will necessarily be explained with a reference to the classical way to compute convolutions...*
+
+The `Conv` operator also does padding and dilation. Padding can be expressed using the ONNX `Pad` operator. since there is no Dilation operator, we have to describe it using simpler operators.
+
+Dilation can be implemented using `Reshape` and `Concat`. For instance, for a 2D tensor:
+- First, we insert zeroes between columns by
+ - reshaping the tensor to add a dimension. This means that the scalar items of the matrix becomes vectors. The initial shape 2x2 becomes 2x2x1 :
+ ```
+ [
+ [1,2],
+ [3,4]
+ ]
+ ```
+ becomes
+ ```
+ [
+ [ [1],[2]],
+ [ [3],[4]]
+ ]
+ ```
+ - we construct a zero tensor with the same shape 2x2x1:
+ ```
+ [
+ [ [0],[0]],
+ [ [0],[0]]
+ ]
+ ```
+ - Then we concat the two tensors along dimension 2. The resulting tensor is now 2x2x2
+ ```
+ [
+ [[1,0],[2,0]],
+ [[3,0],[4,0]]
+ ]
+ ```
+ - Then we reshape the tensor to 2x4 which is the size of the dilated tensor along the second dimension (columns):
+ ```
+ [
+ [1,0,2,0],
+ [3,0,4,0]
+ ]
+ ```
+ - Second, the same process is applied on the rows.
+
+We could also use `pad` to insert the zeroes. For instance, if we consider the dilation on the column dimension:
+- First, as before, we reshape the tensor from 2x2 to 2x2x1
+- We pad the tensor with zeroes (tensor is now 2x2x2):
+ ```
+ [
+ [[1,0],[2,0]],
+ [[3,0],[4,0]]
+ ]
+ ```
+- and we reshape it to 2x4
+ ```
+ [
+ [1,0,2,0],
+ [3,0,4,0]
+ ]
+ ```
+
+We could also use `Reshape` to flatten the tensor, then use `ScatterElement`to insert zeroes and use `Reshape` again to set final tensor shape.
+
+## MaxPool
+
+ - MaxPool = Slice + ReduceMax + Concat
+
+## LayerNormalization
+ - LayerNormalization = ReduceMean, Sub, Pow, Sqrt, Add, Div, Mul
+
+## GlobalAveragePool
+
+*Defined with respect to AveragePool.*
+
+## AveragePool
+
+`AveragePool` can be defined using a channel-wise convolution. Average pooling consists to apply a kernel which values are all equal to $1/\texttt{kernel size}$.
+
+
+It can also be described using `Slice`, `Reshape` and `ReduceMean`
+
+## HardSwish
+
+Operator `HardSwish` can be defined using the `max` and `min` operators:
+
+$$ hardswish(x) = x * max(0, min(1, \alpha * x + \beta))$$
+
+with $\alpha=1/6$ and $\beta=0.5$.
+
+It could also be expressed using `Relu` or `HardSigmoid`.
+
+## LeakyRelu
+
+The mathematical definition of `LeakyRelu` is
+
+$$ LeakyRelu(x) = \begin{cases}
+ x & \text{if}\ x \ge 0 \\
+ \alpha x & \text{if}\ x \lt 0
+ \end{cases} $$
+
+which can be written as
+
+$$LeakyRelu(x) = max(0,x)+min(0, \alpha x)$$
+
+## SoftMax
+
+Operator `SoftMax` is defined as follows:
+$$\texttt{SoftMax}(x_i) = { e^{x_i} \over {\sum_{j=1}^{K} e^{x_j}}}$$
+
+The numerator can be computed using operator `Exp`. The denominator can be computed using the `ReduceSum` operator that computes the sum of the input tensor’s elements along the provided axes.
+
+In order to ensure numerical stability, the actual formula should be
+
+$$\texttt{SoftMax}(x_i) = { e^{x_i-max(x)} \over {\sum_{j=1}^{K} e^{x_j-max(x)}}}$$
+
+which means that we have to use the `ReduceMax` operator.
+
+The netron representation of the `SoftMax` operator is given below:
+
+
+
+## SoftPlus
+
+Operator `SoftPlus` is defined as follows:
+$$\texttt{SoftPlus}(x) = \ln(e^{x} +1 )$$
+
+*Note that in the ONNX documenation, $\ln$ and $\log$ are used. There is a unique logarithm operator, `Log` that computes the natural (neperian) logarithm, i.e, $\log(x)=\ln(x)=\log_e(x)$.*
+
+This operator can be described using `Log` and `Add`.
+
+## Sigmoid
+
+The mathematical expression for operator `Sigmoid` is :
+
+$$ sigmoid(x)= { 1 \over 1+e^{-x} } $$
+
+This operator can be described using `Div`, `Exp` and `Add`.
+
+## Tanh
+
+The mathematical expression for operator `Tanh` is :
+
+$$ tanh(x)= { e^x-e^{-x} \over e^x+e^{-x} } $$
+or
+$$ tanh(x)= { 1-e^{-2x} \over 1+e^{-2x} } $$
+
+
+This operator can be described using `Div`, `Exp`, `Add`, `Sub`, `Mul`
+
+## Transpose
+
+Transpose could be expressed using
+- `Reshape` (or `Flatten`), to flatten the tensor,
+- a computation of the new indices
+- `Gather` to collect the elements of the flattened tensor
+- `Reshape` to set back the dimension of the tensor
+
+## Flatten
+
+Operator `Flatten` flattens a tensor starting from a given axis. If input tensor has shape $(d_0, d_1, … d_n)$ then the output will have shape $(d_0 \times d_1 \times ... \times d_{{axis}-1}, d_{axis} \times d_{{axis}+1} \times ... \times d_n)$.
+
+This operator can be represented using:
+- `Shape` to get the shape of the tensor
+- `Slice`, `ReduceProd`, and `Concat` to compute the flattened dimensions
+- `Reshape`
+
+The following picture gives an example of such transformation applied to a 2D input tensor (but it can be generalized).
+
+Values `dim0` and `dim1` correspond to the previous products:
+- ${dim_0} = d_0 \times d_1 \times ... \times d_{{axis}-1}$
+- ${dim_1} = d_{axis} \times d_{{axis}+1} \times ... \times d_n$
+
+
+
+
+Operator `Slice` uses the starts, ends, axes and steps inputs to select a sub-tensor of its input data tensor. (see the ONNX and numpy documenration: it is a pretty complicated operator...)
+
+## Gemm
+
+Operator `Gemm` is defined as follows:
+$$\texttt{Gemm}(A,B,C) = \alpha \times A' \times B’ + \beta \times C$$
+
+where $A'$ and $B'$ are the transposed version of $A$ and $B$ depending on attributes `transA` and `transB`.
+
+This operator can be described using operators `Transpose`, `MatMul`, `Add`, `Mul`.
+
+The booleans that control the transposition of $A$ and $B$ are attributes, not input tensors. Therefore, the description of the operator should probably (?) use a textual condition, (i.e., "if transA is true then...") rather than other operators. (To be discussed).
+
+
diff --git a/safety-related-profile/attic/operator_spec_sub_wg/core_ops/flatten_netron.png b/safety-related-profile/attic/operator_spec_sub_wg/core_ops/flatten_netron.png
new file mode 100644
index 00000000..d26673cc
Binary files /dev/null and b/safety-related-profile/attic/operator_spec_sub_wg/core_ops/flatten_netron.png differ
diff --git a/safety-related-profile/attic/operator_spec_sub_wg/core_ops/softmax_netron.png b/safety-related-profile/attic/operator_spec_sub_wg/core_ops/softmax_netron.png
new file mode 100644
index 00000000..07653a59
Binary files /dev/null and b/safety-related-profile/attic/operator_spec_sub_wg/core_ops/softmax_netron.png differ
diff --git a/safety-related-profile/attic/operator_spec_sub_wg/dumitru-2025-07-21.md b/safety-related-profile/attic/operator_spec_sub_wg/dumitru-2025-07-21.md
new file mode 100644
index 00000000..4fb89111
--- /dev/null
+++ b/safety-related-profile/attic/operator_spec_sub_wg/dumitru-2025-07-21.md
@@ -0,0 +1,54 @@
+**Dumitru's proposal concerning broadcasting**
+
+ONNX has pretty complex broadcasting rules, described
+here:
+ https://onnx.ai/onnx/repo-docs/Broadcasting.html
+They claim they follow Numpy's rules on most operators,
+as defined here:
+
+ https://numpy.org/doc/stable/user/basics.broadcasting.html#general-broadcasting-rules
+
+and a different rule on Gemm and on Prelu.
+
+But both rules are pretty complex.
+
+> (Eric) They are not *** that *** complex but, for sure, adding broadcasting will make our life more complicated.
+>> (Dumitru) It's arguably more complex than the operators that use it, like "add".
+
+Thus, it draws attention away from the core functionality of the operator to the broadcasting.
+
+The question is: how to define the *semantics* of operators that perform broadcast? Add the (explicit) description of broadcasting to all operators performing it, or defined the operator semantics separately, and the broadcast separately?
+
+One first remark here is that actually decomposing inside ONNX for implementation purposes does not seem to be possible, as no explicit broadcast operator exists. This is unlike in numpy, where functions exist both for the broadcast of a tensor to a shape:
+
+ https://numpy.org/doc/stable/reference/generated/numpy.broadcast_to.html#numpy.broadcast_to
+
+and for computing the broadcast shape.
+
+ https://numpy.org/doc/stable/reference/generated/numpy.broadcast_shapes.html#numpy.broadcast_shapes
+
+However, for semantics definition purposes, my suggestion would be to decompose by introducing a "virtual" broadcast operator (e.g. why3 functions corresponding to numpy.broadcast_to, numpy.broadcast_shapes) and then defining the full semantics of the operator by composing this with a simple definition of the base operator.
+
+> (eric) As you write above, the other solution is to specify the operation including the broadcasting, as it will >be actually done in the implementation. This will make the mathematical formulation and the formal spec significantly more complicated because we will have to play with mods whenever we compute an index.
+
+>> (Dumitru) Exactly.
+
+Something like:
+```
+x = onnx.add(y,z)
+```
+would become:
+```
+ x_shape = broadcast_shapes(shape(y),shape(z))
+ y_full = broadcast_to(y,x_shape)
+ z_full = broadcast_to(z,x_shape)
+ x = add_homogenous(y_full,z_full)
+```
+
+> (Eric) I fully agree with the approach.
+> We may possibly add a predicate "need broadcasting" so that we can clearly express in which condition broadcasting is nedeed and possible. This will anyway be necessary to express the usage constraints.
+So, I propose that we keep the capability of broadcasting (for the moment we can keep our spec as is and we will add broadcasting in a second phase).
+
+> (Eric) Note that concerning `x_shape = broadcast_shapes(shape(y),shape(z))`, this raises another question : we have also forbidden shape inference. Normally, the shape of x should be known in advance...
+
+>> (Dumitru) Oh, then it's even easier, requiring in the operation properties that the constant x_shape provided by the programmer satisfies "x_shape = broadcast_shapes(shape(y),shape(z))"
diff --git a/safety-related-profile/attic/operator_spec_sub_wg/error_conditions.md b/safety-related-profile/attic/operator_spec_sub_wg/error_conditions.md
new file mode 100644
index 00000000..4ca15554
--- /dev/null
+++ b/safety-related-profile/attic/operator_spec_sub_wg/error_conditions.md
@@ -0,0 +1,140 @@
+# Introduction
+
+This document is a followup to our July 2nd discussion about the way to specify the behaviour of operators in the presence of errors conditions.
+
+# The issue
+Some operator are not defined for some input values. Typical examples are division by zero, overflows, etc.
+
+For simple operators, those conditions can be specified in the definition of the input domain. For instance `y = Div (a , b)` is not defined for $b=0$, and the domain of the inputs in $\mathbb R$ or $\mathbb Z$ is $\mathbb R\times \mathbb R^*$ or $\mathbb Z\times \mathbb Z^*$, respectively.
+
+For complex operators, the correct domain (where the function is defined) can't be defined easily due to the complexity of the relation between the error condition (e.g., some denominator equal to 0 or some overflow) and the inputs.
+
+**How can we address this in our informal specification?**
+
+For instance, let's take the `Add` operator whose signature is:
+
+`y : int32 = Add(a: int32, b: int32)`
+
+It can be specified as
+
+$y = a+b$ where operator $+$ is the usual mathematical addition defined in $\mathbb R$, $\mathbb Z$, etc.
+
+Several options for the specification can be proposed...
+
+# The options
+
+#### Option 0
+**Don't say anything...**
+
+The operator `Add` is simply specified as
+$$y = a + b $$
+
+Problem: this specification is incorrect since, as soon as $a+b > 2^{32}$, the value $a+b$ does not belong to the set of integers `INT32`
+.
+
+The user may hopefully be in the case where the condition $a+b\leq 2^{32}$ holds, but the specification remains incorrect or inconsistent (i.e., the "user" of the operator cannot expect condition $y=a+b$ to be satisfied for all values in the domain).
+
+#### Option 1
+**Specify the exact conditions (the domain) for which the specification is applicable.**
+
+Here, the condition is $a+b \leq 2^{32}-1$ (for the right bound of the domain) where, again, operator "$+$" is the usual addition.
+
+The specification becomes
+$$y = a + b $$
+for any $a$ and $b$ in $\mathbb Z \times \mathbb Z$ such that
+$-2^{32} \leq a+b \leq 2^{32}-1$
+
+This solution makes sense but it is not really practical since to check the condition *in practice*, we have to compute the result in $\mathbb Z$)...
+
+In practice, we would be happier with some condition - possibly more conservative - easier to check.
+
+For instance, for a simple addition, this could be : $-2^{31}+1\leq a \leq 2^{31}-1$ and $-2^{31}+1 \leq b \leq 2^{31}-1$ .
+
+However, this approach is not easy to implement for more complex operators. It **may** work for instance if we know that the input values are in a certain range (e.g., because they have been normalized) so that not overflow can occur.
+
+#### Option 2
+**Specify the operator in the set `INT32`, i.e., using signed, two's complement arithmetic.**
+
+Expressed using the usual $+$ operator, the specification becomes
+$$
+y =
+\begin{cases}
+(a + b) \bmod 2^n & \text{if } (a + b) \bmod 2^n < 2^{n-1} \\
+(a + b) \bmod 2^n - 2^n & \text{otherwise}
+\end{cases}
+$$
+
+Advantage: the operation is fully and precisely defined in `INT32`. It matches exactly what happens in an implementation where our `INT32` isa 32 bit machine value.
+
+Problem: This approach could be applied to simple operators but for more complex operator such as, for instance, a matrix multiplication, all intermediate operations used to describe the matrix multiplication would actually refer to operation in `INT32`. The usual $+$ will be replaced by $(+)$, etc. This approach is cumbersome and does not really express what we expect. In practice, we would probably prefer all intermediate "computations" to be carried out in $\mathbb Z$ and the final result to be mapped to `INT32` (to be compared with the case where all intermediate operations are carried out in $\mathbb Z$).
+
+Another solution would be to do all computations using standard arithmetic in $\mathbb Z$ (i.e., use $+$ in the usual addition in $Z$) and require that no "intermediate value" ever gets out of the `INT32`domain.
+
+In that case, it'll be the responsibility of the implementer or the user to ensure that all these "intermediate values" remain in the appropriate domain:
+- The implementer could perform actual (2's arithmetic) intermediate computations in a larger domain (tahn `INT32`) in order to prevent overflows
+- The user could perform some verification (by testing, formal verification, etc.) to ensure that all intermediate values actual remain in the `INT32` domain.
+
+Note that the concept of "intermediate values" is strange in a specification. In a specification, when we write $y=a+b+c+d$, we do not say anything about the order in which the operations shall be actually performed (thanks to commutativity and associativity). We just express that the result $y$ must be equal to $a+b+c+d$ which, for the usual operator $+$ and values in $\mathbb Z$, can be done in any possible way ($a+(b+c+d))$, $((a+b)+(c+d)$), etc.
+
+### Option 3
+**Specify that the semantics is the one defined using the usual $+$ operator considering that no overflow shall occur (some would write "no runtime error occurs").**
+
+Such specification is a bit of a chicken-egg problem in the sense that saying the "no overflow shall occur" is not a complete specification: what are those "overflows"? what is the actual conditions to be checked?
+
+Stated differently, the specification is something abstract and we don't really know "when" those "overflow" may occur.
+
+If we were to be more explicit, we could (for instance) require that, in the case of operation $y=a+b+c+d$ :
+- $a+b$ is in the domain of `INT32`
+- $b+c$ is in the domain of `INT32`
+- $c+d$ is in the domain of `INT32`
+- $a+c$ is in the domain of `INT32`
+- etc.
+
+because we simply don't know in which order the operations will be carried out.
+
+### Option 4
+**Simply state that "some error condition may occur" (e.g., an overflow).
+**
+
+This is strange to write such a thing in a specification... because (i) it is unclear and (ii) brings no useful information (besides the one of being "careful").
+
+### Option 5
+**Chose the most accurate option among the previous ones that can be implemented in practice for a given operator.**
+
+In the example of an operator that can lead to a division by zero, we would either say that "some division by zero could occur" (option 4) or "division by zero will occur for such or such input value" (option 1).
+
+# An illustration
+
+Let's consider the `MatMulInteger` operator.
+This operator computes a matrix multiplication with input tensors in `int8` and output tensor in `int32`.
+
+This operator does not overflow "most of the time" thanks to the width of the accumulator. However, it **can** overflow if the **sizes** of the input tensors are sufficiently large.
+
+Consider the multiplication of two tensors `A` and `B` of shape `[1,N]` and `[N,1]`. The smallest $N$ for which overflow can occur is such that
+$$
+127 \times 127 \times N > 2^{31} - 1
+$$
+
+this gives
+$$
+N > \frac{2^{32}-1}{127^2} \approx 133141.5
+$$
+
+Since N is integer, the minimal value for an error to trigger is
+$$
+N = 133142
+$$
+
+Strangely (?), overflow occurs for $N=133145$.
+
+As shown below, both python reference implementation and ORT give the same (incorrect) result:
+
+```
+ONNX python reference Output: [-2147471591]
+ONNX Runtime Output (int32): -2147471591
+Expected value: 2147495705
+```
+
+The specification of `MatMulInteger` could state a condition on the shapes of `A` and `B` to prevent overflows. The condition only concerns the dimension of accumulation: if the dimension is smaller than 133145, no overflow can occur.
+
+As stated above, we may also specify the multiplication using 2's complement arithmetic. This specification would give the exact (but unexpected) result.
\ No newline at end of file
diff --git a/safety-related-profile/meetings/operator_spec_sub_wg/worksharing.md b/safety-related-profile/attic/operator_spec_sub_wg/worksharing.md
similarity index 56%
rename from safety-related-profile/meetings/operator_spec_sub_wg/worksharing.md
rename to safety-related-profile/attic/operator_spec_sub_wg/worksharing.md
index 8c85bbae..225c3f65 100644
--- a/safety-related-profile/meetings/operator_spec_sub_wg/worksharing.md
+++ b/safety-related-profile/attic/operator_spec_sub_wg/worksharing.md
@@ -1,4 +1,18 @@
-|Bigram | Actual name |
+This document gives
+- the list of operators to be covered by the SONNX working group
+- the list of people involved in the **writing** and **review** processes
+- the status of each operator
+
+If you want to contribute, please:
+- add your name + initials in the "list of contributors"
+- add your initial in the list of "writers" and/or "local reviewers".
+
+*Thanks!*
+
+
+### List of contributors
+
+|Initials | Actual name |
|------|-------------|
| ej | Eric |
| mt | Mariem |
@@ -7,20 +21,38 @@
| tb | Thiziri |
| hb | Henri |
| nv | Nicolas |
+| sml| Salomé |
+| js | Jean |
+
+### Definition of statuses
+
+|Status | Meaning|
+|-------|--------|
+| DR | Draft |
+| RLR-i | Ready for local (*) review #i |
+| RGR-i | Ready for general (**) review #i |
+| RER-i | Ready for external review #i |
+| FI | Finalized |
+
+- (*) A "local" review involves a limited set of people.
+- (**) A "general review" involves the complete working group.
+- (***) An "external" review involves people outside of the working group.
+
+### Status of operators
-| Operator | Writers | Reviewers |
-|------------------------------|--------------------|-------------------|
-| Abs | | |
-| Add |hb?, |hb |
+| Operator | Writers | Local reviewers | Status (WR, RW, FI)
+|------------------------------|--------------------|-------------------|-------------------
+| Abs |hb, | | DR
+| Add |hb | sml | DR
| Cast | | |
| Clip | | |
-| Concat | | |
-| Constant | |hb |
+| Concat |sml | | RGR-1
+| Constant |hb, | | DR
| ConstantOfShape | | |
-| Conv |ej,mt |jlf,sb,tb,hb |
+| Conv |ej,mt |jlf,sb,tb,hb | RGR-1
| ConvTranspose | | |
| Dense | | |
-| Div |hb?, |hb |
+| Div |hb, | | DR
| Equal | | |
| Erf | | |
| Exp | | |
@@ -28,46 +60,45 @@
| Flatten | | |
| FullyConnected | | |
| Gather | | |
-| Gemm |nv | |
+| Gemm |nv | | DR
| GlobalAveragePool | | |
| GRU | | |
| HardSwish | | |
| Identity | | |
| LeakyRelu | | |
-| Less |hb?, |hb |
-| Log | | |
-| LSTM | | |
-| MatMul |nv | |
-| Max | | |
-| MaxPool | | |
+| Less |hb, | | DR
+| Log |hb, | | DR
+| LSTM |nv | | DR
+| MatMul |nv | | DR
+| Max |jlf | |
+| MaxPool |sml, js | |
| Min | | |
| Mod | | |
-| Mul |hb?, |hb |
-| Neg | | |
+| Mul |hb, | | DR
+| Neg |hb, | | DR
| Not | | |
| Pad | | |
-| Padding | | |
-| Pow | | |
+| Pow |hb, | | DR
| Range | | |
| ReduceMean | | |
| ReduceSum | | |
-| Relu | | |
+| Relu |sml, js | |
| Reshape | | |
-| Resize | | |
+| Resize |sml | |
| ScatterND | | |
| Shape | | |
-| Sigmoid | | |
+| Sigmoid | | | DR
| Slice | | |
| Softmax | | |
| SoftPlus | | |
| Split | | |
-| Sqrt | | |
+| Sqrt |hb, | | WR
| Squeeze | | |
-| Sub |hb?, |hb |
-| Tanh | | |
+| Sub |hb, | | WR
+| Tanh | | | WR
| Transpose | | |
| ConvTransposeDeconvolution | | |
| Unsqueeze | | |
-| Where |hb?, |hb |
+| Where |hb, | | WR
diff --git a/safety-related-profile/attic/profile_ir/IR.md b/safety-related-profile/attic/profile_ir/IR.md
new file mode 100644
index 00000000..4b9979bf
--- /dev/null
+++ b/safety-related-profile/attic/profile_ir/IR.md
@@ -0,0 +1,549 @@
+
+
+# Open Neural Network Exchange Intermediate Representation (ONNX IR) Specification
+
+__Purpose__
+
+This document contains the normative specification of the semantics of ONNX.
+
+The `.proto` and `.proto3` files found under the [onnx folder](/onnx/) form the normative specification of its syntax authored in the [Protocol Buffers](https://developers.google.com/protocol-buffers) definition language. Commentary found in the `.proto` and `.proto3` files are intended to improve readability of those files, but are not normative if they conflict with this document. Such conflicts should be reported as documentation bugs.
+
+__Notes on model validation__
+
+A [tool](../onnx/checker.py) is available to perform general validation of models against this specification. It is implemented in C++ with a Python command-line wrapper.
+
+__Notes on language in this and all related documents__:
+
+1. The use of SHOULD, MUST, MAY and so on in this document is consistent with [RFC 2119](https://www.ietf.org/rfc/rfc2119.txt).
+
+2. The use of 'list' shall denote an ordered collection of items, 'set' shall denote an unordered collection of unique elements, and 'bag' an unordered collection of possibly non-unique elements.
+
+## Components
+
+ONNX is an open specification that consists of the following components:
+
+1) A definition of an extensible computation graph model.
+
+2) Definitions of standard data types.
+
+3) Definitions of built-in operators.
+
+#1 and #2 together make up the ONNX Intermediate Representation, or 'IR', specification which is covered herein; the built-in operators are covered in documents listed at the end. Specifically, built-in operators are divided into a set of primitive operators and functions. A function is an operator whose semantics is formally expressed via expansion into a sub-graph (called the function body) using other operators (and functions). Functionality-wise, an ONNX compatible framework or runtime may inline a function body to execute it if it does not have corresponding implementation of the function.
+
+There are two official ONNX variants; the main distinction between the two is found in the default operator sets. __ONNX-ML__ extends the __ONNX__ operator set with ML algorithms that are not based on neural networks.
+
+Up to IR version 6, the ONNX specification and model format addressed only inference (also known as scoring). Starting from IR version 7, the ONNX specification and model format also support training. An ONNX training model is an extension of the inference-model. An inference-only runtime can consume a training model ignoring the training-related extensions. However, an inference-only model may enable a representation that is more optimal for inference purposes than a training model.
+
+## Runtime Agnostic
+
+ONNX does not pre-suppose or imply any particular method of runtime implementation.
+
+For example, an implementation may consist of a rich runtime which interprets the model; it may be a code generator that translates the model in its entirety to executable code for some target programming language; it may be a hardware implementation; it may be a combination of two or three of those.
+
+Nothing in this specification should be construed as advocating one implementation approach over any other; any comments on the inner workings of concrete implementations are to be interpreted as examples.
+
+## ONNX Versioning
+
+The IR specification, individual models, and operator sets are all versioned. Furthermore, each individual operator indicates which version of its containing operator set it was introduced or stabilized in.
+
+Version numbers can be used as a simple number, or used to encode [semantic versions](https://semver.org/)(AKA SemVer). If using semantic versions, the convention is to use the two most significant bytes for the major number, the next two bytes for the minor number, and the least significant four bytes for the patch/build/bugfix number. When using semantic versioning, at least one of the major/minor numbers MUST be non-zero.
+
+The IR specification uses simple monotonically increasing numbers for its versions. The valid IR versions are defined by the `onnx.Version` enumeration in [onnx.proto](/onnx/onnx.proto).
+
+Operator sets use a simple version number. Each operator set version represents a snapshot of the set of operators, and their semantics at a particular point in time.
+
+This specification does not provide guidance on what versioning scheme model producers should be using.
+
+More details on conventions and best practices for versioning of IR, operator sets, and models can be found in [Versioning](Versioning.md).
+
+## Extensible computation graph model
+
+ONNX specifies the portable, serialized format of a computation graph. It does not have to be the form a framework chooses to use internally. For example, an implementation may represent the model differently in memory if it is more efficient to manipulate during optimization passes.
+
+An implementation MAY extend ONNX by adding operators expressing semantics beyond the standard set of operators that all implementations MUST support. The mechanism for this is adding operator sets to the `opset_import` property in a model that depends on the extension operators.
+
+### Models
+
+The top-level ONNX construct is a ‘Model.’, and is represented in protocol buffers as the type `onnx.ModelProto`
+
+The main purpose of the model structure is to associate metadata with a graph which contains all the executable elements. The metadata is used when first reading the model file, giving an implementation the information it needs in order to determine whether it will be able to execute the model, generate logging messages, error reports, etc. Further, the metadata is useful to tools, such as IDEs and model galleries, which need it for informing humans about a given model’s purpose and characteristics.
+
+Each model has the following components:
+
+|Name|Type|Description|
+|---|---|---|
+|ir_version|int64|The ONNX version assumed by the model.|
+|opset_import|OperatorSetId|A collection of operator set identifiers made available to the model. An implementation must support all operators in the set or reject the model.|
+|producer_name|string|The name of the tool used to generate the model.|
+|producer_version|string|The version of the generating tool.|
+|domain|string|A reverse-DNS name to indicate the model namespace or domain, for example, 'org.onnx'|
+|model_version|int64|The version of the model itself, encoded in an integer.|
+|doc_string|string|Human-readable documentation for this model. Markdown is allowed.|
+|graph|Graph|The parameterized graph that is evaluated to execute the model.|
+|metadata_props|map
-
-###### Constraints
-- (C1) Size of `strides`
- - Statement: the number of elements in the `strides` list is equal to 2. `[R5]`
- - Rationale: The SONNX profile only supports 2 spatial axes.
-- (C2) Value domain
- - Statement: `strides` is a list of strictly positive integers.
- - Rationale: Stride values are used in the denominator of expression in [constraint (C3) of X](#shape_consist)
-- (C3) Consistency between the shape of tensors `X`, `W`, `Y` and attributes `pads`, `dilations` and `strides`.
- - Statement: [See constraint (C3) of X](#shape_consist)
-
-##### `auto_pad` : string
-
-The `auto_pad` attribute determines if and how automatic padding is done for the input tensor X.
-
-###### Constraints
-- (C1) Explicit padding
- - Statement: `auto_pad` shall be set to `NOTSET` `[R3]`
- - Rationale: The SONNX profile imposes explicit padding.
-
-##### `pads`: list of int
-
-Attribute `pads` determines the padding at the beginning and end along each spatial axis of the input tensor `X`.
-
-`pads` is a list of the form (`x1_begin`, `x2_begin`,..., `x1_end`, `x2_end`,...), where `xi_begin` is the number of elements (possibly zero) added at the beginning of axis $i$ and `xi_end` is the number of elements added at the end of axis $i$.
-
-The padding value is 0.
-
-The effect of the `pads` attribute is illustrated on the following figure. In this example, `pads`=(1,3,2,2).
-
-
-
-###### Constraints
-- (C1) Value domain
- - Statement: `pads` is a list of positive or null integers.
- - Rationale: A padding value gives a number of elements to be added to some spatial axis. This is positive[^2].
-- (C2) Consistency between the shape of `X` and the length of `pads`
- - Statement: The length of the `pads` list is two times the number of spatial axes of `X`
- - Rationale: Padding shall be given for all spatial axes, and a beggining value and an end value must be given for each axis.
-- (C3) Consistency between the shape of tensors `X`, `W`, `Y` and attributes `pads`, `dilations` and `strides`.
- - Statement: [See constraint (C3) of X](#shape_consist)
-
-##### `dilations`: list of int
-
-Attribute `dilations` specifies the spacing between the kernel elements for each spatial axis of the filter `W`. It is a list of non-null integer values where each value gives the dilation factor for spatial axis $i$. If the dilation factor is greater than 1 for axis $i$, then the kernel points are spaced out by the dilation factor for that axis.
-
-The spacing value is 0.
-
-The effect of the `dilations` attribute for a tensor with two spatial axes is depicted on the following figure. In this example, `dilations`=(2,2).
-
-
-
-
-###### Constraints
-- (C1) Value domain
- - Statement: `dilations` is a list of strictly positive integers
-- (C2) Relation between `dilations` and `W`
- - Statement: The length of the `dilations` list is equal to number of spatial axes of `W`.
- - Rationale: Dilation is defined for all spatial axes of `W`.
-- (C3) Consistency between the shape of tensors `X`, `W`, `Y` and attributes `pads`, `dilations` and `strides`.
- - Statement: [See constraint (C3) of X](#shape_consist)
-
-##### `group`: int
-
-This attribute specifies the number of groups the input channels and output channels are divided into. When `group`=1, a standard convolution is performed.
-When group is greater than 1, convolution is computed for each group separately with a specific set of filters.
-
-The effect of the `group` attribute for a tensor with two spatial axes is depicted on the following figure. In this example `group`=3.
-
-
-
-(Taken from https://eli.thegreenplace.net/2018/depthwise-separable-convolutions-for-machine-learning)
-
-In the example, with `group` set to 3 and an input `X` and an output `Y` with 3 channels, the input and output channels will be divided into 3 groups of 1 channel.
-
-###### Constraints
-- (C1) Support for standard and depthwise convolutions
- - Statement: `group`=1 (standard convolution) or `group`$=c(X)$ (depthwise convolution)
- - Rationale: SONNX only supports standard and depthwise convolutions
-
-##### `kernel_shape`: list of int
-
-This parameter specifies the shape of the convolution kernel `W`.
-
-###### Constraints.
-
-- (C1) Value domain
- - Statement: `kernel_shape` is a list of strictly positive integers
- - Rationale: A dimension is always positive and cannot be null.
-- (C2) Consistency between `W` and `kernel_shape`
- - Statement: [See constraint (C3) of W](#kernel_shape_w)
-
-#### Outputs
-
-##### `Y`
-
-The size of the output `Y` will be $(b(Y) \times c(Y) \times h(Y) \times w(Y))$ where
-- $b(Y)$ is the number of batches
-- $c(Y)$ is the number of channels
-- $h(Y)$ and $w(Y)$ are the sizes of the output for the two spatial axes
-
-###### Constraints.
-- (C1) Consistency between the number of channels of `B` and `Y`
- - Statement: HYPERLIEN VERS W / constraint kernel shape
-- (C2) Consistency between the shape of tensors `X`, `W`, `Y`, attributes `pads` and `strides`,
- - Statement: [see constraint (C3) of X](#shape_consist)
-
-#### Formal specification
-
-The following code specifies the `conv` operator using the Why3 language[^3].
-
-###### Nota: the specification does not cover all attributes values. Currently, there is no padding (`pads` is not set and `auto_pad = NOTSET`) and `dilations` is not set.
-
-``` ocaml
-module Conv
- use int.Int
- use real.RealInfix
- use array.Array
- use int.ComputerDivision
- use real.Truncate
- use real.FromInt
-
- type input_tensor = {
- x: array real;
- x_l: int;
- x_c: int;
- x_b: int;
- x_ch: int;
- }
-
- type convolution_kernel = {
- w: array real;
- w_l: int;
- w_c: int;
- w_ch_in: int;
- w_ch_out: int;
- }
-
- type bias_tensor = {
- b: array real;
- b_c: int;
- }
-
- type attributes = {
- stride: array int;
- pads: array int;
- auto_pad: int;
- dilation: array int;
- }
-
- type output_tensor = {
-
- y_b: int;
- y_ch: int;
- y_l: int;
- y_c: int;
-
- }
-
- function conv_size (out: output_tensor) : int =
- out.y_b * out.y_ch * out.y_l * out.y_c
-
- predicate conv_result
- (inp: input_tensor)
- (kernel: convolution_kernel)
- (bias: bias_tensor)
- (attr: attributes)
- (out: output_tensor)
- (res: array real)
- (bi ci hi wi: int)
- (ci_in ki_h ki_w: int) =
- let y_idx = bi * (out.y_ch * out.y_l * out.y_c) + ci * (out.y_l * out.y_c) + hi * out.y_c + wi in
- let x_l_idx = hi * attr.stride[0] + ki_h * attr.dilation[0] - attr.pads[0] in
- let x_c_idx = wi * attr.stride[1] + ki_w * attr.dilation[1] - attr.pads[1] in
-
- (0 <= x_l_idx < inp.x_l /\ 0 <= x_c_idx < inp.x_c) ->
- let x_idx = bi * (inp.x_ch * inp.x_l * inp.x_c) + ci_in * (inp.x_l * inp.x_c) + x_l_idx * inp.x_c + x_c_idx in
- let w_idx = ci * (kernel.w_ch_in * kernel.w_l * kernel.w_c) + ci_in * (kernel.w_l * kernel.w_c) + ki_h * kernel.w_c + ki_w in
- res.elts (y_idx) = bias.b[ci] +. (inp.x[x_idx] *. kernel.w[w_idx])
-
- val conv (inp: input_tensor)(kernel: convolution_kernel)(bias: bias_tensor)(attr: attributes)(out: output_tensor): array real
- requires{inp.x_ch = out.y_ch = kernel.w_ch_in = bias.b_c}
- requires{out.y_l = (div (inp.x_l + attr.pads[0] + attr.pads[2] - (attr.dilation[0] * kernel.w_l)) attr.stride[0]) + 1}
- requires{out.y_c = (div (inp.x_c + attr.pads[1] + attr.pads[3] - (attr.dilation[1] * kernel.w_c)) attr.stride[1]) +1}
- requires { inp.x_l > 0 /\ inp.x_c > 0 /\ inp.x_ch > 0 /\ inp.x_b > 0}
- requires{kernel.w_l > 0 /\ kernel.w_c > 0 /\ kernel.w_ch_in > 0 /\ kernel.w_ch_out > 0}
- requires { out.y_b > 0 /\ out.y_ch > 0 /\ out.y_l > 0 /\ out.y_c > 0}
- requires { length inp.x = inp.x_l * inp.x_c * inp.x_ch * inp.x_b}
- requires{length kernel.w = kernel.w_l * kernel.w_c * kernel.w_ch_in * kernel.w_ch_out}
- requires{inp.x_l >= kernel.w_l}
- requires{inp.x_c >= kernel.w_c}
- requires{length bias.b = bias.b_c}
- requires{length attr.stride = 2}
- requires{length attr.dilation = 2}
- requires{length attr.pads = 4}
- requires{forall i. 0 <= i < length attr.pads -> attr.pads[i] = 0}
- requires{forall j. 0 <= j < length attr.dilation -> attr.dilation[j] >= 1}
- requires{forall k. 0 <= k < length attr.stride -> attr.stride[k] >= 1}
- ensures { length result = conv_size out }
- ensures { forall bi ci hi wi ci_in ki_h ki_w: int.
- 0 <= bi < out.y_b ->
- 0 <= ci < out.y_ch ->
- 0 <= hi < out.y_l ->
- 0 <= wi < out.y_c ->
- 0 <= ci_in < kernel.w_ch_in ->
- 0 <= ki_h < kernel.w_l ->
- 0 <= ki_w < kernel.w_c -> conv_result inp kernel bias attr out result bi ci hi wi ci_in ki_h ki_w }
-
-end
-
-
-module Test_conv
- use int.Int
- use real.RealInfix
- use array.Array
- use int.ComputerDivision
- use real.Truncate
- use real.FromInt
- use Conv
-
-let test_conv () =
- let inp_x = Array.make 9 1.0 in
- let inp = { x = inp_x; x_l = 3; x_c = 3; x_b = 1; x_ch = 1 } in
-
- let kernel_w = Array.make 4 0.0 in
- let kernel = { w = kernel_w; w_l = 2; w_c = 2; w_ch_in = 1; w_ch_out = 1 } in
-
- let bias_b = Array.make 1 0.5 in
- let bias = { b = bias_b; b_c = 1 } in
- let stride = Array.make 2 1 in (* Stride of 1 *)
- let pads = Array.make 4 0 in (* No padding *)
- let dilation = Array.make 2 1 in (* Dilation of 1 *)
- let attr = { stride = stride; pads = pads; auto_pad = 0; dilation = dilation } in
- let out_h = (div (inp.x_l + pads[0] + pads[2] - (dilation[0] * kernel.w_l)) stride[0]) + 1 in
- let out_w = (div (inp.x_c + pads[1] + pads[3] - (dilation[1] * kernel.w_c)) stride[1]) + 1 in
- let out = { y_b = 1; y_ch = 1; y_l = out_h ; y_c = out_w } in
- (* Call the conv function *)
- let result = conv inp kernel bias attr out in
- let actual_result = result.elts 0 in
- assert { conv_result inp kernel bias attr out result 0 0 0 0 0 0 0} ;
- assert { actual_result = 0.5 } ;
- ()
-
-end
-```
-
-Another formal specification of the `conv` operator using Frama-C
-language[^4] is presented below.
-
-``` objectivec
-#include
-
-Elements of the execution semantics is given on the [IR (Intermediate
-Representation) page](https://onnx.ai/onnx/repo-docs/IR.html) of the
-ONNX web site. In addition, a Python “reference implementation” is also
-provided (see ). The source
-code of this implementation can be found at
-.
-
-Very informally, the semantics is pretty simple: each operator (or
-function) is called according to its position in the topological sorting
-of the operators. The topological order is a partial order that ensures
-that an operator is executed only when its inputs are available. Being a
-partial order, it means that several valid orders exist for a given
-graph. Normally (?) each order should generate the same result, even in
-the presence of floating point operations.
-
-The Python code to execute a graph is given in class
-[`ReferenceEvaluator`](https://github.com/onnx/onnx/blob/main/onnx/reference/reference_evaluator.py)).
-After having processed the inputs and the initializers (i.e., fed the
-`results` dictorionary with these data), the nodes are executed in
-sequence. For each operator, the interpretor checks that its inputs are
-in the `results` dictionary. If they are not, an error is raised (if the
-operators are listed in topological order, this situation should not
-occur). Otherwise, the operator is simply executed (method `run`) with
-or without a context (composed of the current results) depending on the
-type of operators. (Check that this does not create a dependency to the
-total order of operators.)
-
-
-
-### Informal specification
-
-
-
-The semantics of an ONNX model is given in Section "Model Semantics" of
-the [Intermediate
-Representation](https://github.com/onnx/onnx/blob/main/docs/IR.md) page.
-Basically, an inference-model is a stateless function (except possibly
-for some specific nodes such as a random-generation node) represented by
-an acyclic `graph` of nodes. The `graph` is mainly represented by a set
-of inputs and outputs and a topologically sorted list of nodes. Each
-node represents a call to an operator or a function. A `function` is
-itself a graph.
-
-Note that the types of inputs and outputs are not systematically
-required because they can be inferred. In our case, I guess that we will
-forbib shape inference and rely on static tensor shapes (or, at least,
-shape inference can be bone before serializing the model). The proecss
-of shape inference is described in Section [ONNX Shape
-Inference](https://onnx.ai/onnx/repo-docs/ShapeInference.html).
-
-
-
-### Formal specification
-
-*To be completed.*
-
-[^1]: At least in a first phase...
-
-[^2]: Note: in the ONNX runtime implementation, the padding value may be
- negative, which corresponds to reducing the size of the tensor.
-
-[^3]: See [Why3 documentation](https://www(W)hy3.org/)
-
-[^4]: See [Frama-C
- documentation](https://www.frama-c.com/html/documentation.html)
diff --git a/safety-related-profile/documents/issues.md b/safety-related-profile/documents/issues.md
deleted file mode 100644
index 516c7dfd..00000000
--- a/safety-related-profile/documents/issues.md
+++ /dev/null
@@ -1 +0,0 @@
-File moved [here](../deliverables/issues/issues.md).
\ No newline at end of file
diff --git a/safety-related-profile/documents/needs.md b/safety-related-profile/documents/needs.md
deleted file mode 100644
index 08d9779d..00000000
--- a/safety-related-profile/documents/needs.md
+++ /dev/null
@@ -1 +0,0 @@
-File moved [here](../deliverables/needs/needs.md).
\ No newline at end of file
diff --git a/safety-related-profile/documents/profile_formal/README.md b/safety-related-profile/documents/profile_formal/README.md
new file mode 100644
index 00000000..d635b2ce
--- /dev/null
+++ b/safety-related-profile/documents/profile_formal/README.md
@@ -0,0 +1 @@
+This directory contains the formal specification of operators, expressed using the Why3 formal language.
\ No newline at end of file
diff --git a/safety-related-profile/documents/profile_formal/onnxgraph.mlw b/safety-related-profile/documents/profile_formal/onnxgraph.mlw
new file mode 100644
index 00000000..642920dc
--- /dev/null
+++ b/safety-related-profile/documents/profile_formal/onnxgraph.mlw
@@ -0,0 +1,604 @@
+module Graph
+
+
+use int.Int
+use list.List
+use list.Map
+use option.Option
+use map.Map
+use list.Mem
+use list.FoldLeft
+use list.Length
+use list.NthNoOpt
+use map.Const
+use bool.Bool
+
+
+(* A tensor value is just an int [preliminary]*)
+type value = int
+
+(* A tensor is designated by an integer id [preliminary] *)
+(* In the actual implementation, a tensor is designted by a string *)
+(* [TXX] *)
+type tensor = int
+
+(* The state of a graph is a mapping from the set of tensors to a set optional values *)
+(* [TXX] *)
+type graph_state = Map.map tensor (option value)
+
+(* An operator *)
+(* [TODO] The inputs / outputs of an operator are typed. *)
+(* [TODO] The operator may have parameters, e.g., a convolution kernel size *)
+(* [TODO] The operator may have attributes, e.g., a relu activation function *)
+(* [TODO] The operator may have a type, e.g., a convolution, an addition, etc. *)
+(* [TODO] The operator may have a set of attributes, e.g., a relu activation function *)
+
+(* The binding proposed by a node must comply with these typing constraints *)
+type shape = list int (* dimensions of the tensor *)
+
+(* An operator is a function that takes a list of input tensors and produces a list of output tensors *)
+(* [TXX] The operator is defined by its name, its input shapes, and its output shapes *)
+type operator = {
+ name: string; (* name of the operator *)
+ opi: list shape; (* input shapes *)
+ opo: list shape; (* output shapes *)
+}
+
+(* ------------------------------------------------------------------------- *)
+(* [TXX] An operator has at least one output *)
+(* ------------------------------------------------------------------------- *)
+predicate operator_one_output (op: operator) =
+ length op.opo > 0
+
+
+goal operator_one_output_ok :
+ let op : operator = {
+ name="Add" ;
+ opi= Cons (Cons 1 Nil) (Cons (Cons 1 Nil) Nil) ;
+ opo= (Cons (Cons 1 Nil) Nil)
+ } in
+ operator_one_output op
+
+goal operator_one_output_ko :
+ let op : operator = {
+ name="Add" ;
+ opi= Cons (Cons 1 Nil) (Cons (Cons 1 Nil) Nil) ;
+ opo= Nil
+ } in
+ not operator_one_output op
+
+
+(* A node is an application of an operator *)
+(* [TXX] *)
+type node = {
+ ope: operator; (* The operator referred to by the node *)
+ oi: list tensor; (* Input tensors, position-wise *)
+ ou: list tensor; (* Output tensors, position-wise *)
+}
+
+
+(* A graph is a list of tensors and nodes + a list of input and output tensors *)
+(* [TXX] *)
+type graph = {
+ gi: list tensor; (* graph inputs *)
+ go: list tensor; (* graph outputs *)
+ gt: list tensor; (* graph tensors *)
+ gn: list node; (* graph nodes *)
+}
+
+
+(* ------------------------------------------------------------------------- *)
+(* [TXX] In a graph, a node provide all operators inputs and ouputs *)
+(* ------------------------------------------------------------------------- *)
+predicate all_operator_ins_and_outs (g: graph) =
+ forall n: node. mem n g.gn ->
+ length n.oi = length n.ope.opi /\ length n.ou = length n.ope.opo
+
+(* Specification tests *)
+goal all_operator_ins_and_outs_ok :
+ let g : graph = {
+ gi = Cons 1 (Cons 2 Nil);
+ go = Cons 3 (Cons 4 Nil);
+ gt = Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil)));
+ gn = Cons {
+ ope={
+ name="Add" ;
+ opi= Cons (Cons 1 Nil) (Cons (Cons 1 Nil) Nil) ;
+ opo= (Cons (Cons 1 Nil) Nil) };
+ oi=Cons 1 (Cons 2 Nil);
+ ou= (Cons 4 Nil)} Nil;
+ } in
+ all_operator_ins_and_outs g
+
+goal all_operator_ins_and_outs_ko :
+ let g : graph = {
+ gi = Cons 1 (Cons 2 Nil);
+ go = Cons 3 (Cons 4 Nil);
+ gt = Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil)));
+ gn = Cons {
+ ope={
+ name="Add" ;
+ opi= Cons (Cons 1 Nil) (Cons (Cons 1 Nil) Nil) ;
+ opo= (Cons (Cons 1 Nil) Nil) };
+ oi=Cons 1 (Cons 2 Nil);
+ ou= Nil} Nil; (* <= the is no output *)
+ } in
+ not all_operator_ins_and_outs g
+
+
+
+(* ------------------------------------------------------------------------- *)
+(* [TXX] In a graph, a node has at least one output tensor*)
+(* ------------------------------------------------------------------------- *)
+predicate all_node_with_one_output (g: graph) =
+ forall n: node. mem n g.gn -> n.ou <> Nil
+
+(* Specification tests *)
+goal all_node_with_one_output_ok:
+ let g : graph = {
+ gi = Cons 1 (Cons 2 Nil);
+ go = Cons 3 (Cons 4 Nil);
+ gt = Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil)));
+ gn = Cons { ope={ name="Add" ; opi=Nil; opo=Nil }; oi=Cons 1 (Cons 2 Nil); ou=Cons 3 (Cons 4 Nil)}
+ (Cons { ope={ name="Sub" ; opi=Nil; opo=Nil }; oi=Cons 5 (Cons 6 Nil); ou=Cons 7 (Cons 8 Nil)} Nil);
+ } in
+ all_node_with_one_output g
+
+(* Specification tests *)
+goal all_node_with_one_output_ko:
+ let g : graph = {
+ gi = Cons 1 (Cons 2 Nil);
+ go = Cons 3 (Cons 4 Nil);
+ gt = Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil)));
+ gn = Cons { ope={ name="Add" ; opi=Nil; opo=Nil }; oi=Cons 1 (Cons 2 Nil); ou= Nil} (* This operator has no output *)
+ (Cons { ope={ name="Sub" ; opi=Nil; opo=Nil }; oi=Cons 5 (Cons 6 Nil); ou=Cons 7 (Cons 8 Nil)} Nil);
+ } in
+ not all_node_with_one_output g
+
+
+(* ------------------------------------------------------------------------- *)
+(* [TXX] In a graph, a tensor is either an input or the output of at most one node *)
+(* ------------------------------------------------------------------------- *)
+predicate tensor_is_unique_output (g: graph) =
+ forall t: tensor.
+ mem t g.gt ->
+ (mem t g.gi \/
+ (exists n: node.
+ mem n g.gn /\ mem t n.ou /\
+ (forall n': node.
+ (mem n' g.gn /\ mem t n'.ou) -> n = n')))
+
+
+(* Specification tests *)
+goal tensor_is_unique_output_test_ok:
+ let g : graph = {
+ gi = Cons 1 (Cons 2 Nil);
+ go = Cons 3 (Cons 4 Nil);
+ gt = Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil)));
+ gn = Cons { ope={ name="Add" ; opi=Nil; opo=Nil }; oi=Cons 1 (Cons 2 Nil); ou=Cons 3 (Cons 4 Nil)}
+ (Cons { ope={ name="Sub" ; opi=Nil; opo=Nil }; oi=Cons 5 (Cons 6 Nil); ou=Cons 7 (Cons 8 Nil)} Nil);
+ } in
+ tensor_is_unique_output g
+
+(* [TODO] This test and its negation are not valid!! *)
+goal tensor_is_unique_output_test_ko:
+ let g : graph = {
+ gi = Cons 1 (Cons 2 Nil);
+ go = Cons 3 (Cons 4 Nil);
+ gt = Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil)));
+ gn = Cons { ope={ name="Add" ; opi=Nil; opo=Nil }; oi=Cons 1 (Cons 2 Nil); ou=Cons 3 (Cons 4 Nil)}
+ (Cons { ope={ name="Sub" ; opi=Nil; opo=Nil }; oi=Cons 5 (Cons 6 Nil); ou=Cons 7 (Cons 4 Nil)} Nil);
+ } in
+ tensor_is_unique_output g
+
+
+(* ------------------------------------------------------------------------- *)
+(* [TXX] A graph input is the input of at least one node *)
+(* (No useless input) *)
+(* ------------------------------------------------------------------------- *)
+predicate graph_ins_are_node_ins (g: graph) =
+forall t: tensor.
+ mem t g.gi ->
+ exists op. mem op g.gn /\ mem t op.oi
+
+(* Specification tests *)
+goal graph_ins_are_node_ins_test_ok:
+ let g : graph = {
+ gi = Cons 1 (Cons 2 Nil);
+ go = Cons 3 (Cons 4 Nil);
+ gt = Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil)));
+ gn = Cons { ope={ name="Add" ; opi=Nil; opo=Nil }; oi=Cons 1 (Cons 2 Nil); ou=Cons 3 (Cons 4 Nil)} Nil;
+ } in
+ graph_ins_are_node_ins g
+
+goal graph_ins_are_node_ins_test_ko:
+ let g : graph = {
+ gi = Cons 1 (Cons 2 Nil);
+ go = Cons 3 (Cons 4 Nil);
+ gt = Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil)));
+ gn = Cons { ope={ name="Add" ; opi=Nil; opo=Nil }; oi=Cons 5 (Cons 2 Nil); ou= Cons 3 Nil } Nil;
+ } in
+ not graph_ins_are_node_ins g
+
+(* ------------------------------------------------------------------------- *)
+(* [TXX] A graph output is the output of one node *)
+(* ------------------------------------------------------------------------- *)
+predicate graph_outs_are_node_outs (g: graph) =
+ forall t: tensor. mem t g.go ->
+ exists n. mem n g.gn /\ mem t n.ou
+
+(* Specification tests *)
+goal graph_outs_are_node_outs_test_ok:
+ let g : graph = {
+ gi = Cons 1 (Cons 2 Nil);
+ go = Cons 3 (Cons 4 Nil);
+ gt = Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil)));
+ gn = Cons { ope={ name="Add" ; opi=Nil; opo=Nil }; oi=Cons 1 (Cons 2 Nil); ou=Cons 3 (Cons 4 Nil)} Nil;
+ } in
+ graph_outs_are_node_outs g
+
+goal graph_outs_are_node_outs_test_ko:
+ let g : graph = {
+ gi = Cons 1 (Cons 2 Nil);
+ go = Cons 3 (Cons 4 Nil);
+ gt = Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil)));
+ gn = Cons { ope={ name="Add" ; opi=Nil; opo=Nil }; oi=Cons 1 (Cons 2 Nil); ou= Cons 3 Nil } Nil;
+ } in
+ not graph_outs_are_node_outs g
+
+
+(* ------------------------------------------------------------------------- *)
+(* [TXX] Graph inputs and ouputs belong to the set of tensors *)
+(* ------------------------------------------------------------------------- *)
+predicate graph_ins_outs_are_tensors (g: graph) =
+ forall t: tensor. (mem t g.gi \/ mem t g.go) -> mem t g.gt
+
+(* Specification tests *)
+goal graph_ins_outs_are_tensors_test_ok:
+ let g : graph = {
+ gi = Cons 1 (Cons 2 Nil);
+ go = Cons 3 (Cons 4 Nil);
+ gt = Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil)));
+ gn = Cons { ope={ name="Add" ; opi=Nil; opo=Nil }; oi=Cons 1 (Cons 2 Nil); ou=Cons 3 (Cons 4 Nil)} Nil;
+ } in
+ graph_ins_outs_are_tensors g
+
+goal graph_ins_outs_are_tensors_test_ko:
+ let g : graph = {
+ gi = Cons 1 (Cons 2 Nil);
+ go = Cons 3 (Cons 4 Nil); (* <= Output 4 is not in the tensor set *)
+ gt = Cons 1 (Cons 2 (Cons 3 (Cons 5 Nil)));
+ gn = Cons { ope={ name="Add" ; opi=Nil; opo=Nil }; oi=Cons 1 (Cons 2 Nil); ou= Cons 3 Nil } Nil;
+ } in
+ not graph_ins_outs_are_tensors g
+
+
+(* ------------------------------------------------------------------------- *)
+(* [TXX] A tensor is either a graph input or a node output *)
+(* ------------------------------------------------------------------------- *)
+predicate no_free_tensor (g: graph) =
+ forall t: tensor. mem t g.gt ->
+ mem t g.gi \/
+ exists n. mem n g.gn \/ mem t n.ou
+
+
+
+(* =========================================================================== *)
+(* Utilities *)
+(* =========================================================================== *)
+
+(* Create t list of n elements with the same value x *)
+let rec make_list (x: 'a) (n: int) : list 'a
+requires { n >= 0 }
+ensures{ length result = n}
+ensures{ forall v. mem v result -> v = x }
+variant { n }
+=
+ if n = 0
+ then
+ Nil
+ else
+ Cons x (make_list x (n - 1))
+
+(* Fold implementation with one parameters *)
+(*[TODO] Ensures is missing... *)
+let rec fold_left (f: 'acc -> 'a -> 'acc) (acc: 'acc) (l: list 'a) : 'acc
+ variant { l }
+= match l with
+ | Nil -> acc
+ | Cons x xs -> fold_left f (f acc x) xs
+ end
+
+(* Fold implementation with two parameters *)
+(* [TODO] See fold_product in List*)
+let rec fold_left2 (f: 'acc -> 'a -> 'b -> 'acc)
+ (acc: 'acc)
+ (l1: list 'a)
+ (l2: list 'b) : 'acc
+ requires { length l1 = length l2 }
+ variant { l1 }
+ = match l1, l2 with
+ | Nil, Nil -> acc
+ | Cons x xs, Cons y ys -> fold_left2 f (f acc x y) xs ys
+ | _, _ -> absurd
+ end
+
+(* Simple map function *)
+let rec map (f: 'a -> 'b) (l: list 'a) : list 'b
+ensures { length result = length l }
+variant { l }
+= match l with
+ | Nil -> Nil
+ | Cons x xs -> Cons (f x) (map f xs)
+end
+
+
+(* =========================================================================== *)
+(* Simple implementation of a map (using a list) *)
+(* Used to associate a value to a tensor *)
+(* =========================================================================== *)
+
+type fmap = list (tensor, option value)
+
+(* Get an item from the map (spec)*)
+(* Logic functions must be total, so we return None if the tensor is not in the map. *)
+ (* /\ I wuld like to specify this function as if exists k,v . mem (k,v) m then v else None *)
+function fget_logic (m: fmap) (k: tensor) : option value =
+ match m with
+ | Nil -> None
+ | Cons (k', v) xs -> if k = k' then v else fget_logic xs k
+ end
+
+(* Get an item from the map (imp)*)
+let rec fget (m: fmap) (k: tensor) : option value =
+ requires{ exists v. mem (k,v) m } (* The tensor must be in the map (absurd will never be reached) *)
+ requires{ forall v1, v2. mem (k,v1) m /\ mem (k,v2) m -> v1=v2}
+ (* The tensor must be in the map once and only once*)
+ (* Relaxed : it may appear several times, but with theesam value *)
+ ensures { result = fget_logic m k}
+ variant { m }
+ match m with
+ | Nil -> absurd
+ | Cons (k', v) xs ->
+ if k = k' then v
+ else fget xs k
+ end
+
+(* Set an item in the map (spec) *)
+function fset_logic (m: fmap) (k: tensor) (v: option value) : fmap =
+ match m with
+ | Nil -> Cons (k, v) Nil
+ | Cons (k', v') xs ->
+ if k = k' then Cons (k, v) xs
+ else Cons (k', v') (fset_logic xs k v)
+ end
+
+(* Set an item in the map (imp) *)
+let rec fset (m: fmap) (k: tensor) (v: option value) : fmap =
+ ensures { result = fset_logic m k v } (* The value is correctly set *)
+ ensures{ forall k', v'. mem (k', v') m /\ k' <> k ->
+ exists k'', v''. mem (k'',v'') result /\ v'=v''} (* The other values are not modified *)
+ variant { m }
+ match m with
+ | Nil -> Cons (k, v) Nil
+ | Cons (k', v') tl ->
+ if k = k' then Cons (k, v) tl
+ else Cons (k', v') (fset tl k v)
+ end
+
+(* If I set (k,v) in the map, then get(k) shall return v *)
+lemma get_set_eq:
+ forall m: fmap, k: tensor, v: option value.
+ fget_logic (fset_logic m k v) k = v
+
+(* When I set (k,v) in the map, then the rest of the map must not change,
+i.e., for any other key k', the value associated with k' shall not change *)
+lemma get_set_neq:
+ forall m: fmap, k1 k2: tensor, v: option value.
+ k1 <> k2 ->
+ fget_logic (fset_logic m k2 v) k1 = fget_logic m k1
+
+(* ------------------------------------------------------------------------- *)
+(* Link ("collage") between the abstract map and the implementation map *)
+(* ------------------------------------------------------------------------- *)
+
+(* Logical projection from the concrete fmap to the abstract map *)
+function fmap_to_map (m: fmap): Map.map tensor (option value) =
+ fun k -> fget_logic m k
+
+(* [TODO] The inverse projection is not defined, as the fmap is not a total function *)
+(* It is not possible to get a fmap from a map, as the map may contain keys that are not in the fmap *)
+
+(* Logical projection from the abstract map to the concrete fmap *)
+function map_to_fmap (m: Map.map tensor (option value)) : fmap
+
+(* get for fmap and Map are equivalent *)
+lemma fmap_get_complies_with_map_get:
+ forall m: fmap, k: tensor.
+ match fget_logic m k with
+ | Some v -> Map.get (fmap_to_map m) k = Some(v)
+ | None -> true
+ end
+
+(* set for fmap and Map are equivalent *)
+lemma fmap_set_complies_with_map_set:
+ forall m: fmap, k: tensor, v: option value.
+ fmap_to_map (fset_logic m k v) = Map.set (fmap_to_map m) k v
+
+
+(* =========================================================================== *)
+(* Operators *)
+(* =========================================================================== *)
+
+(* Computes the outputs of a node *)
+(* Currently, this is a dummy implementation that returns a list of identical values *)
+function eval_operator_log (op: operator) (inputs: list (option value)) : list (option value)
+
+(* Function modeling the behavior of an operator *)
+(* [TODO] Replace with actual operators *)
+let eval_operator (op: operator) (inputs: list (option value)) : list (option value)
+requires { length inputs = length op.opi } (* The node provides as any iputs as needed by the operator *)
+requires { forall i. mem i inputs -> i <> None } (* All inputs are initialized before execution *)
+ensures { forall i. mem i result -> i <> None } (* All outputs are initialized after execution*)
+ensures { length result = length op.opo } (* There is one value per output tensor *)
+=
+ (* This is a dummy implementation that returns the appropriate number of identical values *)
+ make_list (Some 0) (length op.opo)
+
+
+(* ------------------------------------------------------------------------- *)
+(* True if a tensor t is initialized in state s. *)
+(* ------------------------------------------------------------------------- *)
+predicate tensor_is_initialized (s: graph_state) (t: tensor) =
+ match Map.get s t with
+ | Some _ -> true
+ | None -> false
+end
+
+(* ------------------------------------------------------------------------- *)
+(* True if a tensor t is initialized in state s. *)
+(* ------------------------------------------------------------------------- *)
+let is_initialized (s: graph_state) (t: tensor) : bool
+ensures { result = tensor_is_initialized s t }
+=
+ match Map.get s t with
+ | Some _ -> true
+ | None -> false
+ end
+
+let rec are_initialized (s: graph_state) (l: list tensor) : bool =
+ensures { result = forall t. mem t l -> tensor_is_initialized s t }
+variant {l}
+match l with
+| Nil -> true
+| Cons x xs -> (is_initialized s x) && (are_initialized s xs)
+end
+
+(* ------------------------------------------------------------------------- *)
+(* True if node op is executable in state s *)
+(* ------------------------------------------------------------------------- *)
+predicate node_is_ready (s: graph_state) (op: node) =
+ (* A node is ready if all its inputs tensors are initialized *)
+ forall t: tensor.
+ mem t op.oi -> tensor_is_initialized s t
+
+let node_ready (s: graph_state) (op: node) : bool
+ensures { result = true <-> node_is_ready s op }
+=
+ are_initialized s op.oi
+
+
+(* =========================================================================== *)
+(* Graph execution *)
+(* =========================================================================== *)
+
+(* --------------------------------------------------------------------------- *)
+(* Execute one node *)
+(* --------------------------------------------------------------------------- *)
+let ghost exec_node (s: graph_state) (n: node) : graph_state
+requires { node_is_ready s n } (* The node must be ready to be executed *)
+requires { length n.oi = length n.ope.opi } (* The number of inputs must match the number of operator's inputs *)
+requires { length n.ou = length n.ope.opo } (* The number of outputs must match the number of operator's outputs *)
+ensures { forall t: tensor. mem t n.ou -> tensor_is_initialized result t } (* All output tensors are set *)
+=
+ (* Function that sets the value of a tensor in the graph state *)
+ let f (s: graph_state)(t: tensor)(v: (option value) ) : graph_state
+ (* The value of the tensor is set to v in the state st *)
+ requires { v <> None } (* We never assign a None value during the execution of a node *)
+ ensures { tensor_is_initialized result t }
+ =
+ fun k -> fget (fset (map_to_fmap s) t v) k
+ in
+ (* the values of tensors that are inputs to a node *)
+ let inputs = map (fun t -> Map.get s t) n.oi in
+ assert { forall v. mem v inputs -> v <> None };
+ (* the values of all outputs after evaluation *)
+ let outputs = eval_operator n.ope inputs in
+ assert { forall v. mem v outputs -> v <> None };
+ (* the updated state *)
+ fold_left2 (f) s n.ou outputs
+
+(* --------------------------------------------------------------------------- *)
+(* Execute all nodes.
+ Returns the graph state after executing all nodes in the graph
+ The next node to be executed is chosen non deterministically among the
+ executable nodes *)
+(* --------------------------------------------------------------------------- *)
+
+let rec ghost exec_nodes (s: graph_state) (ns: list node) : graph_state =
+ requires { forall n. mem n ns -> node_is_ready s n } (* All nodes in the list are ready to be executed *)
+ ensures { forall n : node. mem n ns ->
+ forall t: tensor. mem t n.ou ->
+ tensor_is_initialized result t } (* All outputs of the nodes are initialized *)
+ variant { ns }
+ match ns with
+ | Nil -> s
+ | Cons n ns ->
+ let s' = exec_node s n in
+ exec_nodes s' ns
+ end
+
+
+let rec filter ( b: node -> bool) (l: list node) : list node =
+ ensures { forall n. mem n result <-> (mem n l /\ b n) } (* The result contains only nodes that satisfy the predicate b *)
+ variant {l}
+ match l with
+ | Nil -> Nil
+ | Cons x xs ->
+ if b x then Cons x (filter b xs)
+ else filter b xs
+ end
+
+
+let rec ghost exec_nodes_until_completion (s: graph_state) (ns: list node) : graph_state =
+ (* All the output tensors of the nodes in ns are initialized *)
+ requires { forall n. mem n ns -> node_is_ready s n } (* All nodes in ns are ready *)
+ ensures { forall n: node. mem n ns ->
+ forall t: tensor. mem t n.ou ->
+ tensor_is_initialized result t } (* All outputs of the nodes are initialized *)
+ variant {ns}
+ let en = filter (fun n -> node_ready s n) ns
+ in
+ let dn = filter (fun n -> not node_ready s n) ns
+ in
+ match en with
+ | Nil -> s (* No node is ready, return the current state *)
+ | Cons n _ ->
+ let s' = exec_node s n in
+ exec_nodes_until_completion s' dn (* Execute the node and continue with the remaining nodes *)
+ end
+
+let ghost exec_graph (s: graph_state) (g: graph) : graph_state
+ requires { forall t. mem t g.gi -> tensor_is_initialized s t } (* The graph can only be executed if its inputs are initialized *)
+ ensures { forall t. mem t g.go -> tensor_is_initialized result t } (* After execution, all outputs are initialized *)
+ =
+ exec_nodes_until_completion s g.gn
+
+
+(* ------------------------------------------------------------------------- *)
+(* Initial tensor state: all tensors are undefined *)
+(* ------------------------------------------------------------------------- *)
+let ghost set_initial_state (g: graph) : graph_state =
+ fold_left (fun s t -> Map.set s t None) (Const.const None) g.gt
+
+
+(* ------------------------------------------------------------------------- *)
+(* /\ !Simple test: a fold-left and on list l is true iff all elements of
+ l are true. Why does the proof fail? *)
+(* ------------------------------------------------------------------------- *)
+predicate all_true (l: list bool) =
+ forall b: bool. mem b l -> b = true
+
+lemma and_true_true:
+ forall a: bool, b: bool. Bool.andb a b <-> a /\ b
+
+goal fold_left_and_equiv_all_true:
+ forall l: list bool.
+ FoldLeft.fold_left Bool.andb true l = true <-> all_true l
+(* ------------------------------------------------------------------------- *)
+
+
+end
+
+
+
diff --git a/safety-related-profile/documents/profile_graph/graph.md b/safety-related-profile/documents/profile_graph/graph.md
index 6a1a0eda..7987c3fe 100644
--- a/safety-related-profile/documents/profile_graph/graph.md
+++ b/safety-related-profile/documents/profile_graph/graph.md
@@ -1 +1,556 @@
-(Specification of the graph semantics and constraints. *To be completed*)
\ No newline at end of file
+## Restrictions
+The following restrictions apply to graphs in the SONNX profile:
+
+| Restriction | Statement | Origin |
+| -------- | ------- | ------- |
+| `[R1]`| There shall be a 1-to-1 mapping between the inputs and outputs of a node and the inputs and outputs of its associated operator. | TBC |
+| `[R2]` | All computation nodes of a graph must contribute to the computation of the graph outputs | No dead computation nodes |
+| `[R3]` | A graph must only contain computation nodes referring to operators in the SONNX subset | TBC |
+
+> (eric) Add a reference to ONNX documentation, e.g., [ONNX concepts](https://onnx.ai/onnx/intro/concepts.html).
+
+# Informal specification
+
+## Definitions
+### Graph
+- `[T01a]` A graph is an acyclic graph composed of *nodes* and *edges*
+- `[T01b]` A node is either a *tensor node* or a *computation node*
+
+> The fact that the graph is acyclic may not be necessary since there is also the SSA constraint...
+
+In the following example[^1], written using the `onnxruntime` API, the graph is composed of four computation nodes (`add_node`, `cons_node`, `mul_node1`, `mul_node2`) and 4 tensors nodes (`g_i1` and `g_i2`, `op1_o`, `op3_o`). The complete example in given in Section [example](#example) below).
+
+```python
+# Create nodes
+add_node = onnx.helper.make_node(op_type="Add", inputs=[g_i1_id, g_i2_id], outputs=[op1_o_id])
+cons_node = onnx.helper.make_node("Constant", inputs=[], outputs=[op2_o_id], value=const_value)
+mul_node1 = onnx.helper.make_node("Mul", inputs=[op1_o_id, op2_o_id], outputs=[op3_o_id])
+mul_node2 = onnx.helper.make_node("Mul", inputs=[g_i1_id, g_i2_id], outputs=[op4_o_id])
+[...]
+# Create graph
+graph = onnx.helper.make_graph(
+ nodes=[add_node, cons_node, mul_node1, mul_node2],
+ name="Example",
+ inputs=[g_i1, g_i2],
+ outputs=[op1_o, op3_o]
+)
+[...]
+```
+[^1]: The complete example in given in Section [example](#example) below.
+
+
+### Tensor nodes
+- `[T02a]` A tensor node is an object that can have a value or no value
+- `[T02b]` A tensor node is identified by a unique identifier within a graph
+
+`[RX]` A tensor node that is not the input of a computation node (i.e., it does not belong to any edges to a computation node input) must be an output node of the graph.
+
+In the following example[^1], written using the `onnxruntime` API, a tensor node is created using the `onnx.helper.make_tensor_value_info` function. In this example, `op1_o` is a tensor of rank 2 with no given dimensions. Its identifier is `op1_o` is `OP1_O`.
+
+```python
+op1_o_id = "OP1_O"
+op1_o = onnx.helper.make_tensor_value_info(op1_o_id, onnx.TensorProto.FLOAT, [None, None])
+```
+
+### Data flow computation nodes
+
+- `[T03a]` A computation node specifies some relation between its inputs and its outputs.
+- `[T03b]` The relation is defined by the *operator* that is associated with the node. The semantics of operators is defined in the SONNX profile opset (see, e.g., [add](../profile_opset/add/add.md)).
+ - Note that multiple computation nodes can refer to the same operator.
+- `[T03c]` There is a 1-to-1 mapping between the computation node's inputs and outputs and those of its associated operator .
+
+- `[RX]` A computation node must belong to at least one path from an input tensor to an output tensor of the graph (i.e., there shall be no "dead" node)
+- `[Rx]` A computation node must refer to an operator in the SONNX profile.
+
+In the following example[^1], nodes `mul_node1` and `mul_node2` refer to the same operator [`Mul`](../profile_opset/mul/mul.md) that has 2 inputs and 1 output.
+
+```python
+mul_node1 = onnx.helper.make_node("Mul", [op1_o_id, op2_o_id], [op3_o_id])
+mul_node2 = onnx.helper.make_node("Mul", [g_i1_id, g_i2_id], [op4_o_id])
+```
+
+### Control flow computation nodes
+
+> See later.
+
+
+### Edges
+- `[T04a]` An edge is a relation between a computation node, one input or output of this computation node, and a tensor node. A tensor that is related to some computation node input (resp. output) is said to be an input (resp. output) of the computation node.
+
+- `[Rx]` All inputs and outputs of all computation nodes must belong to an edge.
+ - Note that is is a restriction with respect to the ONNX standard that allows fewer inputs or outputs when the omitted input or output is optional
+
+In the following example[^1], edges are defined by the `inputs` and `outputs` arguments of the `make_node` and `make_graph` functions. For instance, the `add_node` computation node has 2 inputs (one for each element of the `inputs` list, noted $i_1$, $i_2$ hereafter) and 1 output (one for each element of the `outputs` list, noted $o$). The corresponding graph edges are:
+- e1: (add_node, $i_1$, g_i1_id)
+- e2: (add_node, $i_2$, g_i2_id)
+
+```python
+# Create nodes
+add_node = onnx.helper.make_node(op_type="Add", inputs=[g_i1_id, g_i2_id], outputs=[op1_o_id])
+cons_node = onnx.helper.make_node("Constant", inputs=[], outputs=[op2_o_id], value=const_value)
+mul_node1 = onnx.helper.make_node("Mul", inputs=[op1_o_id, op2_o_id], outputs=[op3_o_id])
+mul_node2 = onnx.helper.make_node("Mul", inputs=[g_i1_id, g_i2_id], outputs=[op4_o_id])
+[...]
+# Create graph
+graph = onnx.helper.make_graph(
+ nodes=[add_node, cons_node, mul_node1, mul_node2],
+ name="Example",
+ inputs=[g_i1, g_i2],
+ outputs=[op1_o, op3_o]
+)
+[...]
+```
+
+### Operators
+- `[T05a]` An operator specifies a function, i.e., a relation between the values of some input variables (the arguments of the function) and some output variables. For instance operation $z=\text{\bf add}(x,y)$ specifies a relation between variables $x$, $y$, and $z$ such that $z=x+y$.
+ - The set of input variables may be empty (case of a constant function).
+
+
+> (eric) Can a node have an internal state? In that case, it is not functional.
+
+### Example
+The following figure gives an example of a simple graph composed of 4 nodes. The graph has 2 input and 2 output tensors. Note that output of one of the nodes, `mul_node2`, is not used: this is actually forbidden in SONNX.
+
+
+
+The `onnxruntime`used to create the graph is given hereafter:
+
+```python
+import onnx
+import onnxruntime as ort
+import numpy as np
+
+# Define tensor identifiers
+g_i1_id = "G_I1"
+g_i2_id = "G_I2"
+op1_o_id = "OP1_O"
+op2_o_id = "OP2_O"
+op3_o_id = "OP3_O"
+op4_o_id = "OP4_O"
+
+# Create 2-rank input tensors (two inputs for division)
+g_i1 = onnx.helper.make_tensor_value_info(g_i1_id, onnx.TensorProto.FLOAT, [None, None])
+g_i2 = onnx.helper.make_tensor_value_info(g_i2_id, onnx.TensorProto.FLOAT, [None, None])
+
+# Create output tensors
+op1_o = onnx.helper.make_tensor_value_info(op1_o_id, onnx.TensorProto.FLOAT, [None, None])
+op2_o = onnx.helper.make_tensor_value_info(op2_o_id, onnx.TensorProto.FLOAT, [None, None])
+op3_o = onnx.helper.make_tensor_value_info(op3_o_id, onnx.TensorProto.FLOAT, [None, None])
+op4_o = onnx.helper.make_tensor_value_info(op4_o_id, onnx.TensorProto.FLOAT, [None, None])
+
+# Create a constant value
+const_value = onnx.helper.make_tensor(
+ name='const_tensor',
+ data_type=onnx.TensorProto.FLOAT,
+ dims=[2, 2],
+ vals=np.array([[1.0, 2.0], [3.0, 4.0]], dtype=np.float32).flatten() # Example values, adjust as needed
+)
+
+# Create nodes
+add_node = onnx.helper.make_node("Add", [g_i1_id, g_i2_id], [op1_o_id])
+cons_node = onnx.helper.make_node("Constant", [], [op2_o_id], value=const_value)
+mul_node1 = onnx.helper.make_node("Mul", [op1_o_id, op2_o_id], [op3_o_id])
+mul_node2 = onnx.helper.make_node("Mul", [g_i1_id, g_i2_id], [op4_o_id])
+
+# Create the ONNX graph
+graph = onnx.helper.make_graph(
+ nodes=[add_node, cons_node, mul_node1, mul_node2],
+ name="Example",
+ inputs=[g_i1, g_i2],
+ outputs=[op1_o, op3_o]
+)
+
+# Create the ONNX model
+model = onnx.helper.make_model(graph, opset_imports=[onnx.helper.make_opsetid("", 13)], ir_version=10) # Explicitly set opset to 13 and ir_version to 10
+onnx.checker.check_model(model)
+print(onnx.helper.printable_graph(model.graph))
+
+# Save the model
+onnx.save(model, "graph.onnx")
+
+# Load and run the model using ONNX Runtime
+session = ort.InferenceSession("graph.onnx")
+
+# Do inference
+i1 = np.array([[1.0, 2.0],[3.0, 4.0]], dtype=np.float32)
+i2 = np.array([[3.0, 4.0],[5.0, 6.0]], dtype=np.float32)
+output = session.run(None, {g_i1_id: i1, g_i2_id: i2})
+
+# Display results
+i1_f=(np.array2string(i1, separator=',', max_line_width=np.inf).replace('\n', ''))
+i2_f=(np.array2string(i2, separator=',', max_line_width=np.inf).replace('\n', ''))
+o1_f=(np.array2string(output[0], separator=',', max_line_width=np.inf).replace('\n', ''))
+o2_f=(np.array2string(output[1], separator=',', max_line_width=np.inf).replace('\n', ''))
+
+# Display results
+np.set_printoptions(precision=None, floatmode='fixed')
+print(f"I1={i1_f}, I2={i2_f}")
+print(f"Result={o1_f}{o2_f}")
+```
+
+## Execution Semantics
+Executing a graph means evaluating the output tensors of the graph according to the following rules:
+- `[T06a]` A computation node is executable if all the tensors connected to its inputs (i.e., belonging to an edge) are initialized
+
+> Only valid for data flow graphs. To be completed to account for control flow nodes.
+
+- `[T06b]` Executing a computation node means assigning values to the tensors connected to its outputs (i.e., belonging to an edge) so that the relation specified by the operator between its inputs and outputs holds
+- `[T06c]` All executable computation nodes shall be executed
+- `[T06e]` A tensor shall be assigned a value at most once (Single Assignment)
+
+
+## Special nodes
+
+ONNX provides two other categories of special nodes:
+- function nodes
+- control flow nodes.
+
+*This section is very preliminary*
+
+The way graphs are described and executed is independent from the operators used in the graph. In other terms, the semantics of the graph (how the operators are called) and the semantics of the operators (what the operators do) are defined separately. This modularity applies to the standard operators (convolution, relu, etc.) and to the special function and control flow nodes.
+
+### Functions nodes
+
+A "function" node is defined using primitive ONNX operators or other function operators. Function nodes are introduced [here](https://onnx.ai/onnx/intro/concepts.html), Section "Functions".
+
+Some ONNX operators are defined as functions, e.g.:
+- Softplus
+- Softsign
+- - Celu
+- HardSwish
+- Gelu
+- Selu
+
+
+For instance, the `SoftwaPlus`operator is defined as follows:
+```
+<
+ domain: "",
+ opset_import: ["" : 18]
+>
+Softplus (X) => (Y)
+{
+ exp_x = Exp (X)
+ one = Constant
+
+
-
-###### Constraints
-- (C1) Size of `strides`
- - Statement: the number of elements in the `strides` list is equal to 2. `[R5]`
- - Rationale: The SONNX profile only supports 2 spatial axes.
-- (C2) Value domain
- - Statement: `strides` is a list of strictly positive integers.
- - Rationale: Stride values are used in the denominator of expression in [constraint (C3) of X](#shape_consist)
-- (C3) Consistency between the shape of tensors `X`, `W`, `Y` and attributes `pads`, `dilations` and `strides`.
- - Statement: [See constraint (C3) of X](#shape_consist)
-
-##### `auto_pad` : string
-
-The `auto_pad` attribute determines if and how automatic padding is done for the input tensor X.
-
-###### Constraints
-- (C1) Explicit padding
- - Statement: `auto_pad` shall be set to `NOTSET` `[R3]`
- - Rationale: The SONNX profile imposes explicit padding.
-
-##### `pads`: list of int
-
-Attribute `pads` determines the padding at the beginning and end along each spatial axis of the input tensor `X`.
-
-`pads` is a list of the form (`x1_begin`, `x2_begin`,..., `x1_end`, `x2_end`,...), where `xi_begin` is the number of elements (possibly zero) added at the beginning of axis $i$ and `xi_end` is the number of elements added at the end of axis $i$.
-
-The padding value is 0.
-
-The effect of the `pads` attribute is illustrated on the following figure. In this example, `pads`=(1,3,2,2).
-
-
-
-###### Constraints
-- (C1) Value domain
- - Statement: `pads` is a list of positive or null integers.
- - Rationale: A padding value gives a number of elements to be added to some spatial axis. This is positive[^2].
-- (C2) Consistency between the shape of `X` and the length of `pads`
- - Statement: The length of the `pads` list is two times the number of spatial axes of `X`
- - Rationale: Padding shall be given for all spatial axes, and a beggining value and an end value must be given for each axis.
-- (C3) Consistency between the shape of tensors `X`, `W`, `Y` and attributes `pads`, `dilations` and `strides`.
- - Statement: [See constraint (C3) of X](#shape_consist)
-
-##### `dilations`: list of int
-
-Attribute `dilations` specifies the spacing between the kernel elements for each spatial axis of the filter `W`. It is a list of non-null integer values where each value gives the dilation factor for spatial axis $i$. If the dilation factor is greater than 1 for axis $i$, then the kernel points are spaced out by the dilation factor for that axis.
-
-The spacing value is 0.
-
-The effect of the `dilations` attribute for a tensor with two spatial axes is depicted on the following figure. In this example, `dilations`=(2,2).
-
-
-
-
-###### Constraints
-- (C1) Value domain
- - Statement: `dilations` is a list of strictly positive integers
-- (C2) Relation between `dilations` and `W`
- - Statement: The length of the `dilations` list is equal to number of spatial axes of `W`.
- - Rationale: Dilation is defined for all spatial axes of `W`.
-- (C3) Consistency between the shape of tensors `X`, `W`, `Y` and attributes `pads`, `dilations` and `strides`.
- - Statement: [See constraint (C3) of X](#shape_consist)
-
-##### `group`: int
-
-This attribute specifies the number of groups the input channels and output channels are divided into. When `group`=1, a standard convolution is performed.
-When group is greater than 1, convolution is computed for each group separately with a specific set of filters.
-
-The effect of the `group` attribute for a tensor with two spatial axes is depicted on the following figure. In this example `group`=3.
-
-
-
-(Taken from https://eli.thegreenplace.net/2018/depthwise-separable-convolutions-for-machine-learning)
-
-In the example, with `group` set to 3 and an input `X` and an output `Y` with 3 channels, the input and output channels will be divided into 3 groups of 1 channel.
-
-###### Constraints
-- (C1) Support for standard and depthwise convolutions
- - Statement: `group`=1 (standard convolution) or `group`$=c(X)$ (depthwise convolution)
- - Rationale: SONNX only supports standard and depthwise convolutions
-
-##### `kernel_shape`: list of int
-
-This parameter specifies the shape of the convolution kernel `W`.
-
-###### Constraints.
-
-- (C1) Value domain
- - Statement: `kernel_shape` is a list of strictly positive integers
- - Rationale: A dimension is always positive and cannot be null.
-- (C2) Consistency between `W` and `kernel_shape`
- - Statement: [See constraint (C3) of W](#kernel_shape_w)
-
-#### Outputs
-
-##### `Y`
-
-The size of the output `Y` will be $(b(Y) \times c(Y) \times h(Y) \times w(Y))$ where
-- $b(Y)$ is the number of batches
-- $c(Y)$ is the number of channels
-- $h(Y)$ and $w(Y)$ are the sizes of the output for the two spatial axes
-
-###### Constraints.
-- (C1) Consistency between the number of channels of `B` and `Y`
- - Statement: HYPERLIEN VERS W / constraint kernel shape
-- (C2) Consistency between the shape of tensors `X`, `W`, `Y`, attributes `pads` and `strides`,
- - Statement: [see constraint (C3) of X](#shape_consist)
-
-#### Formal specification
-
-The following code specifies the `conv` operator using the Why3 language[^3].
-
-###### Nota: the specification does not cover all attributes values. Currently, there is no padding (`pads` is not set and `auto_pad = NOTSET`) and `dilations` is not set.
-
-``` ocaml
-module Conv
- use int.Int
- use real.RealInfix
- use array.Array
- use int.ComputerDivision
- use real.Truncate
- use real.FromInt
-
- type input_tensor = {
- x: array real;
- x_l: int;
- x_c: int;
- x_b: int;
- x_ch: int;
- }
-
- type convolution_kernel = {
- w: array real;
- w_l: int;
- w_c: int;
- w_ch_in: int;
- w_ch_out: int;
- }
-
- type bias_tensor = {
- b: array real;
- b_c: int;
- }
-
- type attributes = {
- stride: array int;
- pads: array int;
- auto_pad: int;
- dilation: array int;
- }
-
- type output_tensor = {
-
- y_b: int;
- y_ch: int;
- y_l: int;
- y_c: int;
-
- }
-
- function conv_size (out: output_tensor) : int =
- out.y_b * out.y_ch * out.y_l * out.y_c
-
- predicate conv_result
- (inp: input_tensor)
- (kernel: convolution_kernel)
- (bias: bias_tensor)
- (attr: attributes)
- (out: output_tensor)
- (res: array real)
- (bi ci hi wi: int)
- (ci_in ki_h ki_w: int) =
- let y_idx = bi * (out.y_ch * out.y_l * out.y_c) + ci * (out.y_l * out.y_c) + hi * out.y_c + wi in
- let x_l_idx = hi * attr.stride[0] + ki_h * attr.dilation[0] - attr.pads[0] in
- let x_c_idx = wi * attr.stride[1] + ki_w * attr.dilation[1] - attr.pads[1] in
-
- (0 <= x_l_idx < inp.x_l /\ 0 <= x_c_idx < inp.x_c) ->
- let x_idx = bi * (inp.x_ch * inp.x_l * inp.x_c) + ci_in * (inp.x_l * inp.x_c) + x_l_idx * inp.x_c + x_c_idx in
- let w_idx = ci * (kernel.w_ch_in * kernel.w_l * kernel.w_c) + ci_in * (kernel.w_l * kernel.w_c) + ki_h * kernel.w_c + ki_w in
- res.elts (y_idx) = bias.b[ci] +. (inp.x[x_idx] *. kernel.w[w_idx])
-
- val conv (inp: input_tensor)(kernel: convolution_kernel)(bias: bias_tensor)(attr: attributes)(out: output_tensor): array real
- requires{inp.x_ch = out.y_ch = kernel.w_ch_in = bias.b_c}
- requires{out.y_l = (div (inp.x_l + attr.pads[0] + attr.pads[2] - (attr.dilation[0] * kernel.w_l)) attr.stride[0]) + 1}
- requires{out.y_c = (div (inp.x_c + attr.pads[1] + attr.pads[3] - (attr.dilation[1] * kernel.w_c)) attr.stride[1]) +1}
- requires { inp.x_l > 0 /\ inp.x_c > 0 /\ inp.x_ch > 0 /\ inp.x_b > 0}
- requires{kernel.w_l > 0 /\ kernel.w_c > 0 /\ kernel.w_ch_in > 0 /\ kernel.w_ch_out > 0}
- requires { out.y_b > 0 /\ out.y_ch > 0 /\ out.y_l > 0 /\ out.y_c > 0}
- requires { length inp.x = inp.x_l * inp.x_c * inp.x_ch * inp.x_b}
- requires{length kernel.w = kernel.w_l * kernel.w_c * kernel.w_ch_in * kernel.w_ch_out}
- requires{inp.x_l >= kernel.w_l}
- requires{inp.x_c >= kernel.w_c}
- requires{length bias.b = bias.b_c}
- requires{length attr.stride = 2}
- requires{length attr.dilation = 2}
- requires{length attr.pads = 4}
- requires{forall i. 0 <= i < length attr.pads -> attr.pads[i] = 0}
- requires{forall j. 0 <= j < length attr.dilation -> attr.dilation[j] >= 1}
- requires{forall k. 0 <= k < length attr.stride -> attr.stride[k] >= 1}
- ensures { length result = conv_size out }
- ensures { forall bi ci hi wi ci_in ki_h ki_w: int.
- 0 <= bi < out.y_b ->
- 0 <= ci < out.y_ch ->
- 0 <= hi < out.y_l ->
- 0 <= wi < out.y_c ->
- 0 <= ci_in < kernel.w_ch_in ->
- 0 <= ki_h < kernel.w_l ->
- 0 <= ki_w < kernel.w_c -> conv_result inp kernel bias attr out result bi ci hi wi ci_in ki_h ki_w }
-
-end
-
-
-module Test_conv
- use int.Int
- use real.RealInfix
- use array.Array
- use int.ComputerDivision
- use real.Truncate
- use real.FromInt
- use Conv
-
-let test_conv () =
- let inp_x = Array.make 9 1.0 in
- let inp = { x = inp_x; x_l = 3; x_c = 3; x_b = 1; x_ch = 1 } in
-
- let kernel_w = Array.make 4 0.0 in
- let kernel = { w = kernel_w; w_l = 2; w_c = 2; w_ch_in = 1; w_ch_out = 1 } in
-
- let bias_b = Array.make 1 0.5 in
- let bias = { b = bias_b; b_c = 1 } in
- let stride = Array.make 2 1 in (* Stride of 1 *)
- let pads = Array.make 4 0 in (* No padding *)
- let dilation = Array.make 2 1 in (* Dilation of 1 *)
- let attr = { stride = stride; pads = pads; auto_pad = 0; dilation = dilation } in
- let out_h = (div (inp.x_l + pads[0] + pads[2] - (dilation[0] * kernel.w_l)) stride[0]) + 1 in
- let out_w = (div (inp.x_c + pads[1] + pads[3] - (dilation[1] * kernel.w_c)) stride[1]) + 1 in
- let out = { y_b = 1; y_ch = 1; y_l = out_h ; y_c = out_w } in
- (* Call the conv function *)
- let result = conv inp kernel bias attr out in
- let actual_result = result.elts 0 in
- assert { conv_result inp kernel bias attr out result 0 0 0 0 0 0 0} ;
- assert { actual_result = 0.5 } ;
- ()
-
-end
-```
-
-Another formal specification of the `conv` operator using Frama-C
-language[^4] is presented below.
-
-``` objectivec
-#include
-
-Elements of the execution semantics is given on the [IR (Intermediate
-Representation) page](https://onnx.ai/onnx/repo-docs/IR.html) of the
-ONNX web site. In addition, a Python “reference implementation” is also
-provided (see ). The source
-code of this implementation can be found at
-.
-
-Very informally, the semantics is pretty simple: each operator (or
-function) is called according to its position in the topological sorting
-of the operators. The topological order is a partial order that ensures
-that an operator is executed only when its inputs are available. Being a
-partial order, it means that several valid orders exist for a given
-graph. Normally (?) each order should generate the same result, even in
-the presence of floating point operations.
-
-The Python code to execute a graph is given in class
-[`ReferenceEvaluator`](https://github.com/onnx/onnx/blob/main/onnx/reference/reference_evaluator.py)).
-After having processed the inputs and the initializers (i.e., fed the
-`results` dictorionary with these data), the nodes are executed in
-sequence. For each operator, the interpretor checks that its inputs are
-in the `results` dictionary. If they are not, an error is raised (if the
-operators are listed in topological order, this situation should not
-occur). Otherwise, the operator is simply executed (method `run`) with
-or without a context (composed of the current results) depending on the
-type of operators. (Check that this does not create a dependency to the
-total order of operators.)
-
-
-
-### Informal specification
-
-
-
-The semantics of an ONNX model is given in Section "Model Semantics" of
-the [Intermediate
-Representation](https://github.com/onnx/onnx/blob/main/docs/IR.md) page.
-Basically, an inference-model is a stateless function (except possibly
-for some specific nodes such as a random-generation node) represented by
-an acyclic `graph` of nodes. The `graph` is mainly represented by a set
-of inputs and outputs and a topologically sorted list of nodes. Each
-node represents a call to an operator or a function. A `function` is
-itself a graph.
-
-Note that the types of inputs and outputs are not systematically
-required because they can be inferred. In our case, I guess that we will
-forbib shape inference and rely on static tensor shapes (or, at least,
-shape inference can be bone before serializing the model). The proecss
-of shape inference is described in Section [ONNX Shape
-Inference](https://onnx.ai/onnx/repo-docs/ShapeInference.html).
-
-
-
-### Formal specification
-
-*To be completed.*
-
-[^1]: At least in a first phase...
-
-[^2]: Note: in the ONNX runtime implementation, the padding value may be
- negative, which corresponds to reducing the size of the tensor.
-
-[^3]: See [Why3 documentation](https://www(W)hy3.org/)
-
-[^4]: See [Frama-C
- documentation](https://www.frama-c.com/html/documentation.html)
diff --git a/safety-related-profile/documents/profile_opset/conv/imgs/README.md b/safety-related-profile/documents/profile_opset/conv/imgs/README.md
deleted file mode 100644
index 4a389a0a..00000000
--- a/safety-related-profile/documents/profile_opset/conv/imgs/README.md
+++ /dev/null
@@ -1 +0,0 @@
-Images used in the CONV specification example
diff --git a/safety-related-profile/documents/profile_opset/conv/imgs/autopad.png b/safety-related-profile/documents/profile_opset/conv/imgs/autopad.png
deleted file mode 100644
index 614f6942..00000000
Binary files a/safety-related-profile/documents/profile_opset/conv/imgs/autopad.png and /dev/null differ
diff --git a/safety-related-profile/documents/profile_opset/conv/imgs/conv-dep-3-channels.png b/safety-related-profile/documents/profile_opset/conv/imgs/conv-dep-3-channels.png
deleted file mode 100644
index 54b8ab1c..00000000
Binary files a/safety-related-profile/documents/profile_opset/conv/imgs/conv-dep-3-channels.png and /dev/null differ
diff --git a/safety-related-profile/documents/profile_opset/conv/imgs/conv-dep.png b/safety-related-profile/documents/profile_opset/conv/imgs/conv-dep.png
deleted file mode 100644
index 54b8ab1c..00000000
Binary files a/safety-related-profile/documents/profile_opset/conv/imgs/conv-dep.png and /dev/null differ
diff --git a/safety-related-profile/documents/profile_opset/conv/imgs/conv-std-3 channels.png b/safety-related-profile/documents/profile_opset/conv/imgs/conv-std-3 channels.png
deleted file mode 100644
index 8b1b8d10..00000000
Binary files a/safety-related-profile/documents/profile_opset/conv/imgs/conv-std-3 channels.png and /dev/null differ
diff --git a/safety-related-profile/documents/profile_opset/conv/imgs/conv-std-3-channels.png b/safety-related-profile/documents/profile_opset/conv/imgs/conv-std-3-channels.png
deleted file mode 100644
index 8b1b8d10..00000000
Binary files a/safety-related-profile/documents/profile_opset/conv/imgs/conv-std-3-channels.png and /dev/null differ
diff --git a/safety-related-profile/documents/profile_opset/conv/imgs/conv-std.png b/safety-related-profile/documents/profile_opset/conv/imgs/conv-std.png
deleted file mode 100644
index 660284cd..00000000
Binary files a/safety-related-profile/documents/profile_opset/conv/imgs/conv-std.png and /dev/null differ
diff --git a/safety-related-profile/documents/profile_opset/conv/imgs/conv.png b/safety-related-profile/documents/profile_opset/conv/imgs/conv.png
deleted file mode 100644
index 660284cd..00000000
Binary files a/safety-related-profile/documents/profile_opset/conv/imgs/conv.png and /dev/null differ
diff --git a/safety-related-profile/documents/profile_opset/conv/imgs/conv_pad.png b/safety-related-profile/documents/profile_opset/conv/imgs/conv_pad.png
deleted file mode 100644
index 2679ecbc..00000000
Binary files a/safety-related-profile/documents/profile_opset/conv/imgs/conv_pad.png and /dev/null differ
diff --git a/safety-related-profile/documents/profile_opset/conv/imgs/conv_stride.png b/safety-related-profile/documents/profile_opset/conv/imgs/conv_stride.png
deleted file mode 100644
index eed05a17..00000000
Binary files a/safety-related-profile/documents/profile_opset/conv/imgs/conv_stride.png and /dev/null differ
diff --git a/safety-related-profile/documents/profile_opset/conv/imgs/grouped_convolution.png b/safety-related-profile/documents/profile_opset/conv/imgs/grouped_convolution.png
deleted file mode 100644
index dfdf868c..00000000
Binary files a/safety-related-profile/documents/profile_opset/conv/imgs/grouped_convolution.png and /dev/null differ
diff --git a/safety-related-profile/documents/profile_opset/conv/imgs/onnx_conv.drawio b/safety-related-profile/documents/profile_opset/conv/imgs/onnx_conv.drawio
deleted file mode 100644
index 8585004a..00000000
--- a/safety-related-profile/documents/profile_opset/conv/imgs/onnx_conv.drawio
+++ /dev/null
@@ -1,3433 +0,0 @@
-
-
-Example 1:
-```math
-`condition` = \begin{bmatrix} True & False & True \end{bmatrix}
-```
-```math
-`X` = \begin{bmatrix} 9 & 8 & 7 \end{bmatrix}
-```
-```math
-`Y` = \begin{bmatrix} 6 & 5 & 4 \end{bmatrix}
-```
-Result `Z` will be :
-```math
-`Z` = \begin{bmatrix} 9 & 5 & 7 \end{bmatrix}
-```
-
-
-Example 2:
-```math
-`condition` = \begin{bmatrix} True & True \\ True & False \\ False & True \end{bmatrix}
-```
-```math
-`X` = \begin{bmatrix} 1 & 2 \\ 3 & 4 \\ 5 & 6 \end{bmatrix}
-```
-```math
-`Y` = \begin{bmatrix} 12 & 11 \\ 10 & 9 \\ 8 & 7 \end{bmatrix}
-```
-Result `Z` will be :
-```math
-`Z` = \begin{bmatrix} 1 & 2 \\ 3 & 9 \\ 8 & 6 \end{bmatrix}
-```
-
-Note in python is is equivalent to do :
-```python
->>> import numpy as np
-np.where([[True, True], [True, False],[False, True]],[[1, 2], [3, 4],[5, 6]],[[12, 11], [10, 9], [8,7]])
-array([[1, 2],
- [3, 9],
- [8, 6]])
-```
-
-#### Inputs and outputs
-
-##### `condition`
-
-Tensor `condition` is a tensor of boolean values indicating which elements to choose from `X` and `Y`.
-
-The shape of tensor `condition` should be the same as `X` and same as `Y`. `[R1]`. Broadcastable tensor is forbidden.`[R4]`.
-
-###### Constraints
-
-- (C1) Consistency in shape
- - Statement: The shapes of `condition`, `X`, and `Y` must be the same. $N(condition)=N(X)=N(Y)$ `[R1]`. Broadcastable tensor is forbidden.`[R4]`.
-
-##### `X`
-
-Tensor `X` is one of the two input tensors from which elements are picked based on the `condition`.
-
-The shape of tensor `X` should be the same as `condition` and `Y`. $N(X)=N(Y)$ `[R1]`. Broadcastable tensor is forbidden.`[R4]`.
-
-###### Constraints
-
-- (C1) Consistency in shape
- - Statement: The shapes of `condition`, `X`, and `Y` must be the same. `[R1]`. Broadcastable tensor is forbidden.`[R4]`.
-
-##### `Y`
-
-Tensor `Y` is one of the two input tensors from which elements are picked based on the `condition`.
-
-The shape of tensor `Y` should be the same as `condition` and `X`. `[R1]`. Broadcastable tensor is forbidden.`[R4]`.
-
-###### Constraints
-
-- (C1) Consistency in shape
- - Statement: The shapes of `condition`, `X`, and `Y` must be the same. $N(condition)=N(X)=N(Y)$ `[R1]`. Broadcastable tensor is forbidden.`[R4]`.
-
-#### Outputs
-
-##### `Z`
-
-The tensor `Z` is the output tensor formed by picking values from `X` and `Y` based on `condition`.
-
-`Z` will have the resulting shape of `condition`, `X`, and `Y` and must be the same. `[R1]`. Broadcastable tensor is forbidden.`[R4]`.
-
-###### Constraints
-
-- (C1) Consistency in shape
- - Statement: The shape of `Z` will match the `condition`, `X`, and `Y` shape. $N(Z)=N(condition)=N(X)=N(Y)$ `[R1]`. Broadcastable tensor is forbidden.`[R4]`.
-
-
-#### Attributes
-The `where` operator does not require any attributes.
-
-### Formal specification
-
-The formal specification of the `where` operator using the Why3 language[^1] is provided below. This specification ensures the consistency and desired behavior of the operator within the constraints described.
-
-```ocaml
-module Where
- use int.Int
- use bool.Bool
- use array.Array
-
- type tensor = {
- data: array real;
- dims: array int; (* tensor dimension *)
- }
-
- function size (t: tensor) : int =
- let rec product (a: array int) (i: int) : int =
- if i = length a then 1 else a[i] * product a (i + 1)
- in product t.dims 0
-
- predicate same_dimensions (dims1: array int) (dims2: array int) : bool =
- length dims1 = length dims2 /\
- (forall i: int. 0 <= i < length dims1 -> dims1[i] = dims2[i])
-
- predicate where_result
- (cond: tensor)
- (X: tensor)
- (Y: tensor)
- (Z: tensor)
- (i: int) =
- (cond.data[i] <> 0 -> Z.data[i] = X.data[i]) /\
- (cond.data[i] = 0 -> Z.data[i] = Y.data[i])
-
- val where (cond: tensor) (X: tensor) (Y: tensor): tensor
- requires { same_dimensions cond.dims X.dims }
- requires { same_dimensions cond.dims Y.dims }
- requires { same_dimensions X.dims Y.dims }
- ensures { Z.dims = cond.dims }
- ensures { length Z.data = size Z }
- ensures { forall i: int. 0 <= i < length Z.data -> where_result cond X Y Z i }
-```
-
-### Specification en Frama-C
-Another formal specification of the conv operator using Frama-C language is presented below[^2].
-
-
-```c
-#include This is an informative part
+## Actions +### New actions +- [ ] (1103-1, all) Review Ricardo and João's formal specification and verification guidelines +- [ ] (1103-2, all) Concludes on the expected behaviour of a **Conv** or **MaxPool** with incompatible sizes (should these conditions be verified statically? what should happen if these conditions cannot be guaranteed statically?) +- [ ] (1103-3, all) Inform ONNX Runtime about the problem found in their implementation (**MaxPool** and others) +- [ ] (1103-4, all) Find a practical way to discriminate the "specifying" part of the informal specification from the informative part. +- [ ] (1103-5, Mariem) Check why the SONNX backend has not been pushed in the AIDGE repo. +- [ ] (1103-6) Ensure that the **Conv** op integrated in Aidge is actually the one generated out of Ricardo and João's formal spec. +- [ ] (1103-7) Complete tests on **Conv** as they have been done on **MaxPool** (after action 1103-2 is closed) +### Previous actions +- [ ] Provision of the accuracy section for **Div**, **Matmul**, and possibly **tanh**. + - (Franck) Bounds for propagation **Tanh** and **Div**. About **Matmul**, see Franck's slides. +- [ ] (2801-3, all) Check how NaNs are addressed in the completed operators. They shouldn't be treated as "errors". Update the guidelines accordingly. +- [ ] (1911-2, All) Review Jean's V&V proposal + - Eric to put updated slides on the repo : Done. + - File to be reviewed not yet delivered. +- Actions from local work sessions + +# 2026/02/25 +## Participants +- Joõ, Camille, Eric, Mariem, Dumitru, Ricardo, Franck +## Agenda +- Review of actions (Eric) +- Status of [specification](https://github.com/users/ericjenn/projects/4) +- Meeting on accuracy (Eric+Jean+Franck), see the [minutes](../meetings/numerical%20accuracy/2026-02-17%20-%20DeepGreen%20-%20Accuracy.md). +- Meeting on formal methods (Eric+All) +- Progress and questions from Portugal! (Ricardo and João) +- The case of **MaxPool**, continued, see the [Jupyter notebook](https://github.com/ericjenn/working-groups/blob/ericjenn-srpwg-wg1/safety-related-profile/sonnx/ops/spec/tests/maxpool/Test_Max_Pool_Divergence.ipynb) (Henri) +- On the spec of mathematical operators, using [mpfr](https://www.mpfr.org/mpfr-current/mpfr.html#index-mpfr_005fpowr) (Eric) +- Local WG (Eric) + - See [actions](../meetings/Local%20WGs/Tlse/agenda.md) +## Minutes +- Ricardo and João have explained their approach to specify **MatMul**. Having a written version of the general principles, methods (and possibly tricks...) that have been applied would be extremely useful for the team. Hopefully, this could be part of the R&J's master's thesis report. +- On ORT, the behaviour of **Matmul** differs when applied on float null tensors and integer null tensors. Multiplying null tensors is well defined and can lead to non null tensors. We have to add a notice explaining that the behaviour of ORT differ from the spec. +- More generally, we agree that the spec must provide a unique output even though different implementations may return different result. We will add a notice stating the possible divergence (limited to ORT). It is up to an implementer to show where his/her implementation does not comply with the spec. We may produce some kind of a "compliance report" for ORT CPU (for instance) as an example. +- Back to **Maxpool**: + - we have to take care of optional outputs. + - the behaviour of **Maxpool** is extremely variable depending on the backend (CPU, tensortRT, CUDA). Besides the erroneous indexes when dealing with Infs, we also observe strange results on the max value themselves. Refer to [Henri's notebook](../sonnx/ops/spec/tests/maxpool/Test_Max_Pool_Divergence.ipynb) for further details. +## Actions +### New actions +### Previous actions +- [ ] Provision of the accuracy section for **Div**, **Matmul**, and possibly **tanh**. + - (Franck) Bounds for propagation **Tanh** and **Div**. About **Matmul**, see Franck's slides. +- [ ] (2801-3, all) Check how NaNs are addressed in the completed operators. They shouldn't be treated as "errors". Update the guidelines accordingly. +- [X] (1401-4, All) Collect all questions to be asked to Loïc with enough material to present the issues (example) and give our own solution (when available) + - Material shall be placed [here](https://github.dev/ericjenn/working-groups/blob/ericjenn-srpwg-wg1/safety-related-profile/meetings/formal_methods/inputs/inputs-2026-02-18.md) +- [ ] (1911-2, All) Review Jean's V&V proposal + - Eric to put updated slides on the repo : Done. + - File to be reviewed not yet delivered. +- [ ] Actions from local work sessions + - (0511-1, Joao, Ricardo) Check how to handle NaN in Why3 (if possible!)... See Mariem's link. + - To be discussed during Feb session with Loïc. + - Some solutions are available. These solutions must be discussed with Loïc. + - Solution to be sent to Mariem first... + - On-going: First proposal sent by J&R ; currently being discussed with Jorge then to be discussed with Loïc + +# 2026/02/11 (shortened to 1h) +## Participants +- Henri, Ricardo, João, Jean, Mariem, Edoardo, Jean-Loup, Franck +## Agenda +- WG progress +- The case of MaxPool +- Accuracy analysis approach (Franck) +- News from DeepGreen (Mariem) + +## Minutes +- News + - Our work has been presented to the ERTS 2026 conference. The slides are [there](./Other_meetings/SONNX%20-%20ERTS2026.pdf). +- Status of actions (Eric) + - See also [those for the local WG](./Local%20WGs/Tlse/agenda.md). +- Work done by the Tlse WG and actions (Eric) + - See also [those for the local WG](./Local%20WGs/Tlse/agenda.md). +- Discussion about the section on accuracy (see supporting slides) + - We have to provide the user some information to support the analysis of error, including propagated error. We provide the expression of the propagated error at first order. + - Examples are being developed (Franck) on **Div**, **Matmul**, and possibly **tanh**. + - (Note that the accurracy section shall be named ` (Zoom does not give me a list of participants and I have not noted who was there...so the list if incomplete, sorry about that. Please add your name...
+
+## Minutes
+- ONNX model verification tool
+ - This tool will implement the constraints and restrictions identified at operator and graph level
+ - The tool shall be part of the ONNX distribution
+ - Using (e.g.) DeepGreen's ONNX parser could make sense but (i) we have to be sure that we can distribute it as part of ONNX, (ii) it will bring with it part of the AIDGE framework (iii) it may be overkill with respect to the level of parsing that we actually need.
+ - Developing our own parser (possibly from something already available...) could also be a way to specify formally the file format (i.e., a correct ONNX file is a file that can be parsed successfully by our parser).
+- Review of the comments on the [`where`](../documents/profile_opset/matmul/where.md) operator
+ - Sparse tensors have to be forbidden. This can be checked at the file level by looking for the usage of the SparseTensorProto class.
+ - In the specification of operators, we should state that such tensors cannot be used. This should be part of the operators' signatures. To be elaborated, see action [2901-1]
+ - Henri has given an example in Python. Should we generalize this?
+ - We propose to add a few example in a Jupyter Notebook for each operator.
+ - The examples must use ONNX.
+ - Those examples are not a test suite. They allow the user to get acquainted / play with of the operator.
+ - The behaviour of the operator in the Jupytrer notebook may be different from the one of reference implementation.
+ - In the Jupyter notebook, we have to be clear that the example is given for documentation only.
+ - See action [2901-3].
+- Specification work
+ - Nicolas has added LSTM to the operator's list. Dumitru proposes to help. See action [2901-4].
+ - It could be useful to start thinking about the graph semantics... See action [2901-5].
+ - The work moves slowly...
+ - We lack volunteers to do the hard work...
+ - We may become more visible and reach out a larger community (and hopefully, have more volunteers) once we have a first set of specification, completed documents.
+ - Edoardo proposes to use students to help us on the specification activity. (Jean will have one student to work on this topic) See action [2901-6].
+ Note that the initial list of interested people was pretty large... we may ask if some of them are still interested to contribute...
+- List of issues
+ - Anne-Sophie has removed some entries from [issues.md](../deliverables/issues/issues.md) since some of the ambiguities have been solved thanks to Sebastian.
+ - However, it make sense to keep them in the list since part of our job is to prevent such ambiguities... See action [2901-2].
+- On the specification of behavior in case of errors
+ - At operator level
+ - Whenever a value is out of the operator's domain, its behavior is "undefined" (e.g. xi<=0 in x for operator log(x)). In that case, the specification shall (i) indicate the domain constraint and (ii) state that the behaviour of the operator is undefined should the constraint be violated.
+ - For some operators, some inputs will generally be static, even though the ONNX does not enforce this. In that case, we may add a restriction to ensure that the tensor's value will be known before runtime, and add a constraints on its value to prevent runtime error.
+ - At graph level
+ - In some cases, the structure of the graph can ensure that the inputs values of an operator will always be in domain even though, they may be not in the general case.
+ - We may also propagate the domain constraints backward up to the inputs, and provide the user with these constraint (which would restrict the graph input domain). This could be interesting, but goes further than a verification.
+ - Whenever we cannot guarantee the absence of runtime error, the model wil be considered "unsafe".
+- Compliance with regulatory docs.
+ - It would be useful to identify the constraints/reqs in the EASA's concept paper that are relevant to our work. See action [2901-7]
+- Formal methods.
+ - See [minutes](../meetings/formal_methods/minutes.md) of FM sub-group on Feb. 28th.
+ - Main conclusion: We will be using Why3 as the specification language. Work will start with a training session (being planned mid-march) done by Loïc.
+## New actions
+- [ ] (2901-1, Eric) Check how to express constraints about SparseTensor at operator level.
+- [ ] (2901-2, Anne-Sophie) Put back the issues (in the appropriate section) and add the answer given by Seb.
+- [ ] (2901-3, Eric) Provide a Jupyter notebook for the `conv` operator (see [here](../documents/profile_opset/conv/tests/conv_onnx.ipynb)).
+- [ ] (2901-4, Dumitru) Contact Nicolas to lend a hand on LSTM.
+- [ ] (2901-5, Dumitru) Prepare a short presentation on the graph's semantics. Planned for March 12th.
+- [ ] (2901-6, Edoardo) Check how to involve students in the specification work.
+- [ ] (2901-7, Jean-Baptiste) Analysis of EASA's Concept Paper.
+- [ ] (2901-8, Henri) Consider Eric's [remarks](../documents/profile_opset/where/reviews/eric.md) on operator `where`.
+## Past actions
+- [ ] (1501-1, Sebastian) Specify some operators...
+ - Sebastian is working on `reshape`and other ops.
+- [ ] (1501-2, Eric & Jean) Find a way to involve more people in the specification work...
+ - *Thinking...*
+- [X] (1501-4, All) Review the specification of the [`where` operator](../documents/profile_opset/where/where.md). Put your remarks in the [reviews](../documents/profile_opset/where/reviews/) directory (in file `Development
+ + + + diff --git a/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/layout.CFlat.html b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/layout.CFlat.html new file mode 100644 index 00000000..e73e5ba7 --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/layout.CFlat.html @@ -0,0 +1,105 @@ + + + + + +library layout — module CFlat+module CFlat + use tensor.std.Int + use tensor.std.List + use tensor.tensor.Range + + function offset (ks ds : list int) : int = + match ks , ds with + | Cons k ks , Cons _ ds -> k * size ds + offset ks ds + | _ -> 0 + end + + function index (p : int) (ds : list int) : list int = + match ds with + | Nil -> Nil + | Cons _ ds -> let n = size ds in Cons (div p n) (index (mod p n) ds) + end + + let rec lemma offset_size (ks ds : list int) + requires { valid ks ds } + ensures { 0 <= offset ks ds < size ds } + {proof…} + variant { ds } + = match ks , ds with + | Cons k krs , Cons d drs -> + offset_size krs drs ; + let p = offset ks ds in + let q = offset krs drs in + assert { p = size drs * k + q } ; + assert { + size drs * k + <= size drs * (d - 1) + = d * size drs - size drs + } ; + | _ -> () + end + {qed} + + let rec lemma index_range (p : int) (ds : list int) + requires { positive ds } + requires { 0 <= p < size ds } + ensures { valid (index p ds) ds } + {proof…} + variant { ds } + = match ds with + | Nil -> () + | Cons _ rds -> index_range (mod p (size rds)) rds + end + {qed} + + let rec lemma index_of_offset (ks ds : list int) + requires { valid ks ds } + ensures { index (offset ks ds) ds = ks } + {proof…} + variant { ds } + = match ks , ds with + | Cons k rks , Cons _ rds -> + index_of_offset rks rds ; + let p = offset ks ds in + let n = size rds in + let q = offset rks rds in + euclide p k n q ; + | _ -> () + end + {qed} + + let rec lemma offset_of_index (p : int) (ds : list int) + requires { positive ds } + requires { 0 <= p < size ds } + ensures { offset (index p ds) ds = p } + {proof…} + variant { ds } + = match ds with + | Nil -> () + | Cons _ rds -> + let n = size rds in + offset_of_index (mod p n) rds + end + {qed} + + let rec lemma offset_push (ks ds : list int) (k d : int) + requires { valid ks ds } + ensures { offset (push ks k) (push ds d) = offset ks ds * d + k } + {proof…} + variant { ks } + = match ks , ds with + | Cons _ krs , Cons _ drs -> offset_push krs drs k d + | _ -> () + end + {qed} + +end ++ + + diff --git a/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/layout.index.html b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/layout.index.html new file mode 100644 index 00000000..fb908df5 --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/layout.index.html @@ -0,0 +1,13 @@ + + + + + +
library layoutmodule CFlat+ + + diff --git a/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/layout.proof.html b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/layout.proof.html new file mode 100644 index 00000000..6ba4ddd9 --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/layout.proof.html @@ -0,0 +1,41 @@ + + + + + +
library layout — proofsProvers
++ alt-ergo @2.5.4 n=16 171ms + cvc5 @1.2.1 n=42 492ms + z3 @4.13.4 n=33 865ms ++
Proofs
+module layout.CFlat+
+ goal offset_size + split_vc + alt-ergo 25ms + alt-ergo 13ms + alt-ergo 17ms + z3 13ms + cvc5 102ms
+ goal index_range + alt-ergo 101ms
+ goal index_of_offset + cvc5 72ms
+ goal offset_of_index + alt-ergo 189ms
+ goal offset_push + split_vc + alt-ergo 56ms + alt-ergo 15ms + split_vc + alt-ergo 1.4s + alt-ergo 17ms + alt-ergo 43ms+ + diff --git a/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/libtensor.CTensor.html b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/libtensor.CTensor.html new file mode 100644 index 00000000..745d8712 --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/libtensor.CTensor.html @@ -0,0 +1,130 @@ + + + + + +
library libtensor — module CTensor+module CTensor + use tensor.std.Int + use tensor.std.List + use tensor.std.Clib + use tensor.std.Cfloat + use mach.int.Int32 + use tensor.tensor.Range + use tensor.tensor.Tensor + use tensor.layout.CFlat + use tensor.libvector.CIndex + + + type farray = ptr float + + type ctensor = { + t_rank : int32 ; + t_dims : iarray ; + t_data : farray ; + } + + function tensor_dim (t : ctensor) : list int = ivector t.t_dims t.t_rank + function tensor_size (t : ctensor) : int = vdim t.t_dims t.t_rank + predicate valid_index (k : list int) (t : ctensor) = valid k (tensor_dim t) + predicate empty_tensor (t : ctensor) = t.t_rank = 0 + + predicate valid_tensor (t : ctensor) = + dimension t.t_dims t.t_rank /\ + valid_range t.t_data 0 (tensor_size t) /\ + writable t.t_data + + function tensor_offset (k : list int) (t : ctensor) : int = offset k (tensor_dim t) + + function tensor_value_at (k : list int) (t : ctensor) : real = + if valid_index k t then + value_at t.t_data (tensor_offset k t) + else 0.0 + + function tensor_value (t : ctensor) : list int -> real = + fun k -> tensor_value_at k t + + function tensor_valueb (t : ctensor) : list int -> bool = + fun k -> Real.(tensor_value_at k t > 0.0) + + let ghost function tensor (t : ctensor) : tensor real + {proof…} + requires { valid_tensor t } + ensures { result.dims = tensor_dim t } + ensures { result.data = tensor_value t } + ensures { result.background = 0.0 } + {qed} + = { + dims = pure { tensor_dim t } ; + data = pure { tensor_value t } ; + background = 0.0 ; + } + + let ghost function tensorb (t : ctensor) : tensor bool + {proof…} + requires { valid_tensor t } + ensures { result.dims = tensor_dim t } + ensures { result.data = tensor_valueb t } + ensures { result.background = false } + {qed} + = { + dims = pure { tensor_dim t } ; + data = pure { tensor_valueb t } ; + background = false ; + } + + let ctensor_create (ds : iarray) (n : int32) : ctensor = + {proof…} + requires { dimension ds n } + ensures { empty_tensor result \/ valid_tensor result } + ensures { empty_tensor result \/ result.t_rank = n } + ensures { empty_tensor result \/ result.t_dims = ds } + {qed} + let m = cdim_size ds n in + let vs = malloc (to_uint32 m) in + { + t_rank = if is_null vs then 0 else n ; + t_dims = ds ; + t_data = vs ; + } + + let ctensor_clear (r : ctensor) = + requires { valid_tensor r } + ensures { tensor r = Tensor.zero 0.0 (tensor_dim r) } + let m = cdim_size r.t_dims r.t_rank in + for i = 0 to m-1 do + {proof…} + invariant { forall k. 0 <= k < i -> value_at r.t_data k = 0.0 } + {qed} + r.t_data[i] <- f32 0.0 + done + {proof…} + ; assert { tensor r == Tensor.zero 0.0 (tensor_dim r) } + {qed} + + let ctensor_reset (r : ctensor) (v : float) = + requires { valid_tensor r } + ensures { tensor r = Tensor.const (to_real v) 0.0 (tensor_dim r) } + let m = cdim_size r.t_dims r.t_rank in + for i = 0 to m-1 do + {proof…} + invariant { forall k. 0 <= k < i -> value_at r.t_data k = v } + {qed} + r.t_data[i] <- v + done + {proof…} + ; assert { tensor r == Tensor.const (to_real v) 0.0 (tensor_dim r) } + {qed} + + + + +end ++ + + diff --git a/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/libtensor.index.html b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/libtensor.index.html new file mode 100644 index 00000000..34b4db5e --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/libtensor.index.html @@ -0,0 +1,13 @@ + + + + + +
library libtensormodule CTensor+ + + diff --git a/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/libtensor.proof.html b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/libtensor.proof.html new file mode 100644 index 00000000..445f391e --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/libtensor.proof.html @@ -0,0 +1,39 @@ + + + + + +
library libtensor — proofsProvers
++ alt-ergo @2.5.4 n=16 215ms + cvc5 @1.2.1 n=42 489ms + z3 @4.13.4 n=30 140ms ++
Proofs
+module libtensor.CTensor+
+ goal tensor + alt-ergo 29ms
+ goal tensorb + alt-ergo 33ms
+ goal ctensor_create + alt-ergo 40ms
+ goal ctensor_clear + alt-ergo 242ms
+ goal ctensor_reset + split_vc + alt-ergo 20ms + alt-ergo 27ms + alt-ergo 20ms + alt-ergo 19ms + alt-ergo 34ms + alt-ergo 46ms + alt-ergo 75ms + alt-ergo 27ms + alt-ergo 34ms+ + diff --git a/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/libvector.CIndex.html b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/libvector.CIndex.html new file mode 100644 index 00000000..908f7e9a --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/libvector.CIndex.html @@ -0,0 +1,160 @@ + + + + + +
library libvector — module CIndex+module CIndex + use tensor.std.Int + use tensor.std.List + use tensor.std.Clib + use mach.int.Int32 + use tensor.tensor.Range + use tensor.layout.CFlat + + type iarray = ptr int32 + + function ivector (u : iarray) (n : int) : list int + = map Int32.to_int (vector u n) + + function islice (u : iarray) (p q : int) : list int + = map Int32.to_int (slice u p q) ++
+
+Dimensions
++ function vdim (u : iarray) (n : int) : int = size (ivector u n) + function sdim (u : iarray) (p q : int) : int = size (islice u p q) + + predicate pdim (u : iarray) (p q : int) = + forall k. p <= k < q -> 0 < value_at u k + + predicate dimension (u : iarray) (n : int) = + 0 <= n /\ valid_range u 0 n /\ pdim u 0 n /\ 0 < vdim u n <= max_int32 ++
+
+Equivalence betwen pdim and tensor.Range.positive.
+ let rec lemma positive_pdim (u : iarray) (p q : int) + {proof…} + ensures { pdim u p q <-> positive (islice u p q) } + variant { q - p } + = if p < q then positive_pdim u (p+1) q + {qed} + + let ghost sdim_split (u : iarray) (p k q : int) + {proof…} + requires { p <= k < q } + requires { pdim u p q } + ensures { sdim u p k * value_at u k * sdim u (k+1) q = sdim u p q } + = assert { islice u p k ++ islice u k q = islice u p q } + {qed} ++
+
+Extracted Library
++ let cdim_size (u : iarray) (n : int32): int32 = + ensures { result = vdim u n } + {proof…} + requires { dimension u n } + {qed} + begin + let ref p = 1 in + for i = 0 to n - 1 do + {proof…} + invariant { p = vdim u i } + ghost + begin + ensures { 1 <= p * u[i] <= max_int32 } + let ghost dl = pure { sdim u 0 i } in + let ghost di = Int32.to_int u[i] in + let ghost dr = pure { sdim u (i+1) n } in + let ghost dn = pure { sdim u 0 n } in + sdim_split u 0 (Int32.to_int i) (Int32.to_int n) ; + mult_bound (dl * di) dr dn ; + end ; + {qed} + p <- p * u[i] ; + done ; p + end + + let cdim_create_1 (n : int32) : iarray = + requires { 0 < n } + ensures { is_not_null result -> vdim result 1 = n } + {proof…} + ensures { is_not_null result -> dimension result 1 } + ensures { is_not_null result -> value_at result 0 = n } + {qed} + let cd = malloc 1 in + if is_not_null cd then cd[0] <- n ; cd + + let cdim_create_2 (p q : int32) : iarray = + requires { 0 < p /\ 0 < q /\ p * q <= max_int32 } + ensures { is_not_null result -> vdim result 2 = p * q } + {proof…} + ensures { is_not_null result -> dimension result 2 } + ensures { is_not_null result -> value_at result 0 = p } + ensures { is_not_null result -> value_at result 1 = q } + {qed} + let cd = malloc 2 in + if is_not_null cd then (cd[0] <- p ; cd[1] <- q) ; cd ++
+
+Coordinates
++ let coffset (ks : iarray) (ds : iarray) (n : int32) : int32 = + {proof…} + requires { 0 <= n } + requires { valid_range ks 0 n } + requires { dimension ds n } + ensures { 0 <= result -> valid (ivector ks n) (ivector ds n) } + ensures { 0 <= result -> result = offset (ivector ks n) (ivector ds n) } + {qed} + begin + let ref p = 0 in + for i = 0 to n - 1 do + {proof…} + invariant { valid (ivector ks i) (ivector ds i) } + invariant { p = offset (ivector ks i) (ivector ds i) } + {qed} + let d = ds[i] in + let k = ks[i] in + if 0 <= k && k < d then + begin + {proof…} + assert { p * d + k = offset (ivector ks (i+1)) (ivector ds (i+1)) } ; + ghost + begin + ensures { Int32.in_bounds (p * d) } + ensures { Int32.in_bounds (p * d + k) } + let ghost dl = pure { sdim ds 0 i } in + let ghost di = Int32.to_int ds[i] in + let ghost dr = pure { sdim ds (i+1) n } in + let ghost dn = pure { sdim ds 0 n } in + sdim_split ds 0 (Int32.to_int i) (Int32.to_int n) ; + mult_bound (dl * di) dr dn ; + end ; + {qed} + p <- p * d + k ; + end + else return (-1) + done ; p + end + +end ++ + + diff --git a/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/libvector.index.html b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/libvector.index.html new file mode 100644 index 00000000..324ac9a4 --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/libvector.index.html @@ -0,0 +1,16 @@ + + + + + +
library libvector
+
+C–Library to compute Offsets & Dimensions
+module CIndex+ + + diff --git a/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/libvector.proof.html b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/libvector.proof.html new file mode 100644 index 00000000..76a8189b --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/libvector.proof.html @@ -0,0 +1,83 @@ + + + + + +
library libvector — proofsProvers
++ alt-ergo @2.5.4 n=16 171ms + cvc5 @1.2.1 n=42 492ms + z3 @4.13.4 n=33 865ms ++
Proofs
+module libvector.CIndex+
+ goal positive_pdim + alt-ergo 69ms
+ goal sdim_split + alt-ergo 170ms
+ goal cdim_size + split_vc + alt-ergo 19ms + alt-ergo 22ms + alt-ergo 25ms + alt-ergo 17ms + alt-ergo 19ms + alt-ergo 35ms + alt-ergo 626ms + alt-ergo 24ms + alt-ergo 19ms + alt-ergo 126ms + alt-ergo 16ms + alt-ergo 14ms
+ goal cdim_create_1 + alt-ergo 158ms
+ goal cdim_create_2 + split_vc + alt-ergo 16ms + alt-ergo 13ms + alt-ergo 17ms + alt-ergo 17ms + alt-ergo 20ms + alt-ergo 262ms + alt-ergo 34ms + alt-ergo 23ms + alt-ergo 20ms + alt-ergo 16ms + alt-ergo 16ms + alt-ergo 15ms + alt-ergo 17ms
+ goal coffset + split_vc + alt-ergo 18ms + alt-ergo 24ms + alt-ergo 25ms + alt-ergo 24ms + alt-ergo 22ms + alt-ergo 835ms + alt-ergo 34ms + alt-ergo 18ms + alt-ergo 20ms + alt-ergo 65ms + alt-ergo 152ms + split_vc + inline_goal + split_vc + alt-ergo 28ms + stuck + alt-ergo 19ms + alt-ergo 18ms + alt-ergo 17ms + alt-ergo 902ms + alt-ergo 20ms + alt-ergo 17ms + alt-ergo 15ms + alt-ergo 18ms + alt-ergo 14ms + alt-ergo 16ms+ + diff --git a/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/script.js b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/script.js new file mode 100644 index 00000000..9e1faafc --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/script.js @@ -0,0 +1,54 @@ +function toggle(elt) { + var elts,j; + while (elt && !elt.classList.contains("section")) { + elt = elt.parentElement; + } + if (!elt) return; + elts = elt.querySelectorAll(".section-text, .section-toggle"); + for (j = 0; j < elts.length; j++) + elts[j].classList.toggle("active"); +} + +function focus() { + var h,elts,e,tk,i; + h = window.location.hash; + e = document.getElementById(h.substring(1)); + while (e) { + tk = e.classList; + if (tk.contains("section-text") && !tk.contains("active")) { + toggle(e); + break; + } + e = e.parentElement; + } +} + +function escape(evt) { + var elts,e,i; + if (evt.code === "Escape") { + window.location = ""; + elts = document.querySelectorAll(".section"); + for (i=0; i< elts.length; i++) { + e = elts[i]; + if (e.querySelectorAll(".section-toggle.active").length) + toggle(e); + } + } +} + +(function(){ + var nodes,i; + + nodes = document.getElementsByClassName("section-toggle"); + for (i = 0; i < nodes.length; i++) { + nodes[i].addEventListener("click", function() { + toggle(this); + }); + } + + focus(); + window.addEventListener('onload',focus); + window.addEventListener('hashchange',focus); + window.addEventListener('keypress',escape); + +})(); diff --git a/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/std.Cfloat.html b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/std.Cfloat.html new file mode 100644 index 00000000..f92b0ba0 --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/std.Cfloat.html @@ -0,0 +1,59 @@ + + + + + +
library std — module Cfloat+module Cfloat + use int.Int + use real.Real + + type float = abstract { to_real : real } + meta coercion function to_real + + type f32 = < float 8 24 > (* single precision literals *) + type f64 = < float 11 53 > (* double precision literals *) + + val function f32 (k : f32) : float + ensures { result = f32'real k } + + val function f64 (k : f64) : float + ensures { result = f64'real k } + + let constant zero = f64 0.0 + let constant one = f64 1.0 + + val function (.+) (a b : float) : float + ensures { Real.( result = a + b ) } + + val function (.-) (a b : float) : float + ensures { Real.( result = a - b ) } + + val function (.-_) (a : float) : float + ensures { Real.( result = (- a) ) } + + val function ( .* ) (a b : float) : float + ensures { Real.( result = a * b ) } + + val function ( ./ ) (a b : float) : float + requires { b <> 0.0 } + ensures { Real.( result = a / b ) } + + val predicate ( .= ) (a b : float) : bool + ensures { result <-> Real.( a = b ) } + + val predicate ( .< ) (a b : float) : bool + ensures { result <-> Real.( a < b ) } + + val predicate ( .<= ) (a b : float) : bool + ensures { result <-> Real.( a <= b ) } + +end ++ + + diff --git a/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/std.Clib.html b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/std.Clib.html new file mode 100644 index 00000000..a1288577 --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/std.Clib.html @@ -0,0 +1,117 @@ + + + + + +
library std — module Clib+module Clib + use map.Map + use int.Int + use mach.int.Int32 + use export mach.c.C + + type int32 = Int32.int32 + type uint32 = UInt32.uint32 + + val function to_uint32 (v : int32) : uint32 + requires { 0 <= v } + ensures { Int32.to_int v = UInt32.to_int result } ++
+
+Null–Pointer
++ val predicate is_null (vp : ptr 'a) : bool + ensures { result <-> vp.zone = null_zone } ++
+
+Array–range validity
++ predicate valid_range (vp : ptr 'a) (p q : int) = + q <= p \/ + ( 0 <= vp.min <= vp.offset /\ + 0 <= p <= q <= max_int32 /\ + 0 <= vp.min <= vp.offset + p /\ + vp.offset + q <= vp.max <= vp.plength ) + + let lemma valid_in_range (vp : ptr 'a) (p k q : int) + {proof…} + requires { p <= k < q } + requires { valid_range vp p q } + ensures { valid_ptr_shift vp k } + = () + {qed} ++
+
+Array as map
++ let ghost function value_at (vp : ptr 'a) : map int 'a = + pure { fun k -> vp.data.Array.elts (vp.offset + k) } ++
+
+Array access (ghost)
++ function ([]) (vp : ptr 'a) (k : int) : 'a = value_at vp k ++
+
+Array access (C, inlined)
++ let ([]) (vp : ptr 'a) (k : int32) : 'a + {proof…} + requires { vp.min <= vp.offset + k < vp.max } + ensures { result = vp[k] } + = get_ofs vp k + {qed} ++
+
+Array update (C, inlined)
++ let ([]<-) (vp : ptr 'a) (k : int32) (v : 'a) : unit + requires { writable vp } + requires { vp.min <= vp.offset + k < vp.max } + ensures { value_at vp = Map.([<-]) (old (value_at vp)) k v } + = set_ofs vp k v ++
+
+Array as list
++ use List + + let rec ghost function slice (u : ptr 'a) (p q : int) : list 'a = + {proof…} + variant { q - p } + {qed} + if q <= p then Nil else Cons (value_at u p) (slice u (p+1) q) + + let rec lemma slice_append (u : ptr 'a) (p q r : int) + requires { p <= q <= r } + ensures { slice u p r = slice u p q ++ slice u q r } + {proof…} + variant { q - p } + = if p < q then slice_append u (p+1) q r + {qed} + + let ghost function vector (u : ptr 'a) (n : int) = slice u 0 n + + let lemma vector_push (u : ptr 'a) (n : int) + requires { 0 <= n } + ensures { vector u (n+1) = push (vector u n) (value_at u n) } + {proof…} + = slice_append u 0 n (n+1) + {qed} + +end ++ + + diff --git a/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/std.Int.html b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/std.Int.html new file mode 100644 index 00000000..3ded1908 --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/std.Int.html @@ -0,0 +1,50 @@ + + + + + +
library std — module Int+module Int + use export int.Int + use export int.Abs + use export int.ComputerDivision ++
+
+Unicity of euclidian division decomposition
++ let ghost euclide (a b q r : int) + requires { 0 <= a /\ 0 <= r < q } + requires { a = b * q + r } + ensures { b = div a q } + ensures { r = mod a q } + {proof…} + = let rec kernel (b r : int) + requires { b * q + r = 0 } + requires { abs r < q } + ensures { b = r = 0 } + variant { abs b } + = if b < 0 then kernel (b + 1) (r - q) else + if b > 0 then kernel (b - 1) (r + q) else () + in kernel (b - div a q) (r - mod a q) + {qed} ++
+
+Multiplication upper–bound
++ let ghost mult_bound (a b c : int) + requires { 0 < a * b <= c } + ensures { abs a <= c } + ensures { abs b <= c } + = () + +end ++ + + diff --git a/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/std.List.html b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/std.List.html new file mode 100644 index 00000000..13c07ac4 --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/std.List.html @@ -0,0 +1,34 @@ + + + + + +
library std — module List+module List + use export list.List + use export list.Map + use export list.Append ++
+
+Appends an element to the end of the list
++ function push (xs : list 'a) (x : 'a) : list 'a = + xs ++ Cons x Nil + + let rec lemma map_concat (f : 'a -> 'b) (xs ys : list 'a) + ensures { map f (xs ++ ys) = map f xs ++ map f ys } + {proof…} + variant { xs } + = match xs with Cons _ rxs -> map_concat f rxs ys | Nil -> () end + {qed} + +end ++ + + diff --git a/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/std.index.html b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/std.index.html new file mode 100644 index 00000000..fe20174f --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/std.index.html @@ -0,0 +1,16 @@ + + + + + +
library stdmodule Int+
module List+
module Clib+
module Cfloat+ + + diff --git a/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/std.proof.html b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/std.proof.html new file mode 100644 index 00000000..ceb91d5d --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/std.proof.html @@ -0,0 +1,63 @@ + + + + + +
library std — proofsProvers
++ alt-ergo @2.5.4 n=16 171ms + cvc5 @1.2.1 n=42 492ms + z3 @4.13.4 n=33 865ms ++
Proofs
+module std.Int+
+ goal euclide + alt-ergo 47ms
+ goal mult_bound + z3 6ms
module std.List+
+ goal map_concat + alt-ergo 18ms
module std.Clib+
+ value to_uint32 + value is_null ++
+ goal valid_in_range + alt-ergo 14ms
+ goal ([]) + alt-ergo 11ms
+ goal ([]) + alt-ergo 11ms
+ goal ([]<-) + alt-ergo 15ms
+ goal slice + alt-ergo 14ms
+ goal slice_append + alt-ergo 29ms
+ goal vector_push + z3 16ms
module std.Cfloat+
+ value f32 + value f64 + value (.+) + value (.-) + value (.-) + value (.*) + value (./) + value (.=) + value (.<) + value (.<=) ++
+ goal zero + split_vc
+ goal one + split_vc+ + diff --git a/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/style.css b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/style.css new file mode 100644 index 00000000..1c6997e4 --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/style.css @@ -0,0 +1,138 @@ +/* -------------------------------------------------------------------------- */ +/* --- CSS Style Sheet for why3find doc generator --- */ +/* -------------------------------------------------------------------------- */ + +/* -------------------------------------------------------------------------- */ +/* --- Links --- */ +/* -------------------------------------------------------------------------- */ + +a { + color: teal; + outline: none; + text-decoration: none; +} + +a:visited { + color: teal; +} + +a:hover { + background: lightgreen; +} + +a:target { + background: lightblue; +} + +/* -------------------------------------------------------------------------- */ +/* --- Header Styling --- */ +/* -------------------------------------------------------------------------- */ + +header { + padding: 4px ; + color: darkgrey ; + border-bottom: thin solid darkgray ; +} + +header a { color: grey !important } + +/* -------------------------------------------------------------------------- */ +/* --- Table Of Contents --- */ +/* -------------------------------------------------------------------------- */ + +nav { display: none; } + +/* -------------------------------------------------------------------------- */ +/* --- Documentation Styling --- */ +/* -------------------------------------------------------------------------- */ + +div.doc { + /* Documentation block styling */ +} + +/* -------------------------------------------------------------------------- */ +/* --- Source Code Styling --- */ +/* -------------------------------------------------------------------------- */ + +pre.src { + /* Source code block styling */ +} + +.scope { + color: teal; +} + +.keyword { + color: purple; +} + +.admitted { + color: #DA2525; +} + +.attribute { + color: green; +} + +.comment { + color: grey; +} + +/* -------------------------------------------------------------------------- */ +/* --- Proof Marks --- */ +/* -------------------------------------------------------------------------- */ + +.icon { + margin-left: 2px ; + vertical-align: text-top ; + font-size: small ; + text-decoration: none ; +} + +.icon.small { font-size: x-small } + +.valid { color: green !important } +.failed { color: red !important } +.warning { color: orange !important } +.remark { color: lightgrey !important } +.prover:hover { color: purple } + +/* -------------------------------------------------------------------------- */ +/* --- Foldable Section --- */ +/* -------------------------------------------------------------------------- */ + +.section { } + +.section.level1:hover { + background: #fcfce1; +} + +.section.level2:hover { + background: #e9ffe9; +} + +.section.level3:hover { + background: #fff6f6; +} + +.section-toggle:hover { + background: lightgreen; +} + +.section-toggle { + cursor: zoom-in ; +} + +.section-toggle.active { + cursor: zoom-out ; +} + +.section-text { + display: none; +} + +.section-text.active { + display: inline; +} + +/* -------------------------------------------------------------------------- */ diff --git a/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/tensor.Range.html b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/tensor.Range.html new file mode 100644 index 00000000..a2cbf7f7 --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/tensor.Range.html @@ -0,0 +1,80 @@ + + + + + +
library tensor — module Range+module Range + use int.Int + use tensor.std.List + + function size (ds : list int) : int = + match ds with + | Nil -> 1 + | Cons d ds -> d * size ds + end + + predicate positive (ds : list int) = + match ds with + | Nil -> true + | Cons d ds -> 0 < d /\ positive ds + end + + predicate valid (ks ds : list int) = + match ks , ds with + | Nil , Nil -> true + | Cons k ks , Cons d ds -> 0 <= k < d /\ valid ks ds + | _ -> false + end + + let rec lemma valid_push (ks ds : list int) (k d : int) + requires { 0 <= k < d } + requires { valid ks ds } + ensures { valid (push ks k) (push ds d) } + {proof…} + variant { ks } + = match ks , ds with + | Nil , Nil -> () + | Cons _ ks , Cons _ ds -> valid_push ks ds k d + | _ -> absurd + end + {qed} + + let rec lemma size_append (xs ys : list int) + ensures { size (xs ++ ys) = size xs * size ys } + {proof…} + variant { xs } + = match xs with Cons _ rxs -> size_append rxs ys | Nil -> () end + {qed} + + lemma size_push: forall xs x. size (push xs x) = size xs * x + + let rec lemma positive_size (ds : list int) + requires { positive ds } + ensures { 0 < size ds } + {proof…} + variant { ds } + = match ds with Nil -> () | Cons _ ds -> positive_size ds end + {qed} + + let rec lemma positive_valid (ks ds : list int) + requires { valid ks ds } + ensures { positive ds } + ensures { 0 < size ds } + {proof…} + variant { ds } + = match ks , ds with + | Cons _ ks , Cons _ ds -> positive_valid ks ds + | _ -> () + end + {qed} + +end ++ + + diff --git a/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/tensor.Tensor.html b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/tensor.Tensor.html new file mode 100644 index 00000000..bc50c46d --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/tensor.Tensor.html @@ -0,0 +1,112 @@ + + + + + +
library tensor — module Tensor
+Library tensor
+
+
+index —
+
+
+
+Formalization of Tensor
++module Tensor + use int.Int + use map.Map + use list.List + use Range + + type data 'a = map (list int) 'a + + type tensor 'a = { + dims : list int ; + data : data 'a ; + background : 'a ; (* default value, or value for 0-dimensions tensor *) + } + invariant { positive dims } + invariant { forall k. valid k dims \/ data k = background } + {proof…} + by let d = any 'a in { dims = Nil ; data = (fun _ -> d) ; background = d } + {qed} + + meta coercion function dims + meta coercion function data ++
+
+Tensor with the same dimensions
++ predicate (~) (a : tensor 'a) (b : tensor 'b) = a.dims = b.dims ++
+
+Tensor with the same dimensions and background value
++ predicate (~=) (a : tensor 'a) (b : tensor 'a) = + a ~ b /\ a.background = b.background ++
+
+Equal tensors
++ predicate (==) (a b : tensor 'a) = + a ~= b /\ forall k. valid k a.dims -> a.data k = b.data k ++
+
+Extensionality
++ lemma exteq: forall a b : tensor 'a. a == b <-> a = b + {proof…} by tensor'eq a b {qed} ++
+
+Scalar Tensor
++ let ghost function scalar (v : 'a) : tensor 'a + ensures { result.dims = Nil } + ensures { result.background = v } + ensures { forall k. result k = v } + {proof…} + = { dims = Nil ; data = (fun _ -> v) ; background = v } + {qed} ++
+
+Null Tensor
++ let ghost function zero (e : 'a) (ds : list int) : tensor 'a + requires { positive ds } + ensures { result.dims = ds } + ensures { result.background = e } + ensures { forall k. result k = e } + {proof…} + = { dims = ds ; data = (fun _ -> e) ; background = e } + {qed} ++
+
+Constant Tensor
++ let ghost function const (v : 'a) (bg : 'a) (ds : list int): tensor 'a + ensures { result.dims = ds } + requires { positive ds } + ensures { result.background = bg } + ensures { forall k. valid k ds -> result k = v } + {proof…} + = { dims = ds ; data = pure { fun k -> if valid k ds then v else bg } ; background = bg } + {qed} ++
+
+Constant & Null
++ goal zero_is_const: forall e : 'a, ds. positive ds -> zero e ds == const e e ds + +end ++ + + diff --git a/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/tensor.index.html b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/tensor.index.html new file mode 100644 index 00000000..5626f691 --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/tensor.index.html @@ -0,0 +1,18 @@ + + + + + +
library tensor
+
+Formalization of coordinates and dimensions
+module Range+
module Tensor+ + + diff --git a/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/tensor.proof.html b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/tensor.proof.html new file mode 100644 index 00000000..0270105f --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/common/libs/tensor/generated_doc/tensor.proof.html @@ -0,0 +1,46 @@ + + + + + +
library tensor — proofsProvers
++ alt-ergo @2.5.4 n=16 171ms + cvc5 @1.2.1 n=42 489ms + z3 @4.13.4 n=30 140ms ++
Proofs
+module tensor.Range+
+ goal valid_push + alt-ergo 32ms
+ goal size_append + alt-ergo 28ms
+ goal size_push + alt-ergo 11ms
+ goal positive_size + alt-ergo 18ms
+ goal positive_valid + alt-ergo 29ms
module tensor.Tensor+
+ goal tensor + alt-ergo 12ms
+ goal exteq + split_vc + alt-ergo 13ms + alt-ergo 13ms + alt-ergo 13ms
+ goal scalar + alt-ergo 15ms
+ goal zero + alt-ergo 12ms
+ goal const + alt-ergo 17ms
+ goal zero_is_const + alt-ergo 12ms+ + diff --git a/safety-related-profile/sonnx/ops/code/concat/generated_code/c_code/README.md b/safety-related-profile/sonnx/ops/code/concat/generated_code/c_code/README.md new file mode 100644 index 00000000..e69de29b diff --git a/safety-related-profile/sonnx/ops/code/concat/generated_code/ocaml_code/README.md b/safety-related-profile/sonnx/ops/code/concat/generated_code/ocaml_code/README.md new file mode 100644 index 00000000..e69de29b diff --git a/safety-related-profile/sonnx/ops/code/concat/generated_doc/README.md b/safety-related-profile/sonnx/ops/code/concat/generated_doc/README.md new file mode 100644 index 00000000..e69de29b diff --git a/safety-related-profile/sonnx/ops/code/concat/tests/README.md b/safety-related-profile/sonnx/ops/code/concat/tests/README.md new file mode 100644 index 00000000..e69de29b diff --git a/safety-related-profile/sonnx/ops/code/conv/generated_code/c_code/cindex.c b/safety-related-profile/sonnx/ops/code/conv/generated_code/c_code/cindex.c new file mode 100644 index 00000000..6d82f3e4 --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/conv/generated_code/c_code/cindex.c @@ -0,0 +1,58 @@ +#include "cindex.h" + +int32_t cdim_size(int32_t * u, int32_t n) { + int32_t p; + int32_t i, o; + p = 1; + o = n - 1; + if (0 <= o) { + for (i = 0; ; ++i) { + p = p * u[i]; + if (i == o) { + break; + } + } + } + return p; +} + +int32_t * cdim_create_1(int32_t n) { + int32_t * cd; + cd = malloc(1U * sizeof(int32_t)); + if (cd) { + cd[0] = n; + } + return cd; +} + +int32_t * cdim_create_2(int32_t p, int32_t q) { + int32_t * cd; + cd = malloc(2U * sizeof(int32_t)); + if (cd) { + cd[0] = p; + cd[1] = q; + } + return cd; +} + +int32_t coffset(int32_t * ks, int32_t * ds, int32_t n) { + int32_t p; + int32_t i, o, d, k; + p = 0; + o = n - 1; + if (0 <= o) { + for (i = 0; ; ++i) { + d = ds[i]; + k = ks[i]; + if (0 <= k && k < d) { + p = p * d + k; + } else { + return -1; + } + if (i == o) { + break; + } + } + } + return p; +} diff --git a/safety-related-profile/sonnx/ops/code/conv/generated_code/c_code/cindex.h b/safety-related-profile/sonnx/ops/code/conv/generated_code/c_code/cindex.h new file mode 100644 index 00000000..f8c9d87c --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/conv/generated_code/c_code/cindex.h @@ -0,0 +1,15 @@ +#ifndef CINDEX_H_INCLUDED + +#include
Development
+
+
+
+
+
+
diff --git a/safety-related-profile/sonnx/ops/code/where/generated_doc/layout.CFlat.html b/safety-related-profile/sonnx/ops/code/where/generated_doc/layout.CFlat.html
new file mode 100644
index 00000000..4ba4086d
--- /dev/null
+++ b/safety-related-profile/sonnx/ops/code/where/generated_doc/layout.CFlat.html
@@ -0,0 +1,105 @@
+
+
+
+
+
+library layout — module CFlat+module CFlat + use std.Int + use std.List + use tensor.Range + + function offset (ks ds : list int) : int = + match ks , ds with + | Cons k ks , Cons _ ds -> k * size ds + offset ks ds + | _ -> 0 + end + + function index (p : int) (ds : list int) : list int = + match ds with + | Nil -> Nil + | Cons _ ds -> let n = size ds in Cons (div p n) (index (mod p n) ds) + end + + let rec lemma offset_size (ks ds : list int) + requires { valid ks ds } + ensures { 0 <= offset ks ds < size ds } + {proof…} + variant { ds } + = match ks , ds with + | Cons k krs , Cons d drs -> + offset_size krs drs ; + let p = offset ks ds in + let q = offset krs drs in + assert { p = size drs * k + q } ; + assert { + size drs * k + <= size drs * (d - 1) + = d * size drs - size drs + } ; + | _ -> () + end + {qed} + + let rec lemma index_range (p : int) (ds : list int) + requires { positive ds } + requires { 0 <= p < size ds } + ensures { valid (index p ds) ds } + {proof…} + variant { ds } + = match ds with + | Nil -> () + | Cons _ rds -> index_range (mod p (size rds)) rds + end + {qed} + + let rec lemma index_of_offset (ks ds : list int) + requires { valid ks ds } + ensures { index (offset ks ds) ds = ks } + {proof…} + variant { ds } + = match ks , ds with + | Cons k rks , Cons _ rds -> + index_of_offset rks rds ; + let p = offset ks ds in + let n = size rds in + let q = offset rks rds in + euclide p k n q ; + | _ -> () + end + {qed} + + let rec lemma offset_of_index (p : int) (ds : list int) + requires { positive ds } + requires { 0 <= p < size ds } + ensures { offset (index p ds) ds = p } + {proof…} + variant { ds } + = match ds with + | Nil -> () + | Cons _ rds -> + let n = size rds in + offset_of_index (mod p n) rds + end + {qed} + + let rec lemma offset_push (ks ds : list int) (k d : int) + requires { valid ks ds } + ensures { offset (push ks k) (push ds d) = offset ks ds * d + k } + {proof…} + variant { ks } + = match ks , ds with + | Cons _ krs , Cons _ drs -> offset_push krs drs k d + | _ -> () + end + {qed} + +end ++ + + diff --git a/safety-related-profile/sonnx/ops/code/where/generated_doc/layout.index.html b/safety-related-profile/sonnx/ops/code/where/generated_doc/layout.index.html new file mode 100644 index 00000000..fb908df5 --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/where/generated_doc/layout.index.html @@ -0,0 +1,13 @@ + + + + + +
library layoutmodule CFlat+ + + diff --git a/safety-related-profile/sonnx/ops/code/where/generated_doc/layout.proof.html b/safety-related-profile/sonnx/ops/code/where/generated_doc/layout.proof.html new file mode 100644 index 00000000..6ba4ddd9 --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/where/generated_doc/layout.proof.html @@ -0,0 +1,41 @@ + + + + + +
library layout — proofsProvers
++ alt-ergo @2.5.4 n=16 171ms + cvc5 @1.2.1 n=42 492ms + z3 @4.13.4 n=33 865ms ++
Proofs
+module layout.CFlat+
+ goal offset_size + split_vc + alt-ergo 25ms + alt-ergo 13ms + alt-ergo 17ms + z3 13ms + cvc5 102ms
+ goal index_range + alt-ergo 101ms
+ goal index_of_offset + cvc5 72ms
+ goal offset_of_index + alt-ergo 189ms
+ goal offset_push + split_vc + alt-ergo 56ms + alt-ergo 15ms + split_vc + alt-ergo 1.4s + alt-ergo 17ms + alt-ergo 43ms+ + diff --git a/safety-related-profile/sonnx/ops/code/where/generated_doc/libtensor.CTensor.html b/safety-related-profile/sonnx/ops/code/where/generated_doc/libtensor.CTensor.html new file mode 100644 index 00000000..0236b4a6 --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/where/generated_doc/libtensor.CTensor.html @@ -0,0 +1,154 @@ + + + + + +
library libtensor — module CTensor+module CTensor + use std.Int + use std.List + use std.Clib + use std.Cfloat + use mach.int.Int32 + use tensor.Range + use tensor.Tensor + use tensor.OPWhere + use layout.CFlat + use libvector.CIndex + + type farray = ptr float + + type ctensor = { + t_rank : int32 ; + t_dims : iarray ; + t_data : farray ; + } + + function tensor_dim (t : ctensor) : list int = ivector t.t_dims t.t_rank + function tensor_size (t : ctensor) : int = vdim t.t_dims t.t_rank + predicate valid_index (k : list int) (t : ctensor) = valid k (tensor_dim t) + predicate empty_tensor (t : ctensor) = t.t_rank = 0 + + predicate valid_tensor (t : ctensor) = + dimension t.t_dims t.t_rank /\ + valid_range t.t_data 0 (tensor_size t) /\ + writable t.t_data + + function tensor_offset (k : list int) (t : ctensor) : int = offset k (tensor_dim t) + + function tensor_value_at (k : list int) (t : ctensor) : real = + if valid_index k t then + value_at t.t_data (tensor_offset k t) + else 0.0 + + function tensor_value (t : ctensor) : list int -> real = + fun k -> tensor_value_at k t + + function tensor_valueb (t : ctensor) : list int -> bool = + fun k -> Real.(tensor_value_at k t > 0.0) + + let ghost function tensor (t : ctensor) : tensor real + {proof…} + requires { valid_tensor t } + ensures { result.dims = tensor_dim t } + ensures { result.data = tensor_value t } + ensures { result.background = 0.0 } + {qed} + = { + dims = pure { tensor_dim t } ; + data = pure { tensor_value t } ; + background = 0.0 ; + } + + let ghost function tensorb (t : ctensor) : tensor bool + {proof…} + requires { valid_tensor t } + ensures { result.dims = tensor_dim t } + ensures { result.data = tensor_valueb t } + ensures { result.background = false } + {qed} + = { + dims = pure { tensor_dim t } ; + data = pure { tensor_valueb t } ; + background = false ; + } + + let ctensor_create (ds : iarray) (n : int32) : ctensor = + {proof…} + requires { dimension ds n } + ensures { empty_tensor result \/ valid_tensor result } + ensures { empty_tensor result \/ result.t_rank = n } + ensures { empty_tensor result \/ result.t_dims = ds } + {qed} + let m = cdim_size ds n in + let vs = malloc (to_uint32 m) in + { + t_rank = if is_null vs then 0 else n ; + t_dims = ds ; + t_data = vs ; + } + + let ctensor_clear (r : ctensor) = + requires { valid_tensor r } + ensures { tensor r = Tensor.zero 0.0 (tensor_dim r) } + let m = cdim_size r.t_dims r.t_rank in + for i = 0 to m-1 do + {proof…} + invariant { forall k. 0 <= k < i -> value_at r.t_data k = 0.0 } + {qed} + r.t_data[i] <- f32 0.0 + done + {proof…} + ; assert { tensor r == Tensor.zero 0.0 (tensor_dim r) } + {qed} + + let ctensor_reset (r : ctensor) (v : float) = + requires { valid_tensor r } + ensures { tensor r = Tensor.const (to_real v) 0.0 (tensor_dim r) } + let m = cdim_size r.t_dims r.t_rank in + for i = 0 to m-1 do + {proof…} + invariant { forall k. 0 <= k < i -> value_at r.t_data k = v } + {qed} + r.t_data[i] <- v + done + {proof…} + ; assert { tensor r == Tensor.const (to_real v) 0.0 (tensor_dim r) } + {qed} + + let ctensor_where (cond a b r : ctensor) = + {proof…} + requires { valid_tensor cond } + requires { valid_tensor a } + requires { valid_tensor b } + requires { valid_tensor r } + requires { tensor a ~= tensor b ~= tensor r } + {qed} + requires { tensorb cond ~ tensor a ~ tensor b } + ensures { tensor r = opwhere (tensorb cond) (tensor a) (tensor b) } + let m = cdim_size r.t_dims r.t_rank in + for i = 0 to m-1 do + {proof…} + invariant { + forall k. 0 <= k < i -> + value_at r.t_data k = + if Real.(0.0 < value_at cond.t_data k) + then a.t_data[k] else b.t_data[k] + } + {qed} + r.t_data[i] <- + if (f32 0.0) .< cond.t_data[i] then a.t_data[i] else b.t_data[i] + done + {proof…} + ; assert { tensor r == opwhere (tensorb cond) (tensor a) (tensor b) } + {qed} + +end ++ + + diff --git a/safety-related-profile/sonnx/ops/code/where/generated_doc/libtensor.index.html b/safety-related-profile/sonnx/ops/code/where/generated_doc/libtensor.index.html new file mode 100644 index 00000000..abc11ecc --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/where/generated_doc/libtensor.index.html @@ -0,0 +1,13 @@ + + + + + +
library libtensormodule CTensor+ + + diff --git a/safety-related-profile/sonnx/ops/code/where/generated_doc/libtensor.proof.html b/safety-related-profile/sonnx/ops/code/where/generated_doc/libtensor.proof.html new file mode 100644 index 00000000..faf1a5c2 --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/where/generated_doc/libtensor.proof.html @@ -0,0 +1,67 @@ + + + + + +
library libtensor — proofsProvers
++ alt-ergo @2.5.4 n=16 215ms + cvc5 @1.2.1 n=42 489ms + z3 @4.13.4 n=30 140ms ++
Proofs
+module libtensor.CTensor+
+ value to_uint32 + value is_null + value f32 + value f64 + value (.+) + value (.-) + value (.-) + value (.*) + value (./) + value (.=) + value (.<) + value (.<=) ++
+ goal tensor + alt-ergo 29ms
+ goal tensorb + alt-ergo 33ms
+ goal ctensor_create + alt-ergo 40ms
+ goal ctensor_clear + alt-ergo 242ms
+ goal ctensor_reset + split_vc + alt-ergo 20ms + alt-ergo 27ms + alt-ergo 20ms + alt-ergo 19ms + alt-ergo 34ms + alt-ergo 46ms + alt-ergo 75ms + alt-ergo 27ms + alt-ergo 34ms
+ goal ctensor_where + split_vc + alt-ergo 24ms + alt-ergo 34ms + alt-ergo 24ms + alt-ergo 80ms + alt-ergo 81ms + alt-ergo 84ms + alt-ergo 25ms + alt-ergo 47ms + alt-ergo 82ms + alt-ergo 301ms + alt-ergo 28ms + alt-ergo 33ms+ + diff --git a/safety-related-profile/sonnx/ops/code/where/generated_doc/libvector.CIndex.html b/safety-related-profile/sonnx/ops/code/where/generated_doc/libvector.CIndex.html new file mode 100644 index 00000000..f0a09860 --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/where/generated_doc/libvector.CIndex.html @@ -0,0 +1,160 @@ + + + + + +
library libvector — module CIndex+module CIndex + use std.Int + use std.List + use std.Clib + use mach.int.Int32 + use tensor.Range + use layout.CFlat + + type iarray = ptr int32 + + function ivector (u : iarray) (n : int) : list int + = map Int32.to_int (vector u n) + + function islice (u : iarray) (p q : int) : list int + = map Int32.to_int (slice u p q) ++
+
+Dimensions
++ function vdim (u : iarray) (n : int) : int = size (ivector u n) + function sdim (u : iarray) (p q : int) : int = size (islice u p q) + + predicate pdim (u : iarray) (p q : int) = + forall k. p <= k < q -> 0 < value_at u k + + predicate dimension (u : iarray) (n : int) = + 0 <= n /\ valid_range u 0 n /\ pdim u 0 n /\ 0 < vdim u n <= max_int32 ++
+
+Equivalence betwen pdim and tensor.Range.positive.
+ let rec lemma positive_pdim (u : iarray) (p q : int) + {proof…} + ensures { pdim u p q <-> positive (islice u p q) } + variant { q - p } + = if p < q then positive_pdim u (p+1) q + {qed} + + let ghost sdim_split (u : iarray) (p k q : int) + {proof…} + requires { p <= k < q } + requires { pdim u p q } + ensures { sdim u p k * value_at u k * sdim u (k+1) q = sdim u p q } + = assert { islice u p k ++ islice u k q = islice u p q } + {qed} ++
+
+Extracted Library
++ let cdim_size (u : iarray) (n : int32): int32 = + ensures { result = vdim u n } + {proof…} + requires { dimension u n } + {qed} + begin + let ref p = 1 in + for i = 0 to n - 1 do + {proof…} + invariant { p = vdim u i } + ghost + begin + ensures { 1 <= p * u[i] <= max_int32 } + let ghost dl = pure { sdim u 0 i } in + let ghost di = Int32.to_int u[i] in + let ghost dr = pure { sdim u (i+1) n } in + let ghost dn = pure { sdim u 0 n } in + sdim_split u 0 (Int32.to_int i) (Int32.to_int n) ; + mult_bound (dl * di) dr dn ; + end ; + {qed} + p <- p * u[i] ; + done ; p + end + + let cdim_create_1 (n : int32) : iarray = + requires { 0 < n } + ensures { is_not_null result -> vdim result 1 = n } + {proof…} + ensures { is_not_null result -> dimension result 1 } + ensures { is_not_null result -> value_at result 0 = n } + {qed} + let cd = malloc 1 in + if is_not_null cd then cd[0] <- n ; cd + + let cdim_create_2 (p q : int32) : iarray = + requires { 0 < p /\ 0 < q /\ p * q <= max_int32 } + ensures { is_not_null result -> vdim result 2 = p * q } + {proof…} + ensures { is_not_null result -> dimension result 2 } + ensures { is_not_null result -> value_at result 0 = p } + ensures { is_not_null result -> value_at result 1 = q } + {qed} + let cd = malloc 2 in + if is_not_null cd then (cd[0] <- p ; cd[1] <- q) ; cd ++
+
+Coordinates
++ let coffset (ks : iarray) (ds : iarray) (n : int32) : int32 = + {proof…} + requires { 0 <= n } + requires { valid_range ks 0 n } + requires { dimension ds n } + ensures { 0 <= result -> valid (ivector ks n) (ivector ds n) } + ensures { 0 <= result -> result = offset (ivector ks n) (ivector ds n) } + {qed} + begin + let ref p = 0 in + for i = 0 to n - 1 do + {proof…} + invariant { valid (ivector ks i) (ivector ds i) } + invariant { p = offset (ivector ks i) (ivector ds i) } + {qed} + let d = ds[i] in + let k = ks[i] in + if 0 <= k && k < d then + begin + {proof…} + assert { p * d + k = offset (ivector ks (i+1)) (ivector ds (i+1)) } ; + ghost + begin + ensures { Int32.in_bounds (p * d) } + ensures { Int32.in_bounds (p * d + k) } + let ghost dl = pure { sdim ds 0 i } in + let ghost di = Int32.to_int ds[i] in + let ghost dr = pure { sdim ds (i+1) n } in + let ghost dn = pure { sdim ds 0 n } in + sdim_split ds 0 (Int32.to_int i) (Int32.to_int n) ; + mult_bound (dl * di) dr dn ; + end ; + {qed} + p <- p * d + k ; + end + else return (-1) + done ; p + end + +end ++ + + diff --git a/safety-related-profile/sonnx/ops/code/where/generated_doc/libvector.index.html b/safety-related-profile/sonnx/ops/code/where/generated_doc/libvector.index.html new file mode 100644 index 00000000..324ac9a4 --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/where/generated_doc/libvector.index.html @@ -0,0 +1,16 @@ + + + + + +
library libvector
+
+C–Library to compute Offsets & Dimensions
+module CIndex+ + + diff --git a/safety-related-profile/sonnx/ops/code/where/generated_doc/libvector.proof.html b/safety-related-profile/sonnx/ops/code/where/generated_doc/libvector.proof.html new file mode 100644 index 00000000..a1a27bc7 --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/where/generated_doc/libvector.proof.html @@ -0,0 +1,87 @@ + + + + + +
library libvector — proofsProvers
++ alt-ergo @2.5.4 n=16 171ms + cvc5 @1.2.1 n=42 492ms + z3 @4.13.4 n=33 865ms ++
Proofs
+module libvector.CIndex+
+ value to_uint32 + value is_null ++
+ goal positive_pdim + alt-ergo 69ms
+ goal sdim_split + alt-ergo 170ms
+ goal cdim_size + split_vc + alt-ergo 19ms + alt-ergo 22ms + alt-ergo 25ms + alt-ergo 17ms + alt-ergo 19ms + alt-ergo 35ms + alt-ergo 626ms + alt-ergo 24ms + alt-ergo 19ms + alt-ergo 126ms + alt-ergo 16ms + alt-ergo 14ms
+ goal cdim_create_1 + alt-ergo 158ms
+ goal cdim_create_2 + split_vc + alt-ergo 16ms + alt-ergo 13ms + alt-ergo 17ms + alt-ergo 17ms + alt-ergo 20ms + alt-ergo 262ms + alt-ergo 34ms + alt-ergo 23ms + alt-ergo 20ms + alt-ergo 16ms + alt-ergo 16ms + alt-ergo 15ms + alt-ergo 17ms
+ goal coffset + split_vc + alt-ergo 18ms + alt-ergo 24ms + alt-ergo 25ms + alt-ergo 24ms + alt-ergo 22ms + alt-ergo 835ms + alt-ergo 34ms + alt-ergo 18ms + alt-ergo 20ms + alt-ergo 65ms + alt-ergo 152ms + split_vc + inline_goal + split_vc + alt-ergo 28ms + stuck + alt-ergo 19ms + alt-ergo 18ms + alt-ergo 17ms + alt-ergo 902ms + alt-ergo 20ms + alt-ergo 17ms + alt-ergo 15ms + alt-ergo 18ms + alt-ergo 14ms + alt-ergo 16ms+ + diff --git a/safety-related-profile/sonnx/ops/code/where/generated_doc/script.js b/safety-related-profile/sonnx/ops/code/where/generated_doc/script.js new file mode 100644 index 00000000..9e1faafc --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/where/generated_doc/script.js @@ -0,0 +1,54 @@ +function toggle(elt) { + var elts,j; + while (elt && !elt.classList.contains("section")) { + elt = elt.parentElement; + } + if (!elt) return; + elts = elt.querySelectorAll(".section-text, .section-toggle"); + for (j = 0; j < elts.length; j++) + elts[j].classList.toggle("active"); +} + +function focus() { + var h,elts,e,tk,i; + h = window.location.hash; + e = document.getElementById(h.substring(1)); + while (e) { + tk = e.classList; + if (tk.contains("section-text") && !tk.contains("active")) { + toggle(e); + break; + } + e = e.parentElement; + } +} + +function escape(evt) { + var elts,e,i; + if (evt.code === "Escape") { + window.location = ""; + elts = document.querySelectorAll(".section"); + for (i=0; i< elts.length; i++) { + e = elts[i]; + if (e.querySelectorAll(".section-toggle.active").length) + toggle(e); + } + } +} + +(function(){ + var nodes,i; + + nodes = document.getElementsByClassName("section-toggle"); + for (i = 0; i < nodes.length; i++) { + nodes[i].addEventListener("click", function() { + toggle(this); + }); + } + + focus(); + window.addEventListener('onload',focus); + window.addEventListener('hashchange',focus); + window.addEventListener('keypress',escape); + +})(); diff --git a/safety-related-profile/sonnx/ops/code/where/generated_doc/std.Cfloat.html b/safety-related-profile/sonnx/ops/code/where/generated_doc/std.Cfloat.html new file mode 100644 index 00000000..f92b0ba0 --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/where/generated_doc/std.Cfloat.html @@ -0,0 +1,59 @@ + + + + + +
library std — module Cfloat+module Cfloat + use int.Int + use real.Real + + type float = abstract { to_real : real } + meta coercion function to_real + + type f32 = < float 8 24 > (* single precision literals *) + type f64 = < float 11 53 > (* double precision literals *) + + val function f32 (k : f32) : float + ensures { result = f32'real k } + + val function f64 (k : f64) : float + ensures { result = f64'real k } + + let constant zero = f64 0.0 + let constant one = f64 1.0 + + val function (.+) (a b : float) : float + ensures { Real.( result = a + b ) } + + val function (.-) (a b : float) : float + ensures { Real.( result = a - b ) } + + val function (.-_) (a : float) : float + ensures { Real.( result = (- a) ) } + + val function ( .* ) (a b : float) : float + ensures { Real.( result = a * b ) } + + val function ( ./ ) (a b : float) : float + requires { b <> 0.0 } + ensures { Real.( result = a / b ) } + + val predicate ( .= ) (a b : float) : bool + ensures { result <-> Real.( a = b ) } + + val predicate ( .< ) (a b : float) : bool + ensures { result <-> Real.( a < b ) } + + val predicate ( .<= ) (a b : float) : bool + ensures { result <-> Real.( a <= b ) } + +end ++ + + diff --git a/safety-related-profile/sonnx/ops/code/where/generated_doc/std.Clib.html b/safety-related-profile/sonnx/ops/code/where/generated_doc/std.Clib.html new file mode 100644 index 00000000..a1288577 --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/where/generated_doc/std.Clib.html @@ -0,0 +1,117 @@ + + + + + +
library std — module Clib+module Clib + use map.Map + use int.Int + use mach.int.Int32 + use export mach.c.C + + type int32 = Int32.int32 + type uint32 = UInt32.uint32 + + val function to_uint32 (v : int32) : uint32 + requires { 0 <= v } + ensures { Int32.to_int v = UInt32.to_int result } ++
+
+Null–Pointer
++ val predicate is_null (vp : ptr 'a) : bool + ensures { result <-> vp.zone = null_zone } ++
+
+Array–range validity
++ predicate valid_range (vp : ptr 'a) (p q : int) = + q <= p \/ + ( 0 <= vp.min <= vp.offset /\ + 0 <= p <= q <= max_int32 /\ + 0 <= vp.min <= vp.offset + p /\ + vp.offset + q <= vp.max <= vp.plength ) + + let lemma valid_in_range (vp : ptr 'a) (p k q : int) + {proof…} + requires { p <= k < q } + requires { valid_range vp p q } + ensures { valid_ptr_shift vp k } + = () + {qed} ++
+
+Array as map
++ let ghost function value_at (vp : ptr 'a) : map int 'a = + pure { fun k -> vp.data.Array.elts (vp.offset + k) } ++
+
+Array access (ghost)
++ function ([]) (vp : ptr 'a) (k : int) : 'a = value_at vp k ++
+
+Array access (C, inlined)
++ let ([]) (vp : ptr 'a) (k : int32) : 'a + {proof…} + requires { vp.min <= vp.offset + k < vp.max } + ensures { result = vp[k] } + = get_ofs vp k + {qed} ++
+
+Array update (C, inlined)
++ let ([]<-) (vp : ptr 'a) (k : int32) (v : 'a) : unit + requires { writable vp } + requires { vp.min <= vp.offset + k < vp.max } + ensures { value_at vp = Map.([<-]) (old (value_at vp)) k v } + = set_ofs vp k v ++
+
+Array as list
++ use List + + let rec ghost function slice (u : ptr 'a) (p q : int) : list 'a = + {proof…} + variant { q - p } + {qed} + if q <= p then Nil else Cons (value_at u p) (slice u (p+1) q) + + let rec lemma slice_append (u : ptr 'a) (p q r : int) + requires { p <= q <= r } + ensures { slice u p r = slice u p q ++ slice u q r } + {proof…} + variant { q - p } + = if p < q then slice_append u (p+1) q r + {qed} + + let ghost function vector (u : ptr 'a) (n : int) = slice u 0 n + + let lemma vector_push (u : ptr 'a) (n : int) + requires { 0 <= n } + ensures { vector u (n+1) = push (vector u n) (value_at u n) } + {proof…} + = slice_append u 0 n (n+1) + {qed} + +end ++ + + diff --git a/safety-related-profile/sonnx/ops/code/where/generated_doc/std.Int.html b/safety-related-profile/sonnx/ops/code/where/generated_doc/std.Int.html new file mode 100644 index 00000000..3ded1908 --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/where/generated_doc/std.Int.html @@ -0,0 +1,50 @@ + + + + + +
library std — module Int+module Int + use export int.Int + use export int.Abs + use export int.ComputerDivision ++
+
+Unicity of euclidian division decomposition
++ let ghost euclide (a b q r : int) + requires { 0 <= a /\ 0 <= r < q } + requires { a = b * q + r } + ensures { b = div a q } + ensures { r = mod a q } + {proof…} + = let rec kernel (b r : int) + requires { b * q + r = 0 } + requires { abs r < q } + ensures { b = r = 0 } + variant { abs b } + = if b < 0 then kernel (b + 1) (r - q) else + if b > 0 then kernel (b - 1) (r + q) else () + in kernel (b - div a q) (r - mod a q) + {qed} ++
+
+Multiplication upper–bound
++ let ghost mult_bound (a b c : int) + requires { 0 < a * b <= c } + ensures { abs a <= c } + ensures { abs b <= c } + = () + +end ++ + + diff --git a/safety-related-profile/sonnx/ops/code/where/generated_doc/std.List.html b/safety-related-profile/sonnx/ops/code/where/generated_doc/std.List.html new file mode 100644 index 00000000..13c07ac4 --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/where/generated_doc/std.List.html @@ -0,0 +1,34 @@ + + + + + +
library std — module List+module List + use export list.List + use export list.Map + use export list.Append ++
+
+Appends an element to the end of the list
++ function push (xs : list 'a) (x : 'a) : list 'a = + xs ++ Cons x Nil + + let rec lemma map_concat (f : 'a -> 'b) (xs ys : list 'a) + ensures { map f (xs ++ ys) = map f xs ++ map f ys } + {proof…} + variant { xs } + = match xs with Cons _ rxs -> map_concat f rxs ys | Nil -> () end + {qed} + +end ++ + + diff --git a/safety-related-profile/sonnx/ops/code/where/generated_doc/std.index.html b/safety-related-profile/sonnx/ops/code/where/generated_doc/std.index.html new file mode 100644 index 00000000..fe20174f --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/where/generated_doc/std.index.html @@ -0,0 +1,16 @@ + + + + + +
library stdmodule Int+
module List+
module Clib+
module Cfloat+ + + diff --git a/safety-related-profile/sonnx/ops/code/where/generated_doc/std.proof.html b/safety-related-profile/sonnx/ops/code/where/generated_doc/std.proof.html new file mode 100644 index 00000000..ceb91d5d --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/where/generated_doc/std.proof.html @@ -0,0 +1,63 @@ + + + + + +
library std — proofsProvers
++ alt-ergo @2.5.4 n=16 171ms + cvc5 @1.2.1 n=42 492ms + z3 @4.13.4 n=33 865ms ++
Proofs
+module std.Int+
+ goal euclide + alt-ergo 47ms
+ goal mult_bound + z3 6ms
module std.List+
+ goal map_concat + alt-ergo 18ms
module std.Clib+
+ value to_uint32 + value is_null ++
+ goal valid_in_range + alt-ergo 14ms
+ goal ([]) + alt-ergo 11ms
+ goal ([]) + alt-ergo 11ms
+ goal ([]<-) + alt-ergo 15ms
+ goal slice + alt-ergo 14ms
+ goal slice_append + alt-ergo 29ms
+ goal vector_push + z3 16ms
module std.Cfloat+
+ value f32 + value f64 + value (.+) + value (.-) + value (.-) + value (.*) + value (./) + value (.=) + value (.<) + value (.<=) ++
+ goal zero + split_vc
+ goal one + split_vc+ + diff --git a/safety-related-profile/sonnx/ops/code/where/generated_doc/style.css b/safety-related-profile/sonnx/ops/code/where/generated_doc/style.css new file mode 100644 index 00000000..1c6997e4 --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/where/generated_doc/style.css @@ -0,0 +1,138 @@ +/* -------------------------------------------------------------------------- */ +/* --- CSS Style Sheet for why3find doc generator --- */ +/* -------------------------------------------------------------------------- */ + +/* -------------------------------------------------------------------------- */ +/* --- Links --- */ +/* -------------------------------------------------------------------------- */ + +a { + color: teal; + outline: none; + text-decoration: none; +} + +a:visited { + color: teal; +} + +a:hover { + background: lightgreen; +} + +a:target { + background: lightblue; +} + +/* -------------------------------------------------------------------------- */ +/* --- Header Styling --- */ +/* -------------------------------------------------------------------------- */ + +header { + padding: 4px ; + color: darkgrey ; + border-bottom: thin solid darkgray ; +} + +header a { color: grey !important } + +/* -------------------------------------------------------------------------- */ +/* --- Table Of Contents --- */ +/* -------------------------------------------------------------------------- */ + +nav { display: none; } + +/* -------------------------------------------------------------------------- */ +/* --- Documentation Styling --- */ +/* -------------------------------------------------------------------------- */ + +div.doc { + /* Documentation block styling */ +} + +/* -------------------------------------------------------------------------- */ +/* --- Source Code Styling --- */ +/* -------------------------------------------------------------------------- */ + +pre.src { + /* Source code block styling */ +} + +.scope { + color: teal; +} + +.keyword { + color: purple; +} + +.admitted { + color: #DA2525; +} + +.attribute { + color: green; +} + +.comment { + color: grey; +} + +/* -------------------------------------------------------------------------- */ +/* --- Proof Marks --- */ +/* -------------------------------------------------------------------------- */ + +.icon { + margin-left: 2px ; + vertical-align: text-top ; + font-size: small ; + text-decoration: none ; +} + +.icon.small { font-size: x-small } + +.valid { color: green !important } +.failed { color: red !important } +.warning { color: orange !important } +.remark { color: lightgrey !important } +.prover:hover { color: purple } + +/* -------------------------------------------------------------------------- */ +/* --- Foldable Section --- */ +/* -------------------------------------------------------------------------- */ + +.section { } + +.section.level1:hover { + background: #fcfce1; +} + +.section.level2:hover { + background: #e9ffe9; +} + +.section.level3:hover { + background: #fff6f6; +} + +.section-toggle:hover { + background: lightgreen; +} + +.section-toggle { + cursor: zoom-in ; +} + +.section-toggle.active { + cursor: zoom-out ; +} + +.section-text { + display: none; +} + +.section-text.active { + display: inline; +} + +/* -------------------------------------------------------------------------- */ diff --git a/safety-related-profile/sonnx/ops/code/where/generated_doc/tensor.OPWhere.html b/safety-related-profile/sonnx/ops/code/where/generated_doc/tensor.OPWhere.html new file mode 100644 index 00000000..c3a52269 --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/where/generated_doc/tensor.OPWhere.html @@ -0,0 +1,34 @@ + + + + + +
library tensor — module OPWhere
+Module tensor.Range
+
+
+index —
+Module tensor.Tensor
+
+
+index —
+
+
+
+OP–Where Tensor Operation
++module OPWhere + use Tensor + + let ghost function dwhere (c : data bool) (a b : data 'a) : data 'a + = fun ks -> if c ks then a ks else b ks + + let ghost function opwhere (c : tensor bool) (a b : tensor 'a) : tensor 'a + requires { a ~= b } + requires { c ~ a ~ b } + ensures { result ~= a ~= b } + ensures { result = dwhere c a b } + {proof…} + = { dims = c.dims ; data = dwhere c.data a.data b.data ; background = a.background } + {qed} + +end ++ + + diff --git a/safety-related-profile/sonnx/ops/code/where/generated_doc/tensor.Range.html b/safety-related-profile/sonnx/ops/code/where/generated_doc/tensor.Range.html new file mode 100644 index 00000000..fb4549e2 --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/where/generated_doc/tensor.Range.html @@ -0,0 +1,80 @@ + + + + + +
library tensor — module Range+module Range + use int.Int + use std.List + + function size (ds : list int) : int = + match ds with + | Nil -> 1 + | Cons d ds -> d * size ds + end + + predicate positive (ds : list int) = + match ds with + | Nil -> true + | Cons d ds -> 0 < d /\ positive ds + end + + predicate valid (ks ds : list int) = + match ks , ds with + | Nil , Nil -> true + | Cons k ks , Cons d ds -> 0 <= k < d /\ valid ks ds + | _ -> false + end + + let rec lemma valid_push (ks ds : list int) (k d : int) + requires { 0 <= k < d } + requires { valid ks ds } + ensures { valid (push ks k) (push ds d) } + {proof…} + variant { ks } + = match ks , ds with + | Nil , Nil -> () + | Cons _ ks , Cons _ ds -> valid_push ks ds k d + | _ -> absurd + end + {qed} + + let rec lemma size_append (xs ys : list int) + ensures { size (xs ++ ys) = size xs * size ys } + {proof…} + variant { xs } + = match xs with Cons _ rxs -> size_append rxs ys | Nil -> () end + {qed} + + lemma size_push: forall xs x. size (push xs x) = size xs * x + + let rec lemma positive_size (ds : list int) + requires { positive ds } + ensures { 0 < size ds } + {proof…} + variant { ds } + = match ds with Nil -> () | Cons _ ds -> positive_size ds end + {qed} + + let rec lemma positive_valid (ks ds : list int) + requires { valid ks ds } + ensures { positive ds } + ensures { 0 < size ds } + {proof…} + variant { ds } + = match ks , ds with + | Cons _ ks , Cons _ ds -> positive_valid ks ds + | _ -> () + end + {qed} + +end ++ + + diff --git a/safety-related-profile/sonnx/ops/code/where/generated_doc/tensor.Tensor.html b/safety-related-profile/sonnx/ops/code/where/generated_doc/tensor.Tensor.html new file mode 100644 index 00000000..bc50c46d --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/where/generated_doc/tensor.Tensor.html @@ -0,0 +1,112 @@ + + + + + +
library tensor — module Tensor
+Library tensor
+
+
+index —
+
+
+
+Formalization of Tensor
++module Tensor + use int.Int + use map.Map + use list.List + use Range + + type data 'a = map (list int) 'a + + type tensor 'a = { + dims : list int ; + data : data 'a ; + background : 'a ; (* default value, or value for 0-dimensions tensor *) + } + invariant { positive dims } + invariant { forall k. valid k dims \/ data k = background } + {proof…} + by let d = any 'a in { dims = Nil ; data = (fun _ -> d) ; background = d } + {qed} + + meta coercion function dims + meta coercion function data ++
+
+Tensor with the same dimensions
++ predicate (~) (a : tensor 'a) (b : tensor 'b) = a.dims = b.dims ++
+
+Tensor with the same dimensions and background value
++ predicate (~=) (a : tensor 'a) (b : tensor 'a) = + a ~ b /\ a.background = b.background ++
+
+Equal tensors
++ predicate (==) (a b : tensor 'a) = + a ~= b /\ forall k. valid k a.dims -> a.data k = b.data k ++
+
+Extensionality
++ lemma exteq: forall a b : tensor 'a. a == b <-> a = b + {proof…} by tensor'eq a b {qed} ++
+
+Scalar Tensor
++ let ghost function scalar (v : 'a) : tensor 'a + ensures { result.dims = Nil } + ensures { result.background = v } + ensures { forall k. result k = v } + {proof…} + = { dims = Nil ; data = (fun _ -> v) ; background = v } + {qed} ++
+
+Null Tensor
++ let ghost function zero (e : 'a) (ds : list int) : tensor 'a + requires { positive ds } + ensures { result.dims = ds } + ensures { result.background = e } + ensures { forall k. result k = e } + {proof…} + = { dims = ds ; data = (fun _ -> e) ; background = e } + {qed} ++
+
+Constant Tensor
++ let ghost function const (v : 'a) (bg : 'a) (ds : list int): tensor 'a + ensures { result.dims = ds } + requires { positive ds } + ensures { result.background = bg } + ensures { forall k. valid k ds -> result k = v } + {proof…} + = { dims = ds ; data = pure { fun k -> if valid k ds then v else bg } ; background = bg } + {qed} ++
+
+Constant & Null
++ goal zero_is_const: forall e : 'a, ds. positive ds -> zero e ds == const e e ds + +end ++ + + diff --git a/safety-related-profile/sonnx/ops/code/where/generated_doc/tensor.index.html b/safety-related-profile/sonnx/ops/code/where/generated_doc/tensor.index.html new file mode 100644 index 00000000..8b3fe9a7 --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/where/generated_doc/tensor.index.html @@ -0,0 +1,20 @@ + + + + + +
library tensor
+
+Formalization of coordinates and dimensions
+module Range+
module Tensor+
module OPWhere+ + + diff --git a/safety-related-profile/sonnx/ops/code/where/generated_doc/tensor.proof.html b/safety-related-profile/sonnx/ops/code/where/generated_doc/tensor.proof.html new file mode 100644 index 00000000..9827c84c --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/where/generated_doc/tensor.proof.html @@ -0,0 +1,51 @@ + + + + + +
library tensor — proofsProvers
++ alt-ergo @2.5.4 n=16 171ms + cvc5 @1.2.1 n=42 489ms + z3 @4.13.4 n=30 140ms ++
Proofs
+module tensor.Range+
+ goal valid_push + alt-ergo 32ms
+ goal size_append + alt-ergo 28ms
+ goal size_push + alt-ergo 11ms
+ goal positive_size + alt-ergo 18ms
+ goal positive_valid + alt-ergo 29ms
module tensor.Tensor+
+ goal tensor + alt-ergo 12ms
+ goal exteq + split_vc + alt-ergo 13ms + alt-ergo 13ms + alt-ergo 13ms
+ goal scalar + alt-ergo 15ms
+ goal zero + alt-ergo 12ms
+ goal const + alt-ergo 17ms
+ goal zero_is_const + alt-ergo 12ms
module tensor.OPWhere+
+ goal dwhere + split_vc
+ goal opwhere + alt-ergo 15ms+ + diff --git a/safety-related-profile/sonnx/ops/code/where/generated_doc/where.CTensorWhere.html b/safety-related-profile/sonnx/ops/code/where/generated_doc/where.CTensorWhere.html new file mode 100644 index 00000000..578cd279 --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/where/generated_doc/where.CTensorWhere.html @@ -0,0 +1,58 @@ + + + + + +
library where — module CTensorWhere+module CTensorWhere + use tensor.std.Int + use tensor.std.List + use tensor.std.Clib + use tensor.std.Cfloat + use mach.int.Int32 + use tensor.tensor.Range + use tensor.tensor.Tensor + use OPWhere + use tensor.layout.CFlat + use tensor.libvector.CIndex + use tensor.libtensor.CTensor + + + +let ctensor_where (cond a b r : ctensor) = + {proof…} + requires { valid_tensor cond } + requires { valid_tensor a } + requires { valid_tensor b } + requires { valid_tensor r } + requires { tensor a ~= tensor b ~= tensor r } + {qed} + requires { tensorb cond ~ tensor a ~ tensor b } + ensures { tensor r = opwhere (tensorb cond) (tensor a) (tensor b) } + let m = cdim_size r.t_dims r.t_rank in + for i = 0 to m-1 do + {proof…} + invariant { + forall k. 0 <= k < i -> + value_at r.t_data k = + if Real.(0.0 < value_at cond.t_data k) + then a.t_data[k] else b.t_data[k] + } + {qed} + r.t_data[i] <- + if (f32 0.0) .< cond.t_data[i] then a.t_data[i] else b.t_data[i] + done + {proof…} + ; assert { tensor r == opwhere (tensorb cond) (tensor a) (tensor b) } + {qed} + + +end ++ + + diff --git a/safety-related-profile/sonnx/ops/code/where/generated_doc/where.OPWhere.html b/safety-related-profile/sonnx/ops/code/where/generated_doc/where.OPWhere.html new file mode 100644 index 00000000..b76d7899 --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/where/generated_doc/where.OPWhere.html @@ -0,0 +1,34 @@ + + + + + +
library where — module OPWhere
+Library where
+
+
+index —
+
+
+
+OP–Where Tensor Operation
++module OPWhere + use tensor.tensor.Tensor + + let ghost function dwhere (c : data bool) (a b : data 'a) : data 'a + = fun ks -> if c ks then a ks else b ks + + let ghost function opwhere (c : tensor bool) (a b : tensor 'a) : tensor 'a + requires { a ~= b } + requires { c ~ a ~ b } + ensures { result ~= a ~= b } + ensures { result = dwhere c a b } + {proof…} + = { dims = c.dims ; data = dwhere c.data a.data b.data ; background = a.background } + {qed} + +end ++ + + diff --git a/safety-related-profile/sonnx/ops/code/where/generated_doc/where.index.html b/safety-related-profile/sonnx/ops/code/where/generated_doc/where.index.html new file mode 100644 index 00000000..90f575f5 --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/where/generated_doc/where.index.html @@ -0,0 +1,15 @@ + + + + + +
library wheremodule OPWhere+
module CTensorWhere+ + + diff --git a/safety-related-profile/sonnx/ops/code/where/generated_doc/where.proof.html b/safety-related-profile/sonnx/ops/code/where/generated_doc/where.proof.html new file mode 100644 index 00000000..32d0c44c --- /dev/null +++ b/safety-related-profile/sonnx/ops/code/where/generated_doc/where.proof.html @@ -0,0 +1,39 @@ + + + + + +
library where — proofsProvers
++ alt-ergo @2.5.4 n=17 525ms + cvc5 @1.2.1 n=50 537ms + z3 @4.13.4 n=34 538ms ++
Proofs
+module where.OPWhere+
+ goal dwhere + alt-ergo 10ms
+ goal opwhere + alt-ergo 12ms
module where.CTensorWhere+
+ goal ctensor_where + split_vc + alt-ergo 15ms + alt-ergo 19ms + alt-ergo 13ms + alt-ergo 41ms + alt-ergo 42ms + alt-ergo 44ms + alt-ergo 14ms + alt-ergo 28ms + alt-ergo 52ms + alt-ergo 167ms + alt-ergo 18ms + alt-ergo 22ms+ + diff --git a/safety-related-profile/sonnx/ops/code/where/tests/README.md b/safety-related-profile/sonnx/ops/code/where/tests/README.md new file mode 100644 index 00000000..e69de29b diff --git a/safety-related-profile/sonnx/ops/docs/c_code_generation/why3_to_c.md b/safety-related-profile/sonnx/ops/docs/c_code_generation/why3_to_c.md new file mode 100644 index 00000000..2f4ad6e3 --- /dev/null +++ b/safety-related-profile/sonnx/ops/docs/c_code_generation/why3_to_c.md @@ -0,0 +1,152 @@ +# Converting Why3 Specifications to C Code + +This document outlines how to extract C code from Why3 (`.mlw`) specifications using the Why3 extraction mechanism and a C driver. It includes an example, supported features, and key constraints. + +## Compiling Why3 to C language +### Example + +This example defines a function `locate_max` that returns the index of the maximum element in an array `a` of size `n`. + +```whyml +use int.Int +use map.Map as Map +use mach.c.C +use mach.int.Int32 +use mach.int.Int64 + +function ([]) (a: ptr 'a) (i: int): 'a = Map.get a.data.Array.elts (a.offset + i) + +let locate_max (a: ptr int64) (n: int32): int32 + requires { 0 < n } + requires { valid a n } + ensures { 0 <= result < n } + ensures { forall i. 0 <= i < n -> a[i] <= a[result] } += let ref idx = 0 in + for j = 1 to n - 1 do + invariant { 0 <= idx < n } + invariant { forall i. 0 <= i < j -> a[i] <= a[idx] } + if get_ofs a idx < get_ofs a j then idx <- j + done; + idx + ``` + +### Extraction Command +```bash +why3 extract -D c locate_max.mlw +``` +With debug details: +```bash +why3 extract -D c --debug-all locate_max.mlw -o locate_max.c +``` +### Output C code +```c +#include
+ +--- + +
+ + +> (eric) General (detail) remark: use **bold** characters only when it is absolutely necessary. + +# Part 1 — Formalization Styles + +In SONNX, every operator is formalized at **two distinct levels**. + +Each level serves a different purpose and follows a different style. + +> (eric) I would also add that these two levels are a way to lower gradually the specification down to a level where it can be translated automatically into C code. Without this need, we could stick to the first level only. + +Understanding both is essential before writing any specification. + + +## 1.1 Abstract Formalization + +At this level the operator must be specified based only on its behavior and **mathematical semantics**. + +> I would rather say that the specification shall make "no" reference (or "carry") implementation constraints. Providing an algorithm as a specification could be considered as an implementation solution but it is not. The algorithm is only one possible way to implement the operator and the choice of the actual implementation is completely left to the implementer. + +It should the **as close as possible transalation** of the mathematical definition of the operator - **presented in the informal specification**, being therefore easy to read and understand. + +> (eric) The formal specification shall be traceable to the informal specification. Traceability must be enforced +> - first by keeping the formal specification as close to the informal specification (e.g., stick to the mathematical specification given in the informal specification) +> - second by providing explicit link via `[tags]` to specific parts of the informal specification. + +> (eric) "being easy to validate, first and easy to read and understand, second. +> Indeed, the translation from the informal specification to the formal specification cannot (yet) be performed automatically and will have to be checked manually. + +No implementation details should be present at this level, which means that the **tensor' representation** should **mimic the mathematical definition of a tensor** (also similar to the ONNX tensor concept) - a multidimensional array - in which each entry is accessed by its coordinates. + +> (eric) I am not sure that "mimic" is the appropriate word => "which means that the specification of tensors shall remain as abstract as possible, focusing on their mathematical properties. +> Nota that this may be arguable and (possibly) contradictory with the previous requirement about readability. Using arrays to represent tensors is something pretty familiar... Hopefully, wwe use "general indexes" in the informal spec that makes representing a tensor as a function from index to values pretty natural... + +### Tensor +> Tensor**s**? + +- **Type**: At this level tensors are said to be **polymorphic**.
+ +> (eroc) Maybe explain what you mean by "polymorphic", i.e., they must be parameterized by the type of the values "contained" in the tensor. +> (eric) They are not "said to be polymorphic", they **are** specified as polymorphic structures. + + This means that the specifier should be as generic as possible when defining an operator.
+ More details in - [2.5 - Operator tensor types](#25-operator-tensor-types). + +- **Representation**: Tensors are represented as structures containing the following records: + + - `dims` - List of integers representing the shape + + - `data` - A map from coordinates to values + +> (eric) In the informal specification, we use "[indexes](../../../spec/informal/common/definitions.md)" rather than "coordinates". + + - `background` - The default value for out-of-bounds coordinates + +> (eric) "for indexes out of the bounds defined by the shape"? + +- **Type Invariants**: There are two important invariants that must be satisfied by this tensor representatio: + +> (eric) "representation" (missing "n") + + 1. **Positive Dimensions** + + All dimensions in the `dims` list of a tensor must be positive integers.
+ +> (eric) You mean "strictly positive integers" (otherwise I don't understand the following remark). + +From our point of view this will be updated to support **non-negative integers**, therefore allowing for tensors with null dimensions. [***Work in Progress***] +> (eric) Maybe: "This constraint may be relaxed in a lated version of the specification to support tensors with null dimensions. + + **Definition:** + + - Predicate `positive` + + ```why3 + predicate positive (ds : list int) = + match ds with + | Nil -> true + | Cons d ds -> 0 < d /\ positive ds + end + ``` + - `invariant { positive dims }` + +> (eric) Stupid question : why `0 < d` rather than `d > 0`? + + 2. **Valid values** + + Coordinates are either valid for the tensor shape or the value mapped by those coordinates is the `background` value. + +> (eric) In the definition of the background value above, maybe use the term "valid index" since it is used here. +> +> (eric) A "valid index" is an index compatible with the dimension of the tensor, i.e. the i-th components of the index is strictly positive and strictly less than the i-th dimension of the tensor: + + **Definition:** + + - Predicate `valid` + + ```why3 + predicate valid (ks ds : list int) = + match ks , ds with + | Nil , Nil -> true + | Cons k ks , Cons d ds -> 0 <= k < d /\ valid ks ds + | _ -> false + end + ``` + - `invariant { forall k. valid k dims \/ data k = background }` + +
+ + These invariants are extremely important as they will sometimes define how the operator should be formalized. + + For example, while computing the data of the tensor it is **highly recommended** to use the predicate `valid`, essentially to capture and pass the invariant. + + > The previous sentence is a bit strange. Isn't this invariant a part of the specification of the tensor? + +### Specification Style + +Throughout this level, the specification should be carried out in a **purely functional style** meaning that there should be no side effects and no mutable state (functions do not modify state, they receive one as input and return a new one as output). + +Looping constructs are forbidden at this level, and instead, **recursive functions** and **mathematical constructs** should be used to define the behavior of the operator. + +> (eric) Again, this is not very compatible with the "principle" of simplicity and traceability stated earlier. May we should say something about "provability" or "ease of proof"? + +### Importance of this level + +It establishes the logical and mathematical specification of the operator, which serves as the **source of truth** for correctness. + +> (eric) why do you separate "logical" from "mathematical"? + +It also provides the perfect link between the informal specification and the formalization. + +## 1.2 Concrete Formalization + +The concrete level describes the **imperative implementation** that will be extracted to C code. + +> (eric) Stupid remark: Here, you use the work "imperative", as if the specification at the higher level was purely "declarative". But I feel that more often than not, our high-level specification are more "imperative" (they describe how to calculate something) than "declarative" (e.g., they describe the post-condition to be verified). + +It describes it based on a **target C representation** for tensors called **ctensors** which are essentially structures backed by flat arrays in memory. + +### Tensor + +- **Type**: At this level the type of tensor elements is fixed to be `float32`, `float64`, `int32`, `int64`, etc..., and the operator should be defined specifically for that type. + +>(eric) "etc." + +- **Representation**: Tensors are represented as pointers to structures that contain: + + - `t_rank`: Number of dimensions + + - `t_dims`: Pointer to a flat array containing the tensor dimensions - pointer to `int32` array + + - `t_data`: Pointer to a flat array containing the tensor elements - pointer to `type` array (where type is `float32`, `float64`, `int32`, `int64`, ...) + +
+ +Note that, unlike the previous level, here the tensors are defined based on a concrete target representation - tensors are essentially flat arrays in memory. + +Moreover, there is no `background` value in this representation - **tensors entries must be accessed only in valid coordinates** (i.e., coordinates that are within the bounds of the tensor shape). + +> (eric) "only valid indexes must be used to access values of tensors" + +### Specification Style + +Throughout this level, the specification should be carried out in an **imperative style** meaning that **loops and mutable state** are allowed and often necessary to express the implementation. + +>(eric) "In this level..." + +### Importance of this level + +It provides the necessary details to extract executable C code and reason about memory, bounds, and machine integers. + +> (eric) To be consistent with what follows: "integers" => "data types" + +## 1.3 Link between the two levels + +### Why is it important to have two levels? + +- We need somehow to express that the **concrete implementation** is correct with respect to the **operator's intended behavior** - which is captured by the **abstract specification**. + +>(eric) "concrete implementation" or "concrete specification"? + +- The abstract spec is easy to **read, understand, and reason about** — it directly mirrors the mathematical definition from its informal specification. + +- The concrete spec is necessary to **extract executable C code** and reason about memory, bounds, and machine datatypes. + +- The two levels are connected through a **refinement relationship**. The concrete implementation must be proven to produce the same result as the abstract specification. + +The following image gives a high-level overview of the relationship between the two levels and how they connect through refinement: + + + +
+ 
+
+ + +# Part 2 — Guidelines for Abstract Formalization + +## 2.1. Module Structure + +Each abstract module should follow this general structure: + + +``` +module OP
+ +The code written above will not generate any verification conditions, even if the functions called inside it explicitly need **requires clauses**. + +> (eric) Maybe the word "called" is a bit misleading. As far as I understand, When a function is referred to in a pure logical function, as it is a definition, it only refers to the contract of the "called" function (pre, post) which define the function, but not describe how it behaves. + +Therefore, no verification condtions were raised and the function `calculate_dims` does not appear on the Verification Conditions menu (left pannel in the picture above). + +> (eric) "condtions" => "conditions", "pannel" => "panel". + +### 2.2.3 TypeInvariant Lemmas + +When using `let rec function` declarations, their logical context sometimes does not propagate to subsequent functions, or it may appear only in axiomatic form. + +> (eric) I am not sure to understand what you mean by "it may appear only...". + +As a consequence, proving the type invariants of tensors — in particular, ensuring that the output dimensions satisfy the positivity invariant — requires explicit lemmas that establish these properties. + +The `calculate_dY0` function defined above is a concrete example of this issue. + +The following lemma is needed to guarantee that the result produced by `calculate_dY0` is strictly positive: + +```why3 + let rec lemma calculate_dY0_positive (x: tensor real) (axis: int) (i: int) + requires { positive x.dims } + requires { 0 <= axis <= length x.dims } + requires { 0 <= i <= axis } + ensures { 0 < calculate_dY0 x axis i } + variant { axis - i } + = + if i >= axis then + () + else + let d = get_dim x.dims i in + calculate_dY0_positive x axis (i + 1) +``` + +The different kinds of lemmas and how to use them will be covered in section [3.4](#34-invariants), [4.2](#42-ide-transformations-and-prover-hints). + +### 2.2.4 Main Operator Function + +Moreover, the main operator function cannot be declared as `function` because it needs to have contracts (`requires` / `ensures`) and `function` does not support contracts. + +>(eric) Again, I feel as if we were presenting the problem the other way round : what we are specifying is an algorithm to compute the operator because we want to generate code. So, as we are dealing with an algorithm and not a pure logical definition, what we specify is a "let [rec) function."... +> (eric) But I am not sure why we use a ghost function for an operator since we want to generate code out of it. + +Therefore, the main operator function should be declared as `let ghost function` with full contracts. + +```why3 +module OPSummation + use int.Int + + let rec function summation (i : int) (iter : int) : int = + variant { iter - i} + if i < iter then + 1 + summation (i + 1) iter + else + 0 + + let ghost function unitSum (n: int) : int = + requires { n >= 0 } + ensures { result = n } + summation 0 n +end +``` + +### 2.2.5 Guidelines + +| Guideline | Details | +|:---|:---| +| Use `function` for total functions and whenever it is possible! | A `function` is a logical function. | +| Use `let rec function` only when recursion needs a variant. | If Why3 cannot prove termination of a `function`, switch to `let rec function` and provide a `variant` clause. | +| Use `let ghost function` for the **main operator**. | The main function should be a `let ghost function` with full contracts (`requires` / `ensures`). | + +>(eric) I think that we should discuss those "guidelines" because I feel as if we were presenting things in the "wrong direction"... + +### Examples + +Besides the summation example above, here are some examples of such formalization styles: + +- **Clip**: [Clip abstract specification](./examples/clip.mlw) + +- **MatMul**: [MatMul abstract specification](./examples/matmul.mlw) + +## 2.3. Contracts on the Main Function + +Until now, we have stated that no function should have contracts except for the `main function` or any other function declared with `let rec`. + +The `main function`, **must** include as preconditions (`requires`) all the necessary constraints that are present in the informal specification for the inputs and the attributes. Output constraints (such as shape) will not be included at this point. + +On the other hand, the postconditions (`ensures`) of the main operator function **must** include the following three postconditions: + +| Postcondition | Purpose | +|:---|:---| +| `ensures { result.dims = ... }` | Specifies the **output shape** | +| `ensures { result.data = ... }` | Specifies the **output data** (as a map) | +| `ensures { result.background = ... }` | Specifies the **background value** | + +### Example + +```why3 +let ghost function opclip (x l m : tensor real) : tensor real + requires { is_scalar_tensor l } + requires { is_scalar_tensor m } + ensures { result.dims = x.dims } (* ← shape *) + ensures { result.data = dclip x l m } (* ← data *) + ensures { result.background = x.background } (* ← background *) += + { dims = x.dims; data = dclip x l m; background = x.background } +``` + +## 2.4. Data Function Pattern + +Whenever we want to specify the operator along all possible coordinates we can follow any of the following pattern: + +> (eric) I am HERE. + +### Anonymous function declaration + +Create an **anonymous function** for the data that takes the coordinates as input and defines the value at those coordinates based on the operator's semantics. + +We are basically stating that for all possible coordinates, the value at those coordinates is defined by this function. + +Note that, **not all coordinates are valid**, so we need to **check the validity of the coordinates** first and **return the background value for invalid coordinates**. + +That's why we need to compute the output shape, prior to this computation, as proposed in the [previous section](#file-structure-proposal). + +```why3 +let ghost function d
+ +Unlike, the previous examples, this operator is defined for tensors with a polymorphic datatype `'a`. + +Once for clip and matmul we need to compute values, there is no other option but to have an abstract datatype which is in fact **numerical**. + +Nevertheless, **where** doesn´t resort to any mathematical handling whatsoever and that's why its abstract datatype can be polymorphic. + +So whenever possible one should resort to **polymorphic** abstract datatypes. + +This is the case for the vast majority of the structural operators: **flatten**, **reshape**, among others. + + +# Part 3 — Guidelines for Concrete Formalization + +## 3.1. Module Structure + +The concrete module should follow this general structure: + +```why3 + module COP
+Equivalent to what is presented in the image [here](#refinement-mapping) + +To better understand this, check the `coords_from_X_p` function, presented in the [conv](./examples/conv.mlw): + +```why3 + (* Abstract level *) + function coords_from_X_p (x: tensor real) (x_p_coords : list int) ( pad_top pad_left :int) : real + = + let b = get_dim x_p_coords 0 in + let c = get_dim x_p_coords 1 in + let n = (get_dim x_p_coords 2) - pad_top in + let m = (get_dim x_p_coords 3) - pad_left in + let x_coords = Cons b (Cons c (Cons n (Cons m Nil))) in + if valid x_coords x.dims then + x.data x_coords + else + 0.0 +``` + +```why3 + (* Concrete level *) + let coords_from_X_p (x: ctensor) (x_p_coords : iarray) ( pad_top pad_left :int32) : (float, bool) = + requires { valid_tensor x } + requires { x.t_rank = 4 } + requires { valid_range x_p_coords 0 4 } + requires { writable x_p_coords } + requires { in_bounds (value_at x_p_coords 2 - pad_top) } + requires { in_bounds (value_at x_p_coords 3 - pad_left) } + + ensures { let (value, flag) = result in + flag -> coords_from_X_p (tensor x) (ivector x_p_coords 4) (to_int pad_top) (to_int pad_left) = value + } + + let ref flag = False in + let b = x_p_coords[0] in + let c = x_p_coords[1] in + let n = (x_p_coords[2]) - pad_top in + let m = (x_p_coords[3]) - pad_left in + let x_coords_array = malloc (to_uint32 4) in + if is_not_null x_coords_array then begin + flag <- True; + x_coords_array[0] <- b; + x_coords_array[1] <- c; + x_coords_array[2] <- n; + x_coords_array[3] <- m; + + assert { ivector x_coords_array 4 = Cons (to_int b) (Cons (to_int c) (Cons (to_int n) (Cons (to_int m) Nil))) } ; + + let x_coords = coffset x_coords_array x.t_dims x.t_rank in + if x_coords >= 0 then begin + (x.t_data[x_coords], flag) + end + else begin + ((f32 0.0), flag) + end + end + else begin + flag <- False; + ((f32 0.0), flag) + end +``` + +These two functions perform the same exact computation. + +To better understand how these two relate one can compare both specifications: + +**Coordinates** + +- On the **abstract side** the indices of the coordinates are captured with the `get_dim` function while on the **concrete level** the indices are captured by directly accessing the `iarray` with the `[]` operator. + + - These functions are equivalent and such equivalence proof is already available in the tensors library + +- To define the whole coordinates, on the **abstract side**, we only need a **list constructor**. On the **concrete level** such process is performed in two distinct steps: + + - **Firstly**, the appropriate space is allocated with the `malloc` function + + - **If the malloc is successful**, we then set each index of the array with the appropriate value. + + - Once again an equivalence must be established between these two constructs. That's exactly what is performed by the `assert` clause. + +**Computation** + +- On the **abstract side** we perform the computation by checking the validity of the coordinates on the dimensions of tensor x using the predicate **valid**. If the coordinates are valid we are going to return the value that is on that coordinates, else we are going to return 0. + +- On the **concrete side** we perform the computation by calculating the flatindex, of the coordinates on the tensor x dimensions, if the flatindex is a valid index, then we return the value on that index, else we are going to return 0. + +- The equivalence is captured by the postcondition present on the `coffset` function and the `if clause` which follows the same pattern at both levels. + +**Refinement mapping** + +- The refinement mapping relation is expressed with an ensures. In this function this realtion is expressed by: + + ``` + ensures { let (value, flag) = result in + flag -> coords_from_X_p (tensor x) (ivector x_p_coords 4) (to_int pad_top) (to_int pad_left) = value + } + ``` + +- This is the most important relation between both levels, as it states the values returned by both functions are exactly the same. Ultimately this prove that the function specified at the concrete level is correct with respect to the expected one presented at the abstract level, therefore ensuring that the behavior is the same at both levels. + +- Note that, in the concrete level, we need to explicitly check that the `malloc` was successful and return a flag indicating whether the coordinates were successfully computed or not. This is not necessary on the abstract level because we are working with mathematical constructs and we can assume that such constructs are always successfully created. + +### 3.3 Main operator function + +This is naturally the most important function and the one whith more details to be taken into account. + +#### 3.3.1 Contracts + +The **main operator function** must include contracts at both levels. + +**Requires** + +- On the **abstract level** the preconditions should include `requires` for all the necessary constraints that are present in the informal specification for the inputs and the attributes. Output constraints (such as shape) will not be included at this point. + +- On the **concrete level** we should have preconditions for: + + 1. Expressing the **validity of the input tensors**. At this level the tensors are passed as arguments and therefore we need to evalute whether they are **valid tensor** + + 2. Verify if the output tensor (already passed as an argument) has the appropriate shape, computed with the abstract function with such objective. Such verification should be performed by checking the dimensions of the output tensor with the dimensions computed by the abstract function. Moreover, we should also check that the output tensor has the appropriate **rank**. + + 3. All the **preconditions** already present at the abstract level. The **concrete** will essentially have the exact same copy of the abstract preconditions but adapted to the concrete level (the way the accesses are performed for instance will change). + +**Ensures** + +- On the **abstract level** the postconditions should cover each record of the abstract tensor - **dimensions**, **data** and **background**: + +- On the **concrete level** the only needed clause is the refinement mapping, indicating that the concrete implementation is correct with respect to the abstract specification. This is usually expressed by a postcondition of the form: + + - `ensures { tensor result =
+ +--- + +
+ +# Part 1 — Formalization Styles + +In SONNX, every operator must be formalized at two distinct levels: abstract formalization and concrete formalization. + +Each level serves a different purpose and follows a different style. + +We start from an abstract formalization — which captures the mathematical semantics of the operator and serves as the **source of truth** for correctness — and progressively refine it into a concrete formalization that is close enough to the target implementation to be automatically extracted into C code - reasoning about memory, bounds, and machine data types. + +Understanding both is essential before writing any specification. + +## 1.1 Abstract Formalization + +At this level the operator must be specified making no reference to any implementation detail, and therefore it should be **implementation-agnostic**. + +It shall be **traceable** to the **informal specification**, being easy to validate, first and easy to read and understand, second. ==add link to informal spec== Traceability must be enforced: + +- first by keeping the formal specification as close to the informal specification (e.g., stick to the mathematical specification given in the informal specification) + +- second by providing explicit link via `[tags]` to specific parts of the informal specification. + +No implementation details should be present at this level, which means that the specification of tensors shall remain as abstract as possible, focusing on their mathematical properties. + +### Tensors + +- **Type**: At this level tensors are specified as **polymorphic structures**, i.e., they are parameterized by the type of the values they contain.
+ This means that the specification author should be as generic as possible when defining an operator.
+ More details in - [2.5 - Operator tensor types](#25-operator-tensor-types). + +- **Representation**: Tensors are represented as structures containing the following records: + + - `dims` - List of integers representing the shape + + - `data` - A map from [indexes](../../../spec/informal/common/definitions.md) to values + + - `background` - The default value for indexes out of the bounds defined by the shape + + A "valid index" is an index compatible with the dimension of the tensor, i.e. the i-th components of the index is strictly positive and strictly less than the i-th dimension of the tensor + + The data mapping is complete since it maps all possible indexes to values, but the value mapped by invalid indexes is the `background` value. + +- **Type Invariants**: There are two important invariants that must be satisfied by this tensor representation: + + 1. **Positive Dimensions** + + All dimensions in the `dims` list of a tensor must be **strictly positive integers**.
+ This constraint may be relaxed in a lated version of the specification to support tensors with **null** dimensions. [***Work in Progress***] + + - Predicate `positive` + + ```why3 + predicate positive (ds : list int) = + match ds with + | Nil -> true + | Cons d ds -> 0 < d /\ positive ds + end + ``` + - `invariant { positive dims }` + + 2. **Valid values** + + Indexes are either valid for the tensor shape or the value mapped by those indexes is the `background` value. + + - Predicate `valid` ==the code below returns true for an empty index access to an empty tensor. This will be a problem when we introduce null tensors== + + ```why3 + predicate valid (ks ds : list int) = + match ks , ds with + | Nil , Nil -> true + | Cons k ks , Cons d ds -> 0 <= k < d /\ valid ks ds + | _ -> false + end + ``` + - `invariant { forall k. valid k dims \/ data k = background }` + +
+ + These invariants are extremely important as they will sometimes define how the operator should be formalized. + + For example, while computing the data of the tensor it is **highly recommended** to use the predicate `valid`, essentially to capture and pass the invariant. + + An alternative was to define the data through recursive definitions once the shape is already computed, but this approach is much more complex and usually requires auxiliary lemmas to help the proof. ==This sentence is a bit obscure for the casual reader. If the message is important, and it might be as it seems to contain a recommendation on how to do things, I suggest expanding the explanation to two-three sentences== + + The above predicates and invariants are available in the [tensors library](../../../spec/formal/common/libs/tensor/). + +### Specification Style + +Throughout this level, the specification should be carried out in a **purely functional style** meaning that there should be no side effects and no mutable state (functions do not modify state, they receive one as input and return a new one as output). + +Users should specify the operator based on mathematically and recursive definitions, avoiding loops and mutable state, increasing the **provability** and **ease of proof** of this specification. + +## 1.2 Concrete Formalization + +The concrete level describes the **imperative implementation** that will be extracted to C code. + +It describes it based on a **target C representation** for tensors called **ctensors** which are essentially structures backed by flat arrays in memory. + +### Tensors + +- **Type**: At this level the type of tensor elements is fixed to be `float32`, `float64`, `int32`, `int64`, etc. and the operator should be defined specifically for that type. + +- **Representation**: Tensors are represented as pointers to structures that contain: + + - `t_rank`: Number of dimensions + + - `t_dims`: Pointer to a flat array containing the tensor dimensions - pointer to `int32` array ==What happens if the tensor dimension (or number of dimensions) is larger that the max value of int32? It is a ridicolous case in practice, but may happen in a cybersec attack scenario== + + - `t_data`: Pointer to a flat array containing the tensor elements - pointer to `type` array (where type is `float32`, `float64`, `int32`, `int64`, ...) + +
+ +Note that, unlike the previous level, here the tensors are defined based on a target C representation - tensors are essentially flat arrays in memory. + +Moreover, there is no `background` value in this representation - **only valid indexes must be used to access values of tensors** (i.e. coordinates that are within the bounds of the tensor shape).==Any rationale behind this choice, e.g. computational efficiency? What happens if we try to access an invalid index? Do we guarantee that it can never happen?== + +### Specification Style + +In this level, the specification should be carried out in an **imperative style** meaning that **loops and mutable state** are allowed and often necessary to express the implementation. + +### Importance of this level + +It provides the necessary details to extract executable C code and reason about memory, bounds, and machine data types. + +## 1.3 Link between the two levels + +### Why is it important to have two levels? + +- We need somehow to express that the **concrete specification** is correct with respect to the **operator's intended behavior** - which is captured by the **abstract specification**. + +- The abstract spec is easy to **read, understand, and reason about** — it directly mirrors the mathematical definition from its informal specification. + +- The concrete spec is necessary to **extract executable C code** and reason about memory, bounds, and machine datatypes. + +- The two levels are connected through a **refinement relationship**. The concrete implementation must be proven to produce the same result as the abstract specification. ==Maybe "same result" is a little strong, especially regarding numerical error with floating point. I can easily see how the abstract specification defines a set of possible correct executions, and the concrete specification chooses only one (or a small subset of them)== + +The following image gives a high-level overview of the relationship between the two levels and how they connect through refinement: + + + +
+
+
+ +# Part 2 — Guidelines for Abstract Formalization + +## 2.1. Module Structure + +Each abstract module should follow this general structure: + + +``` +module OP
+ +The code written above will not generate any verification conditions, even if the functions referenced inside it explicitly need **requires clauses**. + +Therefore, no verification conditions were raised and the function `calculate_dims` does not appear on the Verification Conditions menu (left panel in the picture above). + +### 2.2.3 TypeInvariant Lemmas + +When using `let rec function` declarations, their logical context sometimes does not propagate to subsequent functions, or it may appear only in axiomatic form.=="sometimes" is a worryingly ambiguous thing to read in a guideline document. If it is well-known Why3 behaviour, add a link to further documentation== + +As a consequence, proving the type invariants of tensors — in particular, ensuring that the output dimensions satisfy the positivity invariant — requires explicit lemmas that establish these properties.==Do we have a strict requirement that type invariants must be proven? Where is it listed? Add reference to relevant doc.== + +The `calculate_dY0` function defined above is a concrete example of this issue. + +The following lemma is needed to guarantee that the result produced by `calculate_dY0` is strictly positive: + +```why3 + let rec lemma calculate_dY0_positive (x: tensor real) (axis: int) (i: int) + requires { positive x.dims } + requires { 0 <= axis <= length x.dims } + requires { 0 <= i <= axis } + ensures { 0 < calculate_dY0 x axis i } + variant { axis - i } + = + if i >= axis then + () + else + let d = get_dim x.dims i in + calculate_dY0_positive x axis (i + 1) +``` + +The different kinds of lemmas and how to use them will be covered in section [3.4](#34-invariants), [4.2](#42-ide-transformations-and-prover-hints). + +### 2.2.4 Main Operator Function + +To enforce traceability, as [previously mentioned](#traceability), the main operator function should capture the constraints present in the informal specification as preconditions (`requires`) while providing postconditions (`ensures`) for every record of the output tensor. + +To capture such contracts one needs to define a construct that belongs to the programming namespace. ==Does it mean we have to do this only for the concrete spec? The guidelines above explicitly state that we should use the logical namespace for the abstract spec...== Moreover, since this function is only used to specification purposes it is not supposed to be used in any implementation context. To enforce that this function can only be used at the logical level sign it as **ghost**.==To quote the beginning of Section 2.2 "at the abstract level we should only declare function with the signature function and no contracts should be used." But the rest of Section 2 seems to implicitly stress that contracts are _very important_, which is confusing== + +Therefore, the main operator function should be declared as `let rec ghost function` with full contracts. + +```why3 +module OPSummation + use int.Int + + let rec ghost function summation (i : int) (iter : int) : int = + variant { iter - i} + if i < iter then + 1 + summation (i + 1) iter + else + 0 + + let ghost function unitSum (n: int) : int = + requires { n >= 0 } + ensures { result = n } + summation 0 n +end +``` + +### Examples + +Besides the summation example above, here are some examples of such formalization styles: + +- **Clip**: [Clip abstract specification](./examples/clip.mlw) + +- **MatMul**: [MatMul abstract specification](./examples/matmul.mlw) + +## 2.3. Contracts on the Main Function + +Until now, we have stated that no function should have contracts except for the `main function` or any other function declared with `let rec ghost function`. ==This is the first time you state this requirement. Indeed, in Sections 2.2.2 and 2.2.3 many examples of non-main functions containing the require keyword are given== + +The `main function`, **must** include as preconditions (`requires`) all the necessary constraints that are present in the informal specification for the inputs and the attributes. Output constraints (such as shape) will not be included at this point. + +On the other hand, the postconditions (`ensures`) of the main operator function **must** include the following three postconditions:==You literally just said "output constraints (such as shape) will NOT be included". This is extremely contradictory== + +| Postcondition | Purpose | +|:---|:---| +| `ensures { result.dims = ... }` | Specifies the **output shape** | +| `ensures { result.data = ... }` | Specifies the **output data** (as a map) | +| `ensures { result.background = ... }` | Specifies the **background value** | + +### Example + +```why3 +let ghost function opclip (x l m : tensor real) : tensor real + requires { is_scalar_tensor l } + requires { is_scalar_tensor m } + ensures { result.dims = x.dims } (* ← shape *) + ensures { result.data = dclip x l m } (* ← data *) + ensures { result.background = x.background } (* ← background *) += + { dims = x.dims; data = dclip x l m; background = x.background } +``` + +## 2.4. Data Function Pattern + +Whenever we want to specify the operator along all possible coordinates we can follow any of the following pattern==s==: + + +### Anonymous function declaration + +Create an **anonymous function** for the data that takes the coordinates as input and defines the value at those coordinates based on the operator's semantics. + +We are basically stating that for all possible coordinates, the value at those coordinates is defined by this function. + +Note that, **not all coordinates are valid**, so we need to **check the validity of the coordinates** first and **return the background value for invalid coordinates**. + +That's why we need to compute the output shape, prior to this computation, as proposed in the [previous section](#file-structure-proposal).==I see what you mean, but the section you link only gives the order in which functions should be declared in the code, which (as far as I understand the semantic of Why3) has no influence on the order of computation.== + +```why3 +let ghost function d
+ +Unlike, the previous examples, this operator is defined for tensors with a polymorphic datatype `'a`. + +Once for clip and matmul we need to compute values, there is no other option but to have an abstract datatype which is in fact **numerical**. + +Nevertheless, **where** doesn´t resort to any mathematical handling whatsoever and that's why its abstract datatype can be polymorphic. + +So whenever possible one should resort to **polymorphic** abstract datatypes. + +This is the case for the vast majority of the structural operators: **flatten**, **reshape**, among others. + + +# Part 3 — Guidelines for Concrete Formalization + +## 3.1. Module Structure + +The concrete module should follow this general structure: + +```why3 + module COP
+Equivalent to what is presented in the image [here](#refinement-mapping) + +To better understand this, check the `coords_from_X_p` function, presented in the [conv](./examples/conv.mlw): + +```why3 + (* Abstract level *) + function coords_from_X_p (x: tensor real) (x_p_coords : list int) ( pad_top pad_left :int) : real + = + let b = get_dim x_p_coords 0 in + let c = get_dim x_p_coords 1 in + let n = (get_dim x_p_coords 2) - pad_top in + let m = (get_dim x_p_coords 3) - pad_left in + let x_coords = Cons b (Cons c (Cons n (Cons m Nil))) in + if valid x_coords x.dims then + x.data x_coords + else + 0.0 +``` + +```why3 + (* Concrete level *) + let coords_from_X_p (x: ctensor) (x_p_coords : iarray) ( pad_top pad_left :int32) : (float, bool) = + requires { valid_tensor x } + requires { x.t_rank = 4 } + requires { valid_range x_p_coords 0 4 } + requires { writable x_p_coords } + requires { in_bounds (value_at x_p_coords 2 - pad_top) } + requires { in_bounds (value_at x_p_coords 3 - pad_left) } + + ensures { let (value, flag) = result in + flag -> coords_from_X_p (tensor x) (ivector x_p_coords 4) (to_int pad_top) (to_int pad_left) = value + } + + let ref flag = False in + let b = x_p_coords[0] in + let c = x_p_coords[1] in + let n = (x_p_coords[2]) - pad_top in + let m = (x_p_coords[3]) - pad_left in + let x_coords_array = malloc (to_uint32 4) in + if is_not_null x_coords_array then begin + flag <- True; + x_coords_array[0] <- b; + x_coords_array[1] <- c; + x_coords_array[2] <- n; + x_coords_array[3] <- m; + + assert { ivector x_coords_array 4 = Cons (to_int b) (Cons (to_int c) (Cons (to_int n) (Cons (to_int m) Nil))) } ; + + let x_coords = coffset x_coords_array x.t_dims x.t_rank in + if x_coords >= 0 then begin + (x.t_data[x_coords], flag) + end + else begin + ((f32 0.0), flag) + end + end + else begin + flag <- False; + ((f32 0.0), flag) + end +``` + +These two functions perform the same exact computation. + +To better understand how these two relate one can compare both specifications: + +**Coordinates** + +- On the **abstract side** the indices of the coordinates are captured with the `get_dim` function while on the **concrete level** the indices are captured by directly accessing the `iarray` with the `[]` operator. + + - These functions are equivalent and such equivalence proof is already available in the tensors library + +- To define the whole coordinates, on the **abstract side**, we only need a **list constructor**. On the **concrete level** such process is performed in two distinct steps: + + - **Firstly**, the appropriate space is allocated with the `malloc` function + + - **If the malloc is successful**, we then set each index of the array with the appropriate value. + + - Once again an equivalence must be established between these two constructs. That's exactly what is performed by the `assert` clause. + +**Computation** + +- On the **abstract side** we perform the computation by checking the validity of the coordinates on the dimensions of tensor x using the predicate **valid**. If the coordinates are valid we are going to return the value that is on that coordinates, else we are going to return 0.==Aren't we supposed to return the background value, rather than 0?== + +- On the **concrete side** we perform the computation by calculating the flatindex, of the coordinates on the tensor x dimensions, if the flatindex is a valid index, then we return the value on that index, else we are going to return 0. + +- The equivalence is captured by the postcondition present on the `coffset` function and the `if clause` which follows the same pattern at both levels.==there is no postcondition on the coffset function in the code above== + +**Refinement mapping** + +- The refinement mapping relation is expressed with an ensures. In this function this ==relation== is expressed by: + + ``` + ensures { let (value, flag) = result in + flag -> coords_from_X_p (tensor x) (ivector x_p_coords 4) (to_int pad_top) (to_int pad_left) = value + } + ``` + +- This is the most important relation between both levels, as it states the values returned by both functions are exactly the same. Ultimately this prove that the function specified at the concrete level is correct with respect to the expected one presented at the abstract level, therefore ensuring that the behavior is the same at both levels. + +- Note that, in the concrete level, we need to explicitly check that the `malloc` was successful and return a flag indicating whether the coordinates were successfully computed or not. This is not necessary on the abstract level because we are working with mathematical constructs and we can assume that such constructs are always successfully created. + +### 3.3 Main operator function + +This is naturally the most important function and the one whith more details to be taken into account. + +#### 3.3.1 Contracts + +The **main operator function** must include contracts at both levels. + +**Requires** + +- On the **abstract level** the preconditions should include `requires` for all the necessary constraints that are present in the informal specification for the inputs and the attributes. Output constraints (such as shape) will not be included at this point.==the guidelines for the abstract specification are covered in Section 2, do not repeat them here== + +- On the **concrete level** we should have preconditions for: + + 1. Expressing the **validity of the input tensors**. At this level the tensors are passed as arguments and therefore we need to evalute whether they are **valid tensor** + + 2. Verify if the output tensor (already passed as an argument) has the appropriate shape, computed with the abstract function with such objective. Such verification should be performed by checking the dimensions of the output tensor with the dimensions computed by the abstract function. Moreover, we should also check that the output tensor has the appropriate **rank**. + + 3. All the **preconditions** already present at the abstract level. The **concrete** ==level== will essentially have the exact same copy of the abstract preconditions but adapted to the concrete level (the way the accesses are performed for instance will change). + +**Ensures** + +- On the **abstract level** the postconditions should cover each record of the abstract tensor - **dimensions**, **data** and **background**:==already covered in Section 2: remove== + +- On the **concrete level** the only needed clause is the refinement mapping, indicating that the concrete implementation is correct with respect to the abstract specification. This is usually expressed by a postcondition of the form: + + - `ensures { tensor result =
+ +--- + +
+> (Jean-Loup) I think that the use of Why3 shall be recomended from the start and that some usefull links shall be provided for readers not familiar with Why3. + +# Part 1 — Formalization Styles + +In SONNX, every operator is formalized at **two distinct levels**. + +> (Jean-Loup) "is" or "must be" or "should be"? +> +> (Jean-Loup) To name the levels ": Abstract formalization and concrete formalization." + +Each level serves a different purpose and follows a different style. + +Understanding both is essential before writing any specification. + +## 1.1 Abstract Formalization + +At this level the operator must be specified based only on its behavior and **mathematical semantics**. + +It should the **as close as possible transalation** of the mathematical definition of the operator - **presented in the informal specification**, being therefore easy to read and understand. + +No implementation details should be present at this level, which means that the **tensor' representation** should **mimic the mathematical definition of a tensor** (also similar to the ONNX tensor concept) - a multidimensional array - in which each entry is accessed by its coordinates. + +### Tensor + +- **Type**: At this level tensors are said to be **polymorphic**.
+ This means that the specifier should be as generic as possible when defining an operator.
+ More details in - [2.5 - Operator tensor types](#25-operator-tensor-types). + + > (Jean-Loup) I have no idea of what a specifier is. Depending on the targeted reader the term should be defined. + +- **Representation**: Tensors are represented as structures containing the following records: + + - `dims` - List of integers representing the shape + + - `data` - A map from coordinates to values + + > (Jean-Loup) May be valid coordinates or in-bounds coordinates instead of just coordinates. "coordinates" seems to be equal to "tensor index". If it is the case, a link to tensor index should be added. + + - `background` - The default value for out-of-bounds coordinates + +- **Type Invariants**: There are two important invariants that must be satisfied by this tensor representatio: + + > (Jean-Loup) "representatio" <- "representation" + + 1. **Positive Dimensions** + + All dimensions in the `dims` list of a tensor must be positive integers.
+ From our point of view this will be updated to support **non-negative integers**, therefore allowing for tensors with null dimensions. [***Work in Progress***] + + **Definition:** + + - Predicate `positive` + + ```why3 + predicate positive (ds : list int) = + match ds with + | Nil -> true + | Cons d ds -> 0 < d /\ positive ds + end + ``` + - `invariant { positive dims }` + + > (Jean-Loup) Indicate this is Why3 code in the text. Looking at https://why3.gitlabpages.inria.fr/why3/syntaxref.html , I can't find a definition of Cons and Nil (Even if I intuitively understand...). There is only list and forest examples using Cons and Nil. Are Cons and Nil defined by other predicates? May be the begining of the guidelines should indicate that Why3 should be used and that the reader should first be familiarized with Why3. + + 2. **Valid values** + + Coordinates are either valid for the tensor shape or the value mapped by those coordinates is the `background` value. + + **Definition:** + + - Predicate `valid` + + ```why3 + predicate valid (ks ds : list int) = + match ks , ds with + | Nil , Nil -> true + | Cons k ks , Cons d ds -> 0 <= k < d /\ valid ks ds + | _ -> false + end + ``` + - `invariant { forall k. valid k dims \/ data k = background }` + +
+ + These invariants are extremely important as they will sometimes define how the operator should be formalized. + + For example, while computing the data of the tensor it is **highly recommended** to use the predicate `valid`, essentially to capture and pass the invariant. + + > (Jean-Loup) Are the predicates positive and valid in a Why3 library? If it is the case, inclusion of the library should be recomended to avoid copy errors. + +### Specification Style + +Throughout this level, the specification should be carried out in a **purely functional style** meaning that there should be no side effects and no mutable state (functions do not modify state, they receive one as input and return a new one as output). + +Looping constructs are forbidden at this level, and instead, **recursive functions** and **mathematical constructs** should be used to define the behavior of the operator. + +> (Jean-Loup) The concept of mathematical construct should be defined. + +### Importance of this level + +It establishes the logical and mathematical specification of the operator, which serves as the **source of truth** for correctness. + +It also provides the perfect link between the informal specification and the formalization. + +## 1.2 Concrete Formalization + +The concrete level describes the **imperative implementation** that will be extracted to C code. + +It describes it based on a **target C representation** for tensors called **ctensors** which are essentially structures backed by flat arrays in memory. + +### Tensor + +- **Type**: At this level the type of tensor elements is fixed to be `float32`, `float64`, `int32`, `int64`, etc..., and the operator should be defined specifically for that type. + +- **Representation**: Tensors are represented as pointers to structures that contain: + + - `t_rank`: Number of dimensions + + - `t_dims`: Pointer to a flat array containing the tensor dimensions - pointer to `int32` array + + - `t_data`: Pointer to a flat array containing the tensor elements - pointer to `type` array (where type is `float32`, `float64`, `int32`, `int64`, ...) + +
+ +Note that, unlike the previous level, here the tensors are defined based on a concrete target representation - tensors are essentially flat arrays in memory. + +> (Jean-Loup) I guess it depends on what is meant by "concrete representation". Asking to ChatGPT the first answer is "yes lists and maps are concrete data structures". May be it should be "target C representation" or "C built in concrete representation". + +Moreover, there is no `background` value in this representation - **tensors entries must be accessed only in valid coordinates** (i.e., coordinates that are within the bounds of the tensor shape). + +### Specification Style + +Throughout this level, the specification should be carried out in an **imperative style** meaning that **loops and mutable state** are allowed and often necessary to express the implementation. + +### Importance of this level + +It provides the necessary details to extract executable C code and reason about memory, bounds, and machine integers. + +> (Jean-Loup) I think the information in sub-sections "Importance of this level" for abstract and concrete representations should be given at the begining, i.e. before 1.1. + +## 1.3 Link between the two levels + +### Why is it important to have two levels? + +- We need somehow to express that the **concrete implementation** is correct with respect to the **operator's intended behavior** - which is captured by the **abstract specification**. + +- The abstract spec is easy to **read, understand, and reason about** — it directly mirrors the mathematical definition from its informal specification. + +- The concrete spec is necessary to **extract executable C code** and reason about memory, bounds, and machine datatypes. + +- The two levels are connected through a **refinement relationship**. The concrete implementation must be proven to produce the same result as the abstract specification. + +The following image gives a high-level overview of the relationship between the two levels and how they connect through refinement: + + + +
+
+
+ +# Part 2 — Guidelines for Abstract Formalization + +## 2.1. Module Structure + +Each abstract module should follow this general structure: + + +``` +module OP
+ +The code written above will not generate any verification conditions, even if the functions called inside it explicitly need **requires clauses**. + +Therefore, no verification condtions were raised and the function `calculate_dims` does not appear on the Verification Conditions menu (left pannel in the picture above). + +### 2.2.3 TypeInvariant Lemmas + +When using `let rec function` declarations, their logical context sometimes does not propagate to subsequent functions, or it may appear only in axiomatic form. + +As a consequence, proving the type invariants of tensors — in particular, ensuring that the output dimensions satisfy the positivity invariant — requires explicit lemmas that establish these properties. + +The `calculate_dY0` function defined above is a concrete example of this issue. + +The following lemma is needed to guarantee that the result produced by `calculate_dY0` is strictly positive: + +```why3 + let rec lemma calculate_dY0_positive (x: tensor real) (axis: int) (i: int) + requires { positive x.dims } + requires { 0 <= axis <= length x.dims } + requires { 0 <= i <= axis } + ensures { 0 < calculate_dY0 x axis i } + variant { axis - i } + = + if i >= axis then + () + else + let d = get_dim x.dims i in + calculate_dY0_positive x axis (i + 1) +``` + +The different kinds of lemmas and how to use them will be covered in section [3.4](#34-invariants), [4.2](#42-ide-transformations-and-prover-hints). + +### 2.2.4 Main Operator Function + +Moreover, the main operator function cannot be declared as `function` because it needs to have contracts (`requires` / `ensures`) and `function` does not support contracts. + +Therefore, the main operator function should be declared as `let ghost function` with full contracts. + +```why3 +module OPSummation + use int.Int + + let rec function summation (i : int) (iter : int) : int = + variant { iter - i} + if i < iter then + 1 + summation (i + 1) iter + else + 0 + + let ghost function unitSum (n: int) : int = + requires { n >= 0 } + ensures { result = n } + summation 0 n +end +``` + +### 2.2.5 Guidelines + +| Guideline | Details | +|:---|:---| +| Use `function` for total functions and whenever it is possible! | A `function` is a logical function. | +| Use `let rec function` only when recursion needs a variant. | If Why3 cannot prove termination of a `function`, switch to `let rec function` and provide a `variant` clause. | +| Use `let ghost function` for the **main operator**. | The main function should be a `let ghost function` with full contracts (`requires` / `ensures`). | + +### Examples + +Besides the summation example above, here are some examples of such formalization styles: + +- **Clip**: [Clip abstract specification](./examples/clip.mlw) + +- **MatMul**: [MatMul abstract specification](./examples/matmul.mlw) + +## 2.3. Contracts on the Main Function + +Until now, we have stated that no function should have contracts except for the `main function` or any other function declared with `let rec`. + +The `main function`, **must** include as preconditions (`requires`) all the necessary constraints that are present in the informal specification for the inputs and the attributes. Output constraints (such as shape) will not be included at this point. + +On the other hand, the postconditions (`ensures`) of the main operator function **must** include the following three postconditions: + +| Postcondition | Purpose | +|:---|:---| +| `ensures { result.dims = ... }` | Specifies the **output shape** | +| `ensures { result.data = ... }` | Specifies the **output data** (as a map) | +| `ensures { result.background = ... }` | Specifies the **background value** | + +### Example + +```why3 +let ghost function opclip (x l m : tensor real) : tensor real + requires { is_scalar_tensor l } + requires { is_scalar_tensor m } + ensures { result.dims = x.dims } (* ← shape *) + ensures { result.data = dclip x l m } (* ← data *) + ensures { result.background = x.background } (* ← background *) += + { dims = x.dims; data = dclip x l m; background = x.background } +``` + +## 2.4. Data Function Pattern + +Whenever we want to specify the operator along all possible coordinates we can follow any of the following pattern: + + +### Anonymous function declaration + +Create an **anonymous function** for the data that takes the coordinates as input and defines the value at those coordinates based on the operator's semantics. + +We are basically stating that for all possible coordinates, the value at those coordinates is defined by this function. + +Note that, **not all coordinates are valid**, so we need to **check the validity of the coordinates** first and **return the background value for invalid coordinates**. + +That's why we need to compute the output shape, prior to this computation, as proposed in the [previous section](#file-structure-proposal). + +```why3 +let ghost function d
+ +Unlike, the previous examples, this operator is defined for tensors with a polymorphic datatype `'a`. + +Once for clip and matmul we need to compute values, there is no other option but to have an abstract datatype which is in fact **numerical**. + +Nevertheless, **where** doesn´t resort to any mathematical handling whatsoever and that's why its abstract datatype can be polymorphic. + +So whenever possible one should resort to **polymorphic** abstract datatypes. + +This is the case for the vast majority of the structural operators: **flatten**, **reshape**, among others. + + +# Part 3 — Guidelines for Concrete Formalization + +## 3.1. Module Structure + +The concrete module should follow this general structure: + +```why3 + module COP
+Equivalent to what is presented in the image [here](#refinement-mapping) + +To better understand this, check the `coords_from_X_p` function, presented in the [conv](./examples/conv.mlw): + +```why3 + (* Abstract level *) + function coords_from_X_p (x: tensor real) (x_p_coords : list int) ( pad_top pad_left :int) : real + = + let b = get_dim x_p_coords 0 in + let c = get_dim x_p_coords 1 in + let n = (get_dim x_p_coords 2) - pad_top in + let m = (get_dim x_p_coords 3) - pad_left in + let x_coords = Cons b (Cons c (Cons n (Cons m Nil))) in + if valid x_coords x.dims then + x.data x_coords + else + 0.0 +``` + +```why3 + (* Concrete level *) + let coords_from_X_p (x: ctensor) (x_p_coords : iarray) ( pad_top pad_left :int32) : (float, bool) = + requires { valid_tensor x } + requires { x.t_rank = 4 } + requires { valid_range x_p_coords 0 4 } + requires { writable x_p_coords } + requires { in_bounds (value_at x_p_coords 2 - pad_top) } + requires { in_bounds (value_at x_p_coords 3 - pad_left) } + + ensures { let (value, flag) = result in + flag -> coords_from_X_p (tensor x) (ivector x_p_coords 4) (to_int pad_top) (to_int pad_left) = value + } + + let ref flag = False in + let b = x_p_coords[0] in + let c = x_p_coords[1] in + let n = (x_p_coords[2]) - pad_top in + let m = (x_p_coords[3]) - pad_left in + let x_coords_array = malloc (to_uint32 4) in + if is_not_null x_coords_array then begin + flag <- True; + x_coords_array[0] <- b; + x_coords_array[1] <- c; + x_coords_array[2] <- n; + x_coords_array[3] <- m; + + assert { ivector x_coords_array 4 = Cons (to_int b) (Cons (to_int c) (Cons (to_int n) (Cons (to_int m) Nil))) } ; + + let x_coords = coffset x_coords_array x.t_dims x.t_rank in + if x_coords >= 0 then begin + (x.t_data[x_coords], flag) + end + else begin + ((f32 0.0), flag) + end + end + else begin + flag <- False; + ((f32 0.0), flag) + end +``` + +These two functions perform the same exact computation. + +To better understand how these two relate one can compare both specifications: + +**Coordinates** + +- On the **abstract side** the indices of the coordinates are captured with the `get_dim` function while on the **concrete level** the indices are captured by directly accessing the `iarray` with the `[]` operator. + + - These functions are equivalent and such equivalence proof is already available in the tensors library + +- To define the whole coordinates, on the **abstract side**, we only need a **list constructor**. On the **concrete level** such process is performed in two distinct steps: + + - **Firstly**, the appropriate space is allocated with the `malloc` function + + - **If the malloc is successful**, we then set each index of the array with the appropriate value. + + - Once again an equivalence must be established between these two constructs. That's exactly what is performed by the `assert` clause. + +**Computation** + +- On the **abstract side** we perform the computation by checking the validity of the coordinates on the dimensions of tensor x using the predicate **valid**. If the coordinates are valid we are going to return the value that is on that coordinates, else we are going to return 0. + +- On the **concrete side** we perform the computation by calculating the flatindex, of the coordinates on the tensor x dimensions, if the flatindex is a valid index, then we return the value on that index, else we are going to return 0. + +- The equivalence is captured by the postcondition present on the `coffset` function and the `if clause` which follows the same pattern at both levels. + +**Refinement mapping** + +- The refinement mapping relation is expressed with an ensures. In this function this realtion is expressed by: + + ``` + ensures { let (value, flag) = result in + flag -> coords_from_X_p (tensor x) (ivector x_p_coords 4) (to_int pad_top) (to_int pad_left) = value + } + ``` + +- This is the most important relation between both levels, as it states the values returned by both functions are exactly the same. Ultimately this prove that the function specified at the concrete level is correct with respect to the expected one presented at the abstract level, therefore ensuring that the behavior is the same at both levels. + +- Note that, in the concrete level, we need to explicitly check that the `malloc` was successful and return a flag indicating whether the coordinates were successfully computed or not. This is not necessary on the abstract level because we are working with mathematical constructs and we can assume that such constructs are always successfully created. + +### 3.3 Main operator function + +This is naturally the most important function and the one whith more details to be taken into account. + +#### 3.3.1 Contracts + +The **main operator function** must include contracts at both levels. + +**Requires** + +- On the **abstract level** the preconditions should include `requires` for all the necessary constraints that are present in the informal specification for the inputs and the attributes. Output constraints (such as shape) will not be included at this point. + +- On the **concrete level** we should have preconditions for: + + 1. Expressing the **validity of the input tensors**. At this level the tensors are passed as arguments and therefore we need to evalute whether they are **valid tensor** + + 2. Verify if the output tensor (already passed as an argument) has the appropriate shape, computed with the abstract function with such objective. Such verification should be performed by checking the dimensions of the output tensor with the dimensions computed by the abstract function. Moreover, we should also check that the output tensor has the appropriate **rank**. + + 3. All the **preconditions** already present at the abstract level. The **concrete** will essentially have the exact same copy of the abstract preconditions but adapted to the concrete level (the way the accesses are performed for instance will change). + +**Ensures** + +- On the **abstract level** the postconditions should cover each record of the abstract tensor - **dimensions**, **data** and **background**: + +- On the **concrete level** the only needed clause is the refinement mapping, indicating that the concrete implementation is correct with respect to the abstract specification. This is usually expressed by a postcondition of the form: + + - `ensures { tensor result =
+ +--- + +
+ +# Part 1 — Formalization Styles + +In SONNX, every operator must be formalized at two distinct levels: abstract formalization and concrete formalization. + +Each level serves a different purpose and follows a different style. + +We start from an abstract formalization — which captures the mathematical semantics of the operator and serves as the **source of truth** for correctness — and progressively refine it into a concrete formalization that is close enough to the target implementation to be automatically extracted into C code - reasoning about memory, bounds, and machine data types. + +Understanding both is essential before writing any specification. + +## 1.1 Abstract Formalization + +At this level the operator must be specified making no reference to any implementation detail, and therefore it should be **implementation-agnostic**. + +It shall be **traceable** to the **informal specification**, being easy to validate, first and easy to read and understand, second. Traceability must be enforced: + +- first by keeping the formal specification as close to the informal specification (e.g., stick to the mathematical specification given in the informal specification) + +- second by providing explicit link via `[tags]` to specific parts of the informal specification. + +No implementation details should be present at this level, which means that the specification of tensors shall remain as abstract as possible, focusing on their mathematical properties. + +### Tensors + +- **Type**: At this level tensors are specified as **polymorphic structures**, i.e., they are parameterized by the type of the values they contain.
+ This means that the specification author should be as generic as possible when defining an operator.
+ More details in - [2.5 - Operator tensor types](#25-operator-tensor-types). + +- **Representation**: Tensors are represented as structures containing the following records: + + - `dims` - List of integers representing the shape + + - `data` - A map from [indexes](../../../spec/informal/common/definitions.md) to values + + - `background` - The default value for indexes out of the bounds defined by the shape + + A "valid index" is an index compatible with the dimension of the tensor, i.e. the i-th components of the index is strictly positive and strictly less than the i-th dimension of the tensor + + The data mapping is complete since it maps all possible indexes to values, but the value mapped by invalid indexes is the `background` value. + +- **Type Invariants**: There are two important invariants that must be satisfied by this tensor representation: + + 1. **Positive Dimensions** + + All dimensions in the `dims` list of a tensor must be **strictly positive integers**.
+ This constraint may be relaxed in a lated version of the specification to support tensors with **null** dimensions. [***Work in Progress***] + + - Predicate `positive` + + ```why3 + predicate positive (ds : list int) = + match ds with + | Nil -> true + | Cons d ds -> 0 < d /\ positive ds + end + ``` + - `invariant { positive dims }` + + 2. **Valid values** + + Indexes are either valid for the tensor shape or the value mapped by those indexes is the `background` value. + + - Predicate `valid` + + ```why3 + predicate valid (ks ds : list int) = + match ks , ds with + | Nil , Nil -> true + | Cons k ks , Cons d ds -> 0 <= k < d /\ valid ks ds + | _ -> false + end + ``` + - `invariant { forall k. valid k dims \/ data k = background }` + +
+ + These invariants are extremely important as they will sometimes define how the operator should be formalized. + + For example, while computing the data of the tensor it is **highly recommended** to use the predicate `valid`, essentially to capture and pass the invariant. + + An alternative was to define the data through recursive definitions once the shape is already computed, but this approach is much more complex and usually requires auxiliary lemmas to help the proof. + + The above predicates and invariants are available in the [tensors library](../../../spec/formal/common/libs/tensor/). + +### Specification Style + +Throughout this level, the specification should be carried out in a **purely functional style** meaning that there should be no side effects and no mutable state (functions do not modify state, they receive one as input and return a new one as output). + +Users should specify the operator based on mathematically and recursive definitions, avoiding loops and mutable state, increasing the **provability** and **ease of proof** of this specification. + +## 1.2 Concrete Formalization + +The concrete level describes the **imperative implementation** that will be extracted to C code. + +It describes it based on a **target C representation** for tensors called **ctensors** which are essentially structures backed by flat arrays in memory. + +### Tensors + +- **Type**: At this level the type of tensor elements is fixed to be `float32`, `float64`, `int32`, `int64`, etc. and the operator should be defined specifically for that type. + +- **Representation**: Tensors are represented as pointers to structures that contain: + + - `t_rank`: Number of dimensions + + - `t_dims`: Pointer to a flat array containing the tensor dimensions - pointer to `int32` array + + - `t_data`: Pointer to a flat array containing the tensor elements - pointer to `type` array (where type is `float32`, `float64`, `int32`, `int64`, ...) + +
+ +Note that, unlike the previous level, here the tensors are defined based on a target C representation - tensors are essentially flat arrays in memory. + +Moreover, there is no `background` value in this representation - **only valid indexes must be used to access values of tensors** (i.e. coordinates that are within the bounds of the tensor shape). + +### Specification Style + +In this level, the specification should be carried out in an **imperative style** meaning that **loops and mutable state** are allowed and often necessary to express the implementation. + +### Importance of this level + +It provides the necessary details to extract executable C code and reason about memory, bounds, and machine data types. + +## 1.3 Link between the two levels + +### Why is it important to have two levels? + +- We need somehow to express that the **concrete specification** is correct with respect to the **operator's intended behavior** - which is captured by the **abstract specification**. + +- The abstract spec is easy to **read, understand, and reason about** — it directly mirrors the mathematical definition from its informal specification. + +- The concrete spec is necessary to **extract executable C code** and reason about memory, bounds, and machine datatypes. + +- The two levels are connected through a **refinement relationship**. The concrete implementation must be proven to produce the same result as the abstract specification. + +The following image gives a high-level overview of the relationship between the two levels and how they connect through refinement: + + + +
+
+
+ +# Part 2 — Guidelines for Abstract Formalization + +## 2.1. Module Structure + +Each abstract module should follow this general structure: + + +``` +module OP
+ +The code written above will not generate any verification conditions, even if the functions referenced inside it explicitly need **requires clauses**. + +Therefore, no verification conditions were raised and the function `calculate_dims` does not appear on the Verification Conditions menu (left panel in the picture above). + +### 2.2.3 TypeInvariant Lemmas + +When using `let rec function` declarations, their logical context sometimes does not propagate to subsequent functions, or it may appear only in axiomatic form. + +As a consequence, proving the type invariants of tensors — in particular, ensuring that the output dimensions satisfy the positivity invariant — requires explicit lemmas that establish these properties. + +The `calculate_dY0` function defined above is a concrete example of this issue. + +The following lemma is needed to guarantee that the result produced by `calculate_dY0` is strictly positive: + +```why3 + let rec lemma calculate_dY0_positive (x: tensor real) (axis: int) (i: int) + requires { positive x.dims } + requires { 0 <= axis <= length x.dims } + requires { 0 <= i <= axis } + ensures { 0 < calculate_dY0 x axis i } + variant { axis - i } + = + if i >= axis then + () + else + let d = get_dim x.dims i in + calculate_dY0_positive x axis (i + 1) +``` + +The different kinds of lemmas and how to use them will be covered in section [3.4](#34-invariants), [4.2](#42-ide-transformations-and-prover-hints). + +### 2.2.4 Main Operator Function + +To enforce traceability, as [previously mentioned](#traceability), the main operator function should capture the constraints present in the informal specification as preconditions (`requires`) while providing postconditions (`ensures`) for every record of the output tensor. + +To capture such contracts one needs to define a construct that belongs to the programming namespace. Moreover, since this function is only used to specification purposes it is not supposed to be used in any implementation context. To enforce that this function can only be used at the logical level sign it as **ghost**. + +Therefore, the main operator function should be declared as `let rec ghost function` with full contracts. + +```why3 +module OPSummation + use int.Int + + let rec ghost function summation (i : int) (iter : int) : int = + variant { iter - i} + if i < iter then + 1 + summation (i + 1) iter + else + 0 + + let ghost function unitSum (n: int) : int = + requires { n >= 0 } + ensures { result = n } + summation 0 n +end +``` + +### Examples + +Besides the summation example above, here are some examples of such formalization styles: + +- **Clip**: [Clip abstract specification](./examples/clip.mlw) + +- **MatMul**: [MatMul abstract specification](./examples/matmul.mlw) + +## 2.3. Contracts on the Main Function + +Until now, we have stated that no function should have contracts except for the `main function` or any other function declared with `let rec ghost function`. + +The `main function`, **must** include as preconditions (`requires`) all the necessary constraints that are present in the informal specification for the inputs and the attributes. Output constraints (such as shape) will not be included at this point. + +On the other hand, the postconditions (`ensures`) of the main operator function **must** include the following three postconditions: + +| Postcondition | Purpose | +|:---|:---| +| `ensures { result.dims = ... }` | Specifies the **output shape** | +| `ensures { result.data = ... }` | Specifies the **output data** (as a map) | +| `ensures { result.background = ... }` | Specifies the **background value** | + +### Example + +```why3 +let ghost function opclip (x l m : tensor real) : tensor real + requires { is_scalar_tensor l } + requires { is_scalar_tensor m } + ensures { result.dims = x.dims } (* ← shape *) + ensures { result.data = dclip x l m } (* ← data *) + ensures { result.background = x.background } (* ← background *) += + { dims = x.dims; data = dclip x l m; background = x.background } +``` + +## 2.4. Data Function Pattern + +Whenever we want to specify the operator along all possible coordinates we can follow any of the following pattern: + + +### Anonymous function declaration + +Create an **anonymous function** for the data that takes the coordinates as input and defines the value at those coordinates based on the operator's semantics. + +We are basically stating that for all possible coordinates, the value at those coordinates is defined by this function. + +Note that, **not all coordinates are valid**, so we need to **check the validity of the coordinates** first and **return the background value for invalid coordinates**. + +That's why we need to compute the output shape, prior to this computation, as proposed in the [previous section](#file-structure-proposal). + +```why3 +let ghost function d
+ +Unlike, the previous examples, this operator is defined for tensors with a polymorphic datatype `'a`. + +Once for clip and matmul we need to compute values, there is no other option but to have an abstract datatype which is in fact **numerical**. + +Nevertheless, **where** doesn´t resort to any mathematical handling whatsoever and that's why its abstract datatype can be polymorphic. + +So whenever possible one should resort to **polymorphic** abstract datatypes. + +This is the case for the vast majority of the structural operators: **flatten**, **reshape**, among others. + + +# Part 3 — Guidelines for Concrete Formalization + +## 3.1. Module Structure + +The concrete module should follow this general structure: + +```why3 + module COP
+Equivalent to what is presented in the image [here](#refinement-mapping) + +To better understand this, check the `coords_from_X_p` function, presented in the [conv](./examples/conv.mlw): + +```why3 + (* Abstract level *) + function coords_from_X_p (x: tensor real) (x_p_coords : list int) ( pad_top pad_left :int) : real + = + let b = get_dim x_p_coords 0 in + let c = get_dim x_p_coords 1 in + let n = (get_dim x_p_coords 2) - pad_top in + let m = (get_dim x_p_coords 3) - pad_left in + let x_coords = Cons b (Cons c (Cons n (Cons m Nil))) in + if valid x_coords x.dims then + x.data x_coords + else + 0.0 +``` + +```why3 + (* Concrete level *) + let coords_from_X_p (x: ctensor) (x_p_coords : iarray) ( pad_top pad_left :int32) : (float, bool) = + requires { valid_tensor x } + requires { x.t_rank = 4 } + requires { valid_range x_p_coords 0 4 } + requires { writable x_p_coords } + requires { in_bounds (value_at x_p_coords 2 - pad_top) } + requires { in_bounds (value_at x_p_coords 3 - pad_left) } + + ensures { let (value, flag) = result in + flag -> coords_from_X_p (tensor x) (ivector x_p_coords 4) (to_int pad_top) (to_int pad_left) = value + } + + let ref flag = False in + let b = x_p_coords[0] in + let c = x_p_coords[1] in + let n = (x_p_coords[2]) - pad_top in + let m = (x_p_coords[3]) - pad_left in + let x_coords_array = malloc (to_uint32 4) in + if is_not_null x_coords_array then begin + flag <- True; + x_coords_array[0] <- b; + x_coords_array[1] <- c; + x_coords_array[2] <- n; + x_coords_array[3] <- m; + + assert { ivector x_coords_array 4 = Cons (to_int b) (Cons (to_int c) (Cons (to_int n) (Cons (to_int m) Nil))) } ; + + let x_coords = coffset x_coords_array x.t_dims x.t_rank in + if x_coords >= 0 then begin + (x.t_data[x_coords], flag) + end + else begin + ((f32 0.0), flag) + end + end + else begin + flag <- False; + ((f32 0.0), flag) + end +``` + +These two functions perform the same exact computation. + +To better understand how these two relate one can compare both specifications: + +**Coordinates** + +- On the **abstract side** the indices of the coordinates are captured with the `get_dim` function while on the **concrete level** the indices are captured by directly accessing the `iarray` with the `[]` operator. + + - These functions are equivalent and such equivalence proof is already available in the tensors library + +- To define the whole coordinates, on the **abstract side**, we only need a **list constructor**. On the **concrete level** such process is performed in two distinct steps: + + - **Firstly**, the appropriate space is allocated with the `malloc` function + + - **If the malloc is successful**, we then set each index of the array with the appropriate value. + + - Once again an equivalence must be established between these two constructs. That's exactly what is performed by the `assert` clause. + +**Computation** + +- On the **abstract side** we perform the computation by checking the validity of the coordinates on the dimensions of tensor x using the predicate **valid**. If the coordinates are valid we are going to return the value that is on that coordinates, else we are going to return 0. + +- On the **concrete side** we perform the computation by calculating the flatindex, of the coordinates on the tensor x dimensions, if the flatindex is a valid index, then we return the value on that index, else we are going to return 0. + +- The equivalence is captured by the postcondition present on the `coffset` function and the `if clause` which follows the same pattern at both levels. + +**Refinement mapping** + +- The refinement mapping relation is expressed with an ensures. In this function this realtion is expressed by: + + ``` + ensures { let (value, flag) = result in + flag -> coords_from_X_p (tensor x) (ivector x_p_coords 4) (to_int pad_top) (to_int pad_left) = value + } + ``` + +- This is the most important relation between both levels, as it states the values returned by both functions are exactly the same. Ultimately this prove that the function specified at the concrete level is correct with respect to the expected one presented at the abstract level, therefore ensuring that the behavior is the same at both levels. + +- Note that, in the concrete level, we need to explicitly check that the `malloc` was successful and return a flag indicating whether the coordinates were successfully computed or not. This is not necessary on the abstract level because we are working with mathematical constructs and we can assume that such constructs are always successfully created. + +### 3.3 Main operator function + +This is naturally the most important function and the one whith more details to be taken into account. + +#### 3.3.1 Contracts + +The **main operator function** must include contracts at both levels. + +**Requires** + +- On the **abstract level** the preconditions should include `requires` for all the necessary constraints that are present in the informal specification for the inputs and the attributes. Output constraints (such as shape) will not be included at this point. + +- On the **concrete level** we should have preconditions for: + + 1. Expressing the **validity of the input tensors**. At this level the tensors are passed as arguments and therefore we need to evalute whether they are **valid tensor** + + 2. Verify if the output tensor (already passed as an argument) has the appropriate shape, computed with the abstract function with such objective. Such verification should be performed by checking the dimensions of the output tensor with the dimensions computed by the abstract function. Moreover, we should also check that the output tensor has the appropriate **rank**. + + 3. All the **preconditions** already present at the abstract level. The **concrete** will essentially have the exact same copy of the abstract preconditions but adapted to the concrete level (the way the accesses are performed for instance will change). + +**Ensures** + +- On the **abstract level** the postconditions should cover each record of the abstract tensor - **dimensions**, **data** and **background**: + +- On the **concrete level** the only needed clause is the refinement mapping, indicating that the concrete implementation is correct with respect to the abstract specification. This is usually expressed by a postcondition of the form: + + - `ensures { tensor result =
+`[T1]` This is a tagged paragraph. + +This is a reference to the tagged paragraph [`[T1]`](#my_tag_name). + +### Types +- The type names shall be the ones used in the ONNX description of the operators, without surrounding them with "tensor()". + - Example: "tensor(double)" in ONNX becomes "double" in the non-formal specification. +- The data types allowed in SONNX operators are: + - IEEE 754 floating-point types: double, float, float16 + - Signed integer types: int64, int32, int16, int8 + - Unsigned integer types: uint64, uint32, uint16, uint8 + - bool + - string +- IEEE 754 floating-point types, i.e., double, float and float16 have the following special numbers: + - +0 and -0 + - +inf and -inf + - NaN (Not a Number) +- All operators applicable to numeric values shall first be specified for values in the domain of real numbers, then specific descriptions shall be given for the other types (float, double, etc.). +- A description can be applicable to multiple types as long as its **semantics description** remains the same for all types. + +## Structure and contents of the specification + +This section describes the required structure and contents of the non-formal specification of an operator. + +The [specification template](informal_spec_template.md) gives an example of the required structure. + +### Contents + +This section gives the list of all non-formal specifications of the operator, for each of the applicable types, with hyperlinks to the sections (see [template](informal_spec_template.md)). + +- **Op** operator for type real +- **Op** operator for types <T1>, <T2>,... +- **Op** operator for types <T1>, <T2>,... +- etc. + +The reference, with link, to the ONNX definition of **Op** shall be inserted in this section. See **Div** example below. + +Here is an example for operator **Div**: +> Contents +>- **Div** operator for type real +>- **Div** operator for types float16, float32, float64 +>- **Div** operator for types int8, int16, int32, int64, uint8, uint16, uint32, uint64 +> +> Based on ONNX [Div version 14](https://onnx.ai/onnx/operators/onnx__Div.html). + +The following section must be repeated for each set of types for which the semantics is the same. One section corresponds to one entry in the "Contents" list. + +## **Op** (