Repository navigation
Expand file tree
/
Copy pathvalue_model_test.cpp
More file actions
152 lines (140 loc) · 8.56 KB
/
Copy pathvalue_model_test.cpp
File metadata and controls
152 lines (140 loc) · 8.56 KB
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
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
#include "cppl/kernel/arithmetic.hpp"
#include "cppl/kernel/check.hpp"
#include "cppl/kernel/context.hpp"
#include "cppl/kernel/proof.hpp"
#include "cppl/kernel/proposition.hpp"
#include "cppl/kernel/substitution.hpp"
#include "cppl/kernel/term.hpp"
#include "cppl/kernel/types.hpp"
#include "cppl/testing/test.hpp"
#include <compare>
namespace {
namespace k = cppl::kernel;
const auto u32 = k::Type::integer(32, k::Signedness::Unsigned);
const auto object = k::Type::value("object", {k::Type{k::kBoolean}, u32});
const auto variable = k::Term::variable({0});
auto reflexive(const k::Type& domain, const k::Type& type, const k::Term& term) {
return k::check({}, k::Proposition::for_all(domain, k::Proposition::equality(type, term, term)),
k::ProofTerm::forall_introduction(domain, k::ProofTerm::reflexivity()), {});
}
} // namespace
CPPL_TEST(abstract_values_and_projections_have_checked_types) {
CPPL_CHECK(reflexive(object, object, variable));
CPPL_CHECK(reflexive(object, u32, k::Term::project(object, 1, variable)));
const auto nested = k::Type::value("nested", {object});
const auto field = k::Term::project(nested, 0, variable);
CPPL_CHECK(reflexive(nested, u32, k::Term::project(object, 1, field)));
}
CPPL_TEST(projection_corruption_fails_independently_of_frontend) {
CPPL_CHECK(!reflexive(object, u32, k::Term::project(object, 0, variable)));
CPPL_CHECK(!reflexive(object, u32, k::Term::project(object, 2, variable)));
CPPL_CHECK(!reflexive(object, u32, k::Term::project(u32, 0, variable)));
CPPL_CHECK(!reflexive(object, u32, k::Term::project(k::Type::value("other", {u32}), 0, variable)));
CPPL_CHECK(!reflexive(object, u32, k::Term::project(k::Type::value("object", {u32}), 0, variable)));
auto malformed = k::Term::project(object, 1, variable);
std::get<k::Projection>(malformed.node).arguments.clear();
CPPL_CHECK(!reflexive(object, u32, malformed));
std::get<k::Projection>(malformed.node).arguments = {variable, variable};
CPPL_CHECK(!reflexive(object, u32, malformed));
CPPL_CHECK(!reflexive(k::Type::value(""), k::Type::value(""), variable));
}
CPPL_TEST(abstract_observations_do_not_manufacture_facts) {
const auto tag = k::Term::project(object, 0, variable);
CPPL_CHECK(!k::check({}, k::Proposition::for_all(object, k::predicate(tag, true)),
k::ProofTerm::forall_introduction(object, k::ProofTerm::reflexivity()), {}));
const auto field = k::Term::project(object, 1, variable);
const auto goal =
k::Proposition::for_all(object, k::Proposition::equality(u32, field, k::Term::literal(u32.integer_type(), 42)));
CPPL_CHECK(!k::check({}, goal, k::ProofTerm::forall_introduction(object, k::ProofTerm::reflexivity()), {}));
}
CPPL_TEST(projection_substitution_is_capture_safe_and_normalization_is_structural) {
const auto field = k::Term::project(object, 1, variable);
const auto shifted = k::Term::project(object, 1, k::Term::variable({2}));
CPPL_CHECK_EQ(k::shift(field, 2), shifted);
CPPL_CHECK_EQ(k::instantiate(field, k::Term::variable({2})), shifted);
CPPL_CHECK_EQ(*k::normalize({}, field), field);
CPPL_CHECK(std::is_neq(k::compare(field, k::Term::project(object, 0, variable))));
CPPL_CHECK(std::is_eq(k::compare(field, field)));
}
// Indexed observation (FOUNDATIONS.md 45). The index is a term, so these tests
// pin the properties a constant-position projection cannot express.
namespace {
const auto indexed = k::Type::indexed(u32, 4);
const auto zero = k::Term::literal(u32.integer_type(), 0);
const auto one = k::Term::literal(u32.integer_type(), 1);
} // namespace
CPPL_TEST(indexed_observations_have_checked_types) {
CPPL_CHECK(reflexive(indexed, u32, k::Term::element(indexed, variable, zero)));
// The index ranges over the whole integer type: an observation past the
// extent is well-typed, because bounds are a separate obligation and not a
// premise of term formation.
CPPL_CHECK(reflexive(indexed, u32, k::Term::element(indexed, variable, k::Term::literal(u32.integer_type(), 99))));
// An element of an abstract value type, and an indexed domain nested in one.
const auto rows = k::Type::indexed(object, 2);
CPPL_CHECK(reflexive(rows, u32, k::Term::project(object, 1, k::Term::element(rows, variable, zero))));
}
CPPL_TEST(indexed_observation_corruption_fails_independently_of_frontend) {
// A domain that is not indexed, and one whose extent admits nothing.
CPPL_CHECK(!reflexive(indexed, u32, k::Term::element(object, variable, zero)));
CPPL_CHECK(!reflexive(indexed, u32, k::Term::element(u32, variable, zero)));
CPPL_CHECK(!reflexive(k::Type::indexed(u32, 0), u32, k::Term::element(k::Type::indexed(u32, 0), variable, zero)));
// The extent is part of type identity, so a subject of one extent does not
// enter a domain of another.
CPPL_CHECK(!reflexive(indexed, u32, k::Term::element(k::Type::indexed(u32, 8), variable, zero)));
// The result type is the element type, not something else.
CPPL_CHECK(!reflexive(indexed, k::Type{k::kBoolean}, k::Term::element(indexed, variable, zero)));
// A non-integer index. The subject is correct and the index is well-typed
// on its own, so only the index-type rule can reject this: under a domain
// of `object` elements, an element observation yields an `object`, which is
// a legal term but not a legal index.
const auto objects = k::Type::indexed(object, 4);
CPPL_CHECK(reflexive(objects, object, k::Term::element(objects, variable, zero)));
CPPL_CHECK(
!reflexive(objects, object, k::Term::element(objects, variable, k::Term::element(objects, variable, zero))));
// Wrong arities.
auto malformed = k::Term::element(indexed, variable, zero);
std::get<k::Element>(malformed.node).arguments.clear();
CPPL_CHECK(!reflexive(indexed, u32, malformed));
std::get<k::Element>(malformed.node).arguments = {variable};
CPPL_CHECK(!reflexive(indexed, u32, malformed));
std::get<k::Element>(malformed.node).arguments = {variable, zero, zero};
CPPL_CHECK(!reflexive(indexed, u32, malformed));
}
CPPL_TEST(indexed_observation_proves_no_bound_and_no_element_value) {
// Forming the observation must not establish anything about the index, and
// must not decide the observed value (SPEC.md STORAGE-005).
const auto at = k::Term::element(indexed, variable, zero);
const auto goal =
k::Proposition::for_all(indexed, k::Proposition::equality(u32, at, k::Term::literal(u32.integer_type(), 42)));
CPPL_CHECK(!k::check({}, goal, k::ProofTerm::forall_introduction(indexed, k::ProofTerm::reflexivity()), {}));
CPPL_CHECK(!k::check({}, k::Proposition::for_all(indexed, k::predicate(at, true)),
k::ProofTerm::forall_introduction(indexed, k::ProofTerm::reflexivity()), {}));
}
CPPL_TEST(indexed_observation_admits_neither_injectivity_nor_extensionality) {
// Two observations of one subject at different index terms are different
// terms, and nothing proves them equal or unequal (SPEC.md STORAGE-005,
// TRUST.md TCB-CORE-016).
const auto first = k::Term::element(indexed, variable, zero);
const auto second = k::Term::element(indexed, variable, one);
CPPL_CHECK(std::is_neq(k::compare(first, second)));
CPPL_CHECK(!k::check({}, k::Proposition::for_all(indexed, k::Proposition::equality(u32, first, second)),
k::ProofTerm::forall_introduction(indexed, k::ProofTerm::reflexivity()), {}));
// Equal observations do not prove equal subjects: reflexivity closes a goal
// only when the two sides are already the same term.
CPPL_CHECK(std::is_eq(k::compare(first, k::Term::element(indexed, variable, zero))));
CPPL_CHECK(std::is_neq(k::compare(first, k::Term::element(indexed, k::Term::variable({1}), zero))));
}
CPPL_TEST(indexed_observation_substitution_reaches_subject_and_index) {
// Both operands are substituted: an index left untouched by instantiation
// would bound a different term than the one the observation reads
// (ARCHITECTURE.md ARCH-ELEM-004).
const auto at = k::Term::element(indexed, variable, variable);
const auto shifted = k::Term::element(indexed, k::Term::variable({2}), k::Term::variable({2}));
CPPL_CHECK_EQ(k::shift(at, 2), shifted);
CPPL_CHECK_EQ(k::instantiate(at, k::Term::variable({2})), shifted);
CPPL_CHECK_EQ(*k::normalize({}, at), at);
// Normalization is structural: the observation has no reduction rule, so it
// never selects a component of anything.
const auto constant = k::Term::element(indexed, variable, zero);
CPPL_CHECK_EQ(*k::normalize({}, constant), constant);
}