|
|
85fdf544b9
|
Translate informal proof of (node) transitivity into formal one.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-04-08 20:57:08 -07:00 |
|
|
|
4f14a7b765
|
Successfully prove that monotonic updates preserve existing indices
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-04-08 00:24:52 -07:00 |
|
|
|
bc5b4b7d9e
|
Explicitly write metas for missing functions
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-04-08 00:16:10 -07:00 |
|
|
|
520b2b514c
|
Clear up vector reindexing
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-04-08 00:12:50 -07:00 |
|
|
|
f7ac22257e
|
Beat head against the vector-cast wall.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-04-07 23:44:35 -07:00 |
|
|
|
b72ad070ba
|
Try using index-based comparisons
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-04-07 23:18:46 -07:00 |
|
|
|
195537fe15
|
Implement graph construction using <*>, map, and update.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-04-07 20:26:38 -07:00 |
|
|
|
d4b0796715
|
Intermediate commit. Switch to *-based definition of <=.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-04-07 19:51:59 -07:00 |
|
|
|
b505063771
|
Start working on proofs of Graph-related things
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-04-04 20:34:28 -07:00 |
|
|
|
844c99336a
|
Intermediate commit: add while loops and start trying to formalize them.
|
2024-04-03 22:31:23 -07:00 |
|
|
|
5d56a7ce2d
|
Fix comments in Forward.agda
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-23 12:09:14 -07:00 |
|
|
|
2e096bd64e
|
Extract common parts of forward analyses into Forward.agda
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-22 17:50:29 -07:00 |
|
|
|
1a7b2a1736
|
Adjust behavior of eval to not require constant 'k in vars' threading
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-22 17:15:40 -07:00 |
|
|
|
f0da9a9020
|
Move more code out of Sign and into Main
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-11 13:07:42 -07:00 |
|
|
|
040c13caba
|
Use instances to simplify printing code
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-11 12:50:05 -07:00 |
|
|
|
56da61b339
|
Delete the bundles since they did not turn out all that useful
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-11 12:14:53 -07:00 |
|
|
|
3e88a64ed9
|
Add some debugging code to sign analysis to print the results
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-10 22:23:45 -07:00 |
|
|
|
8a85c4497c
|
Prove that evaluation is monotonic and complete sign analysis
Other than monotonicity of plus and minus, god damn it.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-10 21:25:46 -07:00 |
|
|
|
8964ba59a1
|
Prove monotonicity of eval
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-10 20:29:05 -07:00 |
|
|
|
96f3ceaeb2
|
Use the previous join function directly in GeneralizedUpdate
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-10 19:41:02 -07:00 |
|
|
|
237250cf72
|
Stop using modules in 'Sign' analysis
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-10 19:23:48 -07:00 |
|
|
|
8515491327
|
Simplify AboveBelow a bit to avoid nested modules
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-10 18:43:10 -07:00 |
|
|
|
3305de4710
|
Remove need for explicit arguments in map derivatives
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-10 18:35:29 -07:00 |
|
|
|
f21ebdcf46
|
Start working on the evaluation operation.
Proving monotonicity is the main hurdle here.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-10 18:13:01 -07:00 |
|
|
|
0705df708e
|
Prove that variables in a program all come from the program's code
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-10 16:41:21 -07:00 |
|
|
|
51accb6438
|
Define 'minus', too -- with no monotonicity proof.
I'm still thinking about how this should be achieved most easily.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-10 16:40:49 -07:00 |
|
|
|
afe5bac2dc
|
Commit result of (unsuccessfully) trying to prove monotonicity of plus.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-10 13:54:19 -07:00 |
|
|
|
fdc40632bf
|
Add a way to retrieve the code for a particular state
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-09 23:09:50 -08:00 |
|
|
|
f84a1c923c
|
Prove that the 'join' transformation is monotonic
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-09 23:06:47 -08:00 |
|
|
|
1b1b80465c
|
Use named modules to avoid having to pass redundant parameters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-09 21:46:15 -08:00 |
|
|
|
56c72e1388
|
Delete unused homomorphism proof that was broken by an Agda update.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-09 14:07:56 -08:00 |
|
|
|
0c30f8be48
|
Start on sign analysis (mostly just imports)
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-09 14:00:10 -08:00 |
|
|
|
75f981cb75
|
Define simple sequential-only programs
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-09 13:59:48 -08:00 |
|
|
|
ca99e18184
|
Tweak exports from finite value bundle to avoid (some) redundant arguments
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-09 13:59:22 -08:00 |
|
|
|
702cf2c298
|
Expose more functionaity from the set lattice
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-09 13:58:40 -08:00 |
|
|
|
0c088ca2ae
|
Prove multi-key access monotonicity in finite maps
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-09 13:58:07 -08:00 |
|
|
|
bc138d87f0
|
Prove things about key-based access in map
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-09 13:57:29 -08:00 |
|
|
|
311ed75186
|
Expose more helpers from 'Map'
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-09 13:57:02 -08:00 |
|
|
|
1ccc6f08e5
|
Add more properties of uniqueness
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-09 13:54:01 -08:00 |
|
|
|
332b7616cf
|
Prove that foldr is monotonic when input lists are pairwise monotonic
This should help prove that "join" is monotonic
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-07 21:53:45 -08:00 |
|
|
|
7905d106e2
|
Tweak signature of 'forget' to simplify proofs
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-07 20:04:33 -08:00 |
|
|
|
34203840c8
|
Use the new provenance function to clean up some proofs
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-07 19:59:14 -08:00 |
|
|
|
48983c55b1
|
Prove exercise 4.26 from the textbook
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-06 00:35:29 -08:00 |
|
|
|
fa0282ff6f
|
Prove that the identity function is monotonic
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-06 00:35:06 -08:00 |
|
|
|
164fc3636f
|
Prove that constant functions are monotonic
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-03 17:23:57 -08:00 |
|
|
|
c932210d37
|
Re-expert monotonicity from Lattice
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-03 17:04:18 -08:00 |
|
|
|
a8d26b1c48
|
Prove that join is monotonic in both arguments
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-03 16:51:57 -08:00 |
|
|
|
2ddac38c3f
|
Update with new changes to Agda
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-03 16:44:10 -08:00 |
|
|
|
f00dabfc93
|
More cleanup to FiniteValueMap
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-02 16:23:33 -08:00 |
|
|
|
01f4e02026
|
More cleanup to FiniteValueMap
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-02 16:05:42 -08:00 |
|
