Issue 121: Proved that nat_decimal_string, nat_binary_string, and nat_hex_string are injective. Rewrote the nat to string conversion functions.

sifive / Kami

Kami - a DSL for designing Hardware in Coq, and the associated semantics and theorems for proving its correctness. Kami is inspired by Bluespec. It is actually a complete rewrite of an older version from MIT

Apache License 2.0

197 stars 11 forks source link

Issue 121: Proved that nat_decimal_string, nat_binary_string, and nat_hex_string are injective. Rewrote the nat to string conversion functions. #122

Closed llee454 closed 4 years ago

vmurali commented 4 years ago

Shouldn't we merge natToHexStr and nat_hex_string - they are literally the same functions.

llee454 commented 4 years ago

[X] update the pmp register names so that they use natToHexStr
[x] move natToHexStr to a new file in Kami/Lib.
[x] remove dependency on Coq.Logic.Classical_Pred_Type by proving inv_inj constructively.
[x] test the natToHexStr function on a large nat and compare execution time against original function

llee454 commented 4 years ago

There was no observable slowdown when converting large nats to strings using the new natToHexStr function. The following is an example time result:

  1 Definition speedTest := ltac:(time reflexivity) : natToHexStr 1000000 = "F4240". (* old 7.938 sec *)         
  2 Definition speedTest2 := ltac:(time reflexivity) : test 1000000 = "F4240". (* new 4.233 sec *)

llee454 commented 4 years ago

[x] add import to Kami/AllDefn.v and remove explicit import statements.
[x] remove commented code.
[x] Simulator/NativeTest.v convert to natToHexStr.