Re-enable the awslc test

[sauclovian-g]

Closes #2273.

[sauclovian-g]

Note: I've filed a draft here so the thing runs, but #2273 shouldn't get closed until I attend to a couple other points in there. I'll either get that done soon or file new issues... in the meantime this shouldn't be merged.

[sauclovian-g]

So, naturally, it doesn't run...

[RyanGlScott]

I wonder if this is an instance of Clang performing more optimizations with a newer compiler version. For context, this is the relevant call to llvm_verify:

  crucible_llvm_verify m "EVP_DigestUpdate"
    [sha512_block_data_order_ov]
    true
    // num=0, len=240 covers the case with one call to the block function,
    // on one block from data, and the rest of data copied in c->data
    (EVP_DigestUpdate_spec 0 240)
    (w4_unint_yices ["processBlock_Common"]);

Notice that it is treating processBlock_Common as uninterpreted. The failing proof goal says:

[04:50:05.421] Subgoal failed: EVP_DigestUpdate SHA512-common.saw:167:3: error: in llvm_points_to
Literal equality postcondition
Expected term: 
let { x@1 = Prelude.Vec 8 Prelude.Bool
      x@2 = Cryptol.TCNum 0
      x@3 = Cryptol.TCNum 128
    }
 in (cryptol:/Primitive/Keyless/Hash/SHA2/SHA384/SHAUpdate
       (Cryptol.TCNum 240)
       (Cryptol.ecCat x@2 x@3 x@1 fresh:sha512_ctx.block#56368
          (Cryptol.ecZero (Prelude.Vec 128 x@1)
             (Cryptol.PZeroSeq x@3 x@1
                (Cryptol.PZeroSeqBool (Cryptol.TCNum 8)))),
        fresh:sha512_ctx.h#56367,
        Cryptol.ecNumber x@2 (Prelude.Vec 32 Prelude.Bool)
          (Cryptol.PLiteralSeqBool (Cryptol.TCNum 32)),
        fresh:sha512_ctx.sz#56369)
       fresh:data#56370).2.2.2
Actual term:
let { x@1 = Prelude.slice Prelude.Bool 64 64 0
              fresh:sha512_ctx.sz#56369
      x@2 = Prelude.bvAdd 64 (Prelude.bvNat 64 1920) x@1
    }
 in Prelude.append 64 64 Prelude.Bool
      (Prelude.bvAdd 64
         (Prelude.slice Prelude.Bool 0 64 64 fresh:sha512_ctx.sz#56369)
         (Prelude.bvUExt 63 1
            (Prelude.ite (Prelude.Vec 1 Prelude.Bool)
               (Prelude.bvult 64 x@2 x@1)
               (Prelude.bvNat 1 1)
               (Prelude.bvNat 1 0))))
      x@2

All things considered, that is a pretty small proof goal. The actual term doesn't mention any Cryptol functions at all, but the expected term does mention the SHAUpdate function, which is transitively defined in terms of processBlock_Common. I wonder if treating processBlock_Common as uninterpreted is the cause of the error, considering that the actual term doesn't mention processBlock_Common at all. (Perhaps it would have if Clang optimized the code less—hard to say without running this myself.)

In any case, I wonder if this proof would work if we didn't treat processBlock_Common as uninterpreted.

[sauclovian-g]

I force-pushed to rebase this on the current trunk not because I think it's fixed (I haven't done anything that would fix it) but so it doesn't just sit there.