Keep an enum constant a contract still names - #216
Draft
nikswamy wants to merge 2 commits into
Draft
Conversation
nikswamy
force-pushed
the
nswamy/pal-pr04a-prune-enum-constants
branch
from
August 20, 2026 06:17
a701397 to
6ff7a6a
Compare
Base automatically changed from
nswamy/pal-pr03-enum-constants-in-contracts
to
main
August 24, 2026 16:28
Clang applies the integral promotions to a switch condition, so the translated condition carries the promoted integer type. An enumeration is modeled by its underlying integer type, which makes that promotion the identity, so the rvalue translation elides it. The scrutinee binding was still annotated with the promoted type, leaving the declared type and the bound value syntactically distinct. The Pulse dereference tactic compares types syntactically and rejected the binding. Annotate the binding with the enumeration's own type when the unpromoted condition is an enumeration. Other promotions remain genuine casts that the rvalue translation preserves, so their promoted type is still correct. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 981f7d3c-6a91-47ad-84d7-7aadf747123d (cherry picked from commit 588982d)
A contract is often the only place an enumerator appears by name: a switch over the same enum reaches it through case labels, which the frontend folds to integers before the pruner runs. The pruner recorded no dependency for a bare variable reference at all, so such an enumerator was dropped and the contract then failed to resolve it. Record a global-variable dependency for every name reference. Locals share the namespace, so this keeps a few declarations that are not needed -- the safe direction for a pruner, which must never drop one that is. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 981f7d3c-6a91-47ad-84d7-7aadf747123d (cherry picked from commit 3b88a43)
gebner
force-pushed
the
nswamy/pal-pr04a-prune-enum-constants
branch
from
August 24, 2026 16:28
6ff7a6a to
d0b403b
Compare
Contributor
|
!diff |
Generated F* output diffEffect of this pull request on the F* code SummaryFull diff: full diff artifact Diffdiff --git head/enum_const_in_contract/Func_color_default.fst head/enum_const_in_contract/Func_color_default.fst
new file mode 100644
index 0000000..14c2017
--- /dev/null
+++ head/enum_const_in_contract/Func_color_default.fst
@@ -0,0 +1,14 @@
+module Func_color_default
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_color_default ()
+ returns return_1 : Typedef_COLOR.ty_color
+ ensures ((Typedef_COLOR.ty_color__pred return_1 1.0R))
+ ensures
+ (with_pure
+ (return_1 = (id #UInt32.t (Int.Cast.int32_to_uint32 Global_Color_Green.var_color_green))))
+{
+ return (id #UInt32.t (Int.Cast.int32_to_uint32 1l));
+}
\ No newline at end of file
diff --git head/enum_const_in_contract/Func_color_default.fsti head/enum_const_in_contract/Func_color_default.fsti
new file mode 100644
index 0000000..e5bd150
--- /dev/null
+++ head/enum_const_in_contract/Func_color_default.fsti
@@ -0,0 +1,11 @@
+module Func_color_default
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_color_default ()
+returns return_1 : Typedef_COLOR.ty_color
+ensures ((Typedef_COLOR.ty_color__pred return_1 1.0R))
+ensures
+ (with_pure
+ (return_1 = (id #UInt32.t (Int.Cast.int32_to_uint32 Global_Color_Green.var_color_green))))
\ No newline at end of file
diff --git head/enum_const_in_contract/Func_color_is_known.fst head/enum_const_in_contract/Func_color_is_known.fst
new file mode 100644
index 0000000..15a6cac
--- /dev/null
+++ head/enum_const_in_contract/Func_color_is_known.fst
@@ -0,0 +1,41 @@
+module Func_color_is_known
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_color_is_known (var_c: Typedef_COLOR.ty_color)
+ requires ((Typedef_COLOR.ty_color__pred var_c 1.0R))
+ returns return_1 : bool
+ ensures ((Typedef_COLOR.ty_color__pred var_c 1.0R))
+ ensures
+ (with_pure
+ (return_1 =
+ (((var_c = (id #UInt32.t (Int.Cast.int32_to_uint32 Global_Color_Red.var_color_red))) ||
+ (var_c = (id #UInt32.t (Int.Cast.int32_to_uint32 Global_Color_Green.var_color_green))))
+ ||
+ (var_c = (id #UInt32.t (Int.Cast.int32_to_uint32 Global_Color_Blue.var_color_blue))))))
+{
+ let mut var_c = var_c;
+ let mut var_known : bool;
+ var_known := (int32_to_bool 0l);
+ let var___switch_scrut_0 : Typedef_COLOR.ty_color = (!var_c);
+ let mut var___switch_hit_0 : bool;
+ var___switch_hit_0 := false;
+ let mut var___switch_brk_0 : bool;
+ var___switch_brk_0 := false;
+ if (((not (!var___switch_brk_0)) &&
+ ((!var___switch_hit_0) ||
+ (((false || (var___switch_scrut_0 = (id #UInt32.t (Int.Cast.int32_to_uint32 0l)))) ||
+ (var___switch_scrut_0 = (id #UInt32.t (Int.Cast.int32_to_uint32 1l))))
+ ||
+ (var___switch_scrut_0 = (id #UInt32.t (Int.Cast.int32_to_uint32 2l))))))) {
+ var___switch_hit_0 := true;
+ var_known := (int32_to_bool 1l);
+ var___switch_brk_0 := true;
+ } else {};
+ if ((not (!var___switch_brk_0))) {
+ var___switch_hit_0 := true;
+ var___switch_brk_0 := true;
+ } else {};
+ return (!var_known);
+}
\ No newline at end of file
diff --git head/enum_const_in_contract/Func_color_is_known.fsti head/enum_const_in_contract/Func_color_is_known.fsti
new file mode 100644
index 0000000..81f3293
--- /dev/null
+++ head/enum_const_in_contract/Func_color_is_known.fsti
@@ -0,0 +1,16 @@
+module Func_color_is_known
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_color_is_known (var_c: Typedef_COLOR.ty_color)
+requires ((Typedef_COLOR.ty_color__pred var_c 1.0R))
+returns return_1 : bool
+ensures ((Typedef_COLOR.ty_color__pred var_c 1.0R))
+ensures
+ (with_pure
+ (return_1 =
+ (((var_c = (id #UInt32.t (Int.Cast.int32_to_uint32 Global_Color_Red.var_color_red))) ||
+ (var_c = (id #UInt32.t (Int.Cast.int32_to_uint32 Global_Color_Green.var_color_green))))
+ ||
+ (var_c = (id #UInt32.t (Int.Cast.int32_to_uint32 Global_Color_Blue.var_color_blue))))))
\ No newline at end of file
diff --git head/enum_const_in_contract/Global_Color_Blue.fst head/enum_const_in_contract/Global_Color_Blue.fst
new file mode 100644
index 0000000..29337f2
--- /dev/null
+++ head/enum_const_in_contract/Global_Color_Blue.fst
@@ -0,0 +1,6 @@
+module Global_Color_Blue
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+let var_color_blue : Int32.t = 2l
\ No newline at end of file
diff --git head/enum_const_in_contract/Global_Color_Green.fst head/enum_const_in_contract/Global_Color_Green.fst
new file mode 100644
index 0000000..8c8ecf7
--- /dev/null
+++ head/enum_const_in_contract/Global_Color_Green.fst
@@ -0,0 +1,6 @@
+module Global_Color_Green
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+let var_color_green : Int32.t = 1l
\ No newline at end of file
diff --git head/enum_const_in_contract/Global_Color_Red.fst head/enum_const_in_contract/Global_Color_Red.fst
new file mode 100644
index 0000000..eccb0c1
--- /dev/null
+++ head/enum_const_in_contract/Global_Color_Red.fst
@@ -0,0 +1,6 @@
+module Global_Color_Red
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+let var_color_red : Int32.t = 0l
\ No newline at end of file
diff --git head/enum_const_in_contract/TranslationErrors.fst head/enum_const_in_contract/TranslationErrors.fst
new file mode 100644
index 0000000..bf62561
--- /dev/null
+++ head/enum_const_in_contract/TranslationErrors.fst
@@ -0,0 +1 @@
+module TranslationErrors
diff --git head/enum_const_in_contract/Typedef_COLOR.fst head/enum_const_in_contract/Typedef_COLOR.fst
new file mode 100644
index 0000000..b25f661
--- /dev/null
+++ head/enum_const_in_contract/Typedef_COLOR.fst
@@ -0,0 +1,11 @@
+module Typedef_COLOR
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+unfold
+let ty_color : Type = UInt32.t
+[@@pulse_eager_unfold] let predicate ty_color__pred ([@@@mkey] this: ty_color) (p: perm) = emp
+[@@pulse_eager_unfold] let predicate ty_color__uninit_pred ([@@@mkey] this: ty_color) = emp
+instance has_zero_default_ty_color : (has_zero_default ty_color) =
+ { zero_default = (UInt32.uint_to_t 0) }
\ No newline at end of file
diff --git head/enum_const_in_contract/diagnostics.json head/enum_const_in_contract/diagnostics.json
new file mode 100644
index 0000000..9e26dfe
--- /dev/null
+++ head/enum_const_in_contract/diagnostics.json
@@ -0,0 +1 @@
+{}
\ No newline at end of file
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Part of the upstreaming of
nswamy/pal-c-project-integration(PR04a of 35 PRs) — seePR_PLAN.mdon that branch for the whole plan and the dependency graph.Base:
nswamy/pal-pr03-enum-constants-in-contracts— a stacked PR. It depends onnswamy/pal-pr03-enum-constants-in-contracts,nswamy/pal-pr19-switch-enum-scrutinee, so only the commits listed below are its own; it will be retargeted atmainonce its parents land.The pruner drops declarations that are not from the main file, and it only kept what it
could see referenced. A bare variable reference in a contract recorded nothing, so an
enumerator a contract still names was pruned away and the generated module referred to a
constant that no longer existed. The scan now records a global-variable dependency for it,
which over-approximates in the safe direction.
Commits
Testing
Verified:
make rust lib,test/check-template.sh,cargo fmt --check,clang-format --dry-run --Werror, and F* verification oftest/enum_const_in_contract,test/enum_constant_in_contract.