saturation.saw

// HARDENS Reactor Trip System (RTS) Assurance Case
// In support of a formal model of RTS system behavior written in the
// Cryptol DSL, verifying the implementation of the RTS, genenerated
// from Cryptol, and hand-written, in both Verilog and C.
//
// @author Alex Bakst <abakst@galois.com>
// @created November, 2021

// Copyright 2021, 2022, 2023 Galois, Inc.
//
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
//     http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License 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.

include "common.saw";
enable_experimental;

cryptol_add_path "../models";

instrumentation_cryp <- cryptol_load "../models/RTS/InstrumentationUnit.cry";
saturation_gen  <- llvm_load_module "generated/saturation_impl.bc";

let saturation_ref = {{ instrumentation_cryp::Saturation }};

let saturation_spec = do {
    t <- llvm_fresh_var "t" (llvm_int 32);
    p <- llvm_fresh_var "p" (llvm_int 32);
    llvm_execute_func [llvm_term t, llvm_term p];
    llvm_return (llvm_term {{ saturation_ref t p }});
};

llvm_verify saturation_gen "Saturation" [] false saturation_spec z3;