diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index c8cba4f..1c61ea2 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -21,7 +21,7 @@ open proof obligation. and the AFFIRMATION honesty snapshot with the systemet identity and an honest status (theory specified; proofs OPEN; no compiler here). * Added the wager experiment for coercions and roles in Cubical Agda -(`+verification/proofs/agda/Wager/+`, stages 0 to 4), with an `+agda+` job +(`+verification/proofs/agda/Wager/+`, stages 0 to 7), with an `+agda+` job in the proofs workflow. The experiment claims no ET obligation. ==== Changed diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index 058aed8..b973804 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -13,7 +13,7 @@ summary from the per-prover MANIFESTs and fails if this file disagrees. // Machine-readable ground-truth markers — checked by scripts/check-proof-status.sh. // Do not edit by hand without changing the MANIFEST accordingly. // gate:lean4 gated=20 quarantined=0 -// gate:agda gated=64 quarantined=0 +// gate:agda gated=79 quarantined=0 == Summary @@ -24,7 +24,7 @@ summary from the per-prover MANIFESTs and fails if this file disagrees. | ET obligations (DOM — the theory itself) | 15 | 2 | 2 | 11 | MECH-1: L1 conversion, Lean4 (covers ET-1, ET-2, part of ET-3) | 1 | — | in progress | — | MECH-2: L2 grade algebras, Lean4 (covers ET-4, ET-5) | 1 | 1 | — | — -| WAGER: the wager experiment for coercions and roles, Cubical Agda (claims no ET obligation) | 1 | - | in progress | - +| WAGER: the wager experiment for coercions and roles, Cubical Agda (claims no ET obligation; stages 0 to 7 are done; 2 decisions are with the owner) | 1 | 1 | - | - |=== The Done/In-progress claims above are scoped to the *mechanized core @@ -158,9 +158,40 @@ no file uses coinduction. One warning class is silenced newtype parameter is the least grade that target kinding accepts | *Proven* -| 5 to 7 -| T6, T7 of the experiment -| not attempted +| 5 +| `Wager.Proofs.t6`, `t6-conversion`, `t6-no-term` : for each nominal + coercion of the source fragment, the two translated types have one normal + form; the coercion becomes conversion and no term remains +| *Proven*. The converse is false for one checked pair of types + +| 6 +| T7 of the experiment (local equality assumptions), in 2 parts. + Part 1, a separation. `Wager.Proofs.t7-separation` : for each closed + instance of one GADT program of a source calculus with local equality + assumptions, no typed closed target term has the erasure of the program + together with a type that has the erased type of the source type. + Part 2, an identity type at the grade `0`, as a family of base constants + of a signature. Equality evidence is a term. `Wager.Proofs.t7-erasure`, + `t7-canonicity`, `t7-intro`, `t7-grade`, `t7-assumption`, + `t7-conservative` : the erasure of the proofs in casts is sound; closed + evidence exists exactly for convertible types; a local equality + assumption is a variable at the grade `0` +| Part 1 *Proven*. It excludes a translation that keeps the erased type + and the erased term, and no other translation. + Part 2 *Proven* for a signature that has an identity family (one such + signature is built). The extension has 1 new rule and 1 new term former. + The owner decides if it is inside the wager + +| 7 +| The optional univalent cross-check. `Wager.Proofs.coercion-denotes-transport`, + `coercion-denotes-transport-back`, `coerce-function-is-transport` : in a + realisability model of the target types in the cubical universe, where a + newtype instance is a wrapper that is equivalent to its content, the + translation of each representational coercion denotes transport along a + path made with `ua` +| *Proven*, for each source signature that passes the role check. The + denotation is by realisers: the development has no denotation of each + typed term |=== == Mechanization slots diff --git a/verification/proofs/agda/MANIFEST b/verification/proofs/agda/MANIFEST index 079ef4c..469eab3 100644 --- a/verification/proofs/agda/MANIFEST +++ b/verification/proofs/agda/MANIFEST @@ -65,3 +65,18 @@ verification/proofs/agda|Wager/Trans/Simulation.agda|gated|Stage 4 (T3, T5): an verification/proofs/agda|Wager/Trans/RoleCorrespondence.agda|gated|Stage 4: the inferred source role is the least grade that target kinding accepts; the target signature is valid verification/proofs/agda|Wager/Trans/TwoStateProofs.agda|gated|Stage 4: the tagged signature has no translation with two-state tropes (checked counterexample) verification/proofs/agda|Wager/Examples/Stage4.agda|gated|Stage 4: accepted and rejected closed examples +verification/proofs/agda|Wager/Examples/Stage5.agda|gated|Stage 5 (T6): accepted and rejected closed examples; the converse of T6 is false for the row scheme +verification/proofs/agda|Wager/L2/Erasure.agda|gated|Stage 6 (lemma): a typed target term erases to a simply typed term, for each signature and each grade algebra +verification/proofs/agda|Wager/Local/Source.agda|gated|Stage 6: the source calculus with local equality assumptions (types, equalities, terms, erasure) +verification/proofs/agda|Wager/Local/Gadt.agda|gated|Stage 6: the GADT program of the separation (definitions only) +verification/proofs/agda|Wager/Local/Separation.agda|gated|Stage 6 (T7, the separation): no typed target term has the erasure and the erased type of the GADT program +verification/proofs/agda|Wager/Examples/Stage6.agda|gated|Stage 6 (T7, the separation): accepted and rejected closed examples +verification/proofs/agda|Wager/Identity/Family.agda|gated|Stage 6, part 2: the identity type as a family of base constants of a signature (definitions only) +verification/proofs/agda|Wager/Identity/Term.agda|gated|Stage 6, part 2: the terms of the target with the cast, and the two erasures (definitions only) +verification/proofs/agda|Wager/Identity/Typing.agda|gated|Stage 6, part 2: the target judgement with the rule t-cast, which uses the evidence at the grade 0 (definitions only) +verification/proofs/agda|Wager/Identity/Soundness.agda|gated|Stage 6, part 2 (T7, the identity type): the erasure of proofs is sound for each signature with an identity family and each set of grade operations; canonicity; the grade lemma needs the laws +verification/proofs/agda|Wager/Identity/Instance.agda|gated|Stage 6, part 2: one signature that has an identity family (the record is not empty) +verification/proofs/agda|Wager/Examples/Stage6Identity.agda|gated|Stage 6, part 2 (T7, the identity type): accepted and rejected closed examples +verification/proofs/agda|Wager/Univalent/Model.agda|gated|Stage 7 (optional): the model of target types in the cubical universe, realisers, and the path of a coercion (definitions only) +verification/proofs/agda|Wager/Univalent/CrossCheck.agda|gated|Stage 7 (optional): the translation of a representational coercion denotes transport along its path, for each source signature, state scheme, grade algebra and interpretation of the base constants +verification/proofs/agda|Wager/Examples/Stage7.agda|gated|Stage 7 (optional): accepted and rejected closed examples diff --git a/verification/proofs/agda/Wager/DESIGN-CHOICES.adoc b/verification/proofs/agda/Wager/DESIGN-CHOICES.adoc index faa71cc..48bf4a4 100644 --- a/verification/proofs/agda/Wager/DESIGN-CHOICES.adoc +++ b/verification/proofs/agda/Wager/DESIGN-CHOICES.adoc @@ -1,7 +1,7 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) = Wager: design choices -Status: entries of Stage 0, Stage 1, Stage 2, Stage 3 and Stage 4. +Status: entries of Stage 0 to Stage 5. :toc: left :sectnums!: @@ -36,7 +36,7 @@ Agda 2.8.0 then rejects an import from a module without the flag (`InfectiveImpo The stock library makes that rule impossible to obey. *Decision.* The owner accepted alternative 1 on 2026-11-10. -At the end of each stage a search for `coinductive` in `Wager/` checks the intent of the rule. The search found nothing at the end of Stage 1, of Stage 2, of Stage 3 and of Stage 4. +At the end of each stage a search for `coinductive` in `Wager/` checks the intent of the rule. The search found nothing at the end of each of the stages 1 to 5. *Alternatives.* @@ -69,6 +69,10 @@ Thus the Lean proofs that use `castNf_diag` (an equality on `Δ = Δ` closed by *Alternative.* Leave the warning on. This is honest but makes the output hard to read. +*Audit at the end of Stage 5.* 36 of the 65 files have the line. The one new file has the line. A test without the line found the warning in it and found no other warning. + +*Audit at the end of Stage 6, part 1.* 39 of the 70 files have the line. Of the 5 new files, 3 have the line (`L2/Erasure`, `Local/Source`, `Local/Separation`): a test without the line found the warning in each of the 3. The other 2 (`Local/Gadt`, `Examples/Stage6`) have no line and build with no warning. + *Audit at the end of Stage 4.* 35 of the 64 files have the line. A test of the 13 new files without the line found the warning in 6 of them. It found no other warning, and it found 2 new files that had the line and did not need it. The line was removed from them. The other 5 new files compile without a warning. *Audit at the end of Stage 3.* 29 of the 51 files have the line. A test of the 10 new files without the line found the warning in each of the 6 new files that have the line. It found no other warning. The other 4 new files compile without a warning. @@ -442,3 +446,227 @@ Kinding has a subusage rule, so it accepts each grade above the least one. "The *Reason.* "This program has no translation" needs a definition of "translation". The three conditions are properties that claim W asks for. The fourth condition is the form of Stage 2. The translation with the row scheme meets the three conditions (`Wager.Proofs.row-translation-exists`), so the conditions are not empty. + +== Stage 5 + +[[DC-5.1]] +=== DC-5.1: the form of T6 + +*Choice.* T6 has three statements (`Wager.Statements.T6-Statements`): + +* `T6`: for each nominal coercion of the source, the two translated types have one normal form; +* `T6-Conversion`: the two translated types are convertible (`DefEq`); +* `T6-No-Term`: the translation of a cast along a nominal coercion is the translation of the term under the cast. + +Each holds for each source signature, each state scheme and each set of grade operations. None needs the role check. + +*Reading of the task text.* The task says: "every source coercion at nominal role built from the axioms of total type-level functions". +In this fragment each nominal coercion (`Co nom`) is built from reflexivity, symmetry, transitivity, congruence and the equations of the type-level functions. T6 is thus stated for each nominal coercion. + +*Reason for the proof.* The normal form of a translated type is a function of the nominal value of the source type (`Wager.Trans.Nominal.nf-T`). A nominal coercion keeps the nominal value (`Wager.Proofs.source-nominal-soundness`). + +*Process.* The proof of the first two statements is the lemma of Stage 4 (DC-4.4). It existed before the statements of T6 were put in `Statements.agda`. + +[[DC-5.2]] +=== DC-5.2: T6 is one direction + +*Choice.* T6 says: a nominal coercion gives one normal form. This development does not state the converse, because the converse is false for the row scheme. + +*Checked example.* `Tag Char` and `Tag Unit` have no nominal coercion in the source (`Wager.Examples.Stage5.tag-char-unit-rejected`). They have one target type (`tag-char-unit-one-type`), and they have a representational coercion (`tag-char-unit-rep`). +The reason: no type-level function of the signature tells the two types apart, so they have one row and one state. + +*Consequence.* The translation can give one target type to two source types that the source keeps apart nominally. + +*Not proved here.* This development does not prove the general sentence "two source types with one target normal form have one erased type". + +== Stage 6 + +[[DC-6.1]] +=== DC-6.1: the owner chose the two options, the separation first + +The task gives two options for Stage 6: (1) an identity type at the grade `0`, with a proof that erasure of its proofs is sound; (2) a separation. +`PLAN.adoc` says that the owner makes the choice. On 2026-11-10 the owner chose: the two options, option 2 first, with a stop and a report between the two parts. + +T7 thus has two parts. Part 1 is the separation (`Wager.Statements.T7-Statements.T7-Separation`). Part 2 is the identity type (`Wager.Statements.T7-Identity-Statements`). The statements of part 2 were frozen on 2026-11-10, after the report on part 1 and after the owner said to continue. + +[[DC-6.2]] +=== DC-6.2: a type is closed, and the type variable of the task is an Agda variable + +*The task text.* "A GADT match in System FC brings an equality such as `a ~ Int` into scope." The type `a` is a type variable. + +*The limit.* The source calculus of Stage 3 has closed types only (DC-3.1). A term of the target calculus has closed types only (`Wager.L2.Typing`: a context gives a closed type to each variable). The systemet documents have no quantifier over types. +This stage does not add type variables to a term of the source or of the target. + +*Choice.* The program of the stage is a family of closed programs. The Agda variable α is the type variable `a` of the Haskell text: `Wager.Local.Gadt.gadt-eval b α` is the function `eval` at the closed instance `a := α`. +The erased term does not depend on α (`Wager.Examples.Stage6.one-erased-text`, and `Wager.Local.Separation.erased-program` for each base type). + +*Consequence.* At a closed instance, a local equality is true or it is false. The two constructors of the program have two different right sides (`b` and `b + b`), so at least one of the two branches of `gadt-eval b α` has a false assumption, for each α. +In System FC such a branch cannot run. This development has no proof of this sentence for its source calculus (DC-6.3). The branch is a part of the program text, and its typing needs the assumption. + +*Not done.* A source or a target with a quantifier over types. A statement about one target term for all instances that has one polymorphic type. + +[[DC-6.3]] +=== DC-6.3: the source calculus of Stage 6 + +*Choice.* `Wager.Local.Source` is a new small calculus. It has base types, functions, sums, and the type `⟨ τ ~ σ ⟩ ρ`. + +* `⟨ τ ~ σ ⟩ ρ` is the type of a GADT constructor field of System FC: a value of the type ρ, with evidence that τ and σ are equal. `lpack` makes such a value from an equality that holds in the current assumptions. +* `lopen` is the match. Its body has the equality `τ ~ σ` as a local assumption (`Eqs`). +* `Coˡ` is equality of two types under assumptions: an assumption, reflexivity, symmetry, transitivity, and congruence for functions and sums. It is a nominal coercion of System FC. It has no role. +* A GADT with more than one constructor is a sum of such types (`Wager.Local.Gadt.G`). + +*What the calculus does not have.* The newtypes, the roles and the type-level functions of Stage 3. The separation does not need them. The calculus is not an extension of the Agda definitions of Stage 3, so no definition of stages 3 to 5 changes. + +*Erasure.* Evidence has no erased type and no erased term: `erˡ (⟨ τ ~ σ ⟩ ρ)` is `erˡ ρ`, and `lpack` and `lcast` vanish. The match becomes a β-redex, so the scrutinee is evaluated before the body. + +*Not proved here.* Type safety of this source calculus. In particular this development has no proof of the sentence "no closed term has the type `⟨ τ ~ σ ⟩ ρ` when τ and σ are different". + +[[DC-6.4]] +=== DC-6.4: what "the target cannot type" means + +*Choice.* `Wager.L2.Erasure.erT` gives the erased type of a closed target type. It is read from the normal form: a trope state vanishes (`A@s` has the erased type of `A`) and a grade vanishes. `eraseᵗ` gives the erased term: a type, a grade and a trope transition vanish. +`eraseᵗ` has the equations of `Wager.Trans.Coercion.eraseT` of Stage 4, by inspection of the two definitions. Agda does not check that the two functions are equal. It is a new definition, because the definition of Stage 4 is in a module for one family of target signatures. + +"The target cannot type the program" means: no typed target term has the erased term of the source program together with a type that has the erased type of the source type. +The statement is for each target signature and each set of grade operations. + +*Reason.* Claim W asks for a translation that preserves types and that preserves behaviour after erasure. A translation that keeps the erased type and the erased term does this in the most direct way. The separation is about this kind of translation. + +*What the statement does not exclude.* + +* A translation that changes the erased type of the data. The erased program has a simple type with another argument type (`Wager.Examples.Stage6.other-erased-type`), and a typed target term with the same erasure exists at that type (`other-typed`, `other-same-erasure`). +* A translation that changes the text of the branch with the false assumption. + +The statement is thus weaker than "the program has no translation". The verdict file says this again at T7. + +[[DC-6.5]] +=== DC-6.5: the identity type is a family of base constants of a signature + +*The task text.* "Add an identity type as an ordinary indexed family used at grade `0`." + +*The documents.* They have no identity type and no rule for an indexed family. `03-l2-grades.adoc` says that `0` is "the grade of an unused assumption". + +*Choice.* DC-1.1 says that a later stage adds entries to a signature and does not add constructors to the language. The identity type is thus a family of entries (`Wager.Identity.Family.IdFamily`): + +* `Id A B` is a base constant, for each pair of closed types A and B of the kind ★. The family respects conversion in each index (`Id-conv`). +* `rfl A` is a literal of the base type `Id A A`. It is the one constructor. The existing rule `t-lit` types it, so there is no introduction rule. +* `diagonal`: a literal of the base type `Id A B` shows that A and B are convertible. The family thus has no constructor off the diagonal. + +*EQUALITY EVIDENCE IS NOW A TERM.* A term of the type `base (Id A B)` is evidence that A and B are equal. It is an ordinary value: a function can take it, a pair can hold it, and a variable can stand for it. A variable of such a type is a local equality assumption. + +*What does not change.* The type language (`Wager.L1.Syntax.Ty`), the conversion relation `DefEq`, normal forms, and the 12 rules of the target judgement. + +*Consequence.* Evidence is a value at run time: a literal. The erased type of `Id A B` is the base type `Id A B`. + +*The record is a hypothesis on a signature.* It does not say that a signature has a family. DC-6.8 gives one signature that has one. + +*Not chosen.* A new type former in `Ty`: it changes each definition of Stage 1. An encoding of `Id A B` as a trope state of `A ⊗ B`: a trope state is a different notion in the documents. + +[[DC-6.6]] +=== DC-6.6: one new term former and one new rule + +*Choice.* `cast e t` is the eliminator: e is evidence, t is the payload. The rule is `Wager.Identity.Typing.t-cast`: + +---- +γ ▸ Γ ⊢ⁱ e ∶ base (Id A B) δ ▸ Γ ⊢ⁱ t ∶ A +----------------------------------------------- +((𝟘 ·ᵘ γ) +ᵘ δ) ▸ Γ ⊢ⁱ cast e t ∶ B +---- + +The rule uses the evidence at the grade `𝟘`. It names no other grade, and it has no side condition for one algebra. + +*The Agda judgement is a new data type.* An Agda data type cannot get a constructor later. `_▸_⊢ⁱ_∶_` has the 12 rules of `Wager.L2.Typing` and the rule `t-cast`. The term syntax `ITm` has the 10 formers of `Wager.L2.Term.Tm` and `cast`. +`T7-Conservative` says that each typed target term is a typed term of the extension. Agda does not check that the 12 rules have the same text; this is by inspection of the two files. + +*Not done.* + +* The other direction: that a derivation with no cast is a derivation of the target. +* A reduction relation for the extension. The relation `_⟶_` of the target is not extended, and progress and preservation are not proved for the extension. The two erasures and the evaluation of the untyped calculus give the meaning of a term of the extension. + +[[DC-6.7]] +=== DC-6.7: what "erasure of its proofs is sound" means + +*The task text.* "Prove that erasure of its proofs is sound, by totality and the grade." + +*Choice.* A term of the extension has two erasures into the untyped calculus (`Wager.Identity.Term`): + +* `keepⁱ` is the reference. For `cast e t` it evaluates the evidence, then the payload, and it gives the value of the payload. It does not inspect the value of the evidence, because the untyped calculus has no test on a literal. +* `eraseⁱ` is the erasure of proofs: `eraseⁱ (cast e t)` is `eraseⁱ t`. The evidence is absent from the program. + +"Sound" is `T7-Erasure`: for a closed typed term, the two programs evaluate, and the two values are observationally equal at the erased type. + +*By totality.* The statement includes that the reference program has a value. If the evidence of a cast has no value, then the reference program has no value. The erased program can have a value. The statement is then false. +The proof also uses the value of the evidence: it is a literal of the type `Id A B`, so A and B are convertible (`diagonal`), so the payload type and the result type have one erased type. `T7-Canonicity` is this fact for a closed term. + +*By the grade.* `T7-Grade`: in a grade algebra, the usage vector of `cast e t` is the usage vector of the payload `t`, which is the term that remains after the erasure. The grade thus makes the resource count of the typed term equal to the resource count of the erased term at each cast. + +The proof of `T7-Erasure` does not use the grade. A test shows this: with the grade `𝟙` in the rule `t-cast`, the proofs of `T7-Erasure` and `T7-Canonicity` check, and the proof of `T7-Grade` does not (`TOOLCHAIN.adoc`, gate watch of part 2). +The behaviour comes from totality, and the resource count comes from the grade. This development has no semantics that counts resources, so it has no theorem that joins the two. + +*What the erasure does not remove.* Evidence that is data: an argument of a function, a component of a pair. Such evidence stays in the erased program as a literal. To remove it, the erasure must read the grade of a binder. Its soundness then needs a property of the grade algebra: in the one-point algebra each binder has the grade `𝟘`, and not each binder is unused. This is not done. + +*The separation of part 1.* `T7-Separation` is a statement about the target with no identity family. This part does not prove and does not refute the same statement for the extension. + +[[DC-6.8]] +=== DC-6.8: one signature that has an identity family + +*Choice.* `Wager.Identity.Instance` builds a signature from a set of base constants and a set of literals. Its base constants are codes: + +* `cb b` is a base constant of the start. +* `cid x y` is the family, at the codes of two closed normal forms. +* The other codes are the code of a closed normal form (`enc`). The function `enc` is injective (`enc-inj`). + +`Id A B` is `cid (enc (nf A)) (enc (nf B))`. The family is thus about the types of the same signature, also about a type that has an identity type in it. +The literals are the literals of the start and one literal for each code `c`, of the base type `cid c c`. + +*Reason.* A base constant cannot hold a type of its own signature directly: the type language is made after the signature. A code is a first-order copy of a closed normal form, so the set of base constants is an ordinary data type. + +*Limits.* + +* The signature has no generative constant, no primitive and no trope operation. It is one signature for the purpose. This development does not show that each signature has an extension with a family. +* Each code is a base constant, also a code that `enc` does not give. +* A literal exists for each code `c`, also when `c` is not the code of a type. Its base type `cid c c` is on the diagonal, so `diagonal` holds. + +== Stage 7 + +[[DC-7.1]] +=== DC-7.1: the model of types in the cubical universe + +*The task text.* "Interpret target types in the cubical universe and newtype transitions as equivalences. Show that the denotation of a translated coercion equals transport along the path from `ua`." The stage is optional. The owner asked for it on 2026-11-10. + +*Choice.* `Wager.Univalent.Model` interprets a closed type of the target of Stage 4 as a type of the cubical universe, by its normal form: + +* A base constant `b` is `El b`. `El` is a parameter of the model, with an element `elLit ℓ` for each literal. +* A function, a pair and a sum are the function type, the product and the sum. +* A newtype instance `capp s A` is `Box X`, where X is the interpretation of A. `Box` is a record with one field. It is a different type from X, and `unboxEquiv : Box X ≃ X` is an equivalence. + +A trope transition (wrap, unwrap) is thus an equivalence, and `ua unboxEquiv` is a path between the two types. + +*Not chosen.* The interpretation of `capp s A` as the interpretation of A. Each transition is then the identity equivalence, and the statement of the stage says no more than T3. + +*Limit.* The model has one wrapper for each state. It does not have a different type for each newtype name: two newtypes with one content have one interpretation. + +[[DC-7.2]] +=== DC-7.2: the denotation of a term is by realisers + +*The gap.* The development has no function from a typed term to an element of the model. The typing judgement of the target is declarative: it has a conversion rule and a subusage rule. A denotation by recursion on a derivation needs a proof that two derivations of one term give one element. This is not done. + +*Choice.* The model is a realisability model. `𝓡 u v x` says that the untyped value v realises the element x of the interpretation of the normal form u. A wrapper is not seen at run time: v realises `box x` when v realises x. +`Denotes X Y f g` says that the term transformer f denotes the function g: on a term that evaluates to a realiser of x, the term `f t` evaluates to a realiser of `g x`. + +"The denotation of a translated coercion equals transport along the path" is thus: the transformer of the coercion denotes the function `transport (pathOf wr γ)`. + +*Limits.* The statement is about an element that has a realiser. The development does not show that each element of the model has a realiser, and it does not show that a realiser has one element only. It has no fundamental lemma for each typed term of the target. + +[[DC-7.3]] +=== DC-7.3: the path of a coercion + +*Choice.* `pathOf wr γ` is a path between the interpretations of the two translated types, by recursion on the coercion: + +* a newtype axiom gives `ua unboxEquiv`, moved along the equation of the type translation (`T-embE`, `T-inst`); +* symmetry gives `sym`, transitivity gives the composition of paths; +* a function, a pair and a sum give the congruence of the type former; +* a nominal coercion gives the path of two types with one normal form; +* congruence for a newtype gives the path of the body below the wrapper, by the role of the parameter. + +The path needs the source role check, as the typing of a translated coercion does (T3). diff --git a/verification/proofs/agda/Wager/Everything.agda b/verification/proofs/agda/Wager/Everything.agda index 67bd9b1..aafdd5b 100644 --- a/verification/proofs/agda/Wager/Everything.agda +++ b/verification/proofs/agda/Wager/Everything.agda @@ -69,3 +69,18 @@ import Wager.Trans.Simulation import Wager.Trans.RoleCorrespondence import Wager.Trans.TwoStateProofs import Wager.Examples.Stage4 +import Wager.Examples.Stage5 +import Wager.L2.Erasure +import Wager.Local.Source +import Wager.Local.Gadt +import Wager.Local.Separation +import Wager.Examples.Stage6 +import Wager.Identity.Family +import Wager.Identity.Term +import Wager.Identity.Typing +import Wager.Identity.Soundness +import Wager.Identity.Instance +import Wager.Examples.Stage6Identity +import Wager.Univalent.Model +import Wager.Univalent.CrossCheck +import Wager.Examples.Stage7 diff --git a/verification/proofs/agda/Wager/Examples/Stage5.agda b/verification/proofs/agda/Wager/Examples/Stage5.agda new file mode 100644 index 0000000..2897976 --- /dev/null +++ b/verification/proofs/agda/Wager/Examples/Stage5.agda @@ -0,0 +1,173 @@ +{-# OPTIONS --cubical --safe #-} +-- Forced by cubical-0.9 (InfectiveImport). No coinduction is used. +{-# OPTIONS --guardedness #-} +-- DESIGN-CHOICES.adoc, DC-0.3: matches on kinded syntax. +{-# OPTIONS -WnoUnsupportedIndexedMatch #-} +-- SPDX-License-Identifier: MPL-2.0 +-- +-- Stage 5 anti-vacuity examples for T6. The source signature is +-- `taggedS rep` of Wager.FC.Tagged, the state scheme is the row scheme, +-- and the term grades are the one-point algebra. +-- +-- type family F a where { F Int = Bool ; F Age = Char ; F (Tag a) = G a } +-- type family G a where { G Int = Bool ; G Bool = Char } +module Wager.Examples.Stage5 where + +open import Cubical.Foundations.Prelude +open import Cubical.Data.Empty as ⊥ using (⊥) +open import Cubical.Data.Unit using (Unit; tt) +open import Cubical.Data.Sigma using (_×_; _,_) +open import Cubical.Data.Sum.Base using (inl; inr) +open import Cubical.Relation.Nullary using (¬_) + +open import Wager.Grade.Trivial +open import Wager.Role.Role +open import Wager.FC.Tagged +import Wager.FC.Types +import Wager.FC.Coercion +import Wager.FC.Term +import Wager.Trans.Scheme +import Wager.Trans.Target +import Wager.Trans.Coercion +import Wager.L1.Normal +import Wager.L1.Eval +import Wager.L1.Conversion +import Wager.L2.Typing +open import Wager.Examples.Stage3 using (module Role-Check) +open import Wager.Proofs + +private + SS = taggedS rep + Sc = Wager.Trans.Scheme.rowScheme SS + +open Wager.FC.Types SS +open Wager.FC.Coercion SS +open Wager.FC.Term SS +open TTypes rep +open Role-Check using (wr-rep) +open Wager.Trans.Target SS Sc trivialOps using (tSig; tTSig; T; idx; Idx; Ty; ★; []; capp; base) +open Wager.Trans.Coercion SS Sc trivialOps using (tr; lit) +open Wager.L1.Normal tSig using (Nf; nbase; ncapp) +open Wager.L1.Eval tSig using (nf) +open Wager.L1.Conversion tSig using (DefEq) +open Wager.L2.Typing tSig tTSig trivialOps using (_▸_⊢_∶_) + +private + sUnit : STy + sUnit = sbase bUnit + +------------------------------------------------------------------------ +-- Accepted: one nominal coercion for each kind of equation, and the +-- instance of T6 for it. + +-- F Int = Bool (a base type). +f-int : Co nom (F sInt) sBool +f-int = c-fbase fE bInt + +f-int-nf : nf (T (F sInt)) ≡ nf (T sBool) +f-int-nf = t6 SS Sc trivialOps f-int + +-- F Age = Char (a newtype with no parameter). +f-age : Co nom (F sAge) sChar +f-age = c-fnt₀ fE ageE + +f-age-nf : nf (T (F sAge)) ≡ nf (T sChar) +f-age-nf = t6 SS Sc trivialOps f-age + +-- F (Tag Int) = G Int = Bool (the function looks at the argument of Tag). +f-tag-int : Co nom (F (Tag sInt)) sBool +f-tag-int = c-trans (c-fnt₁ fE tagE sInt) (c-fbase gE bInt) + +f-tag-int-nf : nf (T (F (Tag sInt))) ≡ nf (T sBool) +f-tag-int-nf = t6 SS Sc trivialOps f-tag-int + +-- F (Int → Int) = Unit (a function type). +f-arr : Co nom (F (sInt ⇒ˢ sInt)) sUnit +f-arr = c-farr fE sInt sInt + +f-arr-nf : nf (T (F (sInt ⇒ˢ sInt))) ≡ nf (T sUnit) +f-arr-nf = t6 SS Sc trivialOps f-arr + +-- Congruence: T (F Age) ~N T Char, below the nominal newtype T. +tee-cong : Co nom (Tee (F sAge)) (Tee sChar) +tee-cong = c-nt₁ teeE f-age + +tee-cong-defeq : DefEq (T (Tee (F sAge))) (T (Tee sChar)) +tee-cong-defeq = t6-conversion SS Sc trivialOps tee-cong + +-- The normal form is the value that the source function computes. +f-tag-int-value : nf (T (F (Tag sInt))) ≡ nbase bBool +f-tag-int-value = refl + +------------------------------------------------------------------------ +-- Accepted (T6-No-Term): a cast along a nominal coercion leaves no +-- term. The literal 'c' : Char, cast to the type `F Age`, translates to +-- the literal. The translation is typed at the translated type `F Age`: +-- the type changes by conversion. + +charAsFAge : STm ∅ˢ (F sAge) +charAsFAge = cast (c-sub (c-sym f-age)) (slit ℓchar) + +no-term : tr charAsFAge ≡ lit ℓchar +no-term = t6-no-term SS Sc trivialOps {Γ = ∅ˢ} (c-sym f-age) (slit ℓchar) + +typed-by-conversion : (λ _ → tt) ▸ (λ i → T (∅ˢ i)) ⊢ tr charAsFAge ∶ T (F sAge) +typed-by-conversion = t5-typing SS Sc trivial wr-rep tt tt charAsFAge + +------------------------------------------------------------------------ +-- Rejected: types with no nominal coercion, and their translations +-- have different normal forms. T6 is thus not true for an empty reason. + +private + IsCapp : Nf [] ★ → Type + IsCapp (ncapp c a) = Unit + IsCapp _ = ⊥ + + IsBoolNf : Nf [] ★ → Type + IsBoolNf (nbase bBool) = Unit + IsBoolNf _ = ⊥ + + IsAgeV : VTy → Type + IsAgeV (vnt₀ ageE) = Unit + IsAgeV _ = ⊥ + + IsTagCharV : VTy → Type + IsTagCharV (vnt₁ tagE (vbase bChar)) = Unit + IsTagCharV _ = ⊥ + +-- Age and Int: no nominal coercion in the source ... +age-int-rejected : ¬ Co nom sAge sInt +age-int-rejected γ = subst IsAgeV (source-nominal-soundness SS _ _ γ) tt + +-- ... and two different normal forms in the target. +age-int-nf-differ : ¬ (nf (T sAge) ≡ nf (T sInt)) +age-int-nf-differ p = subst IsCapp p tt + +-- F Int is Bool and F Age is Char. +f-int-age-nf-differ : ¬ (nf (T (F sInt)) ≡ nf (T (F sAge))) +f-int-age-nf-differ p = subst IsBoolNf p tt + +------------------------------------------------------------------------ +-- A finding: the converse of T6 is false for the row scheme. `Tag Char` +-- and `Tag Unit` have no nominal coercion in the source. No type-level +-- function tells them apart, so they have one row, one state and one +-- target type. + +tag-char-unit-rejected : ¬ Co nom (Tag sChar) (Tag sUnit) +tag-char-unit-rejected γ = subst IsTagCharV (source-nominal-soundness SS _ _ γ) tt + +private + same-row : idx tagE (vbase bChar) ≡ idx tagE (vbase bUnit) + same-row = funExt λ { fE → refl ; gE → refl } + + tagAt : Idx → Ty [] ★ + tagAt i = capp (inr (tagE , i)) (base bInt) + +tag-char-unit-one-type : T (Tag sChar) ≡ T (Tag sUnit) +tag-char-unit-one-type = + cong tagAt same-row + +-- The two source types do have a representational coercion: the +-- parameter of Tag is phantom. +tag-char-unit-rep : Co rep (Tag sChar) (Tag sUnit) +tag-char-unit-rep = c-nt₁ tagE c-ph diff --git a/verification/proofs/agda/Wager/Examples/Stage6.agda b/verification/proofs/agda/Wager/Examples/Stage6.agda new file mode 100644 index 0000000..98fb63b --- /dev/null +++ b/verification/proofs/agda/Wager/Examples/Stage6.agda @@ -0,0 +1,171 @@ +{-# OPTIONS --cubical --safe #-} +-- Forced by cubical-0.9 (InfectiveImport). No coinduction is used. +{-# OPTIONS --guardedness #-} +-- SPDX-License-Identifier: MPL-2.0 +-- +-- Stage 6 anti-vacuity examples for T7, the separation. +-- +-- The target signature of the examples is the signature of Stage 5: +-- `tSig` for `taggedS rep`, the row scheme, and the one-point grade +-- algebra. The base type of the GADT is `Int`. +module Wager.Examples.Stage6 where + +open import Cubical.Foundations.Prelude +open import Cubical.Data.Empty as ⊥ using (⊥) +open import Cubical.Data.Unit using (Unit; tt) +open import Cubical.Data.Sigma using (_×_; _,_; Σ-syntax) +open import Cubical.Data.Nat.Base using (ℕ; zero; suc) +open import Cubical.Data.FinData.Base using (Fin; zero; suc) +open import Cubical.Relation.Nullary using (¬_) + +open import Wager.Grade.Trivial +open import Wager.Role.Role +open import Wager.FC.Tagged +import Wager.Trans.Scheme +import Wager.Trans.Target +import Wager.L1.Syntax +import Wager.L2.Typing +import Wager.L2.Erasure +open import Wager.Erased.Untyped +import Wager.Local.Source +import Wager.Local.Gadt +import Wager.Local.Separation +open import Wager.Proofs + +private + SS = taggedS rep + Sc = Wager.Trans.Scheme.rowScheme SS + +open Wager.Trans.Target SS Sc trivialOps using (tSig; tTSig) +open Wager.L1.Syntax tSig using (Ty; []; ★; base; arr; _⊕_; Base) +open Wager.L2.Typing tSig tTSig trivialOps +open Wager.L2.Erasure tSig tTSig trivialOps using (erT; eraseᵗ; identity-one-type) +open Typing litTy using (_⊢ᵉ_∶_; ∅ᶜ; u-var; u-lam; u-app; u-case) +open Wager.Local.Source Base Lit litTy +open Wager.Local.Gadt Base Lit litTy +open Wager.Local.Separation tSig tTSig trivialOps using (gadt-evalᵘ; erased-program) + +private + variable + τ σ : LTy + + tInt : Ty [] ★ + tInt = base bInt + + lInt : LTy + lInt = lbase bInt + + -- The empty target context and its usage vector. + ∅ᵗ : Cx 0 + ∅ᵗ () + + ∅ᵘ : Usage 0 + ∅ᵘ _ = tt + +------------------------------------------------------------------------ +-- Accepted: the source program. + +-- The program is a term of the source calculus at each instance. +-- Here: the instances `a := Int` and `a := Int + Int`. +eval-at-int : LTm ∅ᵃ ∅ˡ (G bInt lInt ⇒ˡ lInt) +eval-at-int = gadt-eval bInt lInt + +eval-at-sum : LTm ∅ᵃ ∅ˡ (G bInt (lInt +ˡ lInt) ⇒ˡ lInt) +eval-at-sum = gadt-eval bInt (lInt +ˡ lInt) + +-- The text of the program does not depend on the instance. +one-erased-text : ∀ α α' → eraseˡ (gadt-eval bInt α) ≡ eraseˡ (gadt-eval bInt α') +one-erased-text α α' = refl + +-- The constructor GI at the instance `a := Int`, with the literal `ℓint`. +-- The evidence is reflexivity. +gi-one : LTm ∅ᵃ ∅ˡ (G bInt lInt) +gi-one = linl (lpack l-refl (llit ℓint)) + +-- The first branch runs: the erased program gives the literal. +live-branch-runs : ∅ᵉ ⊢ eraseˡ (lapp eval-at-int gi-one) ⇓ vlit ℓint +live-branch-runs = + ⇓-app ⇓-lam (⇓-inl ⇓-lit) + (⇓-casel (⇓-var zero) (⇓-app ⇓-lam (⇓-var zero) (⇓-var zero))) + +------------------------------------------------------------------------ +-- Rejected in the source: the constructor GB at the instance +-- `a := Int` needs evidence for `Int ~ Int + Int`. With no assumption, +-- an equality of the source calculus is the identity of types. + +closed-equality-is-identity : Coˡ ∅ᵃ τ σ → τ ≡ σ +closed-equality-is-identity l-refl = refl +closed-equality-is-identity (l-sym γ) = sym (closed-equality-is-identity γ) +closed-equality-is-identity (l-trans γ δ) = + closed-equality-is-identity γ ∙ closed-equality-is-identity δ +closed-equality-is-identity (l-arr γ δ) = + cong₂ _⇒ˡ_ (closed-equality-is-identity γ) (closed-equality-is-identity δ) +closed-equality-is-identity (l-sum γ δ) = + cong₂ _+ˡ_ (closed-equality-is-identity γ) (closed-equality-is-identity δ) + +private + IsLBase : LTy → Type + IsLBase (lbase b) = Unit + IsLBase (τ ⇒ˡ σ) = ⊥ + IsLBase (τ +ˡ σ) = ⊥ + IsLBase (⟨ τ ~ σ ⟩ ρ) = ⊥ + +no-evidence-for-gb : ¬ Coˡ ∅ᵃ lInt (lInt +ˡ lInt) +no-evidence-for-gb γ = subst IsLBase (closed-equality-is-identity γ) tt + +------------------------------------------------------------------------ +-- Rejected in the target: the instance of T7 for this signature, at +-- the instance `a := Int` of the program. + +no-target-term : + ¬ (Σ[ t ∈ Tm 0 ] Σ[ A ∈ Ty [] ★ ] + (∅ᵘ ▸ ∅ᵗ ⊢ t ∶ A) + × (erT A ≡ erˡ (G bInt lInt ⇒ˡ lInt)) + × (eraseᵗ t ≡ eraseˡ eval-at-int)) +no-target-term (t , A , d , eA , eT) = + t7-separation tSig tTSig trivialOps bInt lInt d eA eT + +-- The simplest case of "no hypothetical equality": the identity +-- function has no type `Int → Int + Int` in the target. +identity-rejected : + ¬ (∅ᵘ ▸ ∅ᵗ ⊢ tlam tt tInt (tvar zero) ∶ arr tt tInt (tInt ⊕ tInt)) +identity-rejected d = subst IsBaseE (identity-one-type d refl) tt + where + IsBaseE : ETy Base → Type + IsBaseE (ebase x) = Unit + IsBaseE (earr a c) = ⊥ + IsBaseE (eprod a c) = ⊥ + IsBaseE (esum a c) = ⊥ + +------------------------------------------------------------------------ +-- Accepted in the target, with another type of the data. This shows +-- what T7 does not exclude (DC-6.4): the erased program has a simple +-- type when the argument of GB has the erased type `Int + Int`. + +other-erased-type : + ∅ᶜ ⊢ᵉ gadt-evalᵘ ∶ earr (esum (ebase bInt) (esum (ebase bInt) (ebase bInt))) (ebase bInt) +other-erased-type = + u-lam (u-case (u-var zero refl) + (u-app (u-lam (u-var zero refl)) (u-var zero refl)) + (u-app (u-lam (u-case (u-var zero refl) (u-var zero refl) (u-var zero refl))) + (u-var zero refl))) + +-- A typed target term with the erasure of the source program. Its type +-- does not have the erased type of the source type. +private + other : Tm 0 + other = + tlam tt (tInt ⊕ (tInt ⊕ tInt)) + (case (tvar zero) + (tapp (tlam tt tInt (tvar zero)) (tvar zero)) + (tapp (tlam tt (tInt ⊕ tInt) (case (tvar zero) (tvar zero) (tvar zero))) + (tvar zero))) + +other-typed : ∅ᵘ ▸ ∅ᵗ ⊢ other ∶ arr tt (tInt ⊕ (tInt ⊕ tInt)) tInt +other-typed = + t-lam (t-case (t-var zero) + (t-app (t-lam (t-var zero)) (t-var zero)) + (t-app (t-lam (t-case (t-var zero) (t-var zero) (t-var zero))) (t-var zero))) + +other-same-erasure : eraseᵗ other ≡ eraseˡ eval-at-int +other-same-erasure = refl diff --git a/verification/proofs/agda/Wager/Examples/Stage6Identity.agda b/verification/proofs/agda/Wager/Examples/Stage6Identity.agda new file mode 100644 index 0000000..2cf8d5d --- /dev/null +++ b/verification/proofs/agda/Wager/Examples/Stage6Identity.agda @@ -0,0 +1,245 @@ +{-# OPTIONS --cubical --safe #-} +-- Forced by cubical-0.9 (InfectiveImport). No coinduction is used. +{-# OPTIONS --guardedness #-} +-- DESIGN-CHOICES.adoc, DC-0.3: matches on normal forms and on evaluations. +{-# OPTIONS -WnoUnsupportedIndexedMatch #-} +-- SPDX-License-Identifier: MPL-2.0 +-- +-- Stage 6, part 2: anti-vacuity examples for T7, the identity type. +-- +-- The signature of the examples is `Wager.Identity.Instance`, with one +-- base constant (`int`) and one literal (`one`). The grade algebra is +-- the one-point algebra, and for one example the algebra {0, 1, ω}. +module Wager.Examples.Stage6Identity where + +open import Cubical.Foundations.Prelude +open import Cubical.Data.Empty as ⊥ using (⊥) +open import Cubical.Data.Unit using (Unit; tt) +open import Cubical.Data.Sigma using (_×_; _,_; Σ-syntax) +open import Cubical.Data.Sum.Base using (inl; inr) +open import Cubical.Data.Nat.Base using (ℕ; zero; suc) +open import Cubical.Data.FinData.Base using (Fin; zero; suc) +open import Cubical.Relation.Nullary using (¬_) + +open import Wager.Grade.Algebra +open import Wager.Grade.Trivial +open import Wager.Grade.Affine using (Affine; a0; a1; affineOps; affineLaws) +import Wager.Identity.Instance +import Wager.Identity.Typing +import Wager.L1.Syntax +import Wager.L1.Normal +import Wager.L1.Conversion +import Wager.L1.Equality +import Wager.L2.Erasure +open import Wager.Erased.Untyped +import Wager.Erased.LogRel +open import Wager.Proofs + +-- The start of the signature: one base constant and one literal. +data B₀ : Type where + int : B₀ + +data L₀ : Type where + one : L₀ + +open Wager.Identity.Instance B₀ L₀ (λ _ → int) trivialOps +open Wager.L1.Syntax sig using (Ty; []; ★; base; arr; _⊗_; _⊕_) +open Wager.L1.Normal sig using (Nf; nbase) +open Wager.L1.Conversion sig using (DefEq; d-refl) +open Wager.L1.Equality sig using (defEq→nf) +open Wager.L2.Erasure sig tsig trivialOps using (erT) +open Wager.Identity.Typing sig tsig trivialOps family +open Terms Lit +open Wager.Erased.LogRel litTy using (FO; fo-base) + +private + -- The empty context and its usage vector. + ∅ᵗ : Cx 0 + ∅ᵗ () + + ∅ᵘ : Usage 0 + ∅ᵘ () + +tInt : Ty [] ★ +tInt = base (cb int) + +ℓone : Lit +ℓone = inl one + +------------------------------------------------------------------------ +-- The family is not empty, and it is the family of the instance. + +-- The constant `Id Int Int` is `cid` at the code of `Int`, two times. +id-int-int : Id tInt tInt ≡ cid (cq (cb int)) (cq (cb int)) +id-int-int = refl + +------------------------------------------------------------------------ +-- T7-Intro and T7-Erasure. ACCEPTED: a cast along `rfl`. + +-- A conversion gives evidence. +evidence-int : ∅ᵘ ▸ ∅ᵗ ⊢ⁱ ilit (rfl tInt) ∶ base (Id tInt tInt) +evidence-int = t7-intro sig tsig trivialOps family {A = tInt} {B = tInt} d-refl + +-- The literal one, moved from Int to Int along the evidence. +cast-one : ITm 0 +cast-one = cast (ilit (rfl tInt)) (ilit ℓone) + +cast-one-typed : ∅ᵘ ▸ ∅ᵗ ⊢ⁱ cast-one ∶ tInt +cast-one-typed = t-cast {A = tInt} {B = tInt} evidence-int (t-lit ℓone) + +-- The erasure of proofs has no evidence. +cast-one-erased : eraseⁱ cast-one ≡ ulit ℓone +cast-one-erased = refl + +-- The reference program evaluates the evidence, then the literal. +cast-one-keep : ∅ᵉ ⊢ keepⁱ cast-one ⇓ vlit ℓone +cast-one-keep = ⇓-letp (⇓-pair ⇓-lit ⇓-lit) (⇓-var zero) + +cast-one-erase : ∅ᵉ ⊢ eraseⁱ cast-one ⇓ vlit ℓone +cast-one-erase = ⇓-lit + +-- T7 at a first-order type: one value for the two programs. +cast-one-sound : + Σ[ v ∈ UVal ] (∅ᵉ ⊢ keepⁱ cast-one ⇓ v) × (∅ᵉ ⊢ eraseⁱ cast-one ⇓ v) +cast-one-sound = + t7-erasure-first-order sig tsig trivialOps family cast-one-typed fo-base + +------------------------------------------------------------------------ +-- T7-Canonicity. REJECTED: closed evidence that Int is Int + Int. + +private + IsNBase : Nf [] ★ → Type + IsNBase (nbase _) = Unit + IsNBase _ = ⊥ + +no-evidence : ∀ {e : ITm 0} → ¬ (∅ᵘ ▸ ∅ᵗ ⊢ⁱ e ∶ base (Id tInt (tInt ⊕ tInt))) +no-evidence d = + subst IsNBase + (defEq→nf (t7-canonicity sig tsig trivialOps family {A = tInt} {B = tInt ⊕ tInt} d)) tt + +------------------------------------------------------------------------ +-- T7-Erasure. REJECTED: a cast whose evidence has no value. The term +-- has no type, and the conclusion of T7 is false for it. + +-- The evidence is the application of a literal to a literal. +stuck : ITm 0 +stuck = cast (iapp (ilit ℓone) (ilit ℓone)) (ilit ℓone) + +-- The program with no evidence has a value. +stuck-erase : ∅ᵉ ⊢ eraseⁱ stuck ⇓ vlit ℓone +stuck-erase = ⇓-lit + +-- The reference program has no value: a literal is not a function. +stuck-keep : ∀ {v} → ¬ (∅ᵉ ⊢ keepⁱ stuck ⇓ v) +stuck-keep (⇓-letp (⇓-pair (⇓-app () _ _) _) _) + +-- So the term has no type (by T7). +stuck-untyped : ∀ {A} → ¬ (∅ᵘ ▸ ∅ᵗ ⊢ⁱ stuck ∶ A) +stuck-untyped d = + let (v , w , dv , dw , h) = t7-erasure sig tsig trivialOps family d + in stuck-keep dv + +------------------------------------------------------------------------ +-- T7-Assumption. ACCEPTED: a local equality assumption. + +-- A typed closed function from Int to Int + Int, under the assumption +-- that the two types are equal. +assume : ITm 0 +assume = use-assumption tInt (tInt ⊕ tInt) + +assume-typed : + ∅ᵘ ▸ ∅ᵗ ⊢ⁱ assume ∶ arr tt (base (Id tInt (tInt ⊕ tInt))) (arr tt tInt (tInt ⊕ tInt)) +assume-typed = + t7-assumption sig tsig trivialOps family trivialLaws tInt (tInt ⊕ tInt) + +-- Its erasure is `λ e. λ x. x`. The inner function is the identity, from +-- Int to Int + Int. In the target with no family, a typed function that +-- erases to the identity has one erased type on its two sides +-- (`Wager.L2.Erasure.identity-one-type`). +assume-erased : eraseⁱ assume ≡ ulam (ulam (uvar zero)) +assume-erased = refl + +-- No closed term can be its argument (`no-evidence`): the assumption is +-- false, so the body does not run in a closed typed program. + +-- The same function in the algebra {0, 1, ω}: the assumption has the +-- grade 0, the grade of an unused assumption. +module AtAffine where + private module I = Wager.Identity.Instance B₀ L₀ (λ _ → int) affineOps + open Wager.L1.Syntax I.sig using () renaming (Ty to Tyᵃ; [] to []ᵃ; ★ to ★ᵃ; base to baseᵃ; arr to arrᵃ; _⊕_ to _⊕ᵃ_) + open Wager.Identity.Typing I.sig I.tsig affineOps I.family + using () renaming (_▸_⊢ⁱ_∶_ to _▸_⊢ᵃ_∶_; use-assumption to use-assumptionᵃ; Id to Idᵃ; 0ᵘ to 0ᵃ; Cx to Cxᵃ) + + private + tIntᵃ : Tyᵃ []ᵃ ★ᵃ + tIntᵃ = baseᵃ (I.cb int) + + ∅ᵃ : Cxᵃ 0 + ∅ᵃ () + + assume-affine : + 0ᵃ ▸ ∅ᵃ ⊢ᵃ use-assumptionᵃ tIntᵃ (tIntᵃ ⊕ᵃ tIntᵃ) + ∶ arrᵃ a0 (baseᵃ (Idᵃ tIntᵃ (tIntᵃ ⊕ᵃ tIntᵃ))) (arrᵃ a1 tIntᵃ (tIntᵃ ⊕ᵃ tIntᵃ)) + assume-affine = + t7-assumption I.sig I.tsig affineOps I.family affineLaws tIntᵃ (tIntᵃ ⊕ᵃ tIntᵃ) + +------------------------------------------------------------------------ +-- The GADT program of part 1, in the extension. ACCEPTED. +-- +-- The data holds the evidence: a constructor is a pair of the evidence +-- and the payload. The Agda variable α is the type variable of the +-- Haskell text (DESIGN-CHOICES.adoc, DC-6.2). + +Gⁱ : Ty [] ★ → Ty [] ★ +Gⁱ α = (base (Id α tInt) ⊗ α) ⊕ (base (Id α (tInt ⊕ tInt)) ⊗ α) + +evalⁱ : Ty [] ★ → ITm 0 +evalⁱ α = + ilam tt (Gⁱ α) (icase (ivar zero) + (iletp (ivar zero) (cast (ivar (suc zero)) (ivar zero))) + (iletp (ivar zero) + (icase (cast (ivar (suc zero)) (ivar zero)) (ivar zero) (ivar zero)))) + +-- The program is typed for each α, in the one-point algebra. +evalⁱ-typed : ∀ α → ∅ᵘ ▸ ∅ᵗ ⊢ⁱ evalⁱ α ∶ arr tt (Gⁱ α) tInt +evalⁱ-typed α = + t-lam (t-case (t-var zero) + (t-letp (t-var zero) (t-cast (t-var (suc zero)) (t-var zero))) + (t-letp (t-var zero) + (t-case (t-cast (t-var (suc zero)) (t-var zero)) (t-var zero) (t-var zero)))) + +-- One erased text for each α. No cast and no evidence is in it, except +-- the evidence that the data holds. +evalⁱ-erased : ∀ α → eraseⁱ (evalⁱ α) ≡ + ulam (ucase (uvar zero) + (uletp (uvar zero) (uvar zero)) + (uletp (uvar zero) (ucase (uvar zero) (uvar zero) (uvar zero)))) +evalⁱ-erased α = refl + +-- The program at α := Int, on the first constructor with the literal one. +gi-one : ITm 0 +gi-one = iapp (evalⁱ tInt) (iinj₁ (ipair (ilit (rfl tInt)) (ilit ℓone))) + +gi-one-typed : ∅ᵘ ▸ ∅ᵗ ⊢ⁱ gi-one ∶ tInt +gi-one-typed = + t-app (evalⁱ-typed tInt) (t-inj₁ (t-pair evidence-int (t-lit ℓone))) + +-- The erased program gives the literal one. +gi-one-runs : ∅ᵉ ⊢ eraseⁱ gi-one ⇓ vlit ℓone +gi-one-runs = + ⇓-app ⇓-lam (⇓-inl (⇓-pair ⇓-lit ⇓-lit)) + (⇓-casel (⇓-var zero) (⇓-letp (⇓-var zero) (⇓-var zero))) + +-- T7: the reference program and the erased program give one value. +gi-one-sound : + Σ[ v ∈ UVal ] (∅ᵉ ⊢ keepⁱ gi-one ⇓ v) × (∅ᵉ ⊢ eraseⁱ gi-one ⇓ v) +gi-one-sound = + t7-erasure-first-order sig tsig trivialOps family gi-one-typed fo-base + +-- THE LIMIT (DESIGN-CHOICES.adoc, DC-6.7). The erased type of the data +-- has a component for the evidence. In part 1 the erased type of the +-- source data has no such component. +data-holds-evidence : erT (Gⁱ tInt) ≡ + esum (eprod (ebase (Id tInt tInt)) (ebase (cb int))) + (eprod (ebase (Id tInt (tInt ⊕ tInt))) (ebase (cb int))) +data-holds-evidence = refl diff --git a/verification/proofs/agda/Wager/Examples/Stage7.agda b/verification/proofs/agda/Wager/Examples/Stage7.agda new file mode 100644 index 0000000..bf1a497 --- /dev/null +++ b/verification/proofs/agda/Wager/Examples/Stage7.agda @@ -0,0 +1,132 @@ +{-# OPTIONS --cubical --safe #-} +-- Forced by cubical-0.9 (InfectiveImport). No coinduction is used. +{-# OPTIONS --guardedness #-} +-- DESIGN-CHOICES.adoc, DC-0.3: matches on evaluations and on realisers. +{-# OPTIONS -WnoUnsupportedIndexedMatch #-} +-- SPDX-License-Identifier: MPL-2.0 +-- +-- Stage 7 anti-vacuity examples for the univalent cross-check. +-- +-- The source signature is `taggedS rep` of Wager.FC.Tagged, with the +-- row scheme and the one-point grade algebra. The model interprets +-- `Int` as the natural numbers, and the literal `ℓint` as the number 7. +module Wager.Examples.Stage7 where + +open import Cubical.Foundations.Prelude +open import Cubical.Data.Bool.Base using (Bool; true) +open import Cubical.Data.Empty as ⊥ using (⊥) +open import Cubical.Data.Unit using (Unit; tt) +open import Cubical.Data.Nat.Base using (ℕ; zero; suc) +open import Cubical.Data.FinData.Base using (Fin; zero; suc) +open import Cubical.Data.Sigma using (_×_; _,_; fst; snd; Σ-syntax) +open import Cubical.Relation.Nullary using (¬_) + +open import Wager.Grade.Trivial +open import Wager.Role.Role +open import Wager.FC.Signature +open import Wager.FC.Tagged +open import Wager.Erased.Untyped +import Wager.FC.Types +import Wager.FC.Coercion +import Wager.Trans.Scheme +import Wager.Trans.Target +import Wager.Trans.Coercion +import Wager.Univalent.Model +import Wager.L1.Eval +open import Wager.Examples.Stage3 using (module Role-Check) +open import Wager.Proofs + +private + SS = taggedS rep + Sc = Wager.Trans.Scheme.rowScheme SS + +-- The interpretation of the base constants, and of the 4 literals. +El : BaseName → Type +El bInt = ℕ +El bBool = Bool +El bChar = Unit +El bUnit = Unit + +elLit : (ℓ : LitName) → El (litTyC ℓ) +elLit ℓint = 7 +elLit ℓbool = true +elLit ℓchar = tt +elLit ℓunit = tt + +open Wager.FC.Types SS +open Wager.FC.Coercion SS +open TTypes rep renaming (Box to BoxS) +open Role-Check using (wr-rep) +open Wager.Trans.Target SS Sc trivialOps using (T; arr; tSig) +open Wager.L1.Eval tSig using (nf) +open Wager.Trans.Coercion SS Sc trivialOps using (coI; fwd; coerceT; eraseT; lit; Tm) +open Wager.Univalent.Model SS Sc trivial El elLit +open Terms Lit + +------------------------------------------------------------------------ +-- The model of two types. + +-- `Int` is the natural numbers. `Age` is a wrapper of them. +int-is-nat : ⟦ T sInt ⟧ ≡ ℕ +int-is-nat = refl + +age-is-box : ⟦ T sAge ⟧ ≡ Box ℕ +age-is-box = refl + +------------------------------------------------------------------------ +-- ACCEPTED: the newtype axiom `Age ~ Int`. + +age-co : Co rep sAge sInt +age-co = c-ax₀ ageE + +-- Transport along the path of the axiom takes the wrapper off. +age-transport : transport (pathOf wr-rep age-co) (box 7) ≡ 7 +age-transport = refl + +-- The literal `ℓint`, as a term of the type `Age`, realises `box 7`. +age-literal : Real (T sAge) ∅ᵉ (ulit ℓint) (box 7) +age-literal = vlit ℓint , ⇓-lit , r-lit ℓint refl + +-- The cross-check at this term: the coerced term evaluates to a +-- realiser of the transported element, which is the number 7. +age-coerced : + Real (T sInt) ∅ᵉ (eraseT (fwd (coI rep age-co) (lit ℓint))) + (transport (pathOf wr-rep age-co) (box 7)) +age-coerced = + coercion-denotes-transport SS Sc trivial El elLit wr-rep age-co (lit ℓint) (box 7) age-literal + +-- The coercion function is a closure that realises transport. +age-function : + Real (arr tt (T sAge) (T sInt)) ∅ᵉ (eraseT (coerceT age-co)) + (transport (pathOf wr-rep age-co)) +age-function = + coerce-function-is-transport SS Sc trivial El elLit wr-rep age-co + +------------------------------------------------------------------------ +-- ACCEPTED: congruence below a newtype with a parameter. +-- `BoxS a` is the source newtype `Box a` of the pair `(a, Int)`. + +box-co : Co rep (BoxS sAge) (BoxS sInt) +box-co = c-nt₁ boxE age-co + +-- Transport along its path changes the first component and keeps the +-- two wrappers of `Box`. +box-transport : + transport (pathOf wr-rep box-co) (box (box 7 , 3)) ≡ box (7 , 3) +box-transport = refl + +------------------------------------------------------------------------ +-- REJECTED: a literal does not realise a function. + +literal-not-function : + ∀ {f : ℕ → ℕ} → ¬ 𝓡 (nf (arr tt (T sInt) (T sInt))) (vlit ℓint) f +literal-not-function () + +-- REJECTED: the literal of the type `Bool` does not realise a number. +private + IsBool : BaseName → Type + IsBool bBool = Unit + IsBool _ = ⊥ + +bool-not-number : ∀ {k : ℕ} → ¬ Real (T sInt) ∅ᵉ (ulit ℓbool) k +bool-not-number (_ , ⇓-lit , r-lit _ p) = subst IsBool p tt diff --git a/verification/proofs/agda/Wager/Identity/Family.agda b/verification/proofs/agda/Wager/Identity/Family.agda new file mode 100644 index 0000000..0587006 --- /dev/null +++ b/verification/proofs/agda/Wager/Identity/Family.agda @@ -0,0 +1,43 @@ +{-# OPTIONS --cubical --safe #-} +-- Forced by cubical-0.9 (InfectiveImport). No coinduction is used. +{-# OPTIONS --guardedness #-} +-- SPDX-License-Identifier: MPL-2.0 +-- +-- The identity type of Stage 6, part 2, as entries of a signature +-- (DESIGN-CHOICES.adoc, DC-6.5). +-- +-- The type language and the conversion relation do not change. The +-- identity type is a family of base constants: one constant `Id A B` +-- for each pair of closed types. Its one constructor is a literal +-- `rfl A` of the base type `Id A A`. The existing rule for literals +-- types it. +-- +-- EQUALITY EVIDENCE IS NOW A TERM. A term of the type `base (Id A B)` +-- is evidence that the types A and B are equal. It is an ordinary +-- value: a function can take it, a pair can hold it. +-- +-- The record does not say that a signature has such a family. +-- `Wager.Identity.Instance` gives one signature that has one. +open import Wager.L1.Signature +import Wager.L2.Signature +module Wager.Identity.Family (S : Sig) (TS : Wager.L2.Signature.TSig S) where + +open import Cubical.Foundations.Prelude + +open import Wager.L1.Syntax S +open import Wager.L1.Conversion S +open Wager.L2.Signature S +open TSig TS + +record IdFamily : Type where + field + -- The family: a base constant for each pair of closed types. + Id : Ty [] ★ → Ty [] ★ → Base + -- The family respects conversion in each index. + Id-conv : ∀ {A A' B B'} → DefEq A A' → DefEq B B' → Id A B ≡ Id A' B' + -- The constructor: a literal on the diagonal. + rfl : Ty [] ★ → Lit + rfl-ty : ∀ A → litTy (rfl A) ≡ Id A A + -- No literal is in the family off the diagonal: a literal of the + -- base type `Id A B` shows that A and B are convertible. + diagonal : ∀ ℓ {A B} → litTy ℓ ≡ Id A B → DefEq A B diff --git a/verification/proofs/agda/Wager/Identity/Instance.agda b/verification/proofs/agda/Wager/Identity/Instance.agda new file mode 100644 index 0000000..f7ecad1 --- /dev/null +++ b/verification/proofs/agda/Wager/Identity/Instance.agda @@ -0,0 +1,140 @@ +{-# OPTIONS --cubical --safe #-} +-- Forced by cubical-0.9 (InfectiveImport). No coinduction is used. +{-# OPTIONS --guardedness #-} +-- DESIGN-CHOICES.adoc, DC-0.3: matches on normal forms. +{-# OPTIONS -WnoUnsupportedIndexedMatch #-} +-- SPDX-License-Identifier: MPL-2.0 +-- +-- A signature that has an identity family (Stage 6, part 2; +-- DESIGN-CHOICES.adoc, DC-6.8). It shows that the record `IdFamily` +-- is not empty. +-- +-- The start is a set B₀ of base constants and a set L₀ of literals. +-- The base constants of the signature are the codes: +-- +-- cb b the base constant b of the start +-- cid x y THE IDENTITY FAMILY, at the codes x and y of two closed +-- normal forms +-- cq, carr, cprod, csum +-- the code of a closed normal form (`enc`) +-- +-- `Id A B` is `cid (enc (nf A)) (enc (nf B))`. The function `enc` is +-- injective, and two types are convertible when they have one normal +-- form. So `Id A B` and `Id A' B'` are one constant exactly when A, A' +-- are convertible and B, B' are convertible. +-- +-- The literals are the literals of the start and one literal for each +-- code c, of the base type `cid c c`. +-- +-- The signature has no generative constant, no primitive and no trope +-- operation. Each code is a base constant, also a code that `enc` does +-- not give. +open import Cubical.Foundations.Prelude +open import Wager.Grade.Algebra +module Wager.Identity.Instance + (B₀ L₀ : Type) (ty₀ : L₀ → B₀) {R : Type} (ops : GradeOps R) where + +open import Cubical.Data.Empty as ⊥ using (⊥) +open import Cubical.Data.Unit using (Unit; tt) +open import Cubical.Data.Sum.Base using (_⊎_; inl; inr) +open import Cubical.Data.Maybe.Base using (Maybe; nothing; just) +open import Cubical.Data.Maybe.Properties using (just-inj) + +open import Wager.L1.Signature +import Wager.L2.Signature +import Wager.L2.Erasure +import Wager.Identity.Family + +data Code : Type where + cb : B₀ → Code + cid : Code → Code → Code + cq : Code → Code + carr : R → Code → Code → Code + cprod : Code → Code → Code + csum : Code → Code → Code + +sig : Sig +sig = record + { KG = Unit ; TG = R ; Base = Code + ; Con₁ = ⊥ ; cgrade = λ () + ; Prim = ⊥ ; pgrade = λ () ; onBase = λ () ; onCon = λ () ; onOther = λ () } + +-- The base type of a literal. +litTy′ : L₀ ⊎ Code → Code +litTy′ (inl ℓ) = cb (ty₀ ℓ) +litTy′ (inr c) = cid c c + +tsig : Wager.L2.Signature.TSig sig +tsig = record + { Lit = L₀ ⊎ Code ; litTy = litTy′ + ; Op = ⊥ ; carrier = λ () ; from = λ () ; to = λ () } + +open import Wager.L1.Syntax sig +open import Wager.L1.Normal sig +open import Wager.L1.Eval sig +open import Wager.L1.Conversion sig +open import Wager.L1.Equality sig +open Wager.L2.Erasure sig tsig ops using (noNe) + +------------------------------------------------------------------------ +-- The code of a closed normal form, and its inverse. + +enc : Nf [] ★ → Code +enc (ne m) = ⊥.rec (noNe m) +enc (nbase c) = cq c +enc (narr q a b) = carr q (enc a) (enc b) +enc (a n⊗ b) = cprod (enc a) (enc b) +enc (a n⊕ b) = csum (enc a) (enc b) + +private + map₂ : {A B C : Type} → (A → B → C) → Maybe A → Maybe B → Maybe C + map₂ f (just a) (just b) = just (f a b) + map₂ f _ _ = nothing + + dec : Code → Maybe (Nf [] ★) + dec (cb _) = nothing + dec (cid _ _) = nothing + dec (cq c) = just (nbase c) + dec (carr q x y) = map₂ (narr q) (dec x) (dec y) + dec (cprod x y) = map₂ _n⊗_ (dec x) (dec y) + dec (csum x y) = map₂ _n⊕_ (dec x) (dec y) + + dec-enc : (u : Nf [] ★) → dec (enc u) ≡ just u + dec-enc (ne m) = ⊥.rec (noNe m) + dec-enc (nbase c) = refl + dec-enc (narr q a b) = cong₂ (map₂ (narr q)) (dec-enc a) (dec-enc b) + dec-enc (a n⊗ b) = cong₂ (map₂ _n⊗_) (dec-enc a) (dec-enc b) + dec-enc (a n⊕ b) = cong₂ (map₂ _n⊕_) (dec-enc a) (dec-enc b) + +enc-inj : ∀ {u v} → enc u ≡ enc v → u ≡ v +enc-inj {u} {v} p = just-inj u v (sym (dec-enc u) ∙ cong dec p ∙ dec-enc v) + +------------------------------------------------------------------------ +-- The family. + +private + -- The two indices of a constant of the family. + cidL cidR : Code → Code + cidL (cid x y) = x + cidL c = c + cidR (cid x y) = y + cidR c = c + + isCid : Code → Type + isCid (cid _ _) = Unit + isCid _ = ⊥ + + diag : ∀ ℓ {A B : Ty [] ★} → + litTy′ ℓ ≡ cid (enc (nf A)) (enc (nf B)) → DefEq A B + -- A literal of the start has a base type of the start. + diag (inl ℓ) p = ⊥.rec (subst isCid (sym p) tt) + -- The literal of the code c has the type `cid c c`. + diag (inr c) p = nf→defEq (enc-inj (sym (cong cidL p) ∙ cong cidR p)) + +family : Wager.Identity.Family.IdFamily sig tsig +family = record + { Id = λ A B → cid (enc (nf A)) (enc (nf B)) + ; Id-conv = λ d e → cong₂ cid (cong enc (defEq→nf d)) (cong enc (defEq→nf e)) + ; rfl = λ A → inr (enc (nf A)) + ; rfl-ty = λ A → refl + ; diagonal = diag } diff --git a/verification/proofs/agda/Wager/Identity/Soundness.agda b/verification/proofs/agda/Wager/Identity/Soundness.agda new file mode 100644 index 0000000..30f4828 --- /dev/null +++ b/verification/proofs/agda/Wager/Identity/Soundness.agda @@ -0,0 +1,225 @@ +{-# OPTIONS --cubical --safe #-} +-- Forced by cubical-0.9 (InfectiveImport). No coinduction is used. +{-# OPTIONS --guardedness #-} +-- DESIGN-CHOICES.adoc, DC-0.3: matches on variables (Fin). +{-# OPTIONS -WnoUnsupportedIndexedMatch #-} +-- SPDX-License-Identifier: MPL-2.0 +-- +-- The erasure of proofs is sound (Stage 6, part 2: theorem T7). +-- +-- 1. The target is a part of the extension (`emb-typed`, `emb-keep`, +-- `emb-erase`). +-- 2. A conversion gives evidence (`intro`). +-- 3. The fundamental lemma (`fund`): for a typed term, in two related +-- environments, the reference program and the program with no +-- evidence in its casts evaluate to related values. The case of a +-- cast uses the value of the evidence: it is a literal of the type +-- `Id A B`, so A and B have one erased type (`evidence`). +-- 4. Closed terms: `erasure-sound`, `erasure-sound-fo`, `canonicity`. +-- 5. The grade: `cast-free`, and the function `use-assumption`. +-- +-- `fund` does not use the grade of the rule `t-cast`. `cast-free` does. +open import Wager.L1.Signature +open import Wager.Grade.Algebra +import Wager.L2.Signature +import Wager.Identity.Family +module Wager.Identity.Soundness + (S : Sig) (TS : Wager.L2.Signature.TSig S) (ops : GradeOps (Sig.TG S)) + (F : Wager.Identity.Family.IdFamily S TS) where + +open import Cubical.Foundations.Prelude +open import Cubical.Data.Nat.Base using (ℕ; zero; suc) +open import Cubical.Data.FinData.Base using (Fin; zero; suc) +open import Cubical.Data.Sigma using (_×_; _,_; Σ-syntax) + +open import Wager.L1.Syntax S +open import Wager.L1.Conversion S +open import Wager.L1.Equality S +import Wager.L2.Typing +open import Wager.L2.Term S TS using (Tm; tvar; tlam; tapp; pair; letp; inj₁; inj₂; case; lit; step) +open import Wager.L2.Erasure S TS ops using (erT; erN; er-at; eraseᵗ) +open import Wager.Identity.Typing S TS ops F +open import Wager.Erased.Untyped +open Terms Lit +open import Wager.Erased.LogRel litTy +open GradeOps ops + +private + module T = Wager.L2.Typing S TS ops + + variable + n : ℕ + +------------------------------------------------------------------------ +-- 1. The target is a part of the extension. + +emb-typed : ∀ {γ : Usage n} {Γ : Cx n} {t A} → γ T.▸ Γ ⊢ t ∶ A → γ ▸ Γ ⊢ⁱ emb t ∶ A +emb-typed (T.t-var i) = t-var i +emb-typed (T.t-lam d) = t-lam (emb-typed d) +emb-typed (T.t-app d e) = t-app (emb-typed d) (emb-typed e) +emb-typed (T.t-pair d e) = t-pair (emb-typed d) (emb-typed e) +emb-typed (T.t-letp d e) = t-letp (emb-typed d) (emb-typed e) +emb-typed (T.t-inj₁ d) = t-inj₁ (emb-typed d) +emb-typed (T.t-inj₂ d) = t-inj₂ (emb-typed d) +emb-typed (T.t-case d l r) = t-case (emb-typed d) (emb-typed l) (emb-typed r) +emb-typed (T.t-lit ℓ) = t-lit ℓ +emb-typed (T.t-step o d) = t-step o (emb-typed d) +emb-typed (T.t-conv d e) = t-conv (emb-typed d) e +emb-typed (T.t-sub d le) = t-sub (emb-typed d) le + +-- A target term has no cast, so its two erasures are its erasure. +emb-keep : (t : Tm n) → keepⁱ (emb t) ≡ eraseᵗ t +emb-keep (tvar i) = refl +emb-keep (tlam q A b) = cong ulam (emb-keep b) +emb-keep (tapp f a) = cong₂ uapp (emb-keep f) (emb-keep a) +emb-keep (pair s t) = cong₂ upair (emb-keep s) (emb-keep t) +emb-keep (letp s b) = cong₂ uletp (emb-keep s) (emb-keep b) +emb-keep (inj₁ t) = cong uinl (emb-keep t) +emb-keep (inj₂ t) = cong uinr (emb-keep t) +emb-keep (case s l r) i = ucase (emb-keep s i) (emb-keep l i) (emb-keep r i) +emb-keep (lit ℓ) = refl +emb-keep (step o t) = emb-keep t + +emb-erase : (t : Tm n) → eraseⁱ (emb t) ≡ eraseᵗ t +emb-erase (tvar i) = refl +emb-erase (tlam q A b) = cong ulam (emb-erase b) +emb-erase (tapp f a) = cong₂ uapp (emb-erase f) (emb-erase a) +emb-erase (pair s t) = cong₂ upair (emb-erase s) (emb-erase t) +emb-erase (letp s b) = cong₂ uletp (emb-erase s) (emb-erase b) +emb-erase (inj₁ t) = cong uinl (emb-erase t) +emb-erase (inj₂ t) = cong uinr (emb-erase t) +emb-erase (case s l r) i = ucase (emb-erase s i) (emb-erase l i) (emb-erase r i) +emb-erase (lit ℓ) = refl +emb-erase (step o t) = emb-erase t + +------------------------------------------------------------------------ +-- 2. A conversion gives evidence. + +intro : ∀ {Γ : Cx n} {A B} → DefEq A B → 0ᵘ ▸ Γ ⊢ⁱ ilit (rfl A) ∶ base (Id A B) +intro {A = A} d = + t-conv (t-lit (rfl A)) (≡→DefEq (cong base (rfl-ty A ∙ Id-conv d-refl d))) + +------------------------------------------------------------------------ +-- 3. The fundamental lemma. + +-- Two environments give related values to each variable. +EnvRel : Cx n → UEnv n → UEnv n → Type +EnvRel Γ ρ ρ' = ∀ i → 𝒱 (erT (Γ i)) (ρ i) (ρ' i) + +env-ext : ∀ {Γ : Cx n} {ρ ρ' : UEnv n} {v w} A → + EnvRel Γ ρ ρ' → 𝒱 (erT A) v w → EnvRel (Γ ▹ᶜ A) (v ∷ᵉ ρ) (w ∷ᵉ ρ') +env-ext A h hvw zero = hvw +env-ext A h hvw (suc i) = h i + +-- The value of evidence is a literal of the type `Id A B`. The family +-- has no literal off the diagonal, so A and B are convertible, and +-- they have one erased type. +evidence : ∀ {A B v w} → RBase (Id A B) v w → erT A ≡ erT B +evidence (r-lit ℓ p) = cong erN (defEq→nf (diagonal ℓ p)) + +fund : ∀ {γ : Usage n} {Γ : Cx n} {t A} → γ ▸ Γ ⊢ⁱ t ∶ A → + {ρ ρ' : UEnv n} → EnvRel Γ ρ ρ' → + ℰ (erT A) ρ (keepⁱ t) ρ' (eraseⁱ t) +fund (t-var i) h = _ , ⇓-var i , _ , ⇓-var i , h i +fund (t-lam {A = A} d) h = + _ , ⇓-lam , _ , ⇓-lam + , r-clo (λ v w hvw → + let (r , dr , s , ds , hrs) = fund d (env-ext A h hvw) + in r , s , dr , ds , hrs) +fund (t-app d e) h with fund d h | fund e h +... | _ , df , _ , df' , r-clo hf | va , da , wa , da' , ha = + let (r , s , dr , ds , hrs) = hf va wa ha + in r , ⇓-app df da dr , s , ⇓-app df' da' ds , hrs +fund (t-pair d e) h = + let (v₁ , d₁ , w₁ , d₁' , h₁) = fund d h + (v₂ , d₂ , w₂ , d₂' , h₂) = fund e h + in vpair v₁ v₂ , ⇓-pair d₁ d₂ , vpair w₁ w₂ , ⇓-pair d₁' d₂' , r-pair h₁ h₂ +fund (t-letp {A = A} {B = B} d e) h with fund d h +... | _ , ds , _ , ds' , r-pair h₁ h₂ = + let (r , dr , r' , dr' , hr) = fund e (env-ext B (env-ext A h h₁) h₂) + in r , ⇓-letp ds dr , r' , ⇓-letp ds' dr' , hr +fund (t-inj₁ d) h = + let (v , dv , w , dw , hv) = fund d h + in vinl v , ⇓-inl dv , vinl w , ⇓-inl dw , r-inl hv +fund (t-inj₂ d) h = + let (v , dv , w , dw , hv) = fund d h + in vinr v , ⇓-inr dv , vinr w , ⇓-inr dw , r-inr hv +fund (t-case {A = A} {B = B} d l r) h with fund d h +... | _ , ds , _ , ds' , r-inl hv = + let (x , dx , x' , dx' , hx) = fund l (env-ext A h hv) + in x , ⇓-casel ds dx , x' , ⇓-casel ds' dx' , hx +... | _ , ds , _ , ds' , r-inr hv = + let (x , dx , x' , dx' , hx) = fund r (env-ext B h hv) + in x , ⇓-caser ds dx , x' , ⇓-caser ds' dx' , hx +fund (t-lit ℓ) h = vlit ℓ , ⇓-lit , vlit ℓ , ⇓-lit , r-lit ℓ refl +-- A trope transition: the two states have one erased type. +fund (t-step {t = t} o d) {ρ} {ρ'} h = + subst (λ a → ℰ a ρ (keepⁱ t) ρ' (eraseⁱ t)) + (er-at (carrier o) (from o) ∙ sym (er-at (carrier o) (to o))) + (fund d h) +-- Conversion: the two types have one normal form. +fund (t-conv {t = t} d e) {ρ} {ρ'} h = + subst (λ a → ℰ a ρ (keepⁱ t) ρ' (eraseⁱ t)) (cong erN (defEq→nf e)) (fund d h) +fund (t-sub d _) h = fund d h +-- THE CAST. The reference program evaluates the evidence, and the lemma +-- for the evidence gives its value. The other program has no evidence. +fund (t-cast de dt) h = + let (ve , dke , we , dee , he) = fund de h + (v , dv , w , dw , hv) = fund dt h + in v , ⇓-letp (⇓-pair dke dv) (⇓-var zero) , w , dw + , subst (λ a → 𝒱 a v w) (evidence he) hv + +------------------------------------------------------------------------ +-- 4. Closed terms. + +-- T7: the erasure of proofs is sound. +erasure-sound : ∀ {γ : Usage 0} {Γ : Cx 0} {t A} → γ ▸ Γ ⊢ⁱ t ∶ A → + Σ[ v ∈ UVal ] Σ[ w ∈ UVal ] + (∅ᵉ ⊢ keepⁱ t ⇓ v) × (∅ᵉ ⊢ eraseⁱ t ⇓ w) × 𝒱 (erT A) v w +erasure-sound d = + let (v , dv , w , dw , h) = fund d {ρ = ∅ᵉ} {ρ' = ∅ᵉ} (λ ()) + in v , w , dv , dw , h + +erasure-sound-fo : ∀ {γ : Usage 0} {Γ : Cx 0} {t A} → γ ▸ Γ ⊢ⁱ t ∶ A → FO (erT A) → + Σ[ v ∈ UVal ] (∅ᵉ ⊢ keepⁱ t ⇓ v) × (∅ᵉ ⊢ eraseⁱ t ⇓ v) +erasure-sound-fo {t = t} d fo = + let (v , w , dv , dw , h) = erasure-sound d + in v , dv , subst (λ x → ∅ᵉ ⊢ eraseⁱ t ⇓ x) (sym (𝒱-fo fo h)) dw + +-- Closed evidence gives a conversion. +canonicity : ∀ {γ : Usage 0} {Γ : Cx 0} {e A B} → + γ ▸ Γ ⊢ⁱ e ∶ base (Id A B) → DefEq A B +canonicity d with erasure-sound d +... | _ , _ , _ , _ , r-lit ℓ p = diagonal ℓ p + +------------------------------------------------------------------------ +-- 5. The grade. + +-- Evidence costs nothing: 𝟘 · γ + δ is δ. +cast-free : GradeLaws ops → + ∀ {γ δ : Usage n} {Γ : Cx n} {e t A B} → + γ ▸ Γ ⊢ⁱ e ∶ base (Id A B) → δ ▸ Γ ⊢ⁱ t ∶ A → + δ ▸ Γ ⊢ⁱ cast e t ∶ B +cast-free laws {γ = γ} {δ = δ} {Γ = Γ} {e = e} {t = t} {B = B} de dt = + subst (λ u → u ▸ Γ ⊢ⁱ cast e t ∶ B) + (funExt (λ i → cong (_+ δ i) (zero-mul (γ i)) ∙ zero-add (δ i))) + (t-cast de dt) + where open GradeLaws laws + +-- A local equality assumption is a variable at the grade 𝟘. +assumption : GradeLaws ops → ∀ (A B : Ty [] ★) {Γ : Cx 0} → + 0ᵘ ▸ Γ ⊢ⁱ use-assumption A B ∶ arr 𝟘 (base (Id A B)) (arr 𝟙 A B) +assumption laws A B {Γ} = t-lam (t-lam body) + where + Γ' : Cx 2 + Γ' = Γ ▹ᶜ base (Id A B) ▹ᶜ A + + -- The usage of the payload: the last variable once, no other variable. + path : ∀ i → unit {n = 2} zero i ≡ (0ᵘ ▹ 𝟘 ▹ 𝟙) i + path zero = refl + path (suc zero) = refl + + body : (0ᵘ ▹ 𝟘 ▹ 𝟙) ▸ Γ' ⊢ⁱ cast (ivar (suc zero)) (ivar zero) ∶ B + body = subst (λ u → u ▸ Γ' ⊢ⁱ cast (ivar (suc zero)) (ivar zero) ∶ B) + (funExt path) + (cast-free laws (t-var (suc zero)) (t-var zero)) diff --git a/verification/proofs/agda/Wager/Identity/Term.agda b/verification/proofs/agda/Wager/Identity/Term.agda new file mode 100644 index 0000000..003fc66 --- /dev/null +++ b/verification/proofs/agda/Wager/Identity/Term.agda @@ -0,0 +1,94 @@ +{-# OPTIONS --cubical --safe #-} +-- Forced by cubical-0.9 (InfectiveImport). No coinduction is used. +{-# OPTIONS --guardedness #-} +-- SPDX-License-Identifier: MPL-2.0 +-- +-- The terms of the target with the identity family (Stage 6, part 2). +-- +-- `ITm` is the term syntax of the target (`Wager.L2.Term.Tm`) with one +-- more former: `cast e t`. The term e is equality evidence, and t is +-- the payload. `emb` shows that each target term is a term here. +-- +-- A term has two erasures into the untyped calculus: +-- +-- keepⁱ the reference. It evaluates the evidence of each cast, then +-- the payload, and gives the value of the payload. It does +-- not inspect the value of the evidence: the untyped calculus +-- has no test on a literal. +-- eraseⁱ the erasure of proofs. The evidence of each cast is absent. +-- `eraseⁱ (cast e t)` is `eraseⁱ t`. +-- +-- The two erasures are equal on a term with no cast. +open import Wager.L1.Signature +import Wager.L2.Signature +module Wager.Identity.Term (S : Sig) (TS : Wager.L2.Signature.TSig S) where + +open import Cubical.Foundations.Prelude +open import Cubical.Data.Nat.Base using (ℕ; zero; suc) +open import Cubical.Data.FinData.Base using (Fin; zero; suc) + +open import Wager.L1.Syntax S +open import Wager.L2.Term S TS +open import Wager.Erased.Untyped +open Terms Lit + +private + variable + n : ℕ + +data ITm : ℕ → Type where + ivar : Fin n → ITm n + ilam : TG → Ty [] ★ → ITm (suc n) → ITm n + iapp : ITm n → ITm n → ITm n + ipair : ITm n → ITm n → ITm n + -- The body sees the first component at index 1 and the second at index 0. + iletp : ITm n → ITm (suc (suc n)) → ITm n + iinj₁ : ITm n → ITm n + iinj₂ : ITm n → ITm n + icase : ITm n → ITm (suc n) → ITm (suc n) → ITm n + ilit : Lit → ITm n + istep : Op → ITm n → ITm n + -- THE NEW FORMER: the evidence, then the payload. + cast : ITm n → ITm n → ITm n + +-- Each target term is a term of the extension. +emb : Tm n → ITm n +emb (tvar i) = ivar i +emb (tlam q A b) = ilam q A (emb b) +emb (tapp f a) = iapp (emb f) (emb a) +emb (pair s t) = ipair (emb s) (emb t) +emb (letp s b) = iletp (emb s) (emb b) +emb (inj₁ t) = iinj₁ (emb t) +emb (inj₂ t) = iinj₂ (emb t) +emb (case s l r) = icase (emb s) (emb l) (emb r) +emb (lit ℓ) = ilit ℓ +emb (step o t) = istep o (emb t) + +-- The reference erasure: each cast evaluates its evidence. +keepⁱ : ITm n → UTm n +keepⁱ (ivar i) = uvar i +keepⁱ (ilam q A b) = ulam (keepⁱ b) +keepⁱ (iapp f a) = uapp (keepⁱ f) (keepⁱ a) +keepⁱ (ipair s t) = upair (keepⁱ s) (keepⁱ t) +keepⁱ (iletp s b) = uletp (keepⁱ s) (keepⁱ b) +keepⁱ (iinj₁ t) = uinl (keepⁱ t) +keepⁱ (iinj₂ t) = uinr (keepⁱ t) +keepⁱ (icase s l r) = ucase (keepⁱ s) (keepⁱ l) (keepⁱ r) +keepⁱ (ilit ℓ) = ulit ℓ +keepⁱ (istep o t) = keepⁱ t +-- Evaluate the evidence, then the payload. Give the payload (index 0). +keepⁱ (cast e t) = uletp (upair (keepⁱ e) (keepⁱ t)) (uvar zero) + +-- The erasure of proofs: the evidence of a cast is absent. +eraseⁱ : ITm n → UTm n +eraseⁱ (ivar i) = uvar i +eraseⁱ (ilam q A b) = ulam (eraseⁱ b) +eraseⁱ (iapp f a) = uapp (eraseⁱ f) (eraseⁱ a) +eraseⁱ (ipair s t) = upair (eraseⁱ s) (eraseⁱ t) +eraseⁱ (iletp s b) = uletp (eraseⁱ s) (eraseⁱ b) +eraseⁱ (iinj₁ t) = uinl (eraseⁱ t) +eraseⁱ (iinj₂ t) = uinr (eraseⁱ t) +eraseⁱ (icase s l r) = ucase (eraseⁱ s) (eraseⁱ l) (eraseⁱ r) +eraseⁱ (ilit ℓ) = ulit ℓ +eraseⁱ (istep o t) = eraseⁱ t +eraseⁱ (cast e t) = eraseⁱ t diff --git a/verification/proofs/agda/Wager/Identity/Typing.agda b/verification/proofs/agda/Wager/Identity/Typing.agda new file mode 100644 index 0000000..5545683 --- /dev/null +++ b/verification/proofs/agda/Wager/Identity/Typing.agda @@ -0,0 +1,86 @@ +{-# OPTIONS --cubical --safe #-} +-- Forced by cubical-0.9 (InfectiveImport). No coinduction is used. +{-# OPTIONS --guardedness #-} +-- SPDX-License-Identifier: MPL-2.0 +-- +-- Typing of the target with the identity family (Stage 6, part 2). +-- +-- The judgement `γ ▸ Γ ⊢ⁱ t ∶ A` has the 12 rules of the target +-- judgement (`Wager.L2.Typing`), with the same text, and ONE new rule: +-- `t-cast`. The judgement form is the form `Γ ⊢ᵣ t : A` of 00-notation. +-- +-- `t-cast` uses the evidence at the grade 𝟘: the usage vector of the +-- evidence is scaled by 𝟘. The rule names no grade other than 𝟘, and +-- it has no side condition for one algebra. +-- +-- There is no introduction rule: the evidence `rfl A` is a literal, +-- and `t-lit` types it. +open import Wager.L1.Signature +open import Wager.Grade.Algebra +import Wager.L2.Signature +import Wager.Identity.Family +module Wager.Identity.Typing + (S : Sig) (TS : Wager.L2.Signature.TSig S) (ops : GradeOps (Sig.TG S)) + (F : Wager.Identity.Family.IdFamily S TS) where + +open import Cubical.Foundations.Prelude +open import Cubical.Data.Nat.Base using (ℕ; zero; suc) +open import Cubical.Data.FinData.Base using (Fin; zero; suc) + +open import Wager.L1.Syntax S +open import Wager.L1.Conversion S +open import Wager.L2.Typing S TS ops using (Cx; _▹ᶜ_) public +open import Wager.L2.Term S TS using (Lit; litTy; Op; carrier; from; to; _at_) public +open import Wager.L2.Usage ops public +open import Wager.Identity.Term S TS public +open Wager.Identity.Family.IdFamily F public +open GradeOps ops + +private + variable + n : ℕ + +infix 3 _▸_⊢ⁱ_∶_ + +data _▸_⊢ⁱ_∶_ {n : ℕ} : Usage n → Cx n → ITm n → Ty [] ★ → Type where + -- The 12 rules of the target. + t-var : ∀ {Γ} i → unit i ▸ Γ ⊢ⁱ ivar i ∶ Γ i + t-lam : ∀ {γ Γ q A B b} → + (γ ▹ q) ▸ (Γ ▹ᶜ A) ⊢ⁱ b ∶ B → + γ ▸ Γ ⊢ⁱ ilam q A b ∶ arr q A B + t-app : ∀ {γ δ Γ q A B f a} → + γ ▸ Γ ⊢ⁱ f ∶ arr q A B → δ ▸ Γ ⊢ⁱ a ∶ A → + (γ +ᵘ (q ·ᵘ δ)) ▸ Γ ⊢ⁱ iapp f a ∶ B + t-pair : ∀ {γ δ Γ A B s t} → + γ ▸ Γ ⊢ⁱ s ∶ A → δ ▸ Γ ⊢ⁱ t ∶ B → + (γ +ᵘ δ) ▸ Γ ⊢ⁱ ipair s t ∶ A ⊗ B + t-letp : ∀ {γ δ Γ A B C s b} → + γ ▸ Γ ⊢ⁱ s ∶ A ⊗ B → + (δ ▹ 𝟙 ▹ 𝟙) ▸ (Γ ▹ᶜ A ▹ᶜ B) ⊢ⁱ b ∶ C → + (γ +ᵘ δ) ▸ Γ ⊢ⁱ iletp s b ∶ C + t-inj₁ : ∀ {γ Γ A B t} → γ ▸ Γ ⊢ⁱ t ∶ A → γ ▸ Γ ⊢ⁱ iinj₁ t ∶ A ⊕ B + t-inj₂ : ∀ {γ Γ A B t} → γ ▸ Γ ⊢ⁱ t ∶ B → γ ▸ Γ ⊢ⁱ iinj₂ t ∶ A ⊕ B + t-case : ∀ {γ δ Γ A B C s l r} → + γ ▸ Γ ⊢ⁱ s ∶ A ⊕ B → + (δ ▹ 𝟙) ▸ (Γ ▹ᶜ A) ⊢ⁱ l ∶ C → + (δ ▹ 𝟙) ▸ (Γ ▹ᶜ B) ⊢ⁱ r ∶ C → + (γ +ᵘ δ) ▸ Γ ⊢ⁱ icase s l r ∶ C + t-lit : ∀ {Γ} ℓ → 0ᵘ ▸ Γ ⊢ⁱ ilit ℓ ∶ base (litTy ℓ) + t-step : ∀ {γ Γ t} o → + γ ▸ Γ ⊢ⁱ t ∶ carrier o at from o → + γ ▸ Γ ⊢ⁱ istep o t ∶ carrier o at to o + t-conv : ∀ {γ Γ A B t} → γ ▸ Γ ⊢ⁱ t ∶ A → DefEq A B → γ ▸ Γ ⊢ⁱ t ∶ B + t-sub : ∀ {γ δ Γ A t} → γ ▸ Γ ⊢ⁱ t ∶ A → γ ≤ᵘ δ → δ ▸ Γ ⊢ⁱ t ∶ A + -- THE NEW RULE. Evidence that A and B are equal moves a term from A + -- to B. The evidence is used at the grade 𝟘. + t-cast : ∀ {γ δ Γ A B e t} → + γ ▸ Γ ⊢ⁱ e ∶ base (Id A B) → + δ ▸ Γ ⊢ⁱ t ∶ A → + ((𝟘 ·ᵘ γ) +ᵘ δ) ▸ Γ ⊢ⁱ cast e t ∶ B + +-- A local equality assumption is a variable. The function takes +-- evidence that A and B are equal, at the grade 𝟘, then a term of the +-- type A, and gives the term at the type B. +use-assumption : Ty [] ★ → Ty [] ★ → ITm 0 +use-assumption A B = + ilam 𝟘 (base (Id A B)) (ilam 𝟙 A (cast (ivar (suc zero)) (ivar zero))) diff --git a/verification/proofs/agda/Wager/L2/Erasure.agda b/verification/proofs/agda/Wager/L2/Erasure.agda new file mode 100644 index 0000000..9ded832 --- /dev/null +++ b/verification/proofs/agda/Wager/L2/Erasure.agda @@ -0,0 +1,141 @@ +{-# OPTIONS --cubical --safe #-} +-- Forced by cubical-0.9 (InfectiveImport). No coinduction is used. +{-# OPTIONS --guardedness #-} +-- DESIGN-CHOICES.adoc, DC-0.3: matches on kinded normal forms and on +-- typing derivations. +{-# OPTIONS -WnoUnsupportedIndexedMatch #-} +-- SPDX-License-Identifier: MPL-2.0 +-- +-- Type erasure of the target calculus (Stage 6, a lemma). +-- +-- A typed target term erases to a term of the untyped calculus, and +-- that term has a simple type: the erased type of the target type. +-- The lemma holds for each signature and each set of grade operations. +-- +-- erT the erased type of a closed target type. It is read from the +-- normal form. A trope state vanishes, and a grade vanishes. +-- eraseᵗ the erasure of a target term. A type, a grade and a trope +-- transition vanish. +-- +-- The target calculus has conversion only (`t-conv`). Two convertible +-- types have one normal form, so they have one erased type. +open import Wager.L1.Signature +open import Wager.Grade.Algebra +import Wager.L2.Signature + +module Wager.L2.Erasure + (S : Sig) (TS : Wager.L2.Signature.TSig S) (ops : GradeOps (Sig.TG S)) where + +open import Cubical.Foundations.Prelude +open import Cubical.Data.Empty as ⊥ using (⊥) +open import Cubical.Data.Nat.Base using (ℕ; zero; suc) +open import Cubical.Data.FinData.Base using (Fin; zero; suc) + +open import Wager.L1.Syntax S +open import Wager.L1.Normal S +open import Wager.L1.Eval S +open import Wager.L1.Conversion S +open import Wager.L1.Equality S +open import Wager.L2.Typing S TS ops +open import Wager.Erased.Untyped +open Terms Lit +open Typing litTy + +private + variable + n : ℕ + +------------------------------------------------------------------------ +-- Erased types. + +-- The empty context has no neutral type. +noNe : ∀ {k} → Ne [] k → ⊥ +noNe (napp m v) = noNe m +noNe (nstuck p m) = noNe m + +erN : Nf [] ★ → ETy Base +erN (ne m) = ⊥.rec (noNe m) +erN (nbase b) = ebase b +erN (ncapp c v) = erN v +erN (narr q a b) = earr (erN a) (erN b) +erN (a n⊗ b) = eprod (erN a) (erN b) +erN (a n⊕ b) = esum (erN a) (erN b) + +erT : Ty [] ★ → ETy Base +erT A = erN (nf A) + +-- The state of a trope does not change the erased type. +er-at : ∀ A m → erT (A at m) ≡ erT A +er-at A nothing = refl +er-at A (just s) = refl + +------------------------------------------------------------------------ +-- Erased terms. + +eraseᵗ : Tm n → UTm n +eraseᵗ (tvar i) = uvar i +eraseᵗ (tlam q A b) = ulam (eraseᵗ b) +eraseᵗ (tapp f a) = uapp (eraseᵗ f) (eraseᵗ a) +eraseᵗ (pair s t) = upair (eraseᵗ s) (eraseᵗ t) +eraseᵗ (letp s b) = uletp (eraseᵗ s) (eraseᵗ b) +eraseᵗ (inj₁ t) = uinl (eraseᵗ t) +eraseᵗ (inj₂ t) = uinr (eraseᵗ t) +eraseᵗ (case s l r) = ucase (eraseᵗ s) (eraseᵗ l) (eraseᵗ r) +eraseᵗ (lit ℓ) = ulit ℓ +eraseᵗ (step o t) = eraseᵗ t + +------------------------------------------------------------------------ +-- Erasure preserves typing. + +-- The erased context agrees with the target context. +Agree : ECx n → Cx n → Type +Agree Δ Γ = ∀ i → Δ i ≡ erT (Γ i) + +agree-ext : ∀ {Δ : ECx n} {Γ : Cx n} A → Agree Δ Γ → Agree (Δ ▹ᵉ erT A) (Γ ▹ᶜ A) +agree-ext A h zero = refl +agree-ext A h (suc i) = h i + +erase-typed′ : ∀ {γ} {Γ : Cx n} {t A} → γ ▸ Γ ⊢ t ∶ A → + (Δ : ECx n) → Agree Δ Γ → Δ ⊢ᵉ eraseᵗ t ∶ erT A +erase-typed′ (t-var i) Δ h = u-var i (h i) +erase-typed′ (t-lam {A = A} d) Δ h = + u-lam (erase-typed′ d (Δ ▹ᵉ erT A) (agree-ext A h)) +erase-typed′ (t-app d e) Δ h = u-app (erase-typed′ d Δ h) (erase-typed′ e Δ h) +erase-typed′ (t-pair d e) Δ h = u-pair (erase-typed′ d Δ h) (erase-typed′ e Δ h) +erase-typed′ (t-letp {A = A} {B = B} d e) Δ h = + u-letp (erase-typed′ d Δ h) + (erase-typed′ e (Δ ▹ᵉ erT A ▹ᵉ erT B) (agree-ext B (agree-ext A h))) +erase-typed′ (t-inj₁ d) Δ h = u-inl (erase-typed′ d Δ h) +erase-typed′ (t-inj₂ d) Δ h = u-inr (erase-typed′ d Δ h) +erase-typed′ (t-case {A = A} {B = B} d l r) Δ h = + u-case (erase-typed′ d Δ h) + (erase-typed′ l (Δ ▹ᵉ erT A) (agree-ext A h)) + (erase-typed′ r (Δ ▹ᵉ erT B) (agree-ext B h)) +erase-typed′ (t-lit ℓ) Δ h = u-lit ℓ refl +-- A trope transition: the two states have one erased type. +erase-typed′ (t-step {t = t} o d) Δ h = + subst (λ a → Δ ⊢ᵉ eraseᵗ t ∶ a) + (er-at (carrier o) (from o) ∙ sym (er-at (carrier o) (to o))) + (erase-typed′ d Δ h) +-- Conversion: the two types have one normal form. +erase-typed′ (t-conv {t = t} d e) Δ h = + subst (λ a → Δ ⊢ᵉ eraseᵗ t ∶ a) (cong erN (defEq→nf e)) (erase-typed′ d Δ h) +erase-typed′ (t-sub d _) Δ h = erase-typed′ d Δ h + +-- THE LEMMA. +erase-typed : ∀ {γ} {Γ : Cx n} {t A} → γ ▸ Γ ⊢ t ∶ A → + (λ i → erT (Γ i)) ⊢ᵉ eraseᵗ t ∶ erT A +erase-typed d = erase-typed′ d _ (λ i → refl) + +------------------------------------------------------------------------ +-- A corollary: the target has no hypothetical equality. +-- +-- If a target term has the type `A → B` and erases to the identity +-- function, then A and B have one erased type. +identity-one-type : ∀ {γ} {Γ : Cx n} {t q A B} → γ ▸ Γ ⊢ t ∶ arr q A B → + eraseᵗ t ≡ ulam (uvar zero) → erT A ≡ erT B +identity-one-type {A = A} {B = B} d p = + inv (subst (λ u → _ ⊢ᵉ u ∶ earr (erT A) (erT B)) p (erase-typed d)) + where + inv : ∀ {Δ : ECx n} {a b} → Δ ⊢ᵉ ulam (uvar zero) ∶ earr a b → a ≡ b + inv (u-lam (u-var zero e)) = e diff --git a/verification/proofs/agda/Wager/Local/Gadt.agda b/verification/proofs/agda/Wager/Local/Gadt.agda new file mode 100644 index 0000000..01cae68 --- /dev/null +++ b/verification/proofs/agda/Wager/Local/Gadt.agda @@ -0,0 +1,40 @@ +{-# OPTIONS --cubical --safe #-} +-- Forced by cubical-0.9 (InfectiveImport). No coinduction is used. +{-# OPTIONS --guardedness #-} +-- SPDX-License-Identifier: MPL-2.0 +-- +-- The program of Stage 6: a GADT match (DESIGN-CHOICES.adoc, DC-6.2). +-- +-- In Haskell, for a base type b: +-- +-- data G a where +-- GI :: (a ~ b) => a -> G a +-- GB :: (a ~ Either b b) => a -> G a +-- +-- eval :: G a -> b +-- eval (GI x) = x +-- eval (GB x) = case x of { Left y -> y ; Right y -> y } +-- +-- The source calculus has no type variable. The type variable `a` of +-- the Haskell text is the Agda variable α: `G b α` is the type `G a` at +-- the closed instance a := α, and `gadt-eval b α` is `eval` at that +-- instance. The text of the program is the same at each instance. +open import Cubical.Foundations.Prelude + +module Wager.Local.Gadt (B Lit : Type) (litTy : Lit → B) where + +open import Cubical.Data.FinData.Base using (zero) + +open import Wager.Local.Source B Lit litTy + +G : B → LTy → LTy +G b α = ⟨ α ~ lbase b ⟩ α +ˡ ⟨ α ~ lbase b +ˡ lbase b ⟩ α + +gadt-eval : ∀ b α → LTm ∅ᵃ ∅ˡ (G b α ⇒ˡ lbase b) +gadt-eval b α = + llam (lcase (lvar zero) + -- GI: the assumption is `α ~ b`. + (lopen (lvar zero) (lcast (l-hyp here) (lvar zero))) + -- GB: the assumption is `α ~ b + b`. + (lopen (lvar zero) + (lcase (lcast (l-hyp here) (lvar zero)) (lvar zero) (lvar zero)))) diff --git a/verification/proofs/agda/Wager/Local/Separation.agda b/verification/proofs/agda/Wager/Local/Separation.agda new file mode 100644 index 0000000..e6d1eff --- /dev/null +++ b/verification/proofs/agda/Wager/Local/Separation.agda @@ -0,0 +1,95 @@ +{-# OPTIONS --cubical --safe #-} +-- Forced by cubical-0.9 (InfectiveImport). No coinduction is used. +{-# OPTIONS --guardedness #-} +-- DESIGN-CHOICES.adoc, DC-0.3: matches on typing derivations of the +-- untyped calculus. +{-# OPTIONS -WnoUnsupportedIndexedMatch #-} +-- SPDX-License-Identifier: MPL-2.0 +-- +-- T7, the separation (Stage 6): the target cannot type the GADT +-- program `gadt-eval b α`. +-- +-- The proof has two steps. +-- +-- 1. The erasure of the program has no simple type of the form +-- `(p + p) → b`, for a base type b (`no-simple-type`). The first +-- branch uses the value at the type b. The second branch uses the +-- same value at a sum type. A simple type cannot do the two. +-- 2. A typed target term erases to a term with a simple type +-- (`Wager.L2.Erasure.erase-typed`). +-- +-- In the source calculus the two branches have two local equality +-- assumptions, so each branch has its type. +open import Wager.L1.Signature +open import Wager.Grade.Algebra +import Wager.L2.Signature + +module Wager.Local.Separation + (S : Sig) (TS : Wager.L2.Signature.TSig S) (ops : GradeOps (Sig.TG S)) where + +open import Cubical.Foundations.Prelude +open import Cubical.Data.Empty as ⊥ using (⊥) +open import Cubical.Data.Unit using (Unit; tt) +open import Cubical.Data.Nat.Base using (ℕ; zero; suc) +open import Cubical.Data.FinData.Base using (Fin; zero; suc) + +open import Wager.L1.Syntax S +open import Wager.L2.Typing S TS ops +open import Wager.L2.Erasure S TS ops +open import Wager.Erased.Untyped +open Typing litTy +open import Wager.Local.Source Base Lit litTy +open import Wager.Local.Gadt Base Lit litTy + +private + variable + n : ℕ + + -- The two sides of an erased sum type. + lft rgt : ETy Base → ETy Base + lft (esum a c) = a + lft (ebase x) = ebase x + lft (earr a c) = earr a c + lft (eprod a c) = eprod a c + rgt (esum a c) = c + rgt (ebase x) = ebase x + rgt (earr a c) = earr a c + rgt (eprod a c) = eprod a c + + IsBase : ETy Base → Type + IsBase (ebase x) = Unit + IsBase (earr a c) = ⊥ + IsBase (eprod a c) = ⊥ + IsBase (esum a c) = ⊥ + +-- The erased program, written out. Agda checks by computation that it +-- is the erasure of `gadt-eval b α`, for each b and each α. +gadt-evalᵘ : UTm 0 +gadt-evalᵘ = + ulam (ucase (uvar zero) + (uapp (ulam (uvar zero)) (uvar zero)) + (uapp (ulam (ucase (uvar zero) (uvar zero) (uvar zero))) (uvar zero))) + +erased-program : ∀ b α → eraseˡ (gadt-eval b α) ≡ gadt-evalᵘ +erased-program b α = refl + +-- Step 1. +no-simple-type : ∀ {Δ : ECx 0} {p} b → + Δ ⊢ᵉ gadt-evalᵘ ∶ earr (esum p p) (ebase b) → ⊥ +no-simple-type b + (u-lam (u-case (u-var zero e₀) + (u-app (u-lam (u-var zero f₁)) (u-var zero f₂)) + (u-app (u-lam (u-case (u-var zero e₁) _ _)) (u-var zero e₂)))) = + subst IsBase + -- the type b, read from the first branch, is a sum in the second + (sym (f₂ ∙ f₁) ∙ sym (cong lft e₀) ∙ cong rgt e₀ ∙ e₂ ∙ e₁) tt + +-- T7, THE SEPARATION. +separation : + (b : Base) (α : LTy) {γ : Usage 0} {Γ : Cx 0} {t : Tm 0} {A : Ty [] ★} → + γ ▸ Γ ⊢ t ∶ A → + erT A ≡ erˡ (G b α ⇒ˡ lbase b) → + eraseᵗ t ≡ eraseˡ (gadt-eval b α) → + ⊥ +separation b α d eA eT = + no-simple-type b (subst2 (λ u a → _ ⊢ᵉ u ∶ a) eT eA (erase-typed d)) diff --git a/verification/proofs/agda/Wager/Local/Source.agda b/verification/proofs/agda/Wager/Local/Source.agda new file mode 100644 index 0000000..15bf697 --- /dev/null +++ b/verification/proofs/agda/Wager/Local/Source.agda @@ -0,0 +1,131 @@ +{-# OPTIONS --cubical --safe #-} +-- Forced by cubical-0.9 (InfectiveImport). No coinduction is used. +{-# OPTIONS --guardedness #-} +-- DESIGN-CHOICES.adoc, DC-0.3: matches on typed terms. +{-# OPTIONS -WnoUnsupportedIndexedMatch #-} +-- SPDX-License-Identifier: MPL-2.0 +-- +-- The source calculus of Stage 6: local equality assumptions +-- (DESIGN-CHOICES.adoc, DC-6.2 and DC-6.3). +-- +-- This is a new small calculus. It is not the calculus of Stage 3: it +-- has no newtype, no role and no type-level function. +-- +-- LTy types: a base type, a function, a sum, and `⟨ τ ~ σ ⟩ ρ`. +-- `⟨ τ ~ σ ⟩ ρ` is the type of a GADT constructor field in +-- System FC: a value of the type ρ, with evidence that the +-- types τ and σ are equal. +-- Eqs a list of local equality assumptions. +-- Coˡ equality of two types under assumptions (a nominal coercion). +-- LTm typed terms. `lpack` builds a value with evidence. `lopen` +-- is the match: its body has the equality as an assumption. +-- erˡ the erased type. Evidence has no erased type. +-- eraseˡ the erased term. A cast and evidence leave no term. +-- +-- A type is closed. The calculus has no type variable (DC-6.2). +open import Cubical.Foundations.Prelude + +module Wager.Local.Source (B Lit : Type) (litTy : Lit → B) where + +open import Cubical.Data.Nat.Base using (ℕ; zero; suc) +open import Cubical.Data.FinData.Base using (Fin; zero; suc) + +open import Wager.Erased.Untyped +open Terms Lit public + +infixr 20 _⇒ˡ_ +infixr 29 _+ˡ_ +infix 31 ⟨_~_⟩_ +infixl 4 _,_~_ +infix 3 _∋_~_ + +------------------------------------------------------------------------ +-- Types and local assumptions. + +data LTy : Type where + lbase : B → LTy + _⇒ˡ_ : LTy → LTy → LTy + _+ˡ_ : LTy → LTy → LTy + ⟨_~_⟩_ : LTy → LTy → LTy → LTy + +private + variable + n : ℕ + τ σ υ ρ τ' σ' : LTy + +data Eqs : Type where + ∅ᵃ : Eqs + _,_~_ : Eqs → LTy → LTy → Eqs + +private + variable + Δ : Eqs + +-- The assumption `τ ~ σ` is in the list. +data _∋_~_ : Eqs → LTy → LTy → Type where + here : (Δ , τ ~ σ) ∋ τ ~ σ + there : Δ ∋ τ ~ σ → (Δ , τ' ~ σ') ∋ τ ~ σ + +-- Equality of two types under the assumptions Δ. +data Coˡ (Δ : Eqs) : LTy → LTy → Type where + l-hyp : Δ ∋ τ ~ σ → Coˡ Δ τ σ + l-refl : Coˡ Δ τ τ + l-sym : Coˡ Δ τ σ → Coˡ Δ σ τ + l-trans : Coˡ Δ τ σ → Coˡ Δ σ υ → Coˡ Δ τ υ + l-arr : Coˡ Δ τ τ' → Coˡ Δ σ σ' → Coˡ Δ (τ ⇒ˡ σ) (τ' ⇒ˡ σ') + l-sum : Coˡ Δ τ τ' → Coˡ Δ σ σ' → Coˡ Δ (τ +ˡ σ) (τ' +ˡ σ') + +------------------------------------------------------------------------ +-- Terms. + +-- A context: the type of each term variable. +LCx : ℕ → Type +LCx n = Fin n → LTy + +infixl 5 _▹ˡ_ +_▹ˡ_ : LCx n → LTy → LCx (suc n) +(Γ ▹ˡ τ) zero = τ +(Γ ▹ˡ τ) (suc i) = Γ i + +∅ˡ : LCx 0 +∅ˡ () + +data LTm : Eqs → LCx n → LTy → Type where + lvar : ∀ {Γ : LCx n} i → LTm Δ Γ (Γ i) + llam : ∀ {Γ : LCx n} → LTm Δ (Γ ▹ˡ τ) σ → LTm Δ Γ (τ ⇒ˡ σ) + lapp : ∀ {Γ : LCx n} → LTm Δ Γ (τ ⇒ˡ σ) → LTm Δ Γ τ → LTm Δ Γ σ + linl : ∀ {Γ : LCx n} → LTm Δ Γ τ → LTm Δ Γ (τ +ˡ σ) + linr : ∀ {Γ : LCx n} → LTm Δ Γ σ → LTm Δ Γ (τ +ˡ σ) + lcase : ∀ {Γ : LCx n} → LTm Δ Γ (τ +ˡ σ) → + LTm Δ (Γ ▹ˡ τ) υ → LTm Δ (Γ ▹ˡ σ) υ → LTm Δ Γ υ + llit : ∀ {Γ : LCx n} ℓ → LTm Δ Γ (lbase (litTy ℓ)) + -- A cast along an equality. + lcast : ∀ {Γ : LCx n} → Coˡ Δ τ σ → LTm Δ Γ τ → LTm Δ Γ σ + -- A value with evidence that τ and σ are equal. + lpack : ∀ {Γ : LCx n} → Coˡ Δ τ σ → LTm Δ Γ ρ → LTm Δ Γ (⟨ τ ~ σ ⟩ ρ) + -- The match: the body sees the value at index 0, and it has the + -- equality `τ ~ σ` as a local assumption. + lopen : ∀ {Γ : LCx n} → LTm Δ Γ (⟨ τ ~ σ ⟩ ρ) → + LTm (Δ , τ ~ σ) (Γ ▹ˡ ρ) υ → LTm Δ Γ υ + +------------------------------------------------------------------------ +-- Erasure. + +erˡ : LTy → ETy B +erˡ (lbase b) = ebase b +erˡ (τ ⇒ˡ σ) = earr (erˡ τ) (erˡ σ) +erˡ (τ +ˡ σ) = esum (erˡ τ) (erˡ σ) +erˡ (⟨ τ ~ σ ⟩ ρ) = erˡ ρ + +-- The match becomes a β-redex: the body is a function of the value. +eraseˡ : ∀ {Γ : LCx n} → LTm Δ Γ τ → UTm n +eraseˡ (lvar i) = uvar i +eraseˡ (llam e) = ulam (eraseˡ e) +eraseˡ (lapp f a) = uapp (eraseˡ f) (eraseˡ a) +eraseˡ (linl e) = uinl (eraseˡ e) +eraseˡ (linr e) = uinr (eraseˡ e) +eraseˡ (lcase s l r) = ucase (eraseˡ s) (eraseˡ l) (eraseˡ r) +eraseˡ (llit ℓ) = ulit ℓ +eraseˡ (lcast γ e) = eraseˡ e +eraseˡ (lpack γ e) = eraseˡ e +eraseˡ (lopen e b) = uapp (ulam (eraseˡ b)) (eraseˡ e) diff --git a/verification/proofs/agda/Wager/Proofs.agda b/verification/proofs/agda/Wager/Proofs.agda index 3d8bceb..689cbf9 100644 --- a/verification/proofs/agda/Wager/Proofs.agda +++ b/verification/proofs/agda/Wager/Proofs.agda @@ -72,6 +72,11 @@ import Wager.Trans.Typing import Wager.Trans.Simulation import Wager.Trans.RoleCorrespondence import Wager.Trans.TwoStateProofs +import Wager.Trans.Nominal +import Wager.Local.Separation +import Wager.Identity.Family +import Wager.Identity.Soundness +import Wager.Univalent.CrossCheck module _ where open T1-Statements @@ -245,3 +250,87 @@ module _ where no-two-state-translation : No-Two-State-Translation no-two-state-translation = TS.no-two-state + +------------------------------------------------------------------------ +-- STAGE 5 +------------------------------------------------------------------------ + +module _ (SS : SSig) (Sc : Wager.Trans.Scheme.StateScheme SS) + {R : Type} (ops : GradeOps R) where + open T6-Statements SS Sc ops + private module NM = Wager.Trans.Nominal SS Sc ops + + t6 : T6 + t6 = NM.nominal-nf + + t6-conversion : T6-Conversion + t6-conversion = NM.nominal-defeq + + -- By the definition of the translation: the transformer of a nominal + -- coercion is the identity. + t6-no-term : T6-No-Term + t6-no-term γ e = refl + +------------------------------------------------------------------------ +-- STAGE 6 +------------------------------------------------------------------------ + +module _ (S : Sig) (TS : Wager.L2.Signature.TSig S) (ops : GradeOps (Sig.TG S)) where + open T7-Statements S TS ops + private module Sep = Wager.Local.Separation S TS ops + + t7-separation : T7-Separation + t7-separation = Sep.separation + +------------------------------------------------------------------------ +-- STAGE 6, PART 2 +------------------------------------------------------------------------ + +module _ (S : Sig) (TS : Wager.L2.Signature.TSig S) (ops : GradeOps (Sig.TG S)) + (F : Wager.Identity.Family.IdFamily S TS) where + open T7-Identity-Statements S TS ops F + private module Snd = Wager.Identity.Soundness S TS ops F + + t7-conservative : T7-Conservative + t7-conservative = Snd.emb-typed + + t7-conservative-erasure : T7-Conservative-Erasure + t7-conservative-erasure t = Snd.emb-keep t , Snd.emb-erase t + + t7-intro : T7-Intro + t7-intro = Snd.intro + + t7-canonicity : T7-Canonicity + t7-canonicity = Snd.canonicity + + t7-erasure : T7-Erasure + t7-erasure = Snd.erasure-sound + + t7-erasure-first-order : T7-Erasure-First-Order + t7-erasure-first-order = Snd.erasure-sound-fo + + t7-grade : T7-Grade + t7-grade laws = Snd.cast-free laws + + t7-assumption : T7-Assumption + t7-assumption = Snd.assumption + +------------------------------------------------------------------------ +-- STAGE 7 +------------------------------------------------------------------------ + +module _ (SS : SSig) (Sc : Wager.Trans.Scheme.StateScheme SS) + {R : Type} (A : GradeAlgebra R) + (El : SSig.Base SS → Type) + (elLit : (ℓ : SSig.Lit SS) → El (SSig.litTy SS ℓ)) where + open Stage7-Statements SS Sc A El elLit + private module CC = Wager.Univalent.CrossCheck SS Sc A El elLit + + coercion-denotes-transport : Coercion-Denotes-Transport + coercion-denotes-transport = CC.coercion-denotes-transport + + coercion-denotes-transport-back : Coercion-Denotes-Transport-Back + coercion-denotes-transport-back = CC.coercion-denotes-transport-back + + coerce-function-is-transport : Coerce-Function-Is-Transport + coerce-function-is-transport = CC.coerce-function-is-transport diff --git a/verification/proofs/agda/Wager/RELATION-LEDGER.adoc b/verification/proofs/agda/Wager/RELATION-LEDGER.adoc index 28fcb46..c649c8f 100644 --- a/verification/proofs/agda/Wager/RELATION-LEDGER.adoc +++ b/verification/proofs/agda/Wager/RELATION-LEDGER.adoc @@ -1,7 +1,7 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) = Wager: relation ledger -Status: Stage 4. Each later stage adds its entries in the same commit as its rules. +Status: Stage 7 (the last stage). Each stage added its entries in the same commit as its rules. :toc: left :sectnums: @@ -21,7 +21,8 @@ Each entry has one class: | source | The relation belongs to the source calculus (the fragment of System FC). The target calculus does not have it. It does not count against the wager. |=== -An ADDED entry counts against the wager. *Stages 1, 2, 3 and 4 have no ADDED entry.* +An ADDED entry counts against the wager. *Stages 1 to 5 and Stage 6, part 1 have no ADDED entry.* +Stage 6, part 2 has 2 entries with no class (R23, R24). The task says that the owner decides how they count. The ledger has one "baseline, changed" entry (R1). The owner decides how it counts. == Judgement forms of the target calculus @@ -177,8 +178,76 @@ The translated terms use the rules of Stage 1 only: the rule `t-step` types each `StateScheme` (`Wager.Trans.Scheme`) is data of the translation: an index type and a table. It is not a relation. +== Stage 5 + +Stage 5 adds no relation. T6 is stated with conversion (R2) and with the function `nf` (R3), which are baseline entries. + +== Relations of the source calculus of Stage 6 + +Stage 6, part 1 (the separation) adds no relation and no rule to the target calculus. It adds a second source calculus (DC-6.3). + +[cols="1,3,2,5",options="header"] +|=== +| Id | Agda identifier | Class | Notes + +| R21 +| `Coˡ` and `_∋_~_` in `Wager.Local.Source` +| source +| Equality of two types under local equality assumptions (a nominal coercion of System FC with hypotheses), and the membership of an assumption in a list. + This is a hypothetical equality. The target calculus does not have it: the conversion `DefEq` (R2) has no assumption. + +| R22 +| `LTm` in `Wager.Local.Source` +| source +| Typing of the terms of the source calculus of Stage 6 (by construction). The match `lopen` adds a local assumption. +|=== + +`erT` and `eraseᵗ` (`Wager.L2.Erasure`), and `erˡ` and `eraseˡ` (`Wager.Local.Source`), are functions. They are not relations. +The proof of T7, part 1 uses the typing of untyped terms (R16). + +== The extension of Stage 6, part 2 (the identity type) + +*The 2 entries of this section have no class. The class is the decision of the owner.* The task says: "Do not decide whether option 1 adds a relation." The entries give the facts. `VERDICT.adoc` gives the trade. + +EQUALITY EVIDENCE IS NOW A TERM (DC-6.5). + +[cols="1,3,2,5",options="header"] +|=== +| Id | Agda identifier | Class | Notes + +| R23 +| `_▸_⊢ⁱ_∶_` in `Wager.Identity.Typing` +| OWNER DECIDES +| The typing judgement of the target with the identity family. It has the form of R4 (`Γ ⊢ᵣ t : A` of 00-notation). It is a new Agda data type (DC-6.6), with the 12 rules of R4 and one more rule, `t-cast`. + `γ ▸ Γ ⊢ⁱ e ∶ base (Id A B)` reads: in the context Γ, the term e is evidence that the closed types A and B are equal. A variable of the type `base (Id A B)` in Γ is a local equality assumption. + The judgement thus does the work of a hypothetical equality. It has no new judgement form. + +| R24 +| `IdFamily` in `Wager.Identity.Family` +| OWNER DECIDES +| Not a relation in Agda. It is a record of signature entries: the base constants `Id A B`, the literals `rfl A`, and 3 laws. + It is in this ledger because the family is conversion in the form of a type: for a closed term, the type `base (Id A B)` has a term exactly when `DefEq A B` holds (`T7-Intro`, `T7-Canonicity`). +|=== + +`keepⁱ` and `eraseⁱ` (`Wager.Identity.Term`) are functions. They are not relations. +The statements of T7, part 2 use the evaluation of untyped terms (R16) and observational equality (R18). +== Stage 7 (the optional cross-check) + +[cols="1,3,2,5",options="header"] +|=== +| Id | Agda identifier | Class | Notes + +| R25 +| `𝓡`, `Real` and `Denotes` in `Wager.Univalent.Model` (with `RLit`, `RFun`, `RPair`, `RSum`) +| specification only +| Realisability: an untyped value realises an element of the interpretation of a closed target type in the cubical universe. `Denotes` says that a term transformer denotes a function of the model. + No typing rule and no kinding rule uses these relations. They are in the statements of Stage 7 only. +|=== + +`⟦_⟧`, `pathOf` and `unboxEquiv` (`Wager.Univalent.Model`) are a function, a path and an equivalence. They are not relations. == What is absent * The target calculus has no coercion relation and no cast judgement. The coercion relation `Co` (R14) is in the source calculus only. The translation of Stage 4 makes each representational coercion a term of the target, with no new judgement. * Representational equivalence exists as "specification only" (R11). It is not a judgement of the calculus. * There is no subtyping relation between types. +* The extension of Stage 6, part 2 has no equality judgement with assumptions and no cast judgement. It has a term former (`cast`) and a rule of the typing judgement (R23). diff --git a/verification/proofs/agda/Wager/RULE-DIFF-LEDGER.adoc b/verification/proofs/agda/Wager/RULE-DIFF-LEDGER.adoc index 1c6e8f1..6a6066b 100644 --- a/verification/proofs/agda/Wager/RULE-DIFF-LEDGER.adoc +++ b/verification/proofs/agda/Wager/RULE-DIFF-LEDGER.adoc @@ -1,7 +1,7 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) = Wager: rule-diff ledger -Status: Stage 4. *The ledger is empty.* +Status: Stage 5. *The ledger is empty.* :toc: left :sectnums: @@ -81,3 +81,58 @@ The translation names the grade `𝟙` only: a function type becomes `arr 𝟙`, Theorem T5 (typing of a translated program) has two hypotheses on the grade algebra: `𝟘 ≤ 𝟙` and `𝟙 + 𝟙 ≤ 𝟙`. They name the grades `𝟘` and `𝟙` only. They are hypotheses of a theorem and not side conditions of a rule, so they are not entries of this ledger. `VERDICT.adoc` records them at T5. + +== Stage 5 + +Stage 5 adds no typing rule and no kinding rule to the target calculus. T6 is a statement about the translation of types and about conversion. + +== Stage 6 + +Stage 6, part 1 (the separation) adds no typing rule and no kinding rule to the target calculus. The separation is a statement about the rules of Stage 1. + +The rule of the match (`lopen`) in the source calculus of Stage 6 has a local equality assumption. It is a rule of a source calculus, so it is not an entry of this ledger. + +Stage 6, part 2 (the identity type) is an extension of the target calculus, in separate modules (`Wager/Identity`). No rule of the target calculus changes. The owner decides if the extension is a part of the target (`VERDICT.adoc`, the trade). + +The difference between the target and the extension: + +[cols="3,1,5",options="header"] +|=== +| Item | Count | Text + +| New judgement forms +| 0 +| The judgement `_▸_⊢ⁱ_∶_` has the form of the target judgement. + +| New typing rules +| 1 +| `t-cast` (`Wager.Identity.Typing`): from `γ ▸ Γ ⊢ⁱ e ∶ base (Id A B)` and `δ ▸ Γ ⊢ⁱ t ∶ A` to `((𝟘 ·ᵘ γ) +ᵘ δ) ▸ Γ ⊢ⁱ cast e t ∶ B`. + The rule names the grade `𝟘` and no other grade. It has no side condition for one algebra. + +| New kinding rules +| 0 +| + +| New conversion rules +| 0 +| `DefEq` does not change. + +| New type formers +| 0 +| `Id A B` is a base constant of the signature. + +| New term formers +| 1 +| `cast e t`. + +| New entries of a signature +| 2 families +| The base constants `Id A B` and the literals `rfl A`, with 3 laws (`Id-conv`, `rfl-ty`, `diagonal`). The existing rule `t-lit` is the introduction rule. +|=== + +`T7-Grade` and `T7-Assumption` have the hypothesis `GradeLaws`. Their proofs use the laws `zero-mul`, `add-comm` and `add-zero`. It is a hypothesis of a theorem and not a side condition of a rule, so it is not an entry of this ledger. +The other statements of part 2 hold for each set of grade operations. + +== Stage 7 + +Stage 7 adds no typing rule and no kinding rule to the target calculus. The cross-check is a statement about a model of the target of Stage 4. diff --git a/verification/proofs/agda/Wager/Statements.agda b/verification/proofs/agda/Wager/Statements.agda index f63201b..a5ede86 100644 --- a/verification/proofs/agda/Wager/Statements.agda +++ b/verification/proofs/agda/Wager/Statements.agda @@ -51,6 +51,13 @@ import Wager.Trans.Scheme import Wager.Trans.Target import Wager.Trans.Coercion import Wager.Trans.TwoState +open import Cubical.Data.Empty using (⊥) +import Wager.L2.Erasure +import Wager.Local.Source +import Wager.Local.Gadt +import Wager.Identity.Family +import Wager.Identity.Typing +import Wager.Univalent.Model ------------------------------------------------------------------------ -- STAGE 1 @@ -566,3 +573,269 @@ module Two-State-Statements where No-Two-State-Translation = (S : Sig) (t : Translation S) → ¬ TwoState S t where open Wager.Trans.TwoState (Wager.FC.Tagged.taggedS rep) + +------------------------------------------------------------------------ +-- STAGE 5: nominal coercions from type-level functions (theorem T6) +------------------------------------------------------------------------ + +-- A nominal coercion of the source is built from reflexivity, symmetry, +-- transitivity, congruence and the equations of the type-level +-- functions. `T` is the translation of types of Stage 4. +module T6-Statements + (SS : SSig) (Sc : Wager.Trans.Scheme.StateScheme SS) + {R : Type} (ops : GradeOps R) where + open Wager.FC.Types SS + open Wager.FC.Coercion SS + open Wager.FC.Term SS + open Wager.Trans.Target SS Sc ops using (tSig; T) + open Wager.Trans.Coercion SS Sc ops using (tr) + open Wager.L1.Conversion tSig using (DefEq) + open Wager.L1.Eval tSig using (nf) + + -- English (T6): for each nominal coercion of the source, the two + -- translated types have one normal form. + T6 : Type + T6 = ∀ {τ σ} → Co nom τ σ → nf (T τ) ≡ nf (T σ) + + -- English: the coercion becomes conversion of the target. + T6-Conversion : Type + T6-Conversion = ∀ {τ σ} → Co nom τ σ → DefEq (T τ) (T σ) + + -- English: no term remains. The translation of a cast along a nominal + -- coercion is the translation of the term under the cast. + T6-No-Term : Type + T6-No-Term = + ∀ {n} {Γ : SCx n} {τ σ} (γ : Co nom τ σ) (e : STm Γ τ) → + tr (cast (c-sub γ) e) ≡ tr e + +------------------------------------------------------------------------ +-- STAGE 6: local equality assumptions (theorem T7) +------------------------------------------------------------------------ + +-- The owner asked for the two options of the stage, the separation +-- first (DESIGN-CHOICES.adoc, DC-6.1). This part is the separation. +-- +-- The source calculus of the stage is `Wager.Local.Source`. It has the +-- type `⟨ τ ~ σ ⟩ ρ` of a GADT constructor field: a value of the type +-- ρ with evidence that the types τ and σ are equal. The match `lopen` +-- brings the equality into scope as a local assumption. +-- +-- The program is `Wager.Local.Gadt.gadt-eval`. In Haskell, for a base +-- type b: +-- +-- data G a where +-- GI :: (a ~ b) => a -> G a +-- GB :: (a ~ Either b b) => a -> G a +-- +-- eval :: G a -> b +-- eval (GI x) = x +-- eval (GB x) = case x of { Left y -> y ; Right y -> y } +-- +-- `gadt-eval b α` is `eval` at the closed instance a := α. It is a term +-- of the source calculus, so it is well typed there. +-- +-- erT the erased type of a closed target type +-- eraseᵗ the erasure of a target term +-- erˡ the erased type of a source type +-- eraseˡ the erasure of a source term +module T7-Statements + (S : Sig) (TS : Wager.L2.Signature.TSig S) (ops : GradeOps (Sig.TG S)) where + open Sig S using (Base) + open Wager.L1.Syntax S using (Ty; []; ★) + open Wager.L2.Typing S TS ops using (_▸_⊢_∶_; Tm; Usage; Cx; Lit; litTy) + open Wager.L2.Erasure S TS ops using (erT; eraseᵗ) + open Wager.Local.Source Base Lit litTy using (LTy; lbase; _⇒ˡ_; erˡ; eraseˡ) + open Wager.Local.Gadt Base Lit litTy using (G; gadt-eval) + + -- English (T7, the separation): the target cannot type this program. + -- For each base type b and each closed type α, no typed target term + -- has these two properties together: + -- its type has the erased type of the source type `G b α → b`; + -- its erasure is the erasure of the source program. + -- This holds for each target signature and each set of grade + -- operations. + -- + -- The statement does not exclude a translation that changes the + -- erased type or the erased term of the program. + T7-Separation : Type + T7-Separation = + (b : Base) (α : LTy) {γ : Usage 0} {Γ : Cx 0} {t : Tm 0} {A : Ty [] ★} → + γ ▸ Γ ⊢ t ∶ A → + erT A ≡ erˡ (G b α ⇒ˡ lbase b) → + eraseᵗ t ≡ eraseˡ (gadt-eval b α) → + ⊥ + +------------------------------------------------------------------------ +-- STAGE 6, PART 2: the identity type at the grade 𝟘 (theorem T7) +------------------------------------------------------------------------ + +-- This part is the other option of the stage (DESIGN-CHOICES.adoc, +-- DC-6.1 and DC-6.5): the target gets an identity type. +-- +-- EQUALITY EVIDENCE IS NOW A TERM. A term of the type `base (Id A B)` +-- is evidence that the closed types A and B are equal. +-- +-- Id A B a base constant of the signature (`IdFamily`) +-- rfl A a literal of the base type `Id A A` +-- cast e t the one new term former: the evidence e, the payload t +-- _▸_⊢ⁱ_∶_ the target judgement with one new rule, `t-cast`, which +-- uses the evidence at the grade 𝟘 +-- keepⁱ the reference erasure: each cast evaluates its +-- evidence, then its payload +-- eraseⁱ the erasure of proofs: the evidence of each cast is +-- absent +-- 𝒱 a observational equality of untyped values at the +-- erased type a (Wager.Erased.LogRel) +-- +-- The statements hold for each signature that has an identity family, +-- and for each set of grade operations. Two statements need the laws +-- of a grade algebra, and they say so. +module T7-Identity-Statements + (S : Sig) (TS : Wager.L2.Signature.TSig S) (ops : GradeOps (Sig.TG S)) + (F : Wager.Identity.Family.IdFamily S TS) where + open Wager.L1.Syntax S using (Ty; []; ★; base; arr) + open Wager.L1.Conversion S using (DefEq) + open Wager.L2.Typing S TS ops using (_▸_⊢_∶_; Tm) + open Wager.L2.Erasure S TS ops using (erT; eraseᵗ) + open Wager.Identity.Typing S TS ops F + open GradeOps ops using (𝟘; 𝟙) + open Wager.Erased.Untyped.Terms Lit using (UVal; ∅ᵉ; _⊢_⇓_) + open Wager.Erased.LogRel litTy using (𝒱; FO) + + -- English (the target is a part): each typed term of the target is a + -- typed term of the extension, with the same usage and the same type. + T7-Conservative : Type + T7-Conservative = + ∀ {n} {γ : Usage n} {Γ : Cx n} {t : Tm n} {A : Ty [] ★} → + γ ▸ Γ ⊢ t ∶ A → γ ▸ Γ ⊢ⁱ emb t ∶ A + + -- English: on a term of the target, the two erasures of the + -- extension are the erasure of the target. + T7-Conservative-Erasure : Type + T7-Conservative-Erasure = + ∀ {n} (t : Tm n) → (keepⁱ (emb t) ≡ eraseᵗ t) × (eraseⁱ (emb t) ≡ eraseᵗ t) + + -- English (introduction): a conversion gives evidence. If A and B + -- are convertible, the literal `rfl A` has the type `Id A B`, in each + -- context, and it uses no variable. + T7-Intro : Type + T7-Intro = + ∀ {n} {Γ : Cx n} {A B : Ty [] ★} → DefEq A B → + 0ᵘ ▸ Γ ⊢ⁱ ilit (rfl A) ∶ base (Id A B) + + -- English (canonicity): closed evidence gives a conversion. If a + -- closed term has the type `Id A B`, then A and B are convertible. + -- The identity family thus adds no equality between closed types. + T7-Canonicity : Type + T7-Canonicity = + ∀ {γ : Usage 0} {Γ : Cx 0} {e : ITm 0} {A B : Ty [] ★} → + γ ▸ Γ ⊢ⁱ e ∶ base (Id A B) → DefEq A B + + -- English (T7, the erasure of proofs is sound): for a closed typed + -- term, the reference program and the program with no evidence in its + -- casts evaluate, and the two values are observationally equal at the + -- erased type. + -- + -- Totality is a part of the statement: the reference program, which + -- evaluates the evidence of each cast, has a value. + T7-Erasure : Type + T7-Erasure = + ∀ {γ : Usage 0} {Γ : Cx 0} {t : ITm 0} {A : Ty [] ★} → + γ ▸ Γ ⊢ⁱ t ∶ A → + Σ[ v ∈ UVal ] Σ[ w ∈ UVal ] + (∅ᵉ ⊢ keepⁱ t ⇓ v) × (∅ᵉ ⊢ eraseⁱ t ⇓ w) × 𝒱 (erT A) v w + + -- English (T7 at a first-order type): the two programs evaluate to + -- one value. + T7-Erasure-First-Order : Type + T7-Erasure-First-Order = + ∀ {γ : Usage 0} {Γ : Cx 0} {t : ITm 0} {A : Ty [] ★} → + γ ▸ Γ ⊢ⁱ t ∶ A → FO (erT A) → + Σ[ v ∈ UVal ] (∅ᵉ ⊢ keepⁱ t ⇓ v) × (∅ᵉ ⊢ eraseⁱ t ⇓ v) + + -- English (the grade): in a grade algebra, evidence costs nothing. + -- The usage vector of `cast e t` is the usage vector of the payload t, + -- which is the term that remains after the erasure of proofs. + T7-Grade : Type + T7-Grade = + GradeLaws ops → + ∀ {n} {γ δ : Usage n} {Γ : Cx n} {e t : ITm n} {A B : Ty [] ★} → + γ ▸ Γ ⊢ⁱ e ∶ base (Id A B) → δ ▸ Γ ⊢ⁱ t ∶ A → + δ ▸ Γ ⊢ⁱ cast e t ∶ B + + -- English (a local equality assumption): in a grade algebra, for each + -- pair of closed types A and B, this closed function is typed: + -- + -- λ (e : Id A B) at the grade 𝟘. λ (x : A) at the grade 𝟙. cast e x + -- + -- It has the type `Id A B → A → B`. The types A and B are any types. + -- The first parameter is the local assumption that A and B are equal. + T7-Assumption : Type + T7-Assumption = + GradeLaws ops → ∀ (A B : Ty [] ★) {Γ : Cx 0} → + 0ᵘ ▸ Γ ⊢ⁱ use-assumption A B ∶ arr 𝟘 (base (Id A B)) (arr 𝟙 A B) + +------------------------------------------------------------------------ +-- STAGE 7: the optional univalent cross-check +------------------------------------------------------------------------ + +-- The task: "Interpret target types in the cubical universe and newtype +-- transitions as equivalences. Show that the denotation of a translated +-- coercion equals transport along the path from `ua`." +-- +-- The model is `Wager.Univalent.Model` (DESIGN-CHOICES.adoc, DC-7.1 to +-- DC-7.3). It is for the target of Stage 4, for each source signature, +-- each state scheme and each grade algebra, and for each interpretation +-- `El` of the base constants with an element `elLit ℓ` for each literal. +-- +-- ⟦ X ⟧ the interpretation of a closed target type: a type of +-- the cubical universe. A newtype instance is a wrapper +-- `Box`, and `unboxEquiv : Box Z ≃ Z` is its transition. +-- Real X ρ u x the untyped term u, in the environment ρ, evaluates +-- to a value that realises the element x of ⟦ X ⟧ +-- Denotes X Y f g +-- the term transformer f denotes the function g: on a +-- term that evaluates to a realiser of x, the term +-- `f t` evaluates to a realiser of `g x` +-- pathOf wr γ the path ⟦ T τ ⟧ ≡ ⟦ T σ ⟧ of a representational +-- coercion γ. It is made from `ua unboxEquiv` (a newtype +-- axiom), `sym`, composition, and congruence of the +-- type formers. It needs the source role check `wr`. +module Stage7-Statements + (SS : SSig) (Sc : Wager.Trans.Scheme.StateScheme SS) + {R : Type} (A : GradeAlgebra R) + (El : SSig.Base SS → Type) + (elLit : (ℓ : SSig.Lit SS) → El (SSig.litTy SS ℓ)) where + private + ops = GradeAlgebra.ops A + open GradeOps ops using (𝟙) + open Wager.FC.Types SS + open Wager.FC.Coercion SS + open Wager.Trans.Target SS Sc ops using (T; arr) + open Wager.Trans.Coercion SS Sc ops using (coI; fwd; bwd; coerceT; eraseT) + open Wager.Univalent.Model SS Sc A El elLit + open Wager.Erased.Untyped.Terms Lit using (UEnv) + + -- English (the cross-check): the translation of a representational + -- coercion denotes transport along its path. On a term that evaluates + -- to a realiser of x, the transformed term evaluates to a realiser of + -- `transport (pathOf wr γ) x`. + Coercion-Denotes-Transport : Type + Coercion-Denotes-Transport = + (wr : WellRoled) → ∀ {τ σ} (γ : Co rep τ σ) → + Denotes (T τ) (T σ) (fwd (coI rep γ)) (transport (pathOf wr γ)) + + -- English: the transformer in the other direction denotes transport + -- along the inverse path. + Coercion-Denotes-Transport-Back : Type + Coercion-Denotes-Transport-Back = + (wr : WellRoled) → ∀ {τ σ} (γ : Co rep τ σ) → + Denotes (T σ) (T τ) (bwd (coI rep γ)) (transport (sym (pathOf wr γ))) + + -- English: the erased coercion function evaluates, in each + -- environment, to a closure that realises the function + -- `transport (pathOf wr γ)`. + Coerce-Function-Is-Transport : Type + Coerce-Function-Is-Transport = + (wr : WellRoled) → ∀ {τ σ} (γ : Co rep τ σ) {n} {ρ : UEnv n} → + Real (arr 𝟙 (T τ) (T σ)) ρ (eraseT (coerceT γ)) (transport (pathOf wr γ)) diff --git a/verification/proofs/agda/Wager/TOOLCHAIN.adoc b/verification/proofs/agda/Wager/TOOLCHAIN.adoc index 628e34d..222b95b 100644 --- a/verification/proofs/agda/Wager/TOOLCHAIN.adoc +++ b/verification/proofs/agda/Wager/TOOLCHAIN.adoc @@ -292,3 +292,135 @@ A clean build of `Wager/Everything.agda` (64 modules) takes about 35 seconds and |=== The third test shows that the proofs of T3 and T5 depend on the terms that the translation gives. + +=== Gate watch at the end of Stage 5 + +A clean build of `Wager/Everything.agda` (65 modules) takes about 35 seconds and prints no warning. + +[cols="3,3,1",options="header"] +|=== +| Change | Error from Agda | Gate + +| `Wager/Examples/Stage5.agda`: a false lemma (the translations of `Age` and `Int` have one normal form), with the proof `refl` +| `[UnequalTerms]`: the normal form of the first type starts with `ncapp` +| FAIL + +| `Wager/Examples/Stage5.agda`: `postulate t6-by-fiat : …` +| `[SafeFlagPostulate] Cannot postulate t6-by-fiat with safe flag`. `scan-dangerous.sh` also fails. +| FAIL + +| `Wager/Trans/Target.agda`: a target primitive ignores the index of a state +| `[UnequalTerms] obs F N (idx N v) != fOther F` in `Wager/Trans/Nominal.agda` +| FAIL + +| All changes removed +| None +| PASS, 65 files +|=== + +The third test shows that the proof of T6 depends on the table of the target primitives. + +=== Gate watch at the end of Stage 6, part 1 (the separation) + +A clean build of `Wager/Everything.agda` (70 modules) takes about 39 seconds and prints no warning. + +[cols="3,3,1",options="header"] +|=== +| Change | Error from Agda | Gate + +| `Wager/Examples/Stage6.agda`: a false lemma (the erased program has the simple type `(Int + Int) → Int`), with the derivation of `other-erased-type` +| `[UnequalTerms] (ebase bInt) != (esum (ebase bInt) (ebase bInt))` +| FAIL + +| `Wager/Examples/Stage6.agda`: `postulate t7-by-fiat : ⊥` +| `[SafeFlagPostulate]`. `scan-dangerous.sh` also fails. +| FAIL + +| `Wager/Local/Gadt.agda`: the second constructor has the assumption `α ~ b`, and the second branch gives the value back +| `[UnequalTerms] UTm.uvar zero != UTm.ucase (uvar zero) (uvar zero) (uvar zero)` in `Wager/Local/Separation.agda` +| FAIL + +| All changes removed +| None +| PASS, 70 files +|=== + +The third test shows that the proof of the separation depends on the text of the program. + +=== Gate watch at the end of Stage 6, part 2 (the identity type) + +A clean build of `Wager/Everything.agda` (76 modules) takes about 43 seconds and prints no warning. + +[cols="3,3,1",options="header"] +|=== +| Change | Error from Agda | Gate + +| `Wager/Examples/Stage6Identity.agda`: a false lemma (no closed term is evidence that `Int` is `Int`) +| `[UnequalTerms]` in `no-evidence` +| FAIL + +| `Wager/Identity/Term.agda`: `eraseⁱ (cast e t)` is the erasure of the evidence +| `[UnequalTerms]` in the case of the cast of `Wager.Identity.Soundness.fund` +| FAIL + +| `Wager/Identity/Typing.agda`: the rule `t-cast` takes evidence of the type `Id A A` +| `[UnequalTerms]` in the case of the cast of `fund` +| FAIL + +| `Wager/Identity/Typing.agda`: the rule `t-cast` uses the evidence at the grade `𝟙` +| `[MismatchedProjectionsError]` in `cast-free` +| FAIL + +| `Wager/Identity/Instance.agda`: the literal of the code `c` has the base type `cid c (cq c)`, off the diagonal +| `[UnequalTerms]` in `diag` +| FAIL + +| `Wager/Identity/Soundness.agda`: `postulate evidence-bad : erT A ≡ erT B` +| `[SafeFlagPostulate]`. `scan-dangerous.sh` also fails. +| FAIL + +| All changes removed +| None +| PASS, 76 files +|=== + +The second and the third test show that the proof of `T7-Erasure` depends on the erasure and on the rule. + +The fourth test has a second part. With the grade `𝟙` in the rule, sections 1 to 4 of `Wager.Identity.Soundness` were checked alone: they pass. These are the embedding of the target, `intro`, `fund`, `erasure-sound`, `erasure-sound-fo` and `canonicity`. Section 5 (`cast-free`, `assumption`) does not pass. +The behaviour statements of part 2 thus do not depend on the grade of the rule, and the grade statements do (DC-6.7). + +=== Gate watch at the end of Stage 7 (the optional cross-check) + +A clean build of `Wager/Everything.agda` (79 modules) takes about 48 seconds and prints no warning. + +[cols="3,3,1",options="header"] +|=== +| Change | Error from Agda | Gate + +| `Wager/Examples/Stage7.agda`: a false lemma (transport along the path of `Age ~ Int` gives 8 from `box 7`) +| `[UnequalTerms]` in `age-transport` +| FAIL + +| `Wager/Univalent/Model.agda`: a wrapper has no realiser +| `[UnequalTerms]` in `Wager.Univalent.CrossCheck.step-den` +| FAIL + +| `Wager/Univalent/Model.agda`: the path of a pair coercion uses the path of its first part two times +| `[UnequalTerms]` in `pathAt` +| FAIL + +| `Wager/Examples/Stage7.agda`: the model gives the number 8 to the literal `ℓint` +| `[UnequalTerms]` in `age-literal` +| FAIL + +| `Wager/Univalent/CrossCheck.agda`: `postulate cross-check-bad : ⊥` +| `[SafeFlagPostulate]`. `scan-dangerous.sh` also fails. +| FAIL + +| All changes removed +| None +| PASS, 79 files +|=== + +The second test shows that the proof depends on the rule "a wrapper is not seen at run time". +The third test fails in the model, before the proof: a wrong path does not have the type of a path between the two interpretations. diff --git a/verification/proofs/agda/Wager/Univalent/CrossCheck.agda b/verification/proofs/agda/Wager/Univalent/CrossCheck.agda new file mode 100644 index 0000000..3c2e944 --- /dev/null +++ b/verification/proofs/agda/Wager/Univalent/CrossCheck.agda @@ -0,0 +1,298 @@ +{-# OPTIONS --cubical --safe #-} +-- Forced by cubical-0.9 (InfectiveImport). No coinduction is used. +{-# OPTIONS --guardedness #-} +-- DESIGN-CHOICES.adoc, DC-0.3: matches on coercions and on realisers. +{-# OPTIONS -WnoUnsupportedIndexedMatch #-} +-- SPDX-License-Identifier: MPL-2.0 +-- +-- Stage 7 (the optional univalent cross-check): the proof. +-- +-- The translation of a representational coercion denotes transport +-- along its path (`Wager.Univalent.Model.pathOf`). +-- +-- The proof has the shape of the typing proof of Stage 4 +-- (`Wager.Trans.Typing.coI-typed`): one lemma for each building block +-- of a transformer, then a recursion on the coercion. +-- +-- a trope transition the realiser does not change. The element +-- changes by `unbox` or `box`, and this is +-- transport along `ua unboxEquiv` (`uaβ`, `~uaβ`). +-- a function, a pair, transport along the congruence of the type +-- a sum former computes to the map of the parts. +-- composition `transportComposite`. +-- a nominal coercion the two types have one normal form. +open import Cubical.Foundations.Prelude +open import Wager.FC.Signature +open import Wager.Grade.Algebra +import Wager.Trans.Scheme +module Wager.Univalent.CrossCheck + (SS : SSig) (Sc : Wager.Trans.Scheme.StateScheme SS) + {R : Type} (A : GradeAlgebra R) + (El : SSig.Base SS → Type) + (elLit : (ℓ : SSig.Lit SS) → El (SSig.litTy SS ℓ)) where + +open import Cubical.Foundations.Transport using (transportComposite) +open import Cubical.Foundations.GroupoidLaws using (symDistr) +open import Cubical.Foundations.Univalence using (ua; uaβ; ~uaβ) +open import Cubical.Data.Bool.Base using (true; false) +open import Cubical.Data.Empty as ⊥ using (⊥) +open import Cubical.Data.Unit using (Unit; tt) +open import Cubical.Data.Nat.Base using (ℕ; zero; suc) +open import Cubical.Data.FinData.Base using (Fin; zero; suc) +open import Cubical.Data.Sigma using (_×_; _,_; fst; snd; Σ-syntax) +open import Cubical.Data.Sum.Base using (_⊎_; inl; inr) + +open import Wager.Grade.Finite using (false≢true) +open import Wager.Role.Role +open import Wager.FC.Types SS +open import Wager.FC.Coercion SS +open import Wager.Trans.Target SS Sc (GradeAlgebra.ops A) +open import Wager.Trans.Nominal SS Sc (GradeAlgebra.ops A) using (nominal-defeq; T-inst; T-embE) +open import Wager.Trans.Coercion SS Sc (GradeAlgebra.ops A) +open import Wager.Trans.Typing SS Sc A using (body-defeq) +open import Wager.L1.Normal tSig +open import Wager.L1.Eval tSig using (nf) +open import Wager.L1.Conversion tSig +open import Wager.L1.Equality tSig using (defEq→nf) +open import Wager.Erased.Untyped +open Terms Lit +open import Wager.Univalent.Model SS Sc A El elLit +open GradeOps (GradeAlgebra.ops A) using (𝟙) + +private + variable + X Y Z X' Y' : Ty [] ★ + τ σ : STy + +-- A pair of transformers denotes transport along a path and along its +-- inverse. +IsoDen : (X Y : Ty [] ★) → ⟦ X ⟧ ≡ ⟦ Y ⟧ → Iso → Type +IsoDen X Y p i = + Denotes X Y (fwd i) (transport p) × Denotes Y X (bwd i) (transport (sym p)) + +------------------------------------------------------------------------ +-- Each building block. + +-- A realiser stays a realiser along a path of normal forms. +𝓡-nf : ∀ {u w : Nf [] ★} (e : u ≡ w) {v : UVal} {x : ⟦ u ⟧ⁿ} → + 𝓡 u v x → 𝓡 w v (transport (cong ⟦_⟧ⁿ e) x) +𝓡-nf e {v} {x} r = + transport (λ i → 𝓡 (e i) v (transport-filler (cong ⟦_⟧ⁿ e) x i)) r + +-- The identity transformer, between two convertible types. +id-den : (e : DefEq X Y) → IsoDen X Y (nomPath e) idIso +id-den e = + (λ t x (v , d , r) → v , d , 𝓡-nf (defEq→nf e) r) + , (λ t y (v , d , r) → v , d , 𝓡-nf (sym (defEq→nf e)) r) + +-- The identity transformer, along the constant path. +refl-den : IsoDen X X refl idIso +refl-den {X = X} = + (λ t x (v , d , r) → v , d , subst (𝓡 (nf X) v) (sym (transportRefl x)) r) + , (λ t x (v , d , r) → v , d , subst (𝓡 (nf X) v) (sym (transportRefl x)) r) + +swap-den : ∀ {p i} → IsoDen X Y p i → IsoDen Y X (sym p) (swapIso i) +swap-den (f , g) = g , f + +comp-den : ∀ {p q i j} → IsoDen X Y p i → IsoDen Y Z q j → + IsoDen X Z (p ∙ q) (compIso i j) +comp-den {X = X} {Z = Z} {p = p} {q = q} {i = i} {j = j} (f , g) (f' , g') = + (λ t x h → + let (w , d , r) = f' (fwd i t) (transport p x) (f t x h) + in w , d , subst (𝓡 (nf Z) w) (sym (transportComposite p q x)) r) + , (λ t z h → + let (w , d , r) = g (bwd j t) (transport (sym q) z) (g' t z h) + in w , d , subst (𝓡 (nf X) w) + (sym (cong (λ s → transport s z) (symDistr p q) + ∙ transportComposite (sym q) (sym p) z)) r) + +-- THE TROPE TRANSITIONS of a newtype instance: the path from `ua`. +step-den : (x : Inst) → + IsoDen (capp (stateOf x) (carrierOf x)) (carrierOf x) (ua unboxEquiv) (stepIso x) +step-den x = + (λ t b (v , d , r) → + v , d , subst (𝓡 (nf (carrierOf x)) v) (sym (uaβ unboxEquiv b)) r) + , (λ t y (v , d , r) → + v , d , subst (𝓡 (nf (carrierOf x)) v) (sym (cong unbox (~uaβ unboxEquiv y))) r) + +-- The map of a function. +arrMap-den : ∀ {h g : Tr} (p : ⟦ X ⟧ ≡ ⟦ X' ⟧) (q : ⟦ Y ⟧ ≡ ⟦ Y' ⟧) → + Denotes X' X h (transport (sym p)) → Denotes Y Y' g (transport q) → + Denotes (arr 𝟙 X Y) (arr 𝟙 X' Y') (arrMap (arr 𝟙 X Y) X' h g) + (transport (cong₂ (λ P Q → P → Q) p q)) +arrMap-den {h = h} p q ch cg t f (_ , dt , r-fun hf) = + _ , ⇓-app ⇓-lam dt ⇓-lam + , r-fun (λ w y ry → + let (w' , dw' , rw') = ch (tvar zero) y (w , ⇓-var zero , ry) + (r , dr , rr) = hf w' (transport (sym p) y) rw' + in cg (tapp (tvar (suc zero)) (h (tvar zero))) (f (transport (sym p) y)) + (r , ⇓-app (⇓-var (suc zero)) dw' dr , rr)) + +arrIso-den : ∀ {i j} (p : ⟦ X ⟧ ≡ ⟦ X' ⟧) (q : ⟦ Y ⟧ ≡ ⟦ Y' ⟧) → + IsoDen X X' p i → IsoDen Y Y' q j → + IsoDen (arr 𝟙 X Y) (arr 𝟙 X' Y') (cong₂ (λ P Q → P → Q) p q) + (arrIso X X' Y Y' i j) +arrIso-den {X = X} {X' = X'} {Y = Y} {Y' = Y'} {i = i} {j = j} p q (f , g) (f' , g') = + arrMap-den {X = X} {X' = X'} {Y = Y} {Y' = Y'} {h = bwd i} {g = fwd j} p q g f' + , arrMap-den {X = X'} {X' = X} {Y = Y'} {Y' = Y} {h = fwd i} {g = bwd j} (sym p) (sym q) f g' + +-- The map of a pair. +prodMap-den : ∀ {f g : Tr} (p : ⟦ X ⟧ ≡ ⟦ X' ⟧) (q : ⟦ Y ⟧ ≡ ⟦ Y' ⟧) → + Denotes X X' f (transport p) → Denotes Y Y' g (transport q) → + Denotes (X ⊗ Y) (X' ⊗ Y') (prodMap f g) (transport (cong₂ _×_ p q)) +prodMap-den p q cf cg t _ (_ , dt , r-pair {v = v₁} {w = v₂} {x = x} {y = y} r₁ r₂) = + let (w₁ , d₁ , s₁) = cf (tvar (suc zero)) x (v₁ , ⇓-var (suc zero) , r₁) + (w₂ , d₂ , s₂) = cg (tvar zero) y (v₂ , ⇓-var zero , r₂) + in vpair w₁ w₂ , ⇓-letp dt (⇓-pair d₁ d₂) , r-pair s₁ s₂ + +prodIso-den : ∀ {i j} (p : ⟦ X ⟧ ≡ ⟦ X' ⟧) (q : ⟦ Y ⟧ ≡ ⟦ Y' ⟧) → + IsoDen X X' p i → IsoDen Y Y' q j → + IsoDen (X ⊗ Y) (X' ⊗ Y') (cong₂ _×_ p q) (prodIso i j) +prodIso-den {X = X} {X' = X'} {Y = Y} {Y' = Y'} {i = i} {j = j} p q (f , g) (f' , g') = + prodMap-den {X = X} {X' = X'} {Y = Y} {Y' = Y'} {f = fwd i} {g = fwd j} p q f f' + , prodMap-den {X = X'} {X' = X} {Y = Y'} {Y' = Y} {f = bwd i} {g = bwd j} (sym p) (sym q) g g' + +-- The map of a sum. +sumMap-den : ∀ {f g : Tr} (p : ⟦ X ⟧ ≡ ⟦ X' ⟧) (q : ⟦ Y ⟧ ≡ ⟦ Y' ⟧) → + Denotes X X' f (transport p) → Denotes Y Y' g (transport q) → + Denotes (X ⊕ Y) (X' ⊕ Y') (sumMap f g) (transport (cong₂ _⊎_ p q)) +sumMap-den p q cf cg t _ (_ , dt , r-inl {v = v} {x = x} r) = + let (w , d , s) = cf (tvar zero) x (v , ⇓-var zero , r) + in vinl w , ⇓-casel dt (⇓-inl d) , r-inl s +sumMap-den p q cf cg t _ (_ , dt , r-inr {v = v} {y = y} r) = + let (w , d , s) = cg (tvar zero) y (v , ⇓-var zero , r) + in vinr w , ⇓-caser dt (⇓-inr d) , r-inr s + +sumIso-den : ∀ {i j} (p : ⟦ X ⟧ ≡ ⟦ X' ⟧) (q : ⟦ Y ⟧ ≡ ⟦ Y' ⟧) → + IsoDen X X' p i → IsoDen Y Y' q j → + IsoDen (X ⊕ Y) (X' ⊕ Y') (cong₂ _⊎_ p q) (sumIso i j) +sumIso-den {X = X} {X' = X'} {Y = Y} {Y' = Y'} {i = i} {j = j} p q (f , g) (f' , g') = + sumMap-den {X = X} {X' = X'} {Y = Y} {Y' = Y'} {f = fwd i} {g = fwd j} p q f f' + , sumMap-den {X = X'} {X' = X} {Y = Y'} {Y' = Y} {f = bwd i} {g = bwd j} (sym p) (sym q) g g' + +------------------------------------------------------------------------ +-- The map of a body, for a parameter that is used at the role d. + +module _ {d : Role} (hn : leR nom d ≡ true → DefEq X Y) + (hv : leR rep d ≡ true → ⟦ X ⟧ ≡ ⟦ Y ⟧) {i : Iso} + (hd : (le : leR rep d ≡ true) → IsoDen X Y (hv le) i) where + + body-den : ∀ β (le : leR (roleOf β) d ≡ true) → + IsoDen (TB β X) (TB β Y) (bodyPath hn hv β le) (bodyIso β X Y i) + body-den bvar le = hd le + body-den (bbase b) le = refl-den {X = base b} + body-den (barr β γ) le = + arrIso-den {X = TB β X} {X' = TB β Y} {Y = TB γ X} {Y' = TB γ Y} + {i = bodyIso β X Y i} {j = bodyIso γ X Y i} + (bodyPath hn hv β le₁) (bodyPath hn hv γ le₂) + (body-den β le₁) (body-den γ le₂) + where + le₁ = leR-trans _ _ _ (max-upper-l (roleOf β) (roleOf γ)) le + le₂ = leR-trans _ _ _ (max-upper-r (roleOf β) (roleOf γ)) le + body-den (bprod β γ) le = + prodIso-den {X = TB β X} {X' = TB β Y} {Y = TB γ X} {Y' = TB γ Y} + {i = bodyIso β X Y i} {j = bodyIso γ X Y i} + (bodyPath hn hv β le₁) (bodyPath hn hv γ le₂) + (body-den β le₁) (body-den γ le₂) + where + le₁ = leR-trans _ _ _ (max-upper-l (roleOf β) (roleOf γ)) le + le₂ = leR-trans _ _ _ (max-upper-r (roleOf β) (roleOf γ)) le + body-den (bsum β γ) le = + sumIso-den {X = TB β X} {X' = TB β Y} {Y = TB γ X} {Y' = TB γ Y} + {i = bodyIso β X Y i} {j = bodyIso γ X Y i} + (bodyPath hn hv β le₁) (bodyPath hn hv γ le₂) + (body-den β le₁) (body-den γ le₂) + where + le₁ = leR-trans _ _ _ (max-upper-l (roleOf β) (roleOf γ)) le + le₂ = leR-trans _ _ _ (max-upper-r (roleOf β) (roleOf γ)) le + body-den (bfam F β) le = id-den (d-papp (body-defeq hn β le)) + +------------------------------------------------------------------------ +-- The translation of a coercion. + +-- What the translation of a coercion at the role r denotes. +DenAt : ∀ r → Co r τ σ → PathAt r τ σ → Type +DenAt {τ = τ} {σ = σ} rep γ p = IsoDen (T τ) (T σ) p (coI rep γ) +DenAt nom γ p = Unit +DenAt ph γ p = Unit + +private + -- A transformer below the wrapper of a newtype: unwrap, map, wrap. + nt-wrap : ∀ N {τ σ i} (pb : ⟦ TB (body N) (T τ) ⟧ ≡ ⟦ TB (body N) (T σ) ⟧) → + IsoDen (TB (body N) (T τ)) (TB (body N) (T σ)) pb + (bodyIso (body N) (T τ) (T σ) i) → + IsoDen (T (nt₁ N τ)) (T (nt₁ N σ)) (cong Box pb) (ntIso N τ σ i) + nt-wrap N {τ} {σ} pb (f , g) = + (λ t x h → f (step (unwrap , inr (N , τ)) t) (unbox x) h) + , (λ t y h → g (step (unwrap , inr (N , σ)) t) (unbox y) h) + + nt-den : ∀ N d (le : leR (roleOf (body N)) d ≡ true) + (γ : Co d τ σ) (pa : PathAt d τ σ) → DenAt d γ pa → + IsoDen (T (nt₁ N τ)) (T (nt₁ N σ)) (ntPath N d le γ pa) (ntIso N τ σ (coI d γ)) + nt-den N rep le γ p den = + nt-wrap N (bodyPath (λ q → ⊥.rec (false≢true q)) (λ _ → p) (body N) le) + (body-den (λ q → ⊥.rec (false≢true q)) (λ _ → p) + {i = coI rep γ} (λ _ → den) (body N) le) + nt-den N nom le γ _ den = + nt-wrap N (bodyPath (λ _ → nominal-defeq γ) (λ _ → nomPath (nominal-defeq γ)) (body N) le) + (body-den (λ _ → nominal-defeq γ) (λ _ → nomPath (nominal-defeq γ)) + {i = idIso} (λ _ → id-den (nominal-defeq γ)) (body N) le) + nt-den N ph le γ _ den = + nt-wrap N (bodyPath (λ q → ⊥.rec (false≢true q)) (λ q → ⊥.rec (false≢true q)) (body N) le) + (body-den (λ q → ⊥.rec (false≢true q)) (λ q → ⊥.rec (false≢true q)) + {i = idIso} (λ q → ⊥.rec (false≢true q)) (body N) le) + + -- A newtype axiom, along the equation of the type translation. + ax-den : ∀ {C i} (e : C ≡ Z) (p : ⟦ X ⟧ ≡ ⟦ C ⟧) → IsoDen X C p i → + IsoDen X Z (subst (λ W → ⟦ X ⟧ ≡ ⟦ W ⟧) e p) i + ax-den {X = X} {i = i} e p h = + transport (λ k → IsoDen X (e k) (subst-filler (λ W → ⟦ X ⟧ ≡ ⟦ W ⟧) e p k) i) h + +coI-den : (wr : WellRoled) → ∀ r (γ : Co r τ σ) → DenAt r γ (pathAt wr r γ) +coI-den wr nom γ = tt +coI-den wr ph γ = tt +coI-den wr rep (c-sym {τ = τ} {σ = σ} γ) = + swap-den {X = T τ} {Y = T σ} {p = pathAt wr rep γ} {i = coI rep γ} (coI-den wr rep γ) +coI-den wr rep (c-trans {τ = τ} {σ = σ} {υ = υ} γ δ) = + comp-den {X = T τ} {Y = T σ} {Z = T υ} {p = pathAt wr rep γ} {q = pathAt wr rep δ} + {i = coI rep γ} {j = coI rep δ} (coI-den wr rep γ) (coI-den wr rep δ) +coI-den wr rep (c-sub γ) = id-den (nominal-defeq γ) +coI-den wr rep (c-arr {τ = τ} {τ' = τ'} {σ = σ} {σ' = σ'} γ δ) = + arrIso-den {X = T τ} {X' = T τ'} {Y = T σ} {Y' = T σ'} {i = coI rep γ} {j = coI rep δ} + (pathAt wr rep γ) (pathAt wr rep δ) (coI-den wr rep γ) (coI-den wr rep δ) +coI-den wr rep (c-prod {τ = τ} {τ' = τ'} {σ = σ} {σ' = σ'} γ δ) = + prodIso-den {X = T τ} {X' = T τ'} {Y = T σ} {Y' = T σ'} {i = coI rep γ} {j = coI rep δ} + (pathAt wr rep γ) (pathAt wr rep δ) (coI-den wr rep γ) (coI-den wr rep δ) +coI-den wr rep (c-sum {τ = τ} {τ' = τ'} {σ = σ} {σ' = σ'} γ δ) = + sumIso-den {X = T τ} {X' = T τ'} {Y = T σ} {Y' = T σ'} {i = coI rep γ} {j = coI rep δ} + (pathAt wr rep γ) (pathAt wr rep δ) (coI-den wr rep γ) (coI-den wr rep δ) +coI-den wr rep (c-nt₁ N γ) = + nt-den N (mulG rep (role N)) (wr N) γ (pathAt wr (mulG rep (role N)) γ) + (coI-den wr (mulG rep (role N)) γ) +coI-den wr rep (c-ax₀ N) = + ax-den {X = T (nt₀ N)} {C = TE (rep₀ N)} {i = stepIso (inl N)} + (sym (T-embE (rep₀ N))) (ua unboxEquiv) (step-den (inl N)) +coI-den wr rep (c-ax₁ N τ) = + ax-den {X = T (nt₁ N τ)} {C = TB (body N) (T τ)} {i = stepIso (inr (N , τ))} + (sym (T-inst (body N) τ)) (ua unboxEquiv) (step-den (inr (N , τ))) + +------------------------------------------------------------------------ +-- THE CROSS-CHECK. + +coercion-denotes-transport : + (wr : WellRoled) → ∀ {τ σ} (γ : Co rep τ σ) → + Denotes (T τ) (T σ) (fwd (coI rep γ)) (transport (pathOf wr γ)) +coercion-denotes-transport wr γ = fst (coI-den wr rep γ) + +coercion-denotes-transport-back : + (wr : WellRoled) → ∀ {τ σ} (γ : Co rep τ σ) → + Denotes (T σ) (T τ) (bwd (coI rep γ)) (transport (sym (pathOf wr γ))) +coercion-denotes-transport-back wr γ = snd (coI-den wr rep γ) + +-- The coercion function: a closure that realises transport. +coerce-function-is-transport : + (wr : WellRoled) → ∀ {τ σ} (γ : Co rep τ σ) {n} {ρ : UEnv n} → + Real (arr 𝟙 (T τ) (T σ)) ρ (eraseT (coerceT γ)) (transport (pathOf wr γ)) +coerce-function-is-transport wr γ = + _ , ⇓-lam + , r-fun (λ w x rx → fst (coI-den wr rep γ) (tvar zero) x (w , ⇓-var zero , rx)) diff --git a/verification/proofs/agda/Wager/Univalent/Model.agda b/verification/proofs/agda/Wager/Univalent/Model.agda new file mode 100644 index 0000000..a950a55 --- /dev/null +++ b/verification/proofs/agda/Wager/Univalent/Model.agda @@ -0,0 +1,215 @@ +{-# OPTIONS --cubical --safe #-} +-- Forced by cubical-0.9 (InfectiveImport). No coinduction is used. +{-# OPTIONS --guardedness #-} +-- DESIGN-CHOICES.adoc, DC-0.3: matches on normal forms and on coercions. +{-# OPTIONS -WnoUnsupportedIndexedMatch #-} +-- SPDX-License-Identifier: MPL-2.0 +-- +-- Stage 7 (the optional univalent cross-check): the model. +-- +-- The types of the target of Stage 4 get an interpretation in the +-- cubical universe (DESIGN-CHOICES.adoc, DC-7.1): +-- +-- a base constant b the type `El b` (a parameter of the model) +-- a function, pair, sum the function type, the product, the sum +-- a newtype instance `Box X`: a wrapper of the interpretation X of +-- its content. `Box X` is not X, and +-- `unboxEquiv` is an equivalence `Box X ≃ X`. +-- +-- A trope transition (wrap, unwrap) is thus an equivalence, and +-- univalence (`ua`) makes it a path between two types. +-- +-- A term has no interpretation by itself. The model is a realisability +-- model: `𝓡 u v x` says that the untyped value v, the result of an +-- erased program, realises the element x of the interpretation of u. +-- A wrapper has no realiser of its own: v realises `box x` when v +-- realises x. +-- +-- `Denotes X Y f g` says that the term transformer f denotes the +-- function g: on a term that evaluates to a realiser of x, the term +-- `f t` evaluates to a realiser of `g x`. +-- +-- `pathOf γ` is the path of a representational coercion γ. It is made +-- from `ua unboxEquiv` (a newtype axiom), `sym`, composition, and +-- congruence of the type formers. +open import Cubical.Foundations.Prelude +open import Wager.FC.Signature +open import Wager.Grade.Algebra +import Wager.Trans.Scheme +module Wager.Univalent.Model + (SS : SSig) (Sc : Wager.Trans.Scheme.StateScheme SS) + {R : Type} (A : GradeAlgebra R) + (El : SSig.Base SS → Type) + (elLit : (ℓ : SSig.Lit SS) → El (SSig.litTy SS ℓ)) where + +open import Cubical.Foundations.Equiv using (_≃_) +import Cubical.Foundations.Isomorphism as CI +open import Cubical.Foundations.Univalence using (ua) +open import Cubical.Data.Bool.Base using (true; false) +open import Cubical.Data.Empty as ⊥ using (⊥) +open import Cubical.Data.Unit using (Unit*; tt*) +open import Cubical.Data.Nat.Base using (ℕ; zero; suc) +open import Cubical.Data.Sigma using (_×_; _,_; Σ-syntax) +open import Cubical.Data.Sum.Base using (_⊎_; inl; inr) + +open import Wager.Grade.Finite using (false≢true) +open import Wager.Role.Role +open import Wager.FC.Types SS +open import Wager.FC.Coercion SS +open import Wager.Trans.Target SS Sc (GradeAlgebra.ops A) +open import Wager.Trans.Nominal SS Sc (GradeAlgebra.ops A) using (nominal-defeq; T-inst; T-embE) +open import Wager.Trans.Coercion SS Sc (GradeAlgebra.ops A) using (Tr; Tm; eraseT) +open import Wager.Trans.Typing SS Sc A using (body-defeq) +open import Wager.L1.Normal tSig +open import Wager.L1.Eval tSig using (nf) +open import Wager.L1.Conversion tSig +open import Wager.L1.Equality tSig using (defEq→nf) +open import Wager.Erased.Untyped +open Terms Lit + +private + variable + X Y : Ty [] ★ + τ σ : STy + +------------------------------------------------------------------------ +-- The interpretation of types. + +-- A newtype instance: a wrapper of its content. +record Box (Z : Type) : Type where + constructor box + field + unbox : Z + +open Box public + +-- THE EQUIVALENCE OF A NEWTYPE TRANSITION. +unboxEquiv : {Z : Type} → Box Z ≃ Z +unboxEquiv = CI.isoToEquiv (CI.iso unbox box (λ _ → refl) (λ _ → refl)) + +-- A closed normal form of the kind ★. The empty context has no neutral +-- type (`Wager.L2.Erasure.noNe`), so the first clause is not used. +⟦_⟧ⁿ : Nf [] ★ → Type +⟦ ne m ⟧ⁿ = ⊥ +⟦ nbase b ⟧ⁿ = El b +⟦ ncapp s u ⟧ⁿ = Box ⟦ u ⟧ⁿ +⟦ narr q a b ⟧ⁿ = ⟦ a ⟧ⁿ → ⟦ b ⟧ⁿ +⟦ a n⊗ b ⟧ⁿ = ⟦ a ⟧ⁿ × ⟦ b ⟧ⁿ +⟦ a n⊕ b ⟧ⁿ = ⟦ a ⟧ⁿ ⊎ ⟦ b ⟧ⁿ + +-- A closed type: the interpretation of its normal form. Two convertible +-- types thus have one interpretation. +⟦_⟧ : Ty [] ★ → Type +⟦ Z ⟧ = ⟦ nf Z ⟧ⁿ + +------------------------------------------------------------------------ +-- Realisers. + +-- A literal ℓ realises its element `elLit ℓ`. +data RLit (b : Base) : UVal → El b → Type where + r-lit : ∀ ℓ (p : litTy ℓ ≡ b) → RLit b (vlit ℓ) (subst El p (elLit ℓ)) + +-- A closure realises a function: on a realiser of x, its body evaluates +-- to a realiser of `f x`. +data RFun {P Q : Type} (𝒫 : UVal → P → Type) (𝒬 : UVal → Q → Type) : + UVal → (P → Q) → Type where + r-fun : ∀ {n} {ρ : UEnv n} {t : UTm (suc n)} {f : P → Q} → + (∀ w x → 𝒫 w x → Σ[ r ∈ UVal ] ((w ∷ᵉ ρ) ⊢ t ⇓ r) × 𝒬 r (f x)) → + RFun 𝒫 𝒬 (vclo ρ t) f + +data RPair {P Q : Type} (𝒫 : UVal → P → Type) (𝒬 : UVal → Q → Type) : + UVal → P × Q → Type where + r-pair : ∀ {v w x y} → 𝒫 v x → 𝒬 w y → RPair 𝒫 𝒬 (vpair v w) (x , y) + +data RSum {P Q : Type} (𝒫 : UVal → P → Type) (𝒬 : UVal → Q → Type) : + UVal → P ⊎ Q → Type where + r-inl : ∀ {v x} → 𝒫 v x → RSum 𝒫 𝒬 (vinl v) (inl x) + r-inr : ∀ {v y} → 𝒬 v y → RSum 𝒫 𝒬 (vinr v) (inr y) + +-- THE REALISABILITY RELATION. A wrapper is not seen at run time. +𝓡 : (u : Nf [] ★) → UVal → ⟦ u ⟧ⁿ → Type +𝓡 (ne m) = λ v x → ⊥ +𝓡 (nbase b) = RLit b +𝓡 (ncapp s u) = λ v x → 𝓡 u v (unbox x) +𝓡 (narr q a b) = RFun (𝓡 a) (𝓡 b) +𝓡 (a n⊗ b) = RPair (𝓡 a) (𝓡 b) +𝓡 (a n⊕ b) = RSum (𝓡 a) (𝓡 b) + +-- An untyped term, in an environment, evaluates to a realiser of x. +Real : (Z : Ty [] ★) → ∀ {n} → UEnv n → UTm n → ⟦ Z ⟧ → Type +Real Z ρ u x = Σ[ v ∈ UVal ] (ρ ⊢ u ⇓ v) × 𝓡 (nf Z) v x + +-- THE DENOTATION OF A TERM TRANSFORMER. The transformer f, from the +-- type X to the type Y, denotes the function g. +Denotes : (X Y : Ty [] ★) → Tr → (⟦ X ⟧ → ⟦ Y ⟧) → Type +Denotes X Y f g = + ∀ {n} {ρ : UEnv n} (t : Tm n) (x : ⟦ X ⟧) → + Real X ρ (eraseT t) x → Real Y ρ (eraseT (f t)) (g x) + +------------------------------------------------------------------------ +-- The path of a coercion. + +-- Two convertible types have one interpretation. +nomPath : DefEq X Y → ⟦ X ⟧ ≡ ⟦ Y ⟧ +nomPath e = cong ⟦_⟧ⁿ (defEq→nf e) + +-- The path of a body, from the path of its parameter. The parameter is +-- used at the role d. Below a type-level function the two instances are +-- convertible (`body-defeq`). +module _ {d : Role} (hn : leR nom d ≡ true → DefEq X Y) + (hv : leR rep d ≡ true → ⟦ X ⟧ ≡ ⟦ Y ⟧) where + + bodyPath : ∀ β → leR (roleOf β) d ≡ true → ⟦ TB β X ⟧ ≡ ⟦ TB β Y ⟧ + bodyPath bvar le = hv le + bodyPath (bbase b) le = refl + bodyPath (barr β γ) le = + cong₂ (λ P Q → P → Q) + (bodyPath β (leR-trans _ _ _ (max-upper-l (roleOf β) (roleOf γ)) le)) + (bodyPath γ (leR-trans _ _ _ (max-upper-r (roleOf β) (roleOf γ)) le)) + bodyPath (bprod β γ) le = + cong₂ _×_ + (bodyPath β (leR-trans _ _ _ (max-upper-l (roleOf β) (roleOf γ)) le)) + (bodyPath γ (leR-trans _ _ _ (max-upper-r (roleOf β) (roleOf γ)) le)) + bodyPath (bsum β γ) le = + cong₂ _⊎_ + (bodyPath β (leR-trans _ _ _ (max-upper-l (roleOf β) (roleOf γ)) le)) + (bodyPath γ (leR-trans _ _ _ (max-upper-r (roleOf β) (roleOf γ)) le)) + bodyPath (bfam F β) le = nomPath (d-papp (body-defeq hn β le)) + +-- What a coercion at the role r gives: a path at the role +-- representational, and no data at the two other roles. +PathAt : Role → STy → STy → Type₁ +PathAt rep τ σ = ⟦ T τ ⟧ ≡ ⟦ T σ ⟧ +PathAt nom τ σ = Unit* +PathAt ph τ σ = Unit* + +-- Congruence for a newtype: the path of the body, below the wrapper. +ntPath : ∀ N d → leR (roleOf (body N)) d ≡ true → + Co d τ σ → PathAt d τ σ → ⟦ T (nt₁ N τ) ⟧ ≡ ⟦ T (nt₁ N σ) ⟧ +ntPath N rep le γ p = + cong Box (bodyPath (λ q → ⊥.rec (false≢true q)) (λ _ → p) (body N) le) +ntPath N nom le γ _ = + cong Box (bodyPath (λ _ → nominal-defeq γ) (λ _ → nomPath (nominal-defeq γ)) (body N) le) +ntPath N ph le γ _ = + cong Box (bodyPath (λ q → ⊥.rec (false≢true q)) (λ q → ⊥.rec (false≢true q)) (body N) le) + +pathAt : WellRoled → ∀ r → Co r τ σ → PathAt r τ σ +pathAt wr nom γ = tt* +pathAt wr ph γ = tt* +pathAt wr rep (c-sym γ) = sym (pathAt wr rep γ) +pathAt wr rep (c-trans γ δ) = pathAt wr rep γ ∙ pathAt wr rep δ +pathAt wr rep (c-sub γ) = nomPath (nominal-defeq γ) +pathAt wr rep (c-arr γ δ) = cong₂ (λ P Q → P → Q) (pathAt wr rep γ) (pathAt wr rep δ) +pathAt wr rep (c-prod γ δ) = cong₂ _×_ (pathAt wr rep γ) (pathAt wr rep δ) +pathAt wr rep (c-sum γ δ) = cong₂ _⊎_ (pathAt wr rep γ) (pathAt wr rep δ) +pathAt wr rep (c-nt₁ N γ) = + ntPath N (mulG rep (role N)) (wr N) γ (pathAt wr (mulG rep (role N)) γ) +-- THE NEWTYPE AXIOMS: the path from `ua`. +pathAt wr rep (c-ax₀ N) = + subst (λ Z → ⟦ T (nt₀ N) ⟧ ≡ ⟦ Z ⟧) (sym (T-embE (rep₀ N))) (ua unboxEquiv) +pathAt wr rep (c-ax₁ N τ) = + subst (λ Z → ⟦ T (nt₁ N τ) ⟧ ≡ ⟦ Z ⟧) (sym (T-inst (body N) τ)) (ua unboxEquiv) + +-- THE PATH OF A REPRESENTATIONAL COERCION. +pathOf : WellRoled → Co rep τ σ → ⟦ T τ ⟧ ≡ ⟦ T σ ⟧ +pathOf wr γ = pathAt wr rep γ diff --git a/verification/proofs/agda/Wager/VERDICT.adoc b/verification/proofs/agda/Wager/VERDICT.adoc index af9d8e3..8910c21 100644 --- a/verification/proofs/agda/Wager/VERDICT.adoc +++ b/verification/proofs/agda/Wager/VERDICT.adoc @@ -1,7 +1,7 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) = Wager: verdict -Status: DRAFT after Stage 4. This file becomes final after the last stage. +Status: FINAL, after Stage 7 (2026-11-10). Two decisions are with the owner: the class of the kinding judgement (R1), and the class of the extension of Stage 6, part 2 (R23, R24). :toc: left :sectnums: @@ -57,13 +57,44 @@ Status: DRAFT after Stage 4. This file becomes final after the last stage. *A condition on the grade algebra.* `t5-typing` needs a grade algebra in which the grade `𝟙` is unrestricted: `𝟘 ≤ 𝟙` and `𝟙 + 𝟙 ≤ 𝟙` (DC-4.5). System FC has no usage discipline. In `Affine` the translation of the source function `λx. 5`, which drops its argument, has no type (`Wager.Examples.Stage4.Coercions-In-Affine.const-rejected`). Agda checked this one function. -| T6 | NOT ATTEMPTED | Stage 5 is not started. The lemma that T6 needs is proved, because T5 uses it: `Wager.Trans.Nominal.nominal-defeq` (DC-4.4). Stage 5 states T6. -| T7 | NOT ATTEMPTED | Stage 6 is not started. +| T6 +| PROVED +| `Wager.Proofs.t6`: for each nominal coercion of the source, the two translated types have one normal form. + `Wager.Proofs.t6-conversion`: the two translated types are convertible. `Wager.Proofs.t6-no-term`: the translation of a cast along a nominal coercion is the translation of the term under the cast. + Each holds for each source signature, each state scheme and each set of grade operations. None needs the role check. + T6 is one direction. The converse is false for the row scheme (finding F16, DC-5.2). +| T7 +| Part 1 (the separation): PROVED. Part 2 (the identity type): PROVED, for a signature that has an identity family. The class of the extension is the decision of the owner +| The owner asked for the two options of Stage 6, the separation first (DC-6.1). + + *Part 1.* `Wager.Proofs.t7-separation`: for each base type b and each closed type α, no typed closed term of the target has the erasure of the source program `gadt-eval b α` together with a type that has the erased type of the source type. + This holds for each target signature and each set of grade operations. + The program is a term of the source calculus of Stage 6 (`Wager.Local.Source`), so it is well typed there. That calculus has local equality assumptions (DC-6.3). + + *What part 1 does not say.* It does not say "the program has no translation". It excludes a translation that keeps the erased type and the erased term, and no other translation (DC-6.4). + The erased program has a simple type with another type of the data (`Wager.Examples.Stage6.other-erased-type`), and a typed target term with the same erasure exists at that type, for the signature of Stage 5 and the one-point grade algebra (`other-typed`, `other-same-erasure`). + A type is closed in this development (DC-6.2). The statement is about each closed instance of the program. It is not about a polymorphic program. + + *Part 2.* EQUALITY EVIDENCE IS NOW A TERM. The identity type is a family of base constants of a signature, `Id A B`, with one literal `rfl A` on the diagonal (DC-6.5). The extension has one new term former, `cast e t`, and one new rule, `t-cast`, which uses the evidence at the grade `𝟘` (DC-6.6). + The statements are in `Wager.Statements.T7-Identity-Statements`. Each holds for each signature that has an identity family and for each set of grade operations. The last two need the laws of a grade algebra. + + * `Wager.Proofs.t7-erasure`: for a closed typed term, the reference program (which evaluates the evidence of each cast) and the program with no evidence in its casts evaluate, and the two values are observationally equal at the erased type. `t7-erasure-first-order`: at a first-order type the two programs have one value. + * `t7-intro` and `t7-canonicity`: a conversion gives evidence, and closed evidence gives a conversion. The family thus adds no equality between closed types. + * `t7-conservative` and `t7-conservative-erasure`: each typed term of the target is a typed term of the extension, with the same erasure. + * `t7-grade`: in a grade algebra, the usage vector of `cast e t` is the usage vector of the payload. + * `t7-assumption`: in a grade algebra, for each pair of closed types A and B, the function `λ e. λ x. cast e x` has the type `Id A B → A → B`, with the first parameter at the grade `𝟘`. The first parameter is a local equality assumption. + + *What part 2 does not say.* It does not say that each signature has an identity family: one signature has one (`Wager.Identity.Instance`, DC-6.8). The erasure removes the evidence of a cast and no other evidence (DC-6.7). + It does not prove and does not refute the statement of part 1 for the extension. The extension has no reduction relation, so progress and preservation are not proved for it (DC-6.6). |=== Stage 1 also proved the L1 equivalence that the task asks for: `Wager.Proofs.l1-equality` : `DefEq t u ↔ nf t ≡ nf u`, for each signature. +Stage 7, the optional univalent cross-check, is done. It has no theorem number in the task. +`Wager.Proofs.coercion-denotes-transport`: in a realisability model of the target types in the cubical universe, the translation of each representational coercion denotes transport along a path that is made with `ua`. `coercion-denotes-transport-back` is the other direction, and `coerce-function-is-transport` is the statement for the coercion function. +Each holds for each source signature that passes the role check, each state scheme, each grade algebra and each interpretation of the base constants. + == Results of Stage 3: the source calculus Stage 3 has no T number. It defines the source calculus of claim W, a small fragment of System FC with roles (`Wager.FC`, DC-3.1 to DC-3.6). @@ -170,24 +201,175 @@ The translation with the row scheme gives the two types two states of the carrie * No theorem says that a role-rejected `coerce` has no translation. The source calculus has no term for such a `coerce` (DC-3.5), and the role correspondence is about kinding. * The row scheme has a finite index type for a finite signature. Agda did not check this sentence (DC-4.1). +== Results of Stage 5: nominal coercions + +T6 is in the table of theorems. Its proof is the lemma that Stage 4 needed for the typing of a cast (DC-4.4, DC-5.1). + +Checked examples (`Wager.Examples.Stage5`): + +* One nominal coercion for each kind of equation of a type-level function (a base type, a newtype with no parameter, a newtype with a parameter, a function type), a congruence below a nominal newtype, and the instance of T6 for each. +* A cast along a nominal coercion: the translation of `'c' : Char` cast to the type `F Age` is the literal, typed at the translated type `F Age` by conversion (`no-term`, `typed-by-conversion`). +* Rejected: `Age` and `Int` have no nominal coercion, and their translations have two normal forms (`age-int-rejected`, `age-int-nf-differ`). + +=== Not proved in Stage 5 + +* The converse of T6. It is false for the row scheme (finding F16). +* The sentence "two source types with one target normal form have one erased type". This development has no proof of it and no counterexample to it. + +== Results of Stage 6, part 1: the separation + +The first result is about the target calculus as it is (`Wager.L2.Erasure`): + +* `erase-typed`: a typed target term erases to a term with a simple type, the erased type of its target type. This holds for each signature and each set of grade operations. +* `identity-one-type`: if a target term has the type `A → B` and erases to the identity function, then `A` and `B` have one erased type. + +The reason is the rule `t-conv`: the target calculus has conversion and no other equality of types, and two convertible types have one normal form. + +Checked examples (`Wager.Examples.Stage6`): + +* The source program at two instances (`eval-at-int`, `eval-at-sum`). The erased text is the same at each instance (`one-erased-text`). +* The first branch runs: the erased program, applied to the constructor GI with the literal `ℓint`, gives that literal (`live-branch-runs`). +* Rejected in the source: with no assumption, `Int ~ Int + Int` has no evidence (`no-evidence-for-gb`), because a closed equality of the source calculus is the identity of types (`closed-equality-is-identity`). +* Rejected in the target, for the signature of Stage 5 and the one-point grade algebra: the instance of T7 (`no-target-term`), and the identity function at the type `Int → Int + Int` (`identity-rejected`). +* Accepted in the target with another type of the data, for the same signature and algebra: `other-typed` and `other-same-erasure`. + +=== Not proved in Stage 6, part 1 + +* Type safety of the source calculus of Stage 6. In particular: "no closed term has the type `⟨ τ ~ σ ⟩ ρ` when τ and σ are different". `no-evidence-for-gb` is about evidence of the form `Coˡ`. It is not about each closed term. +* A separation for a translation that changes the erased type or the erased term. +* A statement about a polymorphic program. The development has no type variable in a term (DC-6.2). + +== Results of Stage 6, part 2: the identity type + +The extension is the target with an identity family (`Wager/Identity`). It is in separate modules, and no definition of stages 1 to 5 changes. + +The main lemma is `Wager.Identity.Soundness.fund`: for a typed term in two related environments, the reference program and the program with no evidence in its casts evaluate to related values. +The case of a cast uses the value of the evidence. The value is a literal of the base type `Id A B`. The family has no literal off the diagonal, so A and B are convertible, so they have one erased type. + +*Totality.* `fund` shows that each closed typed term has a value in the reference program. The reference program evaluates the evidence of each cast. The erased program does not, and it has the same value. The erasure is thus sound because the evidence has a value (DC-6.7). + +*The grade.* The proof of `fund` does not use the grade of the rule `t-cast`. A test with the grade `𝟙` in the rule shows this (`TOOLCHAIN.adoc`). The grade gives `t7-grade`: the usage of a cast is the usage of its payload. +This development has no semantics that counts resources, so no theorem joins the behaviour and the resource count. + +Checked examples (`Wager.Examples.Stage6Identity`), for the signature of `Wager.Identity.Instance` with one base constant and one literal: + +* Accepted: a cast along `rfl` (`cast-one-typed`). Its erasure is the literal alone (`cast-one-erased`), and the two programs give that literal (`cast-one-keep`, `cast-one-erase`, `cast-one-sound`). +* Rejected: no closed term is evidence that `Int` is `Int + Int` (`no-evidence`). +* Rejected: a cast with evidence that has no value (`stuck`). The erased program has a value (`stuck-erase`), the reference program has none (`stuck-keep`), and the term has no type (`stuck-untyped`). The typing hypothesis of `T7-Erasure` is thus needed. +* Accepted: the function `Id Int (Int + Int) → Int → Int + Int` (`assume-typed`). Its erasure is `λ e. λ x. x` (`assume-erased`). The same function is typed in the algebra `{0, 1, ω}`, with the assumption at the grade `0` (`AtAffine.assume-affine`). +* Accepted: the GADT program of part 1, with data that holds the evidence (`evalⁱ-typed`, for each closed type α, in the one-point grade algebra). It has one erased text for each α (`evalⁱ-erased`). At α := `Int`, on the first constructor, the erased program gives the literal (`gi-one-runs`, `gi-one-sound`). +* The limit: the erased type of the data has a component for the evidence (`data-holds-evidence`). + +=== Not proved in Stage 6, part 2 + +* That each signature has an extension with an identity family. One signature has a family (DC-6.8). +* Progress and preservation for the extension. It has no reduction relation (DC-6.6). +* The removal of evidence that is data. The erasure removes the evidence of a cast and no other evidence (DC-6.7). +* A translation from the source calculus of Stage 6 (`Wager.Local.Source`) into the extension, with a theorem as T5. One program is typed in the extension, by hand. +* The GADT program in a grade algebra other than the one-point algebra. This was not tried. A component of a pair has the grade `𝟙` (the rule `t-letp`), and the program uses the evidence component in a cast only, where it counts as `𝟘`. A typing with `t-sub` needs `𝟘 ≤ 𝟙` for that component. Agda did not check that no other typing exists. The target has no pair with a graded component. +* The statement of part 1 for the extension, and its negation. +* That type checking of the extension is decidable. A cast names its evidence, so a checker does not search for evidence. This is by inspection of the rule. + +=== The trade of Stage 6 + +The task says: "Do not decide whether option 1 adds a relation. Describe the trade and leave the decision to the owner." This section gives the facts for the decision. It does not make the decision. + +*The question.* Is the target with an identity family (part 2) inside the wager, which says that the target "uses only the judgement forms in `docs/theory/00-notation.adoc`"? + +*What the target can do with no identity family (part 1).* It has conversion and no other equality of types. It cannot type the two branches of one GADT match in the direct way (`T7-Separation`, with the limits of DC-6.2 and DC-6.4). + +*What the identity family gives (part 2).* + +* A local equality assumption is a variable (`T7-Assumption`). A cast uses it. The GADT program has a typed form. +* The erasure of the proofs in casts is sound (`T7-Erasure`). +* No new equality between closed types: a closed term is evidence for `Id A B` exactly when A and B are convertible (`T7-Intro`, `T7-Canonicity`). + +*What the identity family costs.* + +* EQUALITY EVIDENCE IS A TERM. The judgement `γ ▸ Γ ⊢ⁱ e ∶ base (Id A B)` says that A and B are equal under the assumptions in Γ. An equality with assumptions is thus in the calculus, in the typing judgement. +* Under a binder, conversion does not use an assumption. A program must name a cast at each use. Two types that are equal by an assumption are not convertible. +* The signature must have the family. This is a hypothesis. +* Evidence is data at run time, apart from the evidence of a cast. +* An open term can have a false assumption. Its body then does not run in a closed typed program, as in System FC. + +*Facts for the answer "no relation is added".* + +* The count of new judgement forms is 0. The count of new type formers is 0. `Ty`, `DefEq` and `nf` do not change (`RULE-DIFF-LEDGER.adoc`). +* The family is a set of entries of a signature. DC-1.1 says that a later stage adds entries to a signature. +* The typing judgement has its form of 00-notation, with 1 more rule. + +*Facts for the answer "a relation is added".* + +* The new rule `t-cast` is not in 00-notation, and the term former `cast` is not in the term syntax of the target. +* The typing judgement at the types `base (Id A B)` is a relation between two types under assumptions. It has the same reading as the relation `Coˡ` of the source calculus of Stage 6 (R21), the coercion judgement with assumptions. Agda does not check a correspondence between the two. +* The doctrine of the repository says that the calculus keeps one primitive relation, and that equality is conversion. With the family, a second way to show that two types are equal exists inside a binder. + +*What does not depend on the answer.* A local equality assumption is outside the fragment of claim W (newtypes, roles, `coerce`, total type-level functions). The results for W (T0 to T6) do not use the identity family. +== Results of Stage 7: the univalent cross-check + +The stage is optional. The owner asked for it. Stages 1 to 5 were complete. + +*The model* (`Wager.Univalent.Model`, DC-7.1). A closed type of the target of Stage 4 is a type of the cubical universe. A base constant is a type that the model gets as a parameter. A newtype instance is a wrapper `Box X` of the interpretation X of its content, and `unboxEquiv : Box X ≃ X` is an equivalence. A trope transition is thus an equivalence, and `ua unboxEquiv` is a path between the two types. + +*The denotation* (DC-7.2). The development has no function from a typed term to an element of the model. The model is a realisability model: an untyped value, the result of an erased program, realises an element. A wrapper is not seen at run time. + +*The result.* `pathOf wr γ` is a path between the interpretations of the two sides of a representational coercion γ (DC-7.3). The transformer that Stage 4 gives for γ denotes the function `transport (pathOf wr γ)`: on a term that evaluates to a realiser of x, the transformed term evaluates to a realiser of `transport (pathOf wr γ) x`. +The proof (`Wager.Univalent.CrossCheck.coI-den`) has the shape of the typing proof of Stage 4. At a newtype axiom it uses `uaβ`: transport along `ua unboxEquiv` is `unbox`. + +*What the cross-check adds to T3.* T3 says that an erased coercion does not change the value at run time. Stage 7 says what the coercion does to the meaning of the value: it moves the element along a path of types. The two facts agree: the realiser stays, and the element is transported. + +Checked examples (`Wager.Examples.Stage7`), for the signature `taggedS rep`, the row scheme and the one-point grade algebra, with `Int` as the natural numbers: + +* `Int` is the type of natural numbers, and `Age` is a wrapper of it (`int-is-nat`, `age-is-box`). +* Accepted: the axiom `Age ~ Int`. Transport along its path gives 7 from `box 7`, by computation (`age-transport`). The literal realises `box 7` at `Age` (`age-literal`), and the coerced term evaluates to a realiser of the transported element (`age-coerced`). The coercion function is a closure that realises transport (`age-function`). +* Accepted: congruence below the newtype `Box`. Transport along the path gives `box (7 , 3)` from `box (box 7 , 3)`, by computation (`box-transport`). +* Rejected: a literal does not realise a function (`literal-not-function`), and the literal of the type `Bool` does not realise a number (`bool-not-number`). + +=== Not proved in Stage 7 + +* A denotation of each typed term of the target, with a fundamental lemma for the typing judgement. The statements of the stage are about the transformer of a coercion. +* That each element of the model has a realiser, and that a value realises one element only. +* That `pathOf wr γ` is the only path between the two interpretations, or that two coercions between the same two types give one path. +* A model with a different type for each newtype name. Two newtypes with one content have one interpretation (DC-7.1). +* A statement about the identity family of Stage 6, part 2 in this model. == Overall result -Not available. W is not decided after Stage 4. T6 and T7 are not attempted. +*W does not hold as written. W holds for the fragment with 2 additions.* +The rule of the task says: W holds for the fragment only if T0 and T2 to T6 are PROVED, the relation ledger has no ADDED entry, and the rule-diff ledger is empty. T0, T3, T4 and T6 are PROVED. T2 and T5 are PROVED WITH CHANGE, so the rule is not met. The relation ledger has no ADDED entry, and the rule-diff ledger has no entry for the target calculus of stages 1 to 5. +The smallest addition that makes W true has 2 parts. (1) Trope states with an index: a newtype with a parameter gets one wrapped state for each index of a state scheme, in place of the 2 states of `07-tropes.adoc` (the change of T5). With 2 states, the program of `Wager.Proofs.no-two-state-translation` has no translation of types that keeps the 3 properties of DC-4.8. (2) For a whole program, a grade algebra in which the grade `𝟙` is unrestricted (`𝟘 ≤ 𝟙` and `𝟙 + 𝟙 ≤ 𝟙`), because System FC has no usage discipline. In the algebra `{0, 1, ω}` the translation of the function `λx. 5` has no type (`Wager.Examples.Stage4.Coercions-In-Affine.const-rejected`). The translation of a coercion alone is typed in each grade algebra. +The hypothesis `Valid` of T2 is not an addition for W: each signature that the translation gives satisfies it (`Wager.Proofs.target-signature-valid`). +With the 2 additions, each well-typed program of the fragment has a translation that preserves types and that preserves behaviour after erasure (T5), for each source signature that passes the role check. Each coercion erases to a function that is observationally the identity (T3). A nominal coercion becomes conversion, and no term remains (T6). The role check of the source has the form of the role correspondence in the target (DC-4.7), and the classic unsound program is rejected (T4). No typing rule of the target names a grade other than `𝟘` and `𝟙`, and no rule has a side condition for one algebra. +Agda found no program of the fragment that makes W false with the 2 additions: T5 is a theorem, not a test. + +Two decisions are with the owner. They can change the answer. + +. The kinding judgement has a graded context (R1, "baseline, changed"). If this counts as a change of a judgement form of 00-notation, then W needs a third addition. +. The identity family of Stage 6, part 2 (R23, R24). A local equality assumption is outside the fragment of W, so the answer for W does not depend on this decision. The decision says if the target with the family is a part of the calculus (the trade of Stage 6). + +Status after Stage 7: T0, T1, T3, T4 and T6 are PROVED. T2 and T5 are PROVED WITH CHANGE (class: signature primitive). The two parts of T7 are PROVED, part 2 for a signature that has an identity family. The optional cross-check of Stage 7 is PROVED. + -Results that bear on W after Stage 4: +Results that bear on W, in a list: * Parts (a) and (b) of W hold for the fragment, for each source signature that passes the role check: T5. They hold with one change (a newtype with a parameter needs more than one wrapped state) and one condition (an unrestricted grade `𝟙` for whole programs). * Part (c) of W holds in the sense of T3: each erased coercion is observationally the identity. It is not the empty term (finding F14). * Part (d) of W has the form of the role correspondence (DC-4.7). -* The target calculus has the judgement forms of Stage 1 only. No relation is added and no rule is added. -* T2 is "PROVED WITH CHANGE", so the condition "T2 to T6 are PROVED" of the task does not hold as written. The hypothesis of T2 holds for each signature that the translation gives (`target-signature-valid`). +* The target calculus of stages 1 to 5 has the judgement forms of Stage 1 only. No relation is added and no rule is added. The results for W (T0 to T6) do not use the extension of Stage 6, part 2. +* T2 and T5 are "PROVED WITH CHANGE", so the condition "T2 to T6 are PROVED" of the task does not hold as written. The hypothesis of T2 holds for each signature that the translation gives (`target-signature-valid`). +* A nominal coercion becomes conversion, and no term remains: T6. +* A local equality assumption is outside the fragment of W. The target calculus as it is cannot type one GADT match in the direct way: part 1 of T7, with the limits of DC-6.2 and DC-6.4. Agda checked one program, at each closed instance. +* With an identity family, a local equality assumption is a variable, and the erasure of the proofs in casts is sound: part 2 of T7. The extension has 1 new rule and 1 new term former, and equality evidence is a term. The owner decides if this extension is inside the wager (the trade of Stage 6). +* In a realisability model of the target types in the cubical universe, the translation of a representational coercion denotes transport along a path that is made with `ua`: Stage 7. The cross-check agrees with T3. -== Ledgers after Stage 4 +== Ledgers after Stage 7 -* `RELATION-LEDGER.adoc`: no ADDED entry. One entry is "baseline, changed": the kinding judgement has a graded context (R1). Stage 2 added two "specification only" entries (`≈`, and the observers with `Valid`). +* `RELATION-LEDGER.adoc`: no ADDED entry, and 2 entries with no class (R23 and R24, the extension of Stage 6, part 2: the owner decides). One entry is "baseline, changed": the kinding judgement has a graded context (R1). Stage 2 added two "specification only" entries (`≈`, and the observers with `Valid`). Stage 3 added the relations of the source calculus with the class "source" (the coercion relation `Co` is one of them), and the evaluation and the typing of erased terms as "specification only". - Stage 4 added observational equality (`𝒱`) and the definition of a translation as "specification only". Stage 3 and Stage 4 added nothing to the target calculus. -* `RULE-DIFF-LEDGER.adoc`: empty. Stages 2, 3 and 4 added no rule to the target calculus. + Stage 4 added observational equality (`𝒱`) and the definition of a translation as "specification only". Stage 5 added no relation. + Stage 6, part 1 added the relations of a second source calculus with the class "source". One of them is the equality `Coˡ` with local assumptions, a hypothetical equality. + Stages 3, 4 and 5 and Stage 6, part 1 added nothing to the target calculus. + Stage 7 added realisability (R25) as "specification only". It added nothing to the target calculus. +* `RULE-DIFF-LEDGER.adoc`: no entry for the target calculus. Stages 2, 3, 4, 5 and 7 and Stage 6, part 1 added no rule to it. The ledger has the difference between the target and the extension of Stage 6, part 2: 1 typing rule (`t-cast`), 1 term former (`cast`), 0 judgement forms, 0 type formers, and the entries of the identity family in a signature. == Answers of Stage 1 @@ -326,6 +508,35 @@ Stage 2 proved the laws of the candidate only. It did not prove that the candida | F15 | In this fragment the result of a type-level function is a base type. For a signature with a finite number of base types and of type-level functions, a finite number of states for each newtype is then enough (DC-4.1). Agda did not check this sentence. A function that returns a part of its argument is outside the fragment, in the source and in the target. This development proves nothing about it. + +| F16 +| The converse of T6 is false for the row scheme, in the signature `taggedS rep`. + `Tag Char` and `Tag Unit` have no nominal coercion (`Wager.Examples.Stage5.tag-char-unit-rejected`), and they have one target type (`tag-char-unit-one-type`). They do have a representational coercion (`tag-char-unit-rep`). + The translation thus does not keep each nominal difference of the source. Agda checked this one pair of types. + +| F17 +| The example of the task, `a ~ Int`, has a type variable. The source fragment and the terms of the target have closed types only (DC-6.2). + A text search of `docs/theory` found no quantifier over types. Agda does not check this sentence. + Stage 6 is thus about each closed instance of a GADT match. The two constructors of the program have two different right sides (`b` and `b + b`), so at a closed instance at least one of the two assumptions is false. + In System FC a branch with a false assumption cannot run. This development has no proof of this sentence for its source calculus (see "Not proved in Stage 6, part 1"). + The typing of the two branches together is the part that the target cannot do. + +| F18 +| The target calculus has no hypothetical equality. A typed target term erases to a term with a simple type (`Wager.L2.Erasure.erase-typed`). If a target term has the type `A → B` and erases to the identity function, then `A` and `B` have one erased type (`identity-one-type`). + The source calculus of Stage 6 types the two branches of a GADT match with two local assumptions. This is the separation of T7, part 1. + +| F19 +| The identity type needs no new type former and no new judgement form. A family of base constants of a signature and one literal on the diagonal are enough, with one term former (`cast`) and one rule (`t-cast`) (DC-6.5, DC-6.6). + For a closed term, the family is conversion: `Id A B` has a term exactly when `DefEq A B` holds (`T7-Intro`, `T7-Canonicity`). + +| F20 +| The task text joins two reasons: "by totality and the grade". In this development they are two facts with two proofs (DC-6.7). + The behaviour of the erased program comes from totality: the evidence of a cast has a value, and the value is the literal. The proof does not use the grade: it checks with the grade `𝟙` in the rule (`TOOLCHAIN.adoc`). + The grade gives the resource count: the usage of a cast is the usage of its payload (`T7-Grade`). No theorem joins the two, because the development has no semantics that counts resources. + +| F21 +| The erasure of proofs removes the evidence of a cast. It does not remove evidence that is data. The erased type of the GADT data of part 2 has a component for the evidence (`Wager.Examples.Stage6Identity.data-holds-evidence`), and the erased type of the source data of part 1 has none. + The removal of evidence from data needs an erasure that reads the grade of a binder. In the one-point grade algebra each binder has the grade `𝟘`, so such an erasure needs a property of the algebra. This is not done. |=== == Changes to theorem statements @@ -338,10 +549,119 @@ Process note: the statement `L1-Equality` was put in `Statements.agda` after its The statements of T0, T1, T2 and T4 were put in `Statements.agda`, and committed, before their proofs. The statements of Stage 3 were put in `Statements.agda`, and committed, before their proofs. The statements of Stage 4 were put in `Statements.agda`, and committed, before their proofs. One proof was complete at that time: the lemma `nominal-defeq`, which is not a statement of Stage 4. +The statements of Stage 5 (T6) were put in `Statements.agda`, and committed, before their inhabitants in `Proofs.agda`. The proof of the first two statements is the lemma of Stage 4, so it existed before the statements. This is not the order "statement before proof" (DC-5.1). +The statement of T7, part 1 was put in `Statements.agda`, and committed, before its proof (`Wager.Local.Separation`) was written. One lemma that the proof uses was complete before the statement: `Wager.L2.Erasure.erase-typed`. +The statements of T7, part 2 were put in `Statements.agda`, and committed (`bf5122c`), before their proofs (`Wager.Identity.Soundness`) were written. The 3 modules of definitions that the statements name were written before the statements (`Family`, `Term`, `Typing`). They have no proof. +The statements of Stage 7 were put in `Statements.agda`, and committed (`75da545`), before their proofs (`Wager.Univalent.CrossCheck`) were written. The module of definitions that the statements name was written before the statements (`Wager.Univalent.Model`). It has the definition of the path `pathOf`, and no proof. == Trust base * Agda 2.8.0 with `--cubical --safe`, and `agda/cubical` v0.9 (`TOOLCHAIN.adoc`). * No `postulate`, no hole, no termination pragma, no positivity pragma. * `--guardedness` is on in each file (DC-0.2). No file uses coinduction. -* One warning is silenced, in 35 of the 64 files: `UnsupportedIndexedMatch` (DC-0.3). +* One warning is silenced, in 45 of the 79 files: `UnsupportedIndexedMatch` (DC-0.3). Of the 5 files of Stage 6, part 1, 3 have the line. Of the 6 files of Stage 6, part 2, 3 have the line. Each of the 3 files of Stage 7 has the line. For each file of stages 6 and 7 that has the line, a test without the line found the warning. + +== Draft ADR (not filed) + +This section is a draft. It is not a file in `docs/decisions`, and it has no ADR number. Nothing in it is an obligation. `docs/theory/OBLIGATIONS.adoc` is not changed, and the candidates below have no ET number. + +=== Title + +Candidate obligations from the wager experiment for coercions and roles + +=== Date + +2026-11-10 (draft) + +=== Status + +Draft, not filed. The owner decides if it is filed, and with which changes. + +=== Context + +The wager experiment asked one question: can grades, conversion-only equality and tropes replace the coercions and roles of System FC, for a small fragment (newtypes, roles, `coerce`, total type-level functions)? Its answer is in this file: W holds for the fragment with 2 additions. + +The experiment is in Cubical Agda (`verification/proofs/agda/Wager`, 79 modules, `--cubical --safe`, no `postulate`). The repository has its obligations in `docs/theory/OBLIGATIONS.adoc`, and its mechanisation tracks are in Lean 4. The experiment claims no obligation. + +Each statement below is a type in `Wager/Statements.agda` with an inhabitant in `Wager/Proofs.agda`. Each one was frozen before its proof, with the exceptions that "Changes to theorem statements" records. + +=== Decision (proposed) + +The owner reviews the candidates and decides which of them become obligations of the theory. + +[cols="1,4,3",options="header"] +|=== +| Candidate | Statement | Agda evidence and conditions + +| W-1 +| The graded calculus with pairs, sums and `case` has substitution, preservation and progress, for each grade algebra. +| `t0-substitution`, `t0-preservation`, `t0-progress`. For each signature and each term signature. + +| W-2 +| Conversion of types is equality of normal forms. +| `l1-equality`. For each signature. Compare with ET-1 to ET-3 and with the Lean track MECH-1: this candidate can be a second proof of an existing obligation and not a new one. + +| W-3 +| Roles are a grade algebra with the table `nominal · phantom = phantom`. The table of GHC (`nominal · phantom = nominal`) satisfies 14 of the 15 laws; the law `a · 0 = 0` fails, at `nominal` only. +| `t1-lawful`, `t1-ghc-other-laws`, `t1-ghc-mul-zero-fails`, `t1-ghc-fails-at-nominal-only`. + +| W-4 +| Role noninterference: a type-level function at the grade representational respects representational equality, and one at the grade phantom is constant. +| `noninterference`, `t2-representational`, `t2-phantom`. Condition: each constant and each primitive of the signature respects its declared grade (`Valid`). Without the condition the statement is false (`t2-phantom-fails-without-valid`). + +| W-5 +| The kinding of the target rejects the classic unsound program of roles. +| `t4-kinding-rejects`, `t4-not-equivalent`. + +| W-6 +| A representational coercion is an ordinary typed term of the target, in each grade algebra. Its erasure is observationally the identity. +| `coercion-is-a-term`, `t3`, `t3-first-order`. Condition: the source signature passes the role check. + +| W-7 +| Each program of the fragment has a translation that preserves types and that preserves behaviour after erasure. +| `t5-typing`, `t5-behaviour`, `t5-behaviour-first-order`. Conditions: the role check; trope states with an index (not 2 states); for typing, a grade algebra with an unrestricted grade `𝟙`. With 2 states one program has no translation (`no-two-state-translation`). + +| W-8 +| A nominal coercion becomes conversion, and no term remains. +| `t6`, `t6-conversion`, `t6-no-term`. One direction only: the converse is false for the row scheme (F16). + +| W-9 +| The limit: the target with conversion only cannot type the two branches of one GADT match in the direct way. +| `t7-separation`. For each closed instance of one program. Limits: DC-6.2, DC-6.4. + +| W-10 +| With an identity family in a signature, a local equality assumption is a variable at the grade `𝟘`, closed evidence exists exactly for convertible types, and the erasure of the proofs in casts is sound. +| `t7-assumption`, `t7-intro`, `t7-canonicity`, `t7-erasure`, `t7-grade`. Only if the owner puts the extension inside the calculus (decision 3). Limits: DC-6.5 to DC-6.8. + +| W-11 +| In a realisability model of the target types in the cubical universe, the translation of a representational coercion denotes transport along a path made with `ua`. +| `coercion-denotes-transport`, `coerce-function-is-transport`. A cross-check, not a property of the calculus. Limits: DC-7.1 to DC-7.3. +|=== + +The draft asks the owner for 4 decisions: + +. *The kinding judgement.* The experiment gives the kinding judgement a graded context (R1). Is this a change of a judgement form of `00-notation.adoc`? +. *Trope states with an index.* W-7 needs one wrapped state for each index of a state scheme. `07-tropes.adoc` has a finite set of states for a trope. Does the theory accept a state set with an index? +. *The identity family.* Is the target with an identity family (W-10) a part of the calculus? The trade of Stage 6 gives the facts for each answer. +. *The prover.* The obligations of the repository have Lean 4 tracks. Is a Cubical Agda proof accepted as evidence for an obligation, or must a candidate be proved again in Lean 4? + +=== Consequences + +*Positive.* + +* The claim "grades and conversion replace coercions and roles" gets a checked scope: a fragment, 2 additions, and the programs that show why each addition is needed. +* The role table of the theory gets a checked reason: the table of GHC is not a grade algebra. +* The boundary is explicit: a local equality assumption needs equality evidence as a term, or it is outside the calculus. + +*Negative.* + +* W-7 changes `07-tropes.adoc` (decision 2). +* W-7 holds for a whole program only in a grade algebra with an unrestricted grade `𝟙`. A linear or affine instance types the coercions and not each program of the source. +* The fragment is small: no recursion, no polymorphism in a term, one parameter for a newtype and for a type-level function. An obligation that names the fragment must name these limits. +* A second prover in the repository has a cost: a second toolchain in CI and a second trust base. + +*Neutral.* + +* The candidates are independent. The owner can take a part of the list. +* W-9 and W-10 are two answers to one question. The owner can keep W-9 as the record of the limit with or without W-10. +* Nothing in the experiment changes an existing obligation or its status.