Upgrade to F* Universes by tahina-pro · Pull Request #244 · project-everest/everparse

tahina-pro · 2025-10-30T16:19:00Z

FStarLang/FStar#3699 makes many EverParse proofs fail. This PR, authored by @nikswamy, fixes such proofs. Thanks a lot Nik!

Some remaining admits in this PR are slated to be overwritten once EverCDDL serialization is generalized beyond deterministically encoded CBOR.

This reverts commit f71a6a0.

This reverts commit a2ad34b.

…eck? This commit gives one example of cumbersome workaround, which I have by far not replicated yet.

tahina-pro · 2025-11-20T01:23:01Z

Hi @nikswamy , @gebner and @mtzguido !
I am now catching up on F*, Karamel and Pulse.

Blocking issues

Pulse now fails to typecheck some LowParse (and EverCDDL) combinators with functional types, with an error message like "Inferred type is incompatible with annotation". I started attempting a workaround in f771f78, but I have not replicated it yet. This bug seems to have been introduced by Various optimizations to avoid re-checking terms FStarLang/pulse#502
Pulse seems to have trouble properly solving slprops of the form exists* (x: unit) . p x , see the admits I left in 744a9fa . This bug seems to have been introduced by Phase-1 matcher FStarLang/pulse#483

Can anyone please help me there? Thanks in advance!
(If you want to get started, run ADMIT=1 make -j$(nproc) -k from this branch)

Other lessons learned

Pulse now sometimes needs the user to specify the middle argument of Pulse.Lib.Trade.Util.trans, which I find annoying in the cases where there are exactly two trades and exactly one of them unifies with the first (or third) argument specified by the user. See b9d339c
I am still using "old-style" while loops; now it seems that the pure invariant for the Boolean termination argument has to be separated from other pure invariants, otherwise Pulse cannot compute a witness at the end of the loop iteration, see f174fa2
I had to add many rewrites, and a few trade transitivity lemmas where the middle argument does not unify. More generally, it seems that Pulse no longer unifies with SMT even if the choice of slprops from the context is unambiguous, see 3b97d8f. From what Nik told me, the meaning of mkey has been inverted and maybe I should annotate PulseParse and EverCBOR slprops with it.

Current status

Apart from the blocking issues above:

Pulse runs out of memory in CDDL.Pulse.Serialize.MapGroup.impl_serialize_map_zero_or_more_iterator_gen, but this function is slated to be rewritten soon, since I intend to generalize CDDL serialization to support non-deterministic CBOR, so there is no need to fix that function
I have not fixed SMT failures yet, but there seems to be a significant amount of them in ASN1* (among others)

CI: allow direct push on upgrade, temporarily schedule nightly upgrades for #244, etc.

…ik_smt_univs_2025

this will solve comments at #257 (comment) and #257 (comment)

tahina-pro · 2026-02-11T04:29:50Z

opt/advance.Makefile

@@ -1,3 +1,3 @@
 FStar_hash := origin/master
-karamel_hash := origin/master
+karamel_hash := fb36fecb552c9fb202beb38a6c5a732c3f2cd49f


7f02f85 should be reverted once ~~FStarLang/karamel#676 is solved~~ FStarLang/karamel#681 is merged

…ik_smt_univs_2025

Revert commit e27e3d7 which enabled --proof_recovery, and increase rlimits for all 43 locations that relied on it. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

nikswamy added 10 commits January 15, 2025 18:36

some fixes for upcoming F* branch nik_smt_univs_2025

7421332

merge in master

67b58f8

tweaking some proofs for univs branch

62e3056

Merge remote-tracking branch 'origin/master' into _nik_smt_univs_2025

e459d0b

upgrade to F* universes branch in progress

bc1affe

fixup CBOR.Pulse.API.Det.Common

92766b0

a proof setting tweak

362b6ba

some admits in CDDL.Pulse.Serialize.MapGroup

044e922

fix up proofs in COSE to work again with F* nik_smt_univs_2025

1a68d26

Merge remote-tracking branch 'origin/master' into _nik_smt_univs_2025

a95da9b

tahina-pro requested a review from nikswamy October 30, 2025 16:19

tahina-pro mentioned this pull request Oct 30, 2025

Support for (non-deterministic) definite-length CBOR objects #245

Merged

5 tasks

tahina-pro added 14 commits November 18, 2025 01:02

Revert "Update hashes"

ea8104c

This reverts commit f71a6a0.

Merge branch '_taramana_244' into _nik_smt_univs_2025

7670966

use the right Z3 version in VSCode

3642275

partial F*, Karamel, Pulse upgrade

a2ad34b

specify some missing universes

c4fbe39

split continuation boolean pure condition in loop invariants

f174fa2

ADMIT: Cannot properly solve exists* (x: unit)

744a9fa

ADMIT: Pulse OOM in impl_serialize_map_zero_or_more_iterator_gen

d12f324

WHY WHY WHY do I need to help Pulse with middle Trade.trans arguments?

b9d339c

various rewrites and other Pulse unification issues

3b97d8f

LowParse.Pulse rlimit

c42bf83

Revert "partial F*, Karamel, Pulse upgrade"

2a1a624

This reverts commit a2ad34b.

full F*, Karamel, Pulse upgrade

679a11e

WHY WHY WHY do Pulse functions with functional types no longer typech…

f771f78

…eck? This commit gives one example of cumbersome workaround, which I have by far not replicated yet.

tahina-pro force-pushed the _nik_smt_univs_2025 branch from adc3989 to f771f78 Compare November 20, 2025 00:58

gebner mentioned this pull request Nov 21, 2025

Cannot introduce exists over unit type FStarLang/pulse#511

Closed

WIP CDDL generalized serialization

80d3b04

do not include the generated Makefile for clean

4012667

This was referenced Feb 3, 2026

disable extraction for elaborated terms to blob attributes in the AST… FStarLang/pulse#539

Closed

#664 wrongly reorders extracted C mutually recursive types with monomorphization in the middle FStarLang/karamel#676

Closed

tahina-pro added 3 commits February 9, 2026 19:42

do not print directory when using eval $(make -s env)

b049f8a

try an alternative to FStarLang/pulse#539 by @mtzguido

5d4ba6a

pin setuptools to 81.0.0 because of pypa/setuptools#5007

3c93ba9

This was referenced Feb 10, 2026

Deep-compress elaborated term to save into attributes FStarLang/pulse#555

Merged

CI: allow direct push on upgrade, temporarily schedule nightly upgrades for #244, etc. #257

Merged

tahina-pro added a commit that referenced this pull request Feb 11, 2026

Merge pull request #257 from tahina-pro/_taramana_ci_scheduled

9d614c5

CI: allow direct push on upgrade, temporarily schedule nightly upgrades for #244, etc.

tahina-pro added 3 commits February 11, 2026 04:14

Merge branch 'master' of github.com:project-everest/everparse into _n…

7751677

…ik_smt_univs_2025

(TEMP) freeze Karamel until FStarLang/karamel#676 is fixed

7f02f85

nightly: reset scheduled branch to master

f5639d3

this will solve comments at #257 (comment) and #257 (comment)

tahina-pro commented Feb 11, 2026

View reviewed changes

dzomo and others added 8 commits February 11, 2026 22:26

Update hashes

a918832

Merge branch 'master' into _nik_smt_univs_2025

4d3fcf6

advance Pulse

31ced29

protect some Pulse keywords behind evercddl_

2808d47

COSE snapshot

56a2598

label -> evercddl_label

a76ccc2

Merge branch 'master' into _nik_smt_univs_2025

ceeb6d6

Merge branch 'master' into _nik_smt_univs_2025

57f9624

tahina-pro mentioned this pull request Feb 17, 2026

CI: add EverParse CBOR, COSE regression tests FStarLang/karamel#680

Draft

dzomo and others added 8 commits February 18, 2026 22:29

Update hashes

9d7d7eb

Update hashes

e7b4f85

Merge branch 'master' into _nik_smt_univs_2025

7069d00

Update hashes

82a8a6d

Merge branch 'master' of github.com:project-everest/everparse into _n…

f2c08fd

…ik_smt_univs_2025

Revert proof_recovery and fix rlimits

f978aa0

Revert commit e27e3d7 which enabled --proof_recovery, and increase rlimits for all 43 locations that relied on it. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

remove unnecessary files

74b5688

rlimit

c36b37b

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Upgrade to F* Universes#244

Upgrade to F* Universes#244
tahina-pro wants to merge 94 commits intomasterfrom
_nik_smt_univs_2025

tahina-pro commented Oct 30, 2025

Uh oh!

tahina-pro commented Nov 20, 2025 •

edited

Loading

Uh oh!

tahina-pro Feb 11, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

tahina-pro commented Oct 30, 2025

Uh oh!

tahina-pro commented Nov 20, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Blocking issues

Other lessons learned

Current status

Uh oh!

tahina-pro Feb 11, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

tahina-pro commented Nov 20, 2025 •

edited

Loading

tahina-pro Feb 11, 2026 •

edited

Loading