Commit Graph

11 Commits

Author SHA1 Message Date
c00c8e3e85 Use different graph operations to implement construction
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-04-25 23:10:41 -07:00
4fe0d147fa Adjust 'Program' to have a graph and basic blocks
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-04-13 13:39:15 -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
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
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
3a537f54ba Add a helpful utility function
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-03-01 19:08:11 -08:00
6fe8dc2a02 Add an 'iterate' function to Utils
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-02-11 14:19:41 -08:00
2b27e397b6 Add another utility proof
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-02-11 12:45:33 -08:00
d718338759 Clean up 'Map' to hide implementation details, extract code
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-02-10 16:51:43 -08:00