Lower a fall-through-free switch as a chain of conditionals - #234

Node.js 20 is deprecated. The following actions target Node.js 20 but are being forced to run on Node.js 24: actions/checkout@v3. For more information see: https://github.blog/changelog/2025-09-19-deprecation-of-node-20-on-github-actions-runners/

(321) * Warning 321: - Did not expect module Pulse to be already checked. - Found it in an unexpected location: /home/runner/.local/fstar/lib/fstar/pulse/pulse.checked/Pulse.fst.checked instead of _cache/Pulse.fst.checked

(321) * Warning 321: - Did not expect module Pulse.Main to be already checked. - Found it in an unexpected location: /home/runner/.local/fstar/lib/fstar/pulse/common.checked/Pulse.Main.fsti.checked instead of _cache/Pulse.Main.fsti.checked

(321) * Warning 321: - Did not expect module Pulse to be already checked. - Found it in an unexpected location: /home/runner/.local/fstar/lib/fstar/pulse/pulse.checked/Pulse.fst.checked instead of _cache/Pulse.fst.checked

(321) * Warning 321: - Did not expect module Pulse.Main to be already checked. - Found it in an unexpected location: /home/runner/.local/fstar/lib/fstar/pulse/common.checked/Pulse.Main.fsti.checked instead of _cache/Pulse.Main.fsti.checked

(321) * Warning 321: - Did not expect module Pulse to be already checked. - Found it in an unexpected location: /home/runner/.local/fstar/lib/fstar/pulse/pulse.checked/Pulse.fst.checked instead of _cache/Pulse.fst.checked

(321) * Warning 321: - Did not expect module Pulse to be already checked. - Found it in an unexpected location: /home/runner/.local/fstar/lib/fstar/pulse/pulse.checked/Pulse.fst.checked instead of _cache/Pulse.fst.checked

(321) * Warning 321: - Did not expect module Pulse.Main to be already checked. - Found it in an unexpected location: /home/runner/.local/fstar/lib/fstar/pulse/common.checked/Pulse.Main.fsti.checked instead of _cache/Pulse.Main.fsti.checked

(321) * Warning 321: - Did not expect module Pulse.Main to be already checked. - Found it in an unexpected location: /home/runner/.local/fstar/lib/fstar/pulse/common.checked/Pulse.Main.fsti.checked instead of _cache/Pulse.Main.fsti.checked

(321) * Warning 321: - Did not expect module Pulse to be already checked. - Found it in an unexpected location: /home/runner/.local/fstar/lib/fstar/pulse/pulse.checked/Pulse.fst.checked instead of _cache/Pulse.fst.checked

(321) * Warning 321: - Did not expect module Pulse.Main to be already checked. - Found it in an unexpected location: /home/runner/.local/fstar/lib/fstar/pulse/common.checked/Pulse.Main.fsti.checked instead of _cache/Pulse.Main.fsti.checked

(288) * Warning 288 at Pulse.Lib.C.Array.fst(220,4-220,13): - Pulse.Lib.Array.Core.mask_free is deprecated - Array.mask_free is unsound; only use for model implementations - See also Pulse.Lib.C.Array.fst(220,2-220,15)

(288) * Warning 288 at Pulse.Lib.C.Array.fst(220,4-220,13): - Pulse.Lib.Array.Core.mask_free is deprecated - Array.mask_free is unsound; only use for model implementations - See also Pulse.Lib.C.Array.fst(220,2-220,15)

(288) * Warning 288 at Pulse.Lib.C.Array.fst(203,12-203,22): - Pulse.Lib.Array.Core.mask_alloc is deprecated - Array.mask_alloc is unsound; only use for model implementations - See also Pulse.Lib.C.Array.fst(202,1-210,3)

(288) * Warning 288 at Pulse.Lib.C.Array.fst(203,12-203,22): - Pulse.Lib.Array.Core.mask_alloc is deprecated - Array.mask_alloc is unsound; only use for model implementations - See also Pulse.Lib.C.Array.fst(202,1-210,3)

(288) * Warning 288 at Pulse.Lib.C.Casts.fst(25,4-25,19): - FStar.Int.Cast.uint64_to_int64 is deprecated - with care; in C the result is implementation-defined when not representable - See also /home/runner/.local/fstar/lib/fstar/ulib/FStar.Int.Cast.fst(170,4-170,19)

(288) * Warning 288 at Pulse.Lib.C.Casts.fst(25,4-25,19): - FStar.Int.Cast.uint64_to_int64 is deprecated - with care; in C the result is implementation-defined when not representable - See also /home/runner/.local/fstar/lib/fstar/ulib/FStar.Int.Cast.fst(170,4-170,19)

(288) * Warning 288 at Pulse.Lib.C.Casts.fst(21,4-21,19): - FStar.Int.Cast.uint32_to_int32 is deprecated - with care; in C the result is implementation-defined when not representable - See also /home/runner/.local/fstar/lib/fstar/ulib/FStar.Int.Cast.fst(155,4-155,19)

(288) * Warning 288 at Pulse.Lib.C.Casts.fst(21,4-21,19): - FStar.Int.Cast.uint32_to_int32 is deprecated - with care; in C the result is implementation-defined when not representable - See also /home/runner/.local/fstar/lib/fstar/ulib/FStar.Int.Cast.fst(155,4-155,19)

(321) * Warning 321: - Did not expect module Pulse to be already checked. - Found it in an unexpected location: /home/runner/.local/fstar/lib/fstar/pulse/pulse.checked/Pulse.fst.checked instead of _cache/Pulse.fst.checked