Library CFML.Stdlib.Sys_proof

Set Implicit Arguments.
Require Import CFLib.
Require Import Sys_ml.

Parameter word_size_spec :
  word_size = 32 \/ word_size = 64.



Parameter max_array_length_spec :
  0 <= max_array_length.

Parameter max_string_length_spec :
  0 <= max_string_length.