tutorial.dl

/*
 * Example: "Hello, world!" in Datalog
 */

// Category type with two type constructors.  Since constructors have
// no arguments, this is similar to a C enum.
typedef Category = CategoryStarWars
                 | CategoryOther

// Declare two input relations (the `input` keyword indicates that
// these relations can only be populated by input facts and cannot
// appear in the head of a rule).
// `string` is a primitive type in ddlog.
input relation Word1(word: string, cat: Category)
input relation Word2(word: string, cat: Category)

// Computed relation populated by facts derived from rules.
output relation Phrases(phrase: string)

// Produce phrases by combining pairs of words from the same category.
// The `++` operator is string concatenation.
Phrases(w1 ++ " " ++ w2) :- Word1(w1, cat), Word2(w2, cat).

// Let's add some static facts
Word1("Hello,", CategoryOther).
Word2("World!", CategoryOther).


/*
 * Example: Map hosts to IP subnets.
 */

// Type aliases improve readability.
typedef UUID    = bit<128>
typedef IP4     = bit<32>
typedef NetMask = bit<32>

// IP host specified by its name and address.
input relation Host(id: UUID, name: string, ip: IP4)

// IP subnet specified by its IP prefix and mask
input relation Subnet(id: UUID, prefix: IP4, mask: NetMask)

// HostInSubnet relation maps hosts to known subnets
output relation HostInSubnet(host: UUID, subnet: UUID)

// Compute `HostInSubnet` by filtering all host-subnet pairs where host address matches
// subnet prefix and mask.
//
// Note the use of wildcard (`_`) for fields that are not relevant in this rule.
//
// Note: ddlog computes this space efficiently by applying the
// filter at the same time as it computes Cartesian product of `Host` and
// `Subnet` relations.
HostInSubnet(host_id, subnet_id) :- Host(host_id, _, host_ip),
                                    Subnet(subnet_id, subnet_prefix, subnet_mask),
                                    ((host_ip & subnet_mask) == subnet_prefix).    // filter condition


/*
 * Example: Strings
 */

input relation Number(n: bigint)
output relation Pow2(p: string)

Pow2("The square of ${x} is ${x*x}") :- Number(x).

typedef ip_addr_t = IPAddr{addr: bit<32>}
typedef mac_addr_t = MACAddr{addr: bit<48>}

function to_string(ip: ip_addr_t): string {
    "${ip.addr[31:24]}.${ip.addr[23:16]}.${ip.addr[15:8]}.${ip.addr[7:0]}"
}

function to_string(mac: mac_addr_t): string {
    "${hex(mac.addr[47:40])}:${hex(mac.addr[39:32])}:${hex(mac.addr[31:24])}:\
    \${hex(mac.addr[23:16])}:${hex(mac.addr[15:8])}:${hex(mac.addr[7:0])}"
}

typedef nethost_t = NHost {
    ip:  ip_addr_t,
    mac: mac_addr_t
}

function to_string(h: nethost_t): string {
    "Host: IP=${h.ip}, MAC=${h.mac}"
}

input relation NetHost(id: bigint, h: nethost_t)
output relation NetHostString(id: bigint, s: string)

NetHostString(id, "${h}") :- NetHost(id, h).

/*
 * Example: arithmetics
 */

// Form IP address from bytes using bit vector concatenation
function ip_from_bytes(b3: bit<8>, b2: bit<8>, b1: bit<8>, b0: bit<8>)
    : ip_addr_t
{
    IPAddr{.addr = b3 ++ b2 ++ b1 ++ b0}
}

// Check for multicast IP address using bit slicing
function is_multicast_addr(ip: ip_addr_t): bool { ip.addr[31:28] == 14 }

input relation Bytes(b3: bit<8>, b2: bit<8>, b1: bit<8>, b0: bit<8>)
output relation Address(addr: ip_addr_t)
output relation MCastAddress(addr: ip_addr_t)

Address(ip_from_bytes(b3,b2,b1,b0)) :- Bytes(b3,b2,b1,b0).
MCastAddress(a) :- Address(a), is_multicast_addr(a).

/*
 * Example: control flow
 */

function addr_port(ip: ip_addr_t,
                   proto: string,
                   preferred_port: bit<16>): string {
    var port: bit<16> =
        match (proto) {
            "FTP"   -> 20,
            "HTTPS" -> 443,
            _       -> {
                if (preferred_port != 0)
                    preferred_port
                else
                    return "${ip}:80" // assume HTTP
            }
        };
    "${ip}:${port}"
}

input relation Endpoint(ip: ip_addr_t,
                        proto: string,
                        preferred_port: bit<16>)

output relation EndpointString(s: string)

EndpointString(addr_port(ip, proto, preferred_port)) :-
    Endpoint(ip, proto, preferred_port).

/*
 * Example: extern functions
 */
extern function string_slice_unsafe(x: string, from: bit<64>, to: bit<64>): string

output relation First5(str: string)

First5(string_slice_unsafe(p, 0,5)) :- Phrases(p).

/*
 * Example: closures.
 */

import vec

function times2(x: s64): s64 {
    x << 1
}

function vector_times2(v: Vec<s64>): Vec<s64> {
    // Pass function `times2` as an argument to `map`.
    v.map(times2)
}

function vector_times_n(v: Vec<s64>, n: s64): Vec<s64> {
    v.map(|x| x * n)
}

relation Closures(f: |u64|: string)

Closures(|x| "closure1: ${x}").
Closures(|x| "closure2: ${x}").

relation Arguments(arg: u64)

// Apply all closures in `Closures` to all values in `Arguments`.
output relation ClosuresXArguments(arg: u64, res: string)

ClosuresXArguments(arg, f(arg)) :- Closures(f), Arguments(arg).

function test_vector_transformers(): u64 {
    var vec = [[1,2,3], [4,5,6], [7]];

    /* Remove entries in with less than 2 elements;
     * truncate remaining entries and flatten them into a 1-dimensional
     * vector; compute the sum of elements in the resulting vector. 
     * 
     * Comments in the end of each line show the output of
     * each transformation. */
    vec.filter(|v| v.len() > 1)   // [[1,2,3], [4,5,6]]
       .flatmap(|v| {
           var res = v;
           res.truncate(2);
           res
        }) // [1,2,4,5]
       .fold(|acc, x| acc + x, 0) // 12
}

/*
 * Example: assignment clauses and antijoins
 */
input relation Blocklisted(ep: string)
output relation SanitizedEndpoint(ep: string)

SanitizedEndpoint(endpoint) :-
    Endpoint(ip, proto, preferred_port),
    var endpoint = addr_port(ip, proto, preferred_port),
    not Blocklisted(endpoint).

/*
 * Example: @-bindings.
 */
typedef Book = Book {
    author: string,
    title: string
}

input relation Library(book: Book)
input relation Author(name: string, born: u32)

output relation BookByAuthor(book: Book, author: Author)

BookByAuthor(b, author) :-
    // Variable `b` will be bound to the entire `Book` struct;
    // `author_name` will be bound to `b.author`.
    Library(.book = b@Book{.author = author_name}),
    author in Author(.name = author_name).

/*
 * Example: recursion
 * (see path.dl)
 */

/*
 * Example: FlatMap, extern functions
 */

function split_ip_list(x: string): Vec<string> {
   split(x, " ")
}

input relation HostAddress(host: bit<64>, addrs: string)
output relation HostIP(host: bit<64>, addr: string)

HostIP(host, addr) :- HostAddress(host, addrs),
                      var addr = FlatMap(split_ip_list(addrs)).

function vsep(strs: Vec<string>): string {
    var res = "";
    for (s in strs) {
        res = res ++ s ++ "\n";
    };
    res
}

output relation HostIPVSep(host: bit<64>, addrs: string)

HostIPVSep(host, vaddrs) :- HostAddress(host, addrs),
                            var vaddrs = vsep(split_ip_list(addrs)).

/*
 * Example: `continue` and `break` statements.
 */

// Returns only even elements of the vector.
function evens(vec: Vec<bigint>): Vec<bigint> {
    var res: Vec<bigint> = vec_empty();
    for (x in vec) {
        if (x % 2 != 0) { continue };
        vec_push(res, x);
    };
    res
}

input relation EvensAndOdds(vec: Vec<bigint>)
output relation Evens(evens_and_odds: Vec<bigint>, evens: Vec<bigint>)

Evens(vec, evens(vec)) :- EvensAndOdds(vec).

// Returns prefix of `vec` before the first occurrence of value `v`.
function prefixBefore(vec: Vec<'A>, v: 'A): Vec<'A> {
    var res: Vec<'A> = vec_empty();
    for (x in vec) {
        if (x == v) { break };
        vec_push(res, x);
    };
    res
}

input relation Vect(vec: Vec<string>, sep: string)
output relation Prefix(vec: Vec<string>)

Prefix(prefixBefore(vec, sep)) :- Vect(vec, sep).

/*
 * Example: Multiple heads
 */
input relation X(x: bit<16>)

output relation Sum(x: bit<16>, y: bit<16>, sum: bit<16>)
output relation Product(x: bit<16>, y: bit<16>, prod: bit<16>)

Sum(x,y,x+y),
Product(x,y,x*y) :- X(x), X(y).

/*
 * Example: group_by
 */

import group

input relation Price(item: string, vendor: string, price: u64)
output relation BestPrice(item: string, price: u64)

BestPrice(item, best_price) :-
    Price(.item = item, .price = price),
    var group: Group<string, u64> = price.group_by(item),
    var best_price = group.min().

output relation WorstPrice(item: string, price: u64)

WorstPrice(item, best_price) :-
    Price(.item = item, .price = price),
    var best_price = price.group_by(item).max().

output relation BestVendor(item: string, vendor: string, price: u64)

BestVendor(item, best_vendor, best_price) :-
    Price(item, vendor, price),
    (var best_vendor, var best_price) = (vendor, price).group_by(item).arg_min(|vendor_price| vendor_price.1).

function best_vendor_string(g: Group<string, (string, u64)>): string
{
    var min_vendor = "";
    var min_price = 'hffffffffffffffff;
    for (((vendor, price), _) in g) {
        if (price < min_price) {
            min_vendor = vendor;
            min_price = price;
        }
    };
    "Best deal for ${group_key(g)}: ${min_vendor}, $${min_price}"
}

import inspect_log as log

output relation BestDeal(best: string)
BestDeal(best) :-
    Price(item, vendor, price),
    Inspect log::log("../tutorial.log", "ts:${ddlog_timestamp}, w:${ddlog_weight}: Price(item=\"${item}\", vendor=\"${vendor}\", price=${price})"),
    var best = (vendor, price).group_by(item).best_vendor_string(),
    Inspect log::log("../tutorial.log", "ts:${ddlog_timestamp}, w:${ddlog_weight}: best(\"${item}\")=\"${best}\"").


/*
 * Example: primary key.
 */

input relation Article(author: string, title: string, year: u16, pages: usize)
primary key (x) (x.author, x.title)

// Output relation to mirror the contents of `Article`.
output relation OutArticle[Article]
OutArticle[a] :- a in Article().

/*
 * Example: multisets.
 */

input multiset MSetIn(x: u32)
output multiset MSetOut(x: u32)

MSetOut(x) :- MSetIn(x).

/*
 * Example: streams.
 */

input relation ZipCodes(zip: u32, city: string)
input stream Parcel(zip: u32, weight: usize)

// Add the name of the destination city to each parcel.
output stream ParcelCity(zip: u32, city: string, weight: usize)
ParcelCity(zip, city, weight) :-
    Parcel(zip, weight),
    ZipCodes(zip, city).

output stream ParcelWeight(zip: u32, total_weight: usize)

// Streaming group_by: aggregates parcel weights for each individual transaction.
ParcelWeight(zip, total_weight) :-
    Parcel(zip, weight),
    var total_weight = weight.group_by(zip).sum_with_multiplicities().

function sum_with_multiplicities(g: Group<u32, usize>): usize {
    var s = 0;
    for ((v, m) in g) {
        s = s + v * (m as usize)
    };
    s
}

/* Aggregate the contents of the Parcel stream over time. */

// The ParcelFold relation contains aggregated parcel weights from all earlier
// transactions and the new Parcel records add by the last transaction.
relation ParcelFold(zip: u32, weight: usize)

// Add aggregated pacel weight from previous transactions.
ParcelFold(zip, total_past_weight) :- ParcelWeightAggregated-1(zip, total_past_weight).
// Add new parcels from the last transaction.
ParcelFold(zip, weight) :- Parcel'(zip, weight).

// Group and aggregate weights in the ParcelFold relation.
output relation ParcelWeightAggregated(zip: u32, weight: usize)

ParcelWeightAggregated(zip, total_weight) :-
    ParcelFold(zip, weight),
    var total_weight = weight.group_by(zip).sum_with_multiplicities().


/*
 * Example: tagged unions
 */

typedef ip4_addr_t = bit<32>
typedef ip6_addr_t = bit<128>

typedef eth_pkt_t = EthPacket { src     : bit<48>
                              , dst     : bit<48>
                              , payload : eth_payload_t}

typedef eth_payload_t = EthIP4   {ip4 : ip4_pkt_t}
                      | EthIP6   {ip6 : ip6_pkt_t}
                      | EthOther

typedef ip4_pkt_t = IP4Pkt { ttl      : bit<8>
                           , src      : ip4_addr_t
                           , dst      : ip4_addr_t
                           , payload  : ip_payload_t}

typedef ip6_pkt_t = IP6Pkt { ttl     : bit<8>
                           , src     : ip6_addr_t
                           , dst     : ip6_addr_t
                           , payload : ip_payload_t}

typedef ip_payload_t = IPTCP   { tcp : tcp_pkt_t}
                     | IPUDP   { udp : udp_pkt_t}
                     | IPOther

typedef tcp_pkt_t = TCPPkt { src   : bit<16>
                           , dst   : bit<16>
                           , flags : bit<9> }

typedef udp_pkt_t = UDPPkt { src     : bit<16>
                           , dst     : bit<16>
                           , len     : bit<16>}


function tcp6_packet(ethsrc: bit<48>, ethdst: bit<48>,
                     ipsrc: ip6_addr_t, ipdst: ip6_addr_t,
                     srcport: bit<16>, dstport: bit<16>): eth_pkt_t
{
    EthPacket {
        // Explicitly name constructor arguments for clarity
        .src = ethsrc,
        .dst = ethdst,
        .payload = EthIP6 {
            // Omit argument name here
            IP6Pkt {
                .ttl = 10,
                .src = ipsrc,
                .dst = ipdst,
                .payload = IPTCP {
                    TCPPkt {
                        .src = srcport,
                        .dst = dstport,
                        .flags = 0
                    }
                }
            }
        }
    }
}

function pkt_ip4(pkt: eth_pkt_t): ip4_pkt_t {
    match (pkt) {
        EthPacket{.payload = EthIP4{ip4}} -> ip4,
        _                                 -> IP4Pkt{0,0,0,IPOther}
    }
}

function pkt_ip4_(pkt: eth_pkt_t): Option<ip4_pkt_t> {
    match (pkt) {
        EthPacket{.payload = EthIP4{ip4}} -> Some{ip4},
        _                                 -> None
    }
}


input relation Packet(pkt: eth_pkt_t)

output relation TCPDstPort(port: bit<16>)

TCPDstPort(port) :- Packet(EthPacket{.payload = EthIP4{IP4Pkt{.payload = IPTCP{TCPPkt{.dst = port}}}}}).
TCPDstPort(port) :- Packet(EthPacket{.payload = EthIP6{IP6Pkt{.payload = IPTCP{TCPPkt{.dst = port}}}}}).

function pkt_udp_port(pkt: eth_pkt_t): bit<16> {
    match (pkt) {
        EthPacket{.payload = EthIP4{IP4Pkt{.payload = IPUDP{UDPPkt{.dst = port}}}}} -> port,
        EthPacket{.payload = EthIP6{IP6Pkt{.payload = IPUDP{UDPPkt{.dst = port}}}}} -> port,
        _ -> 0
    }
}

output relation UDPDstPort(port: bit<16>)

UDPDstPort(port) :- Packet(pkt), var port = pkt_udp_port(pkt), port != 0.

function pkt_udp_port2(pkt: eth_pkt_t): Option<bit<16>> {
    match (pkt) {
        EthPacket{.payload = EthIP4{IP4Pkt{.payload = IPUDP{UDPPkt{.dst = port}}}}} -> Some{port},
        EthPacket{.payload = EthIP6{IP6Pkt{.payload = IPUDP{UDPPkt{.dst = port}}}}} -> Some{port},
        _ -> None
    }
}

output relation UDPDstPort2(port: bit<16>)

UDPDstPort2(port) :- Packet(pkt), Some{var port} = pkt_udp_port2(pkt).

/*
 * Example: tuples
 */

input relation KnownHost(addr: ip4_addr_t)

function addr_to_tuple(addr: ip4_addr_t): (bit<8>, bit<8>, bit<8>, bit<8>) {
    (addr[31:24], addr[23:16], addr[15:8], addr[7:0])
}

output relation IntranetHost(addr: ip4_addr_t)
IntranetHost(addr) :- KnownHost(addr),
                      (var b3, var b2, _, _) = addr_to_tuple(addr),
                      b3 == 192,
                      b2 == 168.

output relation IntranetHost2(addr: ip4_addr_t)
IntranetHost2(addr) :- KnownHost(addr), (192, 168, _, _) = addr_to_tuple(addr).

output relation IntranetHost3(addr: ip4_addr_t)
IntranetHost3(addr) :- KnownHost(addr),
                       var t = addr_to_tuple(addr),
                       t.0 == 192, t.1 == 168.

/*
 * Example: error handling.
 */

/* Lookup item in the inventory and return its price in cents. */
function get_price_in_cents(inventory: Map<string, string>, item: string): Option<u64> {
    match (inventory.get(item)) {
        None -> None,
        Some{price} -> match (parse_dec_u64(price)) {
                           None    -> None,
                           Some{p} -> Some{100 * p}
                       }
    }
}

/* As above, but returns 0 if the item is missing from the inventory or the price
 * string is invalid. */
function get_price_in_cents_unwrap(inventory: Map<string, string>, item: string): u64 {
    inventory.get(item).unwrap_or_default().parse_dec_u64().unwrap_or(0) * 100
}

/* get_price_in_cents written more concisely with the help of the `?` operator. */
function get_price_in_cents_(inventory: Map<string, string>, item: string): Option<u64> {
    Some{ inventory.get(item)?.parse_dec_u64()? * 100 }
}

function inventory(): Map<string, string> {
    map_singleton("Falcon 9", "62000000")
    .insert_imm("Soyuz", "180000000")
}

output relation PriceInCents(item: string, price1: Option<u64>, price2: u64, price3: Option<u64>)

PriceInCents("Falcon 9",
             inventory().get_price_in_cents("Falcon 9"),
             inventory().get_price_in_cents_unwrap("Falcon 9"),
             inventory().get_price_in_cents_("Falcon 9")).
PriceInCents("Atlantis",
             inventory().get_price_in_cents("Atlantis"),
             inventory().get_price_in_cents_unwrap("Atlantis"),
             inventory().get_price_in_cents_("Atlantis")).

/*
 * Example: explicit relation type
 */

input relation Person (name: string, nationality: string, occupation: string)

function is_target_audience(person: Person): bool {
    (person.nationality == "USA") and
    (person.occupation == "student")
}

output relation TargetAudience[Person]

TargetAudience[person] :- Person[person], is_target_audience(person).

/*
 * Example: references
 */
typedef student_id = bit<64>

input relation &School(name: string, address: string)
input relation &Student(id: student_id, name: string, school: string, sat_score: bit<16>)

relation StudentInfo(student: Ref<Student>, school: Ref<School>)

StudentInfo(student, school) :-
    student in &Student(.school = school_name),
    school in &School(.name = school_name).

output relation TopScore(school: string, top_score: bit<16>)

TopScore(school, top_score) :-
    StudentInfo(&Student{.sat_score = sat}, &School{.name = school}),
    var top_score = sat.group_by(school).max().

// Alternative syntax.
TopScore(school, top_score) :-
    StudentInfo(student, &School{.name = school}),
    var top_score = student.sat_score.group_by(school).max().

/*
 * Example: interned values
 */

input relation OnlineOrder(order_id: u64, item: istring)
output relation ItemInOrders(item: string, orders: Vec<u64>)

ItemInOrders(ival(item), orders) :-
    OnlineOrder(order, item),
    var orders = order.group_by(item).to_vec().

output relation OrderFormatted(order: string)

OrderFormatted(formatted) :-
    OnlineOrder(order, item),
    var formatted: string = "order: ${order}, item: ${ival(item)}".

output relation MilkOrders(order: u64)
MilkOrders(order) :- OnlineOrder(order, i"milk").

typedef StoreItem = StoreItem {
    name: string,
    description: istring
}

typedef IStoreItem = Intern<StoreItem>

input relation StoreInventory(item: IStoreItem)

output relation InventoryItemName(name: string)

InventoryItemName(name) :-
    StoreInventory(item),
    var name = ival(item).name.

/*
 * Example: Advanced features
 */

// The Load_Balancer relation instantiates Option type for strings.
input relation Load_Balancer (
    lb:           bigint, // bigint is a primitive ddlog type that models
                       // unbounded mathematical integers.
    ls:           bigint,
    ip_addresses: string,
    protocol:     Option<string>,
    name:         string
)

typedef stage_t = LS_IN_PRE_LB
                | LS_OUT_PRE_LB

input relation Logical_Switch (
    ls:  bigint
)

// Relation that represents OVS flows.
output relation Flow(lr: bigint,
                     stage: stage_t,
                     prio: bigint,
                     matchStr: string,
                     actionStr: string)

// The following rule illustrates several new syntactic constructs.
//
// 1. Note the use of named arguments in the head of the relation (e.g., `.stage=LS_IN_PRE_LB`).
//    This syntax is more verbose, but sometimes more readable especially for relations that have
//    several arguments.
// 2. Note the `$` syntax for string literals.  A string literal prefixed by `$` is an interpolated
//    string.  It can contain arbitrary ddlog expressions enclosed in `${}`.  These expressions are
//    automatically converted to string representation and concatenated with the rest of the string.
// 3. The body of the rule uses pattern matching to filter only those Load_Balancer records whose
//    protocol is specified (i.e., is not `None`).  Alternatively, one could match on a specific
//    protocol, e.g., TCP, by writing `Some{"TCP"}` instead of `Some{_}`.
Flow(.lr=ls,
     .stage=LS_IN_PRE_LB,
     .prio=100,
     .matchStr= "ip4.dst == ${addresses}",
     .actionStr="{ reg0[0] = 1; next; }")   :-
    Load_Balancer(_, ls, addresses, Some{_}, _).


Flow(.lr=ls,
     .stage=LS_OUT_PRE_LB,
     .prio=100,
     .matchStr="ip4",
     .actionStr="{ reg0[0] = 1; next; }") :-
    Logical_Switch(.ls=ls),
    Load_Balancer(.ls=ls).


// The above two rules can be equivalently written using FTL syntax.

// Introduce another Flow relation, so that we can compare the results of the two encodings.
output relation Flow1(lr: bigint,
                      stage: stage_t,
                      prio: bigint,
                      matchStr: string,
                      actionStr: string)

for (lb in Load_Balancer) {
    var a = lb.ip_addresses in
    match (lb.protocol) {
        Some{_} -> Flow1(lb.ls, LS_IN_PRE_LB, 100, "ip4.dst == ${a}", "{ reg0[0] = 1; next; }"),
        None -> {}
    }
}


for (ls in Logical_Switch) {
    for (lb in Load_Balancer if lb.ls == ls.ls) {
        Flow1(ls.ls, LS_OUT_PRE_LB, 100, "ip4", "{ reg0[0] = 1; next; }")
    }
}