qd: emit the same_kind assert_norm in the Pulse sum/dsum readers

[gebner]

Problem

331a41199 added the kind equation

assert_norm (LP.parse_sum_kind (LP.get_parser_kind <tn>_repr_parser) <n>_sum parse_<n>_cases == <n>_parser_kind);

to the Pulse payload accessors, the Unknown payload accessor and write_<n>, for both sums and dsums. The copyful readers read_<n>_sum were missed, and they need it for exactly the same reason.

After FStarLang/FStar#4519 ("Encode prop like bool, with boxing to SMT Bool") a prop-valued definition only gets the formula equation Valid (f x) <==> body; the term equation is no longer emitted, since the new encoding is extensional. So a goal of the form

pts_to_parsed_prop p1 w v == pts_to_parsed_prop p2 w v

can no longer be discharged by unfolding both sides, and has to go through SMT congruence on the parser arguments instead — which is what the assert_norm enables.

Without it, read_<n>_sum can fail its own ascription:

* Error 19 at TLS13.Wire.Generated.Handshake.fst(303,2-304,208):
  - Subtyping check failed
  - Expected type
      LowParse.PulseParse.Base.copyful_parse (...) handshake_parser (...)
    got type
      LowParse.PulseParse.Base.copyful_parse (...)
        (LowParse.Spec.Sum.parse_sum handshake_sum
            LowParse.Spec.Int.parse_u8
            parse_handshake_cases)
        (...)
  - The SMT solver could not prove the query.
  - Failed to prove:
      LowParse.PulseParse.Base.pts_to_parsed_prop
        (LowParse.Spec.Sum.parse_sum handshake_sum LowParse.Spec.Int.parse_u8 parse_handshake_cases) w v
      ==
      LowParse.PulseParse.Base.pts_to_parsed_prop handshake_parser w v

Note this is The SMT solver could not prove the query (all-incomplete), not a timeout — raising the rlimit does not help.

Fix

same_kind is already in scope at both reader emission sites, so this is a two-line change mirroring what write_<n> already does: insert %s right after the =\n of the ascription and pass same_kind as the 11th argument, in emit_copyful_owned_sum and emit_copyful_owned_dsum.

Why the existing tests did not catch it

They do not reproduce the failure: for the small sums in unittests.rfc, Z3 still finds the congruence unaided. It shows up on the 9-case Handshake sum and the Extension* sums of the TLS 1.3 RFC in project-everest/mitls-fstar, where all six affected modules verify again with this change.

I did not add a regression test here because reproducing it needs a sum large enough to defeat Z3's unaided search, which would be a fairly brittle test. Happy to add one if you'd prefer.

Validation

• make -C share/everparse/tests/qd — 385 modules verify, 0 F* errors, no change in behaviour.
• The only output change is the new assert_norm line in the seven modules that have a copyful owned sum or dsum reader: T6, T6le, T16_x, T17, T18, T22, and for the dsum path T7. For example, in T7.fst:

 let read_t7_sum
   : PPB.copyful_parse (PPS.vmatch_dsum t7_sum t7_low t7_tag_of_low t7_mid_of_tag t7_casevmatch) t7_parser (PPS.dsum_conv t7_sum t7_mid_of_tag t7_conv_of_tag) =
+  assert_norm (LP.parse_dsum_kind (LP.get_parser_kind tag2_repr_parser) t7_sum parse_t7_cases (LP.get_parser_kind t2_parser) == t7_parser_kind);
   PPS.copyful_parse_dsum t7_sum read_maybe_tag2_key tag2_repr_jumper parse_t7_cases

• Downstream, make verify, make verify-samples and the full test suite of project-everest/mitls-fstar are clean at EverParse ac626cd45.