Instead of using de Bruijn levels, it's better to use labels (strings) and association lists (gmap wouldn't work, as we need nested recursion). The current setup is even implemented incorrectly.
This change is quite invasive, and would also affect new code, so it probably needs to be done sooner rather than later.

Typing derivation would also get freshness assumptions to ensure that labels are disjoint. @amintimany suggested this would be bothersome, but the overhead appears extremely limited in Marianna Rapoport et al.'s formalization.
Instead, values themselves would carry no such assumption.

We should split into separate files

• new typing rules from the DOT ones
• experiments.v (it's too big).
• maybe, add a file for #28, if I get back to it?

This is an idea by Robbert, and it would be nice to dot all the i's with less code and less annoying one.

Instead of updating them in the paper, add the original counts with a correct commit hash.

skeleton.v should encode Section "3.5 Adequacy" in our current draft, but it still has admits. This issue is about finishing it.

Whatever version of translation/stamping we use, this seems necessary — not because we actually use the theorems, but because they help us argue adequacy of our translation.

Status: @amintimany plans to get on it next week.

Subtasks:

• wait on #14 to be merged (this was marked as waiting on #11, but the rest of #11 seems orthogonal).
• maybe redefine same_skel_* predicates as an inductive relation for easier proofs.
  • maybe we should abstract on such relations, similarly to stampedness.v, or maybe not (#40). Amin, please ignore this part.

Otherwise, we'd have to stop updating coqdoc website during AEC, which I'd rather not.

Ideally, this should confirm that we can focus on stamped syntax.

Steps:

• Make typing refer to stamped type members.
• Prove that a typing judgment only refers to stamped expressions/subjects.
• Prove that a typing judgment only refers to stamped types. That'll probably require extra side conditions around subtyping (EDIT: but not occurrences of TSel).
• Check the above lemma can be used for the fundamental lemma. In fact, the fundamental lemma seems to not require explicit proofs that the syntax is stamped (or not).

I moved other items to #43; closing.

• Typecheck DOT examples to argue this is "DOT" enough (#26)
• Technical appendix? Unneeded if the Coq formalization is clean enough. Probably (parts of) stamping goes in there.
• Writing plan/outline

Please help fill in the outline. Items I expect:

• Introduction
• DOT examples, both to explain DOT, and to argue our DOT variant is DOT-like enough
• (Somewhere) examples of issues with the DOT syntax, to motivate why our restrictions make sense regardless of our model. Here we can show cyclic proofs.
• Our model. At first, we should tell the reader to ignore all occurrences of later. We can also keep the "implementation" of storing semantic types in values "abstract", similarly to the runST paper. Then, we explain the restrictions. Since this section is about modeling impredicative type members, it should be written for a larger audience if possible.
• Later, we explain how we use stored predicates and stamping and wellMapped and whatnot. This section requires familiarity not just with step-indexing but also with Iris, so this section should be encapsulated (again, like for runST).
• Some words on the mechanization itself.
• Conclusions

Just for the record (not high priority). I followed the README (with opam 2.0.1) and got

$ opam switch -v -v  create . --deps-only
[ERROR] Could not resolve set of base packages:
        Your request can't be satisfied:
          - No available version of ocaml-base-compiler satisfies the constraints


Switch initialisation failed: clean up? ('n' will leave the switch partially installed) [Y/n] n

I got the switch to work by answering n and pinning things by hand:

opam pin add coq 8.8.2
<answer n>
opam pin add coq-iris dev.2018-11-01.2.19e85810
<answer y and let it install>

@ineol

• Recheck syntactic typing in PDF and code match.
• Fix semantic typing judgments to have the same signatures as syntactic ones.
• Fix all lemmas to use the right judgments.
• Stop using indexed semantic typing.
• Finish fundamental lemma.

Also maybe pick some project to follow in coding style and naming — @ineol was suggesting the runST project:
https://iris-project.org/artifacts/2018-popl-runst.tar.gz
https://people.cs.kuleuven.be/~amin.timany/runst/artifact/coq-index.html

(From #35).
Can we encode D<: into guarded D<:? I keep saying no, but it could in fact be possible. Does this already require adding singletons?

Split out of #21.

• Prove substitution lemmas for well-stamping needed above (#45).
• We should still be able to prove that unstamped syntax can be translated to stamped syntax. DSub/astStamping.v was the first attempt, but has a bug in the setup: it defines the stamping relation through an unstamping function, but that doesn't necessarily terminate if we define it correctly. Instead, we need an (pure) inductive relation between unstamped and stamped syntax.
• ? I'm still be afraid of proving formally adequacy of typing: we could define syntactic typing on unstamped syntax and prove that can be translated, but this seems boring on paper and lots of work in Coq.

Since the AEC is apparently a very light double-blind...

Goal: Enable writing syntactic values in types, for examples such as F.F (\nu z. { A = Int }) (aka, F Int).

To give semantics to such types, we'll use guarded recursion, as in DSub; but we'll combine it with stamping + higher-order ghost state.

Steps:

• Use guarded recursion (#385)
• Prove extra typing rules
• Encode example? (See below).

An updated version of my plan from August 2020:

• stop indexing the Coq types of Dot semantic types by arity (via dependent types) (#347);
• New: Limit dependency on sTEq_Eta #345
• add syntax for HK-DOT (#302)
• New: optionally: fork the syntactic type system.
• Maybe: drop (typing rules for) singleton types (?), since they don't respect functionality. We could allow singletons that don't mention type parameters, but that complicates the judgment.
• (#365) enable writing syntactic values in types, for examples such as F.F (\nu z. { A = Int }) (aka, F Int). This might depend on the previous step, but the changes to the semantics don't.
• Then tackle functionality of type constructors (#396). (TODO: add the remaining steps from the plan).

I suspect we'll have to mention briefly to_subst in the paper (appendix).
Either way, it's high time for a notation for it.
Since it turns finite to infinite substitutions, I'm thinking of:

(* Tighter precedence than [>>], which has level 56. *)
Notation "∞ ρ" := (to_subst ρ) (at level 50).

Instead of switching to the future modality, using an updateless WP seems better for now.

One of my typing rules demands WP e {{ v, ⟦ T1 ⟧ ρ v }} -∗ WP e {{ v, ⟦ T2 ⟧ ρ v }} -∗ WP e {{ v, ⟦ T1 ⟧ ρ v ∧ ⟦ T2 ⟧ ρ v }}, and that feels wrong.

I did prove that, but my proof will fail for a nonpersistent state interpretation. So this will be a problem for mutable DOT.

To prove the thesis, we assume e reduces to e', and apply what we learn about e' from both hypotheses.

https://gist.github.com/Blaisorblade/d70d77f45c22ff3500566c1f4b85f77e

Original goal:

  "IHT" : WP t.|[to_subst ρ] {{ v, ⟦ T1 ⟧ ρ v }}
  "IHT1" : WP t.|[to_subst ρ] {{ v, ⟦ T2 ⟧ ρ v }}
  --------------------------------------□
  WP t.|[to_subst ρ] {{ v, ⟦ T1 ⟧ ρ v ∧ ⟦ T2 ⟧ ρ v }}

To encode DOT in our DOT (or even for D<:), I expect we will need singleton types.

We can't fully encode DOT yet. Assume v: T, and that DOT gives T <: U but we have T <: Later^i U. Then, DOT gives v: U, but we give tskip^i v: U. But we must always translate values to values, since values can be used in more places than expressions.

To fix this, we should just insert lets, and replace e[v] with let x = tskip^i v in e[x] — since x is also a value. To ensure that type selections x.A and v.A are compatible, we must introduce singleton types and give x type U /\ v.type.
I sketched on paper rules that should let us show:

• v: v.type
• v: T -> v.type <: T.
• Using T <: Later^i U, S <: Later^i S, and Later^i A /\ Later^i B = Later^i (A /\ B), we get v.type <: Later^i (U /\ v.type), hence tskip^i v: U /\ v.type as desired.

We currently prove all our propositions are persistent because of the structure of our CMRAs, instead of using boxes everywhere; this strategy simplified the paper, but it doesn't scale to certain potential extensions:

• the proof breaks with Iris 4.0 because the saved proposition CMRA isn't automatically persistent. Of course, we could fix this easily by importing (vendoring) the old construction.
• more importantly, later credits are never persistent, and they'd be really cool.

Concretely, this involves MRs #426, #433 and #421, and undoes the effects of #295, #296 and #297.

We should try switching unary_lr to infinite substitutions, since that's needed to define substitution on semantic types (#81). I've tried in the past defining substitution on semantic types by precomposition, but many binding lemmas become much more complicated (or false).

We could also switch environment validity interp_env to apply directly to infinite substitutions, but that would break the following lemma, that current proofs rely on:

  Lemma interp_env_len_agree ρ:
    ⟦ Γ ⟧* ρ -∗ ⌜ length ρ = length Γ ⌝.

Many proofs can be transitioned to different lemmas, except for stamped type members. Dealing with binding there takes more work today, and also takes more work to adapt.

It's in the way of changing the syntax of types.

• Finish translating typing rules for "guarded D<:".
• Prove axioms on swaps.

• #365 requires using much more setoid rewriting, and performance issues made me realize we had buggy or missing Proper and Params instances (which I'm fixing).

• The Params for hsubst_s_kind is odd:

+(* TODO does this work reasonably? *)
 #[global] Instance: Params (@hsubst_s_kind) 2 := {}.

hsubst_s_kind is not what we apply to arguments or what gets a Proper instance. We aren't using s_kind much (yet?) but if we ever care, testing would be appropriate.

Extracted from #365, and what #379 fixes.

This issue was already agreed, but somebody should do it. I had volunteered, but don't have time. @amintimany, is this something you'd take up?

Self-contained summary below.

Right now, the proof of subsumption uses admitted lemma wp_wand_cl:

  Lemma wp_wand_cl e Φ Ψ:
    (WP e {{ v, Φ v }} -∗ ⌜ nclosed e 0 ⌝ -∗ (∀ v, Φ v -∗ ⌜ nclosed_vl v 0 ⌝ -∗ Ψ v) -∗ WP e {{ v, Ψ v }})%I.

The plan was

• prove that nclosed is preserved by reduction (now done in theories/Dot/fv_step.v)
• then prove a variant of wp_wand generalizing wp_wand_cl:

Lemma wp_wand s E e Φ Ψ :
  WP e @ s; E {{ Φ }} -∗ (∀ v, Φ v -∗ Ψ v) -∗ WP e @ s; E {{ Ψ }}.

The variant would also take a property P preserved by reduction, a proof of P e, and instead of (∀ v, Φ v -∗ Ψ v), it'd require (∀ v, ⌜ P (of_val v) ⌝ -∗ Φ v -∗ Ψ v).

• Then, one could use the fact that nclosed (of_val v) i -> nclosed_vl v i (lemma fv_tv_inv) and prove the original wp_wand_cl.

Instead of storing arbitrary predicates and adding boxes, we could like store persistent predicates built with lty, since they form an OFE.
But the benefit is likely minimal in practice (beyond the conceptual one).

I have not tried proving typing lemmas for paths of arbitrary length, but the ones I did try (for length = 2) followed my expectations.

However, I have tried proving translation lemmas involving path_wp, and it appeared I'd likely need (part of) the usual toolkit of lemmas for working on wps; I suspect it might be the same for path-typing lemmas.

==
It also seems not easy to use the standard wp or twp. path_wp p φ is stronger in three ways:

• it uses later (like wp but unlike twp);
• it demands that evaluation of path p terminates with some value v (unlike wp but like twp);
• it demands that the evaluation result v satisfies φ now, not after some basic/fancy update, unlike twp.

Avoiding updates appears to matter in a few places (I gave a quick try some time ago). IIRC, for instance, if we used a standard wp, we'd fail to prove that (semantically) p: {A <: U} implies p.A <: U, because p.A <: U must hold before any update.

Also, avoiding updates appears to be a reasonable choice: since path evaluation is supposed to be pure and total, there's no reason updates would be required. We might be able to add updates by adding them to value subtyping as well, but I'm pretty wary of the idea — I'm not certain it'd work.

EDIT (2019-06-06): the reason why path_wp must use later is that we can't prove it otherwise. In general, we don't know that x.a.b.c reduces now — we only now we can take the first step, that in the later world we can take the second, etc.

Try modifying is_unstamped_ty to just use atomic_path_root, and drop is_unstamped_* on other syntax. That should also let us drop the free-variable count from it.

However, for examples, we still need an alternative inductive definition for nclosed on types (used for type members); but that should not be needed for path substitution.

Most of this should be easy, and ideally should wait for #21.

• The crucial part here will be proving the semantic typing lemma for type members
• and its corresponding case in the fundamental lemma.
• Also, once we prove that typing only involves stamped syntax, we should adapt the fundamental lemma to assume that the input is stamped and that the stamp table is wellMapped.

The arity is now unused (since we dropped dependent typing). So we should go from:

  | kTSel n (p : path) l : ty (* type selections [p.A]; *)

to

  | TSel (p : path) l : ty (* type selections [p.A]; *)

Leftover TODOs from #45: move some lemmas at more appropriate places.

TODO: We should make the notation in comments consistent with the gDOT paper; in that notation, this is written as { A >: T <: T } # A = Later T.

Originally posted by @Blaisorblade in #304

• Move "Paper correspondence" first.
• Add mapping table?

Part of the new translation/stamping. One needs to map another lemma, transferOne over a gmap, and find an appropriate statement. That lemma is probably short but not trivial.

This is currently described in Sec. 3.2 of the PDF.

Follow up of #18. Gotta figure out if we need except-0 or not, and see if this works out. Also, since there's an except-0 in one case, maybe I can take advantage of it for e.g. nclosed.

Maybe I should first test this on DSub since it's smaller, not sure.

Assigning myself, since I want to figure out how the proofs of typing lemmas are affected...

Also to note: this way, we cannot use invariants. So it's important that mappings used for the translation stop using invariants — which should be achieved by #13.

Commit 74d3c46 (from PR #92) adapts olty_experiments to higher-order subtyping, but it doesn't actually support higher-order type members and kinds. We should fix that.