prove axiom fn in tlb.rs

[Je5s1e]

This PR removes two axiom-backed tracked helpers from ostd/specs/mm/tlb.rs by providing concrete proof implementations for them.

[rikosellic]

This looks a bit strange. The TlbModel is a tracked struct while all fields are ghost. I believe this is a verification design issue. I will look into it later.

[hiroki-chen]

This looks weird to me, why do you want to keep ghost inside tracked?

[hiroki-chen]

The idiomatic way for doing so is to define a pure function, e.g., pub open spec fn update() and then define pub axiom fn tracked_update() to lift the spec to tracked mode.

Because this proof fn does not prove anything (you just want to do some tracked operations), there is no need to define the body.

[hiroki-chen]

This looks a bit strange. The TlbModel is a tracked struct while all fields are ghost. I believe this is a verification design issue. I will look into it later.

I also left some comments.