The poly_use_hint proofs from #1037 currently has the following specs:
POLY_USE_HINT_32_AARCH64_ASM_CORRECT_CODE
POLY_USE_HINT_32_AARCH64_ASM_SUBROUTINE_CORRECT_CODE
POLY_USE_HINT_32_AARCH64_ASM_SUBROUTINE_CORRECT
No other proof in mlkem-native and mldsa-native has this _CORRECT and _CORRECT_CODE split. It would be nice if we can consolidate this to follow the other proofs.
@hanno-becker outlined how this could be done in #1037 (comment).
The poly_use_hint proofs from #1037 currently has the following specs:
No other proof in mlkem-native and mldsa-native has this
_CORRECTand_CORRECT_CODEsplit. It would be nice if we can consolidate this to follow the other proofs.@hanno-becker outlined how this could be done in #1037 (comment).