Index a trivial program

[virgil-serbanuta]

The commented rules have no tests yet. I plan to add tests and uncomment them.

The indexing configuration may change and become more complex, but this is a fairly simple thing that would probably work.

[ACassimiro]

@virgil-serbanuta just as a sanity check, I'm trying to run make build but I'm getting the following error:

> make build
$(which kompile) rust-semantics/rust.md -o .build/rust-kompiled
[Error] Internal: Could not compute least upper bound for rewrite sort.
Possible candidates: [MInt{16}, MInt{64}, MInt{8}, MInt{32}]
  while executing phase "Add sort injections"
make: *** [Makefile:32: .build/rust-kompiled/timestamp] Error 113

Is this related to my K version? Or am I missing any steps that I should do prior to building the project?

[virgil-serbanuta]

@virgil-serbanuta just as a sanity check, I'm trying to run make build but I'm getting the following error:

> make build
$(which kompile) rust-semantics/rust.md -o .build/rust-kompiled
[Error] Internal: Could not compute least upper bound for rewrite sort.
Possible candidates: [MInt{16}, MInt{64}, MInt{8}, MInt{32}]
  while executing phase "Add sort injections"
make: *** [Makefile:32: .build/rust-kompiled/timestamp] Error 113

Is this related to my K version? Or am I missing any steps that I should do prior to building the project?

My guess is that your K needs to be past this commit: runtimeverification/k@7e2efdd

I only checked version 7.1.104, which works for me.

[yanliu18]

The implementation looks fine for me.

However, it will be nice if there is a write up about the purpose of this indexing?

Besides, it will also be good to give references of why this implementation make sense, if there is a reference.
For example, is this Traits section of rust-lang reference used?

[virgil-serbanuta]

Ok, I'll try adding some documentation.