Cortex.Wire.Pure

On this page
  1. Overview
  2. Context
  3. Theorem Split
  4. CorePure Subset
  5. Closed Builtin Signature Mirror
  6. Record Helpers
  7. Evaluation
  8. Static where Field Discovery
  9. Pure Node Lowering
  10. Output Value Contracts
Imports
import Mathlib.Data.Finset.Basic import Mathlib.Data.Int.Basic

Overview

Proof-facing model of Wire's CorePure subset and native pure-task lowering.

Context

Wire pure output equations use a deterministic expression layer. The Haskell implementation evaluates JSON-shaped values and lowers one source pure node to one internal native pure task with top-level bindings, an optional where expression, and output expressions.

This module does not prove the Haskell evaluator correct. It gives the Lean track a small executable model for the first proof slice: integers, booleans, records, field access, non-recursive sequential let, if, record merge, and simple operators. ADR 0010 keeps authority behind registered executor boundaries, and ADR 0023 keeps CorePure in the deterministic expression layer; accordingly, Expr has no constructors for executor calls, rewrites, durable-state reads, tools, model calls, or host callbacks.

ADR 0023 makes duplicate record fields an upstream parse/elaboration error. The evaluator remains deterministic outside the admitted surface, but duplicate field overwrite is not an intended record-literal semantics.

For static where fields, ADR 0031 settles the source surface in favor of the Haskell behavior: local CorePure let bindings are evaluated at runtime but are not expanded by static field discovery. Module-level let-declared records are represented by the initial StaticContext.

Theorem Split

The page defines values, expressions, deterministic evaluation, static where-field discovery, pure-node admission, native pure-task lowering, and the local soundness side condition needed when a where expression contains CorePure let. The facts are local to this proof model; no theorem here claims that the Haskell evaluator or compiler already produces these Lean witnesses. The closed-builtin table below is a proof-side signature mirror, not an evaluator oracle. The where soundness chain is exported for downstream output-value and contract proofs; the output-key theorems in this file are structural and do not need it.

namespace Cortex.Wire

CorePure Subset

namespace CorePure

CorePure names for variables, fields, ports, and output labels.

abbrev Name : Type := String

EvalError is the deterministic typed failure surface for this proof subset.

inductive EvalError : Type where | missingVariable : Name → EvalError | missingField : Name → EvalError | expectedBool : EvalError | expectedInt : EvalError | expectedRecord : EvalError | duplicateBinding : Name → EvalError deriving Repr

Value is the JSON-shaped value subset modeled by the first proof pass.

inductive Value : Type where | null : Value | bool : Bool → Value | int : Int → Value | string : String → Value | record : (Name → Option Value) → Value

Runtime CorePure environment.

abbrev Env : Type := Name → Option Valuenamespace Env

Empty runtime environment.

def empty : Env := fun _name => none

Insert or shadow a runtime binding.

def insert (name : Name) (value : Value) (env : Env) : Env := fun candidate => if candidate = name then some value else env candidateend Env

Static context for expressions known to expose record fields.

abbrev StaticContext : Type := Name → Option (Finset Name)namespace StaticContext

Empty static field context.

def empty : StaticContext := fun _name => none

Insert or shadow a static field binding. none deliberately shadows an outer record.

def insert (name : Name) (fields : Option (Finset Name)) (ctx : StaticContext) : StaticContext := fun candidate => if candidate = name then fields else ctx candidate

Hide static record facts for names opened by a node-local where record.

def hideFields (fields : Finset Name) (ctx : StaticContext) : StaticContext := fun candidate => if candidate ∈ fields then none else ctx candidateend StaticContext

Closed Builtin Signature Mirror

Authority classes used to classify the proof-side CorePure builtin signature mirror.

inductive BuiltinAuthority : Type where | pureValue | executor | host | durableState | model | tool | rewrite deriving DecidableEq, Repr

Proof-side signature for one closed CorePure builtin.

structure BuiltinSpec where

Builtin name exposed in the CorePure environment.

name : Name

Builtin arity.

arity : Nat

Authority class required by the builtin implementation.

authority : BuiltinAuthoritynamespace BuiltinSpec

authorityFree spec means a builtin stays inside pure value computation.

def authorityFree (spec : BuiltinSpec) : Prop := spec.authority = BuiltinAuthority.pureValueend BuiltinSpec

Closed CorePure builtin signatures duplicated from the Haskell evaluator.

This table is intentionally only a proof-side mirror. The Haskell side exposes corePureBuiltinSignature as the runtime review hook; no theorem in this file proves that Haskell evaluation consults this Lean table.

def closedBuiltinEnv : List BuiltinSpec := [ { name := "map", arity := 2, authority := BuiltinAuthority.pureValue } , { name := "fmap", arity := 2, authority := BuiltinAuthority.pureValue } , { name := "filter", arity := 2, authority := BuiltinAuthority.pureValue } , { name := "zip", arity := 2, authority := BuiltinAuthority.pureValue } , { name := "zipWith", arity := 3, authority := BuiltinAuthority.pureValue } , { name := "length", arity := 1, authority := BuiltinAuthority.pureValue } , { name := "sum", arity := 1, authority := BuiltinAuthority.pureValue } , { name := "all", arity := 2, authority := BuiltinAuthority.pureValue } , { name := "any", arity := 2, authority := BuiltinAuthority.pureValue } , { name := "min", arity := 2, authority := BuiltinAuthority.pureValue } , { name := "max", arity := 2, authority := BuiltinAuthority.pureValue } , { name := "abs", arity := 1, authority := BuiltinAuthority.pureValue } , { name := "clamp", arity := 3, authority := BuiltinAuthority.pureValue } , { name := "concat", arity := 1, authority := BuiltinAuthority.pureValue } , { name := "toString", arity := 1, authority := BuiltinAuthority.pureValue } , { name := "joinWith", arity := 2, authority := BuiltinAuthority.pureValue } , { name := "toJson", arity := 1, authority := BuiltinAuthority.pureValue } , { name := "fromJson", arity := 1, authority := BuiltinAuthority.pureValue } ]

Name/arity projection of the proof-side closed builtin mirror.

def closedBuiltinSignature : List (Name × Nat) := closedBuiltinEnv.map (fun spec => (spec.name, spec.arity))

Explicit signature expected from the Haskell corePureBuiltinSignature review hook.

theorem closedBuiltinSignature_eq : closedBuiltinSignature = [ ("map", 2) , ("fmap", 2) , ("filter", 2) , ("zip", 2) , ("zipWith", 3) , ("length", 1) , ("sum", 1) , ("all", 2) , ("any", 2) , ("min", 2) , ("max", 2) , ("abs", 1) , ("clamp", 3) , ("concat", 1) , ("toString", 1) , ("joinWith", 2) , ("toJson", 1) , ("fromJson", 1) ] := rfl

The proof-side closed CorePure builtin mirror contains no authority-bearing entry.

theorem closedBuiltinEnv_authorityFree : ∀ spec, spec ∈ closedBuiltinEnv → spec.authorityFree := ⊢ ∀ spec ∈ closedBuiltinEnv, spec.authorityFree intro spec spec:BuiltinSpechSpec:spec ∈ closedBuiltinEnv⊢ spec.authorityFree spec:BuiltinSpechSpec:spec = { name := "map", arity := 2, authority := BuiltinAuthority.pureValue } ∨ spec = { name := "fmap", arity := 2, authority := BuiltinAuthority.pureValue } ∨ spec = { name := "filter", arity := 2, authority := BuiltinAuthority.pureValue } ∨ spec = { name := "zip", arity := 2, authority := BuiltinAuthority.pureValue } ∨ spec = { name := "zipWith", arity := 3, authority := BuiltinAuthority.pureValue } ∨ spec = { name := "length", arity := 1, authority := BuiltinAuthority.pureValue } ∨ spec = { name := "sum", arity := 1, authority := BuiltinAuthority.pureValue } ∨ spec = { name := "all", arity := 2, authority := BuiltinAuthority.pureValue } ∨ spec = { name := "any", arity := 2, authority := BuiltinAuthority.pureValue } ∨ spec = { name := "min", arity := 2, authority := BuiltinAuthority.pureValue } ∨ spec = { name := "max", arity := 2, authority := BuiltinAuthority.pureValue } ∨ spec = { name := "abs", arity := 1, authority := BuiltinAuthority.pureValue } ∨ spec = { name := "clamp", arity := 3, authority := BuiltinAuthority.pureValue } ∨ spec = { name := "concat", arity := 1, authority := BuiltinAuthority.pureValue } ∨ spec = { name := "toString", arity := 1, authority := BuiltinAuthority.pureValue } ∨ spec = { name := "joinWith", arity := 2, authority := BuiltinAuthority.pureValue } ∨ spec = { name := "toJson", arity := 1, authority := BuiltinAuthority.pureValue } ∨ spec = { name := "fromJson", arity := 1, authority := BuiltinAuthority.pureValue }⊢ spec.authorityFree spec:BuiltinSpechSpec:spec = { name := "map", arity := 2, authority := BuiltinAuthority.pureValue }⊢ spec.authorityFreespec:BuiltinSpechSpec:spec = { name := "fmap", arity := 2, authority := BuiltinAuthority.pureValue }⊢ spec.authorityFreespec:BuiltinSpechSpec:spec = { name := "filter", arity := 2, authority := BuiltinAuthority.pureValue }⊢ spec.authorityFreespec:BuiltinSpechSpec:spec = { name := "zip", arity := 2, authority := BuiltinAuthority.pureValue }⊢ spec.authorityFreespec:BuiltinSpechSpec:spec = { name := "zipWith", arity := 3, authority := BuiltinAuthority.pureValue }⊢ spec.authorityFreespec:BuiltinSpechSpec:spec = { name := "length", arity := 1, authority := BuiltinAuthority.pureValue }⊢ spec.authorityFreespec:BuiltinSpechSpec:spec = { name := "sum", arity := 1, authority := BuiltinAuthority.pureValue }⊢ spec.authorityFreespec:BuiltinSpechSpec:spec = { name := "all", arity := 2, authority := BuiltinAuthority.pureValue }⊢ spec.authorityFreespec:BuiltinSpechSpec:spec = { name := "any", arity := 2, authority := BuiltinAuthority.pureValue }⊢ spec.authorityFreespec:BuiltinSpechSpec:spec = { name := "min", arity := 2, authority := BuiltinAuthority.pureValue }⊢ spec.authorityFreespec:BuiltinSpechSpec:spec = { name := "max", arity := 2, authority := BuiltinAuthority.pureValue }⊢ spec.authorityFreespec:BuiltinSpechSpec:spec = { name := "abs", arity := 1, authority := BuiltinAuthority.pureValue }⊢ spec.authorityFreespec:BuiltinSpechSpec:spec = { name := "clamp", arity := 3, authority := BuiltinAuthority.pureValue }⊢ spec.authorityFreespec:BuiltinSpechSpec:spec = { name := "concat", arity := 1, authority := BuiltinAuthority.pureValue }⊢ spec.authorityFreespec:BuiltinSpechSpec:spec = { name := "toString", arity := 1, authority := BuiltinAuthority.pureValue }⊢ spec.authorityFreespec:BuiltinSpechSpec:spec = { name := "joinWith", arity := 2, authority := BuiltinAuthority.pureValue }⊢ spec.authorityFreespec:BuiltinSpechSpec:spec = { name := "toJson", arity := 1, authority := BuiltinAuthority.pureValue }⊢ spec.authorityFreespec:BuiltinSpechSpec:spec = { name := "fromJson", arity := 1, authority := BuiltinAuthority.pureValue }⊢ spec.authorityFree spec:BuiltinSpechSpec:spec = { name := "map", arity := 2, authority := BuiltinAuthority.pureValue }⊢ spec.authorityFree ⊢ { name := "map", arity := 2, authority := BuiltinAuthority.pureValue }.authorityFree All goals completed! 🐙 spec:BuiltinSpechSpec:spec = { name := "fmap", arity := 2, authority := BuiltinAuthority.pureValue }⊢ spec.authorityFree ⊢ { name := "fmap", arity := 2, authority := BuiltinAuthority.pureValue }.authorityFree All goals completed! 🐙 spec:BuiltinSpechSpec:spec = { name := "filter", arity := 2, authority := BuiltinAuthority.pureValue }⊢ spec.authorityFree ⊢ { name := "filter", arity := 2, authority := BuiltinAuthority.pureValue }.authorityFree All goals completed! 🐙 spec:BuiltinSpechSpec:spec = { name := "zip", arity := 2, authority := BuiltinAuthority.pureValue }⊢ spec.authorityFree ⊢ { name := "zip", arity := 2, authority := BuiltinAuthority.pureValue }.authorityFree All goals completed! 🐙 spec:BuiltinSpechSpec:spec = { name := "zipWith", arity := 3, authority := BuiltinAuthority.pureValue }⊢ spec.authorityFree ⊢ { name := "zipWith", arity := 3, authority := BuiltinAuthority.pureValue }.authorityFree All goals completed! 🐙 spec:BuiltinSpechSpec:spec = { name := "length", arity := 1, authority := BuiltinAuthority.pureValue }⊢ spec.authorityFree ⊢ { name := "length", arity := 1, authority := BuiltinAuthority.pureValue }.authorityFree All goals completed! 🐙 spec:BuiltinSpechSpec:spec = { name := "sum", arity := 1, authority := BuiltinAuthority.pureValue }⊢ spec.authorityFree ⊢ { name := "sum", arity := 1, authority := BuiltinAuthority.pureValue }.authorityFree All goals completed! 🐙 spec:BuiltinSpechSpec:spec = { name := "all", arity := 2, authority := BuiltinAuthority.pureValue }⊢ spec.authorityFree ⊢ { name := "all", arity := 2, authority := BuiltinAuthority.pureValue }.authorityFree All goals completed! 🐙 spec:BuiltinSpechSpec:spec = { name := "any", arity := 2, authority := BuiltinAuthority.pureValue }⊢ spec.authorityFree ⊢ { name := "any", arity := 2, authority := BuiltinAuthority.pureValue }.authorityFree All goals completed! 🐙 spec:BuiltinSpechSpec:spec = { name := "min", arity := 2, authority := BuiltinAuthority.pureValue }⊢ spec.authorityFree ⊢ { name := "min", arity := 2, authority := BuiltinAuthority.pureValue }.authorityFree All goals completed! 🐙 spec:BuiltinSpechSpec:spec = { name := "max", arity := 2, authority := BuiltinAuthority.pureValue }⊢ spec.authorityFree ⊢ { name := "max", arity := 2, authority := BuiltinAuthority.pureValue }.authorityFree All goals completed! 🐙 spec:BuiltinSpechSpec:spec = { name := "abs", arity := 1, authority := BuiltinAuthority.pureValue }⊢ spec.authorityFree ⊢ { name := "abs", arity := 1, authority := BuiltinAuthority.pureValue }.authorityFree All goals completed! 🐙 spec:BuiltinSpechSpec:spec = { name := "clamp", arity := 3, authority := BuiltinAuthority.pureValue }⊢ spec.authorityFree ⊢ { name := "clamp", arity := 3, authority := BuiltinAuthority.pureValue }.authorityFree All goals completed! 🐙 spec:BuiltinSpechSpec:spec = { name := "concat", arity := 1, authority := BuiltinAuthority.pureValue }⊢ spec.authorityFree ⊢ { name := "concat", arity := 1, authority := BuiltinAuthority.pureValue }.authorityFree All goals completed! 🐙 spec:BuiltinSpechSpec:spec = { name := "toString", arity := 1, authority := BuiltinAuthority.pureValue }⊢ spec.authorityFree ⊢ { name := "toString", arity := 1, authority := BuiltinAuthority.pureValue }.authorityFree All goals completed! 🐙 spec:BuiltinSpechSpec:spec = { name := "joinWith", arity := 2, authority := BuiltinAuthority.pureValue }⊢ spec.authorityFree ⊢ { name := "joinWith", arity := 2, authority := BuiltinAuthority.pureValue }.authorityFree All goals completed! 🐙 spec:BuiltinSpechSpec:spec = { name := "toJson", arity := 1, authority := BuiltinAuthority.pureValue }⊢ spec.authorityFree ⊢ { name := "toJson", arity := 1, authority := BuiltinAuthority.pureValue }.authorityFree All goals completed! 🐙 spec:BuiltinSpechSpec:spec = { name := "fromJson", arity := 1, authority := BuiltinAuthority.pureValue }⊢ spec.authorityFree ⊢ { name := "fromJson", arity := 1, authority := BuiltinAuthority.pureValue }.authorityFree All goals completed! 🐙

Unary operators in the modeled CorePure subset.

inductive UnaryOp : Type where | not | negate

Binary operators in the modeled CorePure subset.

inductive BinaryOp : Type where | add | subtract | multiply | and | or | merge

CorePure expression subset for the first proof slice.

inductive Expr : Type where | lit : Value → Expr | var : Name → Expr | record : List (Name × Expr) → Expr | field : Expr → Name → Expr | letE : List (Name × Expr) → Expr → Expr | ifE : Expr → Expr → Expr → Expr | unary : UnaryOp → Expr → Expr | binary : BinaryOp → Expr → Expr → Exprnamespace Value

Interpret a value as a boolean or fail deterministically.

def asBool : Value → Except EvalError Bool | null => Except.error EvalError.expectedBool | bool value => Except.ok value | int _value => Except.error EvalError.expectedBool | string _value => Except.error EvalError.expectedBool | record _fields => Except.error EvalError.expectedBool

Interpret a value as an integer or fail deterministically.

def asInt : Value → Except EvalError Int | null => Except.error EvalError.expectedInt | bool _value => Except.error EvalError.expectedInt | int value => Except.ok value | string _value => Except.error EvalError.expectedInt | record _fields => Except.error EvalError.expectedInt

Interpret a value as a record or fail deterministically.

def asRecord : Value → Except EvalError (Name → Option Value) | null => Except.error EvalError.expectedRecord | bool _value => Except.error EvalError.expectedRecord | int _value => Except.error EvalError.expectedRecord | string _value => Except.error EvalError.expectedRecord | record fields => Except.ok fields

hasOnlyFields value fields says a record value exposes no keys outside fields.

def hasOnlyFields (value : Value) (fields : Finset Name) : Prop := match value with | record recordFields => ∀ name fieldValue, recordFields name = some fieldValue → name ∈ fields | null => False | bool _value => False | int _value => False | string _value => Falseend Value

Record Helpers

Convert evaluated field pairs to a record lookup function.

Admitted CorePure record literals must reject duplicate fields before evaluation. The right-biased fallback here only makes the proof-side evaluator total on raw lists.

def recordFromValues : List (Name × Value) → Name → Option Value | [], _name => none | (fieldName, fieldValue) :: rest, name => match recordFromValues rest name with | some value => some value | none => if name = fieldName then some fieldValue else none

Names present in a field-expression list.

def fieldNameSet (fields : List (Name × Expr)) : Finset Name := fields.foldr (fun field acc => insert field.1 acc) ∅

Names present in an evaluated field-value list.

def valueFieldNameSet (fields : List (Name × Value)) : Finset Name := fields.foldr (fun field acc => insert field.1 acc) ∅

Right-biased record merge for the modeled CorePure merge operator.

def mergeRecordFields (leftFields rightFields : Name → Option Value) : Name → Option Value := fun name => match rightFields name with | some value => some value | none => leftFields name

recordFromValues exposes only names present in its input field list.

theorem recordFromValues_hasOnlyFields (fields : List (Name × Value)) : ∀ name fieldValue, recordFromValues fields name = some fieldValue → name ∈ valueFieldNameSet fields := fields:List (Name × Value)⊢ ∀ (name : Name) (fieldValue : Value), recordFromValues fields name = some fieldValue → name ∈ valueFieldNameSet fields induction fields with ⊢ ∀ (name : Name) (fieldValue : Value), recordFromValues [] name = some fieldValue → name ∈ valueFieldNameSet [] intro name name:NamefieldValue:Value⊢ recordFromValues [] name = some fieldValue → name ∈ valueFieldNameSet [] name:NamefieldValue:ValuehLookup:recordFromValues [] name = some fieldValue⊢ name ∈ valueFieldNameSet [] All goals completed! 🐙 field:Name × Valuerest:List (Name × Value)ih:∀ (name : Name) (fieldValue : Value), recordFromValues rest name = some fieldValue → name ∈ valueFieldNameSet rest⊢ ∀ (name : Name) (fieldValue : Value), recordFromValues (field :: rest) name = some fieldValue → name ∈ valueFieldNameSet (field :: rest) intro name field:Name × Valuerest:List (Name × Value)ih:∀ (name : Name) (fieldValue : Value), recordFromValues rest name = some fieldValue → name ∈ valueFieldNameSet restname:NamefieldValue:Value⊢ recordFromValues (field :: rest) name = some fieldValue → name ∈ valueFieldNameSet (field :: rest) field:Name × Valuerest:List (Name × Value)ih:∀ (name : Name) (fieldValue : Value), recordFromValues rest name = some fieldValue → name ∈ valueFieldNameSet restname:NamefieldValue:ValuehLookup:recordFromValues (field :: rest) name = some fieldValue⊢ name ∈ valueFieldNameSet (field :: rest) rest:List (Name × Value)ih:∀ (name : Name) (fieldValue : Value), recordFromValues rest name = some fieldValue → name ∈ valueFieldNameSet restname:NamefieldValue:ValuefieldName:NamecurrentValue:ValuehLookup:recordFromValues ((fieldName, currentValue) :: rest) name = some fieldValue⊢ name ∈ valueFieldNameSet ((fieldName, currentValue) :: rest) rest:List (Name × Value)ih:∀ (name : Name) (fieldValue : Value), recordFromValues rest name = some fieldValue → name ∈ valueFieldNameSet restname:NamefieldValue:ValuefieldName:NamecurrentValue:ValuehLookup:recordFromValues ((fieldName, currentValue) :: rest) name = some fieldValuehName:name = fieldName⊢ name ∈ valueFieldNameSet ((fieldName, currentValue) :: rest)rest:List (Name × Value)ih:∀ (name : Name) (fieldValue : Value), recordFromValues rest name = some fieldValue → name ∈ valueFieldNameSet restname:NamefieldValue:ValuefieldName:NamecurrentValue:ValuehLookup:recordFromValues ((fieldName, currentValue) :: rest) name = some fieldValuehName:¬name = fieldName⊢ name ∈ valueFieldNameSet ((fieldName, currentValue) :: rest) rest:List (Name × Value)ih:∀ (name : Name) (fieldValue : Value), recordFromValues rest name = some fieldValue → name ∈ valueFieldNameSet restname:NamefieldValue:ValuefieldName:NamecurrentValue:ValuehLookup:recordFromValues ((fieldName, currentValue) :: rest) name = some fieldValuehName:name = fieldName⊢ name ∈ valueFieldNameSet ((fieldName, currentValue) :: rest) All goals completed! 🐙 rest:List (Name × Value)ih:∀ (name : Name) (fieldValue : Value), recordFromValues rest name = some fieldValue → name ∈ valueFieldNameSet restname:NamefieldValue:ValuefieldName:NamecurrentValue:ValuehLookup:recordFromValues ((fieldName, currentValue) :: rest) name = some fieldValuehName:¬name = fieldName⊢ name ∈ valueFieldNameSet ((fieldName, currentValue) :: rest) cases hRest : recordFromValues rest name with rest:List (Name × Value)ih:∀ (name : Name) (fieldValue : Value), recordFromValues rest name = some fieldValue → name ∈ valueFieldNameSet restname:NamefieldValue:ValuefieldName:NamecurrentValue:ValuehLookup:recordFromValues ((fieldName, currentValue) :: rest) name = some fieldValuehName:¬name = fieldNamerestValue:ValuehRest:recordFromValues rest name = some restValue⊢ name ∈ valueFieldNameSet ((fieldName, currentValue) :: rest) rest:List (Name × Value)ih:∀ (name : Name) (fieldValue : Value), recordFromValues rest name = some fieldValue → name ∈ valueFieldNameSet restname:NamefieldValue:ValuefieldName:NamecurrentValue:ValuehLookup:recordFromValues ((fieldName, currentValue) :: rest) name = some fieldValuehName:¬name = fieldNamerestValue:ValuehRest:recordFromValues rest name = some restValuehMember:name ∈ valueFieldNameSet rest⊢ name ∈ valueFieldNameSet ((fieldName, currentValue) :: rest) rest:List (Name × Value)ih:∀ (name : Name) (fieldValue : Value), recordFromValues rest name = some fieldValue → name ∈ valueFieldNameSet restname:NamefieldValue:ValuefieldName:NamecurrentValue:ValuehLookup:recordFromValues ((fieldName, currentValue) :: rest) name = some fieldValuehName:¬name = fieldNamerestValue:ValuehRest:recordFromValues rest name = some restValuehMember:name ∈ valueFieldNameSet rest⊢ name ∈ insert fieldName (valueFieldNameSet rest) All goals completed! 🐙 rest:List (Name × Value)ih:∀ (name : Name) (fieldValue : Value), recordFromValues rest name = some fieldValue → name ∈ valueFieldNameSet restname:NamefieldValue:ValuefieldName:NamecurrentValue:ValuehLookup:recordFromValues ((fieldName, currentValue) :: rest) name = some fieldValuehName:¬name = fieldNamehRest:recordFromValues rest name = none⊢ name ∈ valueFieldNameSet ((fieldName, currentValue) :: rest) All goals completed! 🐙

Every name present in an evaluated field-value list has a concrete record lookup.

theorem recordFromValues_field_present {fields : List (Name × Value)} {name : Name} (hName : name ∈ valueFieldNameSet fields) : ∃ fieldValue, recordFromValues fields name = some fieldValue := fields:List (Name × Value)name:NamehName:name ∈ valueFieldNameSet fields⊢ ∃ fieldValue, recordFromValues fields name = some fieldValue induction fields with name:NamehName:name ∈ valueFieldNameSet []⊢ ∃ fieldValue, recordFromValues [] name = some fieldValue All goals completed! 🐙 name:Namefield:Name × Valuerest:List (Name × Value)ih:name ∈ valueFieldNameSet rest → ∃ fieldValue, recordFromValues rest name = some fieldValuehName:name ∈ valueFieldNameSet (field :: rest)⊢ ∃ fieldValue, recordFromValues (field :: rest) name = some fieldValue name:Namerest:List (Name × Value)ih:name ∈ valueFieldNameSet rest → ∃ fieldValue, recordFromValues rest name = some fieldValuefieldName:NamecurrentValue:ValuehName:name ∈ valueFieldNameSet ((fieldName, currentValue) :: rest)⊢ ∃ fieldValue, recordFromValues ((fieldName, currentValue) :: rest) name = some fieldValue name:Namerest:List (Name × Value)ih:name ∈ valueFieldNameSet rest → ∃ fieldValue, recordFromValues rest name = some fieldValuefieldName:NamecurrentValue:ValuehName:name ∈ valueFieldNameSet ((fieldName, currentValue) :: rest)hCurrent:name = fieldName⊢ ∃ fieldValue, recordFromValues ((fieldName, currentValue) :: rest) name = some fieldValuename:Namerest:List (Name × Value)ih:name ∈ valueFieldNameSet rest → ∃ fieldValue, recordFromValues rest name = some fieldValuefieldName:NamecurrentValue:ValuehName:name ∈ valueFieldNameSet ((fieldName, currentValue) :: rest)hCurrent:¬name = fieldName⊢ ∃ fieldValue, recordFromValues ((fieldName, currentValue) :: rest) name = some fieldValue name:Namerest:List (Name × Value)ih:name ∈ valueFieldNameSet rest → ∃ fieldValue, recordFromValues rest name = some fieldValuefieldName:NamecurrentValue:ValuehName:name ∈ valueFieldNameSet ((fieldName, currentValue) :: rest)hCurrent:name = fieldName⊢ ∃ fieldValue, recordFromValues ((fieldName, currentValue) :: rest) name = some fieldValue name:Namerest:List (Name × Value)ih:name ∈ valueFieldNameSet rest → ∃ fieldValue, recordFromValues rest name = some fieldValuecurrentValue:ValuehName:name ∈ valueFieldNameSet ((name, currentValue) :: rest)⊢ ∃ fieldValue, recordFromValues ((name, currentValue) :: rest) name = some fieldValue cases hRest : recordFromValues rest name with name:Namerest:List (Name × Value)ih:name ∈ valueFieldNameSet rest → ∃ fieldValue, recordFromValues rest name = some fieldValuecurrentValue:ValuehName:name ∈ valueFieldNameSet ((name, currentValue) :: rest)restValue:ValuehRest:recordFromValues rest name = some restValue⊢ ∃ fieldValue, recordFromValues ((name, currentValue) :: rest) name = some fieldValue exact ⟨restValue, name:Namerest:List (Name × Value)ih:name ∈ valueFieldNameSet rest → ∃ fieldValue, recordFromValues rest name = some fieldValuecurrentValue:ValuehName:name ∈ valueFieldNameSet ((name, currentValue) :: rest)restValue:ValuehRest:recordFromValues rest name = some restValue⊢ recordFromValues ((name, currentValue) :: rest) name = some restValue All goals completed! 🐙⟩ name:Namerest:List (Name × Value)ih:name ∈ valueFieldNameSet rest → ∃ fieldValue, recordFromValues rest name = some fieldValuecurrentValue:ValuehName:name ∈ valueFieldNameSet ((name, currentValue) :: rest)hRest:recordFromValues rest name = none⊢ ∃ fieldValue, recordFromValues ((name, currentValue) :: rest) name = some fieldValue exact ⟨currentValue, name:Namerest:List (Name × Value)ih:name ∈ valueFieldNameSet rest → ∃ fieldValue, recordFromValues rest name = some fieldValuecurrentValue:ValuehName:name ∈ valueFieldNameSet ((name, currentValue) :: rest)hRest:recordFromValues rest name = none⊢ recordFromValues ((name, currentValue) :: rest) name = some currentValue All goals completed! 🐙⟩ name:Namerest:List (Name × Value)ih:name ∈ valueFieldNameSet rest → ∃ fieldValue, recordFromValues rest name = some fieldValuefieldName:NamecurrentValue:ValuehName:name ∈ valueFieldNameSet ((fieldName, currentValue) :: rest)hCurrent:¬name = fieldName⊢ ∃ fieldValue, recordFromValues ((fieldName, currentValue) :: rest) name = some fieldValue have hRestName : name ∈ valueFieldNameSet rest := fields:List (Name × Value)name:NamehName:name ∈ valueFieldNameSet fields⊢ ∃ fieldValue, recordFromValues fields name = some fieldValue have hInserted : name ∈ insert fieldName (valueFieldNameSet rest) := fields:List (Name × Value)name:NamehName:name ∈ valueFieldNameSet fields⊢ ∃ fieldValue, recordFromValues fields name = some fieldValue All goals completed! 🐙 All goals completed! 🐙 name:Namerest:List (Name × Value)ih:name ∈ valueFieldNameSet rest → ∃ fieldValue, recordFromValues rest name = some fieldValuefieldName:NamecurrentValue:ValuehName:name ∈ valueFieldNameSet ((fieldName, currentValue) :: rest)hCurrent:¬name = fieldNamehRestName:name ∈ valueFieldNameSet restrestValue:ValuehRestLookup:recordFromValues rest name = some restValue⊢ ∃ fieldValue, recordFromValues ((fieldName, currentValue) :: rest) name = some fieldValue exact ⟨restValue, name:Namerest:List (Name × Value)ih:name ∈ valueFieldNameSet rest → ∃ fieldValue, recordFromValues rest name = some fieldValuefieldName:NamecurrentValue:ValuehName:name ∈ valueFieldNameSet ((fieldName, currentValue) :: rest)hCurrent:¬name = fieldNamehRestName:name ∈ valueFieldNameSet restrestValue:ValuehRestLookup:recordFromValues rest name = some restValue⊢ recordFromValues ((fieldName, currentValue) :: rest) name = some restValue All goals completed! 🐙⟩

A successful record lookup came from one of the evaluated field-value pairs.

theorem recordFromValues_lookup_mem {fields : List (Name × Value)} {name : Name} {fieldValue : Value} (hLookup : recordFromValues fields name = some fieldValue) : (name, fieldValue) ∈ fields := fields:List (Name × Value)name:NamefieldValue:ValuehLookup:recordFromValues fields name = some fieldValue⊢ (name, fieldValue) ∈ fields induction fields generalizing name fieldValue with name:NamefieldValue:ValuehLookup:recordFromValues [] name = some fieldValue⊢ (name, fieldValue) ∈ [] All goals completed! 🐙 field:Name × Valuerest:List (Name × Value)ih:∀ {name : Name} {fieldValue : Value}, recordFromValues rest name = some fieldValue → (name, fieldValue) ∈ restname:NamefieldValue:ValuehLookup:recordFromValues (field :: rest) name = some fieldValue⊢ (name, fieldValue) ∈ field :: rest rest:List (Name × Value)ih:∀ {name : Name} {fieldValue : Value}, recordFromValues rest name = some fieldValue → (name, fieldValue) ∈ restname:NamefieldValue:ValuefieldName:NamecurrentValue:ValuehLookup:recordFromValues ((fieldName, currentValue) :: rest) name = some fieldValue⊢ (name, fieldValue) ∈ (fieldName, currentValue) :: rest cases hRest : recordFromValues rest name with rest:List (Name × Value)ih:∀ {name : Name} {fieldValue : Value}, recordFromValues rest name = some fieldValue → (name, fieldValue) ∈ restname:NamefieldValue:ValuefieldName:NamecurrentValue:ValuehLookup:recordFromValues ((fieldName, currentValue) :: rest) name = some fieldValuerestValue:ValuehRest:recordFromValues rest name = some restValue⊢ (name, fieldValue) ∈ (fieldName, currentValue) :: rest have hValue : restValue = fieldValue := fields:List (Name × Value)name:NamefieldValue:ValuehLookup:recordFromValues fields name = some fieldValue⊢ (name, fieldValue) ∈ fields rest:List (Name × Value)ih:∀ {name : Name} {fieldValue : Value}, recordFromValues rest name = some fieldValue → (name, fieldValue) ∈ restname:NamefieldValue:ValuefieldName:NamecurrentValue:ValuerestValue:ValuehRest:recordFromValues rest name = some restValuehLookup:restValue = fieldValue⊢ restValue = fieldValue All goals completed! 🐙 have hRestMember : (name, fieldValue) ∈ rest := fields:List (Name × Value)name:NamefieldValue:ValuehLookup:recordFromValues fields name = some fieldValue⊢ (name, fieldValue) ∈ fields All goals completed! 🐙 All goals completed! 🐙 rest:List (Name × Value)ih:∀ {name : Name} {fieldValue : Value}, recordFromValues rest name = some fieldValue → (name, fieldValue) ∈ restname:NamefieldValue:ValuefieldName:NamecurrentValue:ValuehLookup:recordFromValues ((fieldName, currentValue) :: rest) name = some fieldValuehRest:recordFromValues rest name = none⊢ (name, fieldValue) ∈ (fieldName, currentValue) :: rest rest:List (Name × Value)ih:∀ {name : Name} {fieldValue : Value}, recordFromValues rest name = some fieldValue → (name, fieldValue) ∈ restname:NamefieldValue:ValuefieldName:NamecurrentValue:ValuehLookup:recordFromValues ((fieldName, currentValue) :: rest) name = some fieldValuehRest:recordFromValues rest name = nonehName:name = fieldName⊢ (name, fieldValue) ∈ (fieldName, currentValue) :: restrest:List (Name × Value)ih:∀ {name : Name} {fieldValue : Value}, recordFromValues rest name = some fieldValue → (name, fieldValue) ∈ restname:NamefieldValue:ValuefieldName:NamecurrentValue:ValuehLookup:recordFromValues ((fieldName, currentValue) :: rest) name = some fieldValuehRest:recordFromValues rest name = nonehName:¬name = fieldName⊢ (name, fieldValue) ∈ (fieldName, currentValue) :: rest rest:List (Name × Value)ih:∀ {name : Name} {fieldValue : Value}, recordFromValues rest name = some fieldValue → (name, fieldValue) ∈ restname:NamefieldValue:ValuefieldName:NamecurrentValue:ValuehLookup:recordFromValues ((fieldName, currentValue) :: rest) name = some fieldValuehRest:recordFromValues rest name = nonehName:name = fieldName⊢ (name, fieldValue) ∈ (fieldName, currentValue) :: rest rest:List (Name × Value)ih:∀ {name : Name} {fieldValue : Value}, recordFromValues rest name = some fieldValue → (name, fieldValue) ∈ restname:NamefieldValue:ValuecurrentValue:ValuehRest:recordFromValues rest name = nonehLookup:recordFromValues ((name, currentValue) :: rest) name = some fieldValue⊢ (name, fieldValue) ∈ (name, currentValue) :: rest rest:List (Name × Value)ih:∀ {name : Name} {fieldValue : Value}, recordFromValues rest name = some fieldValue → (name, fieldValue) ∈ restname:NamefieldValue:ValuecurrentValue:ValuehRest:recordFromValues rest name = nonehLookup:currentValue = fieldValue⊢ (name, fieldValue) ∈ (name, currentValue) :: rest rest:List (Name × Value)ih:∀ {name : Name} {fieldValue : Value}, recordFromValues rest name = some fieldValue → (name, fieldValue) ∈ restname:NamefieldValue:ValuehRest:recordFromValues rest name = none⊢ (name, fieldValue) ∈ (name, fieldValue) :: rest All goals completed! 🐙 rest:List (Name × Value)ih:∀ {name : Name} {fieldValue : Value}, recordFromValues rest name = some fieldValue → (name, fieldValue) ∈ restname:NamefieldValue:ValuefieldName:NamecurrentValue:ValuehLookup:recordFromValues ((fieldName, currentValue) :: rest) name = some fieldValuehRest:recordFromValues rest name = nonehName:¬name = fieldName⊢ (name, fieldValue) ∈ (fieldName, currentValue) :: rest All goals completed! 🐙

Evaluation

Find the first duplicate name in a list, if one exists.

def duplicateName : List Name → Option Name | [] => none | name :: rest => if name ∈ rest then some name else duplicateName restmutual

Evaluate a CorePure expression in a runtime environment.

def eval (env : Env) : Expr → Except EvalError Value | Expr.lit value => Except.ok value | Expr.var name => match env name with | some value => Except.ok value | none => Except.error (EvalError.missingVariable name) | Expr.record fields => match evalFields env fields with | Except.ok values => Except.ok (Value.record (recordFromValues values)) | Except.error err => Except.error err | Expr.field base fieldName => do let baseRecord ← (← eval env base).asRecord match baseRecord fieldName with | some value => Except.ok value | none => Except.error (EvalError.missingField fieldName) | Expr.letE bindings body => match evalBindings env bindings with | Except.ok localEnv => eval localEnv body | Except.error err => Except.error err | Expr.ifE condition thenExpr elseExpr => do let conditionValue ← (← eval env condition).asBool if conditionValue then eval env thenExpr else eval env elseExpr | Expr.unary op operand => do match op with | UnaryOp.not => Except.ok (Value.bool (!(← (← eval env operand).asBool))) | UnaryOp.negate => Except.ok (Value.int (-(← (← eval env operand).asInt))) | Expr.binary op left right => do match op with | BinaryOp.add => Except.ok (Value.int ((← (← eval env left).asInt) + (← (← eval env right).asInt))) | BinaryOp.subtract => Except.ok (Value.int ((← (← eval env left).asInt) - (← (← eval env right).asInt))) | BinaryOp.multiply => Except.ok (Value.int ((← (← eval env left).asInt) * (← (← eval env right).asInt))) | BinaryOp.and => let leftValue ← (← eval env left).asBool if leftValue then Except.ok (Value.bool (← (← eval env right).asBool)) else Except.ok (Value.bool false) | BinaryOp.or => let leftValue ← (← eval env left).asBool if leftValue then Except.ok (Value.bool true) else Except.ok (Value.bool (← (← eval env right).asBool)) | BinaryOp.merge => match eval env left with | Except.error err => Except.error err | Except.ok Value.null => Except.error EvalError.expectedRecord | Except.ok (Value.bool _value) => Except.error EvalError.expectedRecord | Except.ok (Value.int _value) => Except.error EvalError.expectedRecord | Except.ok (Value.string _value) => Except.error EvalError.expectedRecord | Except.ok (Value.record leftRecord) => match eval env right with | Except.error err => Except.error err | Except.ok Value.null => Except.error EvalError.expectedRecord | Except.ok (Value.bool _value) => Except.error EvalError.expectedRecord | Except.ok (Value.int _value) => Except.error EvalError.expectedRecord | Except.ok (Value.string _value) => Except.error EvalError.expectedRecord | Except.ok (Value.record rightRecord) => Except.ok (Value.record (mergeRecordFields leftRecord rightRecord))

Evaluate record fields independently in the same environment.

def evalFields (env : Env) : List (Name × Expr) → Except EvalError (List (Name × Value)) | [] => Except.ok [] | (fieldName, fieldExpr) :: rest => match eval env fieldExpr with | Except.ok fieldValue => match evalFields env rest with | Except.ok restValues => Except.ok ((fieldName, fieldValue) :: restValues) | Except.error err => Except.error err | Except.error err => Except.error err

Evaluate non-recursive sequential let bindings.

def evalBindings (env : Env) : List (Name × Expr) → Except EvalError Env | bindings => match duplicateName (bindings.map Prod.fst) with | some name => Except.error (EvalError.duplicateBinding name) | none => evalBindingsNoDuplicate env bindings

Evaluate bindings after duplicate names have been rejected.

def evalBindingsNoDuplicate (env : Env) : List (Name × Expr) → Except EvalError Env | [] => Except.ok env | (bindingName, bindingExpr) :: rest => match eval env bindingExpr with | Except.ok bindingValue => evalBindingsNoDuplicate (Env.insert bindingName bindingValue env) rest | Except.error err => Except.error err end

Evaluating fields preserves their field-name set.

theorem evalFields_preserves_names {env : Env} {fields : List (Name × Expr)} {values : List (Name × Value)} (hEval : evalFields env fields = Except.ok values) : valueFieldNameSet values = fieldNameSet fields := env:Envfields:List (Name × Expr)values:List (Name × Value)hEval:evalFields env fields = Except.ok values⊢ valueFieldNameSet values = fieldNameSet fields induction fields generalizing values with env:Envvalues:List (Name × Value)hEval:evalFields env [] = Except.ok values⊢ valueFieldNameSet values = fieldNameSet [] env:Envvalues:List (Name × Value)hEval:values = []⊢ valueFieldNameSet values = fieldNameSet [] env:Env⊢ valueFieldNameSet [] = fieldNameSet [] All goals completed! 🐙 env:Envfield:Name × Exprrest:List (Name × Expr)ih:∀ {values : List (Name × Value)}, evalFields env rest = Except.ok values → valueFieldNameSet values = fieldNameSet restvalues:List (Name × Value)hEval:evalFields env (field :: rest) = Except.ok values⊢ valueFieldNameSet values = fieldNameSet (field :: rest) env:Envrest:List (Name × Expr)ih:∀ {values : List (Name × Value)}, evalFields env rest = Except.ok values → valueFieldNameSet values = fieldNameSet restvalues:List (Name × Value)fieldName:NamefieldExpr:ExprhEval:evalFields env ((fieldName, fieldExpr) :: rest) = Except.ok values⊢ valueFieldNameSet values = fieldNameSet ((fieldName, fieldExpr) :: rest) env:Envrest:List (Name × Expr)ih:∀ {values : List (Name × Value)}, evalFields env rest = Except.ok values → valueFieldNameSet values = fieldNameSet restvalues:List (Name × Value)fieldName:NamefieldExpr:ExprhEval:(match eval env fieldExpr with | Except.ok fieldValue => match evalFields env rest with | Except.ok restValues => Except.ok ((fieldName, fieldValue) :: restValues) | Except.error err => Except.error err | Except.error err => Except.error err) = Except.ok values⊢ valueFieldNameSet values = fieldNameSet ((fieldName, fieldExpr) :: rest) cases hField : eval env fieldExpr with env:Envrest:List (Name × Expr)ih:∀ {values : List (Name × Value)}, evalFields env rest = Except.ok values → valueFieldNameSet values = fieldNameSet restvalues:List (Name × Value)fieldName:NamefieldExpr:ExprhEval:(match eval env fieldExpr with | Except.ok fieldValue => match evalFields env rest with | Except.ok restValues => Except.ok ((fieldName, fieldValue) :: restValues) | Except.error err => Except.error err | Except.error err => Except.error err) = Except.ok valueserr:EvalErrorhField:eval env fieldExpr = Except.error err⊢ valueFieldNameSet values = fieldNameSet ((fieldName, fieldExpr) :: rest) All goals completed! 🐙 env:Envrest:List (Name × Expr)ih:∀ {values : List (Name × Value)}, evalFields env rest = Except.ok values → valueFieldNameSet values = fieldNameSet restvalues:List (Name × Value)fieldName:NamefieldExpr:ExprhEval:(match eval env fieldExpr with | Except.ok fieldValue => match evalFields env rest with | Except.ok restValues => Except.ok ((fieldName, fieldValue) :: restValues) | Except.error err => Except.error err | Except.error err => Except.error err) = Except.ok valuesfieldValue:ValuehField:eval env fieldExpr = Except.ok fieldValue⊢ valueFieldNameSet values = fieldNameSet ((fieldName, fieldExpr) :: rest) env:Envrest:List (Name × Expr)ih:∀ {values : List (Name × Value)}, evalFields env rest = Except.ok values → valueFieldNameSet values = fieldNameSet restvalues:List (Name × Value)fieldName:NamefieldExpr:ExprfieldValue:ValuehField:eval env fieldExpr = Except.ok fieldValuehEval:(match evalFields env rest with | Except.ok restValues => Except.ok ((fieldName, fieldValue) :: restValues) | Except.error err => Except.error err) = Except.ok values⊢ valueFieldNameSet values = fieldNameSet ((fieldName, fieldExpr) :: rest) cases hRest : evalFields env rest with env:Envrest:List (Name × Expr)ih:∀ {values : List (Name × Value)}, evalFields env rest = Except.ok values → valueFieldNameSet values = fieldNameSet restvalues:List (Name × Value)fieldName:NamefieldExpr:ExprfieldValue:ValuehField:eval env fieldExpr = Except.ok fieldValuehEval:(match evalFields env rest with | Except.ok restValues => Except.ok ((fieldName, fieldValue) :: restValues) | Except.error err => Except.error err) = Except.ok valueserr:EvalErrorhRest:evalFields env rest = Except.error err⊢ valueFieldNameSet values = fieldNameSet ((fieldName, fieldExpr) :: rest) All goals completed! 🐙 env:Envrest:List (Name × Expr)ih:∀ {values : List (Name × Value)}, evalFields env rest = Except.ok values → valueFieldNameSet values = fieldNameSet restvalues:List (Name × Value)fieldName:NamefieldExpr:ExprfieldValue:ValuehField:eval env fieldExpr = Except.ok fieldValuehEval:(match evalFields env rest with | Except.ok restValues => Except.ok ((fieldName, fieldValue) :: restValues) | Except.error err => Except.error err) = Except.ok valuesrestValues:List (Name × Value)hRest:evalFields env rest = Except.ok restValues⊢ valueFieldNameSet values = fieldNameSet ((fieldName, fieldExpr) :: rest) env:Envrest:List (Name × Expr)ih:∀ {values : List (Name × Value)}, evalFields env rest = Except.ok values → valueFieldNameSet values = fieldNameSet restvalues:List (Name × Value)fieldName:NamefieldExpr:ExprfieldValue:ValuehField:eval env fieldExpr = Except.ok fieldValuerestValues:List (Name × Value)hRest:evalFields env rest = Except.ok restValueshEval:(fieldName, fieldValue) :: restValues = values⊢ valueFieldNameSet values = fieldNameSet ((fieldName, fieldExpr) :: rest) env:Envrest:List (Name × Expr)ih:∀ {values : List (Name × Value)}, evalFields env rest = Except.ok values → valueFieldNameSet values = fieldNameSet restfieldName:NamefieldExpr:ExprfieldValue:ValuehField:eval env fieldExpr = Except.ok fieldValuerestValues:List (Name × Value)hRest:evalFields env rest = Except.ok restValues⊢ valueFieldNameSet ((fieldName, fieldValue) :: restValues) = fieldNameSet ((fieldName, fieldExpr) :: rest) env:Envrest:List (Name × Expr)ih:∀ {values : List (Name × Value)}, evalFields env rest = Except.ok values → valueFieldNameSet values = fieldNameSet restfieldName:NamefieldExpr:ExprfieldValue:ValuehField:eval env fieldExpr = Except.ok fieldValuerestValues:List (Name × Value)hRest:evalFields env rest = Except.ok restValues⊢ insert fieldName (valueFieldNameSet restValues) = insert fieldName (fieldNameSet rest) All goals completed! 🐙

Record expressions evaluate to records containing only their statically named fields.

theorem eval_record_hasOnlyFields {env : Env} {fields : List (Name × Expr)} {recordFields : Name → Option Value} (hEval : eval env (Expr.record fields) = Except.ok (Value.record recordFields)) : ∀ name fieldValue, recordFields name = some fieldValue → name ∈ fieldNameSet fields := env:Envfields:List (Name × Expr)recordFields:Name → Option ValuehEval:eval env (Expr.record fields) = Except.ok (Value.record recordFields)⊢ ∀ (name : Name) (fieldValue : Value), recordFields name = some fieldValue → name ∈ fieldNameSet fields env:Envfields:List (Name × Expr)recordFields:Name → Option ValuehEval:(match evalFields env fields with | Except.ok values => Except.ok (Value.record (recordFromValues values)) | Except.error err => Except.error err) = Except.ok (Value.record recordFields)⊢ ∀ (name : Name) (fieldValue : Value), recordFields name = some fieldValue → name ∈ fieldNameSet fields cases hFields : evalFields env fields with env:Envfields:List (Name × Expr)recordFields:Name → Option ValuehEval:(match evalFields env fields with | Except.ok values => Except.ok (Value.record (recordFromValues values)) | Except.error err => Except.error err) = Except.ok (Value.record recordFields)err:EvalErrorhFields:evalFields env fields = Except.error err⊢ ∀ (name : Name) (fieldValue : Value), recordFields name = some fieldValue → name ∈ fieldNameSet fields All goals completed! 🐙 env:Envfields:List (Name × Expr)recordFields:Name → Option ValuehEval:(match evalFields env fields with | Except.ok values => Except.ok (Value.record (recordFromValues values)) | Except.error err => Except.error err) = Except.ok (Value.record recordFields)values:List (Name × Value)hFields:evalFields env fields = Except.ok values⊢ ∀ (name : Name) (fieldValue : Value), recordFields name = some fieldValue → name ∈ fieldNameSet fields env:Envfields:List (Name × Expr)recordFields:Name → Option Valuevalues:List (Name × Value)hFields:evalFields env fields = Except.ok valueshEval:recordFromValues values = recordFields⊢ ∀ (name : Name) (fieldValue : Value), recordFields name = some fieldValue → name ∈ fieldNameSet fields env:Envfields:List (Name × Expr)values:List (Name × Value)hFields:evalFields env fields = Except.ok values⊢ ∀ (name : Name) (fieldValue : Value), recordFromValues values name = some fieldValue → name ∈ fieldNameSet fields intro name env:Envfields:List (Name × Expr)values:List (Name × Value)hFields:evalFields env fields = Except.ok valuesname:NamefieldValue:Value⊢ recordFromValues values name = some fieldValue → name ∈ fieldNameSet fields env:Envfields:List (Name × Expr)values:List (Name × Value)hFields:evalFields env fields = Except.ok valuesname:NamefieldValue:ValuehLookup:recordFromValues values name = some fieldValue⊢ name ∈ fieldNameSet fields env:Envfields:List (Name × Expr)values:List (Name × Value)hFields:evalFields env fields = Except.ok valuesname:NamefieldValue:ValuehLookup:recordFromValues values name = some fieldValuehMember:name ∈ valueFieldNameSet values⊢ name ∈ fieldNameSet fields env:Envfields:List (Name × Expr)values:List (Name × Value)hFields:evalFields env fields = Except.ok valuesname:NamefieldValue:ValuehLookup:recordFromValues values name = some fieldValuehMember:name ∈ valueFieldNameSet valueshNames:valueFieldNameSet values = fieldNameSet fields⊢ name ∈ fieldNameSet fields All goals completed! 🐙

Record expressions evaluate to values containing only their statically named fields.

theorem eval_record_value_hasOnlyFields {env : Env} {fields : List (Name × Expr)} {value : Value} (hEval : eval env (Expr.record fields) = Except.ok value) : Value.hasOnlyFields value (fieldNameSet fields) := env:Envfields:List (Name × Expr)value:ValuehEval:eval env (Expr.record fields) = Except.ok value⊢ value.hasOnlyFields (fieldNameSet fields) cases hFields : evalFields env fields with env:Envfields:List (Name × Expr)value:ValuehEval:eval env (Expr.record fields) = Except.ok valueerr:EvalErrorhFields:evalFields env fields = Except.error err⊢ value.hasOnlyFields (fieldNameSet fields) All goals completed! 🐙 env:Envfields:List (Name × Expr)value:ValuehEval:eval env (Expr.record fields) = Except.ok valuevalues:List (Name × Value)hFields:evalFields env fields = Except.ok values⊢ value.hasOnlyFields (fieldNameSet fields) env:Envfields:List (Name × Expr)value:Valuevalues:List (Name × Value)hFields:evalFields env fields = Except.ok valueshEval:Value.record (recordFromValues values) = value⊢ value.hasOnlyFields (fieldNameSet fields) env:Envfields:List (Name × Expr)values:List (Name × Value)hFields:evalFields env fields = Except.ok values⊢ (Value.record (recordFromValues values)).hasOnlyFields (fieldNameSet fields) env:Envfields:List (Name × Expr)values:List (Name × Value)hFields:evalFields env fields = Except.ok valueshNames:valueFieldNameSet values = fieldNameSet fields⊢ (Value.record (recordFromValues values)).hasOnlyFields (fieldNameSet fields) All goals completed! 🐙

Right-biased record merge exposes only fields from either input record.

theorem mergeRecordFields_hasOnlyFields {leftFields rightFields : Name → Option Value} {leftStatic rightStatic : Finset Name} (hLeft : Value.hasOnlyFields (Value.record leftFields) leftStatic) (hRight : Value.hasOnlyFields (Value.record rightFields) rightStatic) : Value.hasOnlyFields (Value.record (mergeRecordFields leftFields rightFields)) (leftStatic ∪ rightStatic) := leftFields:Name → Option ValuerightFields:Name → Option ValueleftStatic:Finset NamerightStatic:Finset NamehLeft:(Value.record leftFields).hasOnlyFields leftStatichRight:(Value.record rightFields).hasOnlyFields rightStatic⊢ (Value.record (mergeRecordFields leftFields rightFields)).hasOnlyFields (leftStatic ∪ rightStatic) intro name leftFields:Name → Option ValuerightFields:Name → Option ValueleftStatic:Finset NamerightStatic:Finset NamehLeft:(Value.record leftFields).hasOnlyFields leftStatichRight:(Value.record rightFields).hasOnlyFields rightStaticname:NamefieldValue:Value⊢ mergeRecordFields leftFields rightFields name = some fieldValue → name ∈ leftStatic ∪ rightStatic leftFields:Name → Option ValuerightFields:Name → Option ValueleftStatic:Finset NamerightStatic:Finset NamehLeft:(Value.record leftFields).hasOnlyFields leftStatichRight:(Value.record rightFields).hasOnlyFields rightStaticname:NamefieldValue:ValuehLookup:mergeRecordFields leftFields rightFields name = some fieldValue⊢ name ∈ leftStatic ∪ rightStatic cases hRightLookup : rightFields name with leftFields:Name → Option ValuerightFields:Name → Option ValueleftStatic:Finset NamerightStatic:Finset NamehLeft:(Value.record leftFields).hasOnlyFields leftStatichRight:(Value.record rightFields).hasOnlyFields rightStaticname:NamefieldValue:ValuehLookup:mergeRecordFields leftFields rightFields name = some fieldValuerightValue:ValuehRightLookup:rightFields name = some rightValue⊢ name ∈ leftStatic ∪ rightStatic leftFields:Name → Option ValuerightFields:Name → Option ValueleftStatic:Finset NamerightStatic:Finset NamehLeft:(Value.record leftFields).hasOnlyFields leftStatichRight:(Value.record rightFields).hasOnlyFields rightStaticname:NamefieldValue:ValuehLookup:mergeRecordFields leftFields rightFields name = some fieldValuerightValue:ValuehRightLookup:rightFields name = some rightValuehRightMember:name ∈ rightStatic⊢ name ∈ leftStatic ∪ rightStatic All goals completed! 🐙 leftFields:Name → Option ValuerightFields:Name → Option ValueleftStatic:Finset NamerightStatic:Finset NamehLeft:(Value.record leftFields).hasOnlyFields leftStatichRight:(Value.record rightFields).hasOnlyFields rightStaticname:NamefieldValue:ValuehLookup:mergeRecordFields leftFields rightFields name = some fieldValuehRightLookup:rightFields name = none⊢ name ∈ leftStatic ∪ rightStatic have hLeftLookup : leftFields name = some fieldValue := leftFields:Name → Option ValuerightFields:Name → Option ValueleftStatic:Finset NamerightStatic:Finset NamehLeft:(Value.record leftFields).hasOnlyFields leftStatichRight:(Value.record rightFields).hasOnlyFields rightStatic⊢ (Value.record (mergeRecordFields leftFields rightFields)).hasOnlyFields (leftStatic ∪ rightStatic) All goals completed! 🐙 leftFields:Name → Option ValuerightFields:Name → Option ValueleftStatic:Finset NamerightStatic:Finset NamehLeft:(Value.record leftFields).hasOnlyFields leftStatichRight:(Value.record rightFields).hasOnlyFields rightStaticname:NamefieldValue:ValuehLookup:mergeRecordFields leftFields rightFields name = some fieldValuehRightLookup:rightFields name = nonehLeftLookup:leftFields name = some fieldValuehLeftMember:name ∈ leftStatic⊢ name ∈ leftStatic ∪ rightStatic All goals completed! 🐙

Static where Field Discovery

Static field discovery for expressions used as node-local where clauses.

def whereStaticFields (ctx : StaticContext) : Expr → Option (Finset Name) | Expr.lit _value => none | Expr.record fields => some (fieldNameSet fields) | Expr.var name => ctx name | Expr.field _base _fieldName => none | Expr.letE _bindings body => whereStaticFields ctx body | Expr.ifE _condition _thenExpr _elseExpr => none | Expr.unary _op _operand => none | Expr.binary BinaryOp.merge left right => match whereStaticFields ctx left, whereStaticFields ctx right with | some leftFields, some rightFields => some (leftFields ∪ rightFields) | some _leftFields, none => none | none, some _rightFields => none | none, none => none | Expr.binary BinaryOp.add _left _right => none | Expr.binary BinaryOp.subtract _left _right => none | Expr.binary BinaryOp.multiply _left _right => none | Expr.binary BinaryOp.and _left _right => none | Expr.binary BinaryOp.or _left _right => none

Runtime environments match the static context for known record bindings.

def EnvMatchesStatic (env : Env) (ctx : StaticContext) : Prop := ∀ name fields value, ctx name = some fields → env name = some value → Value.hasOnlyFields value fields

Local CorePure let bindings do not shadow statically known module-level records.

def letBindingsDoNotShadowStatic (ctx : StaticContext) : List (Name × Expr) → Prop | [] => True | (bindingName, _bindingExpr) :: rest => ctx bindingName = none ∧ letBindingsDoNotShadowStatic ctx rest

Side condition for expressions whose local let binders preserve static discovery soundness.

def Expr.staticLetSafe (ctx : StaticContext) : Expr → Prop | Expr.lit _value => True | Expr.record _fields => True | Expr.var _name => True | Expr.field _base _fieldName => True | Expr.letE bindings body => letBindingsDoNotShadowStatic ctx bindings ∧ Expr.staticLetSafe ctx body | Expr.ifE _condition _thenExpr _elseExpr => True | Expr.unary _op _operand => True | Expr.binary BinaryOp.merge left right => Expr.staticLetSafe ctx left ∧ Expr.staticLetSafe ctx right | Expr.binary BinaryOp.add _left _right => True | Expr.binary BinaryOp.subtract _left _right => True | Expr.binary BinaryOp.multiply _left _right => True | Expr.binary BinaryOp.and _left _right => True | Expr.binary BinaryOp.or _left _right => True

Per-binding static facts for top-level CorePure bindings.

def TopLevelBindingStatics (ctx : StaticContext) (bindings : List (Name × Expr)) : Prop := ∀ name expr fields, (name, expr) ∈ bindings → ctx name = some fields → Expr.staticLetSafe ctx expr ∧ whereStaticFields ctx expr = some fields

Top-level bindings establish the static context when every static entry is backed by a binding and every backed binding has matching static record-field discovery.

This is not a Haskell correspondence proof by itself. It is the Lean-side witness shape that a compiler bridge must produce.

structure TopLevelBindingsEstablishStaticContext (ctx : StaticContext) (bindings : List (Name × Expr)) : Prop where

Any binding used by the static context has the corresponding static field discovery fact.

binding_static : TopLevelBindingStatics ctx bindings

Any static context entry is backed by some top-level binding.

ctx_supported : ∀ name fields, ctx name = some fields → ∃ expr, (name, expr) ∈ bindings

Static field discovery succeeds for record literals with exactly their field-name set.

theorem where_staticFields_record (ctx : StaticContext) (fields : List (Name × Expr)) : whereStaticFields ctx (Expr.record fields) = some (fieldNameSet fields) := rfl

Static field discovery for merge is the union of both record field sets.

theorem where_staticFields_merge {ctx : StaticContext} {left right : Expr} {leftFields rightFields : Finset Name} (hLeft : whereStaticFields ctx left = some leftFields) (hRight : whereStaticFields ctx right = some rightFields) : whereStaticFields ctx (Expr.binary BinaryOp.merge left right) = some (leftFields ∪ rightFields) := ctx:StaticContextleft:Exprright:ExprleftFields:Finset NamerightFields:Finset NamehLeft:whereStaticFields ctx left = some leftFieldshRight:whereStaticFields ctx right = some rightFields⊢ whereStaticFields ctx (Expr.binary BinaryOp.merge left right) = some (leftFields ∪ rightFields) All goals completed! 🐙

Static field discovery for let checks only the final body expression.

theorem where_staticFields_let (ctx : StaticContext) (bindings : List (Name × Expr)) (body : Expr) : whereStaticFields ctx (Expr.letE bindings body) = whereStaticFields ctx body := rfl

Evaluated non-duplicate bindings preserve the static context when they do not shadow it.

theorem evalBindingsNoDuplicate_preserves_static_context {ctx : StaticContext} {env localEnv : Env} {bindings : List (Name × Expr)} (hMatch : EnvMatchesStatic env ctx) (hNoShadow : letBindingsDoNotShadowStatic ctx bindings) (hEval : evalBindingsNoDuplicate env bindings = Except.ok localEnv) : EnvMatchesStatic localEnv ctx := ctx:StaticContextenv:EnvlocalEnv:Envbindings:List (Name × Expr)hMatch:EnvMatchesStatic env ctxhNoShadow:letBindingsDoNotShadowStatic ctx bindingshEval:evalBindingsNoDuplicate env bindings = Except.ok localEnv⊢ EnvMatchesStatic localEnv ctx induction bindings generalizing ctx env localEnv with ctx:StaticContextenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxhNoShadow:letBindingsDoNotShadowStatic ctx []hEval:evalBindingsNoDuplicate env [] = Except.ok localEnv⊢ EnvMatchesStatic localEnv ctx ctx:StaticContextenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxhNoShadow:letBindingsDoNotShadowStatic ctx []hEval:env = localEnv⊢ EnvMatchesStatic localEnv ctx ctx:StaticContextenv:EnvhMatch:EnvMatchesStatic env ctxhNoShadow:letBindingsDoNotShadowStatic ctx []⊢ EnvMatchesStatic env ctx All goals completed! 🐙 head:Name × Exprtail:List (Name × Expr)ih:∀ {ctx : StaticContext} {env localEnv : Env}, EnvMatchesStatic env ctx → letBindingsDoNotShadowStatic ctx tail → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxctx:StaticContextenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxhNoShadow:letBindingsDoNotShadowStatic ctx (head :: tail)hEval:evalBindingsNoDuplicate env (head :: tail) = Except.ok localEnv⊢ EnvMatchesStatic localEnv ctx tail:List (Name × Expr)ih:∀ {ctx : StaticContext} {env localEnv : Env}, EnvMatchesStatic env ctx → letBindingsDoNotShadowStatic ctx tail → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxctx:StaticContextenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhNoShadow:letBindingsDoNotShadowStatic ctx ((bindingName, bindingExpr) :: tail)hEval:evalBindingsNoDuplicate env ((bindingName, bindingExpr) :: tail) = Except.ok localEnv⊢ EnvMatchesStatic localEnv ctx tail:List (Name × Expr)ih:∀ {ctx : StaticContext} {env localEnv : Env}, EnvMatchesStatic env ctx → letBindingsDoNotShadowStatic ctx tail → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxctx:StaticContextenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhNoShadow:letBindingsDoNotShadowStatic ctx ((bindingName, bindingExpr) :: tail)hEval:evalBindingsNoDuplicate env ((bindingName, bindingExpr) :: tail) = Except.ok localEnvhHeadNoShadow:ctx bindingName = none⊢ EnvMatchesStatic localEnv ctx tail:List (Name × Expr)ih:∀ {ctx : StaticContext} {env localEnv : Env}, EnvMatchesStatic env ctx → letBindingsDoNotShadowStatic ctx tail → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxctx:StaticContextenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhNoShadow:letBindingsDoNotShadowStatic ctx ((bindingName, bindingExpr) :: tail)hEval:evalBindingsNoDuplicate env ((bindingName, bindingExpr) :: tail) = Except.ok localEnvhHeadNoShadow:ctx bindingName = nonehTailNoShadow:letBindingsDoNotShadowStatic ctx tail⊢ EnvMatchesStatic localEnv ctx tail:List (Name × Expr)ih:∀ {ctx : StaticContext} {env localEnv : Env}, EnvMatchesStatic env ctx → letBindingsDoNotShadowStatic ctx tail → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxctx:StaticContextenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhNoShadow:letBindingsDoNotShadowStatic ctx ((bindingName, bindingExpr) :: tail)hHeadNoShadow:ctx bindingName = nonehTailNoShadow:letBindingsDoNotShadowStatic ctx tailhEval:(match eval env bindingExpr with | Except.ok bindingValue => evalBindingsNoDuplicate (Env.insert bindingName bindingValue env) tail | Except.error err => Except.error err) = Except.ok localEnv⊢ EnvMatchesStatic localEnv ctx cases hBindingEval : eval env bindingExpr with tail:List (Name × Expr)ih:∀ {ctx : StaticContext} {env localEnv : Env}, EnvMatchesStatic env ctx → letBindingsDoNotShadowStatic ctx tail → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxctx:StaticContextenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhNoShadow:letBindingsDoNotShadowStatic ctx ((bindingName, bindingExpr) :: tail)hHeadNoShadow:ctx bindingName = nonehTailNoShadow:letBindingsDoNotShadowStatic ctx tailhEval:(match eval env bindingExpr with | Except.ok bindingValue => evalBindingsNoDuplicate (Env.insert bindingName bindingValue env) tail | Except.error err => Except.error err) = Except.ok localEnverr:EvalErrorhBindingEval:eval env bindingExpr = Except.error err⊢ EnvMatchesStatic localEnv ctx All goals completed! 🐙 tail:List (Name × Expr)ih:∀ {ctx : StaticContext} {env localEnv : Env}, EnvMatchesStatic env ctx → letBindingsDoNotShadowStatic ctx tail → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxctx:StaticContextenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhNoShadow:letBindingsDoNotShadowStatic ctx ((bindingName, bindingExpr) :: tail)hHeadNoShadow:ctx bindingName = nonehTailNoShadow:letBindingsDoNotShadowStatic ctx tailhEval:(match eval env bindingExpr with | Except.ok bindingValue => evalBindingsNoDuplicate (Env.insert bindingName bindingValue env) tail | Except.error err => Except.error err) = Except.ok localEnvbindingValue:ValuehBindingEval:eval env bindingExpr = Except.ok bindingValue⊢ EnvMatchesStatic localEnv ctx tail:List (Name × Expr)ih:∀ {ctx : StaticContext} {env localEnv : Env}, EnvMatchesStatic env ctx → letBindingsDoNotShadowStatic ctx tail → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxctx:StaticContextenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhNoShadow:letBindingsDoNotShadowStatic ctx ((bindingName, bindingExpr) :: tail)hHeadNoShadow:ctx bindingName = nonehTailNoShadow:letBindingsDoNotShadowStatic ctx tailbindingValue:ValuehBindingEval:eval env bindingExpr = Except.ok bindingValuehEval:evalBindingsNoDuplicate (Env.insert bindingName bindingValue env) tail = Except.ok localEnv⊢ EnvMatchesStatic localEnv ctx have hNextMatch : EnvMatchesStatic (Env.insert bindingName bindingValue env) ctx := ctx:StaticContextenv:EnvlocalEnv:Envbindings:List (Name × Expr)hMatch:EnvMatchesStatic env ctxhNoShadow:letBindingsDoNotShadowStatic ctx bindingshEval:evalBindingsNoDuplicate env bindings = Except.ok localEnv⊢ EnvMatchesStatic localEnv ctx intro candidate tail:List (Name × Expr)ih:∀ {ctx : StaticContext} {env localEnv : Env}, EnvMatchesStatic env ctx → letBindingsDoNotShadowStatic ctx tail → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxctx:StaticContextenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhNoShadow:letBindingsDoNotShadowStatic ctx ((bindingName, bindingExpr) :: tail)hHeadNoShadow:ctx bindingName = nonehTailNoShadow:letBindingsDoNotShadowStatic ctx tailbindingValue:ValuehBindingEval:eval env bindingExpr = Except.ok bindingValuehEval:evalBindingsNoDuplicate (Env.insert bindingName bindingValue env) tail = Except.ok localEnvcandidate:Namefields:Finset Name⊢ ∀ (value : Value), ctx candidate = some fields → Env.insert bindingName bindingValue env candidate = some value → value.hasOnlyFields fields tail:List (Name × Expr)ih:∀ {ctx : StaticContext} {env localEnv : Env}, EnvMatchesStatic env ctx → letBindingsDoNotShadowStatic ctx tail → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxctx:StaticContextenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhNoShadow:letBindingsDoNotShadowStatic ctx ((bindingName, bindingExpr) :: tail)hHeadNoShadow:ctx bindingName = nonehTailNoShadow:letBindingsDoNotShadowStatic ctx tailbindingValue:ValuehBindingEval:eval env bindingExpr = Except.ok bindingValuehEval:evalBindingsNoDuplicate (Env.insert bindingName bindingValue env) tail = Except.ok localEnvcandidate:Namefields:Finset Namevalue:Value⊢ ctx candidate = some fields → Env.insert bindingName bindingValue env candidate = some value → value.hasOnlyFields fields tail:List (Name × Expr)ih:∀ {ctx : StaticContext} {env localEnv : Env}, EnvMatchesStatic env ctx → letBindingsDoNotShadowStatic ctx tail → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxctx:StaticContextenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhNoShadow:letBindingsDoNotShadowStatic ctx ((bindingName, bindingExpr) :: tail)hHeadNoShadow:ctx bindingName = nonehTailNoShadow:letBindingsDoNotShadowStatic ctx tailbindingValue:ValuehBindingEval:eval env bindingExpr = Except.ok bindingValuehEval:evalBindingsNoDuplicate (Env.insert bindingName bindingValue env) tail = Except.ok localEnvcandidate:Namefields:Finset Namevalue:ValuehStaticLookup:ctx candidate = some fields⊢ Env.insert bindingName bindingValue env candidate = some value → value.hasOnlyFields fields tail:List (Name × Expr)ih:∀ {ctx : StaticContext} {env localEnv : Env}, EnvMatchesStatic env ctx → letBindingsDoNotShadowStatic ctx tail → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxctx:StaticContextenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhNoShadow:letBindingsDoNotShadowStatic ctx ((bindingName, bindingExpr) :: tail)hHeadNoShadow:ctx bindingName = nonehTailNoShadow:letBindingsDoNotShadowStatic ctx tailbindingValue:ValuehBindingEval:eval env bindingExpr = Except.ok bindingValuehEval:evalBindingsNoDuplicate (Env.insert bindingName bindingValue env) tail = Except.ok localEnvcandidate:Namefields:Finset Namevalue:ValuehStaticLookup:ctx candidate = some fieldshEnvLookup:Env.insert bindingName bindingValue env candidate = some value⊢ value.hasOnlyFields fields tail:List (Name × Expr)ih:∀ {ctx : StaticContext} {env localEnv : Env}, EnvMatchesStatic env ctx → letBindingsDoNotShadowStatic ctx tail → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxctx:StaticContextenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhNoShadow:letBindingsDoNotShadowStatic ctx ((bindingName, bindingExpr) :: tail)hHeadNoShadow:ctx bindingName = nonehTailNoShadow:letBindingsDoNotShadowStatic ctx tailbindingValue:ValuehBindingEval:eval env bindingExpr = Except.ok bindingValuehEval:evalBindingsNoDuplicate (Env.insert bindingName bindingValue env) tail = Except.ok localEnvcandidate:Namefields:Finset Namevalue:ValuehStaticLookup:ctx candidate = some fieldshEnvLookup:(if candidate = bindingName then some bindingValue else env candidate) = some value⊢ value.hasOnlyFields fields tail:List (Name × Expr)ih:∀ {ctx : StaticContext} {env localEnv : Env}, EnvMatchesStatic env ctx → letBindingsDoNotShadowStatic ctx tail → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxctx:StaticContextenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhNoShadow:letBindingsDoNotShadowStatic ctx ((bindingName, bindingExpr) :: tail)hHeadNoShadow:ctx bindingName = nonehTailNoShadow:letBindingsDoNotShadowStatic ctx tailbindingValue:ValuehBindingEval:eval env bindingExpr = Except.ok bindingValuehEval:evalBindingsNoDuplicate (Env.insert bindingName bindingValue env) tail = Except.ok localEnvcandidate:Namefields:Finset Namevalue:ValuehStaticLookup:ctx candidate = some fieldshEnvLookup:(if candidate = bindingName then some bindingValue else env candidate) = some valuehCandidate:candidate = bindingName⊢ value.hasOnlyFields fieldstail:List (Name × Expr)ih:∀ {ctx : StaticContext} {env localEnv : Env}, EnvMatchesStatic env ctx → letBindingsDoNotShadowStatic ctx tail → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxctx:StaticContextenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhNoShadow:letBindingsDoNotShadowStatic ctx ((bindingName, bindingExpr) :: tail)hHeadNoShadow:ctx bindingName = nonehTailNoShadow:letBindingsDoNotShadowStatic ctx tailbindingValue:ValuehBindingEval:eval env bindingExpr = Except.ok bindingValuehEval:evalBindingsNoDuplicate (Env.insert bindingName bindingValue env) tail = Except.ok localEnvcandidate:Namefields:Finset Namevalue:ValuehStaticLookup:ctx candidate = some fieldshEnvLookup:(if candidate = bindingName then some bindingValue else env candidate) = some valuehCandidate:¬candidate = bindingName⊢ value.hasOnlyFields fields tail:List (Name × Expr)ih:∀ {ctx : StaticContext} {env localEnv : Env}, EnvMatchesStatic env ctx → letBindingsDoNotShadowStatic ctx tail → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxctx:StaticContextenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhNoShadow:letBindingsDoNotShadowStatic ctx ((bindingName, bindingExpr) :: tail)hHeadNoShadow:ctx bindingName = nonehTailNoShadow:letBindingsDoNotShadowStatic ctx tailbindingValue:ValuehBindingEval:eval env bindingExpr = Except.ok bindingValuehEval:evalBindingsNoDuplicate (Env.insert bindingName bindingValue env) tail = Except.ok localEnvcandidate:Namefields:Finset Namevalue:ValuehStaticLookup:ctx candidate = some fieldshEnvLookup:(if candidate = bindingName then some bindingValue else env candidate) = some valuehCandidate:candidate = bindingName⊢ value.hasOnlyFields fields tail:List (Name × Expr)ih:∀ {ctx : StaticContext} {env localEnv : Env}, EnvMatchesStatic env ctx → letBindingsDoNotShadowStatic ctx tail → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxctx:StaticContextenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhNoShadow:letBindingsDoNotShadowStatic ctx ((bindingName, bindingExpr) :: tail)hHeadNoShadow:ctx bindingName = nonehTailNoShadow:letBindingsDoNotShadowStatic ctx tailbindingValue:ValuehBindingEval:eval env bindingExpr = Except.ok bindingValuehEval:evalBindingsNoDuplicate (Env.insert bindingName bindingValue env) tail = Except.ok localEnvcandidate:Namefields:Finset Namevalue:ValuehStaticLookup:ctx bindingName = some fieldshEnvLookup:(if candidate = bindingName then some bindingValue else env candidate) = some valuehCandidate:candidate = bindingName⊢ value.hasOnlyFields fields All goals completed! 🐙 tail:List (Name × Expr)ih:∀ {ctx : StaticContext} {env localEnv : Env}, EnvMatchesStatic env ctx → letBindingsDoNotShadowStatic ctx tail → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxctx:StaticContextenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhNoShadow:letBindingsDoNotShadowStatic ctx ((bindingName, bindingExpr) :: tail)hHeadNoShadow:ctx bindingName = nonehTailNoShadow:letBindingsDoNotShadowStatic ctx tailbindingValue:ValuehBindingEval:eval env bindingExpr = Except.ok bindingValuehEval:evalBindingsNoDuplicate (Env.insert bindingName bindingValue env) tail = Except.ok localEnvcandidate:Namefields:Finset Namevalue:ValuehStaticLookup:ctx candidate = some fieldshEnvLookup:(if candidate = bindingName then some bindingValue else env candidate) = some valuehCandidate:¬candidate = bindingName⊢ value.hasOnlyFields fields tail:List (Name × Expr)ih:∀ {ctx : StaticContext} {env localEnv : Env}, EnvMatchesStatic env ctx → letBindingsDoNotShadowStatic ctx tail → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxctx:StaticContextenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhNoShadow:letBindingsDoNotShadowStatic ctx ((bindingName, bindingExpr) :: tail)hHeadNoShadow:ctx bindingName = nonehTailNoShadow:letBindingsDoNotShadowStatic ctx tailbindingValue:ValuehBindingEval:eval env bindingExpr = Except.ok bindingValuehEval:evalBindingsNoDuplicate (Env.insert bindingName bindingValue env) tail = Except.ok localEnvcandidate:Namefields:Finset Namevalue:ValuehStaticLookup:ctx candidate = some fieldshCandidate:¬candidate = bindingNamehEnvLookup:env candidate = some value⊢ value.hasOnlyFields fields All goals completed! 🐙 All goals completed! 🐙

Runtime binding evaluation preserves the static context when it succeeds without shadowing.

theorem evalBindings_preserves_static_context {ctx : StaticContext} {env localEnv : Env} {bindings : List (Name × Expr)} (hMatch : EnvMatchesStatic env ctx) (hNoShadow : letBindingsDoNotShadowStatic ctx bindings) (hEval : evalBindings env bindings = Except.ok localEnv) : EnvMatchesStatic localEnv ctx := ctx:StaticContextenv:EnvlocalEnv:Envbindings:List (Name × Expr)hMatch:EnvMatchesStatic env ctxhNoShadow:letBindingsDoNotShadowStatic ctx bindingshEval:evalBindings env bindings = Except.ok localEnv⊢ EnvMatchesStatic localEnv ctx cases hDuplicate : duplicateName (bindings.map Prod.fst) with ctx:StaticContextenv:EnvlocalEnv:Envbindings:List (Name × Expr)hMatch:EnvMatchesStatic env ctxhNoShadow:letBindingsDoNotShadowStatic ctx bindingshEval:evalBindings env bindings = Except.ok localEnvduplicate:NamehDuplicate:duplicateName (List.map Prod.fst bindings) = some duplicate⊢ EnvMatchesStatic localEnv ctx All goals completed! 🐙 ctx:StaticContextenv:EnvlocalEnv:Envbindings:List (Name × Expr)hMatch:EnvMatchesStatic env ctxhNoShadow:letBindingsDoNotShadowStatic ctx bindingshEval:evalBindings env bindings = Except.ok localEnvhDuplicate:duplicateName (List.map Prod.fst bindings) = none⊢ EnvMatchesStatic localEnv ctx have hNoDuplicateEval : evalBindingsNoDuplicate env bindings = Except.ok localEnv := ctx:StaticContextenv:EnvlocalEnv:Envbindings:List (Name × Expr)hMatch:EnvMatchesStatic env ctxhNoShadow:letBindingsDoNotShadowStatic ctx bindingshEval:evalBindings env bindings = Except.ok localEnv⊢ EnvMatchesStatic localEnv ctx All goals completed! 🐙 All goals completed! 🐙

Runtime merge evaluation preserves the union of the statically admitted fields.

private theorem eval_merge_hasOnlyFields {ctx : StaticContext} {env : Env} {left right : Expr} {leftFields rightFields : Finset Name} {value : Value} (hLeftSafe : Expr.staticLetSafe ctx left) (hRightSafe : Expr.staticLetSafe ctx right) (hMatch : EnvMatchesStatic env ctx) (hLeftStatic : whereStaticFields ctx left = some leftFields) (hRightStatic : whereStaticFields ctx right = some rightFields) (hEval : eval env (Expr.binary BinaryOp.merge left right) = Except.ok value) (leftIH : ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx left → EnvMatchesStatic env ctx → whereStaticFields ctx left = some fields → eval env left = Except.ok value → Value.hasOnlyFields value fields) (rightIH : ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx right → EnvMatchesStatic env ctx → whereStaticFields ctx right = some fields → eval env right = Except.ok value → Value.hasOnlyFields value fields) : Value.hasOnlyFields value (leftFields ∪ rightFields) := ctx:StaticContextenv:Envleft:Exprright:ExprleftFields:Finset NamerightFields:Finset Namevalue:ValuehLeftSafe:Expr.staticLetSafe ctx lefthRightSafe:Expr.staticLetSafe ctx righthMatch:EnvMatchesStatic env ctxhLeftStatic:whereStaticFields ctx left = some leftFieldshRightStatic:whereStaticFields ctx right = some rightFieldshEval:eval env (Expr.binary BinaryOp.merge left right) = Except.ok valueleftIH:∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx left → EnvMatchesStatic env ctx → whereStaticFields ctx left = some fields → eval env left = Except.ok value → value.hasOnlyFields fieldsrightIH:∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx right → EnvMatchesStatic env ctx → whereStaticFields ctx right = some fields → eval env right = Except.ok value → value.hasOnlyFields fields⊢ value.hasOnlyFields (leftFields ∪ rightFields) cases hLeftEval : eval env left with ctx:StaticContextenv:Envleft:Exprright:ExprleftFields:Finset NamerightFields:Finset Namevalue:ValuehLeftSafe:Expr.staticLetSafe ctx lefthRightSafe:Expr.staticLetSafe ctx righthMatch:EnvMatchesStatic env ctxhLeftStatic:whereStaticFields ctx left = some leftFieldshRightStatic:whereStaticFields ctx right = some rightFieldshEval:eval env (Expr.binary BinaryOp.merge left right) = Except.ok valueleftIH:∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx left → EnvMatchesStatic env ctx → whereStaticFields ctx left = some fields → eval env left = Except.ok value → value.hasOnlyFields fieldsrightIH:∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx right → EnvMatchesStatic env ctx → whereStaticFields ctx right = some fields → eval env right = Except.ok value → value.hasOnlyFields fieldserr:EvalErrorhLeftEval:eval env left = Except.error err⊢ value.hasOnlyFields (leftFields ∪ rightFields) All goals completed! 🐙 ctx:StaticContextenv:Envleft:Exprright:ExprleftFields:Finset NamerightFields:Finset Namevalue:ValuehLeftSafe:Expr.staticLetSafe ctx lefthRightSafe:Expr.staticLetSafe ctx righthMatch:EnvMatchesStatic env ctxhLeftStatic:whereStaticFields ctx left = some leftFieldshRightStatic:whereStaticFields ctx right = some rightFieldshEval:eval env (Expr.binary BinaryOp.merge left right) = Except.ok valueleftIH:∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx left → EnvMatchesStatic env ctx → whereStaticFields ctx left = some fields → eval env left = Except.ok value → value.hasOnlyFields fieldsrightIH:∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx right → EnvMatchesStatic env ctx → whereStaticFields ctx right = some fields → eval env right = Except.ok value → value.hasOnlyFields fieldsleftValue:ValuehLeftEval:eval env left = Except.ok leftValue⊢ value.hasOnlyFields (leftFields ∪ rightFields) cases leftValue with ctx:StaticContextenv:Envleft:Exprright:ExprleftFields:Finset NamerightFields:Finset Namevalue:ValuehLeftSafe:Expr.staticLetSafe ctx lefthRightSafe:Expr.staticLetSafe ctx righthMatch:EnvMatchesStatic env ctxhLeftStatic:whereStaticFields ctx left = some leftFieldshRightStatic:whereStaticFields ctx right = some rightFieldshEval:eval env (Expr.binary BinaryOp.merge left right) = Except.ok valueleftIH:∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx left → EnvMatchesStatic env ctx → whereStaticFields ctx left = some fields → eval env left = Except.ok value → value.hasOnlyFields fieldsrightIH:∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx right → EnvMatchesStatic env ctx → whereStaticFields ctx right = some fields → eval env right = Except.ok value → value.hasOnlyFields fieldshLeftEval:eval env left = Except.ok Value.null⊢ value.hasOnlyFields (leftFields ∪ rightFields) All goals completed! 🐙 ctx:StaticContextenv:Envleft:Exprright:ExprleftFields:Finset NamerightFields:Finset Namevalue:ValuehLeftSafe:Expr.staticLetSafe ctx lefthRightSafe:Expr.staticLetSafe ctx righthMatch:EnvMatchesStatic env ctxhLeftStatic:whereStaticFields ctx left = some leftFieldshRightStatic:whereStaticFields ctx right = some rightFieldshEval:eval env (Expr.binary BinaryOp.merge left right) = Except.ok valueleftIH:∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx left → EnvMatchesStatic env ctx → whereStaticFields ctx left = some fields → eval env left = Except.ok value → value.hasOnlyFields fieldsrightIH:∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx right → EnvMatchesStatic env ctx → whereStaticFields ctx right = some fields → eval env right = Except.ok value → value.hasOnlyFields fieldsleftBool:BoolhLeftEval:eval env left = Except.ok (Value.bool leftBool)⊢ value.hasOnlyFields (leftFields ∪ rightFields) All goals completed! 🐙 ctx:StaticContextenv:Envleft:Exprright:ExprleftFields:Finset NamerightFields:Finset Namevalue:ValuehLeftSafe:Expr.staticLetSafe ctx lefthRightSafe:Expr.staticLetSafe ctx righthMatch:EnvMatchesStatic env ctxhLeftStatic:whereStaticFields ctx left = some leftFieldshRightStatic:whereStaticFields ctx right = some rightFieldshEval:eval env (Expr.binary BinaryOp.merge left right) = Except.ok valueleftIH:∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx left → EnvMatchesStatic env ctx → whereStaticFields ctx left = some fields → eval env left = Except.ok value → value.hasOnlyFields fieldsrightIH:∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx right → EnvMatchesStatic env ctx → whereStaticFields ctx right = some fields → eval env right = Except.ok value → value.hasOnlyFields fieldsleftInt:ℤhLeftEval:eval env left = Except.ok (Value.int leftInt)⊢ value.hasOnlyFields (leftFields ∪ rightFields) All goals completed! 🐙 ctx:StaticContextenv:Envleft:Exprright:ExprleftFields:Finset NamerightFields:Finset Namevalue:ValuehLeftSafe:Expr.staticLetSafe ctx lefthRightSafe:Expr.staticLetSafe ctx righthMatch:EnvMatchesStatic env ctxhLeftStatic:whereStaticFields ctx left = some leftFieldshRightStatic:whereStaticFields ctx right = some rightFieldshEval:eval env (Expr.binary BinaryOp.merge left right) = Except.ok valueleftIH:∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx left → EnvMatchesStatic env ctx → whereStaticFields ctx left = some fields → eval env left = Except.ok value → value.hasOnlyFields fieldsrightIH:∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx right → EnvMatchesStatic env ctx → whereStaticFields ctx right = some fields → eval env right = Except.ok value → value.hasOnlyFields fieldsleftString:StringhLeftEval:eval env left = Except.ok (Value.string leftString)⊢ value.hasOnlyFields (leftFields ∪ rightFields) All goals completed! 🐙 ctx:StaticContextenv:Envleft:Exprright:ExprleftFields:Finset NamerightFields:Finset Namevalue:ValuehLeftSafe:Expr.staticLetSafe ctx lefthRightSafe:Expr.staticLetSafe ctx righthMatch:EnvMatchesStatic env ctxhLeftStatic:whereStaticFields ctx left = some leftFieldshRightStatic:whereStaticFields ctx right = some rightFieldshEval:eval env (Expr.binary BinaryOp.merge left right) = Except.ok valueleftIH:∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx left → EnvMatchesStatic env ctx → whereStaticFields ctx left = some fields → eval env left = Except.ok value → value.hasOnlyFields fieldsrightIH:∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx right → EnvMatchesStatic env ctx → whereStaticFields ctx right = some fields → eval env right = Except.ok value → value.hasOnlyFields fieldsleftRecord:Name → Option ValuehLeftEval:eval env left = Except.ok (Value.record leftRecord)⊢ value.hasOnlyFields (leftFields ∪ rightFields) cases hRightEval : eval env right with ctx:StaticContextenv:Envleft:Exprright:ExprleftFields:Finset NamerightFields:Finset Namevalue:ValuehLeftSafe:Expr.staticLetSafe ctx lefthRightSafe:Expr.staticLetSafe ctx righthMatch:EnvMatchesStatic env ctxhLeftStatic:whereStaticFields ctx left = some leftFieldshRightStatic:whereStaticFields ctx right = some rightFieldshEval:eval env (Expr.binary BinaryOp.merge left right) = Except.ok valueleftIH:∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx left → EnvMatchesStatic env ctx → whereStaticFields ctx left = some fields → eval env left = Except.ok value → value.hasOnlyFields fieldsrightIH:∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx right → EnvMatchesStatic env ctx → whereStaticFields ctx right = some fields → eval env right = Except.ok value → value.hasOnlyFields fieldsleftRecord:Name → Option ValuehLeftEval:eval env left = Except.ok (Value.record leftRecord)err:EvalErrorhRightEval:eval env right = Except.error err⊢ value.hasOnlyFields (leftFields ∪ rightFields) All goals completed! 🐙 ctx:StaticContextenv:Envleft:Exprright:ExprleftFields:Finset NamerightFields:Finset Namevalue:ValuehLeftSafe:Expr.staticLetSafe ctx lefthRightSafe:Expr.staticLetSafe ctx righthMatch:EnvMatchesStatic env ctxhLeftStatic:whereStaticFields ctx left = some leftFieldshRightStatic:whereStaticFields ctx right = some rightFieldshEval:eval env (Expr.binary BinaryOp.merge left right) = Except.ok valueleftIH:∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx left → EnvMatchesStatic env ctx → whereStaticFields ctx left = some fields → eval env left = Except.ok value → value.hasOnlyFields fieldsrightIH:∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx right → EnvMatchesStatic env ctx → whereStaticFields ctx right = some fields → eval env right = Except.ok value → value.hasOnlyFields fieldsleftRecord:Name → Option ValuehLeftEval:eval env left = Except.ok (Value.record leftRecord)rightValue:ValuehRightEval:eval env right = Except.ok rightValue⊢ value.hasOnlyFields (leftFields ∪ rightFields) cases rightValue with ctx:StaticContextenv:Envleft:Exprright:ExprleftFields:Finset NamerightFields:Finset Namevalue:ValuehLeftSafe:Expr.staticLetSafe ctx lefthRightSafe:Expr.staticLetSafe ctx righthMatch:EnvMatchesStatic env ctxhLeftStatic:whereStaticFields ctx left = some leftFieldshRightStatic:whereStaticFields ctx right = some rightFieldshEval:eval env (Expr.binary BinaryOp.merge left right) = Except.ok valueleftIH:∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx left → EnvMatchesStatic env ctx → whereStaticFields ctx left = some fields → eval env left = Except.ok value → value.hasOnlyFields fieldsrightIH:∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx right → EnvMatchesStatic env ctx → whereStaticFields ctx right = some fields → eval env right = Except.ok value → value.hasOnlyFields fieldsleftRecord:Name → Option ValuehLeftEval:eval env left = Except.ok (Value.record leftRecord)hRightEval:eval env right = Except.ok Value.null⊢ value.hasOnlyFields (leftFields ∪ rightFields) All goals completed! 🐙 ctx:StaticContextenv:Envleft:Exprright:ExprleftFields:Finset NamerightFields:Finset Namevalue:ValuehLeftSafe:Expr.staticLetSafe ctx lefthRightSafe:Expr.staticLetSafe ctx righthMatch:EnvMatchesStatic env ctxhLeftStatic:whereStaticFields ctx left = some leftFieldshRightStatic:whereStaticFields ctx right = some rightFieldshEval:eval env (Expr.binary BinaryOp.merge left right) = Except.ok valueleftIH:∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx left → EnvMatchesStatic env ctx → whereStaticFields ctx left = some fields → eval env left = Except.ok value → value.hasOnlyFields fieldsrightIH:∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx right → EnvMatchesStatic env ctx → whereStaticFields ctx right = some fields → eval env right = Except.ok value → value.hasOnlyFields fieldsleftRecord:Name → Option ValuehLeftEval:eval env left = Except.ok (Value.record leftRecord)rightBool:BoolhRightEval:eval env right = Except.ok (Value.bool rightBool)⊢ value.hasOnlyFields (leftFields ∪ rightFields) All goals completed! 🐙 ctx:StaticContextenv:Envleft:Exprright:ExprleftFields:Finset NamerightFields:Finset Namevalue:ValuehLeftSafe:Expr.staticLetSafe ctx lefthRightSafe:Expr.staticLetSafe ctx righthMatch:EnvMatchesStatic env ctxhLeftStatic:whereStaticFields ctx left = some leftFieldshRightStatic:whereStaticFields ctx right = some rightFieldshEval:eval env (Expr.binary BinaryOp.merge left right) = Except.ok valueleftIH:∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx left → EnvMatchesStatic env ctx → whereStaticFields ctx left = some fields → eval env left = Except.ok value → value.hasOnlyFields fieldsrightIH:∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx right → EnvMatchesStatic env ctx → whereStaticFields ctx right = some fields → eval env right = Except.ok value → value.hasOnlyFields fieldsleftRecord:Name → Option ValuehLeftEval:eval env left = Except.ok (Value.record leftRecord)rightInt:ℤhRightEval:eval env right = Except.ok (Value.int rightInt)⊢ value.hasOnlyFields (leftFields ∪ rightFields) All goals completed! 🐙 ctx:StaticContextenv:Envleft:Exprright:ExprleftFields:Finset NamerightFields:Finset Namevalue:ValuehLeftSafe:Expr.staticLetSafe ctx lefthRightSafe:Expr.staticLetSafe ctx righthMatch:EnvMatchesStatic env ctxhLeftStatic:whereStaticFields ctx left = some leftFieldshRightStatic:whereStaticFields ctx right = some rightFieldshEval:eval env (Expr.binary BinaryOp.merge left right) = Except.ok valueleftIH:∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx left → EnvMatchesStatic env ctx → whereStaticFields ctx left = some fields → eval env left = Except.ok value → value.hasOnlyFields fieldsrightIH:∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx right → EnvMatchesStatic env ctx → whereStaticFields ctx right = some fields → eval env right = Except.ok value → value.hasOnlyFields fieldsleftRecord:Name → Option ValuehLeftEval:eval env left = Except.ok (Value.record leftRecord)rightString:StringhRightEval:eval env right = Except.ok (Value.string rightString)⊢ value.hasOnlyFields (leftFields ∪ rightFields) All goals completed! 🐙 ctx:StaticContextenv:Envleft:Exprright:ExprleftFields:Finset NamerightFields:Finset Namevalue:ValuehLeftSafe:Expr.staticLetSafe ctx lefthRightSafe:Expr.staticLetSafe ctx righthMatch:EnvMatchesStatic env ctxhLeftStatic:whereStaticFields ctx left = some leftFieldshRightStatic:whereStaticFields ctx right = some rightFieldshEval:eval env (Expr.binary BinaryOp.merge left right) = Except.ok valueleftIH:∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx left → EnvMatchesStatic env ctx → whereStaticFields ctx left = some fields → eval env left = Except.ok value → value.hasOnlyFields fieldsrightIH:∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx right → EnvMatchesStatic env ctx → whereStaticFields ctx right = some fields → eval env right = Except.ok value → value.hasOnlyFields fieldsleftRecord:Name → Option ValuehLeftEval:eval env left = Except.ok (Value.record leftRecord)rightRecord:Name → Option ValuehRightEval:eval env right = Except.ok (Value.record rightRecord)⊢ value.hasOnlyFields (leftFields ∪ rightFields) ctx:StaticContextenv:Envleft:Exprright:ExprleftFields:Finset NamerightFields:Finset Namevalue:ValuehLeftSafe:Expr.staticLetSafe ctx lefthRightSafe:Expr.staticLetSafe ctx righthMatch:EnvMatchesStatic env ctxhLeftStatic:whereStaticFields ctx left = some leftFieldshRightStatic:whereStaticFields ctx right = some rightFieldsleftIH:∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx left → EnvMatchesStatic env ctx → whereStaticFields ctx left = some fields → eval env left = Except.ok value → value.hasOnlyFields fieldsrightIH:∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx right → EnvMatchesStatic env ctx → whereStaticFields ctx right = some fields → eval env right = Except.ok value → value.hasOnlyFields fieldsleftRecord:Name → Option ValuehLeftEval:eval env left = Except.ok (Value.record leftRecord)rightRecord:Name → Option ValuehRightEval:eval env right = Except.ok (Value.record rightRecord)hEval:Value.record (mergeRecordFields leftRecord rightRecord) = value⊢ value.hasOnlyFields (leftFields ∪ rightFields) ctx:StaticContextenv:Envleft:Exprright:ExprleftFields:Finset NamerightFields:Finset NamehLeftSafe:Expr.staticLetSafe ctx lefthRightSafe:Expr.staticLetSafe ctx righthMatch:EnvMatchesStatic env ctxhLeftStatic:whereStaticFields ctx left = some leftFieldshRightStatic:whereStaticFields ctx right = some rightFieldsleftIH:∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx left → EnvMatchesStatic env ctx → whereStaticFields ctx left = some fields → eval env left = Except.ok value → value.hasOnlyFields fieldsrightIH:∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx right → EnvMatchesStatic env ctx → whereStaticFields ctx right = some fields → eval env right = Except.ok value → value.hasOnlyFields fieldsleftRecord:Name → Option ValuehLeftEval:eval env left = Except.ok (Value.record leftRecord)rightRecord:Name → Option ValuehRightEval:eval env right = Except.ok (Value.record rightRecord)⊢ (Value.record (mergeRecordFields leftRecord rightRecord)).hasOnlyFields (leftFields ∪ rightFields) ctx:StaticContextenv:Envleft:Exprright:ExprleftFields:Finset NamerightFields:Finset NamehLeftSafe:Expr.staticLetSafe ctx lefthRightSafe:Expr.staticLetSafe ctx righthMatch:EnvMatchesStatic env ctxhLeftStatic:whereStaticFields ctx left = some leftFieldshRightStatic:whereStaticFields ctx right = some rightFieldsleftIH:∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx left → EnvMatchesStatic env ctx → whereStaticFields ctx left = some fields → eval env left = Except.ok value → value.hasOnlyFields fieldsrightIH:∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx right → EnvMatchesStatic env ctx → whereStaticFields ctx right = some fields → eval env right = Except.ok value → value.hasOnlyFields fieldsleftRecord:Name → Option ValuehLeftEval:eval env left = Except.ok (Value.record leftRecord)rightRecord:Name → Option ValuehRightEval:eval env right = Except.ok (Value.record rightRecord)hLeftHas:(Value.record leftRecord).hasOnlyFields leftFields⊢ (Value.record (mergeRecordFields leftRecord rightRecord)).hasOnlyFields (leftFields ∪ rightFields) ctx:StaticContextenv:Envleft:Exprright:ExprleftFields:Finset NamerightFields:Finset NamehLeftSafe:Expr.staticLetSafe ctx lefthRightSafe:Expr.staticLetSafe ctx righthMatch:EnvMatchesStatic env ctxhLeftStatic:whereStaticFields ctx left = some leftFieldshRightStatic:whereStaticFields ctx right = some rightFieldsleftIH:∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx left → EnvMatchesStatic env ctx → whereStaticFields ctx left = some fields → eval env left = Except.ok value → value.hasOnlyFields fieldsrightIH:∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx right → EnvMatchesStatic env ctx → whereStaticFields ctx right = some fields → eval env right = Except.ok value → value.hasOnlyFields fieldsleftRecord:Name → Option ValuehLeftEval:eval env left = Except.ok (Value.record leftRecord)rightRecord:Name → Option ValuehRightEval:eval env right = Except.ok (Value.record rightRecord)hLeftHas:(Value.record leftRecord).hasOnlyFields leftFieldshRightHas:(Value.record rightRecord).hasOnlyFields rightFields⊢ (Value.record (mergeRecordFields leftRecord rightRecord)).hasOnlyFields (leftFields ∪ rightFields) All goals completed! 🐙

Core recursive proof for static where field soundness.

private theorem whereStaticFields_sound_expr (expr : Expr) : ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → Value.hasOnlyFields value fields := Expr.rec (motive_1 := fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → Value.hasOnlyFields value fields) (motive_2 := fun _bindings => True) (motive_3 := fun _binding => True) (fun literalValue {ctx env fields value} hSafe hMatch hStatic hEval => expr:Exprctx✝:StaticContextenv✝:Envfields✝:Finset Namevalue✝:ValueliteralValue:Valuectx:StaticContextenv:Envfields:Finset Namevalue:ValuehSafe:Expr.staticLetSafe ctx (Expr.lit literalValue)hMatch:EnvMatchesStatic env ctxhStatic:whereStaticFields ctx (Expr.lit literalValue) = some fieldshEval:eval env (Expr.lit literalValue) = Except.ok value⊢ value.hasOnlyFields fields All goals completed! 🐙) (fun name {ctx env fields value} hSafe hMatch hStatic hEval => expr:Exprctx✝:StaticContextenv✝:Envfields✝:Finset Namevalue✝:Valuename:Namectx:StaticContextenv:Envfields:Finset Namevalue:ValuehSafe:Expr.staticLetSafe ctx (Expr.var name)hMatch:EnvMatchesStatic env ctxhStatic:whereStaticFields ctx (Expr.var name) = some fieldshEval:eval env (Expr.var name) = Except.ok value⊢ value.hasOnlyFields fields exact hMatch name fields value hStatic (expr:Exprctx✝:StaticContextenv✝:Envfields✝:Finset Namevalue✝:Valuename:Namectx:StaticContextenv:Envfields:Finset Namevalue:ValuehSafe:Expr.staticLetSafe ctx (Expr.var name)hMatch:EnvMatchesStatic env ctxhStatic:whereStaticFields ctx (Expr.var name) = some fieldshEval:eval env (Expr.var name) = Except.ok value⊢ env name = some value cases hLookup : env name with expr:Exprctx✝:StaticContextenv✝:Envfields✝:Finset Namevalue✝:Valuename:Namectx:StaticContextenv:Envfields:Finset Namevalue:ValuehSafe:Expr.staticLetSafe ctx (Expr.var name)hMatch:EnvMatchesStatic env ctxhStatic:whereStaticFields ctx (Expr.var name) = some fieldshEval:eval env (Expr.var name) = Except.ok valuehLookup:env name = none⊢ none = some value All goals completed! 🐙 expr:Exprctx✝:StaticContextenv✝:Envfields✝:Finset Namevalue✝:Valuename:Namectx:StaticContextenv:Envfields:Finset Namevalue:ValuehSafe:Expr.staticLetSafe ctx (Expr.var name)hMatch:EnvMatchesStatic env ctxhStatic:whereStaticFields ctx (Expr.var name) = some fieldshEval:eval env (Expr.var name) = Except.ok valueenvValue:ValuehLookup:env name = some envValue⊢ some envValue = some value expr:Exprctx✝:StaticContextenv✝:Envfields✝:Finset Namevalue✝:Valuename:Namectx:StaticContextenv:Envfields:Finset Namevalue:ValuehSafe:Expr.staticLetSafe ctx (Expr.var name)hMatch:EnvMatchesStatic env ctxhStatic:whereStaticFields ctx (Expr.var name) = some fieldsenvValue:ValuehLookup:env name = some envValuehEval:envValue = value⊢ some envValue = some value expr:Exprctx✝:StaticContextenv✝:Envfields✝:Finset Namevalue✝:Valuename:Namectx:StaticContextenv:Envfields:Finset Namevalue:ValuehSafe:Expr.staticLetSafe ctx (Expr.var name)hMatch:EnvMatchesStatic env ctxhStatic:whereStaticFields ctx (Expr.var name) = some fieldshLookup:env name = some value⊢ some value = some value All goals completed! 🐙)) (fun fields _fieldsIH {ctx env staticFields value} hSafe hMatch hStatic hEval => expr:Exprctx✝:StaticContextenv✝:Envfields✝:Finset Namevalue✝:Valuefields:List (Name × Expr)_fieldsIH:(fun _bindings => True) fieldsctx:StaticContextenv:EnvstaticFields:Finset Namevalue:ValuehSafe:Expr.staticLetSafe ctx (Expr.record fields)hMatch:EnvMatchesStatic env ctxhStatic:whereStaticFields ctx (Expr.record fields) = some staticFieldshEval:eval env (Expr.record fields) = Except.ok value⊢ value.hasOnlyFields staticFields expr:Exprctx✝:StaticContextenv✝:Envfields✝:Finset Namevalue✝:Valuefields:List (Name × Expr)_fieldsIH:(fun _bindings => True) fieldsctx:StaticContextenv:Envvalue:ValuehSafe:Expr.staticLetSafe ctx (Expr.record fields)hMatch:EnvMatchesStatic env ctxhEval:eval env (Expr.record fields) = Except.ok value⊢ value.hasOnlyFields (fieldNameSet fields) All goals completed! 🐙) (fun base fieldName _baseIH {ctx env fields value} hSafe hMatch hStatic hEval => expr:Exprctx✝:StaticContextenv✝:Envfields✝:Finset Namevalue✝:Valuebase:ExprfieldName:Name_baseIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) basectx:StaticContextenv:Envfields:Finset Namevalue:ValuehSafe:Expr.staticLetSafe ctx (base.field fieldName)hMatch:EnvMatchesStatic env ctxhStatic:whereStaticFields ctx (base.field fieldName) = some fieldshEval:eval env (base.field fieldName) = Except.ok value⊢ value.hasOnlyFields fields All goals completed! 🐙) (fun bindings body _bindingsIH bodyIH {ctx env fields value} hSafe hMatch hStatic hEval => expr:Exprctx✝:StaticContextenv✝:Envfields✝:Finset Namevalue✝:Valuebindings:List (Name × Expr)body:Expr_bindingsIH:(fun _bindings => True) bindingsbodyIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) bodyctx:StaticContextenv:Envfields:Finset Namevalue:ValuehSafe:Expr.staticLetSafe ctx (Expr.letE bindings body)hMatch:EnvMatchesStatic env ctxhStatic:whereStaticFields ctx (Expr.letE bindings body) = some fieldshEval:eval env (Expr.letE bindings body) = Except.ok value⊢ value.hasOnlyFields fields expr:Exprctx✝:StaticContextenv✝:Envfields✝:Finset Namevalue✝:Valuebindings:List (Name × Expr)body:Expr_bindingsIH:(fun _bindings => True) bindingsbodyIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) bodyctx:StaticContextenv:Envfields:Finset Namevalue:ValuehSafe:Expr.staticLetSafe ctx (Expr.letE bindings body)hMatch:EnvMatchesStatic env ctxhStatic:whereStaticFields ctx (Expr.letE bindings body) = some fieldshEval:eval env (Expr.letE bindings body) = Except.ok valuehNoShadow:letBindingsDoNotShadowStatic ctx bindings⊢ value.hasOnlyFields fields expr:Exprctx✝:StaticContextenv✝:Envfields✝:Finset Namevalue✝:Valuebindings:List (Name × Expr)body:Expr_bindingsIH:(fun _bindings => True) bindingsbodyIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) bodyctx:StaticContextenv:Envfields:Finset Namevalue:ValuehSafe:Expr.staticLetSafe ctx (Expr.letE bindings body)hMatch:EnvMatchesStatic env ctxhStatic:whereStaticFields ctx (Expr.letE bindings body) = some fieldshEval:eval env (Expr.letE bindings body) = Except.ok valuehNoShadow:letBindingsDoNotShadowStatic ctx bindingshBodySafe:Expr.staticLetSafe ctx body⊢ value.hasOnlyFields fields expr:Exprctx✝:StaticContextenv✝:Envfields✝:Finset Namevalue✝:Valuebindings:List (Name × Expr)body:Expr_bindingsIH:(fun _bindings => True) bindingsbodyIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) bodyctx:StaticContextenv:Envfields:Finset Namevalue:ValuehSafe:Expr.staticLetSafe ctx (Expr.letE bindings body)hMatch:EnvMatchesStatic env ctxhStatic:whereStaticFields ctx body = some fieldshEval:eval env (Expr.letE bindings body) = Except.ok valuehNoShadow:letBindingsDoNotShadowStatic ctx bindingshBodySafe:Expr.staticLetSafe ctx body⊢ value.hasOnlyFields fields cases hBindings : evalBindings env bindings with expr:Exprctx✝:StaticContextenv✝:Envfields✝:Finset Namevalue✝:Valuebindings:List (Name × Expr)body:Expr_bindingsIH:(fun _bindings => True) bindingsbodyIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) bodyctx:StaticContextenv:Envfields:Finset Namevalue:ValuehSafe:Expr.staticLetSafe ctx (Expr.letE bindings body)hMatch:EnvMatchesStatic env ctxhStatic:whereStaticFields ctx body = some fieldshEval:eval env (Expr.letE bindings body) = Except.ok valuehNoShadow:letBindingsDoNotShadowStatic ctx bindingshBodySafe:Expr.staticLetSafe ctx bodyerr:EvalErrorhBindings:evalBindings env bindings = Except.error err⊢ value.hasOnlyFields fields All goals completed! 🐙 expr:Exprctx✝:StaticContextenv✝:Envfields✝:Finset Namevalue✝:Valuebindings:List (Name × Expr)body:Expr_bindingsIH:(fun _bindings => True) bindingsbodyIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) bodyctx:StaticContextenv:Envfields:Finset Namevalue:ValuehSafe:Expr.staticLetSafe ctx (Expr.letE bindings body)hMatch:EnvMatchesStatic env ctxhStatic:whereStaticFields ctx body = some fieldshEval:eval env (Expr.letE bindings body) = Except.ok valuehNoShadow:letBindingsDoNotShadowStatic ctx bindingshBodySafe:Expr.staticLetSafe ctx bodylocalEnv:EnvhBindings:evalBindings env bindings = Except.ok localEnv⊢ value.hasOnlyFields fields expr:Exprctx✝:StaticContextenv✝:Envfields✝:Finset Namevalue✝:Valuebindings:List (Name × Expr)body:Expr_bindingsIH:(fun _bindings => True) bindingsbodyIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) bodyctx:StaticContextenv:Envfields:Finset Namevalue:ValuehSafe:Expr.staticLetSafe ctx (Expr.letE bindings body)hMatch:EnvMatchesStatic env ctxhStatic:whereStaticFields ctx body = some fieldshEval:eval env (Expr.letE bindings body) = Except.ok valuehNoShadow:letBindingsDoNotShadowStatic ctx bindingshBodySafe:Expr.staticLetSafe ctx bodylocalEnv:EnvhBindings:evalBindings env bindings = Except.ok localEnvhLocalMatch:EnvMatchesStatic localEnv ctx⊢ value.hasOnlyFields fields have hBodyEval : eval localEnv body = Except.ok value := expr:Exprctx✝:StaticContextenv✝:Envfields✝:Finset Namevalue✝:Valuebindings:List (Name × Expr)body:Expr_bindingsIH:(fun _bindings => True) bindingsbodyIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) bodyctx:StaticContextenv:Envfields:Finset Namevalue:ValuehSafe:Expr.staticLetSafe ctx (Expr.letE bindings body)hMatch:EnvMatchesStatic env ctxhStatic:whereStaticFields ctx (Expr.letE bindings body) = some fieldshEval:eval env (Expr.letE bindings body) = Except.ok value⊢ value.hasOnlyFields fields All goals completed! 🐙 All goals completed! 🐙) (fun condition thenExpr elseExpr _conditionIH _thenIH _elseIH {ctx env fields value} hSafe hMatch hStatic hEval => expr:Exprctx✝:StaticContextenv✝:Envfields✝:Finset Namevalue✝:Valuecondition:ExprthenExpr:ExprelseExpr:Expr_conditionIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) condition_thenIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) thenExpr_elseIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) elseExprctx:StaticContextenv:Envfields:Finset Namevalue:ValuehSafe:Expr.staticLetSafe ctx (condition.ifE thenExpr elseExpr)hMatch:EnvMatchesStatic env ctxhStatic:whereStaticFields ctx (condition.ifE thenExpr elseExpr) = some fieldshEval:eval env (condition.ifE thenExpr elseExpr) = Except.ok value⊢ value.hasOnlyFields fields All goals completed! 🐙) (fun op operand _operandIH {ctx env fields value} hSafe hMatch hStatic hEval => expr:Exprctx✝:StaticContextenv✝:Envfields✝:Finset Namevalue✝:Valueop:UnaryOpoperand:Expr_operandIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) operandctx:StaticContextenv:Envfields:Finset Namevalue:ValuehSafe:Expr.staticLetSafe ctx (Expr.unary op operand)hMatch:EnvMatchesStatic env ctxhStatic:whereStaticFields ctx (Expr.unary op operand) = some fieldshEval:eval env (Expr.unary op operand) = Except.ok value⊢ value.hasOnlyFields fields All goals completed! 🐙) (fun op left right leftIH rightIH {ctx env fields value} hSafe hMatch hStatic hEval => expr:Exprctx✝:StaticContextenv✝:Envfields✝:Finset Namevalue✝:Valueop:BinaryOpleft:Exprright:ExprleftIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) leftrightIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) rightctx:StaticContextenv:Envfields:Finset Namevalue:ValuehSafe:Expr.staticLetSafe ctx (Expr.binary op left right)hMatch:EnvMatchesStatic env ctxhStatic:whereStaticFields ctx (Expr.binary op left right) = some fieldshEval:eval env (Expr.binary op left right) = Except.ok value⊢ value.hasOnlyFields fields cases op with expr:Exprctx✝:StaticContextenv✝:Envfields✝:Finset Namevalue✝:Valueleft:Exprright:ExprleftIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) leftrightIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) rightctx:StaticContextenv:Envfields:Finset Namevalue:ValuehMatch:EnvMatchesStatic env ctxhSafe:Expr.staticLetSafe ctx (Expr.binary BinaryOp.add left right)hStatic:whereStaticFields ctx (Expr.binary BinaryOp.add left right) = some fieldshEval:eval env (Expr.binary BinaryOp.add left right) = Except.ok value⊢ value.hasOnlyFields fields All goals completed! 🐙 expr:Exprctx✝:StaticContextenv✝:Envfields✝:Finset Namevalue✝:Valueleft:Exprright:ExprleftIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) leftrightIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) rightctx:StaticContextenv:Envfields:Finset Namevalue:ValuehMatch:EnvMatchesStatic env ctxhSafe:Expr.staticLetSafe ctx (Expr.binary BinaryOp.subtract left right)hStatic:whereStaticFields ctx (Expr.binary BinaryOp.subtract left right) = some fieldshEval:eval env (Expr.binary BinaryOp.subtract left right) = Except.ok value⊢ value.hasOnlyFields fields All goals completed! 🐙 expr:Exprctx✝:StaticContextenv✝:Envfields✝:Finset Namevalue✝:Valueleft:Exprright:ExprleftIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) leftrightIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) rightctx:StaticContextenv:Envfields:Finset Namevalue:ValuehMatch:EnvMatchesStatic env ctxhSafe:Expr.staticLetSafe ctx (Expr.binary BinaryOp.multiply left right)hStatic:whereStaticFields ctx (Expr.binary BinaryOp.multiply left right) = some fieldshEval:eval env (Expr.binary BinaryOp.multiply left right) = Except.ok value⊢ value.hasOnlyFields fields All goals completed! 🐙 expr:Exprctx✝:StaticContextenv✝:Envfields✝:Finset Namevalue✝:Valueleft:Exprright:ExprleftIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) leftrightIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) rightctx:StaticContextenv:Envfields:Finset Namevalue:ValuehMatch:EnvMatchesStatic env ctxhSafe:Expr.staticLetSafe ctx (Expr.binary BinaryOp.and left right)hStatic:whereStaticFields ctx (Expr.binary BinaryOp.and left right) = some fieldshEval:eval env (Expr.binary BinaryOp.and left right) = Except.ok value⊢ value.hasOnlyFields fields All goals completed! 🐙 expr:Exprctx✝:StaticContextenv✝:Envfields✝:Finset Namevalue✝:Valueleft:Exprright:ExprleftIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) leftrightIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) rightctx:StaticContextenv:Envfields:Finset Namevalue:ValuehMatch:EnvMatchesStatic env ctxhSafe:Expr.staticLetSafe ctx (Expr.binary BinaryOp.or left right)hStatic:whereStaticFields ctx (Expr.binary BinaryOp.or left right) = some fieldshEval:eval env (Expr.binary BinaryOp.or left right) = Except.ok value⊢ value.hasOnlyFields fields All goals completed! 🐙 expr:Exprctx✝:StaticContextenv✝:Envfields✝:Finset Namevalue✝:Valueleft:Exprright:ExprleftIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) leftrightIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) rightctx:StaticContextenv:Envfields:Finset Namevalue:ValuehMatch:EnvMatchesStatic env ctxhSafe:Expr.staticLetSafe ctx (Expr.binary BinaryOp.merge left right)hStatic:whereStaticFields ctx (Expr.binary BinaryOp.merge left right) = some fieldshEval:eval env (Expr.binary BinaryOp.merge left right) = Except.ok value⊢ value.hasOnlyFields fields expr:Exprctx✝:StaticContextenv✝:Envfields✝:Finset Namevalue✝:Valueleft:Exprright:ExprleftIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) leftrightIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) rightctx:StaticContextenv:Envfields:Finset Namevalue:ValuehMatch:EnvMatchesStatic env ctxhSafe:Expr.staticLetSafe ctx (Expr.binary BinaryOp.merge left right)hStatic:whereStaticFields ctx (Expr.binary BinaryOp.merge left right) = some fieldshEval:eval env (Expr.binary BinaryOp.merge left right) = Except.ok valuehLeftSafe:Expr.staticLetSafe ctx left⊢ value.hasOnlyFields fields expr:Exprctx✝:StaticContextenv✝:Envfields✝:Finset Namevalue✝:Valueleft:Exprright:ExprleftIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) leftrightIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) rightctx:StaticContextenv:Envfields:Finset Namevalue:ValuehMatch:EnvMatchesStatic env ctxhSafe:Expr.staticLetSafe ctx (Expr.binary BinaryOp.merge left right)hStatic:whereStaticFields ctx (Expr.binary BinaryOp.merge left right) = some fieldshEval:eval env (Expr.binary BinaryOp.merge left right) = Except.ok valuehLeftSafe:Expr.staticLetSafe ctx lefthRightSafe:Expr.staticLetSafe ctx right⊢ value.hasOnlyFields fields cases hLeftStatic : whereStaticFields ctx left with expr:Exprctx✝:StaticContextenv✝:Envfields✝:Finset Namevalue✝:Valueleft:Exprright:ExprleftIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) leftrightIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) rightctx:StaticContextenv:Envfields:Finset Namevalue:ValuehMatch:EnvMatchesStatic env ctxhSafe:Expr.staticLetSafe ctx (Expr.binary BinaryOp.merge left right)hStatic:whereStaticFields ctx (Expr.binary BinaryOp.merge left right) = some fieldshEval:eval env (Expr.binary BinaryOp.merge left right) = Except.ok valuehLeftSafe:Expr.staticLetSafe ctx lefthRightSafe:Expr.staticLetSafe ctx righthLeftStatic:whereStaticFields ctx left = none⊢ value.hasOnlyFields fields cases hRightStatic : whereStaticFields ctx right with expr:Exprctx✝:StaticContextenv✝:Envfields✝:Finset Namevalue✝:Valueleft:Exprright:ExprleftIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) leftrightIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) rightctx:StaticContextenv:Envfields:Finset Namevalue:ValuehMatch:EnvMatchesStatic env ctxhSafe:Expr.staticLetSafe ctx (Expr.binary BinaryOp.merge left right)hStatic:whereStaticFields ctx (Expr.binary BinaryOp.merge left right) = some fieldshEval:eval env (Expr.binary BinaryOp.merge left right) = Except.ok valuehLeftSafe:Expr.staticLetSafe ctx lefthRightSafe:Expr.staticLetSafe ctx righthLeftStatic:whereStaticFields ctx left = nonehRightStatic:whereStaticFields ctx right = none⊢ value.hasOnlyFields fields All goals completed! 🐙 expr:Exprctx✝:StaticContextenv✝:Envfields✝:Finset Namevalue✝:Valueleft:Exprright:ExprleftIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) leftrightIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) rightctx:StaticContextenv:Envfields:Finset Namevalue:ValuehMatch:EnvMatchesStatic env ctxhSafe:Expr.staticLetSafe ctx (Expr.binary BinaryOp.merge left right)hStatic:whereStaticFields ctx (Expr.binary BinaryOp.merge left right) = some fieldshEval:eval env (Expr.binary BinaryOp.merge left right) = Except.ok valuehLeftSafe:Expr.staticLetSafe ctx lefthRightSafe:Expr.staticLetSafe ctx righthLeftStatic:whereStaticFields ctx left = nonerightFields:Finset NamehRightStatic:whereStaticFields ctx right = some rightFields⊢ value.hasOnlyFields fields All goals completed! 🐙 expr:Exprctx✝:StaticContextenv✝:Envfields✝:Finset Namevalue✝:Valueleft:Exprright:ExprleftIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) leftrightIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) rightctx:StaticContextenv:Envfields:Finset Namevalue:ValuehMatch:EnvMatchesStatic env ctxhSafe:Expr.staticLetSafe ctx (Expr.binary BinaryOp.merge left right)hStatic:whereStaticFields ctx (Expr.binary BinaryOp.merge left right) = some fieldshEval:eval env (Expr.binary BinaryOp.merge left right) = Except.ok valuehLeftSafe:Expr.staticLetSafe ctx lefthRightSafe:Expr.staticLetSafe ctx rightleftFields:Finset NamehLeftStatic:whereStaticFields ctx left = some leftFields⊢ value.hasOnlyFields fields cases hRightStatic : whereStaticFields ctx right with expr:Exprctx✝:StaticContextenv✝:Envfields✝:Finset Namevalue✝:Valueleft:Exprright:ExprleftIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) leftrightIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) rightctx:StaticContextenv:Envfields:Finset Namevalue:ValuehMatch:EnvMatchesStatic env ctxhSafe:Expr.staticLetSafe ctx (Expr.binary BinaryOp.merge left right)hStatic:whereStaticFields ctx (Expr.binary BinaryOp.merge left right) = some fieldshEval:eval env (Expr.binary BinaryOp.merge left right) = Except.ok valuehLeftSafe:Expr.staticLetSafe ctx lefthRightSafe:Expr.staticLetSafe ctx rightleftFields:Finset NamehLeftStatic:whereStaticFields ctx left = some leftFieldshRightStatic:whereStaticFields ctx right = none⊢ value.hasOnlyFields fields All goals completed! 🐙 expr:Exprctx✝:StaticContextenv✝:Envfields✝:Finset Namevalue✝:Valueleft:Exprright:ExprleftIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) leftrightIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) rightctx:StaticContextenv:Envfields:Finset Namevalue:ValuehMatch:EnvMatchesStatic env ctxhSafe:Expr.staticLetSafe ctx (Expr.binary BinaryOp.merge left right)hStatic:whereStaticFields ctx (Expr.binary BinaryOp.merge left right) = some fieldshEval:eval env (Expr.binary BinaryOp.merge left right) = Except.ok valuehLeftSafe:Expr.staticLetSafe ctx lefthRightSafe:Expr.staticLetSafe ctx rightleftFields:Finset NamehLeftStatic:whereStaticFields ctx left = some leftFieldsrightFields:Finset NamehRightStatic:whereStaticFields ctx right = some rightFields⊢ value.hasOnlyFields fields expr:Exprctx✝:StaticContextenv✝:Envfields✝:Finset Namevalue✝:Valueleft:Exprright:ExprleftIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) leftrightIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) rightctx:StaticContextenv:Envfields:Finset Namevalue:ValuehMatch:EnvMatchesStatic env ctxhSafe:Expr.staticLetSafe ctx (Expr.binary BinaryOp.merge left right)hEval:eval env (Expr.binary BinaryOp.merge left right) = Except.ok valuehLeftSafe:Expr.staticLetSafe ctx lefthRightSafe:Expr.staticLetSafe ctx rightleftFields:Finset NamehLeftStatic:whereStaticFields ctx left = some leftFieldsrightFields:Finset NamehRightStatic:whereStaticFields ctx right = some rightFieldshStatic:leftFields ∪ rightFields = fields⊢ value.hasOnlyFields fields expr:Exprctx✝:StaticContextenv✝:Envfields✝:Finset Namevalue✝:Valueleft:Exprright:ExprleftIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) leftrightIH:(fun expr => ∀ {ctx : StaticContext} {env : Env} {fields : Finset Name} {value : Value}, Expr.staticLetSafe ctx expr → EnvMatchesStatic env ctx → whereStaticFields ctx expr = some fields → eval env expr = Except.ok value → value.hasOnlyFields fields) rightctx:StaticContextenv:Envvalue:ValuehMatch:EnvMatchesStatic env ctxhSafe:Expr.staticLetSafe ctx (Expr.binary BinaryOp.merge left right)hEval:eval env (Expr.binary BinaryOp.merge left right) = Except.ok valuehLeftSafe:Expr.staticLetSafe ctx lefthRightSafe:Expr.staticLetSafe ctx rightleftFields:Finset NamehLeftStatic:whereStaticFields ctx left = some leftFieldsrightFields:Finset NamehRightStatic:whereStaticFields ctx right = some rightFields⊢ value.hasOnlyFields (leftFields ∪ rightFields) All goals completed! 🐙) True.intro (fun head tail _headIH _tailIH => True.intro) (fun bindingName bindingExpr _exprIH => True.intro) expr

Static field discovery is sound for safe expressions in matching runtime environments.

theorem whereStaticFields_sound {ctx : StaticContext} {env : Env} {expr : Expr} {fields : Finset Name} {value : Value} (hSafe : Expr.staticLetSafe ctx expr) (hMatch : EnvMatchesStatic env ctx) (hStatic : whereStaticFields ctx expr = some fields) (hEval : eval env expr = Except.ok value) : Value.hasOnlyFields value fields := whereStaticFields_sound_expr expr hSafe hMatch hStatic hEval

A top-level binding with a static-context entry evaluates to a value with those fields.

theorem topLevelBinding_value_hasOnlyFields {ctx : StaticContext} {env : Env} {bindings : List (Name × Expr)} {name : Name} {expr : Expr} {fields : Finset Name} {value : Value} (hBindings : TopLevelBindingStatics ctx bindings) (hMatch : EnvMatchesStatic env ctx) (hMember : (name, expr) ∈ bindings) (hStatic : ctx name = some fields) (hEval : eval env expr = Except.ok value) : Value.hasOnlyFields value fields := ctx:StaticContextenv:Envbindings:List (Name × Expr)name:Nameexpr:Exprfields:Finset Namevalue:ValuehBindings:TopLevelBindingStatics ctx bindingshMatch:EnvMatchesStatic env ctxhMember:(name, expr) ∈ bindingshStatic:ctx name = some fieldshEval:eval env expr = Except.ok value⊢ value.hasOnlyFields fields ctx:StaticContextenv:Envbindings:List (Name × Expr)name:Nameexpr:Exprfields:Finset Namevalue:ValuehBindings:TopLevelBindingStatics ctx bindingshMatch:EnvMatchesStatic env ctxhMember:(name, expr) ∈ bindingshStatic:ctx name = some fieldshEval:eval env expr = Except.ok valuehBinding:Expr.staticLetSafe ctx expr ∧ whereStaticFields ctx expr = some fields⊢ value.hasOnlyFields fields All goals completed! 🐙

Evaluating non-duplicate top-level bindings preserves the static context they establish.

private theorem evalBindingsNoDuplicate_establish_staticContext {ctx : StaticContext} {env localEnv : Env} {bindings : List (Name × Expr)} (hBindings : TopLevelBindingStatics ctx bindings) (hMatch : EnvMatchesStatic env ctx) (hEval : evalBindingsNoDuplicate env bindings = Except.ok localEnv) : EnvMatchesStatic localEnv ctx := ctx:StaticContextenv:EnvlocalEnv:Envbindings:List (Name × Expr)hBindings:TopLevelBindingStatics ctx bindingshMatch:EnvMatchesStatic env ctxhEval:evalBindingsNoDuplicate env bindings = Except.ok localEnv⊢ EnvMatchesStatic localEnv ctx induction bindings generalizing env localEnv with ctx:StaticContextenv:EnvlocalEnv:EnvhBindings:TopLevelBindingStatics ctx []hMatch:EnvMatchesStatic env ctxhEval:evalBindingsNoDuplicate env [] = Except.ok localEnv⊢ EnvMatchesStatic localEnv ctx ctx:StaticContextenv:EnvlocalEnv:EnvhBindings:TopLevelBindingStatics ctx []hMatch:EnvMatchesStatic env ctxhEval:env = localEnv⊢ EnvMatchesStatic localEnv ctx ctx:StaticContextenv:EnvhBindings:TopLevelBindingStatics ctx []hMatch:EnvMatchesStatic env ctx⊢ EnvMatchesStatic env ctx All goals completed! 🐙 ctx:StaticContexthead:Name × Exprtail:List (Name × Expr)ih:∀ {env localEnv : Env}, TopLevelBindingStatics ctx tail → EnvMatchesStatic env ctx → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxenv:EnvlocalEnv:EnvhBindings:TopLevelBindingStatics ctx (head :: tail)hMatch:EnvMatchesStatic env ctxhEval:evalBindingsNoDuplicate env (head :: tail) = Except.ok localEnv⊢ EnvMatchesStatic localEnv ctx ctx:StaticContexttail:List (Name × Expr)ih:∀ {env localEnv : Env}, TopLevelBindingStatics ctx tail → EnvMatchesStatic env ctx → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhBindings:TopLevelBindingStatics ctx ((bindingName, bindingExpr) :: tail)hEval:evalBindingsNoDuplicate env ((bindingName, bindingExpr) :: tail) = Except.ok localEnv⊢ EnvMatchesStatic localEnv ctx have hTailBindings : TopLevelBindingStatics ctx tail := ctx:StaticContextenv:EnvlocalEnv:Envbindings:List (Name × Expr)hBindings:TopLevelBindingStatics ctx bindingshMatch:EnvMatchesStatic env ctxhEval:evalBindingsNoDuplicate env bindings = Except.ok localEnv⊢ EnvMatchesStatic localEnv ctx intro name ctx:StaticContexttail:List (Name × Expr)ih:∀ {env localEnv : Env}, TopLevelBindingStatics ctx tail → EnvMatchesStatic env ctx → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhBindings:TopLevelBindingStatics ctx ((bindingName, bindingExpr) :: tail)hEval:evalBindingsNoDuplicate env ((bindingName, bindingExpr) :: tail) = Except.ok localEnvname:Nameexpr:Expr⊢ ∀ (fields : Finset Name), (name, expr) ∈ tail → ctx name = some fields → Expr.staticLetSafe ctx expr ∧ whereStaticFields ctx expr = some fields ctx:StaticContexttail:List (Name × Expr)ih:∀ {env localEnv : Env}, TopLevelBindingStatics ctx tail → EnvMatchesStatic env ctx → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhBindings:TopLevelBindingStatics ctx ((bindingName, bindingExpr) :: tail)hEval:evalBindingsNoDuplicate env ((bindingName, bindingExpr) :: tail) = Except.ok localEnvname:Nameexpr:Exprfields:Finset Name⊢ (name, expr) ∈ tail → ctx name = some fields → Expr.staticLetSafe ctx expr ∧ whereStaticFields ctx expr = some fields ctx:StaticContexttail:List (Name × Expr)ih:∀ {env localEnv : Env}, TopLevelBindingStatics ctx tail → EnvMatchesStatic env ctx → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhBindings:TopLevelBindingStatics ctx ((bindingName, bindingExpr) :: tail)hEval:evalBindingsNoDuplicate env ((bindingName, bindingExpr) :: tail) = Except.ok localEnvname:Nameexpr:Exprfields:Finset NamehMember:(name, expr) ∈ tail⊢ ctx name = some fields → Expr.staticLetSafe ctx expr ∧ whereStaticFields ctx expr = some fields ctx:StaticContexttail:List (Name × Expr)ih:∀ {env localEnv : Env}, TopLevelBindingStatics ctx tail → EnvMatchesStatic env ctx → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhBindings:TopLevelBindingStatics ctx ((bindingName, bindingExpr) :: tail)hEval:evalBindingsNoDuplicate env ((bindingName, bindingExpr) :: tail) = Except.ok localEnvname:Nameexpr:Exprfields:Finset NamehMember:(name, expr) ∈ tailhStatic:ctx name = some fields⊢ Expr.staticLetSafe ctx expr ∧ whereStaticFields ctx expr = some fields All goals completed! 🐙 ctx:StaticContexttail:List (Name × Expr)ih:∀ {env localEnv : Env}, TopLevelBindingStatics ctx tail → EnvMatchesStatic env ctx → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhBindings:TopLevelBindingStatics ctx ((bindingName, bindingExpr) :: tail)hTailBindings:TopLevelBindingStatics ctx tailhEval:(match eval env bindingExpr with | Except.ok bindingValue => evalBindingsNoDuplicate (Env.insert bindingName bindingValue env) tail | Except.error err => Except.error err) = Except.ok localEnv⊢ EnvMatchesStatic localEnv ctx cases hBindingEval : eval env bindingExpr with ctx:StaticContexttail:List (Name × Expr)ih:∀ {env localEnv : Env}, TopLevelBindingStatics ctx tail → EnvMatchesStatic env ctx → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhBindings:TopLevelBindingStatics ctx ((bindingName, bindingExpr) :: tail)hTailBindings:TopLevelBindingStatics ctx tailhEval:(match eval env bindingExpr with | Except.ok bindingValue => evalBindingsNoDuplicate (Env.insert bindingName bindingValue env) tail | Except.error err => Except.error err) = Except.ok localEnverr:EvalErrorhBindingEval:eval env bindingExpr = Except.error err⊢ EnvMatchesStatic localEnv ctx All goals completed! 🐙 ctx:StaticContexttail:List (Name × Expr)ih:∀ {env localEnv : Env}, TopLevelBindingStatics ctx tail → EnvMatchesStatic env ctx → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhBindings:TopLevelBindingStatics ctx ((bindingName, bindingExpr) :: tail)hTailBindings:TopLevelBindingStatics ctx tailhEval:(match eval env bindingExpr with | Except.ok bindingValue => evalBindingsNoDuplicate (Env.insert bindingName bindingValue env) tail | Except.error err => Except.error err) = Except.ok localEnvbindingValue:ValuehBindingEval:eval env bindingExpr = Except.ok bindingValue⊢ EnvMatchesStatic localEnv ctx ctx:StaticContexttail:List (Name × Expr)ih:∀ {env localEnv : Env}, TopLevelBindingStatics ctx tail → EnvMatchesStatic env ctx → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhBindings:TopLevelBindingStatics ctx ((bindingName, bindingExpr) :: tail)hTailBindings:TopLevelBindingStatics ctx tailbindingValue:ValuehBindingEval:eval env bindingExpr = Except.ok bindingValuehEval:evalBindingsNoDuplicate (Env.insert bindingName bindingValue env) tail = Except.ok localEnv⊢ EnvMatchesStatic localEnv ctx have hNextMatch : EnvMatchesStatic (Env.insert bindingName bindingValue env) ctx := ctx:StaticContextenv:EnvlocalEnv:Envbindings:List (Name × Expr)hBindings:TopLevelBindingStatics ctx bindingshMatch:EnvMatchesStatic env ctxhEval:evalBindingsNoDuplicate env bindings = Except.ok localEnv⊢ EnvMatchesStatic localEnv ctx intro candidate ctx:StaticContexttail:List (Name × Expr)ih:∀ {env localEnv : Env}, TopLevelBindingStatics ctx tail → EnvMatchesStatic env ctx → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhBindings:TopLevelBindingStatics ctx ((bindingName, bindingExpr) :: tail)hTailBindings:TopLevelBindingStatics ctx tailbindingValue:ValuehBindingEval:eval env bindingExpr = Except.ok bindingValuehEval:evalBindingsNoDuplicate (Env.insert bindingName bindingValue env) tail = Except.ok localEnvcandidate:Namefields:Finset Name⊢ ∀ (value : Value), ctx candidate = some fields → Env.insert bindingName bindingValue env candidate = some value → value.hasOnlyFields fields ctx:StaticContexttail:List (Name × Expr)ih:∀ {env localEnv : Env}, TopLevelBindingStatics ctx tail → EnvMatchesStatic env ctx → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhBindings:TopLevelBindingStatics ctx ((bindingName, bindingExpr) :: tail)hTailBindings:TopLevelBindingStatics ctx tailbindingValue:ValuehBindingEval:eval env bindingExpr = Except.ok bindingValuehEval:evalBindingsNoDuplicate (Env.insert bindingName bindingValue env) tail = Except.ok localEnvcandidate:Namefields:Finset Namevalue:Value⊢ ctx candidate = some fields → Env.insert bindingName bindingValue env candidate = some value → value.hasOnlyFields fields ctx:StaticContexttail:List (Name × Expr)ih:∀ {env localEnv : Env}, TopLevelBindingStatics ctx tail → EnvMatchesStatic env ctx → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhBindings:TopLevelBindingStatics ctx ((bindingName, bindingExpr) :: tail)hTailBindings:TopLevelBindingStatics ctx tailbindingValue:ValuehBindingEval:eval env bindingExpr = Except.ok bindingValuehEval:evalBindingsNoDuplicate (Env.insert bindingName bindingValue env) tail = Except.ok localEnvcandidate:Namefields:Finset Namevalue:ValuehStaticLookup:ctx candidate = some fields⊢ Env.insert bindingName bindingValue env candidate = some value → value.hasOnlyFields fields ctx:StaticContexttail:List (Name × Expr)ih:∀ {env localEnv : Env}, TopLevelBindingStatics ctx tail → EnvMatchesStatic env ctx → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhBindings:TopLevelBindingStatics ctx ((bindingName, bindingExpr) :: tail)hTailBindings:TopLevelBindingStatics ctx tailbindingValue:ValuehBindingEval:eval env bindingExpr = Except.ok bindingValuehEval:evalBindingsNoDuplicate (Env.insert bindingName bindingValue env) tail = Except.ok localEnvcandidate:Namefields:Finset Namevalue:ValuehStaticLookup:ctx candidate = some fieldshEnvLookup:Env.insert bindingName bindingValue env candidate = some value⊢ value.hasOnlyFields fields ctx:StaticContexttail:List (Name × Expr)ih:∀ {env localEnv : Env}, TopLevelBindingStatics ctx tail → EnvMatchesStatic env ctx → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhBindings:TopLevelBindingStatics ctx ((bindingName, bindingExpr) :: tail)hTailBindings:TopLevelBindingStatics ctx tailbindingValue:ValuehBindingEval:eval env bindingExpr = Except.ok bindingValuehEval:evalBindingsNoDuplicate (Env.insert bindingName bindingValue env) tail = Except.ok localEnvcandidate:Namefields:Finset Namevalue:ValuehStaticLookup:ctx candidate = some fieldshEnvLookup:Env.insert bindingName bindingValue env candidate = some valuehCandidate:candidate = bindingName⊢ value.hasOnlyFields fieldsctx:StaticContexttail:List (Name × Expr)ih:∀ {env localEnv : Env}, TopLevelBindingStatics ctx tail → EnvMatchesStatic env ctx → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhBindings:TopLevelBindingStatics ctx ((bindingName, bindingExpr) :: tail)hTailBindings:TopLevelBindingStatics ctx tailbindingValue:ValuehBindingEval:eval env bindingExpr = Except.ok bindingValuehEval:evalBindingsNoDuplicate (Env.insert bindingName bindingValue env) tail = Except.ok localEnvcandidate:Namefields:Finset Namevalue:ValuehStaticLookup:ctx candidate = some fieldshEnvLookup:Env.insert bindingName bindingValue env candidate = some valuehCandidate:¬candidate = bindingName⊢ value.hasOnlyFields fields ctx:StaticContexttail:List (Name × Expr)ih:∀ {env localEnv : Env}, TopLevelBindingStatics ctx tail → EnvMatchesStatic env ctx → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhBindings:TopLevelBindingStatics ctx ((bindingName, bindingExpr) :: tail)hTailBindings:TopLevelBindingStatics ctx tailbindingValue:ValuehBindingEval:eval env bindingExpr = Except.ok bindingValuehEval:evalBindingsNoDuplicate (Env.insert bindingName bindingValue env) tail = Except.ok localEnvcandidate:Namefields:Finset Namevalue:ValuehStaticLookup:ctx candidate = some fieldshEnvLookup:Env.insert bindingName bindingValue env candidate = some valuehCandidate:candidate = bindingName⊢ value.hasOnlyFields fields ctx:StaticContexttail:List (Name × Expr)ih:∀ {env localEnv : Env}, TopLevelBindingStatics ctx tail → EnvMatchesStatic env ctx → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhBindings:TopLevelBindingStatics ctx ((bindingName, bindingExpr) :: tail)hTailBindings:TopLevelBindingStatics ctx tailbindingValue:ValuehBindingEval:eval env bindingExpr = Except.ok bindingValuehEval:evalBindingsNoDuplicate (Env.insert bindingName bindingValue env) tail = Except.ok localEnvfields:Finset Namevalue:ValuehStaticLookup:ctx bindingName = some fieldshEnvLookup:Env.insert bindingName bindingValue env bindingName = some value⊢ value.hasOnlyFields fields ctx:StaticContexttail:List (Name × Expr)ih:∀ {env localEnv : Env}, TopLevelBindingStatics ctx tail → EnvMatchesStatic env ctx → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhBindings:TopLevelBindingStatics ctx ((bindingName, bindingExpr) :: tail)hTailBindings:TopLevelBindingStatics ctx tailbindingValue:ValuehBindingEval:eval env bindingExpr = Except.ok bindingValuehEval:evalBindingsNoDuplicate (Env.insert bindingName bindingValue env) tail = Except.ok localEnvfields:Finset Namevalue:ValuehStaticLookup:ctx bindingName = some fieldshEnvLookup:bindingValue = value⊢ value.hasOnlyFields fields ctx:StaticContexttail:List (Name × Expr)ih:∀ {env localEnv : Env}, TopLevelBindingStatics ctx tail → EnvMatchesStatic env ctx → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhBindings:TopLevelBindingStatics ctx ((bindingName, bindingExpr) :: tail)hTailBindings:TopLevelBindingStatics ctx tailbindingValue:ValuehBindingEval:eval env bindingExpr = Except.ok bindingValuehEval:evalBindingsNoDuplicate (Env.insert bindingName bindingValue env) tail = Except.ok localEnvfields:Finset NamehStaticLookup:ctx bindingName = some fields⊢ bindingValue.hasOnlyFields fields cases hBindingStatic : ctx bindingName with ctx:StaticContexttail:List (Name × Expr)ih:∀ {env localEnv : Env}, TopLevelBindingStatics ctx tail → EnvMatchesStatic env ctx → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhBindings:TopLevelBindingStatics ctx ((bindingName, bindingExpr) :: tail)hTailBindings:TopLevelBindingStatics ctx tailbindingValue:ValuehBindingEval:eval env bindingExpr = Except.ok bindingValuehEval:evalBindingsNoDuplicate (Env.insert bindingName bindingValue env) tail = Except.ok localEnvfields:Finset NamehStaticLookup:ctx bindingName = some fieldshBindingStatic:ctx bindingName = none⊢ bindingValue.hasOnlyFields fields All goals completed! 🐙 ctx:StaticContexttail:List (Name × Expr)ih:∀ {env localEnv : Env}, TopLevelBindingStatics ctx tail → EnvMatchesStatic env ctx → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhBindings:TopLevelBindingStatics ctx ((bindingName, bindingExpr) :: tail)hTailBindings:TopLevelBindingStatics ctx tailbindingValue:ValuehBindingEval:eval env bindingExpr = Except.ok bindingValuehEval:evalBindingsNoDuplicate (Env.insert bindingName bindingValue env) tail = Except.ok localEnvfields:Finset NamehStaticLookup:ctx bindingName = some fieldsbindingFields:Finset NamehBindingStatic:ctx bindingName = some bindingFields⊢ bindingValue.hasOnlyFields fields have hValueHas := topLevelBinding_value_hasOnlyFields hBindings hMatch (ctx:StaticContexttail:List (Name × Expr)ih:∀ {env localEnv : Env}, TopLevelBindingStatics ctx tail → EnvMatchesStatic env ctx → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhBindings:TopLevelBindingStatics ctx ((bindingName, bindingExpr) :: tail)hTailBindings:TopLevelBindingStatics ctx tailbindingValue:ValuehBindingEval:eval env bindingExpr = Except.ok bindingValuehEval:evalBindingsNoDuplicate (Env.insert bindingName bindingValue env) tail = Except.ok localEnvfields:Finset NamehStaticLookup:ctx bindingName = some fieldsbindingFields:Finset NamehBindingStatic:ctx bindingName = some bindingFields⊢ (bindingName, bindingExpr) ∈ (bindingName, bindingExpr) :: tail All goals completed! 🐙) hBindingStatic hBindingEval ctx:StaticContexttail:List (Name × Expr)ih:∀ {env localEnv : Env}, TopLevelBindingStatics ctx tail → EnvMatchesStatic env ctx → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhBindings:TopLevelBindingStatics ctx ((bindingName, bindingExpr) :: tail)hTailBindings:TopLevelBindingStatics ctx tailbindingValue:ValuehBindingEval:eval env bindingExpr = Except.ok bindingValuehEval:evalBindingsNoDuplicate (Env.insert bindingName bindingValue env) tail = Except.ok localEnvfields:Finset NamebindingFields:Finset NamehStaticLookup:some bindingFields = some fieldshBindingStatic:ctx bindingName = some bindingFieldshValueHas:bindingValue.hasOnlyFields bindingFields⊢ bindingValue.hasOnlyFields fields ctx:StaticContexttail:List (Name × Expr)ih:∀ {env localEnv : Env}, TopLevelBindingStatics ctx tail → EnvMatchesStatic env ctx → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhBindings:TopLevelBindingStatics ctx ((bindingName, bindingExpr) :: tail)hTailBindings:TopLevelBindingStatics ctx tailbindingValue:ValuehBindingEval:eval env bindingExpr = Except.ok bindingValuehEval:evalBindingsNoDuplicate (Env.insert bindingName bindingValue env) tail = Except.ok localEnvfields:Finset NamehBindingStatic:ctx bindingName = some fieldshValueHas:bindingValue.hasOnlyFields fields⊢ bindingValue.hasOnlyFields fields All goals completed! 🐙 ctx:StaticContexttail:List (Name × Expr)ih:∀ {env localEnv : Env}, TopLevelBindingStatics ctx tail → EnvMatchesStatic env ctx → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhBindings:TopLevelBindingStatics ctx ((bindingName, bindingExpr) :: tail)hTailBindings:TopLevelBindingStatics ctx tailbindingValue:ValuehBindingEval:eval env bindingExpr = Except.ok bindingValuehEval:evalBindingsNoDuplicate (Env.insert bindingName bindingValue env) tail = Except.ok localEnvcandidate:Namefields:Finset Namevalue:ValuehStaticLookup:ctx candidate = some fieldshEnvLookup:Env.insert bindingName bindingValue env candidate = some valuehCandidate:¬candidate = bindingName⊢ value.hasOnlyFields fields ctx:StaticContexttail:List (Name × Expr)ih:∀ {env localEnv : Env}, TopLevelBindingStatics ctx tail → EnvMatchesStatic env ctx → evalBindingsNoDuplicate env tail = Except.ok localEnv → EnvMatchesStatic localEnv ctxenv:EnvlocalEnv:EnvhMatch:EnvMatchesStatic env ctxbindingName:NamebindingExpr:ExprhBindings:TopLevelBindingStatics ctx ((bindingName, bindingExpr) :: tail)hTailBindings:TopLevelBindingStatics ctx tailbindingValue:ValuehBindingEval:eval env bindingExpr = Except.ok bindingValuehEval:evalBindingsNoDuplicate (Env.insert bindingName bindingValue env) tail = Except.ok localEnvcandidate:Namefields:Finset Namevalue:ValuehStaticLookup:ctx candidate = some fieldshCandidate:¬candidate = bindingNamehEnvLookup:env candidate = some value⊢ value.hasOnlyFields fields All goals completed! 🐙 All goals completed! 🐙

Runtime top-level binding evaluation preserves the static context it establishes.

theorem evalBindings_establish_staticContext {ctx : StaticContext} {env localEnv : Env} {bindings : List (Name × Expr)} (hBindings : TopLevelBindingStatics ctx bindings) (hMatch : EnvMatchesStatic env ctx) (hEval : evalBindings env bindings = Except.ok localEnv) : EnvMatchesStatic localEnv ctx := ctx:StaticContextenv:EnvlocalEnv:Envbindings:List (Name × Expr)hBindings:TopLevelBindingStatics ctx bindingshMatch:EnvMatchesStatic env ctxhEval:evalBindings env bindings = Except.ok localEnv⊢ EnvMatchesStatic localEnv ctx cases hDuplicate : duplicateName (bindings.map Prod.fst) with ctx:StaticContextenv:EnvlocalEnv:Envbindings:List (Name × Expr)hBindings:TopLevelBindingStatics ctx bindingshMatch:EnvMatchesStatic env ctxhEval:evalBindings env bindings = Except.ok localEnvduplicate:NamehDuplicate:duplicateName (List.map Prod.fst bindings) = some duplicate⊢ EnvMatchesStatic localEnv ctx All goals completed! 🐙 ctx:StaticContextenv:EnvlocalEnv:Envbindings:List (Name × Expr)hBindings:TopLevelBindingStatics ctx bindingshMatch:EnvMatchesStatic env ctxhEval:evalBindings env bindings = Except.ok localEnvhDuplicate:duplicateName (List.map Prod.fst bindings) = none⊢ EnvMatchesStatic localEnv ctx have hNoDuplicateEval : evalBindingsNoDuplicate env bindings = Except.ok localEnv := ctx:StaticContextenv:EnvlocalEnv:Envbindings:List (Name × Expr)hBindings:TopLevelBindingStatics ctx bindingshMatch:EnvMatchesStatic env ctxhEval:evalBindings env bindings = Except.ok localEnv⊢ EnvMatchesStatic localEnv ctx All goals completed! 🐙 All goals completed! 🐙

Successful evaluation from the empty environment constructs an environment matching the static context established by the top-level bindings.

theorem topLevelBindings_establish_staticContext {ctx : StaticContext} {env : Env} {bindings : List (Name × Expr)} (hBindings : TopLevelBindingsEstablishStaticContext ctx bindings) (hEval : evalBindings Env.empty bindings = Except.ok env) : EnvMatchesStatic env ctx := ctx:StaticContextenv:Envbindings:List (Name × Expr)hBindings:TopLevelBindingsEstablishStaticContext ctx bindingshEval:evalBindings Env.empty bindings = Except.ok env⊢ EnvMatchesStatic env ctx have hEmptyMatch : EnvMatchesStatic Env.empty ctx := ctx:StaticContextenv:Envbindings:List (Name × Expr)hBindings:TopLevelBindingsEstablishStaticContext ctx bindingshEval:evalBindings Env.empty bindings = Except.ok env⊢ EnvMatchesStatic env ctx intro _name ctx:StaticContextenv:Envbindings:List (Name × Expr)hBindings:TopLevelBindingsEstablishStaticContext ctx bindingshEval:evalBindings Env.empty bindings = Except.ok env_name:Name_fields:Finset Name⊢ ∀ (value : Value), ctx _name = some _fields → Env.empty _name = some value → value.hasOnlyFields _fields ctx:StaticContextenv:Envbindings:List (Name × Expr)hBindings:TopLevelBindingsEstablishStaticContext ctx bindingshEval:evalBindings Env.empty bindings = Except.ok env_name:Name_fields:Finset Name_value:Value⊢ ctx _name = some _fields → Env.empty _name = some _value → _value.hasOnlyFields _fields ctx:StaticContextenv:Envbindings:List (Name × Expr)hBindings:TopLevelBindingsEstablishStaticContext ctx bindingshEval:evalBindings Env.empty bindings = Except.ok env_name:Name_fields:Finset Name_value:Value_hStatic:ctx _name = some _fields⊢ Env.empty _name = some _value → _value.hasOnlyFields _fields ctx:StaticContextenv:Envbindings:List (Name × Expr)hBindings:TopLevelBindingsEstablishStaticContext ctx bindingshEval:evalBindings Env.empty bindings = Except.ok env_name:Name_fields:Finset Name_value:Value_hStatic:ctx _name = some _fieldshLookup:Env.empty _name = some _value⊢ _value.hasOnlyFields _fields All goals completed! 🐙 All goals completed! 🐙

Pure Node Lowering

Pure output equation in the proof-side lowering model.

structure PureOutputEquation where

Declared output label.

output : Name

CorePure expression that computes the output value.

expr : Expr

Output labels present in an output-equation list.

def outputEquationKeySet (outputs : List PureOutputEquation) : Finset Name := outputs.foldr (fun output acc => insert output.output acc) ∅

Source pure node model needed for lowering proofs.

structure PureNode where

Declared input port names.

inputPorts : Finset Name

Declared output port names.

outputPorts : Finset Name

Top-level delayed bindings visible to this node.

bindings : List (Name × Expr)

Optional node-local where expression.

whereExpr : Option Expr

Output equations.

outputs : List PureOutputEquationnamespace PureNode

Output labels declared by the output-equation map.

def outputKeys (node : PureNode) : Finset Name := outputEquationKeySet node.outputs

Static where field set, with no fields when the node has no where expression.

def whereFields (ctx : StaticContext) (node : PureNode) : Option (Finset Name) := match node.whereExpr with | none => some ∅ | some whereExpr => whereStaticFields ctx whereExprend PureNode

Admission checks needed before lowering a source pure node.

structure PureNodeAdmitted (ctx : StaticContext) (node : PureNode) : Prop where

Top-level node bindings do not shadow statically known module-level records.

bindings_noShadow : letBindingsDoNotShadowStatic ctx node.bindings

Output equations match declared output ports exactly.

outputs_match : node.outputKeys = node.outputPorts

The node-local where expression has a statically known field set.

where_static : ∃ fields, node.whereFields ctx = some fields

Local let binders inside the where expression preserve static field soundness.

where_letSafe : ∀ whereExpr, node.whereExpr = some whereExpr → Expr.staticLetSafe ctx whereExpr

Node-local where fields do not collide with input port names.

where_noInputCollision : ∀ fields, node.whereFields ctx = some fields → Disjoint fields node.inputPorts

Native pure task configuration produced by lowering.

structure NativePureTaskConfig where

Top-level delayed bindings or captured constants.

bindings : List (Name × Expr)

Optional node-local where expression.

whereExpr : Option Expr

Output expression map.

outputs : List PureOutputEquation

Lowered node kind used to state that pure nodes lower to one native pure task.

inductive LoweredNodeKind : Type where | nativePure

Lowered pure node artifact.

structure LoweredPureNode where

Lowered node kind.

kind : LoweredNodeKind

Native pure task configuration.

config : NativePureTaskConfig

Lower a source pure node to one native pure task.

def lowerPureNode (_ctx : StaticContext) (node : PureNode) : LoweredPureNode := { kind := LoweredNodeKind.nativePure config := { bindings := node.bindings whereExpr := node.whereExpr outputs := node.outputs } }

Output Value Contracts

First proof-side value-contract carrier for pure output values.

This is intentionally smaller than JSON Schema or the runtime WireValue wrapper. It gives the proof track a concrete contract predicate that is no longer just an arbitrary Name → Value → Prop.

inductive ValueContract : Type where | any | null | bool | int | string | record deriving DecidableEq, Reprnamespace ValueContract

A proof-side value satisfies a simple value contract.

def accepts : ValueContract → Value → Prop | any, _value => True | null, Value.null => True | null, Value.bool _value => False | null, Value.int _value => False | null, Value.string _value => False | null, Value.record _fields => False | bool, Value.null => False | bool, Value.bool _value => True | bool, Value.int _value => False | bool, Value.string _value => False | bool, Value.record _fields => False | int, Value.null => False | int, Value.bool _value => False | int, Value.int _value => True | int, Value.string _value => False | int, Value.record _fields => False | string, Value.null => False | string, Value.bool _value => False | string, Value.int _value => False | string, Value.string _value => True | string, Value.record _fields => False | record, Value.null => False | record, Value.bool _value => False | record, Value.int _value => False | record, Value.string _value => False | record, Value.record _fields => Trueend ValueContract

Output-contract table for the proof-side value-contract carrier.

abbrev OutputValueContracts : Type := Name → Option ValueContract

A named output value satisfies the concrete proof-side value-contract table.

def outputValueContractOk (contracts : OutputValueContracts) (name : Name) (value : Value) : Prop := ∃ contract, contracts name = some contract ∧ contract.accepts value

Open a record value into an environment, shadowing outer variables by field name.

def openRecordIntoEnv (recordFields : Name → Option Value) (env : Env) : Env := fun name => match recordFields name with | some value => some value | none => env name

Opening a where record preserves static facts outside names opened by the record.

theorem openRecordIntoEnv_preserves_hidden_static_context {ctx : StaticContext} {env : Env} {recordFields : Name → Option Value} {staticFields : Finset Name} (hMatch : EnvMatchesStatic env ctx) (hRecord : Value.hasOnlyFields (Value.record recordFields) staticFields) : EnvMatchesStatic (openRecordIntoEnv recordFields env) (StaticContext.hideFields staticFields ctx) := ctx:StaticContextenv:EnvrecordFields:Name → Option ValuestaticFields:Finset NamehMatch:EnvMatchesStatic env ctxhRecord:(Value.record recordFields).hasOnlyFields staticFields⊢ EnvMatchesStatic (openRecordIntoEnv recordFields env) (StaticContext.hideFields staticFields ctx) intro name ctx:StaticContextenv:EnvrecordFields:Name → Option ValuestaticFields:Finset NamehMatch:EnvMatchesStatic env ctxhRecord:(Value.record recordFields).hasOnlyFields staticFieldsname:Namefields:Finset Name⊢ ∀ (value : Value), StaticContext.hideFields staticFields ctx name = some fields → openRecordIntoEnv recordFields env name = some value → value.hasOnlyFields fields ctx:StaticContextenv:EnvrecordFields:Name → Option ValuestaticFields:Finset NamehMatch:EnvMatchesStatic env ctxhRecord:(Value.record recordFields).hasOnlyFields staticFieldsname:Namefields:Finset Namevalue:Value⊢ StaticContext.hideFields staticFields ctx name = some fields → openRecordIntoEnv recordFields env name = some value → value.hasOnlyFields fields ctx:StaticContextenv:EnvrecordFields:Name → Option ValuestaticFields:Finset NamehMatch:EnvMatchesStatic env ctxhRecord:(Value.record recordFields).hasOnlyFields staticFieldsname:Namefields:Finset Namevalue:ValuehStatic:StaticContext.hideFields staticFields ctx name = some fields⊢ openRecordIntoEnv recordFields env name = some value → value.hasOnlyFields fields ctx:StaticContextenv:EnvrecordFields:Name → Option ValuestaticFields:Finset NamehMatch:EnvMatchesStatic env ctxhRecord:(Value.record recordFields).hasOnlyFields staticFieldsname:Namefields:Finset Namevalue:ValuehStatic:StaticContext.hideFields staticFields ctx name = some fieldshLocal:openRecordIntoEnv recordFields env name = some value⊢ value.hasOnlyFields fields cases hRecordLookup : recordFields name with ctx:StaticContextenv:EnvrecordFields:Name → Option ValuestaticFields:Finset NamehMatch:EnvMatchesStatic env ctxhRecord:(Value.record recordFields).hasOnlyFields staticFieldsname:Namefields:Finset Namevalue:ValuehStatic:StaticContext.hideFields staticFields ctx name = some fieldshLocal:openRecordIntoEnv recordFields env name = some valuehRecordLookup:recordFields name = none⊢ value.hasOnlyFields fields have hOuterLookup : env name = some value := ctx:StaticContextenv:EnvrecordFields:Name → Option ValuestaticFields:Finset NamehMatch:EnvMatchesStatic env ctxhRecord:(Value.record recordFields).hasOnlyFields staticFields⊢ EnvMatchesStatic (openRecordIntoEnv recordFields env) (StaticContext.hideFields staticFields ctx) All goals completed! 🐙 ctx:StaticContextenv:EnvrecordFields:Name → Option ValuestaticFields:Finset NamehMatch:EnvMatchesStatic env ctxhRecord:(Value.record recordFields).hasOnlyFields staticFieldsname:Namefields:Finset Namevalue:ValuehStatic:StaticContext.hideFields staticFields ctx name = some fieldshLocal:openRecordIntoEnv recordFields env name = some valuehRecordLookup:recordFields name = nonehOuterLookup:env name = some valuehMember:name ∈ staticFields⊢ value.hasOnlyFields fieldsctx:StaticContextenv:EnvrecordFields:Name → Option ValuestaticFields:Finset NamehMatch:EnvMatchesStatic env ctxhRecord:(Value.record recordFields).hasOnlyFields staticFieldsname:Namefields:Finset Namevalue:ValuehStatic:StaticContext.hideFields staticFields ctx name = some fieldshLocal:openRecordIntoEnv recordFields env name = some valuehRecordLookup:recordFields name = nonehOuterLookup:env name = some valuehMember:name ∉ staticFields⊢ value.hasOnlyFields fields ctx:StaticContextenv:EnvrecordFields:Name → Option ValuestaticFields:Finset NamehMatch:EnvMatchesStatic env ctxhRecord:(Value.record recordFields).hasOnlyFields staticFieldsname:Namefields:Finset Namevalue:ValuehStatic:StaticContext.hideFields staticFields ctx name = some fieldshLocal:openRecordIntoEnv recordFields env name = some valuehRecordLookup:recordFields name = nonehOuterLookup:env name = some valuehMember:name ∈ staticFields⊢ value.hasOnlyFields fields have hHidden : StaticContext.hideFields staticFields ctx name = none := ctx:StaticContextenv:EnvrecordFields:Name → Option ValuestaticFields:Finset NamehMatch:EnvMatchesStatic env ctxhRecord:(Value.record recordFields).hasOnlyFields staticFields⊢ EnvMatchesStatic (openRecordIntoEnv recordFields env) (StaticContext.hideFields staticFields ctx) All goals completed! 🐙 ctx:StaticContextenv:EnvrecordFields:Name → Option ValuestaticFields:Finset NamehMatch:EnvMatchesStatic env ctxhRecord:(Value.record recordFields).hasOnlyFields staticFieldsname:Namefields:Finset Namevalue:ValuehStatic:none = some fieldshLocal:openRecordIntoEnv recordFields env name = some valuehRecordLookup:recordFields name = nonehOuterLookup:env name = some valuehMember:name ∈ staticFieldshHidden:StaticContext.hideFields staticFields ctx name = none⊢ value.hasOnlyFields fields All goals completed! 🐙 ctx:StaticContextenv:EnvrecordFields:Name → Option ValuestaticFields:Finset NamehMatch:EnvMatchesStatic env ctxhRecord:(Value.record recordFields).hasOnlyFields staticFieldsname:Namefields:Finset Namevalue:ValuehStatic:StaticContext.hideFields staticFields ctx name = some fieldshLocal:openRecordIntoEnv recordFields env name = some valuehRecordLookup:recordFields name = nonehOuterLookup:env name = some valuehMember:name ∉ staticFields⊢ value.hasOnlyFields fields have hOuterStatic : ctx name = some fields := ctx:StaticContextenv:EnvrecordFields:Name → Option ValuestaticFields:Finset NamehMatch:EnvMatchesStatic env ctxhRecord:(Value.record recordFields).hasOnlyFields staticFields⊢ EnvMatchesStatic (openRecordIntoEnv recordFields env) (StaticContext.hideFields staticFields ctx) All goals completed! 🐙 All goals completed! 🐙 ctx:StaticContextenv:EnvrecordFields:Name → Option ValuestaticFields:Finset NamehMatch:EnvMatchesStatic env ctxhRecord:(Value.record recordFields).hasOnlyFields staticFieldsname:Namefields:Finset Namevalue:ValuehStatic:StaticContext.hideFields staticFields ctx name = some fieldshLocal:openRecordIntoEnv recordFields env name = some valueopenedValue:ValuehRecordLookup:recordFields name = some openedValue⊢ value.hasOnlyFields fields ctx:StaticContextenv:EnvrecordFields:Name → Option ValuestaticFields:Finset NamehMatch:EnvMatchesStatic env ctxhRecord:(Value.record recordFields).hasOnlyFields staticFieldsname:Namefields:Finset Namevalue:ValuehStatic:StaticContext.hideFields staticFields ctx name = some fieldshLocal:openRecordIntoEnv recordFields env name = some valueopenedValue:ValuehRecordLookup:recordFields name = some openedValuehMember:name ∈ staticFields⊢ value.hasOnlyFields fields have hHidden : StaticContext.hideFields staticFields ctx name = none := ctx:StaticContextenv:EnvrecordFields:Name → Option ValuestaticFields:Finset NamehMatch:EnvMatchesStatic env ctxhRecord:(Value.record recordFields).hasOnlyFields staticFields⊢ EnvMatchesStatic (openRecordIntoEnv recordFields env) (StaticContext.hideFields staticFields ctx) All goals completed! 🐙 ctx:StaticContextenv:EnvrecordFields:Name → Option ValuestaticFields:Finset NamehMatch:EnvMatchesStatic env ctxhRecord:(Value.record recordFields).hasOnlyFields staticFieldsname:Namefields:Finset Namevalue:ValuehStatic:none = some fieldshLocal:openRecordIntoEnv recordFields env name = some valueopenedValue:ValuehRecordLookup:recordFields name = some openedValuehMember:name ∈ staticFieldshHidden:StaticContext.hideFields staticFields ctx name = none⊢ value.hasOnlyFields fields All goals completed! 🐙

Evaluate an optional where expression into the local pure-task environment.

def evalWhereEnv (env : Env) : Option Expr → Except EvalError Env | none => Except.ok env | some whereExpr => match eval env whereExpr with | Except.error err => Except.error err | Except.ok Value.null => Except.error EvalError.expectedRecord | Except.ok (Value.bool _value) => Except.error EvalError.expectedRecord | Except.ok (Value.int _value) => Except.error EvalError.expectedRecord | Except.ok (Value.string _value) => Except.error EvalError.expectedRecord | Except.ok (Value.record recordFields) => Except.ok (openRecordIntoEnv recordFields env)

Evaluate output equations in an already prepared pure-task environment.

def evalOutputEquationValues (env : Env) : List PureOutputEquation → Except EvalError (List (Name × Value)) | [] => Except.ok [] | output :: rest => match eval env output.expr with | Except.error err => Except.error err | Except.ok outputValue => match evalOutputEquationValues env rest with | Except.error err => Except.error err | Except.ok restValues => Except.ok ((output.output, outputValue) :: restValues)

Convert evaluated output values into the proof-side output lookup surface.

def outputLookupFromValues (values : List (Name × Value)) : Name → Option Value := recordFromValues values

Evaluate output equations to a lookup function in an already prepared environment.

def evalOutputEquations (env : Env) (outputs : List PureOutputEquation) : Except EvalError (Name → Option Value) := match evalOutputEquationValues env outputs with | Except.error err => Except.error err | Except.ok values => Except.ok (outputLookupFromValues values)

Evaluating output equations preserves their declared output-label set.

theorem evalOutputEquationValues_preserves_names {env : Env} {outputs : List PureOutputEquation} {values : List (Name × Value)} (hEval : evalOutputEquationValues env outputs = Except.ok values) : valueFieldNameSet values = outputEquationKeySet outputs := env:Envoutputs:List PureOutputEquationvalues:List (Name × Value)hEval:evalOutputEquationValues env outputs = Except.ok values⊢ valueFieldNameSet values = outputEquationKeySet outputs induction outputs generalizing values with env:Envvalues:List (Name × Value)hEval:evalOutputEquationValues env [] = Except.ok values⊢ valueFieldNameSet values = outputEquationKeySet [] env:Envvalues:List (Name × Value)hEval:values = []⊢ valueFieldNameSet values = outputEquationKeySet [] env:Env⊢ valueFieldNameSet [] = outputEquationKeySet [] All goals completed! 🐙 env:Envoutput:PureOutputEquationrest:List PureOutputEquationih:∀ {values : List (Name × Value)}, evalOutputEquationValues env rest = Except.ok values → valueFieldNameSet values = outputEquationKeySet restvalues:List (Name × Value)hEval:evalOutputEquationValues env (output :: rest) = Except.ok values⊢ valueFieldNameSet values = outputEquationKeySet (output :: rest) env:Envoutput:PureOutputEquationrest:List PureOutputEquationih:∀ {values : List (Name × Value)}, evalOutputEquationValues env rest = Except.ok values → valueFieldNameSet values = outputEquationKeySet restvalues:List (Name × Value)hEval:(match eval env output.expr with | Except.error err => Except.error err | Except.ok outputValue => match evalOutputEquationValues env rest with | Except.error err => Except.error err | Except.ok restValues => Except.ok ((output.output, outputValue) :: restValues)) = Except.ok values⊢ valueFieldNameSet values = outputEquationKeySet (output :: rest) cases hOutputEval : eval env output.expr with env:Envoutput:PureOutputEquationrest:List PureOutputEquationih:∀ {values : List (Name × Value)}, evalOutputEquationValues env rest = Except.ok values → valueFieldNameSet values = outputEquationKeySet restvalues:List (Name × Value)hEval:(match eval env output.expr with | Except.error err => Except.error err | Except.ok outputValue => match evalOutputEquationValues env rest with | Except.error err => Except.error err | Except.ok restValues => Except.ok ((output.output, outputValue) :: restValues)) = Except.ok valueserr:EvalErrorhOutputEval:eval env output.expr = Except.error err⊢ valueFieldNameSet values = outputEquationKeySet (output :: rest) All goals completed! 🐙 env:Envoutput:PureOutputEquationrest:List PureOutputEquationih:∀ {values : List (Name × Value)}, evalOutputEquationValues env rest = Except.ok values → valueFieldNameSet values = outputEquationKeySet restvalues:List (Name × Value)hEval:(match eval env output.expr with | Except.error err => Except.error err | Except.ok outputValue => match evalOutputEquationValues env rest with | Except.error err => Except.error err | Except.ok restValues => Except.ok ((output.output, outputValue) :: restValues)) = Except.ok valuesoutputValue:ValuehOutputEval:eval env output.expr = Except.ok outputValue⊢ valueFieldNameSet values = outputEquationKeySet (output :: rest) env:Envoutput:PureOutputEquationrest:List PureOutputEquationih:∀ {values : List (Name × Value)}, evalOutputEquationValues env rest = Except.ok values → valueFieldNameSet values = outputEquationKeySet restvalues:List (Name × Value)outputValue:ValuehOutputEval:eval env output.expr = Except.ok outputValuehEval:(match evalOutputEquationValues env rest with | Except.error err => Except.error err | Except.ok restValues => Except.ok ((output.output, outputValue) :: restValues)) = Except.ok values⊢ valueFieldNameSet values = outputEquationKeySet (output :: rest) cases hRest : evalOutputEquationValues env rest with env:Envoutput:PureOutputEquationrest:List PureOutputEquationih:∀ {values : List (Name × Value)}, evalOutputEquationValues env rest = Except.ok values → valueFieldNameSet values = outputEquationKeySet restvalues:List (Name × Value)outputValue:ValuehOutputEval:eval env output.expr = Except.ok outputValuehEval:(match evalOutputEquationValues env rest with | Except.error err => Except.error err | Except.ok restValues => Except.ok ((output.output, outputValue) :: restValues)) = Except.ok valueserr:EvalErrorhRest:evalOutputEquationValues env rest = Except.error err⊢ valueFieldNameSet values = outputEquationKeySet (output :: rest) All goals completed! 🐙 env:Envoutput:PureOutputEquationrest:List PureOutputEquationih:∀ {values : List (Name × Value)}, evalOutputEquationValues env rest = Except.ok values → valueFieldNameSet values = outputEquationKeySet restvalues:List (Name × Value)outputValue:ValuehOutputEval:eval env output.expr = Except.ok outputValuehEval:(match evalOutputEquationValues env rest with | Except.error err => Except.error err | Except.ok restValues => Except.ok ((output.output, outputValue) :: restValues)) = Except.ok valuesrestValues:List (Name × Value)hRest:evalOutputEquationValues env rest = Except.ok restValues⊢ valueFieldNameSet values = outputEquationKeySet (output :: rest) env:Envoutput:PureOutputEquationrest:List PureOutputEquationih:∀ {values : List (Name × Value)}, evalOutputEquationValues env rest = Except.ok values → valueFieldNameSet values = outputEquationKeySet restvalues:List (Name × Value)outputValue:ValuehOutputEval:eval env output.expr = Except.ok outputValuerestValues:List (Name × Value)hRest:evalOutputEquationValues env rest = Except.ok restValueshEval:(output.output, outputValue) :: restValues = values⊢ valueFieldNameSet values = outputEquationKeySet (output :: rest) env:Envoutput:PureOutputEquationrest:List PureOutputEquationih:∀ {values : List (Name × Value)}, evalOutputEquationValues env rest = Except.ok values → valueFieldNameSet values = outputEquationKeySet restoutputValue:ValuehOutputEval:eval env output.expr = Except.ok outputValuerestValues:List (Name × Value)hRest:evalOutputEquationValues env rest = Except.ok restValues⊢ valueFieldNameSet ((output.output, outputValue) :: restValues) = outputEquationKeySet (output :: rest) env:Envoutput:PureOutputEquationrest:List PureOutputEquationih:∀ {values : List (Name × Value)}, evalOutputEquationValues env rest = Except.ok values → valueFieldNameSet values = outputEquationKeySet restoutputValue:ValuehOutputEval:eval env output.expr = Except.ok outputValuerestValues:List (Name × Value)hRest:evalOutputEquationValues env rest = Except.ok restValues⊢ insert output.output (valueFieldNameSet restValues) = insert output.output (outputEquationKeySet rest) All goals completed! 🐙

Abstract per-output contract predicate for an output-equation list in one environment.

def OutputExpressionsSatisfyContracts (contractOk : Name → Value → Prop) (env : Env) (outputs : List PureOutputEquation) : Prop := ∀ output, output ∈ outputs → ∀ value, eval env output.expr = Except.ok value → contractOk output.output value

Evaluated output-value pairs satisfy their declared abstract contracts.

theorem evalOutputEquationValues_satisfy_outputContracts {contractOk : Name → Value → Prop} {env : Env} {outputs : List PureOutputEquation} {values : List (Name × Value)} (hEval : evalOutputEquationValues env outputs = Except.ok values) (hContracts : OutputExpressionsSatisfyContracts contractOk env outputs) : ∀ name value, (name, value) ∈ values → contractOk name value := contractOk:Name → Value → Propenv:Envoutputs:List PureOutputEquationvalues:List (Name × Value)hEval:evalOutputEquationValues env outputs = Except.ok valueshContracts:OutputExpressionsSatisfyContracts contractOk env outputs⊢ ∀ (name : Name) (value : Value), (name, value) ∈ values → contractOk name value induction outputs generalizing values with contractOk:Name → Value → Propenv:Envvalues:List (Name × Value)hEval:evalOutputEquationValues env [] = Except.ok valueshContracts:OutputExpressionsSatisfyContracts contractOk env []⊢ ∀ (name : Name) (value : Value), (name, value) ∈ values → contractOk name value contractOk:Name → Value → Propenv:Envvalues:List (Name × Value)hContracts:OutputExpressionsSatisfyContracts contractOk env []hEval:values = []⊢ ∀ (name : Name) (value : Value), (name, value) ∈ values → contractOk name value contractOk:Name → Value → Propenv:EnvhContracts:OutputExpressionsSatisfyContracts contractOk env []⊢ ∀ (name : Name) (value : Value), (name, value) ∈ [] → contractOk name value intro name contractOk:Name → Value → Propenv:EnvhContracts:OutputExpressionsSatisfyContracts contractOk env []name:Namevalue:Value⊢ (name, value) ∈ [] → contractOk name value contractOk:Name → Value → Propenv:EnvhContracts:OutputExpressionsSatisfyContracts contractOk env []name:Namevalue:ValuehMember:(name, value) ∈ []⊢ contractOk name value All goals completed! 🐙 contractOk:Name → Value → Propenv:Envoutput:PureOutputEquationrest:List PureOutputEquationih:∀ {values : List (Name × Value)}, evalOutputEquationValues env rest = Except.ok values → OutputExpressionsSatisfyContracts contractOk env rest → ∀ (name : Name) (value : Value), (name, value) ∈ values → contractOk name valuevalues:List (Name × Value)hEval:evalOutputEquationValues env (output :: rest) = Except.ok valueshContracts:OutputExpressionsSatisfyContracts contractOk env (output :: rest)⊢ ∀ (name : Name) (value : Value), (name, value) ∈ values → contractOk name value contractOk:Name → Value → Propenv:Envoutput:PureOutputEquationrest:List PureOutputEquationih:∀ {values : List (Name × Value)}, evalOutputEquationValues env rest = Except.ok values → OutputExpressionsSatisfyContracts contractOk env rest → ∀ (name : Name) (value : Value), (name, value) ∈ values → contractOk name valuevalues:List (Name × Value)hEval:(match eval env output.expr with | Except.error err => Except.error err | Except.ok outputValue => match evalOutputEquationValues env rest with | Except.error err => Except.error err | Except.ok restValues => Except.ok ((output.output, outputValue) :: restValues)) = Except.ok valueshContracts:OutputExpressionsSatisfyContracts contractOk env (output :: rest)⊢ ∀ (name : Name) (value : Value), (name, value) ∈ values → contractOk name value cases hOutputEval : eval env output.expr with contractOk:Name → Value → Propenv:Envoutput:PureOutputEquationrest:List PureOutputEquationih:∀ {values : List (Name × Value)}, evalOutputEquationValues env rest = Except.ok values → OutputExpressionsSatisfyContracts contractOk env rest → ∀ (name : Name) (value : Value), (name, value) ∈ values → contractOk name valuevalues:List (Name × Value)hEval:(match eval env output.expr with | Except.error err => Except.error err | Except.ok outputValue => match evalOutputEquationValues env rest with | Except.error err => Except.error err | Except.ok restValues => Except.ok ((output.output, outputValue) :: restValues)) = Except.ok valueshContracts:OutputExpressionsSatisfyContracts contractOk env (output :: rest)err:EvalErrorhOutputEval:eval env output.expr = Except.error err⊢ ∀ (name : Name) (value : Value), (name, value) ∈ values → contractOk name value All goals completed! 🐙 contractOk:Name → Value → Propenv:Envoutput:PureOutputEquationrest:List PureOutputEquationih:∀ {values : List (Name × Value)}, evalOutputEquationValues env rest = Except.ok values → OutputExpressionsSatisfyContracts contractOk env rest → ∀ (name : Name) (value : Value), (name, value) ∈ values → contractOk name valuevalues:List (Name × Value)hEval:(match eval env output.expr with | Except.error err => Except.error err | Except.ok outputValue => match evalOutputEquationValues env rest with | Except.error err => Except.error err | Except.ok restValues => Except.ok ((output.output, outputValue) :: restValues)) = Except.ok valueshContracts:OutputExpressionsSatisfyContracts contractOk env (output :: rest)outputValue:ValuehOutputEval:eval env output.expr = Except.ok outputValue⊢ ∀ (name : Name) (value : Value), (name, value) ∈ values → contractOk name value contractOk:Name → Value → Propenv:Envoutput:PureOutputEquationrest:List PureOutputEquationih:∀ {values : List (Name × Value)}, evalOutputEquationValues env rest = Except.ok values → OutputExpressionsSatisfyContracts contractOk env rest → ∀ (name : Name) (value : Value), (name, value) ∈ values → contractOk name valuevalues:List (Name × Value)hContracts:OutputExpressionsSatisfyContracts contractOk env (output :: rest)outputValue:ValuehOutputEval:eval env output.expr = Except.ok outputValuehEval:(match evalOutputEquationValues env rest with | Except.error err => Except.error err | Except.ok restValues => Except.ok ((output.output, outputValue) :: restValues)) = Except.ok values⊢ ∀ (name : Name) (value : Value), (name, value) ∈ values → contractOk name value cases hRest : evalOutputEquationValues env rest with contractOk:Name → Value → Propenv:Envoutput:PureOutputEquationrest:List PureOutputEquationih:∀ {values : List (Name × Value)}, evalOutputEquationValues env rest = Except.ok values → OutputExpressionsSatisfyContracts contractOk env rest → ∀ (name : Name) (value : Value), (name, value) ∈ values → contractOk name valuevalues:List (Name × Value)hContracts:OutputExpressionsSatisfyContracts contractOk env (output :: rest)outputValue:ValuehOutputEval:eval env output.expr = Except.ok outputValuehEval:(match evalOutputEquationValues env rest with | Except.error err => Except.error err | Except.ok restValues => Except.ok ((output.output, outputValue) :: restValues)) = Except.ok valueserr:EvalErrorhRest:evalOutputEquationValues env rest = Except.error err⊢ ∀ (name : Name) (value : Value), (name, value) ∈ values → contractOk name value All goals completed! 🐙 contractOk:Name → Value → Propenv:Envoutput:PureOutputEquationrest:List PureOutputEquationih:∀ {values : List (Name × Value)}, evalOutputEquationValues env rest = Except.ok values → OutputExpressionsSatisfyContracts contractOk env rest → ∀ (name : Name) (value : Value), (name, value) ∈ values → contractOk name valuevalues:List (Name × Value)hContracts:OutputExpressionsSatisfyContracts contractOk env (output :: rest)outputValue:ValuehOutputEval:eval env output.expr = Except.ok outputValuehEval:(match evalOutputEquationValues env rest with | Except.error err => Except.error err | Except.ok restValues => Except.ok ((output.output, outputValue) :: restValues)) = Except.ok valuesrestValues:List (Name × Value)hRest:evalOutputEquationValues env rest = Except.ok restValues⊢ ∀ (name : Name) (value : Value), (name, value) ∈ values → contractOk name value contractOk:Name → Value → Propenv:Envoutput:PureOutputEquationrest:List PureOutputEquationih:∀ {values : List (Name × Value)}, evalOutputEquationValues env rest = Except.ok values → OutputExpressionsSatisfyContracts contractOk env rest → ∀ (name : Name) (value : Value), (name, value) ∈ values → contractOk name valuevalues:List (Name × Value)hContracts:OutputExpressionsSatisfyContracts contractOk env (output :: rest)outputValue:ValuehOutputEval:eval env output.expr = Except.ok outputValuerestValues:List (Name × Value)hRest:evalOutputEquationValues env rest = Except.ok restValueshEval:(output.output, outputValue) :: restValues = values⊢ ∀ (name : Name) (value : Value), (name, value) ∈ values → contractOk name value contractOk:Name → Value → Propenv:Envoutput:PureOutputEquationrest:List PureOutputEquationih:∀ {values : List (Name × Value)}, evalOutputEquationValues env rest = Except.ok values → OutputExpressionsSatisfyContracts contractOk env rest → ∀ (name : Name) (value : Value), (name, value) ∈ values → contractOk name valuehContracts:OutputExpressionsSatisfyContracts contractOk env (output :: rest)outputValue:ValuehOutputEval:eval env output.expr = Except.ok outputValuerestValues:List (Name × Value)hRest:evalOutputEquationValues env rest = Except.ok restValues⊢ ∀ (name : Name) (value : Value), (name, value) ∈ (output.output, outputValue) :: restValues → contractOk name value have hRestContracts : OutputExpressionsSatisfyContracts contractOk env rest := contractOk:Name → Value → Propenv:Envoutputs:List PureOutputEquationvalues:List (Name × Value)hEval:evalOutputEquationValues env outputs = Except.ok valueshContracts:OutputExpressionsSatisfyContracts contractOk env outputs⊢ ∀ (name : Name) (value : Value), (name, value) ∈ values → contractOk name value intro restOutput contractOk:Name → Value → Propenv:Envoutput:PureOutputEquationrest:List PureOutputEquationih:∀ {values : List (Name × Value)}, evalOutputEquationValues env rest = Except.ok values → OutputExpressionsSatisfyContracts contractOk env rest → ∀ (name : Name) (value : Value), (name, value) ∈ values → contractOk name valuehContracts:OutputExpressionsSatisfyContracts contractOk env (output :: rest)outputValue:ValuehOutputEval:eval env output.expr = Except.ok outputValuerestValues:List (Name × Value)hRest:evalOutputEquationValues env rest = Except.ok restValuesrestOutput:PureOutputEquationhRestMember:restOutput ∈ rest⊢ ∀ (value : Value), eval env restOutput.expr = Except.ok value → contractOk restOutput.output value contractOk:Name → Value → Propenv:Envoutput:PureOutputEquationrest:List PureOutputEquationih:∀ {values : List (Name × Value)}, evalOutputEquationValues env rest = Except.ok values → OutputExpressionsSatisfyContracts contractOk env rest → ∀ (name : Name) (value : Value), (name, value) ∈ values → contractOk name valuehContracts:OutputExpressionsSatisfyContracts contractOk env (output :: rest)outputValue:ValuehOutputEval:eval env output.expr = Except.ok outputValuerestValues:List (Name × Value)hRest:evalOutputEquationValues env rest = Except.ok restValuesrestOutput:PureOutputEquationhRestMember:restOutput ∈ restvalue:Value⊢ eval env restOutput.expr = Except.ok value → contractOk restOutput.output value contractOk:Name → Value → Propenv:Envoutput:PureOutputEquationrest:List PureOutputEquationih:∀ {values : List (Name × Value)}, evalOutputEquationValues env rest = Except.ok values → OutputExpressionsSatisfyContracts contractOk env rest → ∀ (name : Name) (value : Value), (name, value) ∈ values → contractOk name valuehContracts:OutputExpressionsSatisfyContracts contractOk env (output :: rest)outputValue:ValuehOutputEval:eval env output.expr = Except.ok outputValuerestValues:List (Name × Value)hRest:evalOutputEquationValues env rest = Except.ok restValuesrestOutput:PureOutputEquationhRestMember:restOutput ∈ restvalue:ValuehRestEval:eval env restOutput.expr = Except.ok value⊢ contractOk restOutput.output value exact hContracts restOutput (contractOk:Name → Value → Propenv:Envoutput:PureOutputEquationrest:List PureOutputEquationih:∀ {values : List (Name × Value)}, evalOutputEquationValues env rest = Except.ok values → OutputExpressionsSatisfyContracts contractOk env rest → ∀ (name : Name) (value : Value), (name, value) ∈ values → contractOk name valuehContracts:OutputExpressionsSatisfyContracts contractOk env (output :: rest)outputValue:ValuehOutputEval:eval env output.expr = Except.ok outputValuerestValues:List (Name × Value)hRest:evalOutputEquationValues env rest = Except.ok restValuesrestOutput:PureOutputEquationhRestMember:restOutput ∈ restvalue:ValuehRestEval:eval env restOutput.expr = Except.ok value⊢ restOutput ∈ output :: rest All goals completed! 🐙) value hRestEval intro name contractOk:Name → Value → Propenv:Envoutput:PureOutputEquationrest:List PureOutputEquationih:∀ {values : List (Name × Value)}, evalOutputEquationValues env rest = Except.ok values → OutputExpressionsSatisfyContracts contractOk env rest → ∀ (name : Name) (value : Value), (name, value) ∈ values → contractOk name valuehContracts:OutputExpressionsSatisfyContracts contractOk env (output :: rest)outputValue:ValuehOutputEval:eval env output.expr = Except.ok outputValuerestValues:List (Name × Value)hRest:evalOutputEquationValues env rest = Except.ok restValueshRestContracts:OutputExpressionsSatisfyContracts contractOk env restname:Namevalue:Value⊢ (name, value) ∈ (output.output, outputValue) :: restValues → contractOk name value contractOk:Name → Value → Propenv:Envoutput:PureOutputEquationrest:List PureOutputEquationih:∀ {values : List (Name × Value)}, evalOutputEquationValues env rest = Except.ok values → OutputExpressionsSatisfyContracts contractOk env rest → ∀ (name : Name) (value : Value), (name, value) ∈ values → contractOk name valuehContracts:OutputExpressionsSatisfyContracts contractOk env (output :: rest)outputValue:ValuehOutputEval:eval env output.expr = Except.ok outputValuerestValues:List (Name × Value)hRest:evalOutputEquationValues env rest = Except.ok restValueshRestContracts:OutputExpressionsSatisfyContracts contractOk env restname:Namevalue:ValuehMember:(name, value) ∈ (output.output, outputValue) :: restValues⊢ contractOk name value contractOk:Name → Value → Propenv:Envoutput:PureOutputEquationrest:List PureOutputEquationih:∀ {values : List (Name × Value)}, evalOutputEquationValues env rest = Except.ok values → OutputExpressionsSatisfyContracts contractOk env rest → ∀ (name : Name) (value : Value), (name, value) ∈ values → contractOk name valuehContracts:OutputExpressionsSatisfyContracts contractOk env (output :: rest)outputValue:ValuehOutputEval:eval env output.expr = Except.ok outputValuerestValues:List (Name × Value)hRest:evalOutputEquationValues env rest = Except.ok restValueshRestContracts:OutputExpressionsSatisfyContracts contractOk env restname:Namevalue:ValuehMember:name = output.output ∧ value = outputValue ∨ (name, value) ∈ restValues⊢ contractOk name value contractOk:Name → Value → Propenv:Envoutput:PureOutputEquationrest:List PureOutputEquationih:∀ {values : List (Name × Value)}, evalOutputEquationValues env rest = Except.ok values → OutputExpressionsSatisfyContracts contractOk env rest → ∀ (name : Name) (value : Value), (name, value) ∈ values → contractOk name valuehContracts:OutputExpressionsSatisfyContracts contractOk env (output :: rest)outputValue:ValuehOutputEval:eval env output.expr = Except.ok outputValuerestValues:List (Name × Value)hRest:evalOutputEquationValues env rest = Except.ok restValueshRestContracts:OutputExpressionsSatisfyContracts contractOk env restname:Namevalue:ValuehHead:name = output.output ∧ value = outputValue⊢ contractOk name valuecontractOk:Name → Value → Propenv:Envoutput:PureOutputEquationrest:List PureOutputEquationih:∀ {values : List (Name × Value)}, evalOutputEquationValues env rest = Except.ok values → OutputExpressionsSatisfyContracts contractOk env rest → ∀ (name : Name) (value : Value), (name, value) ∈ values → contractOk name valuehContracts:OutputExpressionsSatisfyContracts contractOk env (output :: rest)outputValue:ValuehOutputEval:eval env output.expr = Except.ok outputValuerestValues:List (Name × Value)hRest:evalOutputEquationValues env rest = Except.ok restValueshRestContracts:OutputExpressionsSatisfyContracts contractOk env restname:Namevalue:ValuehTail:(name, value) ∈ restValues⊢ contractOk name value contractOk:Name → Value → Propenv:Envoutput:PureOutputEquationrest:List PureOutputEquationih:∀ {values : List (Name × Value)}, evalOutputEquationValues env rest = Except.ok values → OutputExpressionsSatisfyContracts contractOk env rest → ∀ (name : Name) (value : Value), (name, value) ∈ values → contractOk name valuehContracts:OutputExpressionsSatisfyContracts contractOk env (output :: rest)outputValue:ValuehOutputEval:eval env output.expr = Except.ok outputValuerestValues:List (Name × Value)hRest:evalOutputEquationValues env rest = Except.ok restValueshRestContracts:OutputExpressionsSatisfyContracts contractOk env restname:Namevalue:ValuehHead:name = output.output ∧ value = outputValue⊢ contractOk name value contractOk:Name → Value → Propenv:Envoutput:PureOutputEquationrest:List PureOutputEquationih:∀ {values : List (Name × Value)}, evalOutputEquationValues env rest = Except.ok values → OutputExpressionsSatisfyContracts contractOk env rest → ∀ (name : Name) (value : Value), (name, value) ∈ values → contractOk name valuehContracts:OutputExpressionsSatisfyContracts contractOk env (output :: rest)outputValue:ValuehOutputEval:eval env output.expr = Except.ok outputValuerestValues:List (Name × Value)hRest:evalOutputEquationValues env rest = Except.ok restValueshRestContracts:OutputExpressionsSatisfyContracts contractOk env restname:Namevalue:ValuehName:name = output.outputhValue:value = outputValue⊢ contractOk name value contractOk:Name → Value → Propenv:Envoutput:PureOutputEquationrest:List PureOutputEquationih:∀ {values : List (Name × Value)}, evalOutputEquationValues env rest = Except.ok values → OutputExpressionsSatisfyContracts contractOk env rest → ∀ (name : Name) (value : Value), (name, value) ∈ values → contractOk name valuehContracts:OutputExpressionsSatisfyContracts contractOk env (output :: rest)outputValue:ValuehOutputEval:eval env output.expr = Except.ok outputValuerestValues:List (Name × Value)hRest:evalOutputEquationValues env rest = Except.ok restValueshRestContracts:OutputExpressionsSatisfyContracts contractOk env restvalue:ValuehValue:value = outputValue⊢ contractOk output.output value contractOk:Name → Value → Propenv:Envoutput:PureOutputEquationrest:List PureOutputEquationih:∀ {values : List (Name × Value)}, evalOutputEquationValues env rest = Except.ok values → OutputExpressionsSatisfyContracts contractOk env rest → ∀ (name : Name) (value : Value), (name, value) ∈ values → contractOk name valuehContracts:OutputExpressionsSatisfyContracts contractOk env (output :: rest)outputValue:ValuehOutputEval:eval env output.expr = Except.ok outputValuerestValues:List (Name × Value)hRest:evalOutputEquationValues env rest = Except.ok restValueshRestContracts:OutputExpressionsSatisfyContracts contractOk env rest⊢ contractOk output.output outputValue exact hContracts output (contractOk:Name → Value → Propenv:Envoutput:PureOutputEquationrest:List PureOutputEquationih:∀ {values : List (Name × Value)}, evalOutputEquationValues env rest = Except.ok values → OutputExpressionsSatisfyContracts contractOk env rest → ∀ (name : Name) (value : Value), (name, value) ∈ values → contractOk name valuehContracts:OutputExpressionsSatisfyContracts contractOk env (output :: rest)outputValue:ValuehOutputEval:eval env output.expr = Except.ok outputValuerestValues:List (Name × Value)hRest:evalOutputEquationValues env rest = Except.ok restValueshRestContracts:OutputExpressionsSatisfyContracts contractOk env rest⊢ output ∈ output :: rest All goals completed! 🐙) outputValue hOutputEval contractOk:Name → Value → Propenv:Envoutput:PureOutputEquationrest:List PureOutputEquationih:∀ {values : List (Name × Value)}, evalOutputEquationValues env rest = Except.ok values → OutputExpressionsSatisfyContracts contractOk env rest → ∀ (name : Name) (value : Value), (name, value) ∈ values → contractOk name valuehContracts:OutputExpressionsSatisfyContracts contractOk env (output :: rest)outputValue:ValuehOutputEval:eval env output.expr = Except.ok outputValuerestValues:List (Name × Value)hRest:evalOutputEquationValues env rest = Except.ok restValueshRestContracts:OutputExpressionsSatisfyContracts contractOk env restname:Namevalue:ValuehTail:(name, value) ∈ restValues⊢ contractOk name value All goals completed! 🐙

Output lookup exposes only names present in the evaluated output-value list.

theorem outputLookupFromValues_keys_subset {values : List (Name × Value)} {name : Name} {value : Value} (hLookup : outputLookupFromValues values name = some value) : name ∈ valueFieldNameSet values := recordFromValues_hasOnlyFields values name value hLookup

Every evaluated output-value name is present in the output lookup.

theorem outputLookupFromValues_key_present {values : List (Name × Value)} {name : Name} (hName : name ∈ valueFieldNameSet values) : ∃ value, outputLookupFromValues values name = some value := recordFromValues_field_present hName

Successful output-equation evaluation exposes only declared output labels.

theorem evalOutputEquations_keys_subset {env : Env} {outputs : List PureOutputEquation} {lookup : Name → Option Value} {name : Name} {value : Value} (hEval : evalOutputEquations env outputs = Except.ok lookup) (hLookup : lookup name = some value) : name ∈ outputEquationKeySet outputs := env:Envoutputs:List PureOutputEquationlookup:Name → Option Valuename:Namevalue:ValuehEval:evalOutputEquations env outputs = Except.ok lookuphLookup:lookup name = some value⊢ name ∈ outputEquationKeySet outputs cases hValues : evalOutputEquationValues env outputs with env:Envoutputs:List PureOutputEquationlookup:Name → Option Valuename:Namevalue:ValuehEval:evalOutputEquations env outputs = Except.ok lookuphLookup:lookup name = some valueerr:EvalErrorhValues:evalOutputEquationValues env outputs = Except.error err⊢ name ∈ outputEquationKeySet outputs All goals completed! 🐙 env:Envoutputs:List PureOutputEquationlookup:Name → Option Valuename:Namevalue:ValuehEval:evalOutputEquations env outputs = Except.ok lookuphLookup:lookup name = some valuevalues:List (Name × Value)hValues:evalOutputEquationValues env outputs = Except.ok values⊢ name ∈ outputEquationKeySet outputs env:Envoutputs:List PureOutputEquationlookup:Name → Option Valuename:Namevalue:ValuehLookup:lookup name = some valuevalues:List (Name × Value)hValues:evalOutputEquationValues env outputs = Except.ok valueshEval:outputLookupFromValues values = lookup⊢ name ∈ outputEquationKeySet outputs env:Envoutputs:List PureOutputEquationname:Namevalue:Valuevalues:List (Name × Value)hValues:evalOutputEquationValues env outputs = Except.ok valueshLookup:outputLookupFromValues values name = some value⊢ name ∈ outputEquationKeySet outputs env:Envoutputs:List PureOutputEquationname:Namevalue:Valuevalues:List (Name × Value)hValues:evalOutputEquationValues env outputs = Except.ok valueshLookup:outputLookupFromValues values name = some valuehMember:name ∈ valueFieldNameSet values⊢ name ∈ outputEquationKeySet outputs env:Envoutputs:List PureOutputEquationname:Namevalue:Valuevalues:List (Name × Value)hValues:evalOutputEquationValues env outputs = Except.ok valueshLookup:outputLookupFromValues values name = some valuehMember:name ∈ valueFieldNameSet valueshNames:valueFieldNameSet values = outputEquationKeySet outputs⊢ name ∈ outputEquationKeySet outputs All goals completed! 🐙

Every declared output label is present after successful output-equation evaluation.

theorem evalOutputEquations_keys_present {env : Env} {outputs : List PureOutputEquation} {lookup : Name → Option Value} {name : Name} (hEval : evalOutputEquations env outputs = Except.ok lookup) (hName : name ∈ outputEquationKeySet outputs) : ∃ value, lookup name = some value := env:Envoutputs:List PureOutputEquationlookup:Name → Option Valuename:NamehEval:evalOutputEquations env outputs = Except.ok lookuphName:name ∈ outputEquationKeySet outputs⊢ ∃ value, lookup name = some value cases hValues : evalOutputEquationValues env outputs with env:Envoutputs:List PureOutputEquationlookup:Name → Option Valuename:NamehEval:evalOutputEquations env outputs = Except.ok lookuphName:name ∈ outputEquationKeySet outputserr:EvalErrorhValues:evalOutputEquationValues env outputs = Except.error err⊢ ∃ value, lookup name = some value All goals completed! 🐙 env:Envoutputs:List PureOutputEquationlookup:Name → Option Valuename:NamehEval:evalOutputEquations env outputs = Except.ok lookuphName:name ∈ outputEquationKeySet outputsvalues:List (Name × Value)hValues:evalOutputEquationValues env outputs = Except.ok values⊢ ∃ value, lookup name = some value env:Envoutputs:List PureOutputEquationlookup:Name → Option Valuename:NamehName:name ∈ outputEquationKeySet outputsvalues:List (Name × Value)hValues:evalOutputEquationValues env outputs = Except.ok valueshEval:outputLookupFromValues values = lookup⊢ ∃ value, lookup name = some value env:Envoutputs:List PureOutputEquationname:NamehName:name ∈ outputEquationKeySet outputsvalues:List (Name × Value)hValues:evalOutputEquationValues env outputs = Except.ok values⊢ ∃ value, outputLookupFromValues values name = some value env:Envoutputs:List PureOutputEquationname:NamehName:name ∈ outputEquationKeySet outputsvalues:List (Name × Value)hValues:evalOutputEquationValues env outputs = Except.ok valueshNames:valueFieldNameSet values = outputEquationKeySet outputs⊢ ∃ value, outputLookupFromValues values name = some value have hValueName : name ∈ valueFieldNameSet values := env:Envoutputs:List PureOutputEquationlookup:Name → Option Valuename:NamehEval:evalOutputEquations env outputs = Except.ok lookuphName:name ∈ outputEquationKeySet outputs⊢ ∃ value, lookup name = some value All goals completed! 🐙 All goals completed! 🐙

Successful output-equation lookup satisfies abstract output contracts.

theorem evalOutputEquations_values_satisfy_outputContracts {contractOk : Name → Value → Prop} {env : Env} {outputs : List PureOutputEquation} {lookup : Name → Option Value} (hEval : evalOutputEquations env outputs = Except.ok lookup) (hContracts : OutputExpressionsSatisfyContracts contractOk env outputs) : ∀ name value, lookup name = some value → contractOk name value := contractOk:Name → Value → Propenv:Envoutputs:List PureOutputEquationlookup:Name → Option ValuehEval:evalOutputEquations env outputs = Except.ok lookuphContracts:OutputExpressionsSatisfyContracts contractOk env outputs⊢ ∀ (name : Name) (value : Value), lookup name = some value → contractOk name value cases hValues : evalOutputEquationValues env outputs with contractOk:Name → Value → Propenv:Envoutputs:List PureOutputEquationlookup:Name → Option ValuehEval:evalOutputEquations env outputs = Except.ok lookuphContracts:OutputExpressionsSatisfyContracts contractOk env outputserr:EvalErrorhValues:evalOutputEquationValues env outputs = Except.error err⊢ ∀ (name : Name) (value : Value), lookup name = some value → contractOk name value All goals completed! 🐙 contractOk:Name → Value → Propenv:Envoutputs:List PureOutputEquationlookup:Name → Option ValuehEval:evalOutputEquations env outputs = Except.ok lookuphContracts:OutputExpressionsSatisfyContracts contractOk env outputsvalues:List (Name × Value)hValues:evalOutputEquationValues env outputs = Except.ok values⊢ ∀ (name : Name) (value : Value), lookup name = some value → contractOk name value contractOk:Name → Value → Propenv:Envoutputs:List PureOutputEquationlookup:Name → Option ValuehContracts:OutputExpressionsSatisfyContracts contractOk env outputsvalues:List (Name × Value)hValues:evalOutputEquationValues env outputs = Except.ok valueshEval:outputLookupFromValues values = lookup⊢ ∀ (name : Name) (value : Value), lookup name = some value → contractOk name value contractOk:Name → Value → Propenv:Envoutputs:List PureOutputEquationhContracts:OutputExpressionsSatisfyContracts contractOk env outputsvalues:List (Name × Value)hValues:evalOutputEquationValues env outputs = Except.ok values⊢ ∀ (name : Name) (value : Value), outputLookupFromValues values name = some value → contractOk name value intro name contractOk:Name → Value → Propenv:Envoutputs:List PureOutputEquationhContracts:OutputExpressionsSatisfyContracts contractOk env outputsvalues:List (Name × Value)hValues:evalOutputEquationValues env outputs = Except.ok valuesname:Namevalue:Value⊢ outputLookupFromValues values name = some value → contractOk name value contractOk:Name → Value → Propenv:Envoutputs:List PureOutputEquationhContracts:OutputExpressionsSatisfyContracts contractOk env outputsvalues:List (Name × Value)hValues:evalOutputEquationValues env outputs = Except.ok valuesname:Namevalue:ValuehLookup:outputLookupFromValues values name = some value⊢ contractOk name value contractOk:Name → Value → Propenv:Envoutputs:List PureOutputEquationhContracts:OutputExpressionsSatisfyContracts contractOk env outputsvalues:List (Name × Value)hValues:evalOutputEquationValues env outputs = Except.ok valuesname:Namevalue:ValuehLookup:outputLookupFromValues values name = some valuehMember:(name, value) ∈ values⊢ contractOk name value All goals completed! 🐙namespace PureNode

Evaluate a source pure node to its proof-side output lookup function.

def evalOutputs (env : Env) (node : PureNode) : Except EvalError (Name → Option Value) := match evalBindings env node.bindings with | Except.error err => Except.error err | Except.ok outerEnv => match evalWhereEnv outerEnv node.whereExpr with | Except.error err => Except.error err | Except.ok localEnv => evalOutputEquations localEnv node.outputsend PureNodenamespace NativePureTaskConfig

Evaluate a native pure-task config to its proof-side output lookup function.

def evalOutputs (env : Env) (config : NativePureTaskConfig) : Except EvalError (Name → Option Value) := match evalBindings env config.bindings with | Except.error err => Except.error err | Except.ok outerEnv => match evalWhereEnv outerEnv config.whereExpr with | Except.error err => Except.error err | Except.ok localEnv => evalOutputEquations localEnv config.outputsend NativePureTaskConfig

Pure output equation keys match declared ports for admitted pure nodes.

theorem pureOutput_keys_match_declaredPorts {ctx : StaticContext} {node : PureNode} (hNode : PureNodeAdmitted ctx node) : node.outputKeys = node.outputPorts := hNode.outputs_match

Admitted where fields are disjoint from input ports.

theorem where_noInputCollision {ctx : StaticContext} {node : PureNode} {fields : Finset Name} (hNode : PureNodeAdmitted ctx node) (hFields : node.whereFields ctx = some fields) : Disjoint fields node.inputPorts := hNode.where_noInputCollision fields hFields

Admitted pure nodes expose a statically known where field set.

theorem pureNode_whereFields_known {ctx : StaticContext} {node : PureNode} (hNode : PureNodeAdmitted ctx node) : ∃ fields, node.whereFields ctx = some fields := hNode.where_static

Admitted node bindings preserve the static context when evaluated.

theorem pureNode_bindings_noShadow {ctx : StaticContext} {node : PureNode} (hNode : PureNodeAdmitted ctx node) : letBindingsDoNotShadowStatic ctx node.bindings := hNode.bindings_noShadow

Admitted where expressions satisfy the local-let safety side condition.

theorem pureNode_where_letSafe {ctx : StaticContext} {node : PureNode} {whereExpr : Expr} (hNode : PureNodeAdmitted ctx node) (hWhere : node.whereExpr = some whereExpr) : Expr.staticLetSafe ctx whereExpr := hNode.where_letSafe whereExpr hWhere

Admitted where evaluation exposes only the statically admitted fields.

theorem pureNode_where_hasOnlyFields {ctx : StaticContext} {env outerEnv : Env} {node : PureNode} {whereExpr : Expr} {whereFields : Finset Name} {whereValue : Value} (hNode : PureNodeAdmitted ctx node) (hMatch : EnvMatchesStatic env ctx) (hBindings : evalBindings env node.bindings = Except.ok outerEnv) (hWhere : node.whereExpr = some whereExpr) (hStatic : whereStaticFields ctx whereExpr = some whereFields) (hEval : eval outerEnv whereExpr = Except.ok whereValue) : Value.hasOnlyFields whereValue whereFields := ctx:StaticContextenv:EnvouterEnv:Envnode:PureNodewhereExpr:ExprwhereFields:Finset NamewhereValue:ValuehNode:PureNodeAdmitted ctx nodehMatch:EnvMatchesStatic env ctxhBindings:evalBindings env node.bindings = Except.ok outerEnvhWhere:node.whereExpr = some whereExprhStatic:whereStaticFields ctx whereExpr = some whereFieldshEval:eval outerEnv whereExpr = Except.ok whereValue⊢ whereValue.hasOnlyFields whereFields ctx:StaticContextenv:EnvouterEnv:Envnode:PureNodewhereExpr:ExprwhereFields:Finset NamewhereValue:ValuehNode:PureNodeAdmitted ctx nodehMatch:EnvMatchesStatic env ctxhBindings:evalBindings env node.bindings = Except.ok outerEnvhWhere:node.whereExpr = some whereExprhStatic:whereStaticFields ctx whereExpr = some whereFieldshEval:eval outerEnv whereExpr = Except.ok whereValuehOuterMatch:EnvMatchesStatic outerEnv ctx⊢ whereValue.hasOnlyFields whereFields ctx:StaticContextenv:EnvouterEnv:Envnode:PureNodewhereExpr:ExprwhereFields:Finset NamewhereValue:ValuehNode:PureNodeAdmitted ctx nodehMatch:EnvMatchesStatic env ctxhBindings:evalBindings env node.bindings = Except.ok outerEnvhWhere:node.whereExpr = some whereExprhStatic:whereStaticFields ctx whereExpr = some whereFieldshEval:eval outerEnv whereExpr = Except.ok whereValuehOuterMatch:EnvMatchesStatic outerEnv ctxhSafe:Expr.staticLetSafe ctx whereExpr⊢ whereValue.hasOnlyFields whereFields All goals completed! 🐙

Successful where environment evaluation opens a record with statically admitted fields.

theorem pureNode_evalWhereEnv_record_hasOnlyFields {ctx : StaticContext} {env outerEnv localEnv : Env} {node : PureNode} {whereExpr : Expr} {whereFields : Finset Name} (hNode : PureNodeAdmitted ctx node) (hMatch : EnvMatchesStatic env ctx) (hBindings : evalBindings env node.bindings = Except.ok outerEnv) (hWhere : node.whereExpr = some whereExpr) (hStatic : whereStaticFields ctx whereExpr = some whereFields) (hEvalWhere : evalWhereEnv outerEnv node.whereExpr = Except.ok localEnv) : ∃ recordFields, eval outerEnv whereExpr = Except.ok (Value.record recordFields) ∧ localEnv = openRecordIntoEnv recordFields outerEnv ∧ Value.hasOnlyFields (Value.record recordFields) whereFields := ctx:StaticContextenv:EnvouterEnv:EnvlocalEnv:Envnode:PureNodewhereExpr:ExprwhereFields:Finset NamehNode:PureNodeAdmitted ctx nodehMatch:EnvMatchesStatic env ctxhBindings:evalBindings env node.bindings = Except.ok outerEnvhWhere:node.whereExpr = some whereExprhStatic:whereStaticFields ctx whereExpr = some whereFieldshEvalWhere:evalWhereEnv outerEnv node.whereExpr = Except.ok localEnv⊢ ∃ recordFields, eval outerEnv whereExpr = Except.ok (Value.record recordFields) ∧ localEnv = openRecordIntoEnv recordFields outerEnv ∧ (Value.record recordFields).hasOnlyFields whereFields ctx:StaticContextenv:EnvouterEnv:EnvlocalEnv:Envnode:PureNodewhereExpr:ExprwhereFields:Finset NamehNode:PureNodeAdmitted ctx nodehMatch:EnvMatchesStatic env ctxhBindings:evalBindings env node.bindings = Except.ok outerEnvhWhere:node.whereExpr = some whereExprhStatic:whereStaticFields ctx whereExpr = some whereFieldshEvalWhere:(match eval outerEnv whereExpr with | Except.error err => Except.error err | Except.ok Value.null => Except.error EvalError.expectedRecord | Except.ok (Value.bool _value) => Except.error EvalError.expectedRecord | Except.ok (Value.int _value) => Except.error EvalError.expectedRecord | Except.ok (Value.string _value) => Except.error EvalError.expectedRecord | Except.ok (Value.record recordFields) => Except.ok (openRecordIntoEnv recordFields outerEnv)) = Except.ok localEnv⊢ ∃ recordFields, eval outerEnv whereExpr = Except.ok (Value.record recordFields) ∧ localEnv = openRecordIntoEnv recordFields outerEnv ∧ (Value.record recordFields).hasOnlyFields whereFields cases hEval : eval outerEnv whereExpr with ctx:StaticContextenv:EnvouterEnv:EnvlocalEnv:Envnode:PureNodewhereExpr:ExprwhereFields:Finset NamehNode:PureNodeAdmitted ctx nodehMatch:EnvMatchesStatic env ctxhBindings:evalBindings env node.bindings = Except.ok outerEnvhWhere:node.whereExpr = some whereExprhStatic:whereStaticFields ctx whereExpr = some whereFieldshEvalWhere:(match eval outerEnv whereExpr with | Except.error err => Except.error err | Except.ok Value.null => Except.error EvalError.expectedRecord | Except.ok (Value.bool _value) => Except.error EvalError.expectedRecord | Except.ok (Value.int _value) => Except.error EvalError.expectedRecord | Except.ok (Value.string _value) => Except.error EvalError.expectedRecord | Except.ok (Value.record recordFields) => Except.ok (openRecordIntoEnv recordFields outerEnv)) = Except.ok localEnverr:EvalErrorhEval:eval outerEnv whereExpr = Except.error err⊢ ∃ recordFields, Except.error err = Except.ok (Value.record recordFields) ∧ localEnv = openRecordIntoEnv recordFields outerEnv ∧ (Value.record recordFields).hasOnlyFields whereFields All goals completed! 🐙 ctx:StaticContextenv:EnvouterEnv:EnvlocalEnv:Envnode:PureNodewhereExpr:ExprwhereFields:Finset NamehNode:PureNodeAdmitted ctx nodehMatch:EnvMatchesStatic env ctxhBindings:evalBindings env node.bindings = Except.ok outerEnvhWhere:node.whereExpr = some whereExprhStatic:whereStaticFields ctx whereExpr = some whereFieldshEvalWhere:(match eval outerEnv whereExpr with | Except.error err => Except.error err | Except.ok Value.null => Except.error EvalError.expectedRecord | Except.ok (Value.bool _value) => Except.error EvalError.expectedRecord | Except.ok (Value.int _value) => Except.error EvalError.expectedRecord | Except.ok (Value.string _value) => Except.error EvalError.expectedRecord | Except.ok (Value.record recordFields) => Except.ok (openRecordIntoEnv recordFields outerEnv)) = Except.ok localEnvwhereValue:ValuehEval:eval outerEnv whereExpr = Except.ok whereValue⊢ ∃ recordFields, Except.ok whereValue = Except.ok (Value.record recordFields) ∧ localEnv = openRecordIntoEnv recordFields outerEnv ∧ (Value.record recordFields).hasOnlyFields whereFields cases whereValue with ctx:StaticContextenv:EnvouterEnv:EnvlocalEnv:Envnode:PureNodewhereExpr:ExprwhereFields:Finset NamehNode:PureNodeAdmitted ctx nodehMatch:EnvMatchesStatic env ctxhBindings:evalBindings env node.bindings = Except.ok outerEnvhWhere:node.whereExpr = some whereExprhStatic:whereStaticFields ctx whereExpr = some whereFieldshEvalWhere:(match eval outerEnv whereExpr with | Except.error err => Except.error err | Except.ok Value.null => Except.error EvalError.expectedRecord | Except.ok (Value.bool _value) => Except.error EvalError.expectedRecord | Except.ok (Value.int _value) => Except.error EvalError.expectedRecord | Except.ok (Value.string _value) => Except.error EvalError.expectedRecord | Except.ok (Value.record recordFields) => Except.ok (openRecordIntoEnv recordFields outerEnv)) = Except.ok localEnvhEval:eval outerEnv whereExpr = Except.ok Value.null⊢ ∃ recordFields, Except.ok Value.null = Except.ok (Value.record recordFields) ∧ localEnv = openRecordIntoEnv recordFields outerEnv ∧ (Value.record recordFields).hasOnlyFields whereFields All goals completed! 🐙 ctx:StaticContextenv:EnvouterEnv:EnvlocalEnv:Envnode:PureNodewhereExpr:ExprwhereFields:Finset NamehNode:PureNodeAdmitted ctx nodehMatch:EnvMatchesStatic env ctxhBindings:evalBindings env node.bindings = Except.ok outerEnvhWhere:node.whereExpr = some whereExprhStatic:whereStaticFields ctx whereExpr = some whereFieldshEvalWhere:(match eval outerEnv whereExpr with | Except.error err => Except.error err | Except.ok Value.null => Except.error EvalError.expectedRecord | Except.ok (Value.bool _value) => Except.error EvalError.expectedRecord | Except.ok (Value.int _value) => Except.error EvalError.expectedRecord | Except.ok (Value.string _value) => Except.error EvalError.expectedRecord | Except.ok (Value.record recordFields) => Except.ok (openRecordIntoEnv recordFields outerEnv)) = Except.ok localEnvwhereBool:BoolhEval:eval outerEnv whereExpr = Except.ok (Value.bool whereBool)⊢ ∃ recordFields, Except.ok (Value.bool whereBool) = Except.ok (Value.record recordFields) ∧ localEnv = openRecordIntoEnv recordFields outerEnv ∧ (Value.record recordFields).hasOnlyFields whereFields All goals completed! 🐙 ctx:StaticContextenv:EnvouterEnv:EnvlocalEnv:Envnode:PureNodewhereExpr:ExprwhereFields:Finset NamehNode:PureNodeAdmitted ctx nodehMatch:EnvMatchesStatic env ctxhBindings:evalBindings env node.bindings = Except.ok outerEnvhWhere:node.whereExpr = some whereExprhStatic:whereStaticFields ctx whereExpr = some whereFieldshEvalWhere:(match eval outerEnv whereExpr with | Except.error err => Except.error err | Except.ok Value.null => Except.error EvalError.expectedRecord | Except.ok (Value.bool _value) => Except.error EvalError.expectedRecord | Except.ok (Value.int _value) => Except.error EvalError.expectedRecord | Except.ok (Value.string _value) => Except.error EvalError.expectedRecord | Except.ok (Value.record recordFields) => Except.ok (openRecordIntoEnv recordFields outerEnv)) = Except.ok localEnvwhereInt:ℤhEval:eval outerEnv whereExpr = Except.ok (Value.int whereInt)⊢ ∃ recordFields, Except.ok (Value.int whereInt) = Except.ok (Value.record recordFields) ∧ localEnv = openRecordIntoEnv recordFields outerEnv ∧ (Value.record recordFields).hasOnlyFields whereFields All goals completed! 🐙 ctx:StaticContextenv:EnvouterEnv:EnvlocalEnv:Envnode:PureNodewhereExpr:ExprwhereFields:Finset NamehNode:PureNodeAdmitted ctx nodehMatch:EnvMatchesStatic env ctxhBindings:evalBindings env node.bindings = Except.ok outerEnvhWhere:node.whereExpr = some whereExprhStatic:whereStaticFields ctx whereExpr = some whereFieldshEvalWhere:(match eval outerEnv whereExpr with | Except.error err => Except.error err | Except.ok Value.null => Except.error EvalError.expectedRecord | Except.ok (Value.bool _value) => Except.error EvalError.expectedRecord | Except.ok (Value.int _value) => Except.error EvalError.expectedRecord | Except.ok (Value.string _value) => Except.error EvalError.expectedRecord | Except.ok (Value.record recordFields) => Except.ok (openRecordIntoEnv recordFields outerEnv)) = Except.ok localEnvwhereString:StringhEval:eval outerEnv whereExpr = Except.ok (Value.string whereString)⊢ ∃ recordFields, Except.ok (Value.string whereString) = Except.ok (Value.record recordFields) ∧ localEnv = openRecordIntoEnv recordFields outerEnv ∧ (Value.record recordFields).hasOnlyFields whereFields All goals completed! 🐙 ctx:StaticContextenv:EnvouterEnv:EnvlocalEnv:Envnode:PureNodewhereExpr:ExprwhereFields:Finset NamehNode:PureNodeAdmitted ctx nodehMatch:EnvMatchesStatic env ctxhBindings:evalBindings env node.bindings = Except.ok outerEnvhWhere:node.whereExpr = some whereExprhStatic:whereStaticFields ctx whereExpr = some whereFieldshEvalWhere:(match eval outerEnv whereExpr with | Except.error err => Except.error err | Except.ok Value.null => Except.error EvalError.expectedRecord | Except.ok (Value.bool _value) => Except.error EvalError.expectedRecord | Except.ok (Value.int _value) => Except.error EvalError.expectedRecord | Except.ok (Value.string _value) => Except.error EvalError.expectedRecord | Except.ok (Value.record recordFields) => Except.ok (openRecordIntoEnv recordFields outerEnv)) = Except.ok localEnvrecordFields:Name → Option ValuehEval:eval outerEnv whereExpr = Except.ok (Value.record recordFields)⊢ ∃ recordFields_1, Except.ok (Value.record recordFields) = Except.ok (Value.record recordFields_1) ∧ localEnv = openRecordIntoEnv recordFields_1 outerEnv ∧ (Value.record recordFields_1).hasOnlyFields whereFields ctx:StaticContextenv:EnvouterEnv:EnvlocalEnv:Envnode:PureNodewhereExpr:ExprwhereFields:Finset NamehNode:PureNodeAdmitted ctx nodehMatch:EnvMatchesStatic env ctxhBindings:evalBindings env node.bindings = Except.ok outerEnvhWhere:node.whereExpr = some whereExprhStatic:whereStaticFields ctx whereExpr = some whereFieldsrecordFields:Name → Option ValuehEval:eval outerEnv whereExpr = Except.ok (Value.record recordFields)hEvalWhere:openRecordIntoEnv recordFields outerEnv = localEnv⊢ ∃ recordFields_1, Except.ok (Value.record recordFields) = Except.ok (Value.record recordFields_1) ∧ localEnv = openRecordIntoEnv recordFields_1 outerEnv ∧ (Value.record recordFields_1).hasOnlyFields whereFields ctx:StaticContextenv:EnvouterEnv:Envnode:PureNodewhereExpr:ExprwhereFields:Finset NamehNode:PureNodeAdmitted ctx nodehMatch:EnvMatchesStatic env ctxhBindings:evalBindings env node.bindings = Except.ok outerEnvhWhere:node.whereExpr = some whereExprhStatic:whereStaticFields ctx whereExpr = some whereFieldsrecordFields:Name → Option ValuehEval:eval outerEnv whereExpr = Except.ok (Value.record recordFields)⊢ ∃ recordFields_1, Except.ok (Value.record recordFields) = Except.ok (Value.record recordFields_1) ∧ openRecordIntoEnv recordFields outerEnv = openRecordIntoEnv recordFields_1 outerEnv ∧ (Value.record recordFields_1).hasOnlyFields whereFields ctx:StaticContextenv:EnvouterEnv:Envnode:PureNodewhereExpr:ExprwhereFields:Finset NamehNode:PureNodeAdmitted ctx nodehMatch:EnvMatchesStatic env ctxhBindings:evalBindings env node.bindings = Except.ok outerEnvhWhere:node.whereExpr = some whereExprhStatic:whereStaticFields ctx whereExpr = some whereFieldsrecordFields:Name → Option ValuehEval:eval outerEnv whereExpr = Except.ok (Value.record recordFields)hWhereFields:(Value.record recordFields).hasOnlyFields whereFields⊢ ∃ recordFields_1, Except.ok (Value.record recordFields) = Except.ok (Value.record recordFields_1) ∧ openRecordIntoEnv recordFields outerEnv = openRecordIntoEnv recordFields_1 outerEnv ∧ (Value.record recordFields_1).hasOnlyFields whereFields All goals completed! 🐙

The environment produced by the where step matches static facts outside opened fields.

theorem pureNode_evalWhereEnv_localEnv_match_for_fields {ctx : StaticContext} {env outerEnv localEnv : Env} {node : PureNode} {whereFields : Finset Name} (hNode : PureNodeAdmitted ctx node) (hMatch : EnvMatchesStatic env ctx) (hBindings : evalBindings env node.bindings = Except.ok outerEnv) (hFields : node.whereFields ctx = some whereFields) (hEvalWhere : evalWhereEnv outerEnv node.whereExpr = Except.ok localEnv) : EnvMatchesStatic localEnv (StaticContext.hideFields whereFields ctx) := ctx:StaticContextenv:EnvouterEnv:EnvlocalEnv:Envnode:PureNodewhereFields:Finset NamehNode:PureNodeAdmitted ctx nodehMatch:EnvMatchesStatic env ctxhBindings:evalBindings env node.bindings = Except.ok outerEnvhFields:PureNode.whereFields ctx node = some whereFieldshEvalWhere:evalWhereEnv outerEnv node.whereExpr = Except.ok localEnv⊢ EnvMatchesStatic localEnv (StaticContext.hideFields whereFields ctx) ctx:StaticContextenv:EnvouterEnv:EnvlocalEnv:Envnode:PureNodewhereFields:Finset NamehNode:PureNodeAdmitted ctx nodehMatch:EnvMatchesStatic env ctxhBindings:evalBindings env node.bindings = Except.ok outerEnvhFields:PureNode.whereFields ctx node = some whereFieldshEvalWhere:evalWhereEnv outerEnv node.whereExpr = Except.ok localEnvhOuterMatch:EnvMatchesStatic outerEnv ctx⊢ EnvMatchesStatic localEnv (StaticContext.hideFields whereFields ctx) cases hWhere : node.whereExpr with ctx:StaticContextenv:EnvouterEnv:EnvlocalEnv:Envnode:PureNodewhereFields:Finset NamehNode:PureNodeAdmitted ctx nodehMatch:EnvMatchesStatic env ctxhBindings:evalBindings env node.bindings = Except.ok outerEnvhFields:PureNode.whereFields ctx node = some whereFieldshEvalWhere:evalWhereEnv outerEnv node.whereExpr = Except.ok localEnvhOuterMatch:EnvMatchesStatic outerEnv ctxhWhere:node.whereExpr = none⊢ EnvMatchesStatic localEnv (StaticContext.hideFields whereFields ctx) ctx:StaticContextenv:EnvouterEnv:EnvlocalEnv:Envnode:PureNodewhereFields:Finset NamehNode:PureNodeAdmitted ctx nodehMatch:EnvMatchesStatic env ctxhBindings:evalBindings env node.bindings = Except.ok outerEnvhEvalWhere:evalWhereEnv outerEnv node.whereExpr = Except.ok localEnvhOuterMatch:EnvMatchesStatic outerEnv ctxhWhere:node.whereExpr = nonehFields:∅ = whereFields⊢ EnvMatchesStatic localEnv (StaticContext.hideFields whereFields ctx) ctx:StaticContextenv:EnvouterEnv:EnvlocalEnv:Envnode:PureNodehNode:PureNodeAdmitted ctx nodehMatch:EnvMatchesStatic env ctxhBindings:evalBindings env node.bindings = Except.ok outerEnvhEvalWhere:evalWhereEnv outerEnv node.whereExpr = Except.ok localEnvhOuterMatch:EnvMatchesStatic outerEnv ctxhWhere:node.whereExpr = none⊢ EnvMatchesStatic localEnv (StaticContext.hideFields ∅ ctx) ctx:StaticContextenv:EnvouterEnv:EnvlocalEnv:Envnode:PureNodehNode:PureNodeAdmitted ctx nodehMatch:EnvMatchesStatic env ctxhBindings:evalBindings env node.bindings = Except.ok outerEnvhOuterMatch:EnvMatchesStatic outerEnv ctxhWhere:node.whereExpr = nonehEvalWhere:outerEnv = localEnv⊢ EnvMatchesStatic localEnv (StaticContext.hideFields ∅ ctx) ctx:StaticContextenv:EnvouterEnv:Envnode:PureNodehNode:PureNodeAdmitted ctx nodehMatch:EnvMatchesStatic env ctxhBindings:evalBindings env node.bindings = Except.ok outerEnvhOuterMatch:EnvMatchesStatic outerEnv ctxhWhere:node.whereExpr = none⊢ EnvMatchesStatic outerEnv (StaticContext.hideFields ∅ ctx) All goals completed! 🐙 ctx:StaticContextenv:EnvouterEnv:EnvlocalEnv:Envnode:PureNodewhereFields:Finset NamehNode:PureNodeAdmitted ctx nodehMatch:EnvMatchesStatic env ctxhBindings:evalBindings env node.bindings = Except.ok outerEnvhFields:PureNode.whereFields ctx node = some whereFieldshEvalWhere:evalWhereEnv outerEnv node.whereExpr = Except.ok localEnvhOuterMatch:EnvMatchesStatic outerEnv ctxwhereExpr:ExprhWhere:node.whereExpr = some whereExpr⊢ EnvMatchesStatic localEnv (StaticContext.hideFields whereFields ctx) have hStatic : whereStaticFields ctx whereExpr = some whereFields := ctx:StaticContextenv:EnvouterEnv:EnvlocalEnv:Envnode:PureNodewhereFields:Finset NamehNode:PureNodeAdmitted ctx nodehMatch:EnvMatchesStatic env ctxhBindings:evalBindings env node.bindings = Except.ok outerEnvhFields:PureNode.whereFields ctx node = some whereFieldshEvalWhere:evalWhereEnv outerEnv node.whereExpr = Except.ok localEnv⊢ EnvMatchesStatic localEnv (StaticContext.hideFields whereFields ctx) All goals completed! 🐙 ctx:StaticContextenv:EnvouterEnv:EnvlocalEnv:Envnode:PureNodewhereFields:Finset NamehNode:PureNodeAdmitted ctx nodehMatch:EnvMatchesStatic env ctxhBindings:evalBindings env node.bindings = Except.ok outerEnvhFields:PureNode.whereFields ctx node = some whereFieldshEvalWhere:evalWhereEnv outerEnv node.whereExpr = Except.ok localEnvhOuterMatch:EnvMatchesStatic outerEnv ctxwhereExpr:ExprhWhere:node.whereExpr = some whereExprhStatic:whereStaticFields ctx whereExpr = some whereFieldsrecordFields:Name → Option Value_hEval:eval outerEnv whereExpr = Except.ok (Value.record recordFields)hLocalEnv:localEnv = openRecordIntoEnv recordFields outerEnvhRecordFields:(Value.record recordFields).hasOnlyFields whereFields⊢ EnvMatchesStatic localEnv (StaticContext.hideFields whereFields ctx) ctx:StaticContextenv:EnvouterEnv:Envnode:PureNodewhereFields:Finset NamehNode:PureNodeAdmitted ctx nodehMatch:EnvMatchesStatic env ctxhBindings:evalBindings env node.bindings = Except.ok outerEnvhFields:PureNode.whereFields ctx node = some whereFieldshOuterMatch:EnvMatchesStatic outerEnv ctxwhereExpr:ExprhWhere:node.whereExpr = some whereExprhStatic:whereStaticFields ctx whereExpr = some whereFieldsrecordFields:Name → Option Value_hEval:eval outerEnv whereExpr = Except.ok (Value.record recordFields)hRecordFields:(Value.record recordFields).hasOnlyFields whereFieldshEvalWhere:evalWhereEnv outerEnv node.whereExpr = Except.ok (openRecordIntoEnv recordFields outerEnv)⊢ EnvMatchesStatic (openRecordIntoEnv recordFields outerEnv) (StaticContext.hideFields whereFields ctx) All goals completed! 🐙

The environment produced by the where step matches a hidden admitted static context.

theorem pureNode_evalWhereEnv_localEnv_match {ctx : StaticContext} {env outerEnv localEnv : Env} {node : PureNode} (hNode : PureNodeAdmitted ctx node) (hMatch : EnvMatchesStatic env ctx) (hBindings : evalBindings env node.bindings = Except.ok outerEnv) (hEvalWhere : evalWhereEnv outerEnv node.whereExpr = Except.ok localEnv) : ∃ whereFields, node.whereFields ctx = some whereFields ∧ EnvMatchesStatic localEnv (StaticContext.hideFields whereFields ctx) := ctx:StaticContextenv:EnvouterEnv:EnvlocalEnv:Envnode:PureNodehNode:PureNodeAdmitted ctx nodehMatch:EnvMatchesStatic env ctxhBindings:evalBindings env node.bindings = Except.ok outerEnvhEvalWhere:evalWhereEnv outerEnv node.whereExpr = Except.ok localEnv⊢ ∃ whereFields, PureNode.whereFields ctx node = some whereFields ∧ EnvMatchesStatic localEnv (StaticContext.hideFields whereFields ctx) ctx:StaticContextenv:EnvouterEnv:EnvlocalEnv:Envnode:PureNodehNode:PureNodeAdmitted ctx nodehMatch:EnvMatchesStatic env ctxhBindings:evalBindings env node.bindings = Except.ok outerEnvhEvalWhere:evalWhereEnv outerEnv node.whereExpr = Except.ok localEnvwhereFields:Finset NamehFields:PureNode.whereFields ctx node = some whereFields⊢ ∃ whereFields, PureNode.whereFields ctx node = some whereFields ∧ EnvMatchesStatic localEnv (StaticContext.hideFields whereFields ctx) All goals completed! 🐙

Successful source pure-node evaluation exposes only declared output ports.

theorem pureNode_evalOutputs_keys_in_outputPorts {ctx : StaticContext} {env : Env} {node : PureNode} {lookup : Name → Option Value} (hNode : PureNodeAdmitted ctx node) (hEval : node.evalOutputs env = Except.ok lookup) : ∀ name value, lookup name = some value → name ∈ node.outputPorts := ctx:StaticContextenv:Envnode:PureNodelookup:Name → Option ValuehNode:PureNodeAdmitted ctx nodehEval:PureNode.evalOutputs env node = Except.ok lookup⊢ ∀ (name : Name) (value : Value), lookup name = some value → name ∈ node.outputPorts cases hBindings : evalBindings env node.bindings with ctx:StaticContextenv:Envnode:PureNodelookup:Name → Option ValuehNode:PureNodeAdmitted ctx nodehEval:PureNode.evalOutputs env node = Except.ok lookuperr:EvalErrorhBindings:evalBindings env node.bindings = Except.error err⊢ ∀ (name : Name) (value : Value), lookup name = some value → name ∈ node.outputPorts All goals completed! 🐙 ctx:StaticContextenv:Envnode:PureNodelookup:Name → Option ValuehNode:PureNodeAdmitted ctx nodehEval:PureNode.evalOutputs env node = Except.ok lookupouterEnv:EnvhBindings:evalBindings env node.bindings = Except.ok outerEnv⊢ ∀ (name : Name) (value : Value), lookup name = some value → name ∈ node.outputPorts cases hWhere : evalWhereEnv outerEnv node.whereExpr with ctx:StaticContextenv:Envnode:PureNodelookup:Name → Option ValuehNode:PureNodeAdmitted ctx nodehEval:PureNode.evalOutputs env node = Except.ok lookupouterEnv:EnvhBindings:evalBindings env node.bindings = Except.ok outerEnverr:EvalErrorhWhere:evalWhereEnv outerEnv node.whereExpr = Except.error err⊢ ∀ (name : Name) (value : Value), lookup name = some value → name ∈ node.outputPorts All goals completed! 🐙 ctx:StaticContextenv:Envnode:PureNodelookup:Name → Option ValuehNode:PureNodeAdmitted ctx nodehEval:PureNode.evalOutputs env node = Except.ok lookupouterEnv:EnvhBindings:evalBindings env node.bindings = Except.ok outerEnvlocalEnv:EnvhWhere:evalWhereEnv outerEnv node.whereExpr = Except.ok localEnv⊢ ∀ (name : Name) (value : Value), lookup name = some value → name ∈ node.outputPorts have hOutputEval : evalOutputEquations localEnv node.outputs = Except.ok lookup := ctx:StaticContextenv:Envnode:PureNodelookup:Name → Option ValuehNode:PureNodeAdmitted ctx nodehEval:PureNode.evalOutputs env node = Except.ok lookup⊢ ∀ (name : Name) (value : Value), lookup name = some value → name ∈ node.outputPorts All goals completed! 🐙 intro name ctx:StaticContextenv:Envnode:PureNodelookup:Name → Option ValuehNode:PureNodeAdmitted ctx nodehEval:PureNode.evalOutputs env node = Except.ok lookupouterEnv:EnvhBindings:evalBindings env node.bindings = Except.ok outerEnvlocalEnv:EnvhWhere:evalWhereEnv outerEnv node.whereExpr = Except.ok localEnvhOutputEval:evalOutputEquations localEnv node.outputs = Except.ok lookupname:Namevalue:Value⊢ lookup name = some value → name ∈ node.outputPorts ctx:StaticContextenv:Envnode:PureNodelookup:Name → Option ValuehNode:PureNodeAdmitted ctx nodehEval:PureNode.evalOutputs env node = Except.ok lookupouterEnv:EnvhBindings:evalBindings env node.bindings = Except.ok outerEnvlocalEnv:EnvhWhere:evalWhereEnv outerEnv node.whereExpr = Except.ok localEnvhOutputEval:evalOutputEquations localEnv node.outputs = Except.ok lookupname:Namevalue:ValuehLookup:lookup name = some value⊢ name ∈ node.outputPorts ctx:StaticContextenv:Envnode:PureNodelookup:Name → Option ValuehNode:PureNodeAdmitted ctx nodehEval:PureNode.evalOutputs env node = Except.ok lookupouterEnv:EnvhBindings:evalBindings env node.bindings = Except.ok outerEnvlocalEnv:EnvhWhere:evalWhereEnv outerEnv node.whereExpr = Except.ok localEnvhOutputEval:evalOutputEquations localEnv node.outputs = Except.ok lookupname:Namevalue:ValuehLookup:lookup name = some valuehMember:name ∈ outputEquationKeySet node.outputs⊢ name ∈ node.outputPorts have hOutputKey : name ∈ node.outputKeys := ctx:StaticContextenv:Envnode:PureNodelookup:Name → Option ValuehNode:PureNodeAdmitted ctx nodehEval:PureNode.evalOutputs env node = Except.ok lookup⊢ ∀ (name : Name) (value : Value), lookup name = some value → name ∈ node.outputPorts All goals completed! 🐙 All goals completed! 🐙

Successful source pure-node evaluation produces every declared output port.

theorem pureNode_evalOutputs_outputPorts_present {ctx : StaticContext} {env : Env} {node : PureNode} {lookup : Name → Option Value} (hNode : PureNodeAdmitted ctx node) (hEval : node.evalOutputs env = Except.ok lookup) : ∀ name, name ∈ node.outputPorts → ∃ value, lookup name = some value := ctx:StaticContextenv:Envnode:PureNodelookup:Name → Option ValuehNode:PureNodeAdmitted ctx nodehEval:PureNode.evalOutputs env node = Except.ok lookup⊢ ∀ name ∈ node.outputPorts, ∃ value, lookup name = some value cases hBindings : evalBindings env node.bindings with ctx:StaticContextenv:Envnode:PureNodelookup:Name → Option ValuehNode:PureNodeAdmitted ctx nodehEval:PureNode.evalOutputs env node = Except.ok lookuperr:EvalErrorhBindings:evalBindings env node.bindings = Except.error err⊢ ∀ name ∈ node.outputPorts, ∃ value, lookup name = some value All goals completed! 🐙 ctx:StaticContextenv:Envnode:PureNodelookup:Name → Option ValuehNode:PureNodeAdmitted ctx nodehEval:PureNode.evalOutputs env node = Except.ok lookupouterEnv:EnvhBindings:evalBindings env node.bindings = Except.ok outerEnv⊢ ∀ name ∈ node.outputPorts, ∃ value, lookup name = some value cases hWhere : evalWhereEnv outerEnv node.whereExpr with ctx:StaticContextenv:Envnode:PureNodelookup:Name → Option ValuehNode:PureNodeAdmitted ctx nodehEval:PureNode.evalOutputs env node = Except.ok lookupouterEnv:EnvhBindings:evalBindings env node.bindings = Except.ok outerEnverr:EvalErrorhWhere:evalWhereEnv outerEnv node.whereExpr = Except.error err⊢ ∀ name ∈ node.outputPorts, ∃ value, lookup name = some value All goals completed! 🐙 ctx:StaticContextenv:Envnode:PureNodelookup:Name → Option ValuehNode:PureNodeAdmitted ctx nodehEval:PureNode.evalOutputs env node = Except.ok lookupouterEnv:EnvhBindings:evalBindings env node.bindings = Except.ok outerEnvlocalEnv:EnvhWhere:evalWhereEnv outerEnv node.whereExpr = Except.ok localEnv⊢ ∀ name ∈ node.outputPorts, ∃ value, lookup name = some value have hOutputEval : evalOutputEquations localEnv node.outputs = Except.ok lookup := ctx:StaticContextenv:Envnode:PureNodelookup:Name → Option ValuehNode:PureNodeAdmitted ctx nodehEval:PureNode.evalOutputs env node = Except.ok lookup⊢ ∀ name ∈ node.outputPorts, ∃ value, lookup name = some value All goals completed! 🐙 intro name ctx:StaticContextenv:Envnode:PureNodelookup:Name → Option ValuehNode:PureNodeAdmitted ctx nodehEval:PureNode.evalOutputs env node = Except.ok lookupouterEnv:EnvhBindings:evalBindings env node.bindings = Except.ok outerEnvlocalEnv:EnvhWhere:evalWhereEnv outerEnv node.whereExpr = Except.ok localEnvhOutputEval:evalOutputEquations localEnv node.outputs = Except.ok lookupname:NamehPort:name ∈ node.outputPorts⊢ ∃ value, lookup name = some value have hOutputKey : name ∈ node.outputKeys := ctx:StaticContextenv:Envnode:PureNodelookup:Name → Option ValuehNode:PureNodeAdmitted ctx nodehEval:PureNode.evalOutputs env node = Except.ok lookup⊢ ∀ name ∈ node.outputPorts, ∃ value, lookup name = some value All goals completed! 🐙 have hKeySet : name ∈ outputEquationKeySet node.outputs := ctx:StaticContextenv:Envnode:PureNodelookup:Name → Option ValuehNode:PureNodeAdmitted ctx nodehEval:PureNode.evalOutputs env node = Except.ok lookup⊢ ∀ name ∈ node.outputPorts, ∃ value, lookup name = some value All goals completed! 🐙 All goals completed! 🐙

Successful source pure-node evaluation satisfies abstract declared output contracts.

theorem pureNode_evalOutputs_values_satisfy_outputContracts {ctx : StaticContext} {env : Env} {node : PureNode} {lookup : Name → Option Value} {contractOk : Name → Value → Prop} (hNode : PureNodeAdmitted ctx node) (hEval : node.evalOutputs env = Except.ok lookup) (hContracts : ∀ outerEnv localEnv, evalBindings env node.bindings = Except.ok outerEnv → evalWhereEnv outerEnv node.whereExpr = Except.ok localEnv → OutputExpressionsSatisfyContracts contractOk localEnv node.outputs) : ∀ name value, lookup name = some value → name ∈ node.outputPorts ∧ contractOk name value := ctx:StaticContextenv:Envnode:PureNodelookup:Name → Option ValuecontractOk:Name → Value → ProphNode:PureNodeAdmitted ctx nodehEval:PureNode.evalOutputs env node = Except.ok lookuphContracts:∀ (outerEnv localEnv : Env), evalBindings env node.bindings = Except.ok outerEnv → evalWhereEnv outerEnv node.whereExpr = Except.ok localEnv → OutputExpressionsSatisfyContracts contractOk localEnv node.outputs⊢ ∀ (name : Name) (value : Value), lookup name = some value → name ∈ node.outputPorts ∧ contractOk name value cases hBindings : evalBindings env node.bindings with ctx:StaticContextenv:Envnode:PureNodelookup:Name → Option ValuecontractOk:Name → Value → ProphNode:PureNodeAdmitted ctx nodehEval:PureNode.evalOutputs env node = Except.ok lookuphContracts:∀ (outerEnv localEnv : Env), evalBindings env node.bindings = Except.ok outerEnv → evalWhereEnv outerEnv node.whereExpr = Except.ok localEnv → OutputExpressionsSatisfyContracts contractOk localEnv node.outputserr:EvalErrorhBindings:evalBindings env node.bindings = Except.error err⊢ ∀ (name : Name) (value : Value), lookup name = some value → name ∈ node.outputPorts ∧ contractOk name value All goals completed! 🐙 ctx:StaticContextenv:Envnode:PureNodelookup:Name → Option ValuecontractOk:Name → Value → ProphNode:PureNodeAdmitted ctx nodehEval:PureNode.evalOutputs env node = Except.ok lookuphContracts:∀ (outerEnv localEnv : Env), evalBindings env node.bindings = Except.ok outerEnv → evalWhereEnv outerEnv node.whereExpr = Except.ok localEnv → OutputExpressionsSatisfyContracts contractOk localEnv node.outputsouterEnv:EnvhBindings:evalBindings env node.bindings = Except.ok outerEnv⊢ ∀ (name : Name) (value : Value), lookup name = some value → name ∈ node.outputPorts ∧ contractOk name value cases hWhere : evalWhereEnv outerEnv node.whereExpr with ctx:StaticContextenv:Envnode:PureNodelookup:Name → Option ValuecontractOk:Name → Value → ProphNode:PureNodeAdmitted ctx nodehEval:PureNode.evalOutputs env node = Except.ok lookuphContracts:∀ (outerEnv localEnv : Env), evalBindings env node.bindings = Except.ok outerEnv → evalWhereEnv outerEnv node.whereExpr = Except.ok localEnv → OutputExpressionsSatisfyContracts contractOk localEnv node.outputsouterEnv:EnvhBindings:evalBindings env node.bindings = Except.ok outerEnverr:EvalErrorhWhere:evalWhereEnv outerEnv node.whereExpr = Except.error err⊢ ∀ (name : Name) (value : Value), lookup name = some value → name ∈ node.outputPorts ∧ contractOk name value All goals completed! 🐙 ctx:StaticContextenv:Envnode:PureNodelookup:Name → Option ValuecontractOk:Name → Value → ProphNode:PureNodeAdmitted ctx nodehEval:PureNode.evalOutputs env node = Except.ok lookuphContracts:∀ (outerEnv localEnv : Env), evalBindings env node.bindings = Except.ok outerEnv → evalWhereEnv outerEnv node.whereExpr = Except.ok localEnv → OutputExpressionsSatisfyContracts contractOk localEnv node.outputsouterEnv:EnvhBindings:evalBindings env node.bindings = Except.ok outerEnvlocalEnv:EnvhWhere:evalWhereEnv outerEnv node.whereExpr = Except.ok localEnv⊢ ∀ (name : Name) (value : Value), lookup name = some value → name ∈ node.outputPorts ∧ contractOk name value have hOutputEval : evalOutputEquations localEnv node.outputs = Except.ok lookup := ctx:StaticContextenv:Envnode:PureNodelookup:Name → Option ValuecontractOk:Name → Value → ProphNode:PureNodeAdmitted ctx nodehEval:PureNode.evalOutputs env node = Except.ok lookuphContracts:∀ (outerEnv localEnv : Env), evalBindings env node.bindings = Except.ok outerEnv → evalWhereEnv outerEnv node.whereExpr = Except.ok localEnv → OutputExpressionsSatisfyContracts contractOk localEnv node.outputs⊢ ∀ (name : Name) (value : Value), lookup name = some value → name ∈ node.outputPorts ∧ contractOk name value All goals completed! 🐙 intro name ctx:StaticContextenv:Envnode:PureNodelookup:Name → Option ValuecontractOk:Name → Value → ProphNode:PureNodeAdmitted ctx nodehEval:PureNode.evalOutputs env node = Except.ok lookuphContracts:∀ (outerEnv localEnv : Env), evalBindings env node.bindings = Except.ok outerEnv → evalWhereEnv outerEnv node.whereExpr = Except.ok localEnv → OutputExpressionsSatisfyContracts contractOk localEnv node.outputsouterEnv:EnvhBindings:evalBindings env node.bindings = Except.ok outerEnvlocalEnv:EnvhWhere:evalWhereEnv outerEnv node.whereExpr = Except.ok localEnvhOutputEval:evalOutputEquations localEnv node.outputs = Except.ok lookupname:Namevalue:Value⊢ lookup name = some value → name ∈ node.outputPorts ∧ contractOk name value ctx:StaticContextenv:Envnode:PureNodelookup:Name → Option ValuecontractOk:Name → Value → ProphNode:PureNodeAdmitted ctx nodehEval:PureNode.evalOutputs env node = Except.ok lookuphContracts:∀ (outerEnv localEnv : Env), evalBindings env node.bindings = Except.ok outerEnv → evalWhereEnv outerEnv node.whereExpr = Except.ok localEnv → OutputExpressionsSatisfyContracts contractOk localEnv node.outputsouterEnv:EnvhBindings:evalBindings env node.bindings = Except.ok outerEnvlocalEnv:EnvhWhere:evalWhereEnv outerEnv node.whereExpr = Except.ok localEnvhOutputEval:evalOutputEquations localEnv node.outputs = Except.ok lookupname:Namevalue:ValuehLookup:lookup name = some value⊢ name ∈ node.outputPorts ∧ contractOk name value ctx:StaticContextenv:Envnode:PureNodelookup:Name → Option ValuecontractOk:Name → Value → ProphNode:PureNodeAdmitted ctx nodehEval:PureNode.evalOutputs env node = Except.ok lookuphContracts:∀ (outerEnv localEnv : Env), evalBindings env node.bindings = Except.ok outerEnv → evalWhereEnv outerEnv node.whereExpr = Except.ok localEnv → OutputExpressionsSatisfyContracts contractOk localEnv node.outputsouterEnv:EnvhBindings:evalBindings env node.bindings = Except.ok outerEnvlocalEnv:EnvhWhere:evalWhereEnv outerEnv node.whereExpr = Except.ok localEnvhOutputEval:evalOutputEquations localEnv node.outputs = Except.ok lookupname:Namevalue:ValuehLookup:lookup name = some value⊢ name ∈ node.outputPortsctx:StaticContextenv:Envnode:PureNodelookup:Name → Option ValuecontractOk:Name → Value → ProphNode:PureNodeAdmitted ctx nodehEval:PureNode.evalOutputs env node = Except.ok lookuphContracts:∀ (outerEnv localEnv : Env), evalBindings env node.bindings = Except.ok outerEnv → evalWhereEnv outerEnv node.whereExpr = Except.ok localEnv → OutputExpressionsSatisfyContracts contractOk localEnv node.outputsouterEnv:EnvhBindings:evalBindings env node.bindings = Except.ok outerEnvlocalEnv:EnvhWhere:evalWhereEnv outerEnv node.whereExpr = Except.ok localEnvhOutputEval:evalOutputEquations localEnv node.outputs = Except.ok lookupname:Namevalue:ValuehLookup:lookup name = some value⊢ contractOk name value ctx:StaticContextenv:Envnode:PureNodelookup:Name → Option ValuecontractOk:Name → Value → ProphNode:PureNodeAdmitted ctx nodehEval:PureNode.evalOutputs env node = Except.ok lookuphContracts:∀ (outerEnv localEnv : Env), evalBindings env node.bindings = Except.ok outerEnv → evalWhereEnv outerEnv node.whereExpr = Except.ok localEnv → OutputExpressionsSatisfyContracts contractOk localEnv node.outputsouterEnv:EnvhBindings:evalBindings env node.bindings = Except.ok outerEnvlocalEnv:EnvhWhere:evalWhereEnv outerEnv node.whereExpr = Except.ok localEnvhOutputEval:evalOutputEquations localEnv node.outputs = Except.ok lookupname:Namevalue:ValuehLookup:lookup name = some value⊢ name ∈ node.outputPorts All goals completed! 🐙 ctx:StaticContextenv:Envnode:PureNodelookup:Name → Option ValuecontractOk:Name → Value → ProphNode:PureNodeAdmitted ctx nodehEval:PureNode.evalOutputs env node = Except.ok lookuphContracts:∀ (outerEnv localEnv : Env), evalBindings env node.bindings = Except.ok outerEnv → evalWhereEnv outerEnv node.whereExpr = Except.ok localEnv → OutputExpressionsSatisfyContracts contractOk localEnv node.outputsouterEnv:EnvhBindings:evalBindings env node.bindings = Except.ok outerEnvlocalEnv:EnvhWhere:evalWhereEnv outerEnv node.whereExpr = Except.ok localEnvhOutputEval:evalOutputEquations localEnv node.outputs = Except.ok lookupname:Namevalue:ValuehLookup:lookup name = some value⊢ contractOk name value All goals completed! 🐙

Successful source pure-node evaluation satisfies the proof-side value-contract table.

theorem pureNode_evalOutputs_values_satisfy_valueContracts {ctx : StaticContext} {env : Env} {node : PureNode} {lookup : Name → Option Value} {contracts : OutputValueContracts} (hNode : PureNodeAdmitted ctx node) (hEval : node.evalOutputs env = Except.ok lookup) (hContracts : ∀ outerEnv localEnv, evalBindings env node.bindings = Except.ok outerEnv → evalWhereEnv outerEnv node.whereExpr = Except.ok localEnv → OutputExpressionsSatisfyContracts (outputValueContractOk contracts) localEnv node.outputs) : ∀ name value, lookup name = some value → name ∈ node.outputPorts ∧ outputValueContractOk contracts name value := pureNode_evalOutputs_values_satisfy_outputContracts hNode hEval hContracts

Source pure nodes lower to one native pure task.

theorem pureNode_lowers_to_one_nativeTask (ctx : StaticContext) (node : PureNode) : (lowerPureNode ctx node).kind = LoweredNodeKind.nativePure := rfl

Lowering preserves source pure-node output evaluation in the proof-side evaluator.

theorem pureNode_lowering_evalOutputs_eq (ctx : StaticContext) (env : Env) (node : PureNode) : (lowerPureNode ctx node).config.evalOutputs env = node.evalOutputs env := rfl

CorePure evaluation is deterministic because it is a pure function.

theorem pureEvaluation_deterministic {env : Env} {expr : Expr} {left right : Value} (hLeft : eval env expr = Except.ok left) (hRight : eval env expr = Except.ok right) : left = right := env:Envexpr:Exprleft:Valueright:ValuehLeft:eval env expr = Except.ok lefthRight:eval env expr = Except.ok right⊢ left = right env:Envexpr:Exprleft:Valueright:ValuehLeft:eval env expr = Except.ok lefthRight:Except.ok left = Except.ok right⊢ left = right env:Envexpr:Exprleft:ValuehLeft:eval env expr = Except.ok left⊢ left = left All goals completed! 🐙end CorePureend Cortex.Wire