Expressions.md

@@ -154,15 +154,22 @@ unsigned<w1> u1; unsigned<w2> u2;
 | `s1 / u2` | | `signed<wr>`, *wr* = *w1* |
 | `u1 / s2` | | `signed<wr>`, *wr* = *w1* + 1 |
 
-### Modulus
+### Modulus/Remainder
 | Expression | Conditions | Result type |
 | :--------- | :--------- | :---------- |
 | `u1 % u2` | | `unsigned<wr>`, *wr* = min(*w1*, *w2*) |
 | `s1 % s2` | | `signed<wr>`, *wr* = min(*w1*, *w2*) |
 | `s1 % u2` | | `signed<wr>`, *wr* = min(*w1*, *w2* + 1) |
-| `u1 % s2` | | `unsigned<wr>`, *wr* = min(*w1*, *w2* - 1)|
+| `u1 % s2` | *w2* > 1 | `unsigned<wr>`, *wr* = min(*w1*, *w2* - 1) |
+| `u1 % s2` | *w2* = 1 | `unsigned<1>`|
 
-*TODO(jopperm):* Specify concrete semantics for this operation (as modulo is always contentious), and check the `u1 % s2` case as it may yield an (invalid!) `unsigned<0>` type.
+The `%` operator is defined (as in C) to satisfy the following formula:
+```
+      a = ⌊a/b⌋ * b + a%b
+<=> a%b = a - ⌊a/b⌋ * b
+```
+
+As a `signed<1>` divisor can only be -1 or 0, the only non-error outcome in the last case is 0. To retain consistency with the type rules for the literal 0, the result type is special-cased to `unsigned<1>`.
 
 ### Bitwise AND, OR, XOR
 Let `X` be either `&`, `|` or `^`.