[saw-remote-api] [test] tests/saw/test_salsa20.py: ExpandContract should allocate pointer arguments as read-only

[WeeknightMVP]

If we change the size to 65 (or more) when verifying that s20_crypt32 meets Salsa20CryptContract...

class Salsa20EasyTest(unittest.TestCase):
    def test_salsa20(self):
        # ...
        crypt_result = llvm_verify(mod, 's20_crypt32', Salsa20CryptContract(65), lemmas=[expand_result])
        # ...

..., verification fails due to a failed override assumption:

saw-script/saw-remote-api/python$ poetry run python tests/saw/test_salsa20.py
...

⚠️  Failed to verify: lemma_Salsa20CryptContract (defined at .../saw-script/saw-remote-api/python/tests/saw/test_salsa20.py:110):
error: user error (Symbolic execution failed.
Abort due to false assumption:
  salsa20.c:182:7: error: in s20_crypt32
  All overrides failed during structural matching:
  *  Name: s20_expand32
     Location: internal
     Argument types:
     - i8*
     - i8*
     - i8*
     Return type: <void>
     Arguments:
     - concrete pointer: allocation = 15, offset = 0
     - concrete pointer: allocation = 25, offset = 0
     - concrete pointer: allocation = 24, offset = 0
     at internal
     error when loading through pointer that appeared in the override's points-to precondition(s):
     Precondition:
       Pointer: concrete pointer: allocation = 25, offset = 0
       Pointee: fresh:x0#670 : [16][8]

       Assertion made at: internal
     Failure reason:
       When reading through pointer: (25, 0x0:[64])
       in the  precondition of an override
       Tried to read something of size: 16
       And type: [16 x i8]
       Found 1 possibly matching allocation(s):
       - StackAlloc 25 0x10:[64] Mutable 16-byte-aligned salsa20.c:155:11
Stack frame s20_crypt32

Amending ExpandContract to allocate memory for pointer arguments as read-only...

class ExpandContract(Contract):
    def specification(self):
        # ...
        k_p = self.alloc(LLVMArrayType(i8, 32), read_only = True)  # <--
        n_p = self.alloc(LLVMArrayType(i8, 16), read_only = True)  # <--
        # ...

...corrects this:

...

✅  Verified: lemma_Salsa20CryptContract (defined at .../saw-script/saw-remote-api/python/tests/saw/test_salsa20.py:110)

...

[RyanGlScott]

Good catch. In fact, we already use llvm_alloc_readonly in the SAWScript proofs for salsa20, but for whatever reason, the Python version didn't take after this. This should be straightforward to fix.