legacy_model.bend checks

raw source on the hub · import 0x3bdc0c9f5265bb49f7fc76b61f529f24/legacy_model.bend as Legacy_model

PROOF-ONLY historical list model. Not imported by the production API.

6 imports

import Base
import ./core.bend as Runtime
import ./state.bend as State
import ./core_model.bend as Core
import ./packed.bend as Packed
import ./conformance.bend as Proof

Definitions

def constants source · line 11 · raw

List<&2, U32>

The core refinement theorem quantifies over every constant table. Instantiate the verified core with the FIPS 180-4 constants.

def sha256 source · line 29 · raw

@bytes:List<&2, U32> -> List<&2, U32>

def ascii source · line 32 · raw

@s:String -> List<&2, U32>

def hex source · line 35 · raw

@ws:List<&2, U32> -> String

def digest_bytes source · line 39 · raw

@ws:List<&2, U32> -> List<&2, U32>

Big-endian octets, represented as U32 values in 0..255.

def sha256_bytes source · line 49 · raw

@bytes:List<&2, U32> -> List<&2, U32>

def packed_digest source · line 52 · raw

@r:Maybe<&2, 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State> -> Maybe<&2, List<&2, U32>>

def sha256_packed source · line 59 · raw

@words:Array<U32> -> @byte_length:Nat -> Maybe<&2, List<&2, U32>>

Four bytes per U32, big-endian word order. Returns None for an oversized length. This consumes the array; existing list APIs above retain their original behavior.