/*
 * Copyright 2018 Amazon.com, Inc. or its affiliates. All Rights Reserved.
 *
 * Licensed under the Apache License, Version 2.0 (the "License"). You may not use
 * this file except in compliance with the License. A copy of the License is
 * located at
 *
 *     http://aws.amazon.com/apache2.0/
 *
 * or in the "license" file accompanying this file. This file is distributed on an
 * "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
 * implied. See the License for the specific language governing permissions and
 * limitations under the License.
 */

import "proofs.cry";

let runProof string_to_print property_to_check = do { 
    print string_to_print; 
    sat_print z3 property_to_check;
    print "\n";
    };

runProof "Is there any (non-error or done) state from which neither the loop continues nor a larger buffer is expected?" {{ isProgressMade }};

runProof "Is there any (non-error or done) state from which the loop does not continue?" {{ doesLoopContinue }};

runProof "Is there any (non-error or done) state from which neither the loop continues nor a larger buffer is expected when the precise size is known?" {{ isProgressMadeSizeKnown }};

runProof "Is there any (non-error or done) state from which the loop does not continue when the precise size is known?" {{ doesLoopContinueSizeKnown }};

runProof "Is it possible to not progress from the ST_WRITE_HEADER state after one buffer update acording to the size estimates?" {{ doesWriteHeaderContinueAfterUpdate }};

runProof "Is it possible to not progress from the ST_ENCRYPT_BODY state after one buffer update acording to the size estimates?" {{ doesEncryptBodyContinueAfterUpdate }};

runProof "Is it possible to not progress from the ST_ENCRYPT_BODY state when precise size is known after one buffer update acording to the size estimates?" {{ doesEncryptBodyContinueAfterUpdateSizeKnown }};