pnwamk

import Init.Meta

-- This isn't strictly necessary of course - reverse could be a member of `Range`.
class Reverse (α : Type u) where
  reverse : α → α 

open Reverse (reverse)


-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --

pnwamk

import Std.Data.RBMap

-- Summary: Currently `forIn` provides a way to specify how
-- to iterate over values of a particular type in a `for`
-- loop in a way that conveniently guarantees termination
-- and allows arbitrary computation within the loop.

-- This file presents a slightly more general version called
-- `forStream` which aims to allow additional values to be
-- iterated over in-parallel with the first sequence. I.e.,

pnwamk

For common LLVM function contracts it may be useful for SAW users to simply specity the function's signature and pre/postconditions and let the low-level SAW boilerplate (e.g., the Python equivalents to crucible_fresh_var, crucible_alloc, etc) be done automatically since they're fairly predictable.

E.g., The abstract function contract class might look as follows:

class LLVMFunctionContract(metaclass=ABCMeta):

pnwamk

Simple Arithmetic

This Lean4 program

instance FloatHasNeg : HasNeg Float := ⟨λ x => 0 - x⟩
instance HasPowFloatNat : HasPow Float Nat := ⟨λ x y => x ^ (y.toFloat)⟩


def addNats : Nat → Nat → Nat

pnwamk

// Lean compiler output
// Module: StructsAndArith
// Imports: Init
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
#pragma clang diagnostic ignored "-Wunused-label"
#elif defined(__GNUC__) && !defined(__CLANG__)
#pragma GCC diagnostic ignored "-Wunused-parameter"
#pragma GCC diagnostic ignored "-Wunused-label"

pnwamk

// Lean compiler output
// Module: Arith
// Imports: Init
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
#pragma clang diagnostic ignored "-Wunused-label"
#elif defined(__GNUC__) && !defined(__CLANG__)
#pragma GCC diagnostic ignored "-Wunused-parameter"
#pragma GCC diagnostic ignored "-Wunused-label"

pnwamk

instance HasPowFloatNat : HasPow Float Nat := ⟨λ x y => x ^ (y.toFloat)⟩


structure Cartesian :=
(x : Float)
(y : Float)

structure Polar :=

pnwamk

instance FloatHasNeg : HasNeg Float := ⟨λ x => 0 - x⟩
instance HasPowFloatNat : HasPow Float Nat := ⟨λ x y => x ^ (y.toFloat)⟩


def addNats : Nat → Nat → Nat
| x, y => x + y

def addInts : Int → Int → Int
| x, y => x + y

pnwamk

-- eq_comp_err.lean
inductive SmtSort : Type
| bool  : SmtSort

inductive Term : SmtSort -> Type
| true : Term SmtSort.bool
| smtLet {s t : SmtSort} : String -> Term t
                       -> Term s
                       -> Term s

pnwamk

; main.block_0_201089.1 (0x201098). jump precondition: (= (mcstack (bvsub stack_high (_ bv8 64)) (_ BitVec 64)) (fnstart rbp))
(set-logic ALL_SUPPORTED)
(set-option :produce-models true)
(define-fun even_parity ((v (_ BitVec 8))) Bool (= (bvxor ((_ extract 0 0) v) ((_ extract 1 1) v) ((_ extract 2 2) v) ((_ extract 3 3) v) ((_ extract 4 4) v) ((_ extract 5 5) v) ((_ extract 6 6) v) ((_ extract 7 7) v)) #b0))
(define-fun mem_readbv8 ((m (Array (_ BitVec 64) (_ BitVec 8))) (a (_ BitVec 64))) (_ BitVec 8) (select m a))
(define-fun mem_readbv16 ((m (Array (_ BitVec 64) (_ BitVec 8))) (a (_ BitVec 64))) (_ BitVec 16) (concat (select m (bvadd a (_ bv1 64))) (select m a)))
(define-fun mem_readbv32 ((m (Array (_ BitVec 64) (_ BitVec 8))) (a (_ BitVec 64))) (_ BitVec 32) (concat (select m (bvadd a (_ bv3 64))) (concat (select m (bvadd a (_ bv2 64))) (concat (select m (bvadd a (_ bv1 64))) (select m a)))))
(define-fun mem_readbv64 ((m (Array (_ BitVec 64) (_ BitVec 8))) (a (_ BitVec 64))) (_ BitVec 64) (concat (select