Dates, Times, and Property Testing

Introduction

The Gregorian calendar is a royal pain in the arse.

It was introduced in 1582, as a closer approximation of the solar year.

The Gregorian leap year rule is: Every year that is exactly divisible by four is a leap year, except for years that are exactly divisible by 100, but these centurial years are leap years if they are exactly divisible by 400.

Source: Introduction to Calendars, US Naval Observatory

Wonderful.

Computers often use a simpler system called Unix time.

It measures the number of non-leap seconds that have elapsed since 00:00:00 UTC on 1 January 1970, which is known as the 'Unix epoch'.

Developers often need to translate between Unix time and Gregorian time, and every major programming language has a standard library to do this.

But is it possible to achieve inside a smart contract?

A Brilliant Paper

I stumbled on a paper called 'chrono-Compatible Low-Level Date Algorithms' by Howard Hinnant.

Interestingly, he's the lead C++ developer for the Ripple blockchain.

As one StackOverflow user quipped, the paper goes into 'excruciating detail' about efficient algorithms for converting between Unix time and Gregorian time.

My aim is to implement the civil_from_days algorithm in an Algorand smart contract.

If you want to understand it properly, I would recommend reading the paper.

It's certainly not something that makes intuitive sense.

The Function

The function we're going to implement takes a Unix timestamp as an argument, and returns a (year, month, day) triple:

$$f(s) = (y, m, d)$$

Each variable will be represented as a uint64, which means it's limited to the range \([0, \ 2^{64}-1]\):

$$f : uint64 \to (uint64, \ uint64, \ uint64)$$

The Contract Outline

The smart contract will be written in Algorand Python.

It will have a single method (to_date), which can be called from off-chain code or from another smart contract.

We can define a type alias for the return type:

from typing import TypeAlias

YearMonthDay: TypeAlias = tuple[UInt64, UInt64, UInt64]

And define the method signature as:

@arc4.abimethod
def to_date(self, timestamp: UInt64) -> YearMonthDay:
    ...

The Algorithm

The implementation will deviate slightly from Howard's approach.

He uses a proleptic Gregorian calendar, which extends back prior to 1582, and even includes negative years.

Times prior to the Unix epoch are represented with negative numbers.

But for use within a smart contract, we only really care about the Gregorian date of a block's Unix timestamp.

Negative numbers can be abandoned, and we can implement the desired algorithm using unsigned integers.

I'll follow the variable naming conventions in Howard's implementation, for the most part.

The first step is to convert the timestamp (seconds since the epoch) into the number of days since the epoch:

# Number of days since 1970-01-01
z = timestamp // 86400

Then, we offset the epoch from 1970-01-01 to 0000-03-01:

# Shift the epoch from 1970-01-01 to 0000-03-01
z += 719468

These algorithms internally assume that March 1 is the first day of the year. This is convenient because it puts the leap day, Feb. 29 as the last day of the year, or actually the preceding year... This detail is only important for understanding how the algorithm works, and is not exposed to the client of these algorithms.

Source: chrono-Compatible Low-Level Date Algorithms

Next, we calculate the era.

In these algorithms, an era is a 400 year period. As it turns out, the civil calendar exactly repeats itself every 400 years. And so these algorithms will first compute the era of a year/month/day triple, or the era of a serial date, and then factor the era out of the computation.

Source: chrono-Compatible Low-Level Date Algorithms

Each era is exactly 146,097 days long.

Howard's code caters for negative numbers:

const Int era = (z >= 0 ? z : z - 146096) / 146097

But we don't need to worry about that. So it's simply:

era = z // 146097

Then we can calculate the day of the era that z corresponds to, which is always a number in the range \([0, 146096]\):

doe = z - era * 146097

And the year of the era, which is always in the range \([0, 399]\):

yoe = (doe - doe // 1460 + doe // 36524 - doe // 146096) // 365

If you're getting lost at this point, don't worry.

It's all explained in the paper.

The algorithm devolves into madness and magic from here on out, so I'm going to skip ahead and show the final product:

def to_date(self, timestamp: UInt64) -> YearMonthDay:
    """Converts a Unix timestamp to a Gregorian date.

    Args:
        timestamp (UInt64): The Unix timestamp to convert.

    Returns:
        YearMonthDay: The Gregorian date as a (year, month, day) triple.
    """
    # Number of days since 1970-01-01
    z = timestamp // 86400
    # Shift the epoch from 1970-01-01 to 0000-03-01
    z += 719468
    era = z // 146097
    doe = z - era * 146097  # [0, 146096]
    yoe = (doe - doe // 1460 + doe // 36524 - doe // 146096) // 365  # [0, 399]
    y = yoe + era * 400
    doy = doe - (365 * yoe + yoe // 4 - yoe // 100)  # [0, 365]
    mp = (5 * doy + 2) // 153  # [0, 11]
    d = doy - (153 * mp + 2) // 5 + 1  # [1, 31]
    m = mp + 3 if mp < 10 else mp - 9  # [1, 12]
    return y + (UInt64(1) if m <= 2 else UInt64(0)), m, d

In case you're wondering about the last line... this isn't supported yet, at least not in the version of Algorand Python I'm using:

y + (m <= 2), m, d

Now, onto something interesting!

Property Testing

Property testing is a gift from the functional programming world.

It has a declarative feel - you tell the computer what to test, not how to test it.

Instead of checking that specific inputs produce specific outputs, the developer states the properties that a function should satisfy.

The computer then tests that the properties hold for a large number of inputs.

As such, it can be a great way to find edge cases that you may not have thought of.

Property testing seems like a natural fit for smart contracts, so let's explore a simple example.

Imagine we want to check that addition is commutative.

The most basic test in pytest might be:

import pytest

def test_addition_is_commutative() -> None:
    assert 1 + 2 == 2 + 1

And we can parameterise it to test more inputs:

import pytest

@pytest.mark.parametrize("x, y", [(1, 2), (10, 20)])
def test_addition_is_commutative(x: int, y: int) -> None:
    assert x + y == y + x

But what if we want to check that the commutative property holds for all integers?

It would be extremely tedious to specify a sufficient number of inputs for testing.

Fortunately, Python has a wonderful library called Hypothesis that can generate the test cases for us:

from hypothesis import given, strategies as st

@given(st.integers(), st.integers())
def test_addition_is_commutative(x: int, y: int) -> None:
    assert x + y == y + x

It works by generating arbitrary data matching your specification and checking that your guarantee still holds in that case. If it finds an example where it doesn’t, it takes that example and cuts it down to size, simplifying it until it finds a much smaller example that still causes the problem. It then saves that example for later, so that once it has found a problem with your code it will not forget it in the future.

Source: Welcome to Hypothesis!

We can apply the same concept to test that our smart contract's to_date method matches Python's datetime library for a huge range of input timestamps.

Writing Tests

The test cases could either be generated as integers or as datetime objects.

I'm going to opt for the latter, because Hypothesis will automatically check for calendric edge cases like leap seconds.

from hypothesis import given, settings, strategies as st

@settings(deadline=None)
@given(st.datetimes(min_value=datetime(1970, 1, 1)))
def test_to_date(app_client: TimeClient, _datetime: datetime) -> None:
    """Tests the `to_date` method.

    Args:
        app_client (TimeClient): The smart contract app client.
        _datetime (datetime): The datetime to test.
    """
    dt = _datetime.replace(tzinfo=timezone.utc)
    app_value = tuple(app_client.to_date(timestamp=int(dt.timestamp())).return_value)
    reference_value = (dt.year, dt.month, dt.day)
    assert app_value == reference_value

When executed, Hypothesis whirs away running hundreds of tests in search for an input where the property does not hold.

The datetime objects passed from Hypothesis are naive by default, so make sure the timezone is set to UTC before calling the timestamp method.

I chose to disable the deadline (timeout) for the tests, because the execution time can be quite varied.

The Complete Contract Code

The code below is also available on GitHub.

from typing import TypeAlias

from algopy import (
    ARC4Contract,
    UInt64,
    arc4,
)

YearMonthDay: TypeAlias = tuple[UInt64, UInt64, UInt64]


class Time(ARC4Contract):
    """A contract that converts between Unix time and Gregorian time."""

    @arc4.abimethod
    def to_date(self, timestamp: UInt64) -> YearMonthDay:
        """Converts a Unix timestamp to a Gregorian date.

        Args:
            timestamp (UInt64): The Unix timestamp to convert.

        Returns:
            YearMonthDay: The Gregorian date as a (year, month, day) triple.
        """
        # Number of days since 1970-01-01
        z = timestamp // 86400
        # Shift the epoch from 1970-01-01 to 0000-03-01
        z += 719468
        era = z // 146097
        doe = z - era * 146097  # [0, 146096]
        yoe = (doe - doe // 1460 + doe // 36524 - doe // 146096) // 365  # [0, 399]
        y = yoe + era * 400
        doy = doe - (365 * yoe + yoe // 4 - yoe // 100)  # [0, 365]
        mp = (5 * doy + 2) // 153  # [0, 11]
        d = doy - (153 * mp + 2) // 5 + 1  # [1, 31]
        m = mp + 3 if mp < 10 else mp - 9  # [1, 12]
        return y + (UInt64(1) if m <= 2 else UInt64(0)), m, d

The Complete Test Code

The code below are also available on GitHub.

from datetime import datetime, timezone

import algokit_utils
import pytest
from algokit_utils import (
    get_localnet_default_account,
)
from algokit_utils.config import config
from algosdk.v2client.algod import AlgodClient
from algosdk.v2client.indexer import IndexerClient
from hypothesis import given, settings
from hypothesis import strategies as st

from smart_contracts.artifacts.time.client import TimeClient


@pytest.fixture(scope="session")
def app_client(algod_client: AlgodClient, indexer_client: IndexerClient) -> TimeClient:
    config.configure(
        debug=True,
        # trace_all=True,
    )

    account = get_localnet_default_account(algod_client)

    client = TimeClient(
        algod_client,
        creator=account,
        indexer_client=indexer_client,
    )

    client.deploy(
        on_schema_break=algokit_utils.OnSchemaBreak.AppendApp,
        on_update=algokit_utils.OnUpdate.AppendApp,
    )

    return client


@settings(deadline=None)
@given(st.datetimes(min_value=datetime(1970, 1, 1)))
def test_to_date(app_client: TimeClient, _datetime: datetime) -> None:
    """Tests the `to_date` method.

    Args:
        app_client (TimeClient): The smart contract app client.
        _datetime (datetime): The datetime to test.
    """
    dt = _datetime.replace(tzinfo=timezone.utc)
    app_value = tuple(app_client.to_date(timestamp=int(dt.timestamp())).return_value)
    reference_value = (dt.year, dt.month, dt.day)
    assert app_value == reference_value