Cake thunks#78

Merged

myreen merged 48 commits intomasterfrom

Oct 23, 2025

Commits on Dec 3, 2024

Start changing stateLang semantics for new thunks
myreen
committed

Commits on Dec 12, 2024

Commits on Dec 17, 2024

Added thunk app primitives to state lang. Proofs need fixing
nikos-alexandris
committed

Commits on Dec 29, 2024

Fixed proofs and minor style inconsintencies of previous commits. One proof remains cheated in `state_to_cakeProof`
nikos-alexandris
committed

Commits on Dec 30, 2024

Update `binary/pure_backendProgScript`
nikos-alexandris
committed

Commits on Jan 7, 2025

Fix force semantics and env to ns mapping
nikos-alexandris
committed

Commits on Jan 10, 2025

Changed force semantics to apply function directly instead of going through singleton env
nikos-alexandris
committed

Commits on Jan 12, 2025

Changed `measureInduct`s to `application_ind`s
nikos-alexandris
committed

Commits on Jan 15, 2025

Commits on Jan 17, 2025

Hacking during meeting
myreen
committed

Commits on Feb 14, 2025

Assert thunkLang Force doesn't produce thunks.
nikos-alexandris
committed

Commits on Apr 16, 2025

This commit comes after adding the check in the `thunkLang` semantics that
nikos-alexandris
committed

Commits on Apr 20, 2025

Proved a cheat in stateLangScript and removed `rec_env` as a duplicate of `mk_rec_env`
nikos-alexandris
committed

Commits on Apr 21, 2025

Proved remaining cheats in stateLangScript
nikos-alexandris
committed

Commits on Apr 26, 2025

Fixed `Delay_Lam` and `Let_Delay_Var` proofs
nikos-alexandris
committed

Commits on Apr 28, 2025

Commits on Apr 29, 2025

Fixed state-to-cake pass to account for the new thunk representation in
nikos-alexandris
committed

Commits on May 13, 2025

Merge remote-tracking branch 'origin/master' into cake-thunks
nikos-alexandris
committed

Commits on Aug 20, 2025

Commits on Aug 26, 2025

Commits on Aug 27, 2025

Commits on Aug 31, 2025

Fixes for HOL changes
nikos-alexandris
committed

Commits on Sep 1, 2025

Commits on Sep 17, 2025

Merge remote-tracking branch 'origin/master' into cake-thunks
nikos-alexandris
committed

Commits on Sep 25, 2025

Update for change in name of while theory
nikos-alexandris
committed

Commits on Oct 10, 2025

Fixes for `state_unthunk`
nikos-alexandris
committed

Commits on Oct 20, 2025

Commits on Oct 23, 2025