Add support for unsigned bit-fields in structs

[KimayaBedarkar]

Add support for unsigned bit-fields in structs

What this adds

Support for unsigned (and _Bool) bit-fields in C structs, e.g.

struct flags {
    unsigned int a : 3;      // value in [0, 8)
    unsigned int nibble : 4; // value in [0, 16)
    _Bool  ready : 1;        // 0 or 1
    int    normal;           // ordinary field, unchanged
};

Before this change PAL silently mistranslated these: the : N width was
dropped and each bit-field became a full-width, separately-addressable field.
That is wrong — C bit-fields are not addressable (&s.a is illegal) and
share storage units, so they do not fit PAL's per-field ref T + pts_to
model.

Encoding: refined machine cell + mask-on-write

Each unsigned bit-field is modeled as an ordinary scalar record slot whose
backing cell is the declared underlying machine type refined to the width:

unsigned int a : N   ==>   (v:UInt32.t{UInt32.v v < pow2 N})

(UInt8/16/64.t for the other underlying widths.)

• Reads are conversion-free: the stored value already has the bit-field's
  logical unsigned type and is used directly (via subtyping) in returns, specs,
  and arithmetic.
• Writes mask the RHS to the width — s->a = e stores
  Pulse.Lib.C.BitField.mask_uW N e — so the stored value satisfies the cell's
  < pow2 N refinement. This is exactly C unsigned modular truncation
  (e % 2^N), and the masked value's postcondition (mask == e % pow2 N) makes
  the truncation provable in user specs (_ensures(s->a == v % 8)).
• Defaults are 0 (in range for every N >= 1).

Physical bit packing / storage sharing is intentionally not modeled: each
bit-field is an independent value. This is sound because a bit-field's backing
cell is never C-address-exposed (&s->a is illegal C and never appears in valid
input).

Why this design over FStar.UInt.uint_t n

The natural alternative is to store each bit-field as the parametric,
exactly-n-bit integer FStar.UInt.uint_t n (= x:int{0 <= x < pow2 n}).
We chose the refined machine cell instead, for three reasons:

1. It is the faithful model of C. A C bit-field genuinely is an
   unsigned int (or unsigned char, ...) whose value happens to be
   range-limited. (v:UInt32.t{UInt32.v v < pow2 N}) says exactly that.
   uint_t n is a mathematical nat, a value type C has no notion of.

2. Reads are conversion-free. Because the cell already is a UInt32.t, a
   read is directly usable wherever the field's unsigned int value is expected
   — returns, specifications, and integer-promoted arithmetic — with no cast.
   With uint_t n every read site would need a uint_to_t conversion back to a
   machine type, adding proof obligations and noise to generated code.

3. Consistency with how PAL already handles unsigned overflow. PAL lowers
   unsigned +/-/* to width-selected, total library helpers
   (add_wrap/sub_wrap/mul_wrap) that keep values as machine ints and encode
   modular ("wrapping") semantics in their postconditions. The mask-on-write
   design mirrors this one-to-one: a width-selected total helper (mask_uW) that
   keeps the value a machine int and states its modular result (v % pow2 N) in
   the postcondition. uint_t n would introduce a value representation that
   nothing else in PAL uses.

Note: an earlier justification appealed to C extraction ergonomics. That
reasoning was dropped — PAL is a one-way C→Pulse transpiler with no
KaRaMeL/C-extraction path, so extraction is not a factor in this decision.

Why a refinement is still needed

There is no machine type for arbitrary widths (1, 3, 7, 31, ...); the smallest
is UInt8. A bare UInt32.t only bounds the value < pow2 32. The refinement
is what narrows a machine word down to the actual N bits, so it carries the
real invariant regardless of which storage width backs the field.

Why the mask uses rem, not logand

mask_uW truncates by modular arithmetic (UW.rem v (pow2 n)) rather than a
bitwise logand + logand_mask lemma. This is both simpler and more
consistent: the < pow2 n bound falls out of "mod by a positive" and the exact
value v % pow2 n is the rem postcondition, with no bitwise reasoning — and it
uses the same modular primitives as the add_wrap/sub_wrap/mul_wrap
overflow helpers.

Scope and rejections

• Unsigned and _Bool bit-fields are supported.
• Signed bit-fields are rejected with a diagnostic: their reads need
  sign-extension and their out-of-range writes are implementation-defined
  (C11 6.3.1.3p3), so they are not portable to bake into a verification model.
• Union bit-fields are rejected (would need the value encoding layered onto
  the union variant model).
• Anonymous / zero-width bit-fields (int : 3;, int : 0;) are padding and
  are skipped entirely — no record slot, no accessors.

What it gives us

• Correct translation of a common C idiom that was previously mistranslated.
• Reads for free (subtyping, no conversions).
• Writes that truncate with C unsigned modular semantics, provable in user-facing
  specifications (_ensures(s->nibble == v % 16)).
• An encoding that stays uniform across widths and consistent with PAL's existing
  unsigned-overflow handling, keeping the generated Pulse idiomatic.

Commits

1. ir: model unsigned bit-fields as refined machine cells (IR variant, passes,
   emit field/representation helpers).
2. frontend: parse unsigned bit-fields; reject signed/union; skip padding.
3. pulse: add Pulse.Lib.C.BitField truncation helpers (mask_u8/16/32/64).
4. emit: mask unsigned bit-field writes (C truncation on store).
5. test+docs: bitfields test + internals documentation.

[gebner]

This does not seem to work with typedefs:

#include "pal.h"
#include <stdint.h>

struct mine {
  uint16_t a : 2;
};

void should_work(struct mine *s) {
  _assert(s->a <= 4);
}

[KimayaBedarkar]

This does not seem to work with typedefs:

#include "pal.h"
#include <stdint.h>

struct mine {
  uint16_t a : 2;
};

void should_work(struct mine *s) {
  _assert(s->a <= 4);
}

Should work now