Advance F* to 52f17ab8fd and fix prop-encoding fallout

[gebner]

Bumps FStar_hash to 52f17ab8fdea379708a659a1b02c8f8b47f877fa, which picks up FStarLang/FStar#4519 ("Encode prop like bool, with boxing to SMT Bool", merged as ec19167e57) and its follow-up FStarLang/FStar#4522.

The relevant change is that a prop-valued definition is now encoded with a formula equation Valid (f x) <==> body instead of a term equation f x == body; the term equation is no longer emitted at all, since the new encoding of prop is extensional.

Two consequences for EverParse:

• src/qd: the generated Pulse accessors and safe writers were relying on the dropped term equation. Goals of the shape

  pts_to_parsed_prop p1 w v == pts_to_parsed_prop p2 w v
  l2r_safe_writer_postcond conv s1 y v' sz err
  == l2r_safe_writer_postcond conv s2 y v' sz err

  used to be discharged by unfolding both sides to their bodies. Both predicates are prop-valued, so that equation is gone, and the goals now have to go through SMT congruence instead -- which needs the parser (resp. serializer) arguments to be provably equal, not just unfoldable to equal bodies. The generated code was missing the

  assert_norm (parse_[d]sum_kind ... == _parser_kind)

  that establishes exactly that; the LowStar path already emitted it via [same_kind], the Pulse path did not. Emit it in the Pulse payload accessors, the Unknown payload accessor, and write_ for both sums and dsums. Fixes T7, T15_body and T40 in the quackyducky unit tests.

• CBOR.Pulse.Raw.Format.Serialize.map_peek: borderline query that now times out at the default rlimit, so bump it to 32. The identical proof in CBOR.Pulse.Raw.Read still goes through unchanged; no spec changes.

Validated with a clean F* rebuild followed by make and make test.