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

oxilean_std/bitvec/
functions.rs
