blaisorblade / dot-iris Goto Github PK
View Code? Open in Web Editor NEWScala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris — Coq Formalization
Home Page: https://dot-iris.github.io
License: Other
Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris — Coq Formalization
Home Page: https://dot-iris.github.io
License: Other
Most of this should be easy, and ideally should wait for #21.
wellMapped
.Please help fill in the outline. Items I expect:
Otherwise, we'd have to stop updating coqdoc website during AEC, which I'd rather not.
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
nclosed
is preserved by reduction (now done in theories/Dot/fv_step.v
)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)
.
nclosed (of_val v) i -> nclosed_vl v i
(lemma fv_tv_inv
) and prove the original wp_wand_cl
.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
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:
Leftover TODOs from #45: move some lemmas at more appropriate places.
This is an idea by Robbert, and it would be nice to dot all the i's with less code and less annoying one.
Ideally, this should confirm that we can focus on stamped syntax.
Steps:
I moved other items to #43; closing.
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
It's in the way of changing the syntax of types.
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]; *)
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).
(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?
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 wp
s; 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:
wp
but unlike twp
);p
terminates with some value v
(unlike wp
but like twp
);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.
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).
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.
We should split into separate files
experiments.v
(it's too big).Split out of #21.
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.
dot-iris/theories/DSub/typeExtraction.v
Lines 332 to 352 in c34c521
This is currently described in Sec. 3.2 of the PDF.
Instead of switching to the future modality, using an updateless WP seems better for now.
#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.
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.
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:
Concretely, this involves MRs #426, #433 and #421, and undoes the effects of #295, #296 and #297.
Instead of updating them in the paper, add the original counts with a correct commit hash.
Since the AEC is apparently a very light double-blind...
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:
same_skel_*
predicates as an inductive relation for easier proofs.
stampedness.v
, or maybe not (#40). Amin, please ignore this part.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.
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.
An updated version of my plan from August 2020:
F.F (\nu z. { A = Int })
(aka, F Int
). This might depend on the previous step, but the changes to the semantics don't.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>
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
.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.A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.