CODEWITHSUNDEEP
coq
Cryptostasis
Cryptostasis

Reputation: 1216

Example for Coq Cyclic Module usage

I want to model 32 bit integer arithmetic in Coq. I think that the Cyclic Module would be best suited for this. But I have some difficulties to figure out how to use that module. Could you please provide me some examples which show how to use it? Examples for the other number modules like Integer, Natural or Rational would also very helpful.

Upvotes: 0

Views: 93

Answers (1)

pedagand
pedagand

Reputation: 111

Allow me to not-answer your question: 32 bit integer arithmetic has already been modeled to death in the Coq eco-system.

You may want to have a look at CompCert's Integer.v, or x86proved's bits. This latter library has been repackaged by my student Arthur Blot here, extending it with a trustworthy extraction to OCaml integers. It should land in coq-opam soon.

Upvotes: 1

Related Questions