Fix examples/l3-machine-code/arm/step/arm_stepLib for disjnorm

[nspin]

stateLib.spec has been broken for certain ARM instructions since https://github.com/HOL-Theorem-Prover/HOL/commit/4875b1b60d4ee6357932f6ca7e384107130d1169 was merged. This PR fixes it.

Before this PR:

$ echo 'load "arm_progLib"; arm_progLib.arm_spec_hex "e12fff1e"; (* bx lr *)' \
    | (cd examples/l3-machine-code/arm/prog && ../../../../bin/hol)

...

Proof of 

SPEC ARM_MODEL
  (cond
     (GoodMode $var$(%v2) ∧ v2w [x12; x13; x14; x15] ≠ 15w ∧
      ¬(v2w [x0; x1; x2; x3] = 15w ⇒
       v2w [x4; x5; x6; x7] = 15w ⇒
       v2w [x8; x9; x10; x11] ≠ 15w) ∧
      (word_bit 1 $var$(%v5) ⇒ word_bit 0 $var$(%v5)) ∧ aligned 2 pc) *
   arm_Architecture ARMv7_A * arm_exception NoException * arm_CPSR_J F *
   arm_CPSR_E F * arm_CPSR_T F * arm_CPSR_M $var$(%v2) *
   arm_Extensions Extension_Security F *
   arm_REG (R_mode $var$(%v2) (v2w [x12; x13; x14; x15])) $var$(%v5) *
   arm_REG RName_PC pc)
  {(pc,
    v2w
      [T; T; T; F; F; F; F; T; F; F; T; F; x0; x1; x2; x3; x4; x5; x6; x7;
       x8; x9; x10; x11; F; F; F; T; x12; x13; x14; x15])}
  (arm_Architecture ARMv7_A * arm_exception NoException * arm_CPSR_J F *
   arm_CPSR_E F * arm_CPSR_T (word_bit 0 $var$(%v5)) *
   arm_CPSR_M $var$(%v2) * arm_Extensions Extension_Security F *
   arm_REG (R_mode $var$(%v2) (v2w [x12; x13; x14; x15])) $var$(%v5) *
   arm_REG RName_PC
     (if word_bit 0 $var$(%v5) then align 1 $var$(%v5) else $var$(%v5)))

failed.
Exception-
   HOL_ERR
     {message = "first subgoal not solved by second tactic",
      origin_function = "THEN1", origin_structure = "Tactical"} raised

After this PR:

$ echo 'load "arm_progLib"; arm_progLib.arm_spec_hex "e12fff1e"; (* bx lr *)' \
    | (cd examples/l3-machine-code/arm/prog && ../../../../bin/hol)

...

val it =
   [ []
    ⊢ SPEC ARM_MODEL
        (arm_REG (R_mode mode 14w) r14 * arm_CONFIG (vfp,ARMv7_A,F,F,mode) *
         arm_PC pc *
         cond
           ((word_bit 1 r14 ⇒ word_bit 0 r14) ∧
            (aligned 2 pc ⇒
             if word_bit 0 r14 then aligned 2 (align 1 r14)
             else aligned 2 r14))) {(pc,0xE12FFF1Ew)}
        (arm_REG (R_mode mode 14w) r14 *
         arm_CONFIG (vfp,ARMv7_A,F,word_bit 0 r14,mode) *
         arm_PC (if word_bit 0 r14 then align 1 r14 else r14))]: thm list

[mn200]

Many thanks!

If you could add a regression test for this, that’d be great (it’s painful that this has lingered for 5 years!). I can do something super minimal based on your example above but if there are more test-cases that could be used, the tests would presumably be better still.

[nspin]

I'll add a selftest.exe target which covers the test cases in https://github.com/HOL-Theorem-Prover/HOL/blob/develop/examples/l3-machine-code/arm/prog/arm_tests.sml. That set of test cases already includes some that were failing due to this bug.

[mn200]

Thanks for this. I didn't realise we had (sadly, unused) tests already...

[mn200]

Thanks for your work on this!

[mn200]

Having just tried the tests in arm_tests.sml (running the harness in test.sml), I get:

val failed = ["e1810f91", "e95d7ffc", "e95d7fff"]: string list
val l =
   [[ [0w ≠ 1w, s.Architecture = ARMv7_A]
     ⊢ DecodeARM
         (v2w
            [T; T; T; F; F; F; F; T; T; F; F; F; F; F; F; T; F; F; F; F; T;
             T; T; T; T; F; F; T; F; F; F; T])
         (s with Encoding := Encoding_ARM) =
       (Store (StoreExclusive (0w,1w,1w,0w)),
        s with
        <|CurrentCondition := 14w; Encoding := Encoding_ARM; undefined := F|>)],
    [
     [v2w [T; T; T; T; T; T; T; T; T; T; T; T; T; F; F] ≠ 0w,
      s.Architecture = ARMv7_A]
     ⊢ DecodeARM
         (v2w
            [T; T; T; F; T; F; F; T; F; T; F; T; T; T; F; T; F; T; T; T; T;
             T; T; T; T; T; T; T; T; T; F; F])
         (s with Encoding := Encoding_ARM) =
       (Load
          (LoadMultipleUserRegisters
             (F,F,13w,v2w [T; T; T; T; T; T; T; T; T; T; T; T; T; F; F])),
        s with
        <|CurrentCondition := 14w; Encoding := Encoding_ARM; undefined := F|>)],
    [
     [v2w [T; T; T; T; T; T; T; T; T; T; T; T; T; T; T] ≠ 0w,
      s.Architecture = ARMv7_A]
     ⊢ DecodeARM
         (v2w
            [T; T; T; F; T; F; F; T; F; T; F; T; T; T; F; T; F; T; T; T; T;
             T; T; T; T; T; T; T; T; T; T; T])
         (s with Encoding := Encoding_ARM) =
       (Load
          (LoadMultipleUserRegisters
             (F,F,13w,v2w [T; T; T; T; T; T; T; T; T; T; T; T; T; T; T])),
        s with
        <|CurrentCondition := 14w; Encoding := Encoding_ARM; undefined := F|>)]]:
   thm list list