[aeneas] Preserve variable names

[zhassan-aws]

In #3514, the LLBC does not keep the variable names from the Rust source. This PR extracts the names of variables from MIR and carries it over to the LLBC.

For instance, for tests/expected/llbc/basic1 which has the following Rust:

fn select(s: bool, x: i32, y: i32) -> i32 {
    if s { x } else { y }
}

without this PR, running Aeneas on the output LLBC produces:

def select (b : Bool) (i : I32) (i1 : I32) : Result I32 :=
  if b
  then Result.ok i
  else Result.ok i1

but with this PR, it produces:

def select (s : Bool) (x : I32) (y : I32) : Result I32 :=
  if s
  then Result.ok x
  else Result.ok y

This should not be merged before #3514, so keeping it as a draft for the time being.

The actual diff on top of #3514 can be viewed here: zhassan-aws/kani@llbc4...zhassan-aws:kani:llbc-names

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