Work-in-progress non-racy dns txt reservation protocol Quint specification.

dns-reservation.qnt

module dns {
    type Server = str
    type Hostname = str
    type Pubkey = str
    type Option[a] =
        | Some(a)
        | None
    type Reservation = { hostname: Hostname, pubkey: Pubkey }

    pure val weirdKey = "weird"

    type SrvReserveState =
        | Idle
        | WantsReservation(Reservation)
        | CheckForExistingReservation(Reservation)
        | TryReserveRecord(Reservation)
        | ReservationSucceeded(Reservation)
        | ReservationFailed(Reservation)
    def serverIsIdle(server: Server): bool = 
        match srvStates.get(server) {
            | Idle => true
            | _ => false
        }
    def serverWantsReservation(server: Server): bool = 
        match srvStates.get(server) {
            | WantsReservation(_) => true
            | _ => false
        }
    def serverCheckingForExistingReservation(server: Server): bool = 
        match srvStates.get(server) {
            | CheckForExistingReservation(_) => true
            | _ => false
        }

    type DnsTxtRecord = { key: str, value: str, id: int }
    type DnsTxtRecords = List[DnsTxtRecord]

    type ViewedRecords = { hostname: Hostname, records: DnsTxtRecords }

    // The possible server instances ( or threads ) that could all be trying to reserve DNS entries at the same
    // time,
    pure val SERVERS = Set("alice", "bob", "charlie", "eva", "matthew", "jimmy")

    // The different usernames we might try to register
    pure val HOSTNAMES = Set("zicklag", "erlend", "sebadob", "anders")

    // The different public keys that a username might resolve to
    pure val PUBKEYS = Set("k1", "k2", "k3", "k4", "k5")

    // The actual DNS records as stored in, for example, cloudflare.
    var records: Hostname -> DnsTxtRecords

    // The latest list of records that each server has fetched from the DNS server
    var srvViewedRecords: Server -> Option[ViewedRecords]

    var srvStates: Server -> SrvReserveState

    // Combined state
    val state = { records: records, viewedRecords: srvViewedRecords, srvStates: srvStates }

    // TODO: add invariants
    val invariants = true

    action init = {
        all {
            records' = Map(),
            srvViewedRecords' = SERVERS.mapBy(srv => None),
            srvStates' = SERVERS.mapBy(s => Idle),
        }
    }

    action unchanged = all {
        records' = records,
        srvViewedRecords' = srvViewedRecords,
        srvStates' = srvStates,
    }

    action step = any {
        handleServerIdle,
        handleServerWantsRegistration,
        handleServerCheckForExistingRegistration,
    }

    // a user wants to try and map a username to a key
    action handleServerIdle = all {
        SERVERS.exists(serverIsIdle),
        {
            nondet server = oneOf(SERVERS.filter(serverIsIdle))
            nondet hostname = oneOf(HOSTNAMES)
            nondet pubkey = oneOf(PUBKEYS)
            all {
                records' = records,
                srvViewedRecords' = srvViewedRecords,
                srvStates' = srvStates.set(server, WantsReservation({ hostname: hostname, pubkey: pubkey })),
            }
        }            
    }

    action handleServerWantsRegistration = all {
        SERVERS.exists(serverWantsReservation),
        {
            nondet server = oneOf(SERVERS.filter(serverWantsReservation))
            match srvStates.get(server) {
                | WantsReservation(reservation) => all {
                    fetchRecords(server, reservation.hostname),
                    srvStates' = srvStates.set(server, CheckForExistingReservation(reservation)),
                    records' = records,
                }
                | _ => unchanged
            }
        }
    }

    action handleServerCheckForExistingRegistration = all {
        SERVERS.exists(serverCheckingForExistingReservation),
        {
        nondet server = oneOf(SERVERS.filter(serverCheckingForExistingReservation))
            match srvStates.get(server) {
                | CheckForExistingReservation(reservation) => {
                    match srvViewedRecords.get(server) {
                        | Some(existingRecords) => {
                            all {
                                existingRecords.hostname == reservation.hostname,

                                // Record not available
                                if (existingRecords.records.select(x => x.key == weirdKey).length() >= 1) {
                                    all {
                                        records' = records,
                                        srvStates' = srvStates.set(server, ReservationFailed(reservation)),
                                        srvViewedRecords' = srvViewedRecords,
                                    }

                                // Record is available
                                } else {
                                    all {
                                        records' = records,
                                        srvViewedRecords' = srvViewedRecords,
                                        srvStates' = srvStates.set(server, TryReserveRecord(reservation))
                                    }
                                }
                            }
                        }
                        | _ => unchanged
                    }
                }
                | _ => unchanged
            }
        }
    }

    action fetchRecords(server: Server, hostname: Hostname): bool = all {
        srvViewedRecords' = srvViewedRecords.set(
            server,
            if (hostname.in(records.keys())) {
                Some({ hostname: hostname, records: records.get(hostname) })
            } else {
                Some({ hostname: hostname, records: List() })
            }
        ),
    }
}