Prove HLC Preserves Causality Within Epsilon - The Timekeeper

                      TASK
                    

Implementation

HLC has a critical property: it preserves causality AND stays within a bounded distance (epsilon) of physical time. This is what makes it practical for systems like CockroachDB.

Properties to verify:

Causality: if event A happened-before event B, then hlc(A) < hlc(B)
Bounded drift: |hlc.pt - wall_clock| <= epsilon (use epsilon = 250ms)
NTP resilience: even if wall clock jumps backward, HLC moves forward

Implement a hlc_verify_bound handler that checks the epsilon invariant:

Request:  {"type": "hlc_verify_bound", "msg_id": 1, "epsilon_ms": 250}
Response: {"type": "hlc_verify_bound_ok", "in_reply_to": 1, "within_bound": true, "max_drift_ms": 0}

Also implement a hlc_ntp_correction handler that simulates a backward clock jump:

Request:  {"type": "hlc_ntp_correction", "msg_id": 2, "old_wall_ms": 2000, "new_wall_ms": 1900}
Response: {"type": "hlc_ntp_correction_ok", "in_reply_to": 2, "hlc_pt": 2000, "hlc_c": 1, "moved_backward": false}

Sample Test Cases

HLC stays within epsilon after normal ticksTimeout: 5000ms

Input

{"src":"c0","dest":"n1","body":{"type":"init","msg_id":1,"node_id":"n1","node_ids":["n1"]}}
{"src":"c1","dest":"n1","body":{"type":"hlc_tick","msg_id":2,"wall_clock_ms":1000}}
{"src":"c1","dest":"n1","body":{"type":"hlc_tick","msg_id":3,"wall_clock_ms":1100}}
{"src":"c1","dest":"n1","body":{"type":"hlc_verify_bound","msg_id":4,"epsilon_ms":250}}

Expected Output

{"src": "n1", "dest": "c0", "body": {"type": "init_ok", "in_reply_to": 1, "msg_id": 0}}

NTP backward correction does not move HLC backwardTimeout: 5000ms

Input

{"src":"c0","dest":"n1","body":{"type":"init","msg_id":1,"node_id":"n1","node_ids":["n1"]}}
{"src":"c1","dest":"n1","body":{"type":"hlc_tick","msg_id":2,"wall_clock_ms":2000}}
{"src":"c1","dest":"n1","body":{"type":"hlc_ntp_correction","msg_id":3,"old_wall_ms":2000,"new_wall_ms":1900}}

Expected Output

{"src": "n1", "dest": "c0", "body": {"type": "init_ok", "in_reply_to": 1, "msg_id": 0}}
{"src": "n1", "dest": "c1", "body": {"type": "hlc_tick_ok", "in_reply_to": 2, "pt": 2000, "c": 0, "msg_id": 1}}
{"src": "n1", "dest": "c1", "body": {"type": "hlc_ntp_correction_ok", "in_reply_to": 3, "hlc_pt": 2000, "hlc_c": 1, "moved_backward": false, "msg_id": 2}}

Hints

Hint 1▾

HLC always advances: it never goes backward even if physical clock does

Hint 2▾

The logical counter c is bounded because pt will eventually catch up

Hint 3▾

Epsilon (clock skew bound) limits how far HLC can drift from real time

Hint 4▾

Simulate NTP corrections by sending wall_clock_ms values that jump backward

Hint 5▾

Verify that HLC timestamp always stays within epsilon of the real wall clock

Resources

CockroachDB Architecture - Clock Synchronization

How CockroachDB uses HLC for distributed transaction ordering

                      OVERVIEW
                    

Theoretical Hub

Concept overview coming soon

Key Concepts

causality preservationclock skew boundNTP correctionepsilon bound

main.py

python