私は現在vellvmを使用しており、その上で変換を開発しています。私はcoq初心者です。
プログラミング中に、次の警告に直面しました。
警告：NATで多数を処理すると、スタックオーバーフローまたはセグメンテーション違反が発生します（監視されるしきい値は、システムの制限と実行されたコマンドに応じて5000から70000まで変化する可能性があります）。
この警告を生成する私の関数は署名を計算します。署名は上位ビットと下位ビットに分けられます。上位ビットと下位ビットを表す2つのnatsn1とn2が与えられると、（n1 * 65536）+ n2が計算されます。これは、16ビットの2つの2進数を並べて配置するための抽象化です。
Sコンストラクターのおかげで、coq nat定義が外部から大きなintを処理しているように見えるので、私は非常に驚きました。
この警告を回避する/coqで大きな数を使用するにはどうすればよいですか？実装をnatからある種のバイナリ構造に変更することを歓迎します。
ありがとう！
Coq で型を使用する代わりに、nat(大きな数を操作する必要がある場合)Z型を使用する方が良い場合があります。これは、符号と絶対値のペア表現を使用して整数を形式化したものです。トレードオフは、証明が少し複雑になる可能性があることです。natは非常に単純であり、単純な証明原理を認めています。
ただし、Coq では、定義、定理、および証明を簡単に記述できるように、表記法が広範に使用されています。Coq のカーネルは非常に小さく (これが必要なのは、プルーフ チェッカーが正しく、それを読み取ることができると信じたいからです)、その上に多くの表記があります。ただし、物事にはさまざまな表現があり、適切なシンボルはごくわずかであるため、通常、シンボルは衝突します。これを乗り越えるために、coq は解釈スコープを使用してシンボルを明確にし、それらを名前に解決します ("+" は 、 などを意味するためadd) plus。
Z_scopeis where, +for pluswithinを使用して、あなたは正しいですZ。