Reformat some docs for GitHub.
diff --git a/doc/cpp-reference.md b/doc/cpp-reference.md
index 779d777..7938587 100644
--- a/doc/cpp-reference.md
+++ b/doc/cpp-reference.md
@@ -1,12 +1,10 @@
# Emboss C++ Generated Code Reference
-[TOC]
-
## `struct`s
A `struct` will have a corresponding view class, and functions to create views.
-### `Make`*`Struct`*`View` free function
+### <code>Make*Struct*View</code> free function
```c++
template <typename T>
@@ -61,26 +59,28 @@
auto MakeBarView(std::uint8_t x, std::int32_t y, T *container);
```
-The `Make`*`Struct`*`View` functions construct a view for *`Struct`* over the
-given bytes. For the data/size form, the type `T` must be a character type:
-`char`, `const char`, `unsigned char`, `const unsigned char`, `signed char`, or
-`const signed char`. For the container form, the container can be a
+The <code>Make*Struct*View</code> functions construct a view for *`Struct`*
+over the given bytes. For the data/size form, the type `T` must be a character
+type: `char`, `const char`, `unsigned char`, `const unsigned char`, `signed
+char`, or `const signed char`. For the container form, the container can be a
`std::vector`, `std::array`, or `std::basic_string` of a character type, or any
other type with a `data()` method that returns a possibly-`const` `char *`,
`signed char *`, or `unsigned char *`, and a `size()` method that returns a size
in bytes. Google's `absl::string_view` is one example of such a type.
If given a pointer to a `const` character type or a `const` reference to a
-container, `Make`*`Struct`*`View` will return a read-only view; otherwise
+container, <code>Make*Struct*View</code> will return a read-only view; otherwise
it will return a read-write view.
-The result of `Make`*`Struct`*`View` should be stored in an `auto` variable:
+The result of <code>Make*Struct*View</code> should be stored in an `auto`
+variable:
```c++
auto view = MakeFooView(byte_buffer, available_byte_count);
```
-The specific type returned by `Make`*`Struct`*`View` is subject to change.
+The specific type returned by <code>Make*Struct*View</code> is subject to
+change.
### `CopyFrom` method
@@ -405,7 +405,7 @@
assert(foo_view.bar().Read() == 100);
```
-As with `Make`*`Struct`*`View`, the exact return type of field methods is
+As with <code>Make*Struct*View</code>, the exact return type of field methods is
subject to change; if a field's view must be stored, use an `auto` variable.
Fields in anonymous `bits` are treated as if they were fields of the enclosing
@@ -424,9 +424,9 @@
uint8_t bar_value = foo_view.bar().Read();
```
-For each field, there is a `has_`*`field`*`()` method, which returns an object.
-`has_` methods are typically used for conditional fields. Suppose you have a
-`struct` like:
+For each field, there is a <code>has_*field*()</code> method, which returns an
+object. `has_` methods are typically used for conditional fields. Suppose you
+have a `struct` like:
```
struct Foo:
@@ -471,12 +471,12 @@
```
-### *`field`*`().Ok()` vs *`field`*`().IsComplete()` vs `has_`*`field`*`()`
+### <code>*field*().Ok()</code> vs <code>*field*().IsComplete()</code> vs <code>has_*field*()</code>
Emboss provides a number of methods to query different kinds of validity.
-`has_`*`field`*`()` is used for checking the existence condition specified in
-the `.emb` file:
+<code>has_*field*()</code> is used for checking the existence condition
+specified in the `.emb` file:
```
struct Foo:
@@ -529,15 +529,16 @@
assert(!incomplete_foo.has_y().ValueOr(false));
```
-`has_`*`field`*`()` is notional: it queries whether *`field`* *should* be
-present in the view. Even if `has_`*`field`*`().Value()` is `true`,
-*`field`*`().IsComplete()` and *`field`*`().Ok()` might return `false`.
+<code>has_*field*()</code> is notional: it queries whether *`field`* *should* be
+present in the view. Even if <code>has_*field*().Value()</code> is `true`,
+<code>*field*().IsComplete()</code> and *field*().Ok() might return `false`.
-*`field`*`().IsComplete()` tests if there are enough bytes in the backing
-storage to hold *`field`*. If *`field`*`().IsComplete()`, it is safe to call
-`Write()` on the field with a valid value for that field. *`field`*`().Ok()`
-tests if there are enough bytes in the backing storage to hold *`field`*, *and*
-that those bytes contain a valid value for *`field`*:
+<code>*field*().IsComplete()</code> tests if there are enough bytes in the
+backing storage to hold *`field`*. If <code>*field*().IsComplete()</code>, it
+is safe to call `Write()` on the field with a valid value for that field.
+<code>*field*().Ok()</code> tests if there are enough bytes in the backing
+storage to hold *`field`*, *and* that those bytes contain a valid value for
+*`field`*:
```
struct Bar:
@@ -571,7 +572,7 @@
Note that all views have `Ok()` and `IsComplete()` methods. A view of a
structure is `Ok()` if all of its fields are either `Ok()` or not present, and
-`has_`*`field`*`().Known()` is `true` for all fields.
+<code>has_*field*().Known()</code> is `true` for all fields.
A structure view `IsComplete()` if its `SizeIsKnown()` and its backing storage
contains at least `SizeInBits()` or `SizeInBytes()` bits or bytes. In other
@@ -595,7 +596,7 @@
The code generated for a `bits` construct is very similar to the code generated
for a `struct`. The primary differences are that there is no
-`Make`*`Bits`*`View` function and that `SizeInBytes` is replaced by
+<code>Make*Bits*View</code> function and that `SizeInBytes` is replaced by
`SizeInBits`.
diff --git a/doc/language-reference.md b/doc/language-reference.md
index 6084421..59126fa 100644
--- a/doc/language-reference.md
+++ b/doc/language-reference.md
@@ -392,8 +392,8 @@
Each parameter must have the form *name`:` type*. Currently, the *type* can
be:
-* `UInt:`*`n`*, where *`n`* is a number from 1 to 64, inclusive.
-* `Int:`*`n`*, where *`n`* is a number from 1 to 64, inclusive.
+* <code>UInt:*n*</code>, where *`n`* is a number from 1 to 64, inclusive.
+* <code>Int:*n*</code>, where *`n`* is a number from 1 to 64, inclusive.
* The name of an Emboss `enum` type.
`UInt`- and `Int`-typed parameters are integers with the corresponding range:
@@ -1372,8 +1372,9 @@
##### `?:`
-The `?:` operator, used like *`condition`*` ? `*`if_true`*` : `*`if_false`*,
-returns *`if_true`* if *`condition`* is `true`, otherwise *`if_false`*.
+The `?:` operator, used like <code>*condition* ? *if\_true* :
+*if\_false*</code>, returns *`if_true`* if *`condition`* is `true`, otherwise
+*`if_false`*.
Other than having stricter type requirements for its arguments, it behaves like
the C, C++, Java, JavaScript, C#, etc. conditional operator `?:` (sometimes
diff --git a/doc/modular_congruence_multiplication_proof.md b/doc/modular_congruence_multiplication_proof.md
deleted file mode 100644
index e69edfd..0000000
--- a/doc/modular_congruence_multiplication_proof.md
+++ /dev/null
@@ -1,100 +0,0 @@
-# Modular Congruence of the Product of Two Values with Known Modular Congruences
-
-(Draft)
-
-TODO(webstera): Try to simplify this proof.
-
-$$\text{If}$$
-
-$${a} \equiv {r} \pmod{{m}}$$
-
-$${b} \equiv {s} \pmod{{n}}$$
-
-$${a}, {r}, {m}, {b}, {s}, {n} \in ℤ$$
-
-$$\text{then}$$
-
-$${a}{b} \equiv {r}{s} \pmod{G\left(\dfrac{{m}}{G\left({m}, {r}\right)},
-\dfrac{{n}}{G\left({n}, {s}\right)}\right) \cdot G\left({m}, {r}\right) \cdot
-G\left({n}, {s}\right)}$$
-
-$$\text{where }G\text{ is the greatest common divisor function.}$$
-
-$$\text{Proof:}$$
-
-1. $$\exists {x} \in ℤ : {a} = {m}{x} + {r} \text{ by the definition of modular
- congruence}$$
-
-2. $$\exists {y} \in ℤ : {b} = {n}{y} + {s} \text{ by the definition of modular
- congruence}$$
-
-3. $$\text{Let }{q} = G\left({m}, {r}\right)$$
-
-4. $$\text{Let }{p} = G\left({n}, {s}\right)$$
-
-5. $$\text{Let }{z} = G\left(\dfrac{{m}}{{q}}, \dfrac{{n}}{{p}}\right) =
- G\left(\dfrac{{m}}{G\left({m}, {r}\right)}, \dfrac{{n}}{G\left({n},
- {s}\right)}\right)$$
-
-6. $${a} = {q}\left(\dfrac{{m}{x}}{q} + \dfrac{{r}}{q}\right) \text{ by
- multiplying } \dfrac{{q}}{{q}} \text{ and distributing }
- \dfrac{1}{{q}}$$
-
-7. $$\dfrac{{m}{x}}{q}, \dfrac{{r}}{q} \in ℤ \text{ by the definition of
- } {q} \text{ in (3) }$$
-
-8. $${b} = {p}\left(\dfrac{{n}{y}}{{p}} + \dfrac{{s}}{{p}}\right) \text{ by
- multiplying } \dfrac{{p}}{{p}} \text{ and distributing }
- \dfrac{1}{{p}}$$
-
-9. $$\dfrac{{n}{y}}{{p}}, \dfrac{{s}}{{p}} \in ℤ \text{ by the definition of
- } {p} \text{ in (4) }$$
-
-10. $${a} = {q}\left({z} \cdot \dfrac{{m}{x}}{{q}{z}} +
- \dfrac{{r}}{{q}}\right) \text{ by multiplying } \dfrac{{z}}{{z}}$$
-
-11. $$\dfrac{{m}{x}}{{q}{z}} \in ℤ \text{ by the definition of } {z} \text{ in
- (5) }$$
-
-12. $${b} = {p}\left({z} \cdot \dfrac{{n}{y}}{{p}{z}} +
- \dfrac{{s}}{{p}}\right) \text{ by multiplying } \dfrac{{z}}{{z}}$$
-
-13. $$\dfrac{{n}{y}}{{p}{z}} \in ℤ \text{ by the definition of } {z} \text{ in
- (5)}$$
-
-14. $${a}{b} = {q}{p}\left({z} \cdot \dfrac{{m}{x}}{{q}{z}} +
- \dfrac{{r}}{{q}}\right)\left({z} \cdot \dfrac{{n}{y}}{{p}{z}} +
- \dfrac{{s}}{{p}}\right) \text{ by (10) and (12)}$$
-
-15. $${a}{b} = {q}{p}\left({z}^2 \cdot \dfrac{{m}{x}}{{q}{z}} \cdot
- \dfrac{{n}{y}}{{p}{z}} + {z} \cdot \dfrac{{r}}{{q}} \cdot
- \dfrac{{n}{y}}{{p}{z}} + {z} \cdot \dfrac{{m}{x}}{{q}{z}} \cdot
- \dfrac{{s}}{{p}} + \dfrac{{r}}{{q}} \cdot \dfrac{{s}}{{p}}\right) \text{ by
- partially distributing (14)}$$
-
-16. $${a}{b} = {q}{p}\left({z}^2 \cdot \dfrac{{m}{x}}{{q}{z}} \cdot
- \dfrac{{n}{y}}{{p}{z}} + {z} \cdot \dfrac{{r}}{{q}} \cdot
- \dfrac{{n}{y}}{{p}{z}} + {z} \cdot \dfrac{{m}{x}}{{q}{z}} \cdot
- \dfrac{{s}}{{p}}\right) + {r}{s} \text{ by extracting the
- } \dfrac{{r}{s}}{{q}{p}} \text{ term from (15) and cancelling
- } \dfrac{{q}{p}}{{q}{p}}$$
-
-17. $${a}{b} = {q}{p}{z}\left({z} \cdot \dfrac{{m}{x}}{{q}{z}} \cdot
- \dfrac{{n}{y}}{{p}{z}} + \dfrac{{r}}{{q}} \cdot \dfrac{{n}{y}}{{p}{z}} +
- \dfrac{{m}{x}}{{q}{z}} \cdot \dfrac{{s}}{{p}}\right) + {r}{s} \text{ by
- factoring } {z} \text{ from (16)}$$
-
-18. $${z} \cdot \dfrac{{m}{x}}{{q}{z}} \cdot
- \dfrac{{n}{y}}{{p}{z}} + \dfrac{{r}}{{q}} \cdot \dfrac{{n}{y}}{{p}{z}} +
- \dfrac{{m}{x}}{{q}{z}} \cdot \dfrac{{s}}{{p}} \in ℤ \text{ because
- } {z}, \dfrac{{r}}{q}, \dfrac{{s}}{{p}}, \dfrac{{m}{x}}{{q}{z}},
- \dfrac{{n}{y}}{{p}{z}}, {z} \in ℤ \text{ per (5), (7), (9), (11),
- (13)}$$
-
-19. $${a}{b} \equiv {r}{s} \pmod{{q}{p}{z}} \text{ by the definition of
- modulus}$$
-
-20. $${a}{b} ≡ {r}{s} \pmod{G\left(\dfrac{{m}}{G\left({m}, {r}\right)},
- \dfrac{{n}}{G\left({n}, {s}\right)}\right) \cdot G\left({m}, {r}\right)
- \cdot G\left({n}, {s}\right)} \text{ by the definitions of } {q} \text{,
- } {p} \text{, and } {z} \text{ in (3), (4), and (5)}$$
diff --git a/doc/modular_congruence_multiplication_proof.pdf b/doc/modular_congruence_multiplication_proof.pdf
new file mode 100644
index 0000000..86c4aab
--- /dev/null
+++ b/doc/modular_congruence_multiplication_proof.pdf
Binary files differ
diff --git a/doc/modular_congruence_multiplication_proof.tex b/doc/modular_congruence_multiplication_proof.tex
new file mode 100644
index 0000000..10e9f31
--- /dev/null
+++ b/doc/modular_congruence_multiplication_proof.tex
@@ -0,0 +1,153 @@
+%This proof is used in Emboss to propagate alignment restrictions through
+%multiplication: if a and b are non-constant integers, their product can still
+%have a known alignment.
+%
+%Forgive me on the details and formatting, math majors, I never completed my
+%math degree. --bolms
+%
+%Thanks to Aaron Webster for helping me format this as an actual proof.
+\documentclass{article}
+\usepackage[utf8]{inputenc}
+\usepackage[english]{babel}
+\usepackage{amssymb,amsmath,amsthm}
+\title{Modular Congruence of the Product of Two Values with Known Modular Congruences}
+\author{Emboss Authors}
+\date{2017}
+
+\begin{document}
+\maketitle
+
+\section{Introduction}
+
+\newtheorem{theorem}{Theorem}
+
+%(Draft)
+%TODO(webstera): Try to simplify this proof.
+
+\begin{theorem}
+Given
+
+\begin{align*}
+ &{a} \equiv {r} \pmod{{m}} \\
+ &{b} \equiv {s} \pmod{{n}} \\
+ &{a}, {r}, {m}, {b}, {s}, {n} \in \mathbb{Z}
+\end{align*}
+
+then
+
+\begin{align*}
+ &{a}{b} \equiv {r}{s} \pmod{G\left(\dfrac{{m}}{G\left({m}, {r}\right)},
+\dfrac{{n}}{G\left({n}, {s}\right)}\right) \cdot G\left({m}, {r}\right) \cdot
+G\left({n}, {s}\right)}
+\end{align*}
+
+where $G$ is the greatest common divisor function.
+\end{theorem}
+
+\begin{proof}
+\begin{align}
+ \text{Let }{q} &= G\left({m}, {r}\right) \label{eq:qdef} \\
+ {p} &= G\left({n}, {s}\right) \label{eq:pdef} \\
+ {z} &= G\left(\dfrac{{m}}{{q}}, \dfrac{{n}}{{p}}\right) =
+ G\left(\dfrac{{m}}{G\left({m}, {r}\right)},
+ \dfrac{{n}}{G\left({n}, {s}\right)}\right) \label{eq:zdef}
+\end{align}
+
+by the definition of modular congruence:
+\begin{align}
+ &\exists {x} \in \mathbb{Z} : {a} = {m}{x} + {r} \\
+ &\exists {y} \in \mathbb{Z} : {b} = {n}{y} + {s}
+\end{align}
+
+multiplying $\dfrac{{q}}{{q}}$ and distributing $\dfrac{1}{{q}}$:
+\begin{align}
+ &{a} = {q}\left(\dfrac{{m}{x}}{q} + \dfrac{{r}}{q}\right)
+\end{align}
+
+by the definition of ${q}$ in \eqref{eq:qdef}:
+\begin{align}
+ &\dfrac{{m}{x}}{q}, \dfrac{{r}}{q} \in \mathbb{Z} \label{eq:rqinz}
+\end{align}
+
+multiplying $\dfrac{{p}}{{p}}$ and distributing $\dfrac{1}{{p}}$:
+\begin{align}
+ &{b} = {p}\left(\dfrac{{n}{y}}{{p}} + \dfrac{{s}}{{p}}\right)
+\end{align}
+
+by the definition of ${p}$ in \eqref{eq:pdef}:
+\begin{align}
+ &\dfrac{{n}{y}}{{p}}, \dfrac{{s}}{{p}} \in \mathbb{Z} \label{eq:spinz}
+\end{align}
+
+multiplying $\dfrac{{z}}{{z}}$:
+\begin{align}
+ &{a} = {q}\left({z} \cdot \dfrac{{m}{x}}{{q}{z}} + \dfrac{{r}}{{q}}\right) \label{eq:aeqq}
+\end{align}
+
+by the definition of ${z}$ in \eqref{eq:zdef}:
+\begin{align}
+ &\dfrac{{m}{x}}{{q}{z}} \in \mathbb{Z} \label{eq:mxqzinz}
+\end{align}
+
+multiplying $\dfrac{{z}}{{z}}$:
+\begin{align}
+ &{b} = {p}\left({z} \cdot \dfrac{{n}{y}}{{p}{z}} + \dfrac{{s}}{{p}}\right) \label{eq:beqp}
+\end{align}
+
+by the definition of ${z}$ in \eqref{eq:zdef}:
+\begin{align}
+ &\dfrac{{n}{y}}{{p}{z}} \in \mathbb{Z} \label{eq:nypzinz}
+\end{align}
+
+\eqref{eq:aeqq} and \eqref{eq:beqp}:
+\begin{align}
+ &{a}{b} = {q}{p}\left({z} \cdot \dfrac{{m}{x}}{{q}{z}} +
+ \dfrac{{r}}{{q}}\right)\left({z} \cdot \dfrac{{n}{y}}{{p}{z}} +
+ \dfrac{{s}}{{p}}\right) \label{eq:abeqqp}
+\end{align}
+
+partially distributing \eqref{eq:abeqqp}:
+\begin{align}
+ &{a}{b} = {q}{p}\left({z}^2 \cdot \dfrac{{m}{x}}{{q}{z}} \cdot
+ \dfrac{{n}{y}}{{p}{z}} + {z} \cdot \dfrac{{r}}{{q}} \cdot
+ \dfrac{{n}{y}}{{p}{z}} + {z} \cdot \dfrac{{m}{x}}{{q}{z}} \cdot
+ \dfrac{{s}}{{p}} + \dfrac{{r}}{{q}} \cdot \dfrac{{s}}{{p}}\right) \label{eq:abeqqpexp}
+\end{align}
+
+extracting the $\dfrac{{r}{s}}{{q}{p}}$ term from \eqref{eq:abeqqpexp} and cancelling $\dfrac{{q}{p}}{{q}{p}}$:
+\begin{align}
+ &{a}{b} = {q}{p}\left({z}^2 \cdot \dfrac{{m}{x}}{{q}{z}} \cdot
+ \dfrac{{n}{y}}{{p}{z}} + {z} \cdot \dfrac{{r}}{{q}} \cdot
+ \dfrac{{n}{y}}{{p}{z}} + {z} \cdot \dfrac{{m}{x}}{{q}{z}} \cdot
+ \dfrac{{s}}{{p}}\right) + {r}{s} \label{eq:abeqqpextr}
+\end{align}
+
+factoring ${z}$ from \eqref{eq:abeqqpextr}:
+\begin{align}
+ &{a}{b} = {q}{p}{z}\left({z} \cdot \dfrac{{m}{x}}{{q}{z}} \cdot
+ \dfrac{{n}{y}}{{p}{z}} + \dfrac{{r}}{{q}} \cdot \dfrac{{n}{y}}{{p}{z}} +
+ \dfrac{{m}{x}}{{q}{z}} \cdot \dfrac{{s}}{{p}}\right) + {r}{s}
+\end{align}
+
+because ${z}, \dfrac{{r}}{q}, \dfrac{{s}}{{p}}, \dfrac{{m}{x}}{{q}{z}},
+ \dfrac{{n}{y}}{{p}{z}} \in \mathbb{Z}$, per \eqref{eq:zdef}, \eqref{eq:rqinz}, \eqref{eq:spinz}, \eqref{eq:mxqzinz}, \eqref{eq:nypzinz}:
+\begin{align}
+ &{z} \cdot \dfrac{{m}{x}}{{q}{z}} \cdot \dfrac{{n}{y}}{{p}{z}} +
+ \dfrac{{r}}{{q}} \cdot \dfrac{{n}{y}}{{p}{z}} + \dfrac{{m}{x}}{{q}{z}} \cdot
+ \dfrac{{s}}{{p}} \in \mathbb{Z}
+\end{align}
+
+by the definition of modulus:
+\begin{align}
+ &{a}{b} \equiv {r}{s} \pmod{{q}{p}{z}}
+\end{align}
+
+by the definitions of ${q}$, ${p}$, and ${z}$ in \eqref{eq:qdef}, \eqref{eq:pdef}, and \eqref{eq:zdef}:
+\begin{align}
+ &{a}{b} \equiv {r}{s} \pmod{G\left(\dfrac{{m}}{G\left({m}, {r}\right)},
+ \dfrac{{n}}{G\left({n}, {s}\right)}\right) \cdot G\left({m}, {r}\right)
+ \cdot G\left({n}, {s}\right)}
+\end{align}
+
+\end{proof}
+\end{document}
diff --git a/doc/roadmap.md b/doc/roadmap.md
index 87ee2b3..3507046 100644
--- a/doc/roadmap.md
+++ b/doc/roadmap.md
@@ -84,8 +84,8 @@
## Finishing Refactoring Hacky Anonymous Bits Code {#del_anon_hack}
-Replace the final uses of *`name`*`.is_anonymous` with something that marks
-"anonymous" fields as "private."
+Replace the final uses of <code>*name*.is_anonymous</code> with something that
+marks "anonymous" fields as "private."
