• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Zfc
    • Acre
    • Milawa
    • Smtlink
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • C
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • Java
    • Riscv
    • Taspi
    • Bitcoin
    • Des
    • Ethereum
    • X86isa
    • Sha-2
    • Yul
    • Zcash
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Poseidon
    • Where-do-i-place-my-book
    • Axe
    • Aleo
      • Aleobft
      • Aleovm
      • Leo
        • Grammar
        • Early-version
          • Json2ast
          • Testing
          • Definition
            • Flattening
            • Abstract-syntax
            • Dynamic-semantics
            • Compilation
            • Static-semantics
              • Type-checking
              • Static-environments
              • Curve-parameterization
              • Function-recursion
              • Struct-recursion
              • Input-checking
                • Check-input-item
                • Check-input-items
                • Check-input-section-list
                • Check-input-section
                • Check-input-file
                • Check-input-expression
                • Check-input-type
              • Program-checking
              • Type-maps-for-struct-components
              • Program-and-input-checking
              • Output-checking
            • Concrete-syntax
    • Bigmems
    • Builtins
    • Execloader
    • Solidity
    • Paco
    • Concurrent-programs
    • Bls12-377-curves
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Input-checking

Check-input-file

Check an input file.

Signature

(check-input-file infile env) → params

Arguments

infile — Guard (input-filep infile).

env — Guard (senvp env).

Returns

params — Type (funparam-list-resultp params).

Starting with the empty list of function parameters, we go through the file and collect all the function parameters corresponding to the input items. We also ensure that the sections have all distinct titles, i.e. that there are no repeated section titles. It is not required for all possible section titles to be present.

Definitions and Theorems

Function: check-input-file

(defun check-input-file (infile env)
  (declare (xargs :guard (and (input-filep infile) (senvp env))))
  (let ((__function__ 'check-input-file))
    (declare (ignorable __function__))
    (b* ((insecs (input-file->sections infile))
         ((okf params)
          (check-input-section-list insecs nil env))
         ((unless (no-duplicatesp-equal
                       (input-section-list->title-list insecs)))
          (reserrf (list :duplicate-sections))))
      params)))

Theorem: funparam-list-resultp-of-check-input-file

(defthm funparam-list-resultp-of-check-input-file
  (b* ((params (check-input-file infile env)))
    (funparam-list-resultp params))
  :rule-classes :rewrite)

Theorem: check-input-file-of-input-file-fix-infile

(defthm check-input-file-of-input-file-fix-infile
  (equal (check-input-file (input-file-fix infile)
                           env)
         (check-input-file infile env)))

Theorem: check-input-file-input-file-equiv-congruence-on-infile

(defthm check-input-file-input-file-equiv-congruence-on-infile
  (implies (input-file-equiv infile infile-equiv)
           (equal (check-input-file infile env)
                  (check-input-file infile-equiv env)))
  :rule-classes :congruence)

Theorem: check-input-file-of-senv-fix-env

(defthm check-input-file-of-senv-fix-env
  (equal (check-input-file infile (senv-fix env))
         (check-input-file infile env)))

Theorem: check-input-file-senv-equiv-congruence-on-env

(defthm check-input-file-senv-equiv-congruence-on-env
  (implies (senv-equiv env env-equiv)
           (equal (check-input-file infile env)
                  (check-input-file infile env-equiv)))
  :rule-classes :congruence)