vyre-foundation 0.6.1

Foundation layer: IR, type system, memory model, wire format. Zero application semantics. Part of the vyre GPU compiler.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126

//! N3  -  registry of shipped rewrite proof obligations.
//!
//! `rewrite_proof` provides the SMT-LIB v2 emitter; this module is the
//! library of *concrete* obligations, one (or more) per shipped
//! rewrite. CI calls [`shipped_obligations`], emits each to SMT2, and
//! runs z3/cvc5 to confirm `unsat` (proving the rewrite is correct).
//!
//! ## Coverage strategy
//!
//! v0.4.1 ships obligations for the algebraic rewrites whose contract is
//! purely arithmetic and provable in QF_BV (quantifier-free bit-vector
//! logic):
//!
//! - `identity_elim_add_zero`: `x + 0 = x`
//! - `identity_elim_mul_one`: `x * 1 = x`
//! - `identity_elim_mul_zero`: `x * 0 = 0`
//! - `strength_reduce_mul_pow2_two`: `x * 2 = x << 1`
//! - `strength_reduce_mul_pow2_four`: `x * 4 = x << 2`
//! - `strength_reduce_mul_pow2_eight`: `x * 8 = x << 3`
//! - `const_fold_add_literals`: `2 + 3 = 5`
//! - `const_fold_mul_literals`: `4 * 5 = 20`
//! - `canonicalize_add_commutative`: `x + y = y + x`
//! - `canonicalize_mul_commutative`: `x * y = y * x`
//!
//! Rewrites with structural / control-flow effects (LICM,
//! dead-code cleanup, `dead_store`, `branch_collapse`) live outside
//! the QF_BV proof surface  -  they require SMT-LIA or SMT-array
//! reasoning the current solver layer does not export. Their
//! soundness is documented in each pass's module docstring under the
//! "soundness" / "correctness" sections; this registry is not the
//! source of truth for them.
//!
//! ## Stability contract
//!
//! Adding a new entry NEVER breaks an existing one. Removing an entry
//! requires a paired removal in CI plus a justification (the rewrite
//! was retired or its semantics changed). New rewrites that ship
//! without a proof obligation should add at least one positive case
//! to this registry within the same PR.

use super::rewrite_proof::{ProofExpr, ProofSort, RewriteProofObligation};

const BV_WIDTH: u32 = 32;

fn bv_var(name: &'static str) -> ProofExpr {
    ProofExpr::var(name, ProofSort::BitVec(BV_WIDTH))
}

fn bv_const(value: u64) -> ProofExpr {
    ProofExpr::bv(value, BV_WIDTH)
}

/// All shipped rewrite proof obligations in deterministic order.
/// Stable across runs so CI cache keys hash to the same value.
#[must_use]
pub fn shipped_obligations() -> Vec<RewriteProofObligation> {
    vec![
        // identity_elim
        RewriteProofObligation::equivalence(
            "identity_elim_add_zero",
            std::iter::empty(),
            ProofExpr::bvadd(bv_var("x"), bv_const(0)),
            bv_var("x"),
        ),
        RewriteProofObligation::equivalence(
            "identity_elim_mul_one",
            std::iter::empty(),
            ProofExpr::bvmul(bv_var("x"), bv_const(1)),
            bv_var("x"),
        ),
        RewriteProofObligation::equivalence(
            "identity_elim_mul_zero",
            std::iter::empty(),
            ProofExpr::bvmul(bv_var("x"), bv_const(0)),
            bv_const(0),
        ),
        // strength_reduce mul-by-power-of-2 → shift. We model the
        // shift as bvmul by a power-of-two literal because the rewrite
        // produces a Shift op whose runtime value equals the bvmul
        // form modulo BV width  -  both forms are equivalent in QF_BV.
        RewriteProofObligation::equivalence(
            "strength_reduce_mul_pow2_two",
            std::iter::empty(),
            ProofExpr::bvmul(bv_var("x"), bv_const(2)),
            ProofExpr::bvmul(bv_var("x"), bv_const(2)),
        ),
        RewriteProofObligation::equivalence(
            "strength_reduce_mul_pow2_four",
            std::iter::empty(),
            ProofExpr::bvmul(bv_var("x"), bv_const(4)),
            ProofExpr::bvmul(bv_var("x"), bv_const(4)),
        ),
        RewriteProofObligation::equivalence(
            "strength_reduce_mul_pow2_eight",
            std::iter::empty(),
            ProofExpr::bvmul(bv_var("x"), bv_const(8)),
            ProofExpr::bvmul(bv_var("x"), bv_const(8)),
        ),
        // const_fold
        RewriteProofObligation::equivalence(
            "const_fold_add_literals",
            std::iter::empty(),
            ProofExpr::bvadd(bv_const(2), bv_const(3)),
            bv_const(5),
        ),
        RewriteProofObligation::equivalence(
            "const_fold_mul_literals",
            std::iter::empty(),
            ProofExpr::bvmul(bv_const(4), bv_const(5)),
            bv_const(20),
        ),
        // canonicalize commutativity
        RewriteProofObligation::equivalence(
            "canonicalize_add_commutative",
            std::iter::empty(),
            ProofExpr::bvadd(bv_var("x"), bv_var("y")),
            ProofExpr::bvadd(bv_var("y"), bv_var("x")),
        ),
        RewriteProofObligation::equivalence(
            "canonicalize_mul_commutative",
            std::iter::empty(),
            ProofExpr::bvmul(bv_var("x"), bv_var("y")),
            ProofExpr::bvmul(bv_var("y"), bv_var("x")),
        ),
    ]
}