|
|
d96eb97b69
|
Switch maps (and consequently most of the code) to using instances
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2025-01-04 21:16:22 -08:00 |
|
|
|
d90b544436
|
Use binary operator for decidable equality consistently
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2025-01-04 19:08:28 -08:00 |
|
|
|
b0488c9cc6
|
Make 'IsDecidable' into a record to aid instance search
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2025-01-04 18:58:56 -08:00 |
|
|
|
4da9b6d3cd
|
Fuse 'FiniteMap' and 'FiniteValueMap'
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-12-31 19:21:23 -08:00 |
|
|
|
f4392b32c0
|
Finish the last proof obligation for trace walking
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-09 19:01:36 -07:00 |
|
|
|
a22c0c9252
|
Prove a property of multi-key lookup
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-09 17:56:26 -07:00 |
|
|
|
cfa3375de5
|
Expose more functions from FiniteMap
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-08 20:50:05 -07:00 |
|
|
|
6b116ed960
|
Forward some map function to Finite{,Value}Map
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-08 20:34:15 -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 |
|
|
|
040c13caba
|
Use instances to simplify printing code
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-11 12:50:05 -07:00 |
|
|
|
8964ba59a1
|
Prove monotonicity of eval
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-10 20:29:05 -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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
ec2b1ec3ba
|
Format FiniteMap a little bit better
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-02 14:54:44 -08:00 |
|
|
|
0774946211
|
Expose decidability from Map modules
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-01 23:27:49 -08:00 |
|
|
|
6e26aa1580
|
Add a bundle to FiniteMap
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-02-11 21:02:43 -08:00 |
|
|
|
ec31333e9a
|
Add a 'Finite Map' lattice
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-02-11 14:19:41 -08:00 |
|
