forked from leanprover-community/iris-lean
-
Notifications
You must be signed in to change notification settings - Fork 5
Formalisation of the statements of all Bluebell rules except Program WP rules and Derived WP rules #268
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Open
Coda-Coda
wants to merge
167
commits into
master
Choose a base branch
from
Dan/measureMySpace-2
base: master
Could not load branches
Branch not found: {{ refName }}
Loading
Could not load tags
Nothing to show
Loading
Are you sure you want to change the base?
Some commits from the old base branch may be removed from the timeline,
and old review comments may become outdated.
Open
Formalisation of the statements of all Bluebell rules except Program WP rules and Derived WP rules #268
Changes from all commits
Commits
Show all changes
167 commits
Select commit
Hold shift + click to select a range
724664e
Defining MeasureOnSpace as the new notion of resource
shinghinho 969deaf
bump the manifest
Ferinko 9f22758
do not rely on autoImplicit = true
Ferinko 91b7e85
- Put stuff into appropriate namespaces.
Ferinko 5bdc92d
- Define PSpace to be a Subtype rather than a Sub_SET_. This allows u…
Ferinko 5673c5b
Merge pull request #261 from Verified-zkEVM/Ferinko/measureMySpaceR
shinghinho ebc2142
Proved identity and commutativity law for independent product
shinghinho 8bb6d36
Proved identity and commutativity law for independentProduct
shinghinho d704946
Unfinished proof of associativity
shinghinho 14a0e8d
Associativity proof
shinghinho 4a11d3d
Associativity proof
shinghinho 8a51c59
PSp as a discrete camera
shinghinho ac2290e
Discrete CMRA: product space and subspace
shinghinho 00a6319
measurable
shinghinho 30b0daa
prove 'le_preserves_measure'
Ferinko 0f46a64
PSp as an RA
shinghinho f8df189
Compatibility
shinghinho 9eaeb56
PSpace map
shinghinho 10f78db
Lemmas for MeasurableSpace.map
shinghinho 5a58b14
hone proof
shinghinho 5d57263
Introduced independent product notation + cleanup
Julek d3fb0e1
Lemma for PSpace.compatiblePerm
shinghinho 53c70ae
Merged and added MeasurableSpace.map_preserves_sum
shinghinho 0b85cc9
Bluebell RA
shinghinho 822420f
Generalizing Var and Val
shinghinho a2e7ca5
Partial implementation of quotient DiscreteCMRA
shinghinho 5807ece
Complete proof for OrderedUnitalResourceAlgebrar.quotient
shinghinho 78a8bcb
Complete proof for OrderedUnitalResourceAlgebrar.quotient
shinghinho 5248eac
Assertion
shinghinho 338523b
Merge branch 'measureMySpace' of https://github.com/Verified-zkEVM/ir…
shinghinho a706f9f
Restructure
shinghinho 62391cf
UCMRA instance from OrderedUnitalResourceAlgebra
shinghinho 1cac5f7
Assertion
shinghinho 110e77f
Using new definitions
shinghinho 3e80553
Implement PSp.le_of_mul_left
shinghinho 5fb1cc1
Counterexample for DistInj
shinghinho 1dfcffa
Create subtype for valid elements
shinghinho 6851791
Joint conditioning modality and BI instance
shinghinho 0990c98
Refactor to use BI notations
shinghinho 18bc52a
Refined JC def + started proof of C-TRUE
Julek 7a782eb
Partial proof of C_true
shinghinho 7d9a596
C_True attempt
shinghinho 2988946
Proved C_True
shinghinho 1c60159
Proof of sep_affine
shinghinho 1490763
MeasureOnSpace refactor
shinghinho 9b6f318
PSp.top
shinghinho 31eae38
Added Affine instance for bProp
Julek 7fd37cb
Merge branch 'master' into measureMySpace
Julek 9ad3938
Introduced all classes for bProp
Julek d6a2380
Reorganizing sections
shinghinho 6434b1d
Hoare triples
shinghinho 26f936d
C_False and C_Transf rule statements formalised
Julek 52a8728
Merge branch 'measureMySpace' of github.com:Verified-zkEVM/iris-lean …
Julek ccb8c5b
Proof of `C_Transf`
Coda-Coda e56d262
Sure_Str_Convex statement formalised
Coda-Coda cae3fb6
Begin to formalise C-WP-SWAP statement
Coda-Coda dbb0d38
Formalise statement of alternate new variant of C-WP-SWAP statement
Coda-Coda d30ce7c
Revert to the previous definition of `jointConditioning`
Coda-Coda bf820ad
Fix `C_True` lemma
Coda-Coda 5660bdb
Fix `C_Transf` lemma
Coda-Coda 548cb96
Prove `C_False`
Coda-Coda 6bec09b
`And_To_Star` statement formalised, as well as `irrel` and `idx`
Coda-Coda c643ac1
Prove `And_To_Star`
Coda-Coda 9e0fee1
Improve definition of `wp`
Coda-Coda eab4f71
`WP_Conj` statement formalised
Coda-Coda 9124058
Simplify `WP_Conj` statement
Coda-Coda 0c3f509
Fix error in `WP_Conj` statement
Coda-Coda 8c6da78
Revert "Improve definition of `wp`"
Coda-Coda 13f484e
Improve definition of `wp` (second attempt)
Coda-Coda e8d3fe1
Rewrite `t₁_plus_t₂` in `WP_Conj` due to improved `wp`
Coda-Coda a467b16
FIx `WP_Swap` draft, due to changes to `wp`
Coda-Coda 1a07f37
Fix statement of `WP_Conj`
Coda-Coda 47bacaf
Fix typo-related mistake
Coda-Coda ff0a383
Add `dom` as abbreviation for `hyperTermReferences`
Coda-Coda f4697c7
Define product between PMFs with `sorry` for the required proof
Coda-Coda 5071dae
Finish defining product between PMFs (add required proof)
Coda-Coda bc622ae
Formalise statement of PROD-SPLIT
Coda-Coda 192c24e
Begin to formalise SURE-AND-STAR statement
Coda-Coda 5a2a870
Formalise statements of some derived rules
Coda-Coda 1d52e2c
Move `Dist_Fun` below Sure_Sub
Coda-Coda 8a33469
Add side-condition for WP_Conj rule
Coda-Coda f877ac3
Remove comment
Coda-Coda 5142a5b
Add headings for all Bluebell rules
Coda-Coda aba28bb
Move And_To_Star lemmas+spec+proof under heading
Coda-Coda 4fd1a97
Move Dist_Inj spec+proof under heading
Coda-Coda 21700c9
Move Sure_Merge spec under heading
Coda-Coda 4278ade
Move Sure_And_Star spec under heading
Coda-Coda 7d48414
Move Prod_Split spec under heading
Coda-Coda dbf0af3
Move C_True spec+proof under heading
Coda-Coda 78116b4
Move C_False spec+proof under heading
Coda-Coda 376b432
Add TODO comments
Coda-Coda 768284f
Add TODO comments
Coda-Coda 470e677
Move C_Transf spec+proof under heading
Coda-Coda 489a8c2
Move Sure_Str_Convex spec under heading
Coda-Coda 94dd805
Add TODO comments
Coda-Coda 0a1fe6e
Move WP_Cons spec+proof under heading
Coda-Coda 12619ea
Move WP_Frame spec+proof under heading
Coda-Coda 9f07704
Add TODO comment
Coda-Coda 49a8e38
Move WP_Conj spec under heading
Coda-Coda 15bd88d
Move C_WP_Swap spec under heading
Coda-Coda 30b1af6
Add TODO comments
Coda-Coda b7a2265
Move Sure_Dirac spec+proof under heading
Coda-Coda 0e7e1b4
Move Sure_Eq_Inj spec under heading
Coda-Coda 0343a56
Move Sure_Sub spec under heading
Coda-Coda 1d94ebd
Move Dist_Fun spec under heading
Coda-Coda 6acb066
Move Dist_Dup spec under heading
Coda-Coda 641153b
Move Dist_Supp spec under heading
Coda-Coda 8cba470
Move Prod_Unsplit spec under heading
Coda-Coda cb746d1
Move Sure_Convex spec under heading
Coda-Coda 614f1d3
Move Dist_Convex spec under heading
Coda-Coda b22e078
Add TODO comments
Coda-Coda e65175f
Move C_Extract spec under heading
Coda-Coda ec8c0c9
Add TODO comments
Coda-Coda d7f4aba
Move Properties section above BluebellRules section
Coda-Coda da9f6e5
Delete leftover comments from before restructure
Coda-Coda 898de9b
Add DONE comments
Coda-Coda 985521c
Copy in the already done specs from previous Bluebell formalisation (…
Coda-Coda 8c22c2b
Improve comment
Coda-Coda 7049783
Name all rules `theorem` rather than `lemma`
Coda-Coda 9d52667
Definition of relational lifting
Julek d781202
formalised RL-Cons, RL-Conver, RL-Merge, fix to DIST-Fun and SURE-Sbu
Julek 84ab0c1
Typeclass instances clean up
Coda-Coda d3aabc5
Improve heading
Coda-Coda a9fdf64
Remove completed TODO
Coda-Coda 196c90b
Prove C-CONS and RL-CONS rules
Coda-Coda 108c59f
Update comments indicating formalisation progress
Coda-Coda aaec996
Formalise statement of C-FRAME, C-UNIT-L, C-UNIT-R, C-AND, C-FOR-ALL,…
Coda-Coda e450e9d
Formalise PMF bind and return as `PMF.bind` and `PMF.pure` by importi…
Coda-Coda aa4899c
Formalise statement of C-ASSOC and C-UNASSOC
Coda-Coda 6441799
Include a `LawfulMonad PMF` instance by importing ProbabilityMassFunc…
Coda-Coda 4306d31
Show PMF satisfyies monadic laws as written in the paper
Coda-Coda b1b746f
Fix issue with `⌈E⟨i⟩⌉` notation for `almostSurely`
Coda-Coda 31450c5
Improve precedence for `𝒞⟨μ⟩v; K` notation
Coda-Coda fbdad29
Fix `C_WP_Swap'`
Coda-Coda 1868f91
Fix unused variable warning
Coda-Coda fdbb9bd
Prove SURE-EQ-INJ and SURE-CONVEX
Coda-Coda d232818
Comment out `#check`
Coda-Coda c797dc0
Fill `sorry` in `t₁_plus_t₂` by showing that the case is unreachable
Coda-Coda 48f2269
Formalise the statement of C-SKOLEM
Coda-Coda 163404e
Formalise the statement of WP-NEST
Coda-Coda 9210182
Use if/then/else instead of matches in WP-NEST
Coda-Coda 44ee3b2
Tweak variable name to match order in the type `I × Var`
Coda-Coda bb7813c
Formalise statements of C-SWAP and RL-EQ-DIST
Coda-Coda 59683b5
Formalise statement of C-FUSE and define `fusion`
Coda-Coda 80c5809
Fill `sorry` in `fusion` definition showing `HasSum f 1`
Coda-Coda 5691f19
Formalise statement of C-SURE-PROJ, except proof of `HasSum (fun a =>…
Coda-Coda f51c39f
Add proof of `HasSum ... 1` to C-SURE-PROJ spec
Coda-Coda db56e0a
Update TODO to reflect that `prf` is done
Coda-Coda 3f1e6ce
Fill `sorry`s in statements of SURE-SUB and DIST-FUN showing `HasSum …
Coda-Coda 1967521
Replace inline proofs of `HasSum ... 1` with `prf` and `let prf : Has…
Coda-Coda 57b871b
Remove unnecessary comments
Coda-Coda 0aaa6e1
Formalise statement of C-SURE-PROJ-MANY
Coda-Coda b389fe1
Formalise statement of C-DIST-PROJ
Coda-Coda 37af47a
Added definition of pabs and fixed Sure_And_Star accordingly
Julek 3fbf774
WIP on formalising statement of RL-SURE-MERGE
Coda-Coda 7d5811a
Formalised the RL-Unary and Coupling rules + refined RL-Sure-Merge
Julek 8bbf49a
Update comments to indicate what was finished in the previous commit
Coda-Coda 136c9a3
Make TODO comments consistent
Coda-Coda 21b2889
Minor cleanup
Coda-Coda 309e5b4
Prove C-UNIT-L, C-UNASSOC, C-SKOLEM, C-FOR-ALL, C-PURE, SURE-SUB, DIS…
Coda-Coda d7975ef
Add note on the use of generative AI in the `BluebellRules` section
Coda-Coda 1926d5c
Add "🤖:" to comments that were added by generative AI in the `Bluebel…
Coda-Coda 965589e
Add TODO comment
Coda-Coda dc3420f
Fix incorrect names of rules in TODO comments (found by Alex's AI)
Coda-Coda c2fe4dc
Fix mistake in formalisation of statement of RL-EQ-DIST rule (found b…
Coda-Coda b6dbf4a
Remove requirement for `A` and `X` to be `Inhabited` in RL-EQ-DIST
Coda-Coda 556153c
Remove unnecessary parameters in RL-EQ-DIST (found by Alex's AI)
Coda-Coda File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,11 +1,3 @@ | ||
| import Bluebell.Algebra.CMRA | ||
| import Bluebell.Algebra.HyperAssertion | ||
| import Bluebell.Algebra.PSpPm | ||
| import Bluebell.Algebra.Permission | ||
| import Bluebell.Algebra.Probability | ||
| import Bluebell.Core.Indexed | ||
| import Bluebell.Logic.JointCondition | ||
| import Bluebell.Logic.Ownership | ||
| import Bluebell.Logic.WeakestPre | ||
| import Bluebell.ProbabilityTheory.Coupling | ||
| import Bluebell.ProbabilityTheory.IndepProduct | ||
| import Bluebell.Assertion | ||
| import Bluebell.OURA | ||
| import Bluebell.MeasureOnSpace | ||
This file was deleted.
Oops, something went wrong.
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Uh oh!
There was an error while loading. Please reload this page.