From 869ac617436391baf44b5f065ee3bb6651321d15 Mon Sep 17 00:00:00 2001
From: Ferdinand Bachmann <theferdi265@gmail.com>
Date: Sun, 8 Sep 2019 22:13:31 +0200
Subject: [PATCH] epicardium/rtc: add explanation comment for numerically
 stable subsecond decode

---
 epicardium/modules/rtc.c | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/epicardium/modules/rtc.c b/epicardium/modules/rtc.c
index 630ece854..b563462db 100644
--- a/epicardium/modules/rtc.c
+++ b/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;
 }
 
-- 
GitLab