www

invariants-phantom.hl.rkt (30279B)

---

 #lang aful/unhygienic hyper-literate type-expander/lang
 
 @require[scribble-math
          scribble-enhanced/doc
          "notations.rkt"]
 
 @title[#:style (with-html5 manual-doc-style)
        #:tag "inv-phantom"
        #:tag-prefix "phc-graph/inv-phantom"]{Tracking checked contracts
  via refinement types}
 
 @(chunks-toc-prefix
   '("(lib phc-graph/scribblings/phc-graph-implementation.scrbl)"
     "phc-graph/inv-phantom"))
 
 @section{Introduction}
 
 The cautious compiler writer will no doubt want to check that the Abstract
 Syntax Tree or Graph used to represent the program verifies some structural
 properties. For example, the compiled language might not allow cycles between
 types. Another desirable property is that the @racket[in-method] field of the
 node representing an instruction points back to the method containing it. We
 will use this second property as a running example in this section.
 
 @section{Implementation overview : subtyping, variance and phantom types}
 
 It is possible to express with Typed/Racket that a @racket[Method] should
 contain a list of @racket[Instruction]s, and that @racket[Instruction]s should
 point to a @racket[Method]@note{We are not concerned here about the ability to
  create such values, which necessarily contain some form of cycle. The goal of
  the graph library is indeed to handle the creation and traversal of such
  cyclic data structures in a safe way}:
 
 @chunk[<invariant-1>
        (struct Instruction ([opcode : Byte]
                             [in-method : Method]))
        (struct Method ([body : (Listof Instruction)]))]
 
 This type does not, however, encode the fact that an instruction should point
 to the method containing it. Typed/Racket does not really have a notion of
 singleton types, aside from symbols and other primitive data. It also lacks a
 way to type "the value itself" (e.g. to describe a single-field structure
 pointing to itself, possibly via a @racket[Promise]). This means that the
 property could only be expressed in a rather contrived way, if it is at all
 possible.
 
 @; (define-type Self-Loop (∀ (A) (→ (Pairof Integer (Self-Loop A)))))
 
 We decide to rely instead on a run-time check, i.e. a sort of contract which
 checks the structural invariant on the whole graph. In order to let the
 type-checker know whether a value was checked against that contract or not, we
 include within the node a phantom type which is used as a flag, indicating
 that the graph was checked against that contract. This phantom type in a sense
 refines the node type, indicating an additional property (which, in our case,
 is not checked at compile-time but instead enforced at run-time).
 
 @chunk[<invariant-2>
        (struct (Flag) Instruction ([opcode : Byte]
                                    [in-method : (Method Flag)]))
        (struct (Flag) Method ([body : (Listof (Instruction Flag))]))]
 
 We would then write a function accepting a @racket[Method] for which the
 contract @racket[method→instruction→same-method] was checked like this:
 
 @chunk[<invariant-2-use>
        (λ ([m : (Method 'method→instruction→same-method)])
          …)]
 
 Unfortunately, this attempt fails to catch errors as one would expect, because
 Typed/Racket discards unused polymorphic arguments, as can be seen in the
 following example, which type-checks without any complaint:
 
 @chunk[<phantom-types-ignored>
        (struct (Phantom) S ([x : Integer]))
        (define inst-sa : (S 'a) (S 1))
        (ann inst-sa (S 'b))]
 
 We must therefore make a field with the @racket[Flag] type actually appear
 within the instance:
 
 @chunk[<invariant-3>
        (struct (Flag) Instruction ([opcode : Byte]
                                    [in-method : (Method Flag)]
                                    [flag : Flag]))
        (struct (Flag) Method ([body : (Listof (Instruction Flag))]
                               [flag : Flag]))]
 
 Another issue is that the flag can easily be forged. We would therefore like
 to wrap it in a struct type which is only accessible by the graph library:
 
 @chunk[<invariant-4>
        (struct (Flag) Flag-Wrapper-Struct ([flag : Flag]))
        (define-type Flag-Wrapper Flag-Wrapper-Struct)
        (code:comment "provide only the type, not the constructor or accessor")
        (provide Flag-Wrapper)]
 
 We would like to be able to indicate that a graph node has validated several
 invariants. For that, we need a way to represent the type of a "set" of
 invariant witnesses. We also want some subtyping relationship between the
 sets: a set @${s₁} with more invariant witnesses should be a subtype of a
 subset @${s₂ ⊆ s₁}. We can order the invariant witnesses and use @racket[Rec]
 to build the type of a list of invariant witnesses, where some may be missing:
 
 @chunk[<invariant-set-as-List+Rec>
        (define-type At-Least-InvB+InvD
          (Rec R₁ (U (Pairof Any R₁)
                     (Pairof 'InvB (Rec R₂ (U (Pairof Any R₂)
                                              (Pairof 'InvD (Listof Any))))))))]
 
 @chunk[<invariant-set-as-List+Rec-use>
        (ann '(InvA InvB InvC InvD InvE) At-Least-InvB+InvD)
        (ann '(InvB InvD) At-Least-InvB+InvD)
        (code:comment "Rejected, because it lacks 'InvD")
        (code:comment "(ann '(InvB InvC InvE) At-Least-InvB+InvD)")
        (code:comment "The elements must be in the right order,")
        (code:comment "this would be rejected by the typechecker:")
        (code:comment "(ann '(InvD InvB) At-Least-InvB+InvD)")]
 
 Another solution is to group the witnesses in an untagged union with
 @racket[U], and place it in a contravariant position:
 
 @chunk[<invariant-set-as-contravariant-U>
        (define-type At-Least-InvB+InvD
          (→ (U 'InvB 'InvD) Void))]
 
 In the case where no invariant is present in the untagged union, the type
 @racket[(U)] a.k.a @racket[Nothing], the bottom type with no value, would
 appear. This type is somewhat pathological and allows absurd reasoning (a
 function accepting @racket[Nothing] can never be called, which may incite the
 type checker to perform excessive elision). To avoid any pitfalls, we will
 systematically include a dummy element @racket[Or] in the union, to make sure
 the union never becomes empty.
 
 This solution also has the advantage that the size of the run-time witness is
 constant, and does not depend on the number of checked contracts (unlike the
 representation using a list). In practice the function should never be called.
 It can however simply be implemented, in a way which will match all witness
 types, as a function accepting anything and returning void.
 
 In addition to testifying that a graph node was checked against multiple,
 separate contracts, there might be some contracts which check stronger
 properties than others. A way to encode this relationship in the type system
 is to have subtyping relationships between the contract witnesses, so that
 @; TODO: get rid of the textit
 @${\textit{P}₁(x) ⇒ \textit{P}₂(x) ⇒ \textit{Inv}₁ @texsubtype \textit{Inv}₂}:
 
 @chunk[<invariant-contract-subtyping>
        (struct InvWeak ())
        (struct InvStrong InvWeak ())]
 
 If the witnesses must appear in a contravariant position (when using
 @racket[U] to group them), the relationship must be reversed:
 
 @chunk[<invariant-contract-subtyping>
        (struct InvStrongContra ())
        (struct InvWeakContra InvStrongContra ())]
 
 Alternatively, it is possible to use a second contravariant position to
 reverse the subtyping relationship again:
 
 @chunk[<invariant-contract-subtyping>
        (struct InvWeak ())
        (struct InvStrong InvWeak ())
 
        (define InvWeakContra (→ InvWeak Void))
        (define InvStrongContra (→ InvStrong Void))]
 
 Finally, we note that the invariants should always be represented using a
 particular struct type, instead of using a symbol, so that name clashes are
 not a problem.
 
 @section{Encoding property implication as subtyping}
 
 The witness for a strong property should be a subtype of the witness for a
 weaker property. This allows a node with a strong property to be passed where
 a node with a weaker property is passed.
 
 @chunk[<structural-draft>
        (code:comment "Draft ideas")
        
        (struct inv∈ ())
        (struct inv≡ ())
        (struct inv∉ ())
 
        ;(List Rel From Path1 Path2)
        (List ≡ ANodeName (List f1 f2) (List))
        (List ∈ ANodeName (List f1 f2) (List))
        (List ∉ ANodeName (List f1 f2) (List))
        (List ∉ ANodeName (List (* f1 f2 f3 f4) (* f5 f6)) (List))
 
        ;(List From Path+Rel)
        (List ANodeName (List f1 f2 ≡))
        (List ANodeName (List f1 f2 ∈))
        (List ANodeName (List f1 f2 ∉))
        (List ANodeName (List (List f1 ∉)
                              (List f2 ∉)
                              (List f3 ∉)
                              (List f4
                                    (List f5 ∉)
                                    (List f6 ∉))))
        
        ;; How to make it have the right kind of subtyping?
 
        
        ]
 
 @subsection{Properties applying to all reachable nodes from @racket[x]}
 
 The property @racket[x ≢ x.**] can be expanded to a series of properties. For
 example, if @racket[x] has two fields @racket[a] and @racket[d], the former
 itself having two fields @racket[b] and @racket[c], and the latter having a
 field @racket[e], itself with a field @racket[f]:
 @chunk[<expanded-path-set>
        (x ≢ x.a)
        (x ≢ x.a.b)
        (x ≢ x.a.c)
        (x ≢ x.d)
        (x ≢ x.d.e)
        (x ≢ x.d.e.f)]
 
 @subsection{Prefix trees to the rescue}
 
 This expanded representation is however costly, and can be expressed more
 concisely by factoring out the prefixes.
 
 @chunk[<prefixes>
        (x ≢ (x (a (b) (c))
                (d (e (f)))))]
 
 One thing which notably cannot be represented concisely in this way is
 @racket[x.a.** ≢ x.b.**], meaning that the subgraphs rooted at @racket[x.a]
 and @racket[x.b] are disjoint. It would be possible to have a representation
 combining a prefix-tree on the left, and a prefix-tree on the right, implying
 the cartesian product of both sets of paths. This has a negligible cost in the
 size of the type for the case where one of the members of the cartesian
 product, as we end up with the following (the left-hand-side @racket[x] gains
 an extra pair of parentheses, because it is now an empty tree):
 
 @chunk[<prefixes>
        ((x) ≢ (x (a (b) (c))
                  (d (e (f)))))]
 
 This does not allow concise expression of all properties, i.e. this is a form
 of compression, which encodes concisely likely sets of pairs of paths, but is
 of little help for more random properties. For example, if a random subset of
 the cartesian product of reachable paths is selected, there is no obvious way
 to encode it in a significantly more concise way than simply listing the pairs
 of paths one by one.
 
 @subsection{Cycles in properties}
 
 If a @racket[**] path element (i.e. a set of paths representing any path of
 any length) corresponds to a part of the graph which contains a cycle in the
 type, it is necessary to make that cycle appear in the expanded form. For
 that, we use @racket[Rec]. Supposing that the node @racket[x] has two fields,
 @racket[a] and @racket[c], the first itself having a field @racket[b] of type
 @racket[x]. We would expand @racket[x.**] to the following shape:
 
 @racket[(Rec X (≢ (Node0 'x)
                   (Node2 'x
                          (Field1 'a (Field1 'b (Field1 X)))
                          (Field1 'c))))]
 
 If one of the fields refers not to the root, but to 
 
 TODO: distinction between root nodes and fields in the path. Add an @racket[ε]
 component at the root of each path?
 
 @subsection{Partial paths}
 
 Partial paths: if a property holds between @racket[x.a] and @racket[x.b], then
 it is stronger than a property which holds between @racket[y.fx.a] and
 @racket[y.fx.b] (i.e. the common prefix path narrows down the set of pairs of
 values which are related by the property).
 
 A possible solution idea: mask the "beginning" of the path with a @racket[∀]
 or @racket[Any]. Either use
 @racket[(Rec Ign (U (Field1 Any Ign) Actual-tail-of-type))], or reverse the
 ``list'', so that one writes @racket[(Field1 'b (Field1 'a Any))], i.e. we
 have @racket[(Field1 field-name up)] instead of
 @racket[(Field1 field-name children)]. The problem with the reversed version
 is that two child fields @racket[b] and @racket[c] need to refer to the same
 parent @racket[a], which leads to duplication or naming (in the case of
 naming, Typed/Racket tends to perform some inlining anyway, except if tricks
 are used to force the type to be recursive (in which case the subtyping / type
 matching is less good and fails to recognise weaker or equivalent formulations
 of the type)). The problem with the @racket[Rec] solution for an ignored head
 of any length is that the number of fields is not known in advance (but
 hopefully our representation choices to allow weaker properties with missing
 fields could make this a non-problem?).
 
 @subsection{Array and list indices}
 
 When a path reaches an array, list, set or another similar collection, the
 special path element @racket[*] can be used to indicate ``any element in the
 array or list''. Specific indices can be indicated by an integer, or for lists
 with @racket[car], @racket[first], @racket[second], @racket[third] and so on.
 The special path elements @racket[cdr] and @racket[rest] access the rest of
 the list, i.e. everything but the first element.
 
 @subsection{Other richer properties}
 
 Other richer properties can be expressed, like
 @racket[x.len = (length x.somelist)]. This property calls some racket
 primitives (@racket[length]), and compares numeric values. However, we do not
 attempt to make the type checker automatically recognise weaker or equivalent
 properties. Instead, we simply add to the phantom type a literal description
 of the checked property, which will only match the same exact property.
 
 @section{Implementation}
 
 @subsection{The witness value}
 
 Since all witnesses will have a type of the form
 @racket[(→ (U (→ invᵢ Void) …) Void)], they can all be represented at run-time
 by a single value: a function accepting any argument and returning
 @racket[Void]. Note that the type of the witness is normally a phantom type,
 and an actual value is supplied only because Typed/Racket drops phantom types
 before typechecking, as mentioned earlier.
 
 @chunk[<witness-value>
        (: witness-value (→ Any Void))
        (define witness-value (λ (x) (void)))]
 
 @subsection{Grouping multiple invariants}
 
 As mentioned earlier, we group invariants together using an untagged union
 @racket[U], which must appear in a contravariant position. We wish to express
 witnesses for stronger invariants as subtypes of witnesses for weaker
 invariants, and therefore use a second nested function type to flip again the
 variance direction. We always include the @racket[Or] element in the union, to
 avoid ever having an empty union.
 
 @chunk[<Or>
        (struct Or ())]
 
 @chunk[<grouping-invariants>
        (define-type-expander (Invariants stx)
          (syntax-case stx ()
            [(_ invᵢ …)
             #'(→ (U Or (→ invᵢ Void) …) Void)
             #;#'(→ (→ (∩ invᵢ …) Void) Void)]))]
 
 @subsection{Structural (in)equality and (non-)membership invariants}
 
 @subsubsection{Invariants and their relationships}
 
 We design our typing hierarchy to allow encoding the equality, inequality,
 membership and non-membership between paths. A simple example would be
 the property @racket[:A.b.c ≡ :A.d.e], which would hold for all nodes of type
 @racket[A].
 
 These paths patterns form a suffix of actual paths. Let @${S₁} and @${S₂} be
 two sets of pairs of suffixes. If the set of pairs of actual paths covered by
 @${S₁} is a superset the set of pairs of actual paths covered by @${S₂}, then
 @${S₁} can be used to express a property over more pairs of actual paths,
 and the resulting property on the graph as a whole is therefore more precise.
 
 Our implementation allows the concise expression of a set of paths using a
 template within which sections of the path may be repeated any number of
 times. For example, the template @racket[:A.b(.c)*.d] corresponds to the set of
 paths containing @racket[:A.b.d], @racket[:A.b.c.d], @racket[:A.b.c.c.d] and so
 on.
 
 When path elements may produce a value whose type is a variant (i.e. a union
 of several constructors), it can be necessary to distinguish which
 constructor(s) the path applies to. We use a syntax inspired from that of
 @racketmodname[syntax/parse] for that purpose. Any point in a path can be
 followed by @racket[:node-name], which effectively refines the set of actual
 paths so that it contains only paths where the value at that point is of the
 given type. The syntax @racket[:A.b.c] therefore indicates that the path must
 start on an element of type @racket[A], and follow its fields @racket[b] then
 @racket[c]. The syntax @racket[.x:T.y.z] indicates paths @racket[.x.y.z], where
 the element accessed by @racket[.x] has the type @racket[T].
 
 The @racket[?] path element indicates that any field can be used at the given
 point. The syntax @racket[.x.?.y] therefore indicates the paths
 @racket[.x.f.y], @racket[.x.g.y], @racket[.x.h.y] and so on, where @racket[f],
 @racket[g] and @racket[h] are the fields of the value obtained after
 @racket[.x]. The @racket[?] path element can be used to describe all fields,
 including those hidden away by row polymorphism.
 
 It would be possible to represent sets of path concisely by reversing all
 these paths so that they start with their target element, and building a
 prefix tree. Unfortunately, Typed Racket does not currently does not
 automatically detect the equivalence between the types
 @racket[(U (Pairof A B) (Pairof A C))] and @racket[(Pairof A (U B C))]. @;{
  TODO: insert reference to the relevant bug.} In other words, at the type
 level, unions do not implicitly distribute onto pairs. When a set of
 properties @racket[S] is extended with a new property @racket[p], the
 resulting set of properties will be encoded as @racket[(U S p)]. If @racket[S]
 is encoded as a prefix tree, @racket[p] will not implicitly be merged into the
 prefix tree. This means that if prefix trees were to be used, extending a set
 of properties with a new property would give one representation, and directly
 encoding that set would give another representation, and the two
 representations would be incomparable.
 
 We therefore represent sets of paths using a more costly representation, by
 making a union of all paths, without factoring out common parts.
 
 @subsection{Parsing paths}
 
 @; TODO: make sure the literal "dot" is provided.
 
 @;   .a.b(.c.d)*.e
 @; ⇒ (λdot a b) ((λdot c d)) * (λdot e)
 
 @chunk[<parse>
        (begin-for-syntax
          (define (match-id rx id)
            (let ([m (regexp-match rx (identifier→string id))])
              (and m (map (λ (%) (datum->syntax id (string->symbol %) id id))
                          (cdr m)))))
          (define-syntax ~rx-id
            (pattern-expander
             (λ (stx)
               (syntax-case stx ()
                 [(_ rx g …)
                  #'(~and x:id
                          {~parse (g …) (match-id rx #'x)})]))))
 
          (define-syntax-class f+τ
            #:attributes (f τ)
            (pattern {~rx-id #px"^([^:]+):([^:]+)$" f τ})
            (pattern {~rx-id #px"^([^:]+)$" f} #:with ({~optional τ}) #'())
            (pattern {~rx-id #px"^:([^:]+)$" τ} #:with ({~optional f}) #'())
            (pattern {~rx-id #px"^:$"} #:with ({~optional (f τ)}) #'()))
          (define-syntax-class just-τ
            #:attributes (τ)
            (pattern {~rx-id #px"^:([^:]+)$" τ}))
          (define-syntax-class π-elements
            #:literals (#%dotted-id #%dot-separator)
            #:attributes ([f 1] [τ 1])
            (pattern (#%dotted-id {~seq #%dot-separator :f+τ} …)))
          (define-syntax-class extract-star
            #:literals (* #%dotted-id)
            (pattern (#%dotted-id {~and st *} . rest)
                     #:with {extracted-star …} #'{st (#%dotted-id . rest)})
            (pattern other
                     #:with {extracted-star …} #'{other}))
          (define-syntax-class sub-elements
            #:literals (* #%dot-separator)
            #:attributes ([f 2] [τ 2] [sub 1])
            (pattern
             (:extract-star …)
             #:with ({~either :π-elements {~seq sub:sub-elements *}} …)
             #|  |# #'(extracted-star … …))))]
 
 @chunk[<parse>
        (define-type-expander <~τ
          (syntax-parser
            [(_ τ) #'τ]
            [(_ f₀ . more)
             #`(f₀ (<~τ . more))]))
        (begin-for-syntax
          (define-template-metafunction generate-sub-π
            (syntax-parser
              [(_ :sub-elements after)
               #:with R (gensym 'R)
               (template
                (Rec R
                     (U (<~τ (?? (∀ (more) (generate-sub-π sub more))
                                 (∀ (more) (List* (Pairof (?? 'f AnyField)
                                                          (?? τ AnyType))
                                                  …
                                                  more)))
                             …
                             R)
                        after)))])))
        (define-type-expander Π
          (syntax-parser
            #:literals (#%dotted-id #%dot-separator)
            [(_ {~optional (~or (#%dotted-id fst-τ:just-τ
                                             {~seq #%dot-separator fst:f+τ} …)
                                {~datum :}
                                (~and fst-τ:just-τ
                                      {~parse (fst:f+τ …) #'()}))}
                . :sub-elements)
             #:with R (gensym 'R)
             (template/top-loc
              this-syntax
              (Rec R (U (Pairof Any R)
                        (List* (?? (?@ (Pairof AnyField fst-τ.τ)
                                       (Pairof (?? 'fst.f AnyField)
                                               (?? fst.τ AnyType))
                                       …))
                               <π>))))]))]
 
 @chunk[<π>
        (<~τ (?? (∀ (more) (generate-sub-π sub more))
                 (∀ (more) (List* (Pairof (?? 'f AnyField) (?? τ AnyType))
                                  …
                                  more)))
             …
             Null)]
 
 @chunk[<Invariant>
        (define-type-expander Invariant
          (syntax-parser
            #:literals (≡ ≢ ∈ ∉ ∋ ∌ = ≤ ≥ length +)
            [(_ π₁ … ≡ π₂ …) #`(U (inv≡ (Π π₁ …) (Π π₂ …))
                                  (inv≡ (Π π₂ …) (Π π₁ …)))]
            [(_ π₁ … ≢ π₂ …) #`(U (inv≢ (Π π₁ …) (Π π₂ …))
                                  (inv≢ (Π π₂ …) (Π π₁ …)))]
            [(_ π₁ … ∈ π₂ …) #`(inv∈ (Π π₁ …) (Π π₂ …))]
            [(_ π₁ … ∋ π₂ …) #`(inv∈ (Π π₂ …) (Π π₁ …))]
            [(_ π₁ … ∉ π₂ …) 
             #`(U (inv≢ (Π π₁ …) (Π π₂ … (#%dotted-id #%dot-separator :)))
                  (inv≢ (Π π₂ … (#%dotted-id #%dot-separator :)) (Π π₁ …)))]
            [(_ π₁ … ∌ π₂ …)
             #`(U (inv≢ (Π π₂ …) (Π π₁ … (#%dotted-id #%dot-separator :)))
                  (inv≢ (Π π₁ … (#%dotted-id #%dot-separator :)) (Π π₂ …)))]
            ;; TODO: = should use a combination of ≤ and ≥
            [(_ π₁ …
                {~and op {~or = ≤ ≥}}
                (~or (+ (length π₂ …) n:nat)
                     {~and (length π₂ …) {~parse n 0}}))
             #:with opN (syntax-case #'op (= ≤ ≥)
                          [= #'=N]
                          [≤ #'≤N]
                          [≥ #'≥N])
             #`(→ (invLength (opN n) (Π π₁ …) (Π π₂ …)) Void)]))]
 
 @CHUNK[<=>
        (define-type (P A B) (Promise (Pairof A B)))
        (define-type a 'a)
        (define-type x 'x)
        (define-type ax (U a x))
        (define-type x* (Rec R (P x R)))
        (define-type ax* (Rec R (P ax R)))
        (define-type-expander =N
          (syntax-parser
            [(_ 0) #'x*]
            [(_ n:nat) #`(P a (=N #,(sub1 (syntax-e #'n))))]))
        (define-type-expander ≥N
          (syntax-parser
            [(_ 0) #'ax*]
            [(_ n:nat) #`(P a (≥N #,(sub1 (syntax-e #'n))))]))
        (define-type-expander ≤N
          (syntax-parser
            [(_ 0) #'x*]
            [(_ n:nat) #`(P ax (≤N #,(sub1 (syntax-e #'n))))]))]
 
 @chunk[<Invariants>
        (define-type-expander Invariants
          (syntax-parser
            [(_ inv …)
             #`(→ (U Or (Invariant . inv) …) Void)]))]
 
 @chunk[<Any*>
        (define-type AnyField Symbol);(struct AnyField () #:transparent)
        (struct AnyType () #:transparent)
        (define-type ε (Π))]
 
 @subsubsection{Comparison operator tokens}
 
 We define some tokens which will be used to identify the operator which
 relates two nodes in the graph.
 
 @chunk[<comparison-operators>
        (struct (A B) inv≡ ([a : A] [b : B]))
        (struct (A B) inv≢ ([a : A] [b : B]))
        (struct (A B) inv∈ ([a : A] [b : B]))
        (struct (A B C) invLength ([a : A] [b : B] [c : C]))
        ;(struct inv∉ ()) ;; Can be expressed in terms of ≢
 
        (module literals typed/racket
          (define-syntax-rule (define-literals name ...)
            (begin
              (provide name ...)
              (define-syntax name
                (λ (stx)
                  (raise-syntax-error 'name
                                      "Can only be used in special contexts"
                                      stx)))
              ...))
          
          (define-literals ≡ ≢ ∈ ∉ ∋ ∌ ≥ ≤))
        (require 'literals)]
 
 @CHUNK[<≡>
        (define-for-syntax (relation inv)
          (syntax-parser
            [(_ (pre-a … {~literal _} post-a …)
                (pre-b … {~literal _} post-b …))
             #:with (r-pre-a …) (reverse (syntax->list #'(pre-a …)))
             #:with (r-pre-b …) (reverse (syntax->list #'(pre-b …)))
             ;; Use U to make it order-independent
             #`(#,inv (U (Pairof (Cycle r-pre-a …)
                                 (Cycle post-a …))
                         (Pairof (Cycle r-pre-b …)
                                 (Cycle post-b …))))]))
 
        (define-type-expander ≡x (relation #'inv≡))
        (define-type-expander ≢x (relation #'inv≢))]
 
 @chunk[<cycles>
        (struct ε () #:transparent)
        (struct (T) Target ([x : T]) #:transparent)
        (struct (T) NonTarget Target () #:transparent)
        
        (define-type-expander Cycle
          (syntax-parser
            [(_ field:id … {~literal ↙} loop1:id … (target:id) loop2:id …)
             #'(→ (List* (NonTarget ε)
                         (NonTarget 'field) …
                         (Rec R (List* (NonTarget 'loop1) … ;(NonTarget 'loop1) …
                                       (Target 'target) ;(NonTarget 'target)
                                       (U (List* (NonTarget 'loop2) … ;(NonTarget 'loop2) …
                                                 R)
                                          Null)))) Void)]
            [(_ field … target)
             #'(→ (List (NonTarget ε)
                        (NonTarget 'field)
                        …
                        (Target 'target)) Void)]
            [(_)
             #'(→ (List (Target ε)) Void)]))]
 
 @;{@[
    
  ;.a.b = .x.y
  ;(l1=a ∧ l2=b ∧ r1=x ∧ r2=y) ⇒ eq
  ;¬(l1=a ∧ l2=b ∧ r1=x ∧ r2=y) ∨ eq
  ;¬l1=a ∨ ¬l2=b ∨ ¬r1=x ∨ ¬r2=y ∨ eq
 
  ;.a.c = .x.y
  ;(l1=a ∧ l2=c ∧ r1=x ∧ r2=y) ⇒ eq
 
  ;.a.c = .x.z
  ;(l1=a ∧ l2=b ∧ r1=x ∧ r2=z) ⇒ eq
  ;¬l1=a ∨ ¬l2=b ∨ ¬r1=x ∨ ¬r2=z ∨ eq
 
 
  ;.a.b = .x.y ∧ .a.c = .x.z
  ;(¬l1=a ∨ ¬l2=b ∨ ¬r1=x ∨ ¬r2=y ∨ eq) ∧ (¬l1=a ∨ ¬l2=b ∨ ¬r1=x ∨ ¬r2=z ∨ eq)
  ;¬¬(¬l1=a ∨ ¬l2=b ∨ ¬r1=x ∨ ¬r2=y ∨ eq) ∧ (¬l1=a ∨ ¬l2=b ∨ ¬r1=x ∨ ¬r2=z ∨ eq)
  ;¬(l1=a ∧ l2=b ∧ r1=x ∧ r2=y ∧ eq) ∨ (l1=a ∧ l2=b ∧ r1=x ∧ r2=z ∧ ¬eq)
  ]}
 
 @; Problem with ∩: it factors out too much, (∩ '(a . b) '(a . c) '(x . b))
 @; becomes (Pairof (∩ 'a 'x) (∩ 'b 'c)), which is equivalent to have all four
 @; elements of {a,x} × {b,c}, but we only want three out of these four.
 
 @;{
  Two sorts of paths inside (in)equality constraints:
 
  @itemlist[
  @item{those anchored on a node, stating that
    @$${
     ∀\ \textit{node} : \textit{NodeType},\quad
     \textit{node}.\textit{path}₁ ≡ \textit{node}.\textit{path}₂}}
  @item{those not anchored on a node, stating that
    @$${
     \begin{array}{c}
     ∀\ \textit{node}₁ : \textit{NodeType}₁,\quad
     ∀\ \textit{node}₂ : \textit{NodeType}₂,\\
     \textit{node}₁.\textit{path}₁ ≡ \textit{node}₂.\textit{path}₂
     \end{array}}}]
 }
 
 @subsection{Putting it all together}
 
 @CHUNK[<*>
        (require (only-in typed/dotlambda #%dotted-id #%dot-separator)
                 "dot-lang.rkt"
                 (for-syntax racket/base
                             racket/list
                             phc-toolkit/untyped
                             syntax/parse
                             syntax/parse/experimental/template)
                 (for-meta 2 racket/base)
                 (for-meta 2 phc-toolkit/untyped/aliases)
                 (for-meta 3 racket/base))
 
        (begin-for-syntax
          (define-syntax-rule (quasisyntax e)
            (quasisyntax/top-loc this-syntax e))
          (define-syntax-rule (template/top-loc loc e)
            (quasisyntax/top-loc loc #,(template e))))
 
        (provide ≡ ≢ ∈ ∉ ∋ ∌ ≥ ≤)
        
        ;; For testing:
        (provide Invariants
                 inv≡
                 inv≢
                 Or
                 ;Target
                 ;NonTarget
                 ε
                 witness-value
                 Π
                 AnyType
                 AnyField
                 Invariant)
 
        <parse>
 
        <witness-value>
        <Any*>
        <comparison-operators>
        <Invariant>
        <Invariants>
        <Or>
        <=>]