Clarify @Custom (#16)

Author: rossberg

document/core/appendix/custom.rst

@@ -273,7 +273,8 @@ They must not be nested into other constructs.
      \text{start} \\ &&|&
      \text{elem} \\ &&|&
      \text{code} \\ &&|&
-     \text{data} \\
+     \text{data} \\ &&|&
+     \text{datacount} \\
    \end{array}
 
 The first :ref:`string <text-string>` in a custom annotation denotes the name of the custom section it represents.
@@ -282,6 +283,7 @@ The remaining strings collectively represent the section's payload data, written
 An arbitrary number of custom annotations (even of the same name) may occur in a module,
 each defining a separate custom section when converting to :ref:`binary format <binary>`.
 Placement of the sections in the binary can be customized via explicit *placement* directives, that position them either directly before or directly after a known section.
+That section must exist and be non-empty in the binary encoding of the annotated module.
 The placements :math:`\T{(before~first)}` and :math:`\T{(after~last)}` denote virtual sections before the first and after the last known section, respectively.
 When the placement directive is omitted, it defaults to :math:`\T{(after~last)}`.
 

proposals/annotations/Overview.md

@@ -41,6 +41,31 @@ Extend the Appendix on the Custom Sections:
   They may be placed after the binder for any construct that can be named by the name section.
 
 * Define annotation syntax expressing arbitrary custom sections; cf. https://gist.github.com/binji/d1cfff7faaebb2aa4f8b1c995234e5a0
+
+  With that, a custom section annotation is specified as follows:
+  ```
+  custom ::= '(' '@custom' string place? datastring ')'
+  place ::=
+    | '(' 'before' section ')'
+    | '(' 'after' section ')'
+    | '(' 'before' 'first' ')'
+    | '(' 'after' 'last' ')'
+  section ::=
+    | 'type'
+    | 'import'
+    | 'func'
+    | 'table'
+    | 'memory'
+    | 'global'
+    | 'export'
+    | 'start'
+    | 'elem'
+    | 'code'
+    | 'data'
+    | 'datacount'
+  ```
+  If placement relative to an explicit section is used, then that section must exist in the encoding of the annotated module.
+
   As with any matter concerning annotations, it is up to implementations how they handle the case where an explicit custom section overlaps with individual annotations that are associated with the same custom section.