Uart semantics and proofs (cont'd)

[dayeol]

This completes the spec & proof of the following functions (#889)

• uart_putchar
• uart_tx_full

The function has 2 while loops: at the beginning to make sure the tx FIFO is not full, and at the end to ensure the device is back to IDLE state.
For now, it has been proven with the precondition where the device state is always IDLE when we enter the function.
This makes the first loop iterate exactly once.
It makes sense in a single-threaded environment because the only way to make the device busy is via uart_putchar,
but the function waits the device to be IDLE state before it returns.
However, we could also generalize it by relaxing the precondition to be execution tr s for any state s,
and it would be pretty straightforward to prove that too -- s can be destructed, and if s is IDLE we just do the same thing, and if s is BUSY then we can prove that at some point the loop should break leaving the device in IDLE state.

[jadephilipoom]

The UART proofs look good, great work! However, I want to resolve the point about IncrementWait before merging.

[google-cla]

Thanks for your pull request. It looks like this may be your first contribution to a Google open source project (if not, look below for help). Before we can look at your pull request, you'll need to sign a Contributor License Agreement (CLA).

📝 Please visit https://cla.developers.google.com/ to sign.

Once you've signed (or fixed any issues), please reply here with @googlebot I signed it! and we'll verify it.

---

What to do if you already signed the CLA

Individual signers

• It's possible we don't have your GitHub username or you're using a different email address on your commit. Check your existing CLA data and verify that your email is set on your git commits.

Corporate signers

• Your company has a Point of Contact who decides which employees are authorized to participate. Ask your POC to be added to the group of authorized contributors. If you don't know who your Point of Contact is, direct the Google project maintainer to go/cla#troubleshoot (Public version).
• The email used to register you as an authorized contributor must be the email used for the Git commit. Check your existing CLA data and verify that your email is set on your git commits.
• The email used to register you as an authorized contributor must also be attached to your GitHub account.

ℹ️ Googlers: Go here for more info.

[dayeol]

@googlebot I signed it!

[samuelgruetter]

It seems that @jadephilipoom's as well as my requested changes have been addressed, or turned into new issues, so I'm going to merge this now, so that I can make my next PR on top of it.

[samuelgruetter]

Thanks @dayeol for dealing with all my nitpicks 😉