[tahina-pro]

Discard unused initializer and sequence results before simplifying and floating nested lets. Eliminate droppable computations while retaining comment text and observable effects, and preserve named unused lets for the KaRaMeL backends.

Extend PulseComment to cover discarded read chains, compound initializers, and effectful results. Register OCaml extraction coverage alongside the native C/C++ regression.

Summary

Fix dead-local elimination in Custard when an expression's result is unused.
Discarding the result must happen before simplifying and floating the
expression's nested lets, so bindings used only to compute that result can
also be eliminated.

This surfaced during EverParse direct-to-C extraction: generated validators
contained unused intermediate locals and failed to compile with
-Werror=unused-variable.

Problem

Two related cases left dead bindings in the generated C:

1. Discarded commented expressions. The C printer already omits a
   droppable operand when printing a discarded Commented expression, while
   retaining the comment text. However, simplification had counted uses in
   that operand and retained the bindings producing it. For example:

   let first = a[0];
   let middle = first + 1;
   let unused = comment_gen "before" (middle + 2) "after";
   

   Once the commented value disappeared, middle was left unused.

2. Discarded compound initializers. An initializer containing nested lets
   was simplified before the enclosing binding was recognized as unused.
   Floating those lets out could leave intermediates whose only consumer was
   the initializer's discarded result. An effectful call must still execute,
   but its unused return value need not be bound to a local.

This is over-retention of dead values, not deletion of live computations.

Implementation

In src/custard/FStarC.Custard.Simplify.fst:

• Add discard_value, which propagates discarded-result handling through
  the result positions of nested lets and sequences.
• Replace droppable results with unit. For a commented expression with a
  droppable operand, retain the comment node and replace only its operand
  with unit.
• Simplify a let's continuation first, determine whether the binding is
  used, and discard an unused initializer's result before simplifying and
  floating its lets.
• Apply the same handling to the discarded first expression of a sequence.

The transformation uses the existing is_droppable predicate. Observable
effects are retained, and the existing treatment of programmer-named unused
lets for the KrmlC and KrmlRust backends is preserved.

There are no new options, attributes, or CUI-format changes, and the fix does
not depend on the separate EverParse-related Custard feature branches.

Regression coverage

Extend tests/custard/pulse/PulseComment.fst with:

• An array-read/arithmetic chain used only by a discarded commented value.
• An inlined compound initializer whose result is discarded but whose
  effectful call must remain.
• A discarded commented call result whose reference update must remain.

The program checks that both effectful calls execute. The Makefile also
checks that the new comment strings survive and registers PulseComment
for OCaml extraction/type-checking alongside its existing native C test.

Focused validation

• On the upstream compiler, the extended regression fails C++ compilation
  with unused middle, n, and __anf0 locals.
• With the fix, PulseComment compiles as C11 and C++17 with warnings treated
  as errors, and its C executable succeeds.
• OCaml extraction, compilation, and execution of PulseComment succeed.
• Existing DeadRead and CDeadLet C/C++ compilation and execution succeed.
• Existing PulseCommentEnd and PulseCommentDyn rejection checks succeed.