Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: bug_7854.v Sprache: Coq

Original von: Coq^©

Require Import Coq.ZArith.ZArith.
Require Import Coq.micromega.Lia.

Local Open Scope Z_scope.

Definition Register := Z%type.

Definition Opcode := Z%type.

Inductive InstructionI : Type
  := Lb : Register -> Register -> Z -> InstructionI
  |  InvalidI : InstructionI.

Inductive Instruction : Type
  := IInstruction : InstructionI -> Instruction.

Definition funct3_LB : Z := 0.

Definition opcode_LOAD : Opcode := 3.

Set Universe Polymorphism.

Definition MachineInt := Z.

Definition funct3_JALR := 0.

Axiom InstructionMapper: Type -> Type.

Definition apply_InstructionMapper(mapper: InstructionMapper Z)(inst: Instruction): Z :=
  match inst with
  | IInstruction   InvalidI   => 2
  | IInstruction   (Lb  rd rs1 oimm12) => 3
   end.

Axiom Encoder: InstructionMapper MachineInt.

Definition encode: Instruction -> MachineInt := apply_InstructionMapper Encoder.

Lemma foo: forall (ins: InstructionI),
    0 <= encode (IInstruction ins) ->
    0 <= encode (IInstruction ins) .
Proof.
  Set Printing Universes.
  intros.
  lia.
Qed.

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
Eigene Datei ansehen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.