oxilean_std/bitvec/
functions.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4#![allow(clippy::items_after_test_module)]
5
6use oxilean_kernel::Node;
7use oxilean_kernel::{BinderInfo, Declaration, Environment, Expr, Level, Name};
8
9/// Build a function application `f a`.
10#[allow(dead_code)]
11pub fn app(f: Expr, a: Expr) -> Expr {
12    Expr::App(Node::new(f), Node::new(a))
13}
14/// Build a function application `f a b`.
15#[allow(dead_code)]
16pub fn app2(f: Expr, a: Expr, b: Expr) -> Expr {
17    app(app(f, a), b)
18}
19/// Build a function application `f a b c`.
20#[allow(dead_code)]
21pub fn app3(f: Expr, a: Expr, b: Expr, c: Expr) -> Expr {
22    app(app2(f, a, b), c)
23}
24/// Build `Pi (name : dom), body` with given binder info.
25#[allow(dead_code)]
26pub fn pi(bi: BinderInfo, name: &str, dom: Expr, body: Expr) -> Expr {
27    Expr::Pi(bi, Name::str(name), Node::new(dom), Node::new(body))
28}
29/// Build a non-dependent arrow `A -> B`.
30#[allow(dead_code)]
31pub fn arrow(a: Expr, b: Expr) -> Expr {
32    pi(BinderInfo::Default, "_", a, b)
33}
34/// Named constant with no universe levels.
35#[allow(dead_code)]
36pub fn cst(s: &str) -> Expr {
37    Expr::Const(Name::str(s), vec![])
38}
39/// Prop: `Sort 0`.
40#[allow(dead_code)]
41pub fn prop() -> Expr {
42    Expr::Sort(Level::zero())
43}
44/// Type 1: `Sort 1`.
45#[allow(dead_code)]
46pub fn type1() -> Expr {
47    Expr::Sort(Level::succ(Level::zero()))
48}
49/// Bound variable.
50#[allow(dead_code)]
51pub fn bvar(n: u32) -> Expr {
52    Expr::BVar(n)
53}
54/// Nat type.
55#[allow(dead_code)]
56pub fn nat_ty() -> Expr {
57    cst("Nat")
58}
59/// Int type.
60#[allow(dead_code)]
61pub fn int_ty() -> Expr {
62    cst("Int")
63}
64/// Bool type.
65#[allow(dead_code)]
66pub fn bool_ty() -> Expr {
67    cst("Bool")
68}
69/// Build `BitVec n` type expression.
70#[allow(dead_code)]
71pub fn mk_bitvec(n: Expr) -> Expr {
72    app(cst("BitVec"), n)
73}
74/// Build `BitVec.ofNat n val`.
75#[allow(dead_code)]
76pub fn mk_bitvec_of_nat(n: Expr, val: Expr) -> Expr {
77    app2(cst("BitVec.ofNat"), n, val)
78}
79/// Build `BitVec.zero n`.
80#[allow(dead_code)]
81pub fn mk_bitvec_zero(n: Expr) -> Expr {
82    app(cst("BitVec.zero"), n)
83}
84/// Build `BitVec.and a b` (implicit n).
85#[allow(dead_code)]
86pub fn mk_bitvec_and(a: Expr, b: Expr) -> Expr {
87    app2(cst("BitVec.and"), a, b)
88}
89/// Build `BitVec.or a b` (implicit n).
90#[allow(dead_code)]
91pub fn mk_bitvec_or(a: Expr, b: Expr) -> Expr {
92    app2(cst("BitVec.or"), a, b)
93}
94/// Build `BitVec.xor a b` (implicit n).
95#[allow(dead_code)]
96pub fn mk_bitvec_xor(a: Expr, b: Expr) -> Expr {
97    app2(cst("BitVec.xor"), a, b)
98}
99/// Build `BitVec.add a b` (implicit n).
100#[allow(dead_code)]
101pub fn mk_bitvec_add(a: Expr, b: Expr) -> Expr {
102    app2(cst("BitVec.add"), a, b)
103}
104/// Build `BitVec.sub a b` (implicit n).
105#[allow(dead_code)]
106pub fn mk_bitvec_sub(a: Expr, b: Expr) -> Expr {
107    app2(cst("BitVec.sub"), a, b)
108}
109/// Build `BitVec.mul a b` (implicit n).
110#[allow(dead_code)]
111pub fn mk_bitvec_mul(a: Expr, b: Expr) -> Expr {
112    app2(cst("BitVec.mul"), a, b)
113}
114/// Build `Eq @{} ty a b`.
115#[allow(dead_code)]
116pub fn mk_eq(ty: Expr, a: Expr, b: Expr) -> Expr {
117    app3(cst("Eq"), ty, a, b)
118}
119/// Build `Eq @{} (BitVec n) a b` where n is a bvar.
120#[allow(dead_code)]
121pub fn mk_bv_eq(n: Expr, a: Expr, b: Expr) -> Expr {
122    mk_eq(mk_bitvec(n), a, b)
123}
124/// Build `Iff a b`.
125#[allow(dead_code)]
126pub fn mk_iff(a: Expr, b: Expr) -> Expr {
127    app2(cst("Iff"), a, b)
128}
129/// Build `Eq @{} Nat a b`.
130#[allow(dead_code)]
131pub fn mk_nat_eq(a: Expr, b: Expr) -> Expr {
132    mk_eq(nat_ty(), a, b)
133}
134#[allow(dead_code)]
135pub fn add_axiom(
136    env: &mut Environment,
137    name: &str,
138    univ_params: Vec<Name>,
139    ty: Expr,
140) -> Result<(), String> {
141    env.add(Declaration::Axiom {
142        name: Name::str(name),
143        univ_params,
144        ty,
145    })
146    .map_err(|e| e.to_string())
147}
148/// `∀ {n : Nat}, BitVec n → BitVec n → BitVec n`
149#[allow(dead_code)]
150pub fn bitvec_binop_ty() -> Expr {
151    pi(
152        BinderInfo::Implicit,
153        "n",
154        nat_ty(),
155        arrow(
156            mk_bitvec(bvar(0)),
157            arrow(mk_bitvec(bvar(1)), mk_bitvec(bvar(2))),
158        ),
159    )
160}
161/// `∀ {n : Nat}, BitVec n → BitVec n`
162#[allow(dead_code)]
163pub fn bitvec_unop_ty() -> Expr {
164    pi(
165        BinderInfo::Implicit,
166        "n",
167        nat_ty(),
168        arrow(mk_bitvec(bvar(0)), mk_bitvec(bvar(1))),
169    )
170}
171/// `∀ {n : Nat}, BitVec n → Nat → BitVec n`
172#[allow(dead_code)]
173pub fn bitvec_shift_ty() -> Expr {
174    pi(
175        BinderInfo::Implicit,
176        "n",
177        nat_ty(),
178        arrow(mk_bitvec(bvar(0)), arrow(nat_ty(), mk_bitvec(bvar(1)))),
179    )
180}
181/// `∀ {n : Nat}, BitVec n → BitVec n → Bool`
182#[allow(dead_code)]
183pub fn bitvec_cmp_ty() -> Expr {
184    pi(
185        BinderInfo::Implicit,
186        "n",
187        nat_ty(),
188        arrow(mk_bitvec(bvar(0)), arrow(mk_bitvec(bvar(1)), bool_ty())),
189    )
190}
191/// `∀ {n : Nat}, BitVec n → Nat → Bool`
192#[allow(dead_code)]
193pub fn bitvec_getbit_ty() -> Expr {
194    pi(
195        BinderInfo::Implicit,
196        "n",
197        nat_ty(),
198        arrow(mk_bitvec(bvar(0)), arrow(nat_ty(), bool_ty())),
199    )
200}
201/// Build the BitVec environment, adding the BitVec type, operations,
202/// and theorems as axioms.
203///
204/// Assumes `Nat`, `Int`, `Bool`, `Eq`, and `Iff` are already declared in `env`.
205#[allow(clippy::too_many_lines)]
206pub fn build_bitvec_env(env: &mut Environment) -> Result<(), String> {
207    add_axiom(env, "BitVec", vec![], arrow(nat_ty(), type1()))?;
208    let of_nat_ty = pi(
209        BinderInfo::Default,
210        "n",
211        nat_ty(),
212        arrow(nat_ty(), mk_bitvec(bvar(0))),
213    );
214    add_axiom(env, "BitVec.ofNat", vec![], of_nat_ty)?;
215    let to_nat_ty = pi(
216        BinderInfo::Implicit,
217        "n",
218        nat_ty(),
219        arrow(mk_bitvec(bvar(0)), nat_ty()),
220    );
221    add_axiom(env, "BitVec.toNat", vec![], to_nat_ty)?;
222    let of_bool_ty = arrow(bool_ty(), mk_bitvec(app(cst("Nat.succ"), cst("Nat.zero"))));
223    add_axiom(env, "BitVec.ofBool", vec![], of_bool_ty)?;
224    let zero_ty = pi(BinderInfo::Default, "n", nat_ty(), mk_bitvec(bvar(0)));
225    add_axiom(env, "BitVec.zero", vec![], zero_ty)?;
226    let all_ones_ty = pi(BinderInfo::Default, "n", nat_ty(), mk_bitvec(bvar(0)));
227    add_axiom(env, "BitVec.allOnes", vec![], all_ones_ty)?;
228    add_axiom(env, "BitVec.and", vec![], bitvec_binop_ty())?;
229    add_axiom(env, "BitVec.or", vec![], bitvec_binop_ty())?;
230    add_axiom(env, "BitVec.xor", vec![], bitvec_binop_ty())?;
231    add_axiom(env, "BitVec.not", vec![], bitvec_unop_ty())?;
232    add_axiom(env, "BitVec.shiftLeft", vec![], bitvec_shift_ty())?;
233    add_axiom(env, "BitVec.shiftRight", vec![], bitvec_shift_ty())?;
234    add_axiom(env, "BitVec.add", vec![], bitvec_binop_ty())?;
235    add_axiom(env, "BitVec.sub", vec![], bitvec_binop_ty())?;
236    add_axiom(env, "BitVec.mul", vec![], bitvec_binop_ty())?;
237    add_axiom(env, "BitVec.neg", vec![], bitvec_unop_ty())?;
238    add_axiom(env, "BitVec.udiv", vec![], bitvec_binop_ty())?;
239    add_axiom(env, "BitVec.umod", vec![], bitvec_binop_ty())?;
240    add_axiom(env, "BitVec.sdiv", vec![], bitvec_binop_ty())?;
241    add_axiom(env, "BitVec.smod", vec![], bitvec_binop_ty())?;
242    add_axiom(env, "BitVec.ult", vec![], bitvec_cmp_ty())?;
243    add_axiom(env, "BitVec.ule", vec![], bitvec_cmp_ty())?;
244    add_axiom(env, "BitVec.slt", vec![], bitvec_cmp_ty())?;
245    add_axiom(env, "BitVec.sle", vec![], bitvec_cmp_ty())?;
246    add_axiom(env, "BitVec.beq", vec![], bitvec_cmp_ty())?;
247    add_axiom(env, "BitVec.getLsb", vec![], bitvec_getbit_ty())?;
248    add_axiom(env, "BitVec.getMsb", vec![], bitvec_getbit_ty())?;
249    let set_width_ty = pi(
250        BinderInfo::Implicit,
251        "n",
252        nat_ty(),
253        pi(
254            BinderInfo::Default,
255            "m",
256            nat_ty(),
257            arrow(mk_bitvec(bvar(1)), mk_bitvec(bvar(0))),
258        ),
259    );
260    add_axiom(env, "BitVec.setWidth", vec![], set_width_ty)?;
261    let append_ty = pi(
262        BinderInfo::Implicit,
263        "n",
264        nat_ty(),
265        pi(
266            BinderInfo::Implicit,
267            "m",
268            nat_ty(),
269            arrow(
270                mk_bitvec(bvar(1)),
271                arrow(
272                    mk_bitvec(bvar(1)),
273                    mk_bitvec(app2(cst("Nat.add"), bvar(3), bvar(2))),
274                ),
275            ),
276        ),
277    );
278    add_axiom(env, "BitVec.append", vec![], append_ty)?;
279    let extract_lsb_ty = pi(
280        BinderInfo::Implicit,
281        "n",
282        nat_ty(),
283        pi(
284            BinderInfo::Default,
285            "hi",
286            nat_ty(),
287            pi(
288                BinderInfo::Default,
289                "lo",
290                nat_ty(),
291                arrow(
292                    mk_bitvec(bvar(2)),
293                    mk_bitvec(app2(
294                        cst("Nat.add"),
295                        app2(cst("Nat.sub"), bvar(2), bvar(1)),
296                        app(cst("Nat.succ"), cst("Nat.zero")),
297                    )),
298                ),
299            ),
300        ),
301    );
302    add_axiom(env, "BitVec.extractLsb", vec![], extract_lsb_ty)?;
303    let replicate_ty = pi(
304        BinderInfo::Implicit,
305        "n",
306        nat_ty(),
307        pi(
308            BinderInfo::Default,
309            "k",
310            nat_ty(),
311            arrow(
312                mk_bitvec(bvar(1)),
313                mk_bitvec(app2(cst("Nat.mul"), bvar(1), bvar(2))),
314            ),
315        ),
316    );
317    add_axiom(env, "BitVec.replicate", vec![], replicate_ty)?;
318    add_axiom(env, "BitVec.rotateLeft", vec![], bitvec_shift_ty())?;
319    add_axiom(env, "BitVec.rotateRight", vec![], bitvec_shift_ty())?;
320    let sign_extend_ty = pi(
321        BinderInfo::Implicit,
322        "n",
323        nat_ty(),
324        pi(
325            BinderInfo::Default,
326            "m",
327            nat_ty(),
328            arrow(mk_bitvec(bvar(1)), mk_bitvec(bvar(0))),
329        ),
330    );
331    add_axiom(env, "BitVec.signExtend", vec![], sign_extend_ty)?;
332    let to_int_ty = pi(
333        BinderInfo::Implicit,
334        "n",
335        nat_ty(),
336        arrow(mk_bitvec(bvar(0)), int_ty()),
337    );
338    add_axiom(env, "BitVec.toInt", vec![], to_int_ty)?;
339    let of_int_ty = pi(
340        BinderInfo::Default,
341        "n",
342        nat_ty(),
343        arrow(int_ty(), mk_bitvec(bvar(0))),
344    );
345    add_axiom(env, "BitVec.ofInt", vec![], of_int_ty)?;
346    let add_comm_ty = pi(
347        BinderInfo::Implicit,
348        "n",
349        nat_ty(),
350        pi(
351            BinderInfo::Default,
352            "a",
353            mk_bitvec(bvar(0)),
354            pi(
355                BinderInfo::Default,
356                "b",
357                mk_bitvec(bvar(1)),
358                mk_bv_eq(
359                    bvar(2),
360                    app2(cst("BitVec.add"), bvar(1), bvar(0)),
361                    app2(cst("BitVec.add"), bvar(0), bvar(1)),
362                ),
363            ),
364        ),
365    );
366    add_axiom(env, "BitVec.add_comm", vec![], add_comm_ty)?;
367    let add_assoc_ty = pi(
368        BinderInfo::Implicit,
369        "n",
370        nat_ty(),
371        pi(
372            BinderInfo::Default,
373            "a",
374            mk_bitvec(bvar(0)),
375            pi(
376                BinderInfo::Default,
377                "b",
378                mk_bitvec(bvar(1)),
379                pi(
380                    BinderInfo::Default,
381                    "c",
382                    mk_bitvec(bvar(2)),
383                    mk_bv_eq(
384                        bvar(3),
385                        app2(
386                            cst("BitVec.add"),
387                            app2(cst("BitVec.add"), bvar(2), bvar(1)),
388                            bvar(0),
389                        ),
390                        app2(
391                            cst("BitVec.add"),
392                            bvar(2),
393                            app2(cst("BitVec.add"), bvar(1), bvar(0)),
394                        ),
395                    ),
396                ),
397            ),
398        ),
399    );
400    add_axiom(env, "BitVec.add_assoc", vec![], add_assoc_ty)?;
401    let add_zero_ty = pi(
402        BinderInfo::Implicit,
403        "n",
404        nat_ty(),
405        pi(
406            BinderInfo::Default,
407            "a",
408            mk_bitvec(bvar(0)),
409            mk_bv_eq(
410                bvar(1),
411                app2(cst("BitVec.add"), bvar(0), app(cst("BitVec.zero"), bvar(1))),
412                bvar(0),
413            ),
414        ),
415    );
416    add_axiom(env, "BitVec.add_zero", vec![], add_zero_ty)?;
417    let zero_add_ty = pi(
418        BinderInfo::Implicit,
419        "n",
420        nat_ty(),
421        pi(
422            BinderInfo::Default,
423            "a",
424            mk_bitvec(bvar(0)),
425            mk_bv_eq(
426                bvar(1),
427                app2(cst("BitVec.add"), app(cst("BitVec.zero"), bvar(1)), bvar(0)),
428                bvar(0),
429            ),
430        ),
431    );
432    add_axiom(env, "BitVec.zero_add", vec![], zero_add_ty)?;
433    let and_comm_ty = pi(
434        BinderInfo::Implicit,
435        "n",
436        nat_ty(),
437        pi(
438            BinderInfo::Default,
439            "a",
440            mk_bitvec(bvar(0)),
441            pi(
442                BinderInfo::Default,
443                "b",
444                mk_bitvec(bvar(1)),
445                mk_bv_eq(
446                    bvar(2),
447                    app2(cst("BitVec.and"), bvar(1), bvar(0)),
448                    app2(cst("BitVec.and"), bvar(0), bvar(1)),
449                ),
450            ),
451        ),
452    );
453    add_axiom(env, "BitVec.and_comm", vec![], and_comm_ty)?;
454    let and_assoc_ty = pi(
455        BinderInfo::Implicit,
456        "n",
457        nat_ty(),
458        pi(
459            BinderInfo::Default,
460            "a",
461            mk_bitvec(bvar(0)),
462            pi(
463                BinderInfo::Default,
464                "b",
465                mk_bitvec(bvar(1)),
466                pi(
467                    BinderInfo::Default,
468                    "c",
469                    mk_bitvec(bvar(2)),
470                    mk_bv_eq(
471                        bvar(3),
472                        app2(
473                            cst("BitVec.and"),
474                            app2(cst("BitVec.and"), bvar(2), bvar(1)),
475                            bvar(0),
476                        ),
477                        app2(
478                            cst("BitVec.and"),
479                            bvar(2),
480                            app2(cst("BitVec.and"), bvar(1), bvar(0)),
481                        ),
482                    ),
483                ),
484            ),
485        ),
486    );
487    add_axiom(env, "BitVec.and_assoc", vec![], and_assoc_ty)?;
488    let or_comm_ty = pi(
489        BinderInfo::Implicit,
490        "n",
491        nat_ty(),
492        pi(
493            BinderInfo::Default,
494            "a",
495            mk_bitvec(bvar(0)),
496            pi(
497                BinderInfo::Default,
498                "b",
499                mk_bitvec(bvar(1)),
500                mk_bv_eq(
501                    bvar(2),
502                    app2(cst("BitVec.or"), bvar(1), bvar(0)),
503                    app2(cst("BitVec.or"), bvar(0), bvar(1)),
504                ),
505            ),
506        ),
507    );
508    add_axiom(env, "BitVec.or_comm", vec![], or_comm_ty)?;
509    let or_assoc_ty = pi(
510        BinderInfo::Implicit,
511        "n",
512        nat_ty(),
513        pi(
514            BinderInfo::Default,
515            "a",
516            mk_bitvec(bvar(0)),
517            pi(
518                BinderInfo::Default,
519                "b",
520                mk_bitvec(bvar(1)),
521                pi(
522                    BinderInfo::Default,
523                    "c",
524                    mk_bitvec(bvar(2)),
525                    mk_bv_eq(
526                        bvar(3),
527                        app2(
528                            cst("BitVec.or"),
529                            app2(cst("BitVec.or"), bvar(2), bvar(1)),
530                            bvar(0),
531                        ),
532                        app2(
533                            cst("BitVec.or"),
534                            bvar(2),
535                            app2(cst("BitVec.or"), bvar(1), bvar(0)),
536                        ),
537                    ),
538                ),
539            ),
540        ),
541    );
542    add_axiom(env, "BitVec.or_assoc", vec![], or_assoc_ty)?;
543    let xor_self_ty = pi(
544        BinderInfo::Implicit,
545        "n",
546        nat_ty(),
547        pi(
548            BinderInfo::Default,
549            "a",
550            mk_bitvec(bvar(0)),
551            mk_bv_eq(
552                bvar(1),
553                app2(cst("BitVec.xor"), bvar(0), bvar(0)),
554                app(cst("BitVec.zero"), bvar(1)),
555            ),
556        ),
557    );
558    add_axiom(env, "BitVec.xor_self", vec![], xor_self_ty)?;
559    let and_self_ty = pi(
560        BinderInfo::Implicit,
561        "n",
562        nat_ty(),
563        pi(
564            BinderInfo::Default,
565            "a",
566            mk_bitvec(bvar(0)),
567            mk_bv_eq(bvar(1), app2(cst("BitVec.and"), bvar(0), bvar(0)), bvar(0)),
568        ),
569    );
570    add_axiom(env, "BitVec.and_self", vec![], and_self_ty)?;
571    let or_self_ty = pi(
572        BinderInfo::Implicit,
573        "n",
574        nat_ty(),
575        pi(
576            BinderInfo::Default,
577            "a",
578            mk_bitvec(bvar(0)),
579            mk_bv_eq(bvar(1), app2(cst("BitVec.or"), bvar(0), bvar(0)), bvar(0)),
580        ),
581    );
582    add_axiom(env, "BitVec.or_self", vec![], or_self_ty)?;
583    let not_not_ty = pi(
584        BinderInfo::Implicit,
585        "n",
586        nat_ty(),
587        pi(
588            BinderInfo::Default,
589            "a",
590            mk_bitvec(bvar(0)),
591            mk_bv_eq(
592                bvar(1),
593                app(cst("BitVec.not"), app(cst("BitVec.not"), bvar(0))),
594                bvar(0),
595            ),
596        ),
597    );
598    add_axiom(env, "BitVec.not_not", vec![], not_not_ty)?;
599    let demorgan_and_ty = pi(
600        BinderInfo::Implicit,
601        "n",
602        nat_ty(),
603        pi(
604            BinderInfo::Default,
605            "a",
606            mk_bitvec(bvar(0)),
607            pi(
608                BinderInfo::Default,
609                "b",
610                mk_bitvec(bvar(1)),
611                mk_bv_eq(
612                    bvar(2),
613                    app(cst("BitVec.not"), app2(cst("BitVec.and"), bvar(1), bvar(0))),
614                    app2(
615                        cst("BitVec.or"),
616                        app(cst("BitVec.not"), bvar(1)),
617                        app(cst("BitVec.not"), bvar(0)),
618                    ),
619                ),
620            ),
621        ),
622    );
623    add_axiom(env, "BitVec.demorgan_and", vec![], demorgan_and_ty)?;
624    let demorgan_or_ty = pi(
625        BinderInfo::Implicit,
626        "n",
627        nat_ty(),
628        pi(
629            BinderInfo::Default,
630            "a",
631            mk_bitvec(bvar(0)),
632            pi(
633                BinderInfo::Default,
634                "b",
635                mk_bitvec(bvar(1)),
636                mk_bv_eq(
637                    bvar(2),
638                    app(cst("BitVec.not"), app2(cst("BitVec.or"), bvar(1), bvar(0))),
639                    app2(
640                        cst("BitVec.and"),
641                        app(cst("BitVec.not"), bvar(1)),
642                        app(cst("BitVec.not"), bvar(0)),
643                    ),
644                ),
645            ),
646        ),
647    );
648    add_axiom(env, "BitVec.demorgan_or", vec![], demorgan_or_ty)?;
649    let to_nat_of_nat_ty = pi(
650        BinderInfo::Default,
651        "n",
652        nat_ty(),
653        pi(
654            BinderInfo::Default,
655            "val",
656            nat_ty(),
657            mk_nat_eq(
658                app(
659                    cst("BitVec.toNat"),
660                    app2(cst("BitVec.ofNat"), bvar(1), bvar(0)),
661                ),
662                app2(
663                    cst("Nat.mod"),
664                    bvar(0),
665                    app2(
666                        cst("Nat.pow"),
667                        app(cst("Nat.succ"), app(cst("Nat.succ"), cst("Nat.zero"))),
668                        bvar(1),
669                    ),
670                ),
671            ),
672        ),
673    );
674    add_axiom(env, "BitVec.toNat_ofNat", vec![], to_nat_of_nat_ty)?;
675    let of_nat_to_nat_ty = pi(
676        BinderInfo::Implicit,
677        "n",
678        nat_ty(),
679        pi(
680            BinderInfo::Default,
681            "v",
682            mk_bitvec(bvar(0)),
683            mk_bv_eq(
684                bvar(1),
685                app2(
686                    cst("BitVec.ofNat"),
687                    bvar(1),
688                    app(cst("BitVec.toNat"), bvar(0)),
689                ),
690                bvar(0),
691            ),
692        ),
693    );
694    add_axiom(env, "BitVec.ofNat_toNat", vec![], of_nat_to_nat_ty)?;
695    Ok(())
696}
697#[cfg(test)]
698mod tests {
699    use super::*;
700    /// Set up a minimal environment with prerequisite declarations.
701    fn setup_env() -> Environment {
702        let mut env = Environment::new();
703        env.add(Declaration::Axiom {
704            name: Name::str("Nat"),
705            univ_params: vec![],
706            ty: type1(),
707        })
708        .expect("operation should succeed");
709        for name in &[
710            "Nat.zero", "Nat.succ", "Nat.add", "Nat.mul", "Nat.sub", "Nat.mod", "Nat.pow",
711        ] {
712            env.add(Declaration::Axiom {
713                name: Name::str(*name),
714                univ_params: vec![],
715                ty: nat_ty(),
716            })
717            .expect("operation should succeed");
718        }
719        env.add(Declaration::Axiom {
720            name: Name::str("Int"),
721            univ_params: vec![],
722            ty: type1(),
723        })
724        .expect("operation should succeed");
725        env.add(Declaration::Axiom {
726            name: Name::str("Bool"),
727            univ_params: vec![],
728            ty: type1(),
729        })
730        .expect("operation should succeed");
731        for name in &["true", "false"] {
732            env.add(Declaration::Axiom {
733                name: Name::str(*name),
734                univ_params: vec![],
735                ty: bool_ty(),
736            })
737            .expect("operation should succeed");
738        }
739        env.add(Declaration::Axiom {
740            name: Name::str("Eq"),
741            univ_params: vec![],
742            ty: prop(),
743        })
744        .expect("operation should succeed");
745        env.add(Declaration::Axiom {
746            name: Name::str("Iff"),
747            univ_params: vec![],
748            ty: prop(),
749        })
750        .expect("operation should succeed");
751        env
752    }
753    /// Build a full test environment.
754    fn full_env() -> Environment {
755        let mut env = setup_env();
756        build_bitvec_env(&mut env).expect("build_bitvec_env should succeed");
757        env
758    }
759    #[test]
760    fn test_build_bitvec_env_succeeds() {
761        let _ = full_env();
762    }
763    #[test]
764    fn test_bitvec_type_present() {
765        let env = full_env();
766        assert!(env.contains(&Name::str("BitVec")));
767    }
768    #[test]
769    fn test_bitvec_constructors_present() {
770        let env = full_env();
771        let names = [
772            "BitVec.ofNat",
773            "BitVec.toNat",
774            "BitVec.ofBool",
775            "BitVec.zero",
776            "BitVec.allOnes",
777        ];
778        for name in &names {
779            assert!(
780                env.contains(&Name::str(*name)),
781                "missing constructor: {}",
782                name
783            );
784        }
785    }
786    #[test]
787    fn test_bitvec_bitwise_ops_present() {
788        let env = full_env();
789        let names = [
790            "BitVec.and",
791            "BitVec.or",
792            "BitVec.xor",
793            "BitVec.not",
794            "BitVec.shiftLeft",
795            "BitVec.shiftRight",
796        ];
797        for name in &names {
798            assert!(
799                env.contains(&Name::str(*name)),
800                "missing bitwise op: {}",
801                name
802            );
803        }
804    }
805    #[test]
806    fn test_bitvec_arithmetic_ops_present() {
807        let env = full_env();
808        let names = [
809            "BitVec.add",
810            "BitVec.sub",
811            "BitVec.mul",
812            "BitVec.neg",
813            "BitVec.udiv",
814            "BitVec.umod",
815            "BitVec.sdiv",
816            "BitVec.smod",
817        ];
818        for name in &names {
819            assert!(
820                env.contains(&Name::str(*name)),
821                "missing arith op: {}",
822                name
823            );
824        }
825    }
826    #[test]
827    fn test_bitvec_comparison_ops_present() {
828        let env = full_env();
829        let names = [
830            "BitVec.ult",
831            "BitVec.ule",
832            "BitVec.slt",
833            "BitVec.sle",
834            "BitVec.beq",
835        ];
836        for name in &names {
837            assert!(
838                env.contains(&Name::str(*name)),
839                "missing comparison: {}",
840                name
841            );
842        }
843    }
844    #[test]
845    fn test_bitvec_bit_ops_present() {
846        let env = full_env();
847        let names = [
848            "BitVec.getLsb",
849            "BitVec.getMsb",
850            "BitVec.setWidth",
851            "BitVec.append",
852            "BitVec.extractLsb",
853            "BitVec.replicate",
854            "BitVec.rotateLeft",
855            "BitVec.rotateRight",
856            "BitVec.signExtend",
857        ];
858        for name in &names {
859            assert!(env.contains(&Name::str(*name)), "missing bit op: {}", name);
860        }
861    }
862    #[test]
863    fn test_bitvec_conversion_present() {
864        let env = full_env();
865        let names = ["BitVec.toInt", "BitVec.ofInt"];
866        for name in &names {
867            assert!(
868                env.contains(&Name::str(*name)),
869                "missing conversion: {}",
870                name
871            );
872        }
873    }
874    #[test]
875    fn test_bitvec_theorems_present() {
876        let env = full_env();
877        let names = [
878            "BitVec.add_comm",
879            "BitVec.add_assoc",
880            "BitVec.add_zero",
881            "BitVec.zero_add",
882            "BitVec.and_comm",
883            "BitVec.and_assoc",
884            "BitVec.or_comm",
885            "BitVec.or_assoc",
886            "BitVec.xor_self",
887            "BitVec.and_self",
888            "BitVec.or_self",
889            "BitVec.not_not",
890            "BitVec.demorgan_and",
891            "BitVec.demorgan_or",
892            "BitVec.toNat_ofNat",
893            "BitVec.ofNat_toNat",
894        ];
895        for name in &names {
896            assert!(env.contains(&Name::str(*name)), "missing theorem: {}", name);
897        }
898    }
899    #[test]
900    fn test_bitvec_type_is_arrow() {
901        let env = full_env();
902        let decl = env
903            .get(&Name::str("BitVec"))
904            .expect("declaration 'BitVec' should exist in env");
905        let ty = decl.ty();
906        assert!(ty.is_pi());
907    }
908    #[test]
909    fn test_bitvec_of_nat_type_is_pi() {
910        let env = full_env();
911        let decl = env
912            .get(&Name::str("BitVec.ofNat"))
913            .expect("declaration 'BitVec.ofNat' should exist in env");
914        let ty = decl.ty();
915        assert!(ty.is_pi());
916    }
917    #[test]
918    fn test_bitvec_and_type_is_pi() {
919        let env = full_env();
920        let decl = env
921            .get(&Name::str("BitVec.and"))
922            .expect("declaration 'BitVec.and' should exist in env");
923        let ty = decl.ty();
924        assert!(ty.is_pi());
925        if let Expr::Pi(bi, _, dom, _) = ty {
926            assert_eq!(*bi, BinderInfo::Implicit);
927            assert_eq!(**dom, nat_ty());
928        }
929    }
930    #[test]
931    fn test_bitvec_add_type_is_pi() {
932        let env = full_env();
933        let decl = env
934            .get(&Name::str("BitVec.add"))
935            .expect("declaration 'BitVec.add' should exist in env");
936        let ty = decl.ty();
937        assert!(ty.is_pi());
938    }
939    #[test]
940    fn test_bitvec_ult_type_is_pi() {
941        let env = full_env();
942        let decl = env
943            .get(&Name::str("BitVec.ult"))
944            .expect("declaration 'BitVec.ult' should exist in env");
945        let ty = decl.ty();
946        assert!(ty.is_pi());
947    }
948    #[test]
949    fn test_bitvec_get_lsb_type_is_pi() {
950        let env = full_env();
951        let decl = env
952            .get(&Name::str("BitVec.getLsb"))
953            .expect("declaration 'BitVec.getLsb' should exist in env");
954        let ty = decl.ty();
955        assert!(ty.is_pi());
956    }
957    #[test]
958    fn test_bitvec_to_int_type_is_pi() {
959        let env = full_env();
960        let decl = env
961            .get(&Name::str("BitVec.toInt"))
962            .expect("declaration 'BitVec.toInt' should exist in env");
963        let ty = decl.ty();
964        assert!(ty.is_pi());
965    }
966    #[test]
967    fn test_bitvec_add_comm_type_is_pi() {
968        let env = full_env();
969        let decl = env
970            .get(&Name::str("BitVec.add_comm"))
971            .expect("declaration 'BitVec.add_comm' should exist in env");
972        let ty = decl.ty();
973        assert!(ty.is_pi());
974    }
975    #[test]
976    fn test_bitvec_not_not_type_is_pi() {
977        let env = full_env();
978        let decl = env
979            .get(&Name::str("BitVec.not_not"))
980            .expect("declaration 'BitVec.not_not' should exist in env");
981        let ty = decl.ty();
982        assert!(ty.is_pi());
983    }
984    #[test]
985    fn test_bitvec_append_type_is_pi() {
986        let env = full_env();
987        let decl = env
988            .get(&Name::str("BitVec.append"))
989            .expect("declaration 'BitVec.append' should exist in env");
990        let ty = decl.ty();
991        assert!(ty.is_pi());
992    }
993    #[test]
994    fn test_mk_bitvec_structure() {
995        let e = mk_bitvec(cst("n"));
996        if let Expr::App(f, arg) = &e {
997            assert_eq!(**f, cst("BitVec"));
998            assert_eq!(**arg, cst("n"));
999        } else {
1000            panic!("expected App");
1001        }
1002    }
1003    #[test]
1004    fn test_mk_bitvec_of_nat_structure() {
1005        let e = mk_bitvec_of_nat(cst("n"), cst("val"));
1006        assert!(e.is_app());
1007    }
1008    #[test]
1009    fn test_mk_bitvec_zero_structure() {
1010        let e = mk_bitvec_zero(cst("n"));
1011        if let Expr::App(f, arg) = &e {
1012            assert_eq!(**f, cst("BitVec.zero"));
1013            assert_eq!(**arg, cst("n"));
1014        } else {
1015            panic!("expected App");
1016        }
1017    }
1018    #[test]
1019    fn test_mk_bitvec_and_structure() {
1020        let e = mk_bitvec_and(cst("a"), cst("b"));
1021        assert!(e.is_app());
1022    }
1023    #[test]
1024    fn test_mk_bitvec_or_structure() {
1025        let e = mk_bitvec_or(cst("a"), cst("b"));
1026        assert!(e.is_app());
1027    }
1028    #[test]
1029    fn test_mk_bitvec_xor_structure() {
1030        let e = mk_bitvec_xor(cst("a"), cst("b"));
1031        assert!(e.is_app());
1032    }
1033    #[test]
1034    fn test_mk_bitvec_add_structure() {
1035        let e = mk_bitvec_add(cst("a"), cst("b"));
1036        assert!(e.is_app());
1037    }
1038    #[test]
1039    fn test_mk_bitvec_sub_structure() {
1040        let e = mk_bitvec_sub(cst("a"), cst("b"));
1041        assert!(e.is_app());
1042    }
1043    #[test]
1044    fn test_mk_bitvec_mul_structure() {
1045        let e = mk_bitvec_mul(cst("a"), cst("b"));
1046        assert!(e.is_app());
1047    }
1048    #[test]
1049    fn test_total_declaration_count() {
1050        let env = full_env();
1051        let prereq_count = 13;
1052        assert!(
1053            env.len() >= prereq_count + 52,
1054            "expected at least {} declarations, got {}",
1055            prereq_count + 52,
1056            env.len()
1057        );
1058    }
1059    #[test]
1060    fn test_bitvec_set_width_type_structure() {
1061        let env = full_env();
1062        let decl = env
1063            .get(&Name::str("BitVec.setWidth"))
1064            .expect("declaration 'BitVec.setWidth' should exist in env");
1065        let ty = decl.ty();
1066        assert!(ty.is_pi());
1067        if let Expr::Pi(bi, _, dom, _) = ty {
1068            assert_eq!(*bi, BinderInfo::Implicit);
1069            assert_eq!(**dom, nat_ty());
1070        }
1071    }
1072    #[test]
1073    fn test_bitvec_sign_extend_type_structure() {
1074        let env = full_env();
1075        let decl = env
1076            .get(&Name::str("BitVec.signExtend"))
1077            .expect("declaration 'BitVec.signExtend' should exist in env");
1078        let ty = decl.ty();
1079        assert!(ty.is_pi());
1080    }
1081    #[test]
1082    fn test_bitvec_of_bool_type_structure() {
1083        let env = full_env();
1084        let decl = env
1085            .get(&Name::str("BitVec.ofBool"))
1086            .expect("declaration 'BitVec.ofBool' should exist in env");
1087        let ty = decl.ty();
1088        assert!(ty.is_pi());
1089        if let Expr::Pi(_, _, dom, _) = ty {
1090            assert_eq!(**dom, bool_ty());
1091        }
1092    }
1093}
1094/// Build `∀ {n} (a b : BitVec n), P a b` — the standard two-bitvec quantifier.
1095#[allow(dead_code)]
1096pub fn bvx_ext_forall_two(body_builder: impl Fn() -> Expr) -> Expr {
1097    pi(
1098        BinderInfo::Implicit,
1099        "n",
1100        nat_ty(),
1101        pi(
1102            BinderInfo::Default,
1103            "a",
1104            mk_bitvec(bvar(0)),
1105            pi(BinderInfo::Default, "b", mk_bitvec(bvar(1)), body_builder()),
1106        ),
1107    )
1108}
1109/// Build `∀ {n} (a : BitVec n), P a`.
1110#[allow(dead_code)]
1111pub fn bvx_ext_forall_one(body_builder: impl Fn() -> Expr) -> Expr {
1112    pi(
1113        BinderInfo::Implicit,
1114        "n",
1115        nat_ty(),
1116        pi(BinderInfo::Default, "a", mk_bitvec(bvar(0)), body_builder()),
1117    )
1118}
1119/// Build `∀ {n} (a b c : BitVec n), P a b c`.
1120#[allow(dead_code)]
1121pub fn bvx_ext_forall_three(body_builder: impl Fn() -> Expr) -> Expr {
1122    pi(
1123        BinderInfo::Implicit,
1124        "n",
1125        nat_ty(),
1126        pi(
1127            BinderInfo::Default,
1128            "a",
1129            mk_bitvec(bvar(0)),
1130            pi(
1131                BinderInfo::Default,
1132                "b",
1133                mk_bitvec(bvar(1)),
1134                pi(BinderInfo::Default, "c", mk_bitvec(bvar(2)), body_builder()),
1135            ),
1136        ),
1137    )
1138}
1139/// Build `∀ {n} (a : BitVec n) (k : Nat), P a k`.
1140#[allow(dead_code)]
1141pub fn bvx_ext_forall_bv_nat(body_builder: impl Fn() -> Expr) -> Expr {
1142    pi(
1143        BinderInfo::Implicit,
1144        "n",
1145        nat_ty(),
1146        pi(
1147            BinderInfo::Default,
1148            "a",
1149            mk_bitvec(bvar(0)),
1150            pi(BinderInfo::Default, "k", nat_ty(), body_builder()),
1151        ),
1152    )
1153}
1154/// Build `∀ (n : Nat) (a : BitVec n), P n a`.
1155#[allow(dead_code)]
1156pub fn bvx_ext_forall_nat_bv(body_builder: impl Fn() -> Expr) -> Expr {
1157    pi(
1158        BinderInfo::Default,
1159        "n",
1160        nat_ty(),
1161        pi(BinderInfo::Default, "a", mk_bitvec(bvar(0)), body_builder()),
1162    )
1163}
1164/// BV equality shorthand for bvar indices `(a_idx, b_idx)` under width bvar `n_idx`.
1165#[allow(dead_code)]
1166pub fn bvx_ext_bveq(n_idx: u32, a_idx: u32, b_idx: u32) -> Expr {
1167    mk_bv_eq(bvar(n_idx), bvar(a_idx), bvar(b_idx))
1168}
1169/// Nat equality `Eq Nat lhs rhs`.
1170#[allow(dead_code)]
1171pub fn bvx_ext_nateq(lhs: Expr, rhs: Expr) -> Expr {
1172    mk_nat_eq(lhs, rhs)
1173}
1174/// Build `BitVec.arithShiftRight : {n : Nat} → BitVec n → Nat → BitVec n`.
1175#[allow(dead_code)]
1176pub fn bvx_ext_arith_shift_right_ty() -> Expr {
1177    bitvec_shift_ty()
1178}
1179/// Build type for `popcount : {n : Nat} → BitVec n → Nat`.
1180#[allow(dead_code)]
1181pub fn bvx_ext_popcount_ty() -> Expr {
1182    pi(
1183        BinderInfo::Implicit,
1184        "n",
1185        nat_ty(),
1186        arrow(mk_bitvec(bvar(0)), nat_ty()),
1187    )
1188}
1189/// Build type for `clz/ctz : {n : Nat} → BitVec n → Nat`.
1190#[allow(dead_code)]
1191pub fn bvx_ext_count_zeros_ty() -> Expr {
1192    pi(
1193        BinderInfo::Implicit,
1194        "n",
1195        nat_ty(),
1196        arrow(mk_bitvec(bvar(0)), nat_ty()),
1197    )
1198}
1199/// Build type for `reverse : {n : Nat} → BitVec n → BitVec n`.
1200#[allow(dead_code)]
1201pub fn bvx_ext_reverse_ty() -> Expr {
1202    bitvec_unop_ty()
1203}
1204/// Build `∀ {n} (a b : BitVec n), a = b ↔ (∀ i < n, getLsb a i = getLsb b i)`.
1205/// Simplified as a Prop-valued type.
1206#[allow(dead_code)]
1207pub fn bvx_ext_ext_ty() -> Expr {
1208    bvx_ext_forall_two(|| bvx_ext_bveq(2, 1, 0))
1209}
1210/// Zero-extension type: `{n : Nat} → (m : Nat) → BitVec n → BitVec m`.
1211#[allow(dead_code)]
1212pub fn bvx_ext_zero_extend_ty() -> Expr {
1213    pi(
1214        BinderInfo::Implicit,
1215        "n",
1216        nat_ty(),
1217        pi(
1218            BinderInfo::Default,
1219            "m",
1220            nat_ty(),
1221            arrow(mk_bitvec(bvar(1)), mk_bitvec(bvar(0))),
1222        ),
1223    )
1224}
1225/// Concatenation result type helper: `BitVec (Nat.add n m)`.
1226#[allow(dead_code)]
1227pub fn bvx_ext_concat_result(n_bvar: u32, m_bvar: u32) -> Expr {
1228    mk_bitvec(app2(cst("Nat.add"), bvar(n_bvar), bvar(m_bvar)))
1229}
1230/// Build `Fin (Nat.pow 2 n)` type expression.
1231#[allow(dead_code)]
1232pub fn bvx_ext_fin2n(n: Expr) -> Expr {
1233    app(
1234        cst("Fin"),
1235        app2(
1236            cst("Nat.pow"),
1237            app(cst("Nat.succ"), app(cst("Nat.succ"), cst("Nat.zero"))),
1238            n,
1239        ),
1240    )
1241}
1242/// Build `Int` constant.
1243#[allow(dead_code)]
1244pub fn bvx_ext_int() -> Expr {
1245    int_ty()
1246}
1247/// Build `Nat` constant.
1248#[allow(dead_code)]
1249pub fn bvx_ext_nat() -> Expr {
1250    nat_ty()
1251}
oxilean_std/bitvec/functions.rs

oxilean_std/bitvec/
functions.rs
