From 807f707b8a98eb6b5be92d93af74261b7f0caa33 Mon Sep 17 00:00:00 2001 From: Denis Merigoux Date: Wed, 3 Mar 2021 12:32:16 +0100 Subject: [PATCH] Updated README --- doc/formalization/README.md | 38 ++++++++++++++++--------------------- 1 file changed, 16 insertions(+), 22 deletions(-) diff --git a/doc/formalization/README.md b/doc/formalization/README.md index 075c78cd..59a4d063 100644 --- a/doc/formalization/README.md +++ b/doc/formalization/README.md @@ -2,22 +2,25 @@ ## Presentation -This folder contains the F* proof of the correctness of the translation from the default calculus +This folder contains the F\* proof of the correctness of the translation from the default calculus to the target lambda calculus. The proof is organized as follows: -* `Catala.DefaultCalculus.fst` contains the semantics of the default calculus as well as the +- `Catala.DefaultCalculus.fst` contains the semantics of the default calculus as well as the type safety theorems and proofs; -* `Catala.LambdaCalculus.fst` contains the semantics of the lambda calculus as well as the +- `Catala.LambdaCalculus.fst` contains the semantics of the lambda calculus as well as the type safety theorems and proofs; -* `Catala.Translation.Helpers.fst` contains various helpers related to the lambda calculus, +- `Catala.Translation.Helpers.fst` contains various helpers related to the lambda calculus, used in the translation correctness proof; -* `Catala.Translation.fst` contains the definition of the translation as well as its proof +- `Catala.Translation.fst` contains the definition of the translation as well as its proof of correctness, culminating in the last wrap-up theorem of the file. +The `*.hints` files are merely F\* technical helper files that speed up the proof replay by recording +a list of lemmas to feed in priority to the SMT solver. + ## Proof replay -To replay the proofs, you will need to have [F*](https://github.com/FStarLang/FStar) installed -on your machine, and the `FSTAR_HOME` environement variable pointed to the location of the F* +To replay the proofs, you will need to have [F\*](https://github.com/FStarLang/FStar) installed +on your machine, and the `FSTAR_HOME` environement variable pointed to the location of the F\* directory. You can then replay the proofs using: make verify @@ -28,19 +31,10 @@ sure to strenghen the flaky proofs for the camera-ready version of the artefact. ## Disclaimer -This mechanization contains two distinct admitted lemmas, all related to administrative aspects of -the target lambda calculus. Both are in `Catala.TranslationHelpers.fst`. +This mechanization contains one admitted lemma, related to administrative aspects of +the target lambda calculus. It is in `Catala.TranslationHelpers.fst`. -* The first admit concerns `well_typed_terms_invariant_by_subst`, which is a classic result stating - that correclty typed terms with no free variables are invariant by substitution. The proof in F* - needs a version of context invariance different from the one we used to prove type safety, hence - this temporary admit. -* The second assumed hypothesis in inside `lift_multiple_l_steps_exceptions_head`, and is related - two lambda calculus terms, `init0` and `init2`. `init2` is the result of the double application - of the beta-reduction to `init0`. Both terms are reduced versions of the big, deeply embedded - term `process_exceptions`, which causes F* automation a lot of troubles. The difficulty with - the proof seems to stem from the instantiations of `well_typed_terms_invariant_by_subst`, which - is missing some key step. - -We plan of course to prove those two hypothesis in due time for an upcoming artefact, and hope these -explanations did convince you that the rest of the proof remains solidly grounded. \ No newline at end of file +The admit concerns `well_typed_terms_invariant_by_subst`, which is a classic result stating +that correclty typed terms with no free variables are invariant by substitution. The proof in F\* +needs a version of context invariance different from the one we used to prove type safety, hence +this temporary admit.