epicardium/rtc: add explanation comment for numerically stable subsecond decode

epicardium/modules/rtc.c

@@ -44,6 +44,22 @@ uint64_t epic_rtc_get_milliseconds(void)
 	while (RTC_GetTime(&sec, &subsec) == E_BUSY) {
 		vTaskDelay(pdMS_TO_TICKS(4));
 	}
+
+	// Without the bias of 999 (0.24 milliseconds), this decoding function is
+	// numerically unstable:
+	//
+	// Encoding 5 milliseconds into 20 subsecs (using the encoding function in
+	// epic_rtc_set_milliseconds) and decoding it without the bias of 999 yields
+	// 4 milliseconds.
+	//
+	// The following invariants should hold when encoding / decoding from and to
+	// milliseconds / subseconds:
+	//
+	// - 0 <= encode(ms) < 4096 for 0 <= ms < 1000
+	// - decode(encode(ms)) == ms for 0 <= ms < 1000
+	// - 0 <= decode(subsec) < 1000 for 0 <= subsec < 4096
+	//
+	// These invariants were proven experimentally.
 	return (subsec * 1000ULL + 999ULL) / 4096 + sec * 1000ULL;
 }