Speedup ARM_ADD_RETURN_STACK_TAC

[hanno-becker]

For some proofs in mlkem-native, specifically those introduced in pq-code-package/mlkem-native#883, I notice that ARM_ADD_RETURN_STACK_TAC takes far longer than the actual correctness proof for the body of the function. The worst one is mlkem_poly_basemul_acc_montgomery_cached_k4, which takes 2h in CI, mostly in ARM_ADD_RETURN_STACK_TAC outside of symbolic execution.

It would be nice to analyze where time is lost here, and improve it.

[hanno-becker]

One step that seems surprisingly slow is ENSURES_EXISTING_PRESERVED_TAC, and probably also ENSURES_PRESERVED_DREG_TAC. Within ENSURES_EXISTING_PRESERVED_TAC, one faces a goal of the shape

( ASSIGNS c0 ,, ASSIGNS c1 ,, ... ,,  ASSIGNS cN) s s' ==> f s = f s'

where f is a component orthogonal to all c_i. This is approached using

REWRITE_TAC[ASSIGNS_SEQ] 

which applies ASSIGNS_SEQ: |- (ASSIGNS c ,, r) = \s s'. ?y. r (write c y s) s' to generate N nested existentials for the modifications of s into s'. Somewhat surprisingly, this takes noticable time.

I am not sufficiently familiar with HOL-Light yet to proceed on my own, but it would seem that an alternative approach could be to prove something along the lines of

let ASSIGNS_ORTHOGONAL = `
        (!(s:armstate) x. (f : armstate -> 'a) (write c s x) = f s) ==>
        (!(s:armstate) s'. r s s' ==> f s' = f s) ==>
        (ASSIGNS c ,, r) s s' ==> f s' = f s
        `;;

and use that to generate N separate (non-nested) orthogonality goals for f and the c_i.

[hanno-becker]

The following helps a little. With

let SEQ_ORTHOGONAL = prove(`! s s' r0 r1 f.
        ((!(x:armstate) x'. r0 x x' ==> (f : armstate -> 'a) x' = f x) /\
        (!(x:armstate) x'. r1 x x' ==> f x' = f x)) ==>
        ( r0 ,, r1 ) s s' ==> f s' = f s
        `, REWRITE_TAC[assign; seq; FUN_EQ_THM] THEN MESON_TAC []);;

let rec SEQ_ORTHOGONAL_TAC t = 
  ((MATCH_MP_TAC SEQ_ORTHOGONAL THEN CONJ_TAC) THENL 
  [ REPEAT GEN_TAC; REPEAT GEN_TAC THEN TRY SEQ_ORTHOGONAL_TAC ]) t

one can replace, inside ENSURES_EXISTING_PRESERVED_TAC, the block

REWRITE_TAC[ASSIGNS_SEQ] THEN 
    REWRITE_TAC[ASSIGNS_THM] THEN
    REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN REPEAT GEN_TAC THEN
    DISCH_THEN(SUBST1_TAC o SYM) THEN
    CONV_TAC(LAND_CONV(DEPTH_CONV
     COMPONENT_READ_OVER_WRITE_ORTHOGONAL_CONV)) THEN
    REFL_TAC

by

SEQ_ORTHOGONAL_TAC THEN REWRITE_TAC [ASSIGNS_THM; LEFT_IMP_EXISTS_THM] THEN 
      GEN_TAC THEN DISCH_THEN(SUBST1_TAC o SYM) THEN
      CONV_TAC(LAND_CONV(DEPTH_CONV
        COMPONENT_READ_OVER_WRITE_ORTHOGONAL_CONV)) THEN
      REFL_TAC

which is seems noticably faster.

(NB: There is probably a better way to do the desired repetition of SEQ_ORTHOGONAL above?)