Final fixes for #75

OpenCyphal · Jul 13, 2020 · f993558 · f993558
1 parent 2c16baa
commit f993558
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 9 deletions.
diff --git a/dsdl b/dsdl
diff --git a/specification/dsdl/attributes.tex b/specification/dsdl/attributes.tex
@@ -160,7 +160,7 @@ \subsubsection{Offset attribute}
 $$
     \texttt{\_offset\_}_\text{union} =
     \bigcup\limits_{i=1}^{n}
-    \left\{ \lceil{}\log_2 n\rceil{} + b : b \in B_i \right\}
+    \left\{ 2^{\lceil\log_2 \text{max}\left(8, \lceil\log_2 n\rceil\right)\rceil} + b : b \in B_i \right\}
 $$
 where $n$ is the number of fields defined in the current union definition,
 and $B_i$ is the bit length set of the data type of the field number $i$.
@@ -186,7 +186,7 @@ \subsubsection{Offset attribute}
         uint8 a
         #@print _offset_  # Would fail: it's a tagged union, _offset_ is undefined until after the last field
         uint16 b
-        @assert _offset_ == {1 + 8,  1 + 16}
+        @assert _offset_ == {8 + 8,  8 + 16}
         ---
         @assert _offset_ == {0}
         float16 a
@@ -196,12 +196,11 @@ \subsubsection{Offset attribute}
         int4 b
         @assert _offset_ == {24}
         uint8[<4] c
-        @assert _offset_ == 2 + {24,  32,  40,  48}
-        void6
+        @assert _offset_ == 8 + {24,  32,  40,  48}
         @assert _offset_ % 8 == {0}
         # One of the main usages for _offset_ is statically proving that the following field is byte-aligned
         # for all possible valid serialized representations of the preceding fields. It is done by computing
-        # a remainder as shown below. If the field is aligned, the remainder set will equal {0}. If the
+        # a remainder as shown above. If the field is aligned, the remainder set will equal {0}. If the
         # remainder set contains other elements, the field may be misaligned under some circumstances.
         # If the remainder set does not contain zero, the field is never aligned.
         uint8 well_aligned   # Proven to be byte-aligned.

diff --git a/specification/dsdl/serializable_types.tex b/specification/dsdl/serializable_types.tex
@@ -317,7 +317,8 @@ \subsubsection{Type polymorphism and equivalency}
     \item both $B$ and $D$ define tagged unions;
     \item $B$ is not $D$;
     \item $b \leq d$;
-    \item $\lceil{}\log_2 b\rceil{} = \lceil{}\log_2 d\rceil{}$;
+    \item $2^{\lceil\log_2 \text{max}\left(8, \lceil\log_2 b\rceil\right)\rceil} =
+           2^{\lceil\log_2 \text{max}\left(8, \lceil\log_2 d\rceil\right)\rceil}$;
     \item for $i \in \left[0, b\right)$, the type of the field attribute of $D$ at index $i$
           is the same or is a subtype of the type of the field attribute of $B$ at index $i$.
     \item for $i \in \left[0, b\right)$, the name of the field attribute of $D$ at index $i$
@@ -352,7 +353,7 @@ \subsubsection{Type polymorphism and equivalency}
     Subtyping example for union types. First type:
 
     \begin{minted}{python}
-        @union                            # The implicit union tag field is 2 bits wide
+        @union                            # The implicit union tag field is 8 bits wide
         uavcan.primitive.Empty.1.0 foo
         float16 bar
         uint8 zoo
@@ -361,7 +362,7 @@ \subsubsection{Type polymorphism and equivalency}
     The second type is a structural subtype of the first type:
 
     \begin{minted}{python}
-        @union                            # The implicit union tag field is 2 bits wide
+        @union                            # The implicit union tag field is 8 bits wide
         uavcan.diagnostic.Record.1.0 foo  # Subtype
         float16 bar                       # Same
         uint8 zoo                         # Same