Respect Apple's ABI for cosimulations

[shigoel]

Description:

Workaround to avoid clobbering x18 and x29 on Apple's Arm machines.

Testing:

make all ran on my M3 and a Graviton2 machine.

License:

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.

[bollu]

LGTM, I'm a little hesitant about the cost of spinning up a new process and checking the platform each time we want a GPR. I would prefer if we refactor this into a abbrev SampleM := ReaderT Config IO, where

namespace Sample
structure Config where
    isDarwin : Bool

def SampleM := ReaderT Config IO

def Config.setup : IO Config := do
    pure { isDarwin := true } /- do the process querying here-/

def SampleM.run (m : SampleM a) : IO a := do
  ReaderT.run m (← Config.setup)

end Sample

[bollu]

I volunteer myself to perform the refactor I propose as a follow up PR if you like, @shigoel :)

[shigoel]

LGTM, I'm a little hesitant about the cost of spinning up a new process and checking the platform each time we want a GPR. I would prefer if we refactor this into a abbrev SampleM := ReaderT Config IO, where

namespace Sample
structure Config where
    isDarwin : Bool

def SampleM := ReaderT Config IO

def Config.setup : IO Config := do
    pure { isDarwin := true } /- do the process querying here-/

def SampleM.run (m : SampleM a) : IO a := do
  ReaderT.run m (← Config.setup)

end Sample

@bollu Yes, fair point indeed re. the cost of GPRIndex.rand, and I'll take you up on your volunteer offer. :)

But I recommend letting these changes get stress-tested in CI for a bit to see if they helped or not (I'm optimistic that they'll fix the bogus mismatch issues, but still...). If they did, then let's do that refactoring.

Another thing to note: Config above might as well cache other things, like the machine we're running on and the platform features we need. E.g., see https://github.com/leanprover/LNSym/blob/6d1ef32d9d253b8b7667edfaa08f38ea82da2dc1/Arm/Insts/DPSFP/Crypto_four_reg.lean#L38.